============================== FOF-Prover9 =========================== FOF-Prover9 (32) version 2008-05A, May 2008. Process 21812 was started by mccune on cleo, Wed May 7 22:14:46 2008 The command was "/home/mccune/LADR/bin/fof-prover9 -f MGT025+1.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file MGT025+1.in assign(max_seconds,30). set(prolog_style_variables). formulas(assumptions). (all E all X all T (environment(E) & subpopulation(X,E,T) & (greater(cardinality_at_time(X,T),zero) -> X = efficient_producers | X = first_movers) -> number_of_organizations(E,T) = sum(cardinality_at_time(first_movers,T),cardinality_at_time(efficient_producers,T)))). (all E all T (environment(E) & in_environment(E,T) -> subpopulation(first_movers,E,T) & subpopulation(efficient_producers,E,T))). (all A all B all C (A = sum(B,C) & constant(A) -> constant(B) & constant(C) | increases(B) & decreases(C) | decreases(B) & increases(C))). (all X all E all T (environment(E) & in_environment(E,T) & subpopulation(X,E,T) & greater(cardinality_at_time(X,T),zero) -> (constant(cardinality_at_time(X,T)) -> growth_rate(X,T) = zero) & (increases(cardinality_at_time(X,T)) -> greater(growth_rate(X,T),zero)) & (decreases(cardinality_at_time(X,T)) -> greater(zero,growth_rate(X,T))))). (all E all T (environment(E) & subpopulations(first_movers,efficient_producers,E,T) -> greater(cardinality_at_time(first_movers,T),zero) & greater(cardinality_at_time(efficient_producers,T),zero))). (all E all T (environment(E) & subpopulations(first_movers,efficient_producers,E,T) -> in_environment(E,T))). (all E all X all T (environment(E) & subpopulation(X,E,T) & greater(cardinality_at_time(X,T),zero) -> X = efficient_producers | X = first_movers)). -(all E all T (environment(E) & subpopulations(first_movers,efficient_producers,E,T) & constant(number_of_organizations(E,T)) -> growth_rate(first_movers,T) = zero & growth_rate(efficient_producers,T) = zero | greater(growth_rate(first_movers,T),zero) & greater(zero,growth_rate(efficient_producers,T)) | greater(growth_rate(efficient_producers,T),zero) & greater(zero,growth_rate(first_movers,T)))). end_of_list. ============================== end of input ========================== % clear(auto_denials), because it is incompatiable with FOF reduction. Attempting problem reduction; original problem has = <133,26>. Problem reduction (0.00 sec) gives 8 independent subproblems: ( <263,26> <263,26> <263,26> <263,26> <263,26> <263,26> <263,26> <263,26> ). Max nnf_size of subproblems is 263; max cnf_max is 26. ============================== FOF REDUCTION MULTISEARCH ============= Subproblem 1 of 8 (negated): ((all E (- environment(E) | (all X ((all T (- subpopulation(X,E,T) | greater(cardinality_at_time(X,T),zero) | =(sum(cardinality_at_time(first_movers,T),cardinality_at_time(efficient_producers,T)),number_of_organizations(E,T)))))))) & (all E (- environment(E) | (all X (- =(efficient_producers,X) | (all T (- subpopulation(X,E,T) | =(sum(cardinality_at_time(first_movers,T),cardinality_at_time(efficient_producers,T)),number_of_organizations(E,T)))))))) & (all E (- environment(E) | (all X (- =(first_movers,X) | (all T (- subpopulation(X,E,T) | =(sum(cardinality_at_time(first_movers,T),cardinality_at_time(efficient_producers,T)),number_of_organizations(E,T)))))))) & (all E (- environment(E) | (all T (- in_environment(E,T) | subpopulation(first_movers,E,T))))) & (all E (- environment(E) | (all T (- in_environment(E,T) | subpopulation(efficient_producers,E,T))))) & (all A (- constant(A) | (all B (constant(B) | increases(B) | decreases(B) | (all C (- =(sum(B,C),A))))))) & (all A (- constant(A) | (all B (constant(B) | increases(B) | (all C (- =(sum(B,C),A) | increases(C))))))) & (all A (- constant(A) | (all B (constant(B) | decreases(B) | (all C (- =(sum(B,C),A) | decreases(C))))))) & (all A (- constant(A) | (all B (constant(B) | (all C (- =(sum(B,C),A) | decreases(C) | increases(C))))))) & (all A (- constant(A) | (all B (increases(B) | decreases(B) | (all C (- =(sum(B,C),A) | constant(C))))))) & (all A (- constant(A) | (all B (increases(B) | (all C (- =(sum(B,C),A) | constant(C) | increases(C))))))) & (all A (- constant(A) | (all B (decreases(B) | (all C (- =(sum(B,C),A) | constant(C) | decreases(C))))))) & (all A (- constant(A) | (all B ((all C (- =(sum(B,C),A) | constant(C) | decreases(C) | increases(C))))))) & (all X (all E (- environment(E) | (all T (- in_environment(E,T) | - subpopulation(X,E,T) | - greater(cardinality_at_time(X,T),zero) | - constant(cardinality_at_time(X,T)) | =(growth_rate(X,T),zero)))))) & (all X (all E (- environment(E) | (all T (- in_environment(E,T) | - subpopulation(X,E,T) | - greater(cardinality_at_time(X,T),zero) | - increases(cardinality_at_time(X,T)) | greater(growth_rate(X,T),zero)))))) & (all X (all E (- environment(E) | (all T (- in_environment(E,T) | - subpopulation(X,E,T) | - greater(cardinality_at_time(X,T),zero) | - decreases(cardinality_at_time(X,T)) | greater(zero,growth_rate(X,T))))))) & (all E (- environment(E) | (all T (- subpopulations(first_movers,efficient_producers,E,T) | greater(cardinality_at_time(first_movers,T),zero))))) & (all E (- environment(E) | (all T (- subpopulations(first_movers,efficient_producers,E,T) | greater(cardinality_at_time(efficient_producers,T),zero))))) & (all E (- environment(E) | (all T (- subpopulations(first_movers,efficient_producers,E,T) | in_environment(E,T))))) & (all E (- environment(E) | (all X (=(efficient_producers,X) | =(first_movers,X) | (all T (- subpopulation(X,E,T) | - greater(cardinality_at_time(X,T),zero))))))) & (exists E (environment(E) & (exists T (subpopulations(first_movers,efficient_producers,E,T) & constant(number_of_organizations(E,T)) & - =(growth_rate(first_movers,T),zero) & - greater(growth_rate(first_movers,T),zero) & - greater(growth_rate(efficient_producers,T),zero)))))). Max_seconds is 30 for this subproblem. Child search process 21813 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). -environment(A) | -subpopulation(B,A,C) | greater(cardinality_at_time(B,C),zero) | sum(cardinality_at_time(first_movers,C),cardinality_at_time(efficient_producers,C)) = number_of_organizations(A,C). [assumption]. -environment(A) | efficient_producers != B | -subpopulation(B,A,C) | sum(cardinality_at_time(first_movers,C),cardinality_at_time(efficient_producers,C)) = number_of_organizations(A,C). [assumption]. -environment(A) | first_movers != B | -subpopulation(B,A,C) | sum(cardinality_at_time(first_movers,C),cardinality_at_time(efficient_producers,C)) = number_of_organizations(A,C). [assumption]. -environment(A) | -in_environment(A,B) | subpopulation(first_movers,A,B). [assumption]. -environment(A) | -in_environment(A,B) | subpopulation(efficient_producers,A,B). [assumption]. -constant(A) | constant(B) | increases(B) | decreases(B) | sum(B,C) != A. [assumption]. -constant(A) | constant(B) | increases(B) | sum(B,C) != A | increases(C). [assumption]. -constant(A) | constant(B) | decreases(B) | sum(B,C) != A | decreases(C). [assumption]. -constant(A) | constant(B) | sum(B,C) != A | decreases(C) | increases(C). [assumption]. -constant(A) | increases(B) | decreases(B) | sum(B,C) != A | constant(C). [assumption]. -constant(A) | increases(B) | sum(B,C) != A | constant(C) | increases(C). [assumption]. -constant(A) | decreases(B) | sum(B,C) != A | constant(C) | decreases(C). [assumption]. -constant(A) | sum(B,C) != A | constant(C) | decreases(C) | increases(C). [assumption]. -environment(A) | -in_environment(A,B) | -subpopulation(C,A,B) | -greater(cardinality_at_time(C,B),zero) | -constant(cardinality_at_time(C,B)) | growth_rate(C,B) = zero. [assumption]. -environment(A) | -in_environment(A,B) | -subpopulation(C,A,B) | -greater(cardinality_at_time(C,B),zero) | -increases(cardinality_at_time(C,B)) | greater(growth_rate(C,B),zero). [assumption]. -environment(A) | -in_environment(A,B) | -subpopulation(C,A,B) | -greater(cardinality_at_time(C,B),zero) | -decreases(cardinality_at_time(C,B)) | greater(zero,growth_rate(C,B)). [assumption]. -environment(A) | -subpopulations(first_movers,efficient_producers,A,B) | greater(cardinality_at_time(first_movers,B),zero). [assumption]. -environment(A) | -subpopulations(first_movers,efficient_producers,A,B) | greater(cardinality_at_time(efficient_producers,B),zero). [assumption]. -environment(A) | -subpopulations(first_movers,efficient_producers,A,B) | in_environment(A,B). [assumption]. -environment(A) | efficient_producers = B | first_movers = B | -subpopulation(B,A,C) | -greater(cardinality_at_time(B,C),zero). [assumption]. environment(c1). [assumption]. subpopulations(first_movers,efficient_producers,c1,c2). [assumption]. constant(number_of_organizations(c1,c2)). [assumption]. growth_rate(first_movers,c2) != zero. [assumption]. -greater(growth_rate(first_movers,c2),zero). [assumption]. -greater(growth_rate(efficient_producers,c2),zero). [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= Eliminating environment/1 1 environment(c1). [assumption]. 2 -environment(A) | -subpopulation(B,A,C) | greater(cardinality_at_time(B,C),zero) | sum(cardinality_at_time(first_movers,C),cardinality_at_time(efficient_producers,C)) = number_of_organizations(A,C). [assumption]. 3 -environment(A) | efficient_producers != B | -subpopulation(B,A,C) | sum(cardinality_at_time(first_movers,C),cardinality_at_time(efficient_producers,C)) = number_of_organizations(A,C). [assumption]. 4 -environment(A) | first_movers != B | -subpopulation(B,A,C) | sum(cardinality_at_time(first_movers,C),cardinality_at_time(efficient_producers,C)) = number_of_organizations(A,C). [assumption]. 5 -environment(A) | -in_environment(A,B) | subpopulation(first_movers,A,B). [assumption]. 6 -environment(A) | -in_environment(A,B) | subpopulation(efficient_producers,A,B). [assumption]. 7 -environment(A) | -in_environment(A,B) | -subpopulation(C,A,B) | -greater(cardinality_at_time(C,B),zero) | -constant(cardinality_at_time(C,B)) | growth_rate(C,B) = zero. [assumption]. 8 -environment(A) | -in_environment(A,B) | -subpopulation(C,A,B) | -greater(cardinality_at_time(C,B),zero) | -increases(cardinality_at_time(C,B)) | greater(growth_rate(C,B),zero). [assumption]. 9 -environment(A) | -in_environment(A,B) | -subpopulation(C,A,B) | -greater(cardinality_at_time(C,B),zero) | -decreases(cardinality_at_time(C,B)) | greater(zero,growth_rate(C,B)). [assumption]. 10 -environment(A) | -subpopulations(first_movers,efficient_producers,A,B) | greater(cardinality_at_time(first_movers,B),zero). [assumption]. 11 -environment(A) | -subpopulations(first_movers,efficient_producers,A,B) | greater(cardinality_at_time(efficient_producers,B),zero). [assumption]. 12 -environment(A) | -subpopulations(first_movers,efficient_producers,A,B) | in_environment(A,B). [assumption]. 13 -environment(A) | efficient_producers = B | first_movers = B | -subpopulation(B,A,C) | -greater(cardinality_at_time(B,C),zero). [assumption]. Derived: -subpopulation(A,c1,B) | greater(cardinality_at_time(A,B),zero) | sum(cardinality_at_time(first_movers,B),cardinality_at_time(efficient_producers,B)) = number_of_organizations(c1,B). [resolve(1,a,2,a)]. Derived: efficient_producers != A | -subpopulation(A,c1,B) | sum(cardinality_at_time(first_movers,B),cardinality_at_time(efficient_producers,B)) = number_of_organizations(c1,B). [resolve(1,a,3,a)]. Derived: first_movers != A | -subpopulation(A,c1,B) | sum(cardinality_at_time(first_movers,B),cardinality_at_time(efficient_producers,B)) = number_of_organizations(c1,B). [resolve(1,a,4,a)]. Derived: -in_environment(c1,A) | subpopulation(first_movers,c1,A). [resolve(1,a,5,a)]. Derived: -in_environment(c1,A) | subpopulation(efficient_producers,c1,A). [resolve(1,a,6,a)]. Derived: -in_environment(c1,A) | -subpopulation(B,c1,A) | -greater(cardinality_at_time(B,A),zero) | -constant(cardinality_at_time(B,A)) | growth_rate(B,A) = zero. [resolve(1,a,7,a)]. Derived: -in_environment(c1,A) | -subpopulation(B,c1,A) | -greater(cardinality_at_time(B,A),zero) | -increases(cardinality_at_time(B,A)) | greater(growth_rate(B,A),zero). [resolve(1,a,8,a)]. Derived: -in_environment(c1,A) | -subpopulation(B,c1,A) | -greater(cardinality_at_time(B,A),zero) | -decreases(cardinality_at_time(B,A)) | greater(zero,growth_rate(B,A)). [resolve(1,a,9,a)]. Derived: -subpopulations(first_movers,efficient_producers,c1,A) | greater(cardinality_at_time(first_movers,A),zero). [resolve(1,a,10,a)]. Derived: -subpopulations(first_movers,efficient_producers,c1,A) | greater(cardinality_at_time(efficient_producers,A),zero). [resolve(1,a,11,a)]. Derived: -subpopulations(first_movers,efficient_producers,c1,A) | in_environment(c1,A). [resolve(1,a,12,a)]. Derived: efficient_producers = A | first_movers = A | -subpopulation(A,c1,B) | -greater(cardinality_at_time(A,B),zero). [resolve(1,a,13,a)]. ============================== end predicate elimination ============= Term ordering decisions: Predicate symbol precedence: predicate_order([ =, constant, decreases, increases, greater, in_environment, subpopulation, subpopulations ]). Function symbol precedence: function_order([ efficient_producers, first_movers, zero, c1, c2, cardinality_at_time, sum, number_of_organizations, growth_rate ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(binary_resolution). % (non-Horn) % set(neg_ur_resolution). % (non-Horn, less than 100 clauses) Auto_process settings: % set(factor). % (non-Horn) % set(unit_deletion). % (non-Horn) ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 14 -constant(A) | constant(B) | increases(B) | decreases(B) | sum(B,C) != A. [assumption]. 15 -constant(A) | constant(B) | increases(B) | sum(B,C) != A | increases(C). [assumption]. 16 -constant(A) | constant(B) | decreases(B) | sum(B,C) != A | decreases(C). [assumption]. 17 -constant(A) | constant(B) | sum(B,C) != A | decreases(C) | increases(C). [assumption]. 18 -constant(A) | increases(B) | decreases(B) | sum(B,C) != A | constant(C). [assumption]. 19 -constant(A) | increases(B) | sum(B,C) != A | constant(C) | increases(C). [assumption]. 20 -constant(A) | decreases(B) | sum(B,C) != A | constant(C) | decreases(C). [assumption]. 21 -constant(A) | sum(B,C) != A | constant(C) | decreases(C) | increases(C). [assumption]. 22 subpopulations(first_movers,efficient_producers,c1,c2). [assumption]. 23 constant(number_of_organizations(c1,c2)). [assumption]. 24 growth_rate(first_movers,c2) != zero. [assumption]. 25 -greater(growth_rate(first_movers,c2),zero). [assumption]. 26 -greater(growth_rate(efficient_producers,c2),zero). [assumption]. 28 -subpopulation(A,c1,B) | greater(cardinality_at_time(A,B),zero) | number_of_organizations(c1,B) = sum(cardinality_at_time(first_movers,B),cardinality_at_time(efficient_producers,B)). [copy(27),flip(c)]. 30 efficient_producers != A | -subpopulation(A,c1,B) | number_of_organizations(c1,B) = sum(cardinality_at_time(first_movers,B),cardinality_at_time(efficient_producers,B)). [copy(29),flip(c)]. 32 first_movers != A | -subpopulation(A,c1,B) | number_of_organizations(c1,B) = sum(cardinality_at_time(first_movers,B),cardinality_at_time(efficient_producers,B)). [copy(31),flip(c)]. 33 -in_environment(c1,A) | subpopulation(first_movers,c1,A). [resolve(1,a,5,a)]. 34 -in_environment(c1,A) | subpopulation(efficient_producers,c1,A). [resolve(1,a,6,a)]. 35 -in_environment(c1,A) | -subpopulation(B,c1,A) | -greater(cardinality_at_time(B,A),zero) | -constant(cardinality_at_time(B,A)) | growth_rate(B,A) = zero. [resolve(1,a,7,a)]. 36 -in_environment(c1,A) | -subpopulation(B,c1,A) | -greater(cardinality_at_time(B,A),zero) | -increases(cardinality_at_time(B,A)) | greater(growth_rate(B,A),zero). [resolve(1,a,8,a)]. 37 -in_environment(c1,A) | -subpopulation(B,c1,A) | -greater(cardinality_at_time(B,A),zero) | -decreases(cardinality_at_time(B,A)) | greater(zero,growth_rate(B,A)). [resolve(1,a,9,a)]. 38 -subpopulations(first_movers,efficient_producers,c1,A) | greater(cardinality_at_time(first_movers,A),zero). [resolve(1,a,10,a)]. 39 -subpopulations(first_movers,efficient_producers,c1,A) | greater(cardinality_at_time(efficient_producers,A),zero). [resolve(1,a,11,a)]. 40 -subpopulations(first_movers,efficient_producers,c1,A) | in_environment(c1,A). [resolve(1,a,12,a)]. 41 efficient_producers = A | first_movers = A | -subpopulation(A,c1,B) | -greater(cardinality_at_time(A,B),zero). [resolve(1,a,13,a)]. 42 -constant(A) | constant(B) | increases(B) | sum(B,B) != A. [factor(15,c,e)]. 43 -constant(A) | constant(B) | decreases(B) | sum(B,B) != A. [factor(16,c,e)]. end_of_list. formulas(demodulators). end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=13): 14 -constant(A) | constant(B) | increases(B) | decreases(B) | sum(B,C) != A. [assumption]. given #2 (I,wt=13): 15 -constant(A) | constant(B) | increases(B) | sum(B,C) != A | increases(C). [assumption]. given #3 (I,wt=13): 16 -constant(A) | constant(B) | decreases(B) | sum(B,C) != A | decreases(C). [assumption]. given #4 (I,wt=13): 17 -constant(A) | constant(B) | sum(B,C) != A | decreases(C) | increases(C). [assumption]. given #5 (I,wt=13): 18 -constant(A) | increases(B) | decreases(B) | sum(B,C) != A | constant(C). [assumption]. given #6 (I,wt=13): 19 -constant(A) | increases(B) | sum(B,C) != A | constant(C) | increases(C). [assumption]. given #7 (I,wt=13): 20 -constant(A) | decreases(B) | sum(B,C) != A | constant(C) | decreases(C). [assumption]. given #8 (I,wt=13): 21 -constant(A) | sum(B,C) != A | constant(C) | decreases(C) | increases(C). [assumption]. given #9 (I,wt=5): 22 subpopulations(first_movers,efficient_producers,c1,c2). [assumption]. given #10 (I,wt=4): 23 constant(number_of_organizations(c1,c2)). [assumption]. given #11 (I,wt=5): 24 growth_rate(first_movers,c2) != zero. [assumption]. given #12 (I,wt=5): 25 -greater(growth_rate(first_movers,c2),zero). [assumption]. given #13 (I,wt=5): 26 -greater(growth_rate(efficient_producers,c2),zero). [assumption]. given #14 (I,wt=20): 28 -subpopulation(A,c1,B) | greater(cardinality_at_time(A,B),zero) | number_of_organizations(c1,B) = sum(cardinality_at_time(first_movers,B),cardinality_at_time(efficient_producers,B)). [copy(27),flip(c)]. given #15 (I,wt=18): 30 efficient_producers != A | -subpopulation(A,c1,B) | number_of_organizations(c1,B) = sum(cardinality_at_time(first_movers,B),cardinality_at_time(efficient_producers,B)). [copy(29),flip(c)]. given #16 (I,wt=18): 32 first_movers != A | -subpopulation(A,c1,B) | number_of_organizations(c1,B) = sum(cardinality_at_time(first_movers,B),cardinality_at_time(efficient_producers,B)). [copy(31),flip(c)]. given #17 (I,wt=7): 33 -in_environment(c1,A) | subpopulation(first_movers,c1,A). [resolve(1,a,5,a)]. given #18 (I,wt=7): 34 -in_environment(c1,A) | subpopulation(efficient_producers,c1,A). [resolve(1,a,6,a)]. given #19 (I,wt=21): 35 -in_environment(c1,A) | -subpopulation(B,c1,A) | -greater(cardinality_at_time(B,A),zero) | -constant(cardinality_at_time(B,A)) | growth_rate(B,A) = zero. [resolve(1,a,7,a)]. given #20 (I,wt=21): 36 -in_environment(c1,A) | -subpopulation(B,c1,A) | -greater(cardinality_at_time(B,A),zero) | -increases(cardinality_at_time(B,A)) | greater(growth_rate(B,A),zero). [resolve(1,a,8,a)]. given #21 (I,wt=21): 37 -in_environment(c1,A) | -subpopulation(B,c1,A) | -greater(cardinality_at_time(B,A),zero) | -decreases(cardinality_at_time(B,A)) | greater(zero,growth_rate(B,A)). [resolve(1,a,9,a)]. given #22 (I,wt=10): 38 -subpopulations(first_movers,efficient_producers,c1,A) | greater(cardinality_at_time(first_movers,A),zero). [resolve(1,a,10,a)]. given #23 (I,wt=10): 39 -subpopulations(first_movers,efficient_producers,c1,A) | greater(cardinality_at_time(efficient_producers,A),zero). [resolve(1,a,11,a)]. given #24 (I,wt=8): 40 -subpopulations(first_movers,efficient_producers,c1,A) | in_environment(c1,A). [resolve(1,a,12,a)]. given #25 (I,wt=15): 41 efficient_producers = A | first_movers = A | -subpopulation(A,c1,B) | -greater(cardinality_at_time(A,B),zero). [resolve(1,a,13,a)]. given #26 (I,wt=11): 42 -constant(A) | constant(B) | increases(B) | sum(B,B) != A. [factor(15,c,e)]. given #27 (I,wt=11): 43 -constant(A) | constant(B) | decreases(B) | sum(B,B) != A. [factor(16,c,e)]. given #28 (A,wt=13): 44 sum(A,B) != number_of_organizations(c1,c2) | constant(B) | decreases(B) | increases(B). [resolve(23,a,21,a)]. given #29 (T,wt=3): 56 in_environment(c1,c2). [resolve(40,a,22,a)]. given #30 (T,wt=4): 57 subpopulation(efficient_producers,c1,c2). [resolve(56,a,34,a)]. given #31 (T,wt=4): 58 subpopulation(first_movers,c1,c2). [resolve(56,a,33,a)]. given #32 (T,wt=5): 54 greater(cardinality_at_time(first_movers,c2),zero). [resolve(38,a,22,a)]. given #33 (A,wt=5): 55 greater(cardinality_at_time(efficient_producers,c2),zero). [resolve(39,a,22,a)]. given #34 (F,wt=4): 60 -increases(cardinality_at_time(efficient_producers,c2)). [resolve(57,a,36,b),unit_del(a,56),unit_del(b,55),unit_del(d,26)]. given #35 (F,wt=4): 76 -increases(cardinality_at_time(first_movers,c2)). [resolve(58,a,36,b),unit_del(a,56),unit_del(b,54),unit_del(d,25)]. given #36 (F,wt=4): 77 -constant(cardinality_at_time(first_movers,c2)). [resolve(58,a,35,b),unit_del(a,56),unit_del(b,54),unit_del(d,24)]. ============================== PROOF ================================= % Proof 1 at 0.01 (+ 0.00) seconds. % Length of proof is 35. % Level of proof is 6. % Maximum clause weight is 21. % Given clauses 36. 1 environment(c1). [assumption]. 3 -environment(A) | efficient_producers != B | -subpopulation(B,A,C) | sum(cardinality_at_time(first_movers,C),cardinality_at_time(efficient_producers,C)) = number_of_organizations(A,C). [assumption]. 5 -environment(A) | -in_environment(A,B) | subpopulation(first_movers,A,B). [assumption]. 6 -environment(A) | -in_environment(A,B) | subpopulation(efficient_producers,A,B). [assumption]. 7 -environment(A) | -in_environment(A,B) | -subpopulation(C,A,B) | -greater(cardinality_at_time(C,B),zero) | -constant(cardinality_at_time(C,B)) | growth_rate(C,B) = zero. [assumption]. 8 -environment(A) | -in_environment(A,B) | -subpopulation(C,A,B) | -greater(cardinality_at_time(C,B),zero) | -increases(cardinality_at_time(C,B)) | greater(growth_rate(C,B),zero). [assumption]. 10 -environment(A) | -subpopulations(first_movers,efficient_producers,A,B) | greater(cardinality_at_time(first_movers,B),zero). [assumption]. 11 -environment(A) | -subpopulations(first_movers,efficient_producers,A,B) | greater(cardinality_at_time(efficient_producers,B),zero). [assumption]. 12 -environment(A) | -subpopulations(first_movers,efficient_producers,A,B) | in_environment(A,B). [assumption]. 15 -constant(A) | constant(B) | increases(B) | sum(B,C) != A | increases(C). [assumption]. 22 subpopulations(first_movers,efficient_producers,c1,c2). [assumption]. 23 constant(number_of_organizations(c1,c2)). [assumption]. 24 growth_rate(first_movers,c2) != zero. [assumption]. 25 -greater(growth_rate(first_movers,c2),zero). [assumption]. 26 -greater(growth_rate(efficient_producers,c2),zero). [assumption]. 29 efficient_producers != A | -subpopulation(A,c1,B) | sum(cardinality_at_time(first_movers,B),cardinality_at_time(efficient_producers,B)) = number_of_organizations(c1,B). [resolve(1,a,3,a)]. 30 efficient_producers != A | -subpopulation(A,c1,B) | number_of_organizations(c1,B) = sum(cardinality_at_time(first_movers,B),cardinality_at_time(efficient_producers,B)). [copy(29),flip(c)]. 33 -in_environment(c1,A) | subpopulation(first_movers,c1,A). [resolve(1,a,5,a)]. 34 -in_environment(c1,A) | subpopulation(efficient_producers,c1,A). [resolve(1,a,6,a)]. 35 -in_environment(c1,A) | -subpopulation(B,c1,A) | -greater(cardinality_at_time(B,A),zero) | -constant(cardinality_at_time(B,A)) | growth_rate(B,A) = zero. [resolve(1,a,7,a)]. 36 -in_environment(c1,A) | -subpopulation(B,c1,A) | -greater(cardinality_at_time(B,A),zero) | -increases(cardinality_at_time(B,A)) | greater(growth_rate(B,A),zero). [resolve(1,a,8,a)]. 38 -subpopulations(first_movers,efficient_producers,c1,A) | greater(cardinality_at_time(first_movers,A),zero). [resolve(1,a,10,a)]. 39 -subpopulations(first_movers,efficient_producers,c1,A) | greater(cardinality_at_time(efficient_producers,A),zero). [resolve(1,a,11,a)]. 40 -subpopulations(first_movers,efficient_producers,c1,A) | in_environment(c1,A). [resolve(1,a,12,a)]. 54 greater(cardinality_at_time(first_movers,c2),zero). [resolve(38,a,22,a)]. 55 greater(cardinality_at_time(efficient_producers,c2),zero). [resolve(39,a,22,a)]. 56 in_environment(c1,c2). [resolve(40,a,22,a)]. 57 subpopulation(efficient_producers,c1,c2). [resolve(56,a,34,a)]. 58 subpopulation(first_movers,c1,c2). [resolve(56,a,33,a)]. 60 -increases(cardinality_at_time(efficient_producers,c2)). [resolve(57,a,36,b),unit_del(a,56),unit_del(b,55),unit_del(d,26)]. 63 number_of_organizations(c1,c2) = sum(cardinality_at_time(first_movers,c2),cardinality_at_time(efficient_producers,c2)). [resolve(57,a,30,b),xx(a)]. 74 constant(sum(cardinality_at_time(first_movers,c2),cardinality_at_time(efficient_producers,c2))). [back_rewrite(23),rewrite([63(3)])]. 76 -increases(cardinality_at_time(first_movers,c2)). [resolve(58,a,36,b),unit_del(a,56),unit_del(b,54),unit_del(d,25)]. 77 -constant(cardinality_at_time(first_movers,c2)). [resolve(58,a,35,b),unit_del(a,56),unit_del(b,54),unit_del(d,24)]. 80 $F. [ur(15,b,77,a,c,76,a,d,xx,e,60,a),unit_del(a,74)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=36. Generated=85. Kept=63. proofs=1. Usable=34. Sos=15. Demods=1. Limbo=2, Disabled=50. Hints=0. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=21. Back_subsumed=1. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=1 (0 lex), Back_demodulated=11. Back_unit_deleted=0. Demod_attempts=405. Demod_rewrites=15. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=46. Nonunit_bsub_feature_tests=131. Megabytes=0.26. User_CPU=0.01, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 21813 exit (max_proofs) Wed May 7 22:14:46 2008 ============================== continuing FOF reduction multisearch == Subproblem 2 of 8 (negated): ((all E (- environment(E) | (all X ((all T (- subpopulation(X,E,T) | greater(cardinality_at_time(X,T),zero) | =(sum(cardinality_at_time(first_movers,T),cardinality_at_time(efficient_producers,T)),number_of_organizations(E,T)))))))) & (all E (- environment(E) | (all X (- =(efficient_producers,X) | (all T (- subpopulation(X,E,T) | =(sum(cardinality_at_time(first_movers,T),cardinality_at_time(efficient_producers,T)),number_of_organizations(E,T)))))))) & (all E (- environment(E) | (all X (- =(first_movers,X) | (all T (- subpopulation(X,E,T) | =(sum(cardinality_at_time(first_movers,T),cardinality_at_time(efficient_producers,T)),number_of_organizations(E,T)))))))) & (all E (- environment(E) | (all T (- in_environment(E,T) | subpopulation(first_movers,E,T))))) & (all E (- environment(E) | (all T (- in_environment(E,T) | subpopulation(efficient_producers,E,T))))) & (all A (- constant(A) | (all B (constant(B) | increases(B) | decreases(B) | (all C (- =(sum(B,C),A))))))) & (all A (- constant(A) | (all B (constant(B) | increases(B) | (all C (- =(sum(B,C),A) | increases(C))))))) & (all A (- constant(A) | (all B (constant(B) | decreases(B) | (all C (- =(sum(B,C),A) | decreases(C))))))) & (all A (- constant(A) | (all B (constant(B) | (all C (- =(sum(B,C),A) | decreases(C) | increases(C))))))) & (all A (- constant(A) | (all B (increases(B) | decreases(B) | (all C (- =(sum(B,C),A) | constant(C))))))) & (all A (- constant(A) | (all B (increases(B) | (all C (- =(sum(B,C),A) | constant(C) | increases(C))))))) & (all A (- constant(A) | (all B (decreases(B) | (all C (- =(sum(B,C),A) | constant(C) | decreases(C))))))) & (all A (- constant(A) | (all B ((all C (- =(sum(B,C),A) | constant(C) | decreases(C) | increases(C))))))) & (all X (all E (- environment(E) | (all T (- in_environment(E,T) | - subpopulation(X,E,T) | - greater(cardinality_at_time(X,T),zero) | - constant(cardinality_at_time(X,T)) | =(growth_rate(X,T),zero)))))) & (all X (all E (- environment(E) | (all T (- in_environment(E,T) | - subpopulation(X,E,T) | - greater(cardinality_at_time(X,T),zero) | - increases(cardinality_at_time(X,T)) | greater(growth_rate(X,T),zero)))))) & (all X (all E (- environment(E) | (all T (- in_environment(E,T) | - subpopulation(X,E,T) | - greater(cardinality_at_time(X,T),zero) | - decreases(cardinality_at_time(X,T)) | greater(zero,growth_rate(X,T))))))) & (all E (- environment(E) | (all T (- subpopulations(first_movers,efficient_producers,E,T) | greater(cardinality_at_time(first_movers,T),zero))))) & (all E (- environment(E) | (all T (- subpopulations(first_movers,efficient_producers,E,T) | greater(cardinality_at_time(efficient_producers,T),zero))))) & (all E (- environment(E) | (all T (- subpopulations(first_movers,efficient_producers,E,T) | in_environment(E,T))))) & (all E (- environment(E) | (all X (=(efficient_producers,X) | =(first_movers,X) | (all T (- subpopulation(X,E,T) | - greater(cardinality_at_time(X,T),zero))))))) & (exists E (environment(E) & (exists T (subpopulations(first_movers,efficient_producers,E,T) & constant(number_of_organizations(E,T)) & - =(growth_rate(first_movers,T),zero) & - greater(growth_rate(first_movers,T),zero) & - greater(zero,growth_rate(first_movers,T))))))). Max_seconds is 30 for this subproblem. Child search process 21814 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). -environment(A) | -subpopulation(B,A,C) | greater(cardinality_at_time(B,C),zero) | sum(cardinality_at_time(first_movers,C),cardinality_at_time(efficient_producers,C)) = number_of_organizations(A,C). [assumption]. -environment(A) | efficient_producers != B | -subpopulation(B,A,C) | sum(cardinality_at_time(first_movers,C),cardinality_at_time(efficient_producers,C)) = number_of_organizations(A,C). [assumption]. -environment(A) | first_movers != B | -subpopulation(B,A,C) | sum(cardinality_at_time(first_movers,C),cardinality_at_time(efficient_producers,C)) = number_of_organizations(A,C). [assumption]. -environment(A) | -in_environment(A,B) | subpopulation(first_movers,A,B). [assumption]. -environment(A) | -in_environment(A,B) | subpopulation(efficient_producers,A,B). [assumption]. -constant(A) | constant(B) | increases(B) | decreases(B) | sum(B,C) != A. [assumption]. -constant(A) | constant(B) | increases(B) | sum(B,C) != A | increases(C). [assumption]. -constant(A) | constant(B) | decreases(B) | sum(B,C) != A | decreases(C). [assumption]. -constant(A) | constant(B) | sum(B,C) != A | decreases(C) | increases(C). [assumption]. -constant(A) | increases(B) | decreases(B) | sum(B,C) != A | constant(C). [assumption]. -constant(A) | increases(B) | sum(B,C) != A | constant(C) | increases(C). [assumption]. -constant(A) | decreases(B) | sum(B,C) != A | constant(C) | decreases(C). [assumption]. -constant(A) | sum(B,C) != A | constant(C) | decreases(C) | increases(C). [assumption]. -environment(A) | -in_environment(A,B) | -subpopulation(C,A,B) | -greater(cardinality_at_time(C,B),zero) | -constant(cardinality_at_time(C,B)) | growth_rate(C,B) = zero. [assumption]. -environment(A) | -in_environment(A,B) | -subpopulation(C,A,B) | -greater(cardinality_at_time(C,B),zero) | -increases(cardinality_at_time(C,B)) | greater(growth_rate(C,B),zero). [assumption]. -environment(A) | -in_environment(A,B) | -subpopulation(C,A,B) | -greater(cardinality_at_time(C,B),zero) | -decreases(cardinality_at_time(C,B)) | greater(zero,growth_rate(C,B)). [assumption]. -environment(A) | -subpopulations(first_movers,efficient_producers,A,B) | greater(cardinality_at_time(first_movers,B),zero). [assumption]. -environment(A) | -subpopulations(first_movers,efficient_producers,A,B) | greater(cardinality_at_time(efficient_producers,B),zero). [assumption]. -environment(A) | -subpopulations(first_movers,efficient_producers,A,B) | in_environment(A,B). [assumption]. -environment(A) | efficient_producers = B | first_movers = B | -subpopulation(B,A,C) | -greater(cardinality_at_time(B,C),zero). [assumption]. environment(c1). [assumption]. subpopulations(first_movers,efficient_producers,c1,c2). [assumption]. constant(number_of_organizations(c1,c2)). [assumption]. growth_rate(first_movers,c2) != zero. [assumption]. -greater(growth_rate(first_movers,c2),zero). [assumption]. -greater(zero,growth_rate(first_movers,c2)). [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= Eliminating environment/1 1 environment(c1). [assumption]. 2 -environment(A) | -subpopulation(B,A,C) | greater(cardinality_at_time(B,C),zero) | sum(cardinality_at_time(first_movers,C),cardinality_at_time(efficient_producers,C)) = number_of_organizations(A,C). [assumption]. 3 -environment(A) | efficient_producers != B | -subpopulation(B,A,C) | sum(cardinality_at_time(first_movers,C),cardinality_at_time(efficient_producers,C)) = number_of_organizations(A,C). [assumption]. 4 -environment(A) | first_movers != B | -subpopulation(B,A,C) | sum(cardinality_at_time(first_movers,C),cardinality_at_time(efficient_producers,C)) = number_of_organizations(A,C). [assumption]. 5 -environment(A) | -in_environment(A,B) | subpopulation(first_movers,A,B). [assumption]. 6 -environment(A) | -in_environment(A,B) | subpopulation(efficient_producers,A,B). [assumption]. 7 -environment(A) | -in_environment(A,B) | -subpopulation(C,A,B) | -greater(cardinality_at_time(C,B),zero) | -constant(cardinality_at_time(C,B)) | growth_rate(C,B) = zero. [assumption]. 8 -environment(A) | -in_environment(A,B) | -subpopulation(C,A,B) | -greater(cardinality_at_time(C,B),zero) | -increases(cardinality_at_time(C,B)) | greater(growth_rate(C,B),zero). [assumption]. 9 -environment(A) | -in_environment(A,B) | -subpopulation(C,A,B) | -greater(cardinality_at_time(C,B),zero) | -decreases(cardinality_at_time(C,B)) | greater(zero,growth_rate(C,B)). [assumption]. 10 -environment(A) | -subpopulations(first_movers,efficient_producers,A,B) | greater(cardinality_at_time(first_movers,B),zero). [assumption]. 11 -environment(A) | -subpopulations(first_movers,efficient_producers,A,B) | greater(cardinality_at_time(efficient_producers,B),zero). [assumption]. 12 -environment(A) | -subpopulations(first_movers,efficient_producers,A,B) | in_environment(A,B). [assumption]. 13 -environment(A) | efficient_producers = B | first_movers = B | -subpopulation(B,A,C) | -greater(cardinality_at_time(B,C),zero). [assumption]. Derived: -subpopulation(A,c1,B) | greater(cardinality_at_time(A,B),zero) | sum(cardinality_at_time(first_movers,B),cardinality_at_time(efficient_producers,B)) = number_of_organizations(c1,B). [resolve(1,a,2,a)]. Derived: efficient_producers != A | -subpopulation(A,c1,B) | sum(cardinality_at_time(first_movers,B),cardinality_at_time(efficient_producers,B)) = number_of_organizations(c1,B). [resolve(1,a,3,a)]. Derived: first_movers != A | -subpopulation(A,c1,B) | sum(cardinality_at_time(first_movers,B),cardinality_at_time(efficient_producers,B)) = number_of_organizations(c1,B). [resolve(1,a,4,a)]. Derived: -in_environment(c1,A) | subpopulation(first_movers,c1,A). [resolve(1,a,5,a)]. Derived: -in_environment(c1,A) | subpopulation(efficient_producers,c1,A). [resolve(1,a,6,a)]. Derived: -in_environment(c1,A) | -subpopulation(B,c1,A) | -greater(cardinality_at_time(B,A),zero) | -constant(cardinality_at_time(B,A)) | growth_rate(B,A) = zero. [resolve(1,a,7,a)]. Derived: -in_environment(c1,A) | -subpopulation(B,c1,A) | -greater(cardinality_at_time(B,A),zero) | -increases(cardinality_at_time(B,A)) | greater(growth_rate(B,A),zero). [resolve(1,a,8,a)]. Derived: -in_environment(c1,A) | -subpopulation(B,c1,A) | -greater(cardinality_at_time(B,A),zero) | -decreases(cardinality_at_time(B,A)) | greater(zero,growth_rate(B,A)). [resolve(1,a,9,a)]. Derived: -subpopulations(first_movers,efficient_producers,c1,A) | greater(cardinality_at_time(first_movers,A),zero). [resolve(1,a,10,a)]. Derived: -subpopulations(first_movers,efficient_producers,c1,A) | greater(cardinality_at_time(efficient_producers,A),zero). [resolve(1,a,11,a)]. Derived: -subpopulations(first_movers,efficient_producers,c1,A) | in_environment(c1,A). [resolve(1,a,12,a)]. Derived: efficient_producers = A | first_movers = A | -subpopulation(A,c1,B) | -greater(cardinality_at_time(A,B),zero). [resolve(1,a,13,a)]. ============================== end predicate elimination ============= Term ordering decisions: Predicate symbol precedence: predicate_order([ =, constant, decreases, increases, greater, in_environment, subpopulation, subpopulations ]). Function symbol precedence: function_order([ efficient_producers, first_movers, zero, c1, c2, cardinality_at_time, sum, number_of_organizations, growth_rate ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(binary_resolution). % (non-Horn) % set(neg_ur_resolution). % (non-Horn, less than 100 clauses) Auto_process settings: % set(factor). % (non-Horn) % set(unit_deletion). % (non-Horn) ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 14 -constant(A) | constant(B) | increases(B) | decreases(B) | sum(B,C) != A. [assumption]. 15 -constant(A) | constant(B) | increases(B) | sum(B,C) != A | increases(C). [assumption]. 16 -constant(A) | constant(B) | decreases(B) | sum(B,C) != A | decreases(C). [assumption]. 17 -constant(A) | constant(B) | sum(B,C) != A | decreases(C) | increases(C). [assumption]. 18 -constant(A) | increases(B) | decreases(B) | sum(B,C) != A | constant(C). [assumption]. 19 -constant(A) | increases(B) | sum(B,C) != A | constant(C) | increases(C). [assumption]. 20 -constant(A) | decreases(B) | sum(B,C) != A | constant(C) | decreases(C). [assumption]. 21 -constant(A) | sum(B,C) != A | constant(C) | decreases(C) | increases(C). [assumption]. 22 subpopulations(first_movers,efficient_producers,c1,c2). [assumption]. 23 constant(number_of_organizations(c1,c2)). [assumption]. 24 growth_rate(first_movers,c2) != zero. [assumption]. 25 -greater(growth_rate(first_movers,c2),zero). [assumption]. 26 -greater(zero,growth_rate(first_movers,c2)). [assumption]. 28 -subpopulation(A,c1,B) | greater(cardinality_at_time(A,B),zero) | number_of_organizations(c1,B) = sum(cardinality_at_time(first_movers,B),cardinality_at_time(efficient_producers,B)). [copy(27),flip(c)]. 30 efficient_producers != A | -subpopulation(A,c1,B) | number_of_organizations(c1,B) = sum(cardinality_at_time(first_movers,B),cardinality_at_time(efficient_producers,B)). [copy(29),flip(c)]. 32 first_movers != A | -subpopulation(A,c1,B) | number_of_organizations(c1,B) = sum(cardinality_at_time(first_movers,B),cardinality_at_time(efficient_producers,B)). [copy(31),flip(c)]. 33 -in_environment(c1,A) | subpopulation(first_movers,c1,A). [resolve(1,a,5,a)]. 34 -in_environment(c1,A) | subpopulation(efficient_producers,c1,A). [resolve(1,a,6,a)]. 35 -in_environment(c1,A) | -subpopulation(B,c1,A) | -greater(cardinality_at_time(B,A),zero) | -constant(cardinality_at_time(B,A)) | growth_rate(B,A) = zero. [resolve(1,a,7,a)]. 36 -in_environment(c1,A) | -subpopulation(B,c1,A) | -greater(cardinality_at_time(B,A),zero) | -increases(cardinality_at_time(B,A)) | greater(growth_rate(B,A),zero). [resolve(1,a,8,a)]. 37 -in_environment(c1,A) | -subpopulation(B,c1,A) | -greater(cardinality_at_time(B,A),zero) | -decreases(cardinality_at_time(B,A)) | greater(zero,growth_rate(B,A)). [resolve(1,a,9,a)]. 38 -subpopulations(first_movers,efficient_producers,c1,A) | greater(cardinality_at_time(first_movers,A),zero). [resolve(1,a,10,a)]. 39 -subpopulations(first_movers,efficient_producers,c1,A) | greater(cardinality_at_time(efficient_producers,A),zero). [resolve(1,a,11,a)]. 40 -subpopulations(first_movers,efficient_producers,c1,A) | in_environment(c1,A). [resolve(1,a,12,a)]. 41 efficient_producers = A | first_movers = A | -subpopulation(A,c1,B) | -greater(cardinality_at_time(A,B),zero). [resolve(1,a,13,a)]. 42 -constant(A) | constant(B) | increases(B) | sum(B,B) != A. [factor(15,c,e)]. 43 -constant(A) | constant(B) | decreases(B) | sum(B,B) != A. [factor(16,c,e)]. end_of_list. formulas(demodulators). end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=13): 14 -constant(A) | constant(B) | increases(B) | decreases(B) | sum(B,C) != A. [assumption]. given #2 (I,wt=13): 15 -constant(A) | constant(B) | increases(B) | sum(B,C) != A | increases(C). [assumption]. given #3 (I,wt=13): 16 -constant(A) | constant(B) | decreases(B) | sum(B,C) != A | decreases(C). [assumption]. given #4 (I,wt=13): 17 -constant(A) | constant(B) | sum(B,C) != A | decreases(C) | increases(C). [assumption]. given #5 (I,wt=13): 18 -constant(A) | increases(B) | decreases(B) | sum(B,C) != A | constant(C). [assumption]. given #6 (I,wt=13): 19 -constant(A) | increases(B) | sum(B,C) != A | constant(C) | increases(C). [assumption]. given #7 (I,wt=13): 20 -constant(A) | decreases(B) | sum(B,C) != A | constant(C) | decreases(C). [assumption]. given #8 (I,wt=13): 21 -constant(A) | sum(B,C) != A | constant(C) | decreases(C) | increases(C). [assumption]. given #9 (I,wt=5): 22 subpopulations(first_movers,efficient_producers,c1,c2). [assumption]. given #10 (I,wt=4): 23 constant(number_of_organizations(c1,c2)). [assumption]. given #11 (I,wt=5): 24 growth_rate(first_movers,c2) != zero. [assumption]. given #12 (I,wt=5): 25 -greater(growth_rate(first_movers,c2),zero). [assumption]. given #13 (I,wt=5): 26 -greater(zero,growth_rate(first_movers,c2)). [assumption]. given #14 (I,wt=20): 28 -subpopulation(A,c1,B) | greater(cardinality_at_time(A,B),zero) | number_of_organizations(c1,B) = sum(cardinality_at_time(first_movers,B),cardinality_at_time(efficient_producers,B)). [copy(27),flip(c)]. given #15 (I,wt=18): 30 efficient_producers != A | -subpopulation(A,c1,B) | number_of_organizations(c1,B) = sum(cardinality_at_time(first_movers,B),cardinality_at_time(efficient_producers,B)). [copy(29),flip(c)]. given #16 (I,wt=18): 32 first_movers != A | -subpopulation(A,c1,B) | number_of_organizations(c1,B) = sum(cardinality_at_time(first_movers,B),cardinality_at_time(efficient_producers,B)). [copy(31),flip(c)]. given #17 (I,wt=7): 33 -in_environment(c1,A) | subpopulation(first_movers,c1,A). [resolve(1,a,5,a)]. given #18 (I,wt=7): 34 -in_environment(c1,A) | subpopulation(efficient_producers,c1,A). [resolve(1,a,6,a)]. given #19 (I,wt=21): 35 -in_environment(c1,A) | -subpopulation(B,c1,A) | -greater(cardinality_at_time(B,A),zero) | -constant(cardinality_at_time(B,A)) | growth_rate(B,A) = zero. [resolve(1,a,7,a)]. given #20 (I,wt=21): 36 -in_environment(c1,A) | -subpopulation(B,c1,A) | -greater(cardinality_at_time(B,A),zero) | -increases(cardinality_at_time(B,A)) | greater(growth_rate(B,A),zero). [resolve(1,a,8,a)]. given #21 (I,wt=21): 37 -in_environment(c1,A) | -subpopulation(B,c1,A) | -greater(cardinality_at_time(B,A),zero) | -decreases(cardinality_at_time(B,A)) | greater(zero,growth_rate(B,A)). [resolve(1,a,9,a)]. given #22 (I,wt=10): 38 -subpopulations(first_movers,efficient_producers,c1,A) | greater(cardinality_at_time(first_movers,A),zero). [resolve(1,a,10,a)]. given #23 (I,wt=10): 39 -subpopulations(first_movers,efficient_producers,c1,A) | greater(cardinality_at_time(efficient_producers,A),zero). [resolve(1,a,11,a)]. given #24 (I,wt=8): 40 -subpopulations(first_movers,efficient_producers,c1,A) | in_environment(c1,A). [resolve(1,a,12,a)]. given #25 (I,wt=15): 41 efficient_producers = A | first_movers = A | -subpopulation(A,c1,B) | -greater(cardinality_at_time(A,B),zero). [resolve(1,a,13,a)]. given #26 (I,wt=11): 42 -constant(A) | constant(B) | increases(B) | sum(B,B) != A. [factor(15,c,e)]. given #27 (I,wt=11): 43 -constant(A) | constant(B) | decreases(B) | sum(B,B) != A. [factor(16,c,e)]. given #28 (A,wt=13): 44 sum(A,B) != number_of_organizations(c1,c2) | constant(B) | decreases(B) | increases(B). [resolve(23,a,21,a)]. given #29 (T,wt=3): 56 in_environment(c1,c2). [resolve(40,a,22,a)]. given #30 (T,wt=4): 57 subpopulation(efficient_producers,c1,c2). [resolve(56,a,34,a)]. given #31 (T,wt=4): 58 subpopulation(first_movers,c1,c2). [resolve(56,a,33,a)]. given #32 (T,wt=5): 54 greater(cardinality_at_time(first_movers,c2),zero). [resolve(38,a,22,a)]. given #33 (A,wt=5): 55 greater(cardinality_at_time(efficient_producers,c2),zero). [resolve(39,a,22,a)]. given #34 (F,wt=4): 75 -decreases(cardinality_at_time(first_movers,c2)). [resolve(58,a,37,b),unit_del(a,56),unit_del(b,54),unit_del(d,26)]. given #35 (F,wt=4): 76 -increases(cardinality_at_time(first_movers,c2)). [resolve(58,a,36,b),unit_del(a,56),unit_del(b,54),unit_del(d,25)]. given #36 (F,wt=4): 77 -constant(cardinality_at_time(first_movers,c2)). [resolve(58,a,35,b),unit_del(a,56),unit_del(b,54),unit_del(d,24)]. ============================== PROOF ================================= % Proof 1 at 0.00 (+ 0.00) seconds. % Length of proof is 35. % Level of proof is 6. % Maximum clause weight is 21. % Given clauses 36. 1 environment(c1). [assumption]. 3 -environment(A) | efficient_producers != B | -subpopulation(B,A,C) | sum(cardinality_at_time(first_movers,C),cardinality_at_time(efficient_producers,C)) = number_of_organizations(A,C). [assumption]. 5 -environment(A) | -in_environment(A,B) | subpopulation(first_movers,A,B). [assumption]. 6 -environment(A) | -in_environment(A,B) | subpopulation(efficient_producers,A,B). [assumption]. 7 -environment(A) | -in_environment(A,B) | -subpopulation(C,A,B) | -greater(cardinality_at_time(C,B),zero) | -constant(cardinality_at_time(C,B)) | growth_rate(C,B) = zero. [assumption]. 8 -environment(A) | -in_environment(A,B) | -subpopulation(C,A,B) | -greater(cardinality_at_time(C,B),zero) | -increases(cardinality_at_time(C,B)) | greater(growth_rate(C,B),zero). [assumption]. 9 -environment(A) | -in_environment(A,B) | -subpopulation(C,A,B) | -greater(cardinality_at_time(C,B),zero) | -decreases(cardinality_at_time(C,B)) | greater(zero,growth_rate(C,B)). [assumption]. 10 -environment(A) | -subpopulations(first_movers,efficient_producers,A,B) | greater(cardinality_at_time(first_movers,B),zero). [assumption]. 12 -environment(A) | -subpopulations(first_movers,efficient_producers,A,B) | in_environment(A,B). [assumption]. 14 -constant(A) | constant(B) | increases(B) | decreases(B) | sum(B,C) != A. [assumption]. 22 subpopulations(first_movers,efficient_producers,c1,c2). [assumption]. 23 constant(number_of_organizations(c1,c2)). [assumption]. 24 growth_rate(first_movers,c2) != zero. [assumption]. 25 -greater(growth_rate(first_movers,c2),zero). [assumption]. 26 -greater(zero,growth_rate(first_movers,c2)). [assumption]. 29 efficient_producers != A | -subpopulation(A,c1,B) | sum(cardinality_at_time(first_movers,B),cardinality_at_time(efficient_producers,B)) = number_of_organizations(c1,B). [resolve(1,a,3,a)]. 30 efficient_producers != A | -subpopulation(A,c1,B) | number_of_organizations(c1,B) = sum(cardinality_at_time(first_movers,B),cardinality_at_time(efficient_producers,B)). [copy(29),flip(c)]. 33 -in_environment(c1,A) | subpopulation(first_movers,c1,A). [resolve(1,a,5,a)]. 34 -in_environment(c1,A) | subpopulation(efficient_producers,c1,A). [resolve(1,a,6,a)]. 35 -in_environment(c1,A) | -subpopulation(B,c1,A) | -greater(cardinality_at_time(B,A),zero) | -constant(cardinality_at_time(B,A)) | growth_rate(B,A) = zero. [resolve(1,a,7,a)]. 36 -in_environment(c1,A) | -subpopulation(B,c1,A) | -greater(cardinality_at_time(B,A),zero) | -increases(cardinality_at_time(B,A)) | greater(growth_rate(B,A),zero). [resolve(1,a,8,a)]. 37 -in_environment(c1,A) | -subpopulation(B,c1,A) | -greater(cardinality_at_time(B,A),zero) | -decreases(cardinality_at_time(B,A)) | greater(zero,growth_rate(B,A)). [resolve(1,a,9,a)]. 38 -subpopulations(first_movers,efficient_producers,c1,A) | greater(cardinality_at_time(first_movers,A),zero). [resolve(1,a,10,a)]. 40 -subpopulations(first_movers,efficient_producers,c1,A) | in_environment(c1,A). [resolve(1,a,12,a)]. 54 greater(cardinality_at_time(first_movers,c2),zero). [resolve(38,a,22,a)]. 56 in_environment(c1,c2). [resolve(40,a,22,a)]. 57 subpopulation(efficient_producers,c1,c2). [resolve(56,a,34,a)]. 58 subpopulation(first_movers,c1,c2). [resolve(56,a,33,a)]. 63 number_of_organizations(c1,c2) = sum(cardinality_at_time(first_movers,c2),cardinality_at_time(efficient_producers,c2)). [resolve(57,a,30,b),xx(a)]. 74 constant(sum(cardinality_at_time(first_movers,c2),cardinality_at_time(efficient_producers,c2))). [back_rewrite(23),rewrite([63(3)])]. 75 -decreases(cardinality_at_time(first_movers,c2)). [resolve(58,a,37,b),unit_del(a,56),unit_del(b,54),unit_del(d,26)]. 76 -increases(cardinality_at_time(first_movers,c2)). [resolve(58,a,36,b),unit_del(a,56),unit_del(b,54),unit_del(d,25)]. 77 -constant(cardinality_at_time(first_movers,c2)). [resolve(58,a,35,b),unit_del(a,56),unit_del(b,54),unit_del(d,24)]. 80 -constant(sum(cardinality_at_time(first_movers,c2),A)). [ur(14,b,77,a,c,76,a,d,75,a,e,xx)]. 81 $F. [resolve(80,a,74,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=36. Generated=90. Kept=64. proofs=1. Usable=34. Sos=15. Demods=1. Limbo=2, Disabled=50. Hints=0. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=26. Back_subsumed=1. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=1 (0 lex), Back_demodulated=11. Back_unit_deleted=0. Demod_attempts=439. Demod_rewrites=15. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=46. Nonunit_bsub_feature_tests=131. Megabytes=0.27. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 21814 exit (max_proofs) Wed May 7 22:14:46 2008 ============================== continuing FOF reduction multisearch == Subproblem 3 of 8 (negated): ((all E (- environment(E) | (all X ((all T (- subpopulation(X,E,T) | greater(cardinality_at_time(X,T),zero) | =(sum(cardinality_at_time(first_movers,T),cardinality_at_time(efficient_producers,T)),number_of_organizations(E,T)))))))) & (all E (- environment(E) | (all X (- =(efficient_producers,X) | (all T (- subpopulation(X,E,T) | =(sum(cardinality_at_time(first_movers,T),cardinality_at_time(efficient_producers,T)),number_of_organizations(E,T)))))))) & (all E (- environment(E) | (all X (- =(first_movers,X) | (all T (- subpopulation(X,E,T) | =(sum(cardinality_at_time(first_movers,T),cardinality_at_time(efficient_producers,T)),number_of_organizations(E,T)))))))) & (all E (- environment(E) | (all T (- in_environment(E,T) | subpopulation(first_movers,E,T))))) & (all E (- environment(E) | (all T (- in_environment(E,T) | subpopulation(efficient_producers,E,T))))) & (all A (- constant(A) | (all B (constant(B) | increases(B) | decreases(B) | (all C (- =(sum(B,C),A))))))) & (all A (- constant(A) | (all B (constant(B) | increases(B) | (all C (- =(sum(B,C),A) | increases(C))))))) & (all A (- constant(A) | (all B (constant(B) | decreases(B) | (all C (- =(sum(B,C),A) | decreases(C))))))) & (all A (- constant(A) | (all B (constant(B) | (all C (- =(sum(B,C),A) | decreases(C) | increases(C))))))) & (all A (- constant(A) | (all B (increases(B) | decreases(B) | (all C (- =(sum(B,C),A) | constant(C))))))) & (all A (- constant(A) | (all B (increases(B) | (all C (- =(sum(B,C),A) | constant(C) | increases(C))))))) & (all A (- constant(A) | (all B (decreases(B) | (all C (- =(sum(B,C),A) | constant(C) | decreases(C))))))) & (all A (- constant(A) | (all B ((all C (- =(sum(B,C),A) | constant(C) | decreases(C) | increases(C))))))) & (all X (all E (- environment(E) | (all T (- in_environment(E,T) | - subpopulation(X,E,T) | - greater(cardinality_at_time(X,T),zero) | - constant(cardinality_at_time(X,T)) | =(growth_rate(X,T),zero)))))) & (all X (all E (- environment(E) | (all T (- in_environment(E,T) | - subpopulation(X,E,T) | - greater(cardinality_at_time(X,T),zero) | - increases(cardinality_at_time(X,T)) | greater(growth_rate(X,T),zero)))))) & (all X (all E (- environment(E) | (all T (- in_environment(E,T) | - subpopulation(X,E,T) | - greater(cardinality_at_time(X,T),zero) | - decreases(cardinality_at_time(X,T)) | greater(zero,growth_rate(X,T))))))) & (all E (- environment(E) | (all T (- subpopulations(first_movers,efficient_producers,E,T) | greater(cardinality_at_time(first_movers,T),zero))))) & (all E (- environment(E) | (all T (- subpopulations(first_movers,efficient_producers,E,T) | greater(cardinality_at_time(efficient_producers,T),zero))))) & (all E (- environment(E) | (all T (- subpopulations(first_movers,efficient_producers,E,T) | in_environment(E,T))))) & (all E (- environment(E) | (all X (=(efficient_producers,X) | =(first_movers,X) | (all T (- subpopulation(X,E,T) | - greater(cardinality_at_time(X,T),zero))))))) & (exists E (environment(E) & (exists T (subpopulations(first_movers,efficient_producers,E,T) & constant(number_of_organizations(E,T)) & - =(growth_rate(first_movers,T),zero) & - greater(zero,growth_rate(efficient_producers,T)) & - greater(growth_rate(efficient_producers,T),zero)))))). Max_seconds is 30 for this subproblem. Child search process 21815 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). -environment(A) | -subpopulation(B,A,C) | greater(cardinality_at_time(B,C),zero) | sum(cardinality_at_time(first_movers,C),cardinality_at_time(efficient_producers,C)) = number_of_organizations(A,C). [assumption]. -environment(A) | efficient_producers != B | -subpopulation(B,A,C) | sum(cardinality_at_time(first_movers,C),cardinality_at_time(efficient_producers,C)) = number_of_organizations(A,C). [assumption]. -environment(A) | first_movers != B | -subpopulation(B,A,C) | sum(cardinality_at_time(first_movers,C),cardinality_at_time(efficient_producers,C)) = number_of_organizations(A,C). [assumption]. -environment(A) | -in_environment(A,B) | subpopulation(first_movers,A,B). [assumption]. -environment(A) | -in_environment(A,B) | subpopulation(efficient_producers,A,B). [assumption]. -constant(A) | constant(B) | increases(B) | decreases(B) | sum(B,C) != A. [assumption]. -constant(A) | constant(B) | increases(B) | sum(B,C) != A | increases(C). [assumption]. -constant(A) | constant(B) | decreases(B) | sum(B,C) != A | decreases(C). [assumption]. -constant(A) | constant(B) | sum(B,C) != A | decreases(C) | increases(C). [assumption]. -constant(A) | increases(B) | decreases(B) | sum(B,C) != A | constant(C). [assumption]. -constant(A) | increases(B) | sum(B,C) != A | constant(C) | increases(C). [assumption]. -constant(A) | decreases(B) | sum(B,C) != A | constant(C) | decreases(C). [assumption]. -constant(A) | sum(B,C) != A | constant(C) | decreases(C) | increases(C). [assumption]. -environment(A) | -in_environment(A,B) | -subpopulation(C,A,B) | -greater(cardinality_at_time(C,B),zero) | -constant(cardinality_at_time(C,B)) | growth_rate(C,B) = zero. [assumption]. -environment(A) | -in_environment(A,B) | -subpopulation(C,A,B) | -greater(cardinality_at_time(C,B),zero) | -increases(cardinality_at_time(C,B)) | greater(growth_rate(C,B),zero). [assumption]. -environment(A) | -in_environment(A,B) | -subpopulation(C,A,B) | -greater(cardinality_at_time(C,B),zero) | -decreases(cardinality_at_time(C,B)) | greater(zero,growth_rate(C,B)). [assumption]. -environment(A) | -subpopulations(first_movers,efficient_producers,A,B) | greater(cardinality_at_time(first_movers,B),zero). [assumption]. -environment(A) | -subpopulations(first_movers,efficient_producers,A,B) | greater(cardinality_at_time(efficient_producers,B),zero). [assumption]. -environment(A) | -subpopulations(first_movers,efficient_producers,A,B) | in_environment(A,B). [assumption]. -environment(A) | efficient_producers = B | first_movers = B | -subpopulation(B,A,C) | -greater(cardinality_at_time(B,C),zero). [assumption]. environment(c1). [assumption]. subpopulations(first_movers,efficient_producers,c1,c2). [assumption]. constant(number_of_organizations(c1,c2)). [assumption]. growth_rate(first_movers,c2) != zero. [assumption]. -greater(zero,growth_rate(efficient_producers,c2)). [assumption]. -greater(growth_rate(efficient_producers,c2),zero). [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= Eliminating environment/1 1 environment(c1). [assumption]. 2 -environment(A) | -subpopulation(B,A,C) | greater(cardinality_at_time(B,C),zero) | sum(cardinality_at_time(first_movers,C),cardinality_at_time(efficient_producers,C)) = number_of_organizations(A,C). [assumption]. 3 -environment(A) | efficient_producers != B | -subpopulation(B,A,C) | sum(cardinality_at_time(first_movers,C),cardinality_at_time(efficient_producers,C)) = number_of_organizations(A,C). [assumption]. 4 -environment(A) | first_movers != B | -subpopulation(B,A,C) | sum(cardinality_at_time(first_movers,C),cardinality_at_time(efficient_producers,C)) = number_of_organizations(A,C). [assumption]. 5 -environment(A) | -in_environment(A,B) | subpopulation(first_movers,A,B). [assumption]. 6 -environment(A) | -in_environment(A,B) | subpopulation(efficient_producers,A,B). [assumption]. 7 -environment(A) | -in_environment(A,B) | -subpopulation(C,A,B) | -greater(cardinality_at_time(C,B),zero) | -constant(cardinality_at_time(C,B)) | growth_rate(C,B) = zero. [assumption]. 8 -environment(A) | -in_environment(A,B) | -subpopulation(C,A,B) | -greater(cardinality_at_time(C,B),zero) | -increases(cardinality_at_time(C,B)) | greater(growth_rate(C,B),zero). [assumption]. 9 -environment(A) | -in_environment(A,B) | -subpopulation(C,A,B) | -greater(cardinality_at_time(C,B),zero) | -decreases(cardinality_at_time(C,B)) | greater(zero,growth_rate(C,B)). [assumption]. 10 -environment(A) | -subpopulations(first_movers,efficient_producers,A,B) | greater(cardinality_at_time(first_movers,B),zero). [assumption]. 11 -environment(A) | -subpopulations(first_movers,efficient_producers,A,B) | greater(cardinality_at_time(efficient_producers,B),zero). [assumption]. 12 -environment(A) | -subpopulations(first_movers,efficient_producers,A,B) | in_environment(A,B). [assumption]. 13 -environment(A) | efficient_producers = B | first_movers = B | -subpopulation(B,A,C) | -greater(cardinality_at_time(B,C),zero). [assumption]. Derived: -subpopulation(A,c1,B) | greater(cardinality_at_time(A,B),zero) | sum(cardinality_at_time(first_movers,B),cardinality_at_time(efficient_producers,B)) = number_of_organizations(c1,B). [resolve(1,a,2,a)]. Derived: efficient_producers != A | -subpopulation(A,c1,B) | sum(cardinality_at_time(first_movers,B),cardinality_at_time(efficient_producers,B)) = number_of_organizations(c1,B). [resolve(1,a,3,a)]. Derived: first_movers != A | -subpopulation(A,c1,B) | sum(cardinality_at_time(first_movers,B),cardinality_at_time(efficient_producers,B)) = number_of_organizations(c1,B). [resolve(1,a,4,a)]. Derived: -in_environment(c1,A) | subpopulation(first_movers,c1,A). [resolve(1,a,5,a)]. Derived: -in_environment(c1,A) | subpopulation(efficient_producers,c1,A). [resolve(1,a,6,a)]. Derived: -in_environment(c1,A) | -subpopulation(B,c1,A) | -greater(cardinality_at_time(B,A),zero) | -constant(cardinality_at_time(B,A)) | growth_rate(B,A) = zero. [resolve(1,a,7,a)]. Derived: -in_environment(c1,A) | -subpopulation(B,c1,A) | -greater(cardinality_at_time(B,A),zero) | -increases(cardinality_at_time(B,A)) | greater(growth_rate(B,A),zero). [resolve(1,a,8,a)]. Derived: -in_environment(c1,A) | -subpopulation(B,c1,A) | -greater(cardinality_at_time(B,A),zero) | -decreases(cardinality_at_time(B,A)) | greater(zero,growth_rate(B,A)). [resolve(1,a,9,a)]. Derived: -subpopulations(first_movers,efficient_producers,c1,A) | greater(cardinality_at_time(first_movers,A),zero). [resolve(1,a,10,a)]. Derived: -subpopulations(first_movers,efficient_producers,c1,A) | greater(cardinality_at_time(efficient_producers,A),zero). [resolve(1,a,11,a)]. Derived: -subpopulations(first_movers,efficient_producers,c1,A) | in_environment(c1,A). [resolve(1,a,12,a)]. Derived: efficient_producers = A | first_movers = A | -subpopulation(A,c1,B) | -greater(cardinality_at_time(A,B),zero). [resolve(1,a,13,a)]. ============================== end predicate elimination ============= Term ordering decisions: Predicate symbol precedence: predicate_order([ =, constant, decreases, increases, greater, in_environment, subpopulation, subpopulations ]). Function symbol precedence: function_order([ efficient_producers, first_movers, zero, c1, c2, cardinality_at_time, sum, number_of_organizations, growth_rate ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(binary_resolution). % (non-Horn) % set(neg_ur_resolution). % (non-Horn, less than 100 clauses) Auto_process settings: % set(factor). % (non-Horn) % set(unit_deletion). % (non-Horn) ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 14 -constant(A) | constant(B) | increases(B) | decreases(B) | sum(B,C) != A. [assumption]. 15 -constant(A) | constant(B) | increases(B) | sum(B,C) != A | increases(C). [assumption]. 16 -constant(A) | constant(B) | decreases(B) | sum(B,C) != A | decreases(C). [assumption]. 17 -constant(A) | constant(B) | sum(B,C) != A | decreases(C) | increases(C). [assumption]. 18 -constant(A) | increases(B) | decreases(B) | sum(B,C) != A | constant(C). [assumption]. 19 -constant(A) | increases(B) | sum(B,C) != A | constant(C) | increases(C). [assumption]. 20 -constant(A) | decreases(B) | sum(B,C) != A | constant(C) | decreases(C). [assumption]. 21 -constant(A) | sum(B,C) != A | constant(C) | decreases(C) | increases(C). [assumption]. 22 subpopulations(first_movers,efficient_producers,c1,c2). [assumption]. 23 constant(number_of_organizations(c1,c2)). [assumption]. 24 growth_rate(first_movers,c2) != zero. [assumption]. 25 -greater(zero,growth_rate(efficient_producers,c2)). [assumption]. 26 -greater(growth_rate(efficient_producers,c2),zero). [assumption]. 28 -subpopulation(A,c1,B) | greater(cardinality_at_time(A,B),zero) | number_of_organizations(c1,B) = sum(cardinality_at_time(first_movers,B),cardinality_at_time(efficient_producers,B)). [copy(27),flip(c)]. 30 efficient_producers != A | -subpopulation(A,c1,B) | number_of_organizations(c1,B) = sum(cardinality_at_time(first_movers,B),cardinality_at_time(efficient_producers,B)). [copy(29),flip(c)]. 32 first_movers != A | -subpopulation(A,c1,B) | number_of_organizations(c1,B) = sum(cardinality_at_time(first_movers,B),cardinality_at_time(efficient_producers,B)). [copy(31),flip(c)]. 33 -in_environment(c1,A) | subpopulation(first_movers,c1,A). [resolve(1,a,5,a)]. 34 -in_environment(c1,A) | subpopulation(efficient_producers,c1,A). [resolve(1,a,6,a)]. 35 -in_environment(c1,A) | -subpopulation(B,c1,A) | -greater(cardinality_at_time(B,A),zero) | -constant(cardinality_at_time(B,A)) | growth_rate(B,A) = zero. [resolve(1,a,7,a)]. 36 -in_environment(c1,A) | -subpopulation(B,c1,A) | -greater(cardinality_at_time(B,A),zero) | -increases(cardinality_at_time(B,A)) | greater(growth_rate(B,A),zero). [resolve(1,a,8,a)]. 37 -in_environment(c1,A) | -subpopulation(B,c1,A) | -greater(cardinality_at_time(B,A),zero) | -decreases(cardinality_at_time(B,A)) | greater(zero,growth_rate(B,A)). [resolve(1,a,9,a)]. 38 -subpopulations(first_movers,efficient_producers,c1,A) | greater(cardinality_at_time(first_movers,A),zero). [resolve(1,a,10,a)]. 39 -subpopulations(first_movers,efficient_producers,c1,A) | greater(cardinality_at_time(efficient_producers,A),zero). [resolve(1,a,11,a)]. 40 -subpopulations(first_movers,efficient_producers,c1,A) | in_environment(c1,A). [resolve(1,a,12,a)]. 41 efficient_producers = A | first_movers = A | -subpopulation(A,c1,B) | -greater(cardinality_at_time(A,B),zero). [resolve(1,a,13,a)]. 42 -constant(A) | constant(B) | increases(B) | sum(B,B) != A. [factor(15,c,e)]. 43 -constant(A) | constant(B) | decreases(B) | sum(B,B) != A. [factor(16,c,e)]. end_of_list. formulas(demodulators). end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=13): 14 -constant(A) | constant(B) | increases(B) | decreases(B) | sum(B,C) != A. [assumption]. given #2 (I,wt=13): 15 -constant(A) | constant(B) | increases(B) | sum(B,C) != A | increases(C). [assumption]. given #3 (I,wt=13): 16 -constant(A) | constant(B) | decreases(B) | sum(B,C) != A | decreases(C). [assumption]. given #4 (I,wt=13): 17 -constant(A) | constant(B) | sum(B,C) != A | decreases(C) | increases(C). [assumption]. given #5 (I,wt=13): 18 -constant(A) | increases(B) | decreases(B) | sum(B,C) != A | constant(C). [assumption]. given #6 (I,wt=13): 19 -constant(A) | increases(B) | sum(B,C) != A | constant(C) | increases(C). [assumption]. given #7 (I,wt=13): 20 -constant(A) | decreases(B) | sum(B,C) != A | constant(C) | decreases(C). [assumption]. given #8 (I,wt=13): 21 -constant(A) | sum(B,C) != A | constant(C) | decreases(C) | increases(C). [assumption]. given #9 (I,wt=5): 22 subpopulations(first_movers,efficient_producers,c1,c2). [assumption]. given #10 (I,wt=4): 23 constant(number_of_organizations(c1,c2)). [assumption]. given #11 (I,wt=5): 24 growth_rate(first_movers,c2) != zero. [assumption]. given #12 (I,wt=5): 25 -greater(zero,growth_rate(efficient_producers,c2)). [assumption]. given #13 (I,wt=5): 26 -greater(growth_rate(efficient_producers,c2),zero). [assumption]. given #14 (I,wt=20): 28 -subpopulation(A,c1,B) | greater(cardinality_at_time(A,B),zero) | number_of_organizations(c1,B) = sum(cardinality_at_time(first_movers,B),cardinality_at_time(efficient_producers,B)). [copy(27),flip(c)]. given #15 (I,wt=18): 30 efficient_producers != A | -subpopulation(A,c1,B) | number_of_organizations(c1,B) = sum(cardinality_at_time(first_movers,B),cardinality_at_time(efficient_producers,B)). [copy(29),flip(c)]. given #16 (I,wt=18): 32 first_movers != A | -subpopulation(A,c1,B) | number_of_organizations(c1,B) = sum(cardinality_at_time(first_movers,B),cardinality_at_time(efficient_producers,B)). [copy(31),flip(c)]. given #17 (I,wt=7): 33 -in_environment(c1,A) | subpopulation(first_movers,c1,A). [resolve(1,a,5,a)]. given #18 (I,wt=7): 34 -in_environment(c1,A) | subpopulation(efficient_producers,c1,A). [resolve(1,a,6,a)]. given #19 (I,wt=21): 35 -in_environment(c1,A) | -subpopulation(B,c1,A) | -greater(cardinality_at_time(B,A),zero) | -constant(cardinality_at_time(B,A)) | growth_rate(B,A) = zero. [resolve(1,a,7,a)]. given #20 (I,wt=21): 36 -in_environment(c1,A) | -subpopulation(B,c1,A) | -greater(cardinality_at_time(B,A),zero) | -increases(cardinality_at_time(B,A)) | greater(growth_rate(B,A),zero). [resolve(1,a,8,a)]. given #21 (I,wt=21): 37 -in_environment(c1,A) | -subpopulation(B,c1,A) | -greater(cardinality_at_time(B,A),zero) | -decreases(cardinality_at_time(B,A)) | greater(zero,growth_rate(B,A)). [resolve(1,a,9,a)]. given #22 (I,wt=10): 38 -subpopulations(first_movers,efficient_producers,c1,A) | greater(cardinality_at_time(first_movers,A),zero). [resolve(1,a,10,a)]. given #23 (I,wt=10): 39 -subpopulations(first_movers,efficient_producers,c1,A) | greater(cardinality_at_time(efficient_producers,A),zero). [resolve(1,a,11,a)]. given #24 (I,wt=8): 40 -subpopulations(first_movers,efficient_producers,c1,A) | in_environment(c1,A). [resolve(1,a,12,a)]. given #25 (I,wt=15): 41 efficient_producers = A | first_movers = A | -subpopulation(A,c1,B) | -greater(cardinality_at_time(A,B),zero). [resolve(1,a,13,a)]. given #26 (I,wt=11): 42 -constant(A) | constant(B) | increases(B) | sum(B,B) != A. [factor(15,c,e)]. given #27 (I,wt=11): 43 -constant(A) | constant(B) | decreases(B) | sum(B,B) != A. [factor(16,c,e)]. given #28 (A,wt=13): 44 sum(A,B) != number_of_organizations(c1,c2) | constant(B) | decreases(B) | increases(B). [resolve(23,a,21,a)]. given #29 (T,wt=3): 56 in_environment(c1,c2). [resolve(40,a,22,a)]. given #30 (T,wt=4): 57 subpopulation(efficient_producers,c1,c2). [resolve(56,a,34,a)]. given #31 (T,wt=4): 58 subpopulation(first_movers,c1,c2). [resolve(56,a,33,a)]. given #32 (T,wt=5): 54 greater(cardinality_at_time(first_movers,c2),zero). [resolve(38,a,22,a)]. given #33 (A,wt=5): 55 greater(cardinality_at_time(efficient_producers,c2),zero). [resolve(39,a,22,a)]. given #34 (F,wt=4): 59 -decreases(cardinality_at_time(efficient_producers,c2)). [resolve(57,a,37,b),unit_del(a,56),unit_del(b,55),unit_del(d,25)]. given #35 (F,wt=4): 60 -increases(cardinality_at_time(efficient_producers,c2)). [resolve(57,a,36,b),unit_del(a,56),unit_del(b,55),unit_del(d,26)]. given #36 (F,wt=4): 77 -constant(cardinality_at_time(first_movers,c2)). [resolve(58,a,35,b),unit_del(a,56),unit_del(b,54),unit_del(d,24)]. ============================== PROOF ================================= % Proof 1 at 0.01 (+ 0.00) seconds. % Length of proof is 37. % Level of proof is 6. % Maximum clause weight is 21. % Given clauses 36. 1 environment(c1). [assumption]. 3 -environment(A) | efficient_producers != B | -subpopulation(B,A,C) | sum(cardinality_at_time(first_movers,C),cardinality_at_time(efficient_producers,C)) = number_of_organizations(A,C). [assumption]. 5 -environment(A) | -in_environment(A,B) | subpopulation(first_movers,A,B). [assumption]. 6 -environment(A) | -in_environment(A,B) | subpopulation(efficient_producers,A,B). [assumption]. 7 -environment(A) | -in_environment(A,B) | -subpopulation(C,A,B) | -greater(cardinality_at_time(C,B),zero) | -constant(cardinality_at_time(C,B)) | growth_rate(C,B) = zero. [assumption]. 8 -environment(A) | -in_environment(A,B) | -subpopulation(C,A,B) | -greater(cardinality_at_time(C,B),zero) | -increases(cardinality_at_time(C,B)) | greater(growth_rate(C,B),zero). [assumption]. 9 -environment(A) | -in_environment(A,B) | -subpopulation(C,A,B) | -greater(cardinality_at_time(C,B),zero) | -decreases(cardinality_at_time(C,B)) | greater(zero,growth_rate(C,B)). [assumption]. 10 -environment(A) | -subpopulations(first_movers,efficient_producers,A,B) | greater(cardinality_at_time(first_movers,B),zero). [assumption]. 11 -environment(A) | -subpopulations(first_movers,efficient_producers,A,B) | greater(cardinality_at_time(efficient_producers,B),zero). [assumption]. 12 -environment(A) | -subpopulations(first_movers,efficient_producers,A,B) | in_environment(A,B). [assumption]. 17 -constant(A) | constant(B) | sum(B,C) != A | decreases(C) | increases(C). [assumption]. 22 subpopulations(first_movers,efficient_producers,c1,c2). [assumption]. 23 constant(number_of_organizations(c1,c2)). [assumption]. 24 growth_rate(first_movers,c2) != zero. [assumption]. 25 -greater(zero,growth_rate(efficient_producers,c2)). [assumption]. 26 -greater(growth_rate(efficient_producers,c2),zero). [assumption]. 29 efficient_producers != A | -subpopulation(A,c1,B) | sum(cardinality_at_time(first_movers,B),cardinality_at_time(efficient_producers,B)) = number_of_organizations(c1,B). [resolve(1,a,3,a)]. 30 efficient_producers != A | -subpopulation(A,c1,B) | number_of_organizations(c1,B) = sum(cardinality_at_time(first_movers,B),cardinality_at_time(efficient_producers,B)). [copy(29),flip(c)]. 33 -in_environment(c1,A) | subpopulation(first_movers,c1,A). [resolve(1,a,5,a)]. 34 -in_environment(c1,A) | subpopulation(efficient_producers,c1,A). [resolve(1,a,6,a)]. 35 -in_environment(c1,A) | -subpopulation(B,c1,A) | -greater(cardinality_at_time(B,A),zero) | -constant(cardinality_at_time(B,A)) | growth_rate(B,A) = zero. [resolve(1,a,7,a)]. 36 -in_environment(c1,A) | -subpopulation(B,c1,A) | -greater(cardinality_at_time(B,A),zero) | -increases(cardinality_at_time(B,A)) | greater(growth_rate(B,A),zero). [resolve(1,a,8,a)]. 37 -in_environment(c1,A) | -subpopulation(B,c1,A) | -greater(cardinality_at_time(B,A),zero) | -decreases(cardinality_at_time(B,A)) | greater(zero,growth_rate(B,A)). [resolve(1,a,9,a)]. 38 -subpopulations(first_movers,efficient_producers,c1,A) | greater(cardinality_at_time(first_movers,A),zero). [resolve(1,a,10,a)]. 39 -subpopulations(first_movers,efficient_producers,c1,A) | greater(cardinality_at_time(efficient_producers,A),zero). [resolve(1,a,11,a)]. 40 -subpopulations(first_movers,efficient_producers,c1,A) | in_environment(c1,A). [resolve(1,a,12,a)]. 54 greater(cardinality_at_time(first_movers,c2),zero). [resolve(38,a,22,a)]. 55 greater(cardinality_at_time(efficient_producers,c2),zero). [resolve(39,a,22,a)]. 56 in_environment(c1,c2). [resolve(40,a,22,a)]. 57 subpopulation(efficient_producers,c1,c2). [resolve(56,a,34,a)]. 58 subpopulation(first_movers,c1,c2). [resolve(56,a,33,a)]. 59 -decreases(cardinality_at_time(efficient_producers,c2)). [resolve(57,a,37,b),unit_del(a,56),unit_del(b,55),unit_del(d,25)]. 60 -increases(cardinality_at_time(efficient_producers,c2)). [resolve(57,a,36,b),unit_del(a,56),unit_del(b,55),unit_del(d,26)]. 63 number_of_organizations(c1,c2) = sum(cardinality_at_time(first_movers,c2),cardinality_at_time(efficient_producers,c2)). [resolve(57,a,30,b),xx(a)]. 74 constant(sum(cardinality_at_time(first_movers,c2),cardinality_at_time(efficient_producers,c2))). [back_rewrite(23),rewrite([63(3)])]. 77 -constant(cardinality_at_time(first_movers,c2)). [resolve(58,a,35,b),unit_del(a,56),unit_del(b,54),unit_del(d,24)]. 79 $F. [ur(17,b,77,a,c,xx,d,59,a,e,60,a),unit_del(a,74)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=36. Generated=82. Kept=62. proofs=1. Usable=34. Sos=15. Demods=1. Limbo=1, Disabled=50. Hints=0. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=19. Back_subsumed=1. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=1 (0 lex), Back_demodulated=11. Back_unit_deleted=0. Demod_attempts=381. Demod_rewrites=15. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=46. Nonunit_bsub_feature_tests=131. Megabytes=0.27. User_CPU=0.01, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 21815 exit (max_proofs) Wed May 7 22:14:46 2008 ============================== continuing FOF reduction multisearch == Subproblem 4 of 8 (negated): ((all E (- environment(E) | (all X ((all T (- subpopulation(X,E,T) | greater(cardinality_at_time(X,T),zero) | =(sum(cardinality_at_time(first_movers,T),cardinality_at_time(efficient_producers,T)),number_of_organizations(E,T)))))))) & (all E (- environment(E) | (all X (- =(efficient_producers,X) | (all T (- subpopulation(X,E,T) | =(sum(cardinality_at_time(first_movers,T),cardinality_at_time(efficient_producers,T)),number_of_organizations(E,T)))))))) & (all E (- environment(E) | (all X (- =(first_movers,X) | (all T (- subpopulation(X,E,T) | =(sum(cardinality_at_time(first_movers,T),cardinality_at_time(efficient_producers,T)),number_of_organizations(E,T)))))))) & (all E (- environment(E) | (all T (- in_environment(E,T) | subpopulation(first_movers,E,T))))) & (all E (- environment(E) | (all T (- in_environment(E,T) | subpopulation(efficient_producers,E,T))))) & (all A (- constant(A) | (all B (constant(B) | increases(B) | decreases(B) | (all C (- =(sum(B,C),A))))))) & (all A (- constant(A) | (all B (constant(B) | increases(B) | (all C (- =(sum(B,C),A) | increases(C))))))) & (all A (- constant(A) | (all B (constant(B) | decreases(B) | (all C (- =(sum(B,C),A) | decreases(C))))))) & (all A (- constant(A) | (all B (constant(B) | (all C (- =(sum(B,C),A) | decreases(C) | increases(C))))))) & (all A (- constant(A) | (all B (increases(B) | decreases(B) | (all C (- =(sum(B,C),A) | constant(C))))))) & (all A (- constant(A) | (all B (increases(B) | (all C (- =(sum(B,C),A) | constant(C) | increases(C))))))) & (all A (- constant(A) | (all B (decreases(B) | (all C (- =(sum(B,C),A) | constant(C) | decreases(C))))))) & (all A (- constant(A) | (all B ((all C (- =(sum(B,C),A) | constant(C) | decreases(C) | increases(C))))))) & (all X (all E (- environment(E) | (all T (- in_environment(E,T) | - subpopulation(X,E,T) | - greater(cardinality_at_time(X,T),zero) | - constant(cardinality_at_time(X,T)) | =(growth_rate(X,T),zero)))))) & (all X (all E (- environment(E) | (all T (- in_environment(E,T) | - subpopulation(X,E,T) | - greater(cardinality_at_time(X,T),zero) | - increases(cardinality_at_time(X,T)) | greater(growth_rate(X,T),zero)))))) & (all X (all E (- environment(E) | (all T (- in_environment(E,T) | - subpopulation(X,E,T) | - greater(cardinality_at_time(X,T),zero) | - decreases(cardinality_at_time(X,T)) | greater(zero,growth_rate(X,T))))))) & (all E (- environment(E) | (all T (- subpopulations(first_movers,efficient_producers,E,T) | greater(cardinality_at_time(first_movers,T),zero))))) & (all E (- environment(E) | (all T (- subpopulations(first_movers,efficient_producers,E,T) | greater(cardinality_at_time(efficient_producers,T),zero))))) & (all E (- environment(E) | (all T (- subpopulations(first_movers,efficient_producers,E,T) | in_environment(E,T))))) & (all E (- environment(E) | (all X (=(efficient_producers,X) | =(first_movers,X) | (all T (- subpopulation(X,E,T) | - greater(cardinality_at_time(X,T),zero))))))) & (exists E (environment(E) & (exists T (subpopulations(first_movers,efficient_producers,E,T) & constant(number_of_organizations(E,T)) & - =(growth_rate(first_movers,T),zero) & - greater(zero,growth_rate(efficient_producers,T)) & - greater(zero,growth_rate(first_movers,T))))))). Max_seconds is 30 for this subproblem. Child search process 21816 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). -environment(A) | -subpopulation(B,A,C) | greater(cardinality_at_time(B,C),zero) | sum(cardinality_at_time(first_movers,C),cardinality_at_time(efficient_producers,C)) = number_of_organizations(A,C). [assumption]. -environment(A) | efficient_producers != B | -subpopulation(B,A,C) | sum(cardinality_at_time(first_movers,C),cardinality_at_time(efficient_producers,C)) = number_of_organizations(A,C). [assumption]. -environment(A) | first_movers != B | -subpopulation(B,A,C) | sum(cardinality_at_time(first_movers,C),cardinality_at_time(efficient_producers,C)) = number_of_organizations(A,C). [assumption]. -environment(A) | -in_environment(A,B) | subpopulation(first_movers,A,B). [assumption]. -environment(A) | -in_environment(A,B) | subpopulation(efficient_producers,A,B). [assumption]. -constant(A) | constant(B) | increases(B) | decreases(B) | sum(B,C) != A. [assumption]. -constant(A) | constant(B) | increases(B) | sum(B,C) != A | increases(C). [assumption]. -constant(A) | constant(B) | decreases(B) | sum(B,C) != A | decreases(C). [assumption]. -constant(A) | constant(B) | sum(B,C) != A | decreases(C) | increases(C). [assumption]. -constant(A) | increases(B) | decreases(B) | sum(B,C) != A | constant(C). [assumption]. -constant(A) | increases(B) | sum(B,C) != A | constant(C) | increases(C). [assumption]. -constant(A) | decreases(B) | sum(B,C) != A | constant(C) | decreases(C). [assumption]. -constant(A) | sum(B,C) != A | constant(C) | decreases(C) | increases(C). [assumption]. -environment(A) | -in_environment(A,B) | -subpopulation(C,A,B) | -greater(cardinality_at_time(C,B),zero) | -constant(cardinality_at_time(C,B)) | growth_rate(C,B) = zero. [assumption]. -environment(A) | -in_environment(A,B) | -subpopulation(C,A,B) | -greater(cardinality_at_time(C,B),zero) | -increases(cardinality_at_time(C,B)) | greater(growth_rate(C,B),zero). [assumption]. -environment(A) | -in_environment(A,B) | -subpopulation(C,A,B) | -greater(cardinality_at_time(C,B),zero) | -decreases(cardinality_at_time(C,B)) | greater(zero,growth_rate(C,B)). [assumption]. -environment(A) | -subpopulations(first_movers,efficient_producers,A,B) | greater(cardinality_at_time(first_movers,B),zero). [assumption]. -environment(A) | -subpopulations(first_movers,efficient_producers,A,B) | greater(cardinality_at_time(efficient_producers,B),zero). [assumption]. -environment(A) | -subpopulations(first_movers,efficient_producers,A,B) | in_environment(A,B). [assumption]. -environment(A) | efficient_producers = B | first_movers = B | -subpopulation(B,A,C) | -greater(cardinality_at_time(B,C),zero). [assumption]. environment(c1). [assumption]. subpopulations(first_movers,efficient_producers,c1,c2). [assumption]. constant(number_of_organizations(c1,c2)). [assumption]. growth_rate(first_movers,c2) != zero. [assumption]. -greater(zero,growth_rate(efficient_producers,c2)). [assumption]. -greater(zero,growth_rate(first_movers,c2)). [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= Eliminating environment/1 1 environment(c1). [assumption]. 2 -environment(A) | -subpopulation(B,A,C) | greater(cardinality_at_time(B,C),zero) | sum(cardinality_at_time(first_movers,C),cardinality_at_time(efficient_producers,C)) = number_of_organizations(A,C). [assumption]. 3 -environment(A) | efficient_producers != B | -subpopulation(B,A,C) | sum(cardinality_at_time(first_movers,C),cardinality_at_time(efficient_producers,C)) = number_of_organizations(A,C). [assumption]. 4 -environment(A) | first_movers != B | -subpopulation(B,A,C) | sum(cardinality_at_time(first_movers,C),cardinality_at_time(efficient_producers,C)) = number_of_organizations(A,C). [assumption]. 5 -environment(A) | -in_environment(A,B) | subpopulation(first_movers,A,B). [assumption]. 6 -environment(A) | -in_environment(A,B) | subpopulation(efficient_producers,A,B). [assumption]. 7 -environment(A) | -in_environment(A,B) | -subpopulation(C,A,B) | -greater(cardinality_at_time(C,B),zero) | -constant(cardinality_at_time(C,B)) | growth_rate(C,B) = zero. [assumption]. 8 -environment(A) | -in_environment(A,B) | -subpopulation(C,A,B) | -greater(cardinality_at_time(C,B),zero) | -increases(cardinality_at_time(C,B)) | greater(growth_rate(C,B),zero). [assumption]. 9 -environment(A) | -in_environment(A,B) | -subpopulation(C,A,B) | -greater(cardinality_at_time(C,B),zero) | -decreases(cardinality_at_time(C,B)) | greater(zero,growth_rate(C,B)). [assumption]. 10 -environment(A) | -subpopulations(first_movers,efficient_producers,A,B) | greater(cardinality_at_time(first_movers,B),zero). [assumption]. 11 -environment(A) | -subpopulations(first_movers,efficient_producers,A,B) | greater(cardinality_at_time(efficient_producers,B),zero). [assumption]. 12 -environment(A) | -subpopulations(first_movers,efficient_producers,A,B) | in_environment(A,B). [assumption]. 13 -environment(A) | efficient_producers = B | first_movers = B | -subpopulation(B,A,C) | -greater(cardinality_at_time(B,C),zero). [assumption]. Derived: -subpopulation(A,c1,B) | greater(cardinality_at_time(A,B),zero) | sum(cardinality_at_time(first_movers,B),cardinality_at_time(efficient_producers,B)) = number_of_organizations(c1,B). [resolve(1,a,2,a)]. Derived: efficient_producers != A | -subpopulation(A,c1,B) | sum(cardinality_at_time(first_movers,B),cardinality_at_time(efficient_producers,B)) = number_of_organizations(c1,B). [resolve(1,a,3,a)]. Derived: first_movers != A | -subpopulation(A,c1,B) | sum(cardinality_at_time(first_movers,B),cardinality_at_time(efficient_producers,B)) = number_of_organizations(c1,B). [resolve(1,a,4,a)]. Derived: -in_environment(c1,A) | subpopulation(first_movers,c1,A). [resolve(1,a,5,a)]. Derived: -in_environment(c1,A) | subpopulation(efficient_producers,c1,A). [resolve(1,a,6,a)]. Derived: -in_environment(c1,A) | -subpopulation(B,c1,A) | -greater(cardinality_at_time(B,A),zero) | -constant(cardinality_at_time(B,A)) | growth_rate(B,A) = zero. [resolve(1,a,7,a)]. Derived: -in_environment(c1,A) | -subpopulation(B,c1,A) | -greater(cardinality_at_time(B,A),zero) | -increases(cardinality_at_time(B,A)) | greater(growth_rate(B,A),zero). [resolve(1,a,8,a)]. Derived: -in_environment(c1,A) | -subpopulation(B,c1,A) | -greater(cardinality_at_time(B,A),zero) | -decreases(cardinality_at_time(B,A)) | greater(zero,growth_rate(B,A)). [resolve(1,a,9,a)]. Derived: -subpopulations(first_movers,efficient_producers,c1,A) | greater(cardinality_at_time(first_movers,A),zero). [resolve(1,a,10,a)]. Derived: -subpopulations(first_movers,efficient_producers,c1,A) | greater(cardinality_at_time(efficient_producers,A),zero). [resolve(1,a,11,a)]. Derived: -subpopulations(first_movers,efficient_producers,c1,A) | in_environment(c1,A). [resolve(1,a,12,a)]. Derived: efficient_producers = A | first_movers = A | -subpopulation(A,c1,B) | -greater(cardinality_at_time(A,B),zero). [resolve(1,a,13,a)]. ============================== end predicate elimination ============= Term ordering decisions: Predicate symbol precedence: predicate_order([ =, constant, decreases, increases, greater, in_environment, subpopulation, subpopulations ]). Function symbol precedence: function_order([ efficient_producers, first_movers, zero, c1, c2, cardinality_at_time, sum, number_of_organizations, growth_rate ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(binary_resolution). % (non-Horn) % set(neg_ur_resolution). % (non-Horn, less than 100 clauses) Auto_process settings: % set(factor). % (non-Horn) % set(unit_deletion). % (non-Horn) ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 14 -constant(A) | constant(B) | increases(B) | decreases(B) | sum(B,C) != A. [assumption]. 15 -constant(A) | constant(B) | increases(B) | sum(B,C) != A | increases(C). [assumption]. 16 -constant(A) | constant(B) | decreases(B) | sum(B,C) != A | decreases(C). [assumption]. 17 -constant(A) | constant(B) | sum(B,C) != A | decreases(C) | increases(C). [assumption]. 18 -constant(A) | increases(B) | decreases(B) | sum(B,C) != A | constant(C). [assumption]. 19 -constant(A) | increases(B) | sum(B,C) != A | constant(C) | increases(C). [assumption]. 20 -constant(A) | decreases(B) | sum(B,C) != A | constant(C) | decreases(C). [assumption]. 21 -constant(A) | sum(B,C) != A | constant(C) | decreases(C) | increases(C). [assumption]. 22 subpopulations(first_movers,efficient_producers,c1,c2). [assumption]. 23 constant(number_of_organizations(c1,c2)). [assumption]. 24 growth_rate(first_movers,c2) != zero. [assumption]. 25 -greater(zero,growth_rate(efficient_producers,c2)). [assumption]. 26 -greater(zero,growth_rate(first_movers,c2)). [assumption]. 28 -subpopulation(A,c1,B) | greater(cardinality_at_time(A,B),zero) | number_of_organizations(c1,B) = sum(cardinality_at_time(first_movers,B),cardinality_at_time(efficient_producers,B)). [copy(27),flip(c)]. 30 efficient_producers != A | -subpopulation(A,c1,B) | number_of_organizations(c1,B) = sum(cardinality_at_time(first_movers,B),cardinality_at_time(efficient_producers,B)). [copy(29),flip(c)]. 32 first_movers != A | -subpopulation(A,c1,B) | number_of_organizations(c1,B) = sum(cardinality_at_time(first_movers,B),cardinality_at_time(efficient_producers,B)). [copy(31),flip(c)]. 33 -in_environment(c1,A) | subpopulation(first_movers,c1,A). [resolve(1,a,5,a)]. 34 -in_environment(c1,A) | subpopulation(efficient_producers,c1,A). [resolve(1,a,6,a)]. 35 -in_environment(c1,A) | -subpopulation(B,c1,A) | -greater(cardinality_at_time(B,A),zero) | -constant(cardinality_at_time(B,A)) | growth_rate(B,A) = zero. [resolve(1,a,7,a)]. 36 -in_environment(c1,A) | -subpopulation(B,c1,A) | -greater(cardinality_at_time(B,A),zero) | -increases(cardinality_at_time(B,A)) | greater(growth_rate(B,A),zero). [resolve(1,a,8,a)]. 37 -in_environment(c1,A) | -subpopulation(B,c1,A) | -greater(cardinality_at_time(B,A),zero) | -decreases(cardinality_at_time(B,A)) | greater(zero,growth_rate(B,A)). [resolve(1,a,9,a)]. 38 -subpopulations(first_movers,efficient_producers,c1,A) | greater(cardinality_at_time(first_movers,A),zero). [resolve(1,a,10,a)]. 39 -subpopulations(first_movers,efficient_producers,c1,A) | greater(cardinality_at_time(efficient_producers,A),zero). [resolve(1,a,11,a)]. 40 -subpopulations(first_movers,efficient_producers,c1,A) | in_environment(c1,A). [resolve(1,a,12,a)]. 41 efficient_producers = A | first_movers = A | -subpopulation(A,c1,B) | -greater(cardinality_at_time(A,B),zero). [resolve(1,a,13,a)]. 42 -constant(A) | constant(B) | increases(B) | sum(B,B) != A. [factor(15,c,e)]. 43 -constant(A) | constant(B) | decreases(B) | sum(B,B) != A. [factor(16,c,e)]. end_of_list. formulas(demodulators). end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=13): 14 -constant(A) | constant(B) | increases(B) | decreases(B) | sum(B,C) != A. [assumption]. given #2 (I,wt=13): 15 -constant(A) | constant(B) | increases(B) | sum(B,C) != A | increases(C). [assumption]. given #3 (I,wt=13): 16 -constant(A) | constant(B) | decreases(B) | sum(B,C) != A | decreases(C). [assumption]. given #4 (I,wt=13): 17 -constant(A) | constant(B) | sum(B,C) != A | decreases(C) | increases(C). [assumption]. given #5 (I,wt=13): 18 -constant(A) | increases(B) | decreases(B) | sum(B,C) != A | constant(C). [assumption]. given #6 (I,wt=13): 19 -constant(A) | increases(B) | sum(B,C) != A | constant(C) | increases(C). [assumption]. given #7 (I,wt=13): 20 -constant(A) | decreases(B) | sum(B,C) != A | constant(C) | decreases(C). [assumption]. given #8 (I,wt=13): 21 -constant(A) | sum(B,C) != A | constant(C) | decreases(C) | increases(C). [assumption]. given #9 (I,wt=5): 22 subpopulations(first_movers,efficient_producers,c1,c2). [assumption]. given #10 (I,wt=4): 23 constant(number_of_organizations(c1,c2)). [assumption]. given #11 (I,wt=5): 24 growth_rate(first_movers,c2) != zero. [assumption]. given #12 (I,wt=5): 25 -greater(zero,growth_rate(efficient_producers,c2)). [assumption]. given #13 (I,wt=5): 26 -greater(zero,growth_rate(first_movers,c2)). [assumption]. given #14 (I,wt=20): 28 -subpopulation(A,c1,B) | greater(cardinality_at_time(A,B),zero) | number_of_organizations(c1,B) = sum(cardinality_at_time(first_movers,B),cardinality_at_time(efficient_producers,B)). [copy(27),flip(c)]. given #15 (I,wt=18): 30 efficient_producers != A | -subpopulation(A,c1,B) | number_of_organizations(c1,B) = sum(cardinality_at_time(first_movers,B),cardinality_at_time(efficient_producers,B)). [copy(29),flip(c)]. given #16 (I,wt=18): 32 first_movers != A | -subpopulation(A,c1,B) | number_of_organizations(c1,B) = sum(cardinality_at_time(first_movers,B),cardinality_at_time(efficient_producers,B)). [copy(31),flip(c)]. given #17 (I,wt=7): 33 -in_environment(c1,A) | subpopulation(first_movers,c1,A). [resolve(1,a,5,a)]. given #18 (I,wt=7): 34 -in_environment(c1,A) | subpopulation(efficient_producers,c1,A). [resolve(1,a,6,a)]. given #19 (I,wt=21): 35 -in_environment(c1,A) | -subpopulation(B,c1,A) | -greater(cardinality_at_time(B,A),zero) | -constant(cardinality_at_time(B,A)) | growth_rate(B,A) = zero. [resolve(1,a,7,a)]. given #20 (I,wt=21): 36 -in_environment(c1,A) | -subpopulation(B,c1,A) | -greater(cardinality_at_time(B,A),zero) | -increases(cardinality_at_time(B,A)) | greater(growth_rate(B,A),zero). [resolve(1,a,8,a)]. given #21 (I,wt=21): 37 -in_environment(c1,A) | -subpopulation(B,c1,A) | -greater(cardinality_at_time(B,A),zero) | -decreases(cardinality_at_time(B,A)) | greater(zero,growth_rate(B,A)). [resolve(1,a,9,a)]. given #22 (I,wt=10): 38 -subpopulations(first_movers,efficient_producers,c1,A) | greater(cardinality_at_time(first_movers,A),zero). [resolve(1,a,10,a)]. given #23 (I,wt=10): 39 -subpopulations(first_movers,efficient_producers,c1,A) | greater(cardinality_at_time(efficient_producers,A),zero). [resolve(1,a,11,a)]. given #24 (I,wt=8): 40 -subpopulations(first_movers,efficient_producers,c1,A) | in_environment(c1,A). [resolve(1,a,12,a)]. given #25 (I,wt=15): 41 efficient_producers = A | first_movers = A | -subpopulation(A,c1,B) | -greater(cardinality_at_time(A,B),zero). [resolve(1,a,13,a)]. given #26 (I,wt=11): 42 -constant(A) | constant(B) | increases(B) | sum(B,B) != A. [factor(15,c,e)]. given #27 (I,wt=11): 43 -constant(A) | constant(B) | decreases(B) | sum(B,B) != A. [factor(16,c,e)]. given #28 (A,wt=13): 44 sum(A,B) != number_of_organizations(c1,c2) | constant(B) | decreases(B) | increases(B). [resolve(23,a,21,a)]. given #29 (T,wt=3): 56 in_environment(c1,c2). [resolve(40,a,22,a)]. given #30 (T,wt=4): 57 subpopulation(efficient_producers,c1,c2). [resolve(56,a,34,a)]. given #31 (T,wt=4): 58 subpopulation(first_movers,c1,c2). [resolve(56,a,33,a)]. given #32 (T,wt=5): 54 greater(cardinality_at_time(first_movers,c2),zero). [resolve(38,a,22,a)]. given #33 (A,wt=5): 55 greater(cardinality_at_time(efficient_producers,c2),zero). [resolve(39,a,22,a)]. given #34 (F,wt=4): 59 -decreases(cardinality_at_time(efficient_producers,c2)). [resolve(57,a,37,b),unit_del(a,56),unit_del(b,55),unit_del(d,25)]. given #35 (F,wt=4): 75 -decreases(cardinality_at_time(first_movers,c2)). [resolve(58,a,37,b),unit_del(a,56),unit_del(b,54),unit_del(d,26)]. given #36 (F,wt=4): 77 -constant(cardinality_at_time(first_movers,c2)). [resolve(58,a,35,b),unit_del(a,56),unit_del(b,54),unit_del(d,24)]. ============================== PROOF ================================= % Proof 1 at 0.00 (+ 0.00) seconds. % Length of proof is 35. % Level of proof is 6. % Maximum clause weight is 21. % Given clauses 36. 1 environment(c1). [assumption]. 3 -environment(A) | efficient_producers != B | -subpopulation(B,A,C) | sum(cardinality_at_time(first_movers,C),cardinality_at_time(efficient_producers,C)) = number_of_organizations(A,C). [assumption]. 5 -environment(A) | -in_environment(A,B) | subpopulation(first_movers,A,B). [assumption]. 6 -environment(A) | -in_environment(A,B) | subpopulation(efficient_producers,A,B). [assumption]. 7 -environment(A) | -in_environment(A,B) | -subpopulation(C,A,B) | -greater(cardinality_at_time(C,B),zero) | -constant(cardinality_at_time(C,B)) | growth_rate(C,B) = zero. [assumption]. 9 -environment(A) | -in_environment(A,B) | -subpopulation(C,A,B) | -greater(cardinality_at_time(C,B),zero) | -decreases(cardinality_at_time(C,B)) | greater(zero,growth_rate(C,B)). [assumption]. 10 -environment(A) | -subpopulations(first_movers,efficient_producers,A,B) | greater(cardinality_at_time(first_movers,B),zero). [assumption]. 11 -environment(A) | -subpopulations(first_movers,efficient_producers,A,B) | greater(cardinality_at_time(efficient_producers,B),zero). [assumption]. 12 -environment(A) | -subpopulations(first_movers,efficient_producers,A,B) | in_environment(A,B). [assumption]. 16 -constant(A) | constant(B) | decreases(B) | sum(B,C) != A | decreases(C). [assumption]. 22 subpopulations(first_movers,efficient_producers,c1,c2). [assumption]. 23 constant(number_of_organizations(c1,c2)). [assumption]. 24 growth_rate(first_movers,c2) != zero. [assumption]. 25 -greater(zero,growth_rate(efficient_producers,c2)). [assumption]. 26 -greater(zero,growth_rate(first_movers,c2)). [assumption]. 29 efficient_producers != A | -subpopulation(A,c1,B) | sum(cardinality_at_time(first_movers,B),cardinality_at_time(efficient_producers,B)) = number_of_organizations(c1,B). [resolve(1,a,3,a)]. 30 efficient_producers != A | -subpopulation(A,c1,B) | number_of_organizations(c1,B) = sum(cardinality_at_time(first_movers,B),cardinality_at_time(efficient_producers,B)). [copy(29),flip(c)]. 33 -in_environment(c1,A) | subpopulation(first_movers,c1,A). [resolve(1,a,5,a)]. 34 -in_environment(c1,A) | subpopulation(efficient_producers,c1,A). [resolve(1,a,6,a)]. 35 -in_environment(c1,A) | -subpopulation(B,c1,A) | -greater(cardinality_at_time(B,A),zero) | -constant(cardinality_at_time(B,A)) | growth_rate(B,A) = zero. [resolve(1,a,7,a)]. 37 -in_environment(c1,A) | -subpopulation(B,c1,A) | -greater(cardinality_at_time(B,A),zero) | -decreases(cardinality_at_time(B,A)) | greater(zero,growth_rate(B,A)). [resolve(1,a,9,a)]. 38 -subpopulations(first_movers,efficient_producers,c1,A) | greater(cardinality_at_time(first_movers,A),zero). [resolve(1,a,10,a)]. 39 -subpopulations(first_movers,efficient_producers,c1,A) | greater(cardinality_at_time(efficient_producers,A),zero). [resolve(1,a,11,a)]. 40 -subpopulations(first_movers,efficient_producers,c1,A) | in_environment(c1,A). [resolve(1,a,12,a)]. 54 greater(cardinality_at_time(first_movers,c2),zero). [resolve(38,a,22,a)]. 55 greater(cardinality_at_time(efficient_producers,c2),zero). [resolve(39,a,22,a)]. 56 in_environment(c1,c2). [resolve(40,a,22,a)]. 57 subpopulation(efficient_producers,c1,c2). [resolve(56,a,34,a)]. 58 subpopulation(first_movers,c1,c2). [resolve(56,a,33,a)]. 59 -decreases(cardinality_at_time(efficient_producers,c2)). [resolve(57,a,37,b),unit_del(a,56),unit_del(b,55),unit_del(d,25)]. 63 number_of_organizations(c1,c2) = sum(cardinality_at_time(first_movers,c2),cardinality_at_time(efficient_producers,c2)). [resolve(57,a,30,b),xx(a)]. 74 constant(sum(cardinality_at_time(first_movers,c2),cardinality_at_time(efficient_producers,c2))). [back_rewrite(23),rewrite([63(3)])]. 75 -decreases(cardinality_at_time(first_movers,c2)). [resolve(58,a,37,b),unit_del(a,56),unit_del(b,54),unit_del(d,26)]. 77 -constant(cardinality_at_time(first_movers,c2)). [resolve(58,a,35,b),unit_del(a,56),unit_del(b,54),unit_del(d,24)]. 80 $F. [ur(16,b,77,a,c,75,a,d,xx,e,59,a),unit_del(a,74)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=36. Generated=85. Kept=63. proofs=1. Usable=34. Sos=15. Demods=1. Limbo=2, Disabled=50. Hints=0. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=21. Back_subsumed=1. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=1 (0 lex), Back_demodulated=11. Back_unit_deleted=0. Demod_attempts=405. Demod_rewrites=15. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=46. Nonunit_bsub_feature_tests=131. Megabytes=0.27. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 21816 exit (max_proofs) Wed May 7 22:14:46 2008 ============================== continuing FOF reduction multisearch == Subproblem 5 of 8 (negated): ((all E (- environment(E) | (all X ((all T (- subpopulation(X,E,T) | greater(cardinality_at_time(X,T),zero) | =(sum(cardinality_at_time(first_movers,T),cardinality_at_time(efficient_producers,T)),number_of_organizations(E,T)))))))) & (all E (- environment(E) | (all X (- =(efficient_producers,X) | (all T (- subpopulation(X,E,T) | =(sum(cardinality_at_time(first_movers,T),cardinality_at_time(efficient_producers,T)),number_of_organizations(E,T)))))))) & (all E (- environment(E) | (all X (- =(first_movers,X) | (all T (- subpopulation(X,E,T) | =(sum(cardinality_at_time(first_movers,T),cardinality_at_time(efficient_producers,T)),number_of_organizations(E,T)))))))) & (all E (- environment(E) | (all T (- in_environment(E,T) | subpopulation(first_movers,E,T))))) & (all E (- environment(E) | (all T (- in_environment(E,T) | subpopulation(efficient_producers,E,T))))) & (all A (- constant(A) | (all B (constant(B) | increases(B) | decreases(B) | (all C (- =(sum(B,C),A))))))) & (all A (- constant(A) | (all B (constant(B) | increases(B) | (all C (- =(sum(B,C),A) | increases(C))))))) & (all A (- constant(A) | (all B (constant(B) | decreases(B) | (all C (- =(sum(B,C),A) | decreases(C))))))) & (all A (- constant(A) | (all B (constant(B) | (all C (- =(sum(B,C),A) | decreases(C) | increases(C))))))) & (all A (- constant(A) | (all B (increases(B) | decreases(B) | (all C (- =(sum(B,C),A) | constant(C))))))) & (all A (- constant(A) | (all B (increases(B) | (all C (- =(sum(B,C),A) | constant(C) | increases(C))))))) & (all A (- constant(A) | (all B (decreases(B) | (all C (- =(sum(B,C),A) | constant(C) | decreases(C))))))) & (all A (- constant(A) | (all B ((all C (- =(sum(B,C),A) | constant(C) | decreases(C) | increases(C))))))) & (all X (all E (- environment(E) | (all T (- in_environment(E,T) | - subpopulation(X,E,T) | - greater(cardinality_at_time(X,T),zero) | - constant(cardinality_at_time(X,T)) | =(growth_rate(X,T),zero)))))) & (all X (all E (- environment(E) | (all T (- in_environment(E,T) | - subpopulation(X,E,T) | - greater(cardinality_at_time(X,T),zero) | - increases(cardinality_at_time(X,T)) | greater(growth_rate(X,T),zero)))))) & (all X (all E (- environment(E) | (all T (- in_environment(E,T) | - subpopulation(X,E,T) | - greater(cardinality_at_time(X,T),zero) | - decreases(cardinality_at_time(X,T)) | greater(zero,growth_rate(X,T))))))) & (all E (- environment(E) | (all T (- subpopulations(first_movers,efficient_producers,E,T) | greater(cardinality_at_time(first_movers,T),zero))))) & (all E (- environment(E) | (all T (- subpopulations(first_movers,efficient_producers,E,T) | greater(cardinality_at_time(efficient_producers,T),zero))))) & (all E (- environment(E) | (all T (- subpopulations(first_movers,efficient_producers,E,T) | in_environment(E,T))))) & (all E (- environment(E) | (all X (=(efficient_producers,X) | =(first_movers,X) | (all T (- subpopulation(X,E,T) | - greater(cardinality_at_time(X,T),zero))))))) & (exists E (environment(E) & (exists T (subpopulations(first_movers,efficient_producers,E,T) & constant(number_of_organizations(E,T)) & - =(growth_rate(efficient_producers,T),zero) & - greater(growth_rate(first_movers,T),zero) & - greater(growth_rate(efficient_producers,T),zero)))))). Max_seconds is 30 for this subproblem. Child search process 21817 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). -environment(A) | -subpopulation(B,A,C) | greater(cardinality_at_time(B,C),zero) | sum(cardinality_at_time(first_movers,C),cardinality_at_time(efficient_producers,C)) = number_of_organizations(A,C). [assumption]. -environment(A) | efficient_producers != B | -subpopulation(B,A,C) | sum(cardinality_at_time(first_movers,C),cardinality_at_time(efficient_producers,C)) = number_of_organizations(A,C). [assumption]. -environment(A) | first_movers != B | -subpopulation(B,A,C) | sum(cardinality_at_time(first_movers,C),cardinality_at_time(efficient_producers,C)) = number_of_organizations(A,C). [assumption]. -environment(A) | -in_environment(A,B) | subpopulation(first_movers,A,B). [assumption]. -environment(A) | -in_environment(A,B) | subpopulation(efficient_producers,A,B). [assumption]. -constant(A) | constant(B) | increases(B) | decreases(B) | sum(B,C) != A. [assumption]. -constant(A) | constant(B) | increases(B) | sum(B,C) != A | increases(C). [assumption]. -constant(A) | constant(B) | decreases(B) | sum(B,C) != A | decreases(C). [assumption]. -constant(A) | constant(B) | sum(B,C) != A | decreases(C) | increases(C). [assumption]. -constant(A) | increases(B) | decreases(B) | sum(B,C) != A | constant(C). [assumption]. -constant(A) | increases(B) | sum(B,C) != A | constant(C) | increases(C). [assumption]. -constant(A) | decreases(B) | sum(B,C) != A | constant(C) | decreases(C). [assumption]. -constant(A) | sum(B,C) != A | constant(C) | decreases(C) | increases(C). [assumption]. -environment(A) | -in_environment(A,B) | -subpopulation(C,A,B) | -greater(cardinality_at_time(C,B),zero) | -constant(cardinality_at_time(C,B)) | growth_rate(C,B) = zero. [assumption]. -environment(A) | -in_environment(A,B) | -subpopulation(C,A,B) | -greater(cardinality_at_time(C,B),zero) | -increases(cardinality_at_time(C,B)) | greater(growth_rate(C,B),zero). [assumption]. -environment(A) | -in_environment(A,B) | -subpopulation(C,A,B) | -greater(cardinality_at_time(C,B),zero) | -decreases(cardinality_at_time(C,B)) | greater(zero,growth_rate(C,B)). [assumption]. -environment(A) | -subpopulations(first_movers,efficient_producers,A,B) | greater(cardinality_at_time(first_movers,B),zero). [assumption]. -environment(A) | -subpopulations(first_movers,efficient_producers,A,B) | greater(cardinality_at_time(efficient_producers,B),zero). [assumption]. -environment(A) | -subpopulations(first_movers,efficient_producers,A,B) | in_environment(A,B). [assumption]. -environment(A) | efficient_producers = B | first_movers = B | -subpopulation(B,A,C) | -greater(cardinality_at_time(B,C),zero). [assumption]. environment(c1). [assumption]. subpopulations(first_movers,efficient_producers,c1,c2). [assumption]. constant(number_of_organizations(c1,c2)). [assumption]. growth_rate(efficient_producers,c2) != zero. [assumption]. -greater(growth_rate(first_movers,c2),zero). [assumption]. -greater(growth_rate(efficient_producers,c2),zero). [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= Eliminating environment/1 1 environment(c1). [assumption]. 2 -environment(A) | -subpopulation(B,A,C) | greater(cardinality_at_time(B,C),zero) | sum(cardinality_at_time(first_movers,C),cardinality_at_time(efficient_producers,C)) = number_of_organizations(A,C). [assumption]. 3 -environment(A) | efficient_producers != B | -subpopulation(B,A,C) | sum(cardinality_at_time(first_movers,C),cardinality_at_time(efficient_producers,C)) = number_of_organizations(A,C). [assumption]. 4 -environment(A) | first_movers != B | -subpopulation(B,A,C) | sum(cardinality_at_time(first_movers,C),cardinality_at_time(efficient_producers,C)) = number_of_organizations(A,C). [assumption]. 5 -environment(A) | -in_environment(A,B) | subpopulation(first_movers,A,B). [assumption]. 6 -environment(A) | -in_environment(A,B) | subpopulation(efficient_producers,A,B). [assumption]. 7 -environment(A) | -in_environment(A,B) | -subpopulation(C,A,B) | -greater(cardinality_at_time(C,B),zero) | -constant(cardinality_at_time(C,B)) | growth_rate(C,B) = zero. [assumption]. 8 -environment(A) | -in_environment(A,B) | -subpopulation(C,A,B) | -greater(cardinality_at_time(C,B),zero) | -increases(cardinality_at_time(C,B)) | greater(growth_rate(C,B),zero). [assumption]. 9 -environment(A) | -in_environment(A,B) | -subpopulation(C,A,B) | -greater(cardinality_at_time(C,B),zero) | -decreases(cardinality_at_time(C,B)) | greater(zero,growth_rate(C,B)). [assumption]. 10 -environment(A) | -subpopulations(first_movers,efficient_producers,A,B) | greater(cardinality_at_time(first_movers,B),zero). [assumption]. 11 -environment(A) | -subpopulations(first_movers,efficient_producers,A,B) | greater(cardinality_at_time(efficient_producers,B),zero). [assumption]. 12 -environment(A) | -subpopulations(first_movers,efficient_producers,A,B) | in_environment(A,B). [assumption]. 13 -environment(A) | efficient_producers = B | first_movers = B | -subpopulation(B,A,C) | -greater(cardinality_at_time(B,C),zero). [assumption]. Derived: -subpopulation(A,c1,B) | greater(cardinality_at_time(A,B),zero) | sum(cardinality_at_time(first_movers,B),cardinality_at_time(efficient_producers,B)) = number_of_organizations(c1,B). [resolve(1,a,2,a)]. Derived: efficient_producers != A | -subpopulation(A,c1,B) | sum(cardinality_at_time(first_movers,B),cardinality_at_time(efficient_producers,B)) = number_of_organizations(c1,B). [resolve(1,a,3,a)]. Derived: first_movers != A | -subpopulation(A,c1,B) | sum(cardinality_at_time(first_movers,B),cardinality_at_time(efficient_producers,B)) = number_of_organizations(c1,B). [resolve(1,a,4,a)]. Derived: -in_environment(c1,A) | subpopulation(first_movers,c1,A). [resolve(1,a,5,a)]. Derived: -in_environment(c1,A) | subpopulation(efficient_producers,c1,A). [resolve(1,a,6,a)]. Derived: -in_environment(c1,A) | -subpopulation(B,c1,A) | -greater(cardinality_at_time(B,A),zero) | -constant(cardinality_at_time(B,A)) | growth_rate(B,A) = zero. [resolve(1,a,7,a)]. Derived: -in_environment(c1,A) | -subpopulation(B,c1,A) | -greater(cardinality_at_time(B,A),zero) | -increases(cardinality_at_time(B,A)) | greater(growth_rate(B,A),zero). [resolve(1,a,8,a)]. Derived: -in_environment(c1,A) | -subpopulation(B,c1,A) | -greater(cardinality_at_time(B,A),zero) | -decreases(cardinality_at_time(B,A)) | greater(zero,growth_rate(B,A)). [resolve(1,a,9,a)]. Derived: -subpopulations(first_movers,efficient_producers,c1,A) | greater(cardinality_at_time(first_movers,A),zero). [resolve(1,a,10,a)]. Derived: -subpopulations(first_movers,efficient_producers,c1,A) | greater(cardinality_at_time(efficient_producers,A),zero). [resolve(1,a,11,a)]. Derived: -subpopulations(first_movers,efficient_producers,c1,A) | in_environment(c1,A). [resolve(1,a,12,a)]. Derived: efficient_producers = A | first_movers = A | -subpopulation(A,c1,B) | -greater(cardinality_at_time(A,B),zero). [resolve(1,a,13,a)]. ============================== end predicate elimination ============= Term ordering decisions: Predicate symbol precedence: predicate_order([ =, constant, decreases, increases, greater, in_environment, subpopulation, subpopulations ]). Function symbol precedence: function_order([ efficient_producers, first_movers, zero, c1, c2, cardinality_at_time, sum, number_of_organizations, growth_rate ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(binary_resolution). % (non-Horn) % set(neg_ur_resolution). % (non-Horn, less than 100 clauses) Auto_process settings: % set(factor). % (non-Horn) % set(unit_deletion). % (non-Horn) ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 14 -constant(A) | constant(B) | increases(B) | decreases(B) | sum(B,C) != A. [assumption]. 15 -constant(A) | constant(B) | increases(B) | sum(B,C) != A | increases(C). [assumption]. 16 -constant(A) | constant(B) | decreases(B) | sum(B,C) != A | decreases(C). [assumption]. 17 -constant(A) | constant(B) | sum(B,C) != A | decreases(C) | increases(C). [assumption]. 18 -constant(A) | increases(B) | decreases(B) | sum(B,C) != A | constant(C). [assumption]. 19 -constant(A) | increases(B) | sum(B,C) != A | constant(C) | increases(C). [assumption]. 20 -constant(A) | decreases(B) | sum(B,C) != A | constant(C) | decreases(C). [assumption]. 21 -constant(A) | sum(B,C) != A | constant(C) | decreases(C) | increases(C). [assumption]. 22 subpopulations(first_movers,efficient_producers,c1,c2). [assumption]. 23 constant(number_of_organizations(c1,c2)). [assumption]. 24 growth_rate(efficient_producers,c2) != zero. [assumption]. 25 -greater(growth_rate(first_movers,c2),zero). [assumption]. 26 -greater(growth_rate(efficient_producers,c2),zero). [assumption]. 28 -subpopulation(A,c1,B) | greater(cardinality_at_time(A,B),zero) | number_of_organizations(c1,B) = sum(cardinality_at_time(first_movers,B),cardinality_at_time(efficient_producers,B)). [copy(27),flip(c)]. 30 efficient_producers != A | -subpopulation(A,c1,B) | number_of_organizations(c1,B) = sum(cardinality_at_time(first_movers,B),cardinality_at_time(efficient_producers,B)). [copy(29),flip(c)]. 32 first_movers != A | -subpopulation(A,c1,B) | number_of_organizations(c1,B) = sum(cardinality_at_time(first_movers,B),cardinality_at_time(efficient_producers,B)). [copy(31),flip(c)]. 33 -in_environment(c1,A) | subpopulation(first_movers,c1,A). [resolve(1,a,5,a)]. 34 -in_environment(c1,A) | subpopulation(efficient_producers,c1,A). [resolve(1,a,6,a)]. 35 -in_environment(c1,A) | -subpopulation(B,c1,A) | -greater(cardinality_at_time(B,A),zero) | -constant(cardinality_at_time(B,A)) | growth_rate(B,A) = zero. [resolve(1,a,7,a)]. 36 -in_environment(c1,A) | -subpopulation(B,c1,A) | -greater(cardinality_at_time(B,A),zero) | -increases(cardinality_at_time(B,A)) | greater(growth_rate(B,A),zero). [resolve(1,a,8,a)]. 37 -in_environment(c1,A) | -subpopulation(B,c1,A) | -greater(cardinality_at_time(B,A),zero) | -decreases(cardinality_at_time(B,A)) | greater(zero,growth_rate(B,A)). [resolve(1,a,9,a)]. 38 -subpopulations(first_movers,efficient_producers,c1,A) | greater(cardinality_at_time(first_movers,A),zero). [resolve(1,a,10,a)]. 39 -subpopulations(first_movers,efficient_producers,c1,A) | greater(cardinality_at_time(efficient_producers,A),zero). [resolve(1,a,11,a)]. 40 -subpopulations(first_movers,efficient_producers,c1,A) | in_environment(c1,A). [resolve(1,a,12,a)]. 41 efficient_producers = A | first_movers = A | -subpopulation(A,c1,B) | -greater(cardinality_at_time(A,B),zero). [resolve(1,a,13,a)]. 42 -constant(A) | constant(B) | increases(B) | sum(B,B) != A. [factor(15,c,e)]. 43 -constant(A) | constant(B) | decreases(B) | sum(B,B) != A. [factor(16,c,e)]. end_of_list. formulas(demodulators). end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=13): 14 -constant(A) | constant(B) | increases(B) | decreases(B) | sum(B,C) != A. [assumption]. given #2 (I,wt=13): 15 -constant(A) | constant(B) | increases(B) | sum(B,C) != A | increases(C). [assumption]. given #3 (I,wt=13): 16 -constant(A) | constant(B) | decreases(B) | sum(B,C) != A | decreases(C). [assumption]. given #4 (I,wt=13): 17 -constant(A) | constant(B) | sum(B,C) != A | decreases(C) | increases(C). [assumption]. given #5 (I,wt=13): 18 -constant(A) | increases(B) | decreases(B) | sum(B,C) != A | constant(C). [assumption]. given #6 (I,wt=13): 19 -constant(A) | increases(B) | sum(B,C) != A | constant(C) | increases(C). [assumption]. given #7 (I,wt=13): 20 -constant(A) | decreases(B) | sum(B,C) != A | constant(C) | decreases(C). [assumption]. given #8 (I,wt=13): 21 -constant(A) | sum(B,C) != A | constant(C) | decreases(C) | increases(C). [assumption]. given #9 (I,wt=5): 22 subpopulations(first_movers,efficient_producers,c1,c2). [assumption]. given #10 (I,wt=4): 23 constant(number_of_organizations(c1,c2)). [assumption]. given #11 (I,wt=5): 24 growth_rate(efficient_producers,c2) != zero. [assumption]. given #12 (I,wt=5): 25 -greater(growth_rate(first_movers,c2),zero). [assumption]. given #13 (I,wt=5): 26 -greater(growth_rate(efficient_producers,c2),zero). [assumption]. given #14 (I,wt=20): 28 -subpopulation(A,c1,B) | greater(cardinality_at_time(A,B),zero) | number_of_organizations(c1,B) = sum(cardinality_at_time(first_movers,B),cardinality_at_time(efficient_producers,B)). [copy(27),flip(c)]. given #15 (I,wt=18): 30 efficient_producers != A | -subpopulation(A,c1,B) | number_of_organizations(c1,B) = sum(cardinality_at_time(first_movers,B),cardinality_at_time(efficient_producers,B)). [copy(29),flip(c)]. given #16 (I,wt=18): 32 first_movers != A | -subpopulation(A,c1,B) | number_of_organizations(c1,B) = sum(cardinality_at_time(first_movers,B),cardinality_at_time(efficient_producers,B)). [copy(31),flip(c)]. given #17 (I,wt=7): 33 -in_environment(c1,A) | subpopulation(first_movers,c1,A). [resolve(1,a,5,a)]. given #18 (I,wt=7): 34 -in_environment(c1,A) | subpopulation(efficient_producers,c1,A). [resolve(1,a,6,a)]. given #19 (I,wt=21): 35 -in_environment(c1,A) | -subpopulation(B,c1,A) | -greater(cardinality_at_time(B,A),zero) | -constant(cardinality_at_time(B,A)) | growth_rate(B,A) = zero. [resolve(1,a,7,a)]. given #20 (I,wt=21): 36 -in_environment(c1,A) | -subpopulation(B,c1,A) | -greater(cardinality_at_time(B,A),zero) | -increases(cardinality_at_time(B,A)) | greater(growth_rate(B,A),zero). [resolve(1,a,8,a)]. given #21 (I,wt=21): 37 -in_environment(c1,A) | -subpopulation(B,c1,A) | -greater(cardinality_at_time(B,A),zero) | -decreases(cardinality_at_time(B,A)) | greater(zero,growth_rate(B,A)). [resolve(1,a,9,a)]. given #22 (I,wt=10): 38 -subpopulations(first_movers,efficient_producers,c1,A) | greater(cardinality_at_time(first_movers,A),zero). [resolve(1,a,10,a)]. given #23 (I,wt=10): 39 -subpopulations(first_movers,efficient_producers,c1,A) | greater(cardinality_at_time(efficient_producers,A),zero). [resolve(1,a,11,a)]. given #24 (I,wt=8): 40 -subpopulations(first_movers,efficient_producers,c1,A) | in_environment(c1,A). [resolve(1,a,12,a)]. given #25 (I,wt=15): 41 efficient_producers = A | first_movers = A | -subpopulation(A,c1,B) | -greater(cardinality_at_time(A,B),zero). [resolve(1,a,13,a)]. given #26 (I,wt=11): 42 -constant(A) | constant(B) | increases(B) | sum(B,B) != A. [factor(15,c,e)]. given #27 (I,wt=11): 43 -constant(A) | constant(B) | decreases(B) | sum(B,B) != A. [factor(16,c,e)]. given #28 (A,wt=13): 44 sum(A,B) != number_of_organizations(c1,c2) | constant(B) | decreases(B) | increases(B). [resolve(23,a,21,a)]. given #29 (T,wt=3): 56 in_environment(c1,c2). [resolve(40,a,22,a)]. given #30 (T,wt=4): 57 subpopulation(efficient_producers,c1,c2). [resolve(56,a,34,a)]. given #31 (T,wt=4): 58 subpopulation(first_movers,c1,c2). [resolve(56,a,33,a)]. given #32 (T,wt=5): 54 greater(cardinality_at_time(first_movers,c2),zero). [resolve(38,a,22,a)]. given #33 (A,wt=5): 55 greater(cardinality_at_time(efficient_producers,c2),zero). [resolve(39,a,22,a)]. given #34 (F,wt=4): 60 -increases(cardinality_at_time(efficient_producers,c2)). [resolve(57,a,36,b),unit_del(a,56),unit_del(b,55),unit_del(d,26)]. given #35 (F,wt=4): 61 -constant(cardinality_at_time(efficient_producers,c2)). [resolve(57,a,35,b),unit_del(a,56),unit_del(b,55),unit_del(d,24)]. given #36 (F,wt=4): 76 -increases(cardinality_at_time(first_movers,c2)). [resolve(58,a,36,b),unit_del(a,56),unit_del(b,54),unit_del(d,25)]. ============================== PROOF ================================= % Proof 1 at 0.00 (+ 0.00) seconds. % Length of proof is 35. % Level of proof is 6. % Maximum clause weight is 21. % Given clauses 36. 1 environment(c1). [assumption]. 3 -environment(A) | efficient_producers != B | -subpopulation(B,A,C) | sum(cardinality_at_time(first_movers,C),cardinality_at_time(efficient_producers,C)) = number_of_organizations(A,C). [assumption]. 5 -environment(A) | -in_environment(A,B) | subpopulation(first_movers,A,B). [assumption]. 6 -environment(A) | -in_environment(A,B) | subpopulation(efficient_producers,A,B). [assumption]. 7 -environment(A) | -in_environment(A,B) | -subpopulation(C,A,B) | -greater(cardinality_at_time(C,B),zero) | -constant(cardinality_at_time(C,B)) | growth_rate(C,B) = zero. [assumption]. 8 -environment(A) | -in_environment(A,B) | -subpopulation(C,A,B) | -greater(cardinality_at_time(C,B),zero) | -increases(cardinality_at_time(C,B)) | greater(growth_rate(C,B),zero). [assumption]. 10 -environment(A) | -subpopulations(first_movers,efficient_producers,A,B) | greater(cardinality_at_time(first_movers,B),zero). [assumption]. 11 -environment(A) | -subpopulations(first_movers,efficient_producers,A,B) | greater(cardinality_at_time(efficient_producers,B),zero). [assumption]. 12 -environment(A) | -subpopulations(first_movers,efficient_producers,A,B) | in_environment(A,B). [assumption]. 19 -constant(A) | increases(B) | sum(B,C) != A | constant(C) | increases(C). [assumption]. 22 subpopulations(first_movers,efficient_producers,c1,c2). [assumption]. 23 constant(number_of_organizations(c1,c2)). [assumption]. 24 growth_rate(efficient_producers,c2) != zero. [assumption]. 25 -greater(growth_rate(first_movers,c2),zero). [assumption]. 26 -greater(growth_rate(efficient_producers,c2),zero). [assumption]. 29 efficient_producers != A | -subpopulation(A,c1,B) | sum(cardinality_at_time(first_movers,B),cardinality_at_time(efficient_producers,B)) = number_of_organizations(c1,B). [resolve(1,a,3,a)]. 30 efficient_producers != A | -subpopulation(A,c1,B) | number_of_organizations(c1,B) = sum(cardinality_at_time(first_movers,B),cardinality_at_time(efficient_producers,B)). [copy(29),flip(c)]. 33 -in_environment(c1,A) | subpopulation(first_movers,c1,A). [resolve(1,a,5,a)]. 34 -in_environment(c1,A) | subpopulation(efficient_producers,c1,A). [resolve(1,a,6,a)]. 35 -in_environment(c1,A) | -subpopulation(B,c1,A) | -greater(cardinality_at_time(B,A),zero) | -constant(cardinality_at_time(B,A)) | growth_rate(B,A) = zero. [resolve(1,a,7,a)]. 36 -in_environment(c1,A) | -subpopulation(B,c1,A) | -greater(cardinality_at_time(B,A),zero) | -increases(cardinality_at_time(B,A)) | greater(growth_rate(B,A),zero). [resolve(1,a,8,a)]. 38 -subpopulations(first_movers,efficient_producers,c1,A) | greater(cardinality_at_time(first_movers,A),zero). [resolve(1,a,10,a)]. 39 -subpopulations(first_movers,efficient_producers,c1,A) | greater(cardinality_at_time(efficient_producers,A),zero). [resolve(1,a,11,a)]. 40 -subpopulations(first_movers,efficient_producers,c1,A) | in_environment(c1,A). [resolve(1,a,12,a)]. 54 greater(cardinality_at_time(first_movers,c2),zero). [resolve(38,a,22,a)]. 55 greater(cardinality_at_time(efficient_producers,c2),zero). [resolve(39,a,22,a)]. 56 in_environment(c1,c2). [resolve(40,a,22,a)]. 57 subpopulation(efficient_producers,c1,c2). [resolve(56,a,34,a)]. 58 subpopulation(first_movers,c1,c2). [resolve(56,a,33,a)]. 60 -increases(cardinality_at_time(efficient_producers,c2)). [resolve(57,a,36,b),unit_del(a,56),unit_del(b,55),unit_del(d,26)]. 61 -constant(cardinality_at_time(efficient_producers,c2)). [resolve(57,a,35,b),unit_del(a,56),unit_del(b,55),unit_del(d,24)]. 63 number_of_organizations(c1,c2) = sum(cardinality_at_time(first_movers,c2),cardinality_at_time(efficient_producers,c2)). [resolve(57,a,30,b),xx(a)]. 74 constant(sum(cardinality_at_time(first_movers,c2),cardinality_at_time(efficient_producers,c2))). [back_rewrite(23),rewrite([63(3)])]. 76 -increases(cardinality_at_time(first_movers,c2)). [resolve(58,a,36,b),unit_del(a,56),unit_del(b,54),unit_del(d,25)]. 79 $F. [ur(19,b,76,a,c,xx,d,61,a,e,60,a),unit_del(a,74)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=36. Generated=84. Kept=62. proofs=1. Usable=34. Sos=16. Demods=1. Limbo=0, Disabled=50. Hints=0. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=21. Back_subsumed=1. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=1 (0 lex), Back_demodulated=11. Back_unit_deleted=0. Demod_attempts=397. Demod_rewrites=15. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=46. Nonunit_bsub_feature_tests=131. Megabytes=0.27. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 21817 exit (max_proofs) Wed May 7 22:14:46 2008 ============================== continuing FOF reduction multisearch == Subproblem 6 of 8 (negated): ((all E (- environment(E) | (all X ((all T (- subpopulation(X,E,T) | greater(cardinality_at_time(X,T),zero) | =(sum(cardinality_at_time(first_movers,T),cardinality_at_time(efficient_producers,T)),number_of_organizations(E,T)))))))) & (all E (- environment(E) | (all X (- =(efficient_producers,X) | (all T (- subpopulation(X,E,T) | =(sum(cardinality_at_time(first_movers,T),cardinality_at_time(efficient_producers,T)),number_of_organizations(E,T)))))))) & (all E (- environment(E) | (all X (- =(first_movers,X) | (all T (- subpopulation(X,E,T) | =(sum(cardinality_at_time(first_movers,T),cardinality_at_time(efficient_producers,T)),number_of_organizations(E,T)))))))) & (all E (- environment(E) | (all T (- in_environment(E,T) | subpopulation(first_movers,E,T))))) & (all E (- environment(E) | (all T (- in_environment(E,T) | subpopulation(efficient_producers,E,T))))) & (all A (- constant(A) | (all B (constant(B) | increases(B) | decreases(B) | (all C (- =(sum(B,C),A))))))) & (all A (- constant(A) | (all B (constant(B) | increases(B) | (all C (- =(sum(B,C),A) | increases(C))))))) & (all A (- constant(A) | (all B (constant(B) | decreases(B) | (all C (- =(sum(B,C),A) | decreases(C))))))) & (all A (- constant(A) | (all B (constant(B) | (all C (- =(sum(B,C),A) | decreases(C) | increases(C))))))) & (all A (- constant(A) | (all B (increases(B) | decreases(B) | (all C (- =(sum(B,C),A) | constant(C))))))) & (all A (- constant(A) | (all B (increases(B) | (all C (- =(sum(B,C),A) | constant(C) | increases(C))))))) & (all A (- constant(A) | (all B (decreases(B) | (all C (- =(sum(B,C),A) | constant(C) | decreases(C))))))) & (all A (- constant(A) | (all B ((all C (- =(sum(B,C),A) | constant(C) | decreases(C) | increases(C))))))) & (all X (all E (- environment(E) | (all T (- in_environment(E,T) | - subpopulation(X,E,T) | - greater(cardinality_at_time(X,T),zero) | - constant(cardinality_at_time(X,T)) | =(growth_rate(X,T),zero)))))) & (all X (all E (- environment(E) | (all T (- in_environment(E,T) | - subpopulation(X,E,T) | - greater(cardinality_at_time(X,T),zero) | - increases(cardinality_at_time(X,T)) | greater(growth_rate(X,T),zero)))))) & (all X (all E (- environment(E) | (all T (- in_environment(E,T) | - subpopulation(X,E,T) | - greater(cardinality_at_time(X,T),zero) | - decreases(cardinality_at_time(X,T)) | greater(zero,growth_rate(X,T))))))) & (all E (- environment(E) | (all T (- subpopulations(first_movers,efficient_producers,E,T) | greater(cardinality_at_time(first_movers,T),zero))))) & (all E (- environment(E) | (all T (- subpopulations(first_movers,efficient_producers,E,T) | greater(cardinality_at_time(efficient_producers,T),zero))))) & (all E (- environment(E) | (all T (- subpopulations(first_movers,efficient_producers,E,T) | in_environment(E,T))))) & (all E (- environment(E) | (all X (=(efficient_producers,X) | =(first_movers,X) | (all T (- subpopulation(X,E,T) | - greater(cardinality_at_time(X,T),zero))))))) & (exists E (environment(E) & (exists T (subpopulations(first_movers,efficient_producers,E,T) & constant(number_of_organizations(E,T)) & - =(growth_rate(efficient_producers,T),zero) & - greater(growth_rate(first_movers,T),zero) & - greater(zero,growth_rate(first_movers,T))))))). Max_seconds is 30 for this subproblem. Child search process 21818 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). -environment(A) | -subpopulation(B,A,C) | greater(cardinality_at_time(B,C),zero) | sum(cardinality_at_time(first_movers,C),cardinality_at_time(efficient_producers,C)) = number_of_organizations(A,C). [assumption]. -environment(A) | efficient_producers != B | -subpopulation(B,A,C) | sum(cardinality_at_time(first_movers,C),cardinality_at_time(efficient_producers,C)) = number_of_organizations(A,C). [assumption]. -environment(A) | first_movers != B | -subpopulation(B,A,C) | sum(cardinality_at_time(first_movers,C),cardinality_at_time(efficient_producers,C)) = number_of_organizations(A,C). [assumption]. -environment(A) | -in_environment(A,B) | subpopulation(first_movers,A,B). [assumption]. -environment(A) | -in_environment(A,B) | subpopulation(efficient_producers,A,B). [assumption]. -constant(A) | constant(B) | increases(B) | decreases(B) | sum(B,C) != A. [assumption]. -constant(A) | constant(B) | increases(B) | sum(B,C) != A | increases(C). [assumption]. -constant(A) | constant(B) | decreases(B) | sum(B,C) != A | decreases(C). [assumption]. -constant(A) | constant(B) | sum(B,C) != A | decreases(C) | increases(C). [assumption]. -constant(A) | increases(B) | decreases(B) | sum(B,C) != A | constant(C). [assumption]. -constant(A) | increases(B) | sum(B,C) != A | constant(C) | increases(C). [assumption]. -constant(A) | decreases(B) | sum(B,C) != A | constant(C) | decreases(C). [assumption]. -constant(A) | sum(B,C) != A | constant(C) | decreases(C) | increases(C). [assumption]. -env