============================== FOF-Prover9 =========================== FOF-Prover9 (32) version November-2006, November 2006. Process 3759 was started by mccune on cleo.thornwood, Wed Nov 22 11:23:39 2006 The command was "/home/mccune/bin/fof-prover9 -f MGT025+1.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file MGT025+1.in 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)))))). Child search process 3760 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: Relation symbol precedence: lex([ constant, decreases, increases, greater, in_environment, subpopulation, subpopulations, =, environment ]). Function symbol precedence: lex([ 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(paramodulation) -> set(back_demod). % set(binary_resolution). % (non-Horn) % set(neg_ur_resolution). % (non-Horn, less than 100 clauses) Auto_process settings: % set(factor). % (non-Horn) % set(back_unit_deletion). % (non-Horn) % set(back_unit_deletion) -> set(unit_deletion). ============================== 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 (F,wt=3): 58 in_environment(c1,c2). [resolve(40,a,22,a)]. given #29 (T,wt=4): 59 subpopulation(efficient_producers,c1,c2). [resolve(58,a,34,a)]. given #30 (T,wt=4): 60 subpopulation(first_movers,c1,c2). [resolve(58,a,33,a)]. given #31 (A,wt=10): 44 -constant(sum(A,B)) | constant(A) | increases(A) | decreases(A). [xx_res(14,e)]. given #32 (F,wt=4): 62 -increases(cardinality_at_time(efficient_producers,c2)). [resolve(59,a,36,b),unit_del(a,58),unit_del(b,57),unit_del(d,26)]. given #33 (F,wt=4): 65 -increases(cardinality_at_time(first_movers,c2)). [resolve(60,a,36,b),unit_del(a,58),unit_del(b,56),unit_del(d,25)]. given #34 (T,wt=5): 56 greater(cardinality_at_time(first_movers,c2),zero). [resolve(38,a,22,a)]. given #35 (T,wt=5): 57 greater(cardinality_at_time(efficient_producers,c2),zero). [resolve(39,a,22,a)]. given #36 (A,wt=10): 45 -constant(sum(A,B)) | constant(A) | increases(A) | increases(B). [xx_res(15,d)]. given #37 (F,wt=4): 66 -constant(cardinality_at_time(first_movers,c2)). [resolve(60,a,35,b),unit_del(a,58),unit_del(b,56),unit_del(d,24)]. given #38 (F,wt=8): 67 -constant(sum(cardinality_at_time(first_movers,c2),cardinality_at_time(first_movers,c2))). [ur(45,b,66,a,c,65,a,d,65,a)]. given #39 (T,wt=8): 46 -constant(sum(A,A)) | constant(A) | increases(A). [factor(45,c,d)]. given #40 (T,wt=8): 48 -constant(sum(A,A)) | constant(A) | decreases(A). [factor(47,c,d)]. given #41 (A,wt=10): 47 -constant(sum(A,B)) | constant(A) | decreases(A) | decreases(B). [xx_res(16,d)]. given #42 (F,wt=8): 68 -constant(sum(cardinality_at_time(first_movers,c2),cardinality_at_time(efficient_producers,c2))). [ur(45,b,66,a,c,65,a,d,62,a)]. given #43 (F,wt=8): 70 -constant(sum(cardinality_at_time(efficient_producers,c2),cardinality_at_time(first_movers,c2))). [ur(19,b,62,a,c,xx,d,66,a,e,65,a)]. given #44 (T,wt=9): 61 -decreases(cardinality_at_time(efficient_producers,c2)) | greater(zero,growth_rate(efficient_producers,c2)). [resolve(59,a,37,b),unit_del(a,58),unit_del(b,57)]. given #45 (T,wt=9): 63 -constant(cardinality_at_time(efficient_producers,c2)) | growth_rate(efficient_producers,c2) = zero. [resolve(59,a,35,b),unit_del(a,58),unit_del(b,57)]. given #46 (A,wt=10): 49 -constant(sum(A,B)) | constant(A) | decreases(B) | increases(B). [xx_res(17,c)]. given #47 (F,wt=11): 69 number_of_organizations(c1,c2) != sum(cardinality_at_time(first_movers,c2),cardinality_at_time(first_movers,c2)). [ur(42,a,23,a,b,66,a,c,65,a),flip(a)]. given #48 (F,wt=11): 71 number_of_organizations(c1,c2) != sum(cardinality_at_time(efficient_producers,c2),cardinality_at_time(first_movers,c2)). [ur(19,a,23,a,b,62,a,d,66,a,e,65,a),flip(a)]. given #49 (T,wt=9): 64 -decreases(cardinality_at_time(first_movers,c2)) | greater(zero,growth_rate(first_movers,c2)). [resolve(60,a,37,b),unit_del(a,58),unit_del(b,56)]. given #50 (T,wt=10): 50 -constant(sum(A,B)) | increases(A) | decreases(A) | constant(B). [xx_res(18,d)]. given #51 (A,wt=10): 51 -constant(sum(A,B)) | increases(A) | constant(B) | increases(B). [xx_res(19,c)]. given #52 (F,wt=11): 72 number_of_organizations(c1,c2) != sum(cardinality_at_time(first_movers,c2),cardinality_at_time(efficient_producers,c2)). [ur(15,a,23,a,b,66,a,c,65,a,e,62,a),flip(a)]. ============================== PROOF ================================= % Proof 1 at 0.00 (+ 0.01) seconds. % Length of proof is 34. % Level of proof is 6. % Maximum clause weight is 21. % Given clauses 52. 1 environment(c1). [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]. 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]. 31 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)]. 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)]. 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)]. 56 greater(cardinality_at_time(first_movers,c2),zero). [resolve(38,a,22,a)]. 57 greater(cardinality_at_time(efficient_producers,c2),zero). [resolve(39,a,22,a)]. 58 in_environment(c1,c2). [resolve(40,a,22,a)]. 59 subpopulation(efficient_producers,c1,c2). [resolve(58,a,34,a)]. 60 subpopulation(first_movers,c1,c2). [resolve(58,a,33,a)]. 62 -increases(cardinality_at_time(efficient_producers,c2)). [resolve(59,a,36,b),unit_del(a,58),unit_del(b,57),unit_del(d,26)]. 65 -increases(cardinality_at_time(first_movers,c2)). [resolve(60,a,36,b),unit_del(a,58),unit_del(b,56),unit_del(d,25)]. 66 -constant(cardinality_at_time(first_movers,c2)). [resolve(60,a,35,b),unit_del(a,58),unit_del(b,56),unit_del(d,24)]. 72 number_of_organizations(c1,c2) != sum(cardinality_at_time(first_movers,c2),cardinality_at_time(efficient_producers,c2)). [ur(15,a,23,a,b,66,a,c,65,a,e,62,a),flip(a)]. 73 $F. [ur(32,b,60,a,c,72,a),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=52. Generated=79. Kept=56. proofs=1. Usable=52. Sos=4. Demods=0. Limbo=0, Disabled=38. Hints=0. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=22. Back_subsumed=0. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=0. Demod_rewrites=0. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=30. Nonunit_bsub_feature_tests=117. Megabytes=0.26. User_CPU=0.00, System_CPU=0.01, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 3760 exit (max_proofs) Wed Nov 22 11:23:39 2006 ============================== 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))))))). Child search process 3761 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: Relation symbol precedence: lex([ constant, decreases, increases, greater, in_environment, subpopulation, subpopulations, =, environment ]). Function symbol precedence: lex([ 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(paramodulation) -> set(back_demod). % set(binary_resolution). % (non-Horn) % set(neg_ur_resolution). % (non-Horn, less than 100 clauses) Auto_process settings: % set(factor). % (non-Horn) % set(back_unit_deletion). % (non-Horn) % set(back_unit_deletion) -> set(unit_deletion). ============================== 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 (F,wt=3): 58 in_environment(c1,c2). [resolve(40,a,22,a)]. given #29 (T,wt=4): 59 subpopulation(efficient_producers,c1,c2). [resolve(58,a,34,a)]. given #30 (T,wt=4): 60 subpopulation(first_movers,c1,c2). [resolve(58,a,33,a)]. given #31 (A,wt=10): 44 -constant(sum(A,B)) | constant(A) | increases(A) | decreases(A). [xx_res(14,e)]. given #32 (F,wt=4): 64 -decreases(cardinality_at_time(first_movers,c2)). [resolve(60,a,37,b),unit_del(a,58),unit_del(b,56),unit_del(d,26)]. given #33 (F,wt=4): 65 -increases(cardinality_at_time(first_movers,c2)). [resolve(60,a,36,b),unit_del(a,58),unit_del(b,56),unit_del(d,25)]. given #34 (T,wt=5): 56 greater(cardinality_at_time(first_movers,c2),zero). [resolve(38,a,22,a)]. given #35 (T,wt=5): 57 greater(cardinality_at_time(efficient_producers,c2),zero). [resolve(39,a,22,a)]. given #36 (A,wt=10): 45 -constant(sum(A,B)) | constant(A) | increases(A) | increases(B). [xx_res(15,d)]. given #37 (F,wt=4): 66 -constant(cardinality_at_time(first_movers,c2)). [resolve(60,a,35,b),unit_del(a,58),unit_del(b,56),unit_del(d,24)]. given #38 (F,wt=6): 68 -constant(sum(cardinality_at_time(first_movers,c2),A)). [ur(44,b,66,a,c,65,a,d,64,a)]. given #39 (T,wt=8): 46 -constant(sum(A,A)) | constant(A) | increases(A). [factor(45,c,d)]. given #40 (T,wt=8): 48 -constant(sum(A,A)) | constant(A) | decreases(A). [factor(47,c,d)]. given #41 (A,wt=10): 47 -constant(sum(A,B)) | constant(A) | decreases(A) | decreases(B). [xx_res(16,d)]. given #42 (F,wt=6): 70 -constant(sum(A,cardinality_at_time(first_movers,c2))). [ur(21,b,xx,c,66,a,d,64,a,e,65,a)]. given #43 (F,wt=9): 71 sum(A,cardinality_at_time(first_movers,c2)) != number_of_organizations(c1,c2). [ur(21,a,23,a,c,66,a,d,64,a,e,65,a)]. given #44 (T,wt=9): 61 -decreases(cardinality_at_time(efficient_producers,c2)) | greater(zero,growth_rate(efficient_producers,c2)). [resolve(59,a,37,b),unit_del(a,58),unit_del(b,57)]. given #45 (T,wt=9): 62 -increases(cardinality_at_time(efficient_producers,c2)) | greater(growth_rate(efficient_producers,c2),zero). [resolve(59,a,36,b),unit_del(a,58),unit_del(b,57)]. given #46 (A,wt=10): 49 -constant(sum(A,B)) | constant(A) | decreases(B) | increases(B). [xx_res(17,c)]. given #47 (F,wt=9): 72 sum(cardinality_at_time(first_movers,c2),A) != number_of_organizations(c1,c2). [ur(14,a,23,a,b,66,a,c,65,a,d,64,a)]. ============================== PROOF ================================= % Proof 1 at 0.01 (+ 0.00) seconds. % Length of proof is 30. % Level of proof is 6. % Maximum clause weight is 21. % Given clauses 47. 1 environment(c1). [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]. 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]. 31 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)]. 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)]. 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)]. 56 greater(cardinality_at_time(first_movers,c2),zero). [resolve(38,a,22,a)]. 58 in_environment(c1,c2). [resolve(40,a,22,a)]. 60 subpopulation(first_movers,c1,c2). [resolve(58,a,33,a)]. 64 -decreases(cardinality_at_time(first_movers,c2)). [resolve(60,a,37,b),unit_del(a,58),unit_del(b,56),unit_del(d,26)]. 65 -increases(cardinality_at_time(first_movers,c2)). [resolve(60,a,36,b),unit_del(a,58),unit_del(b,56),unit_del(d,25)]. 66 -constant(cardinality_at_time(first_movers,c2)). [resolve(60,a,35,b),unit_del(a,58),unit_del(b,56),unit_del(d,24)]. 72 sum(cardinality_at_time(first_movers,c2),A) != number_of_organizations(c1,c2). [ur(14,a,23,a,b,66,a,c,65,a,d,64,a)]. 73 $F. [ur(32,b,60,a,c,72,a(flip)),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=47. Generated=100. Kept=56. proofs=1. Usable=47. Sos=8. Demods=0. Limbo=0, Disabled=39. Hints=0. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=43. Back_subsumed=1. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=0. Demod_rewrites=0. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=30. Nonunit_bsub_feature_tests=117. 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 3761 exit (max_proofs) Wed Nov 22 11:23:39 2006 ============================== 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)))))). Child search process 3762 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: Relation symbol precedence: lex([ constant, decreases, increases, greater, in_environment, subpopulation, subpopulations, =, environment ]). Function symbol precedence: lex([ 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(paramodulation) -> set(back_demod). % set(binary_resolution). % (non-Horn) % set(neg_ur_resolution). % (non-Horn, less than 100 clauses) Auto_process settings: % set(factor). % (non-Horn) % set(back_unit_deletion). % (non-Horn) % set(back_unit_deletion) -> set(unit_deletion). ============================== 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 (F,wt=3): 58 in_environment(c1,c2). [resolve(40,a,22,a)]. given #29 (T,wt=4): 59 subpopulation(efficient_producers,c1,c2). [resolve(58,a,34,a)]. given #30 (T,wt=4): 60 subpopulation(first_movers,c1,c2). [resolve(58,a,33,a)]. given #31 (A,wt=10): 44 -constant(sum(A,B)) | constant(A) | increases(A) | decreases(A). [xx_res(14,e)]. given #32 (F,wt=4): 61 -decreases(cardinality_at_time(efficient_producers,c2)). [resolve(59,a,37,b),unit_del(a,58),unit_del(b,57),unit_del(d,25)]. given #33 (F,wt=4): 62 -increases(cardinality_at_time(efficient_producers,c2)). [resolve(59,a,36,b),unit_del(a,58),unit_del(b,57),unit_del(d,26)]. given #34 (T,wt=5): 56 greater(cardinality_at_time(first_movers,c2),zero). [resolve(38,a,22,a)]. given #35 (T,wt=5): 57 greater(cardinality_at_time(efficient_producers,c2),zero). [resolve(39,a,22,a)]. given #36 (A,wt=10): 45 -constant(sum(A,B)) | constant(A) | increases(A) | increases(B). [xx_res(15,d)]. given #37 (F,wt=4): 66 -constant(cardinality_at_time(first_movers,c2)). [resolve(60,a,35,b),unit_del(a,58),unit_del(b,56),unit_del(d,24)]. given #38 (F,wt=8): 67 -constant(sum(cardinality_at_time(efficient_producers,c2),cardinality_at_time(first_movers,c2))). [ur(18,b,62,a,c,61,a,d,xx,e,66,a)]. given #39 (T,wt=8): 46 -constant(sum(A,A)) | constant(A) | increases(A). [factor(45,c,d)]. given #40 (T,wt=8): 48 -constant(sum(A,A)) | constant(A) | decreases(A). [factor(47,c,d)]. given #41 (A,wt=10): 47 -constant(sum(A,B)) | constant(A) | decreases(A) | decreases(B). [xx_res(16,d)]. given #42 (F,wt=8): 69 -constant(sum(cardinality_at_time(first_movers,c2),cardinality_at_time(efficient_producers,c2))). [ur(17,b,66,a,c,xx,d,61,a,e,62,a)]. given #43 (F,wt=11): 68 number_of_organizations(c1,c2) != sum(cardinality_at_time(efficient_producers,c2),cardinality_at_time(first_movers,c2)). [ur(18,a,23,a,b,62,a,c,61,a,e,66,a),flip(a)]. given #44 (T,wt=9): 63 -constant(cardinality_at_time(efficient_producers,c2)) | growth_rate(efficient_producers,c2) = zero. [resolve(59,a,35,b),unit_del(a,58),unit_del(b,57)]. given #45 (T,wt=9): 64 -decreases(cardinality_at_time(first_movers,c2)) | greater(zero,growth_rate(first_movers,c2)). [resolve(60,a,37,b),unit_del(a,58),unit_del(b,56)]. given #46 (A,wt=10): 49 -constant(sum(A,B)) | constant(A) | decreases(B) | increases(B). [xx_res(17,c)]. given #47 (F,wt=11): 70 number_of_organizations(c1,c2) != sum(cardinality_at_time(first_movers,c2),cardinality_at_time(efficient_producers,c2)). [ur(17,a,23,a,b,66,a,d,61,a,e,62,a),flip(a)]. ============================== PROOF ================================= % Proof 1 at 0.00 (+ 0.00) seconds. % Length of proof is 36. % Level of proof is 6. % Maximum clause weight is 21. % Given clauses 47. 1 environment(c1). [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]. 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]. 31 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)]. 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)]. 56 greater(cardinality_at_time(first_movers,c2),zero). [resolve(38,a,22,a)]. 57 greater(cardinality_at_time(efficient_producers,c2),zero). [resolve(39,a,22,a)]. 58 in_environment(c1,c2). [resolve(40,a,22,a)]. 59 subpopulation(efficient_producers,c1,c2). [resolve(58,a,34,a)]. 60 subpopulation(first_movers,c1,c2). [resolve(58,a,33,a)]. 61 -decreases(cardinality_at_time(efficient_producers,c2)). [resolve(59,a,37,b),unit_del(a,58),unit_del(b,57),unit_del(d,25)]. 62 -increases(cardinality_at_time(efficient_producers,c2)). [resolve(59,a,36,b),unit_del(a,58),unit_del(b,57),unit_del(d,26)]. 66 -constant(cardinality_at_time(first_movers,c2)). [resolve(60,a,35,b),unit_del(a,58),unit_del(b,56),unit_del(d,24)]. 70 number_of_organizations(c1,c2) != sum(cardinality_at_time(first_movers,c2),cardinality_at_time(efficient_producers,c2)). [ur(17,a,23,a,b,66,a,d,61,a,e,62,a),flip(a)]. 79 $F. [ur(32,b,60,a,c,70,a),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=47. Generated=79. Kept=62. proofs=1. Usable=47. Sos=15. Demods=0. Limbo=0, Disabled=38. Hints=0. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=16. Back_subsumed=0. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=0. Demod_rewrites=0. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=30. Nonunit_bsub_feature_tests=117. 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 3762 exit (max_proofs) Wed Nov 22 11:23:39 2006 ============================== 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))))))). Child search process 3763 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: Relation symbol precedence: lex([ constant, decreases, increases, greater, in_environment, subpopulation, subpopulations, =, environment ]). Function symbol precedence: lex([ 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(paramodulation) -> set(back_demod). % set(binary_resolution). % (non-Horn) % set(neg_ur_resolution). % (non-Horn, less than 100 clauses) Auto_process settings: % set(factor). % (non-Horn) % set(back_unit_deletion). % (non-Horn) % set(back_unit_deletion) -> set(unit_deletion). ============================== 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 (F,wt=3): 58 in_environment(c1,c2). [resolve(40,a,22,a)]. given #29 (T,wt=4): 59 subpopulation(efficient_producers,c1,c2). [resolve(58,a,34,a)]. given #30 (T,wt=4): 60 subpopulation(first_movers,c1,c2). [resolve(58,a,33,a)]. given #31 (A,wt=10): 44 -constant(sum(A,B)) | constant(A) | increases(A) | decreases(A). [xx_res(14,e)]. given #32 (F,wt=4): 61 -decreases(cardinality_at_time(efficient_producers,c2)). [resolve(59,a,37,b),unit_del(a,58),unit_del(b,57),unit_del(d,25)]. given #33 (F,wt=4): 64 -decreases(cardinality_at_time(first_movers,c2)). [resolve(60,a,37,b),unit_del(a,58),unit_del(b,56),unit_del(d,26)]. given #34 (T,wt=5): 56 greater(cardinality_at_time(first_movers,c2),zero). [resolve(38,a,22,a)]. given #35 (T,wt=5): 57 greater(cardinality_at_time(efficient_producers,c2),zero). [resolve(39,a,22,a)]. given #36 (A,wt=10): 45 -constant(sum(A,B)) | constant(A) | increases(A) | increases(B). [xx_res(15,d)]. given #37 (F,wt=4): 66 -constant(cardinality_at_time(first_movers,c2)). [resolve(60,a,35,b),unit_del(a,58),unit_del(b,56),unit_del(d,24)]. given #38 (F,wt=8): 67 -constant(sum(cardinality_at_time(first_movers,c2),cardinality_at_time(first_movers,c2))). [ur(43,b,66,a,c,64,a,d,xx)]. given #39 (T,wt=8): 46 -constant(sum(A,A)) | constant(A) | increases(A). [factor(45,c,d)]. given #40 (T,wt=8): 48 -constant(sum(A,A)) | constant(A) | decreases(A). [factor(47,c,d)]. given #41 (A,wt=10): 47 -constant(sum(A,B)) | constant(A) | decreases(A) | decreases(B). [xx_res(16,d)]. given #42 (F,wt=8): 69 -constant(sum(cardinality_at_time(efficient_producers,c2),cardinality_at_time(first_movers,c2))). [ur(20,b,61,a,c,xx,d,66,a,e,64,a)]. given #43 (F,wt=8): 71 -constant(sum(cardinality_at_time(first_movers,c2),cardinality_at_time(efficient_producers,c2))). [ur(16,b,66,a,c,64,a,d,xx,e,61,a)]. given #44 (T,wt=9): 62 -increases(cardinality_at_time(efficient_producers,c2)) | greater(growth_rate(efficient_producers,c2),zero). [resolve(59,a,36,b),unit_del(a,58),unit_del(b,57)]. given #45 (T,wt=9): 63 -constant(cardinality_at_time(efficient_producers,c2)) | growth_rate(efficient_producers,c2) = zero. [resolve(59,a,35,b),unit_del(a,58),unit_del(b,57)]. given #46 (A,wt=10): 49 -constant(sum(A,B)) | constant(A) | decreases(B) | increases(B). [xx_res(17,c)]. given #47 (F,wt=11): 68 number_of_organizations(c1,c2) != sum(cardinality_at_time(first_movers,c2),cardinality_at_time(first_movers,c2)). [ur(43,a,23,a,b,66,a,c,64,a),flip(a)]. given #48 (F,wt=11): 70 number_of_organizations(c1,c2) != sum(cardinality_at_time(efficient_producers,c2),cardinality_at_time(first_movers,c2)). [ur(20,a,23,a,b,61,a,d,66,a,e,64,a),flip(a)]. given #49 (T,wt=9): 65 -increases(cardinality_at_time(first_movers,c2)) | greater(growth_rate(first_movers,c2),zero). [resolve(60,a,36,b),unit_del(a,58),unit_del(b,56)]. given #50 (T,wt=10): 50 -constant(sum(A,B)) | increases(A) | decreases(A) | constant(B). [xx_res(18,d)]. given #51 (A,wt=10): 51 -constant(sum(A,B)) | increases(A) | constant(B) | increases(B). [xx_res(19,c)]. given #52 (F,wt=11): 72 number_of_organizations(c1,c2) != sum(cardinality_at_time(first_movers,c2),cardinality_at_time(efficient_producers,c2)). [ur(16,a,23,a,b,66,a,c,64,a,e,61,a),flip(a)]. ============================== PROOF ================================= % Proof 1 at 0.01 (+ 0.00) seconds. % Length of proof is 34. % Level of proof is 6. % Maximum clause weight is 21. % Given clauses 52. 1 environment(c1). [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]. 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]. 31 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)]. 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)]. 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)]. 56 greater(cardinality_at_time(first_movers,c2),zero). [resolve(38,a,22,a)]. 57 greater(cardinality_at_time(efficient_producers,c2),zero). [resolve(39,a,22,a)]. 58 in_environment(c1,c2). [resolve(40,a,22,a)]. 59 subpopulation(efficient_producers,c1,c2). [resolve(58,a,34,a)]. 60 subpopulation(first_movers,c1,c2). [resolve(58,a,33,a)]. 61 -decreases(cardinality_at_time(efficient_producers,c2)). [resolve(59,a,37,b),unit_del(a,58),unit_del(b,57),unit_del(d,25)]. 64 -decreases(cardinality_at_time(first_movers,c2)). [resolve(60,a,37,b),unit_del(a,58),unit_del(b,56),unit_del(d,26)]. 66 -constant(cardinality_at_time(first_movers,c2)). [resolve(60,a,35,b),unit_del(a,58),unit_del(b,56),unit_del(d,24)]. 72 number_of_organizations(c1,c2) != sum(cardinality_at_time(first_movers,c2),cardinality_at_time(efficient_producers,c2)). [ur(16,a,23,a,b,66,a,c,64,a,e,61,a),flip(a)]. 73 $F. [ur(32,b,60,a,c,72,a),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=52. Generated=77. Kept=56. proofs=1. Usable=52. Sos=4. Demods=0. Limbo=0, Disabled=38. Hints=0. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=20. Back_subsumed=0. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=0. Demod_rewrites=0. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=30. Nonunit_bsub_feature_tests=117. 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 3763 exit (max_proofs) Wed Nov 22 11:23:39 2006 ============================== 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)))))). Child search process 3764 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: Relation symbol precedence: lex([ constant, decreases, increases, greater, in_environment, subpopulation, subpopulations, =, environment ]). Function symbol precedence: lex([ 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(paramodulation) -> set(back_demod). % set(binary_resolution). % (non-Horn) % set(neg_ur_resolution). % (non-Horn, less than 100 clauses) Auto_process settings: % set(factor). % (non-Horn) % set(back_unit_deletion). % (non-Horn) % set(back_unit_deletion) -> set(unit_deletion). ============================== 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 (F,wt=3): 58 in_environment(c1,c2). [resolve(40,a,22,a)]. given #29 (T,wt=4): 59 subpopulation(efficient_producers,c1,c2). [resolve(58,a,34,a)]. given #30 (T,wt=4): 60 subpopulation(first_movers,c1,c2). [resolve(58,a,33,a)]. given #31 (A,wt=10): 44 -constant(sum(A,B)) | constant(A) | increases(A) | decreases(A). [xx_res(14,e)]. given #32 (F,wt=4): 62 -increases(cardinality_at_time(efficient_producers,c2)). [resolve(59,a,36,b),unit_del(a,58),unit_del(b,57),unit_del(d,26)]. given #33 (F,wt=4): 63 -constant(cardinality_at_time(efficient_producers,c2)). [resolve(59,a,35,b),unit_del(a,58),unit_del(b,57),unit_del(d,24)]. given #34 (T,wt=5): 56 greater(cardinality_at_time(first_movers,c2),zero). [resolve(38,a,22,a)]. given #35 (T,wt=5): 57 greater(cardinality_at_time(efficient_producers,c2),zero). [resolve(39,a,22,a)]. given #36 (A,wt=10): 45 -constant(sum(A,B)) | constant(A) | increases(A) | increases(B). [xx_res(15,d)]. given #37 (F,wt=4): 65 -increases(cardinality_at_time(first_movers,c2)). [resolve(60,a,36,b),unit_del(a,58),unit_del(b,56),unit_del(d,25)]. given #38 (F,wt=8): 67 -constant(sum(cardinality_at_time(efficient_producers,c2),cardinality_at_time(efficient_producers,c2))). [ur(42,b,63,a,c,62,a,d,xx)]. given #39 (T,wt=8): 46 -constant(sum(A,A)) | constant(A) | increases(A). [factor(45,c,d)]. given #40 (T,wt=8): 48 -constant(sum(A,A)) | constant(A) | decreases(A). [factor(47,c,d)]. given #41 (A,wt=10): 47 -constant(sum(A,B)) | constant(A) | decreases(A) | decreases(B). [xx_res(16,d)]. given #42 (F,wt=8): 69 -constant(sum(cardinality_at_time(efficient_producers,c2),cardinality_at_time(first_movers,c2))). [ur(45,b,63,a,c,62,a,d,65,a)]. given #43 (F,wt=8): 70 -constant(sum(cardinality_at_time(first_movers,c2),cardinality_at_time(efficient_producers,c2))). [ur(19,b,65,a,c,xx,d,63,a,e,62,a)]. given #44 (T,wt=9): 61 -decreases(cardinality_at_time(efficient_producers,c2)) | greater(zero,growth_rate(efficient_producers,c2)). [resolve(59,a,37,b),unit_del(a,58),unit_del(b,57)]. given #45 (T,wt=9): 64 -decreases(cardinality_at_time(first_movers,c2)) | greater(zero,growth_rate(first_movers,c2)). [resolve(60,a,37,b),unit_del(a,58),unit_del(b,56)]. given #46 (A,wt=10): 49 -constant(sum(A,B)) | constant(A) | decreases(B) | increases(B). [xx_res(17,c)]. given #47 (F,wt=11): 68 number_of_organizations(c1,c2) != sum(cardinality_at_time(efficient_producers,c2),cardinality_at_time(efficient_producers,c2)). [ur(42,a,23,a,b,63,a,c,62,a),flip(a)]. given #48 (F,wt=11): 71 number_of_organizations(c1,c2) != sum(cardinality_at_time(first_movers,c2),cardinality_at_time(efficient_producers,c2)). [ur(19,a,23,a,b,65,a,d,63,a,e,62,a),flip(a)]. ============================== PROOF ================================= % Proof 1 at 0.00 (+ 0.00) seconds. % Length of proof is 34. % Level of proof is 6. % Maximum clause weight is 21. % Given clauses 48. 1 environment(c1). [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]. 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]. 31 first_movers