============================== FOF-Prover9 =========================== FOF-Prover9 (32) version November-2006, November 2006. Process 3769 was started by mccune on cleo.thornwood, Wed Nov 22 11:23:39 2006 The command was "/home/mccune/bin/fof-prover9 -f MGT063+1.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file MGT063+1.in set(prolog_style_variables). formulas(assumptions). (all X all Y (smaller_or_equal(X,Y) <-> smaller(X,Y) | X = Y)). (all X all Y (greater_or_equal(X,Y) <-> greater(X,Y) | X = Y)). (all X all Y (smaller(X,Y) <-> greater(Y,X))). (all X all Y (-(greater(X,Y) & greater(Y,X)))). (all X all Y all Z (greater(X,Y) & greater(Y,Z) -> greater(X,Z))). (all X all Y (smaller(X,Y) | X = Y | greater(X,Y))). (all X (has_endowment(X) <-> (all T (organization(X) & (smaller_or_equal(age(X,T),eta) -> has_immunity(X,T)) & (greater(age(X,T),eta) -> -has_immunity(X,T)))))). (all X all T (organization(X) & -has_endowment(X) -> -has_immunity(X,T))). (all X all T0 all T (dissimilar(X,T0,T) <-> organization(X) & -(is_aligned(X,T0) <-> is_aligned(X,T)))). (all X all T (organization(X) & age(X,T) = zero -> is_aligned(X,T))). (all X all T0 all T (organization(X) & age(X,T0) = zero -> (greater(age(X,T),sigma) <-> dissimilar(X,T0,T)))). (all X (robust_position(X) <-> (all T ((smaller_or_equal(age(X,T),tau) -> -positional_advantage(X,T)) & (greater(age(X,T),tau) -> positional_advantage(X,T)))))). (all X all T (organization(X) -> (has_immunity(X,T) -> hazard_of_mortality(X,T) = very_low) & (-has_immunity(X,T) -> (is_aligned(X,T) & positional_advantage(X,T) -> hazard_of_mortality(X,T) = low) & (-is_aligned(X,T) & positional_advantage(X,T) -> hazard_of_mortality(X,T) = mod1) & (is_aligned(X,T) & -positional_advantage(X,T) -> hazard_of_mortality(X,T) = mod2) & (-is_aligned(X,T) & -positional_advantage(X,T) -> hazard_of_mortality(X,T) = high)))). greater(high,mod1). greater(mod1,low). greater(low,very_low). greater(high,mod2). greater(mod2,low). greater(mod2,mod1). -(all X all T0 all T1 all T2 all T3 (organization(X) & robust_position(X) & -has_endowment(X) & age(X,T0) = zero & greater(sigma,zero) & greater(tau,zero) & smaller(sigma,tau) & smaller_or_equal(age(X,T1),sigma) & greater(age(X,T2),sigma) & smaller_or_equal(age(X,T2),tau) & greater(age(X,T3),tau) -> smaller(hazard_of_mortality(X,T3),hazard_of_mortality(X,T1)) & smaller(hazard_of_mortality(X,T1),hazard_of_mortality(X,T2)) & hazard_of_mortality(X,T1) = hazard_of_mortality(X,T0))). end_of_list. ============================== end of input ========================== % clear(auto_denials), because it is incompatiable with FOF reduction. Attempting problem reduction; original problem has = <263,113>. Problem reduction (0.00 sec) gives 3 independent subproblems: ( <393,72> <393,72> <393,72> ). Max nnf_size of subproblems is 393; max cnf_max is 72. ============================== FOF REDUCTION MULTISEARCH ============= Subproblem 1 of 3 (negated): ((all X (all Y (smaller_or_equal(X,Y) | - smaller(X,Y)))) & (all X (all Y (smaller_or_equal(X,Y) | - =(Y,X)))) & (all X (all Y (smaller(X,Y) | =(Y,X) | - smaller_or_equal(X,Y)))) & (all X (all Y (greater_or_equal(X,Y) | - greater(X,Y)))) & (all X (all Y (greater_or_equal(X,Y) | - =(Y,X)))) & (all X (all Y (greater(X,Y) | =(Y,X) | - greater_or_equal(X,Y)))) & (all X (all Y (smaller(X,Y) | - greater(Y,X)))) & (all X (all Y (greater(Y,X) | - smaller(X,Y)))) & (all X (all Y (- greater(X,Y) | - greater(Y,X)))) & (all X (all Y (- greater(X,Y) | (all Z (- greater(Y,Z) | greater(X,Z)))))) & (all X (all Y (smaller(X,Y) | =(Y,X) | greater(X,Y)))) & (all X (has_endowment(X) | - organization(X) | (exists T (smaller_or_equal(age(X,T),eta) & - has_immunity(X,T))) | (exists T (greater(age(X,T),eta) & has_immunity(X,T))))) & (all X (organization(X) | - has_endowment(X))) & (all X ((all T (- smaller_or_equal(age(X,T),eta) | has_immunity(X,T))) | - has_endowment(X))) & (all X ((all T (- smaller_or_equal(age(X,T),eta) | has_immunity(X,T))) | - organization(X) | (exists T (smaller_or_equal(age(X,T),eta) & - has_immunity(X,T))) | (exists T (greater(age(X,T),eta) & has_immunity(X,T))))) & (all X ((all T (- greater(age(X,T),eta) | - has_immunity(X,T))) | - has_endowment(X))) & (all X ((all T (- greater(age(X,T),eta) | - has_immunity(X,T))) | - organization(X) | (exists T (smaller_or_equal(age(X,T),eta) & - has_immunity(X,T))) | (exists T (greater(age(X,T),eta) & has_immunity(X,T))))) & (all X (- organization(X) | has_endowment(X) | (all T (- has_immunity(X,T))))) & (all X (- organization(X) | (all T0 (is_aligned(X,T0) | (all T (dissimilar(X,T0,T) | - is_aligned(X,T))))))) & (all X (- organization(X) | (all T0 (- is_aligned(X,T0) | (all T (dissimilar(X,T0,T) | is_aligned(X,T))))))) & (all X (organization(X) | (all T0 ((all T (- dissimilar(X,T0,T))))))) & (all X (all T0 (is_aligned(X,T0) | (all T (is_aligned(X,T) | - dissimilar(X,T0,T)))))) & (all X (all T0 (- is_aligned(X,T0) | (all T (- is_aligned(X,T) | - dissimilar(X,T0,T)))))) & (all X (- organization(X) | (all T (- =(age(X,T),zero) | is_aligned(X,T))))) & (all X (- organization(X) | (all T0 (- =(age(X,T0),zero) | (all T (greater(age(X,T),sigma) | - dissimilar(X,T0,T))))))) & (all X (- organization(X) | (all T0 (- =(age(X,T0),zero) | (all T (dissimilar(X,T0,T) | - greater(age(X,T),sigma))))))) & (all X (robust_position(X) | (exists T (smaller_or_equal(age(X,T),tau) & positional_advantage(X,T))) | (exists T (greater(age(X,T),tau) & - positional_advantage(X,T))))) & (all X ((all T (- smaller_or_equal(age(X,T),tau) | - positional_advantage(X,T))) | - robust_position(X))) & (all X ((all T (- smaller_or_equal(age(X,T),tau) | - positional_advantage(X,T))) | (exists T (smaller_or_equal(age(X,T),tau) & positional_advantage(X,T))) | (exists T (greater(age(X,T),tau) & - positional_advantage(X,T))))) & (all X ((all T (- greater(age(X,T),tau) | positional_advantage(X,T))) | - robust_position(X))) & (all X ((all T (- greater(age(X,T),tau) | positional_advantage(X,T))) | (exists T (smaller_or_equal(age(X,T),tau) & positional_advantage(X,T))) | (exists T (greater(age(X,T),tau) & - positional_advantage(X,T))))) & (all X (- organization(X) | (all T (- has_immunity(X,T) | =(hazard_of_mortality(X,T),very_low))))) & (all X (- organization(X) | (all T (has_immunity(X,T) | - is_aligned(X,T) | - positional_advantage(X,T) | =(hazard_of_mortality(X,T),low))))) & (all X (- organization(X) | (all T (has_immunity(X,T) | is_aligned(X,T) | - positional_advantage(X,T) | =(hazard_of_mortality(X,T),mod1))))) & (all X (- organization(X) | (all T (has_immunity(X,T) | - is_aligned(X,T) | positional_advantage(X,T) | =(hazard_of_mortality(X,T),mod2))))) & (all X (- organization(X) | (all T (has_immunity(X,T) | is_aligned(X,T) | positional_advantage(X,T) | =(hazard_of_mortality(X,T),high))))) & greater(high,mod1) & greater(mod1,low) & greater(low,very_low) & greater(high,mod2) & greater(mod2,low) & greater(mod2,mod1) & greater(sigma,zero) & greater(tau,zero) & smaller(sigma,tau) & (exists X (organization(X) & robust_position(X) & - has_endowment(X) & (exists T2 (greater(age(X,T2),sigma) & smaller_or_equal(age(X,T2),tau))) & (exists T1 (smaller_or_equal(age(X,T1),sigma) & (exists T3 (greater(age(X,T3),tau) & - smaller(hazard_of_mortality(X,T3),hazard_of_mortality(X,T1)))))) & (exists T0 (=(age(X,T0),zero)))))). Child search process 3770 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). smaller_or_equal(A,B) | -smaller(A,B). [assumption]. smaller_or_equal(A,B) | B != A. [assumption]. smaller(A,B) | B = A | -smaller_or_equal(A,B). [assumption]. greater_or_equal(A,B) | -greater(A,B). [assumption]. greater_or_equal(A,B) | B != A. [assumption]. greater(A,B) | B = A | -greater_or_equal(A,B). [assumption]. smaller(A,B) | -greater(B,A). [assumption]. greater(A,B) | -smaller(B,A). [assumption]. -greater(A,B) | -greater(B,A). [assumption]. -greater(A,B) | -greater(B,C) | greater(A,C). [assumption]. smaller(A,B) | B = A | greater(A,B). [assumption]. has_endowment(A) | -organization(A) | smaller_or_equal(age(A,f1(A)),eta) | greater(age(A,f2(A)),eta). [assumption]. has_endowment(A) | -organization(A) | smaller_or_equal(age(A,f1(A)),eta) | has_immunity(A,f2(A)). [assumption]. has_endowment(A) | -organization(A) | -has_immunity(A,f1(A)) | greater(age(A,f2(A)),eta). [assumption]. has_endowment(A) | -organization(A) | -has_immunity(A,f1(A)) | has_immunity(A,f2(A)). [assumption]. organization(A) | -has_endowment(A). [assumption]. -smaller_or_equal(age(A,B),eta) | has_immunity(A,B) | -has_endowment(A). [assumption]. -smaller_or_equal(age(A,B),eta) | has_immunity(A,B) | -organization(A) | smaller_or_equal(age(A,f3(A)),eta) | greater(age(A,f4(A)),eta). [assumption]. -smaller_or_equal(age(A,B),eta) | has_immunity(A,B) | -organization(A) | smaller_or_equal(age(A,f3(A)),eta) | has_immunity(A,f4(A)). [assumption]. -smaller_or_equal(age(A,B),eta) | has_immunity(A,B) | -organization(A) | -has_immunity(A,f3(A)) | greater(age(A,f4(A)),eta). [assumption]. -smaller_or_equal(age(A,B),eta) | has_immunity(A,B) | -organization(A) | -has_immunity(A,f3(A)) | has_immunity(A,f4(A)). [assumption]. -greater(age(A,B),eta) | -has_immunity(A,B) | -has_endowment(A). [assumption]. -greater(age(A,B),eta) | -has_immunity(A,B) | -organization(A) | smaller_or_equal(age(A,f5(A)),eta) | greater(age(A,f6(A)),eta). [assumption]. -greater(age(A,B),eta) | -has_immunity(A,B) | -organization(A) | smaller_or_equal(age(A,f5(A)),eta) | has_immunity(A,f6(A)). [assumption]. -greater(age(A,B),eta) | -has_immunity(A,B) | -organization(A) | -has_immunity(A,f5(A)) | greater(age(A,f6(A)),eta). [assumption]. -greater(age(A,B),eta) | -has_immunity(A,B) | -organization(A) | -has_immunity(A,f5(A)) | has_immunity(A,f6(A)). [assumption]. -organization(A) | has_endowment(A) | -has_immunity(A,B). [assumption]. -organization(A) | is_aligned(A,B) | dissimilar(A,B,C) | -is_aligned(A,C). [assumption]. -organization(A) | -is_aligned(A,B) | dissimilar(A,B,C) | is_aligned(A,C). [assumption]. organization(A) | -dissimilar(A,B,C). [assumption]. is_aligned(A,B) | is_aligned(A,C) | -dissimilar(A,B,C). [assumption]. -is_aligned(A,B) | -is_aligned(A,C) | -dissimilar(A,B,C). [assumption]. -organization(A) | age(A,B) != zero | is_aligned(A,B). [assumption]. -organization(A) | age(A,B) != zero | greater(age(A,C),sigma) | -dissimilar(A,B,C). [assumption]. -organization(A) | age(A,B) != zero | dissimilar(A,B,C) | -greater(age(A,C),sigma). [assumption]. robust_position(A) | smaller_or_equal(age(A,f7(A)),tau) | greater(age(A,f8(A)),tau). [assumption]. robust_position(A) | smaller_or_equal(age(A,f7(A)),tau) | -positional_advantage(A,f8(A)). [assumption]. robust_position(A) | positional_advantage(A,f7(A)) | greater(age(A,f8(A)),tau). [assumption]. robust_position(A) | positional_advantage(A,f7(A)) | -positional_advantage(A,f8(A)). [assumption]. -smaller_or_equal(age(A,B),tau) | -positional_advantage(A,B) | -robust_position(A). [assumption]. -smaller_or_equal(age(A,B),tau) | -positional_advantage(A,B) | smaller_or_equal(age(A,f9(A)),tau) | greater(age(A,f10(A)),tau). [assumption]. -smaller_or_equal(age(A,B),tau) | -positional_advantage(A,B) | smaller_or_equal(age(A,f9(A)),tau) | -positional_advantage(A,f10(A)). [assumption]. -smaller_or_equal(age(A,B),tau) | -positional_advantage(A,B) | positional_advantage(A,f9(A)) | greater(age(A,f10(A)),tau). [assumption]. -smaller_or_equal(age(A,B),tau) | -positional_advantage(A,B) | positional_advantage(A,f9(A)) | -positional_advantage(A,f10(A)). [assumption]. -greater(age(A,B),tau) | positional_advantage(A,B) | -robust_position(A). [assumption]. -greater(age(A,B),tau) | positional_advantage(A,B) | smaller_or_equal(age(A,f11(A)),tau) | greater(age(A,f12(A)),tau). [assumption]. -greater(age(A,B),tau) | positional_advantage(A,B) | smaller_or_equal(age(A,f11(A)),tau) | -positional_advantage(A,f12(A)). [assumption]. -greater(age(A,B),tau) | positional_advantage(A,B) | positional_advantage(A,f11(A)) | greater(age(A,f12(A)),tau). [assumption]. -greater(age(A,B),tau) | positional_advantage(A,B) | positional_advantage(A,f11(A)) | -positional_advantage(A,f12(A)). [assumption]. -organization(A) | -has_immunity(A,B) | hazard_of_mortality(A,B) = very_low. [assumption]. -organization(A) | has_immunity(A,B) | -is_aligned(A,B) | -positional_advantage(A,B) | hazard_of_mortality(A,B) = low. [assumption]. -organization(A) | has_immunity(A,B) | is_aligned(A,B) | -positional_advantage(A,B) | hazard_of_mortality(A,B) = mod1. [assumption]. -organization(A) | has_immunity(A,B) | -is_aligned(A,B) | positional_advantage(A,B) | hazard_of_mortality(A,B) = mod2. [assumption]. -organization(A) | has_immunity(A,B) | is_aligned(A,B) | positional_advantage(A,B) | hazard_of_mortality(A,B) = high. [assumption]. greater(high,mod1). [assumption]. greater(mod1,low). [assumption]. greater(low,very_low). [assumption]. greater(high,mod2). [assumption]. greater(mod2,low). [assumption]. greater(mod2,mod1). [assumption]. greater(sigma,zero). [assumption]. greater(tau,zero). [assumption]. smaller(sigma,tau). [assumption]. organization(c1). [assumption]. robust_position(c1). [assumption]. -has_endowment(c1). [assumption]. greater(age(c1,c2),sigma). [assumption]. smaller_or_equal(age(c1,c2),tau). [assumption]. smaller_or_equal(age(c1,c3),sigma). [assumption]. greater(age(c1,c4),tau). [assumption]. -smaller(hazard_of_mortality(c1,c4),hazard_of_mortality(c1,c3)). [assumption]. age(c1,c5) = zero. [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= Eliminating greater_or_equal/2 1 greater(A,B) | B = A | -greater_or_equal(A,B). [assumption]. 2 greater_or_equal(A,B) | -greater(A,B). [assumption]. 3 greater_or_equal(A,B) | B != A. [assumption]. Eliminating organization/1 4 organization(A) | -has_endowment(A). [assumption]. 5 has_endowment(A) | -organization(A) | smaller_or_equal(age(A,f1(A)),eta) | greater(age(A,f2(A)),eta). [assumption]. 6 has_endowment(A) | -organization(A) | smaller_or_equal(age(A,f1(A)),eta) | has_immunity(A,f2(A)). [assumption]. 7 has_endowment(A) | -organization(A) | -has_immunity(A,f1(A)) | greater(age(A,f2(A)),eta). [assumption]. 8 has_endowment(A) | -organization(A) | -has_immunity(A,f1(A)) | has_immunity(A,f2(A)). [assumption]. 9 -smaller_or_equal(age(A,B),eta) | has_immunity(A,B) | -organization(A) | smaller_or_equal(age(A,f3(A)),eta) | greater(age(A,f4(A)),eta). [assumption]. Derived: -smaller_or_equal(age(A,B),eta) | has_immunity(A,B) | smaller_or_equal(age(A,f3(A)),eta) | greater(age(A,f4(A)),eta) | -has_endowment(A). [resolve(9,c,4,a)]. 10 -smaller_or_equal(age(A,B),eta) | has_immunity(A,B) | -organization(A) | smaller_or_equal(age(A,f3(A)),eta) | has_immunity(A,f4(A)). [assumption]. Derived: -smaller_or_equal(age(A,B),eta) | has_immunity(A,B) | smaller_or_equal(age(A,f3(A)),eta) | has_immunity(A,f4(A)) | -has_endowment(A). [resolve(10,c,4,a)]. 11 -smaller_or_equal(age(A,B),eta) | has_immunity(A,B) | -organization(A) | -has_immunity(A,f3(A)) | greater(age(A,f4(A)),eta). [assumption]. Derived: -smaller_or_equal(age(A,B),eta) | has_immunity(A,B) | -has_immunity(A,f3(A)) | greater(age(A,f4(A)),eta) | -has_endowment(A). [resolve(11,c,4,a)]. 12 -smaller_or_equal(age(A,B),eta) | has_immunity(A,B) | -organization(A) | -has_immunity(A,f3(A)) | has_immunity(A,f4(A)). [assumption]. Derived: -smaller_or_equal(age(A,B),eta) | has_immunity(A,B) | -has_immunity(A,f3(A)) | has_immunity(A,f4(A)) | -has_endowment(A). [resolve(12,c,4,a)]. 13 -greater(age(A,B),eta) | -has_immunity(A,B) | -organization(A) | smaller_or_equal(age(A,f5(A)),eta) | greater(age(A,f6(A)),eta). [assumption]. Derived: -greater(age(A,B),eta) | -has_immunity(A,B) | smaller_or_equal(age(A,f5(A)),eta) | greater(age(A,f6(A)),eta) | -has_endowment(A). [resolve(13,c,4,a)]. 14 -greater(age(A,B),eta) | -has_immunity(A,B) | -organization(A) | smaller_or_equal(age(A,f5(A)),eta) | has_immunity(A,f6(A)). [assumption]. Derived: -greater(age(A,B),eta) | -has_immunity(A,B) | smaller_or_equal(age(A,f5(A)),eta) | has_immunity(A,f6(A)) | -has_endowment(A). [resolve(14,c,4,a)]. 15 -greater(age(A,B),eta) | -has_immunity(A,B) | -organization(A) | -has_immunity(A,f5(A)) | greater(age(A,f6(A)),eta). [assumption]. Derived: -greater(age(A,B),eta) | -has_immunity(A,B) | -has_immunity(A,f5(A)) | greater(age(A,f6(A)),eta) | -has_endowment(A). [resolve(15,c,4,a)]. 16 -greater(age(A,B),eta) | -has_immunity(A,B) | -organization(A) | -has_immunity(A,f5(A)) | has_immunity(A,f6(A)). [assumption]. Derived: -greater(age(A,B),eta) | -has_immunity(A,B) | -has_immunity(A,f5(A)) | has_immunity(A,f6(A)) | -has_endowment(A). [resolve(16,c,4,a)]. 17 -organization(A) | has_endowment(A) | -has_immunity(A,B). [assumption]. 18 -organization(A) | is_aligned(A,B) | dissimilar(A,B,C) | -is_aligned(A,C). [assumption]. Derived: is_aligned(A,B) | dissimilar(A,B,C) | -is_aligned(A,C) | -has_endowment(A). [resolve(18,a,4,a)]. 19 -organization(A) | -is_aligned(A,B) | dissimilar(A,B,C) | is_aligned(A,C). [assumption]. Derived: -is_aligned(A,B) | dissimilar(A,B,C) | is_aligned(A,C) | -has_endowment(A). [resolve(19,a,4,a)]. 20 organization(A) | -dissimilar(A,B,C). [assumption]. Derived: -dissimilar(A,B,C) | has_endowment(A) | smaller_or_equal(age(A,f1(A)),eta) | greater(age(A,f2(A)),eta). [resolve(20,a,5,b)]. Derived: -dissimilar(A,B,C) | has_endowment(A) | smaller_or_equal(age(A,f1(A)),eta) | has_immunity(A,f2(A)). [resolve(20,a,6,b)]. Derived: -dissimilar(A,B,C) | has_endowment(A) | -has_immunity(A,f1(A)) | greater(age(A,f2(A)),eta). [resolve(20,a,7,b)]. Derived: -dissimilar(A,B,C) | has_endowment(A) | -has_immunity(A,f1(A)) | has_immunity(A,f2(A)). [resolve(20,a,8,b)]. Derived: -dissimilar(A,B,C) | -smaller_or_equal(age(A,D),eta) | has_immunity(A,D) | smaller_or_equal(age(A,f3(A)),eta) | greater(age(A,f4(A)),eta). [resolve(20,a,9,c)]. Derived: -dissimilar(A,B,C) | -smaller_or_equal(age(A,D),eta) | has_immunity(A,D) | smaller_or_equal(age(A,f3(A)),eta) | has_immunity(A,f4(A)). [resolve(20,a,10,c)]. Derived: -dissimilar(A,B,C) | -smaller_or_equal(age(A,D),eta) | has_immunity(A,D) | -has_immunity(A,f3(A)) | greater(age(A,f4(A)),eta). [resolve(20,a,11,c)]. Derived: -dissimilar(A,B,C) | -smaller_or_equal(age(A,D),eta) | has_immunity(A,D) | -has_immunity(A,f3(A)) | has_immunity(A,f4(A)). [resolve(20,a,12,c)]. Derived: -dissimilar(A,B,C) | -greater(age(A,D),eta) | -has_immunity(A,D) | smaller_or_equal(age(A,f5(A)),eta) | greater(age(A,f6(A)),eta). [resolve(20,a,13,c)]. Derived: -dissimilar(A,B,C) | -greater(age(A,D),eta) | -has_immunity(A,D) | smaller_or_equal(age(A,f5(A)),eta) | has_immunity(A,f6(A)). [resolve(20,a,14,c)]. Derived: -dissimilar(A,B,C) | -greater(age(A,D),eta) | -has_immunity(A,D) | -has_immunity(A,f5(A)) | greater(age(A,f6(A)),eta). [resolve(20,a,15,c)]. Derived: -dissimilar(A,B,C) | -greater(age(A,D),eta) | -has_immunity(A,D) | -has_immunity(A,f5(A)) | has_immunity(A,f6(A)). [resolve(20,a,16,c)]. Derived: -dissimilar(A,B,C) | has_endowment(A) | -has_immunity(A,D). [resolve(20,a,17,a)]. Derived: -dissimilar(A,B,C) | is_aligned(A,D) | dissimilar(A,D,E) | -is_aligned(A,E). [resolve(20,a,18,a)]. Derived: -dissimilar(A,B,C) | -is_aligned(A,D) | dissimilar(A,D,E) | is_aligned(A,E). [resolve(20,a,19,a)]. 21 -organization(A) | age(A,B) != zero | is_aligned(A,B). [assumption]. Derived: age(A,B) != zero | is_aligned(A,B) | -has_endowment(A). [resolve(21,a,4,a)]. Derived: age(A,B) != zero | is_aligned(A,B) | -dissimilar(A,C,D). [resolve(21,a,20,a)]. 22 -organization(A) | age(A,B) != zero | greater(age(A,C),sigma) | -dissimilar(A,B,C). [assumption]. Derived: age(A,B) != zero | greater(age(A,C),sigma) | -dissimilar(A,B,C) | -has_endowment(A). [resolve(22,a,4,a)]. Derived: age(A,B) != zero | greater(age(A,C),sigma) | -dissimilar(A,B,C) | -dissimilar(A,D,E). [resolve(22,a,20,a)]. 23 -organization(A) | age(A,B) != zero | dissimilar(A,B,C) | -greater(age(A,C),sigma). [assumption]. Derived: age(A,B) != zero | dissimilar(A,B,C) | -greater(age(A,C),sigma) | -has_endowment(A). [resolve(23,a,4,a)]. Derived: age(A,B) != zero | dissimilar(A,B,C) | -greater(age(A,C),sigma) | -dissimilar(A,D,E). [resolve(23,a,20,a)]. 24 -organization(A) | -has_immunity(A,B) | hazard_of_mortality(A,B) = very_low. [assumption]. Derived: -has_immunity(A,B) | hazard_of_mortality(A,B) = very_low | -has_endowment(A). [resolve(24,a,4,a)]. Derived: -has_immunity(A,B) | hazard_of_mortality(A,B) = very_low | -dissimilar(A,C,D). [resolve(24,a,20,a)]. 25 -organization(A) | has_immunity(A,B) | -is_aligned(A,B) | -positional_advantage(A,B) | hazard_of_mortality(A,B) = low. [assumption]. Derived: has_immunity(A,B) | -is_aligned(A,B) | -positional_advantage(A,B) | hazard_of_mortality(A,B) = low | -has_endowment(A). [resolve(25,a,4,a)]. Derived: has_immunity(A,B) | -is_aligned(A,B) | -positional_advantage(A,B) | hazard_of_mortality(A,B) = low | -dissimilar(A,C,D). [resolve(25,a,20,a)]. 26 -organization(A) | has_immunity(A,B) | is_aligned(A,B) | -positional_advantage(A,B) | hazard_of_mortality(A,B) = mod1. [assumption]. Derived: has_immunity(A,B) | is_aligned(A,B) | -positional_advantage(A,B) | hazard_of_mortality(A,B) = mod1 | -has_endowment(A). [resolve(26,a,4,a)]. Derived: has_immunity(A,B) | is_aligned(A,B) | -positional_advantage(A,B) | hazard_of_mortality(A,B) = mod1 | -dissimilar(A,C,D). [resolve(26,a,20,a)]. 27 -organization(A) | has_immunity(A,B) | -is_aligned(A,B) | positional_advantage(A,B) | hazard_of_mortality(A,B) = mod2. [assumption]. Derived: has_immunity(A,B) | -is_aligned(A,B) | positional_advantage(A,B) | hazard_of_mortality(A,B) = mod2 | -has_endowment(A). [resolve(27,a,4,a)]. Derived: has_immunity(A,B) | -is_aligned(A,B) | positional_advantage(A,B) | hazard_of_mortality(A,B) = mod2 | -dissimilar(A,C,D). [resolve(27,a,20,a)]. 28 -organization(A) | has_immunity(A,B) | is_aligned(A,B) | positional_advantage(A,B) | hazard_of_mortality(A,B) = high. [assumption]. Derived: has_immunity(A,B) | is_aligned(A,B) | positional_advantage(A,B) | hazard_of_mortality(A,B) = high | -has_endowment(A). [resolve(28,a,4,a)]. Derived: has_immunity(A,B) | is_aligned(A,B) | positional_advantage(A,B) | hazard_of_mortality(A,B) = high | -dissimilar(A,C,D). [resolve(28,a,20,a)]. 29 organization(c1). [assumption]. Derived: has_endowment(c1) | smaller_or_equal(age(c1,f1(c1)),eta) | greater(age(c1,f2(c1)),eta). [resolve(29,a,5,b)]. Derived: has_endowment(c1) | smaller_or_equal(age(c1,f1(c1)),eta) | has_immunity(c1,f2(c1)). [resolve(29,a,6,b)]. Derived: has_endowment(c1) | -has_immunity(c1,f1(c1)) | greater(age(c1,f2(c1)),eta). [resolve(29,a,7,b)]. Derived: has_endowment(c1) | -has_immunity(c1,f1(c1)) | has_immunity(c1,f2(c1)). [resolve(29,a,8,b)]. Derived: -smaller_or_equal(age(c1,A),eta) | has_immunity(c1,A) | smaller_or_equal(age(c1,f3(c1)),eta) | greater(age(c1,f4(c1)),eta). [resolve(29,a,9,c)]. Derived: -smaller_or_equal(age(c1,A),eta) | has_immunity(c1,A) | smaller_or_equal(age(c1,f3(c1)),eta) | has_immunity(c1,f4(c1)). [resolve(29,a,10,c)]. Derived: -smaller_or_equal(age(c1,A),eta) | has_immunity(c1,A) | -has_immunity(c1,f3(c1)) | greater(age(c1,f4(c1)),eta). [resolve(29,a,11,c)]. Derived: -smaller_or_equal(age(c1,A),eta) | has_immunity(c1,A) | -has_immunity(c1,f3(c1)) | has_immunity(c1,f4(c1)). [resolve(29,a,12,c)]. Derived: -greater(age(c1,A),eta) | -has_immunity(c1,A) | smaller_or_equal(age(c1,f5(c1)),eta) | greater(age(c1,f6(c1)),eta). [resolve(29,a,13,c)]. Derived: -greater(age(c1,A),eta) | -has_immunity(c1,A) | smaller_or_equal(age(c1,f5(c1)),eta) | has_immunity(c1,f6(c1)). [resolve(29,a,14,c)]. Derived: -greater(age(c1,A),eta) | -has_immunity(c1,A) | -has_immunity(c1,f5(c1)) | greater(age(c1,f6(c1)),eta). [resolve(29,a,15,c)]. Derived: -greater(age(c1,A),eta) | -has_immunity(c1,A) | -has_immunity(c1,f5(c1)) | has_immunity(c1,f6(c1)). [resolve(29,a,16,c)]. Derived: has_endowment(c1) | -has_immunity(c1,A). [resolve(29,a,17,a)]. Derived: is_aligned(c1,A) | dissimilar(c1,A,B) | -is_aligned(c1,B). [resolve(29,a,18,a)]. Derived: -is_aligned(c1,A) | dissimilar(c1,A,B) | is_aligned(c1,B). [resolve(29,a,19,a)]. Derived: age(c1,A) != zero | is_aligned(c1,A). [resolve(29,a,21,a)]. Derived: age(c1,A) != zero | dissimilar(c1,A,B) | -greater(age(c1,B),sigma). [resolve(29,a,23,a)]. Derived: -has_immunity(c1,A) | hazard_of_mortality(c1,A) = very_low. [resolve(29,a,24,a)]. Derived: has_immunity(c1,A) | -is_aligned(c1,A) | -positional_advantage(c1,A) | hazard_of_mortality(c1,A) = low. [resolve(29,a,25,a)]. Derived: has_immunity(c1,A) | is_aligned(c1,A) | -positional_advantage(c1,A) | hazard_of_mortality(c1,A) = mod1. [resolve(29,a,26,a)]. Derived: has_immunity(c1,A) | -is_aligned(c1,A) | positional_advantage(c1,A) | hazard_of_mortality(c1,A) = mod2. [resolve(29,a,27,a)]. Derived: has_immunity(c1,A) | is_aligned(c1,A) | positional_advantage(c1,A) | hazard_of_mortality(c1,A) = high. [resolve(29,a,28,a)]. Eliminating robust_position/1 30 -smaller_or_equal(age(A,B),tau) | -positional_advantage(A,B) | -robust_position(A). [assumption]. 31 robust_position(A) | smaller_or_equal(age(A,f7(A)),tau) | greater(age(A,f8(A)),tau). [assumption]. 32 robust_position(A) | smaller_or_equal(age(A,f7(A)),tau) | -positional_advantage(A,f8(A)). [assumption]. 33 robust_position(A) | positional_advantage(A,f7(A)) | greater(age(A,f8(A)),tau). [assumption]. 34 robust_position(A) | positional_advantage(A,f7(A)) | -positional_advantage(A,f8(A)). [assumption]. Derived: -smaller_or_equal(age(A,B),tau) | -positional_advantage(A,B) | smaller_or_equal(age(A,f7(A)),tau) | greater(age(A,f8(A)),tau). [resolve(30,c,31,a)]. Derived: -smaller_or_equal(age(A,B),tau) | -positional_advantage(A,B) | smaller_or_equal(age(A,f7(A)),tau) | -positional_advantage(A,f8(A)). [resolve(30,c,32,a)]. Derived: -smaller_or_equal(age(A,B),tau) | -positional_advantage(A,B) | positional_advantage(A,f7(A)) | greater(age(A,f8(A)),tau). [resolve(30,c,33,a)]. Derived: -smaller_or_equal(age(A,B),tau) | -positional_advantage(A,B) | positional_advantage(A,f7(A)) | -positional_advantage(A,f8(A)). [resolve(30,c,34,a)]. 35 -greater(age(A,B),tau) | positional_advantage(A,B) | -robust_position(A). [assumption]. Derived: -greater(age(A,B),tau) | positional_advantage(A,B) | smaller_or_equal(age(A,f7(A)),tau) | greater(age(A,f8(A)),tau). [resolve(35,c,31,a)]. Derived: -greater(age(A,B),tau) | positional_advantage(A,B) | smaller_or_equal(age(A,f7(A)),tau) | -positional_advantage(A,f8(A)). [resolve(35,c,32,a)]. Derived: -greater(age(A,B),tau) | positional_advantage(A,B) | positional_advantage(A,f7(A)) | greater(age(A,f8(A)),tau). [resolve(35,c,33,a)]. Derived: -greater(age(A,B),tau) | positional_advantage(A,B) | positional_advantage(A,f7(A)) | -positional_advantage(A,f8(A)). [resolve(35,c,34,a)]. 36 robust_position(c1). [assumption]. Derived: -smaller_or_equal(age(c1,A),tau) | -positional_advantage(c1,A). [resolve(36,a,30,c)]. Derived: -greater(age(c1,A),tau) | positional_advantage(c1,A). [resolve(36,a,35,c)]. ============================== end predicate elimination ============= Term ordering decisions: Relation symbol precedence: lex([ has_endowment, has_immunity, greater, smaller_or_equal, positional_advantage, is_aligned, smaller, dissimilar, =, robust_position, organization, greater_or_equal ]). Function symbol precedence: lex([ eta, tau, zero, sigma, low, mod1, mod2, high, very_low, c1, c2, c3, c4, c5, age, hazard_of_mortality, f1, f2, f3, f4, f5, f6, f7, f8, f9, f10, f11, f12 ]). 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). 37 smaller_or_equal(A,B) | -smaller(A,B). [assumption]. 38 smaller_or_equal(A,B) | B != A. [assumption]. 39 smaller(A,B) | B = A | -smaller_or_equal(A,B). [assumption]. 40 smaller(A,B) | -greater(B,A). [assumption]. 41 greater(A,B) | -smaller(B,A). [assumption]. 42 -greater(A,B) | -greater(B,A). [assumption]. 43 -greater(A,B) | -greater(B,C) | greater(A,C). [assumption]. 44 smaller(A,B) | B = A | greater(A,B). [assumption]. 45 -smaller_or_equal(age(A,B),eta) | has_immunity(A,B) | -has_endowment(A). [assumption]. 46 -greater(age(A,B),eta) | -has_immunity(A,B) | -has_endowment(A). [assumption]. 47 is_aligned(A,B) | is_aligned(A,C) | -dissimilar(A,B,C). [assumption]. 48 -is_aligned(A,B) | -is_aligned(A,C) | -dissimilar(A,B,C). [assumption]. 49 -smaller_or_equal(age(A,B),tau) | -positional_advantage(A,B) | smaller_or_equal(age(A,f9(A)),tau) | greater(age(A,f10(A)),tau). [assumption]. 50 -smaller_or_equal(age(A,B),tau) | -positional_advantage(A,B) | smaller_or_equal(age(A,f9(A)),tau) | -positional_advantage(A,f10(A)). [assumption]. 51 -smaller_or_equal(age(A,B),tau) | -positional_advantage(A,B) | positional_advantage(A,f9(A)) | greater(age(A,f10(A)),tau). [assumption]. 52 -smaller_or_equal(age(A,B),tau) | -positional_advantage(A,B) | positional_advantage(A,f9(A)) | -positional_advantage(A,f10(A)). [assumption]. 53 -greater(age(A,B),tau) | positional_advantage(A,B) | smaller_or_equal(age(A,f11(A)),tau) | greater(age(A,f12(A)),tau). [assumption]. 54 -greater(age(A,B),tau) | positional_advantage(A,B) | smaller_or_equal(age(A,f11(A)),tau) | -positional_advantage(A,f12(A)). [assumption]. 55 -greater(age(A,B),tau) | positional_advantage(A,B) | positional_advantage(A,f11(A)) | greater(age(A,f12(A)),tau). [assumption]. 56 -greater(age(A,B),tau) | positional_advantage(A,B) | positional_advantage(A,f11(A)) | -positional_advantage(A,f12(A)). [assumption]. 57 greater(high,mod1). [assumption]. 58 greater(mod1,low). [assumption]. 59 greater(low,very_low). [assumption]. 60 greater(high,mod2). [assumption]. 61 greater(mod2,low). [assumption]. 62 greater(mod2,mod1). [assumption]. 63 greater(sigma,zero). [assumption]. 64 greater(tau,zero). [assumption]. 65 smaller(sigma,tau). [assumption]. 66 -has_endowment(c1). [assumption]. 67 greater(age(c1,c2),sigma). [assumption]. 68 smaller_or_equal(age(c1,c2),tau). [assumption]. 69 smaller_or_equal(age(c1,c3),sigma). [assumption]. 70 greater(age(c1,c4),tau). [assumption]. 71 -smaller(hazard_of_mortality(c1,c4),hazard_of_mortality(c1,c3)). [assumption]. 72 age(c1,c5) = zero. [assumption]. 73 is_aligned(A,B) | dissimilar(A,B,C) | -is_aligned(A,C) | -has_endowment(A). [resolve(18,a,4,a)]. 74 -is_aligned(A,B) | dissimilar(A,B,C) | is_aligned(A,C) | -has_endowment(A). [resolve(19,a,4,a)]. 75 -dissimilar(A,B,C) | has_endowment(A) | smaller_or_equal(age(A,f1(A)),eta) | greater(age(A,f2(A)),eta). [resolve(20,a,5,b)]. 76 -dissimilar(A,B,C) | has_endowment(A) | smaller_or_equal(age(A,f1(A)),eta) | has_immunity(A,f2(A)). [resolve(20,a,6,b)]. 79 -dissimilar(A,B,C) | -smaller_or_equal(age(A,D),eta) | has_immunity(A,D) | smaller_or_equal(age(A,f3(A)),eta) | greater(age(A,f4(A)),eta). [resolve(20,a,9,c)]. 80 -dissimilar(A,B,C) | -smaller_or_equal(age(A,D),eta) | has_immunity(A,D) | smaller_or_equal(age(A,f3(A)),eta) | has_immunity(A,f4(A)). [resolve(20,a,10,c)]. 81 -dissimilar(A,B,C) | -smaller_or_equal(age(A,D),eta) | has_immunity(A,D) | -has_immunity(A,f3(A)) | greater(age(A,f4(A)),eta). [resolve(20,a,11,c)]. 82 -dissimilar(A,B,C) | -smaller_or_equal(age(A,D),eta) | has_immunity(A,D) | -has_immunity(A,f3(A)) | has_immunity(A,f4(A)). [resolve(20,a,12,c)]. 83 -dissimilar(A,B,C) | -greater(age(A,D),eta) | -has_immunity(A,D) | smaller_or_equal(age(A,f5(A)),eta) | greater(age(A,f6(A)),eta). [resolve(20,a,13,c)]. 84 -dissimilar(A,B,C) | -greater(age(A,D),eta) | -has_immunity(A,D) | smaller_or_equal(age(A,f5(A)),eta) | has_immunity(A,f6(A)). [resolve(20,a,14,c)]. 85 -dissimilar(A,B,C) | -greater(age(A,D),eta) | -has_immunity(A,D) | -has_immunity(A,f5(A)) | greater(age(A,f6(A)),eta). [resolve(20,a,15,c)]. 86 -dissimilar(A,B,C) | -greater(age(A,D),eta) | -has_immunity(A,D) | -has_immunity(A,f5(A)) | has_immunity(A,f6(A)). [resolve(20,a,16,c)]. 87 -dissimilar(A,B,C) | has_endowment(A) | -has_immunity(A,D). [resolve(20,a,17,a)]. 88 -dissimilar(A,B,C) | is_aligned(A,D) | dissimilar(A,D,E) | -is_aligned(A,E). [resolve(20,a,18,a)]. 89 -dissimilar(A,B,C) | -is_aligned(A,D) | dissimilar(A,D,E) | is_aligned(A,E). [resolve(20,a,19,a)]. 90 age(A,B) != zero | is_aligned(A,B) | -has_endowment(A). [resolve(21,a,4,a)]. 91 age(A,B) != zero | is_aligned(A,B) | -dissimilar(A,C,D). [resolve(21,a,20,a)]. 94 age(A,B) != zero | dissimilar(A,B,C) | -greater(age(A,C),sigma) | -has_endowment(A). [resolve(23,a,4,a)]. 95 age(A,B) != zero | dissimilar(A,B,C) | -greater(age(A,C),sigma) | -dissimilar(A,D,E). [resolve(23,a,20,a)]. 96 -has_immunity(A,B) | hazard_of_mortality(A,B) = very_low | -has_endowment(A). [resolve(24,a,4,a)]. 97 -has_immunity(A,B) | hazard_of_mortality(A,B) = very_low | -dissimilar(A,C,D). [resolve(24,a,20,a)]. 98 has_immunity(A,B) | -is_aligned(A,B) | -positional_advantage(A,B) | hazard_of_mortality(A,B) = low | -has_endowment(A). [resolve(25,a,4,a)]. 99 has_immunity(A,B) | -is_aligned(A,B) | -positional_advantage(A,B) | hazard_of_mortality(A,B) = low | -dissimilar(A,C,D). [resolve(25,a,20,a)]. 100 has_immunity(A,B) | is_aligned(A,B) | -positional_advantage(A,B) | hazard_of_mortality(A,B) = mod1 | -has_endowment(A). [resolve(26,a,4,a)]. 101 has_immunity(A,B) | is_aligned(A,B) | -positional_advantage(A,B) | hazard_of_mortality(A,B) = mod1 | -dissimilar(A,C,D). [resolve(26,a,20,a)]. 102 has_immunity(A,B) | -is_aligned(A,B) | positional_advantage(A,B) | hazard_of_mortality(A,B) = mod2 | -has_endowment(A). [resolve(27,a,4,a)]. 103 has_immunity(A,B) | -is_aligned(A,B) | positional_advantage(A,B) | hazard_of_mortality(A,B) = mod2 | -dissimilar(A,C,D). [resolve(27,a,20,a)]. 104 has_immunity(A,B) | is_aligned(A,B) | positional_advantage(A,B) | hazard_of_mortality(A,B) = high | -has_endowment(A). [resolve(28,a,4,a)]. 105 has_immunity(A,B) | is_aligned(A,B) | positional_advantage(A,B) | hazard_of_mortality(A,B) = high | -dissimilar(A,C,D). [resolve(28,a,20,a)]. 123 -has_immunity(c1,A). [copy(122),unit_del(a,66)]. 124 is_aligned(c1,A) | dissimilar(c1,A,B) | -is_aligned(c1,B). [resolve(29,a,18,a)]. 125 -is_aligned(c1,A) | dissimilar(c1,A,B) | is_aligned(c1,B). [resolve(29,a,19,a)]. 126 age(c1,A) != zero | is_aligned(c1,A). [resolve(29,a,21,a)]. 127 age(c1,A) != zero | dissimilar(c1,A,B) | -greater(age(c1,B),sigma). [resolve(29,a,23,a)]. 129 -is_aligned(c1,A) | -positional_advantage(c1,A) | hazard_of_mortality(c1,A) = low. [copy(128),unit_del(a,123)]. 131 is_aligned(c1,A) | -positional_advantage(c1,A) | hazard_of_mortality(c1,A) = mod1. [copy(130),unit_del(a,123)]. 133 -is_aligned(c1,A) | positional_advantage(c1,A) | hazard_of_mortality(c1,A) = mod2. [copy(132),unit_del(a,123)]. 135 is_aligned(c1,A) | positional_advantage(c1,A) | hazard_of_mortality(c1,A) = high. [copy(134),unit_del(a,123)]. 136 -smaller_or_equal(age(A,B),tau) | -positional_advantage(A,B) | smaller_or_equal(age(A,f7(A)),tau) | greater(age(A,f8(A)),tau). [resolve(30,c,31,a)]. 137 -smaller_or_equal(age(A,B),tau) | -positional_advantage(A,B) | smaller_or_equal(age(A,f7(A)),tau) | -positional_advantage(A,f8(A)). [resolve(30,c,32,a)]. 138 -smaller_or_equal(age(A,B),tau) | -positional_advantage(A,B) | positional_advantage(A,f7(A)) | greater(age(A,f8(A)),tau). [resolve(30,c,33,a)]. 139 -smaller_or_equal(age(A,B),tau) | -positional_advantage(A,B) | positional_advantage(A,f7(A)) | -positional_advantage(A,f8(A)). [resolve(30,c,34,a)]. 140 -greater(age(A,B),tau) | positional_advantage(A,B) | smaller_or_equal(age(A,f7(A)),tau) | greater(age(A,f8(A)),tau). [resolve(35,c,31,a)]. 141 -greater(age(A,B),tau) | positional_advantage(A,B) | smaller_or_equal(age(A,f7(A)),tau) | -positional_advantage(A,f8(A)). [resolve(35,c,32,a)]. 142 -greater(age(A,B),tau) | positional_advantage(A,B) | positional_advantage(A,f7(A)) | greater(age(A,f8(A)),tau). [resolve(35,c,33,a)]. 143 -greater(age(A,B),tau) | positional_advantage(A,B) | positional_advantage(A,f7(A)) | -positional_advantage(A,f8(A)). [resolve(35,c,34,a)]. 144 -smaller_or_equal(age(c1,A),tau) | -positional_advantage(c1,A). [resolve(36,a,30,c)]. 145 -greater(age(c1,A),tau) | positional_advantage(c1,A). [resolve(36,a,35,c)]. 146 -greater(A,A). [factor(42,a,b)]. 147 is_aligned(A,B) | -dissimilar(A,B,B). [factor(47,a,b)]. 148 -is_aligned(A,B) | -dissimilar(A,B,B). [factor(48,a,b)]. 149 -smaller_or_equal(age(A,f10(A)),tau) | -positional_advantage(A,f10(A)) | smaller_or_equal(age(A,f9(A)),tau). [factor(50,b,d)]. 150 -smaller_or_equal(age(A,f10(A)),tau) | -positional_advantage(A,f10(A)) | positional_advantage(A,f9(A)). [factor(52,b,d)]. 151 -greater(age(A,f11(A)),tau) | positional_advantage(A,f11(A)) | greater(age(A,f12(A)),tau). [factor(55,b,c)]. 152 -greater(age(A,f11(A)),tau) | positional_advantage(A,f11(A)) | -positional_advantage(A,f12(A)). [factor(56,b,c)]. 153 -dissimilar(A,B,C) | -smaller_or_equal(age(A,f4(A)),eta) | has_immunity(A,f4(A)) | smaller_or_equal(age(A,f3(A)),eta). [factor(80,c,e)]. 154 -dissimilar(A,B,C) | -smaller_or_equal(age(A,f4(A)),eta) | has_immunity(A,f4(A)) | -has_immunity(A,f3(A)). [factor(82,c,e)]. 155 -dissimilar(A,B,C) | -greater(age(A,f5(A)),eta) | -has_immunity(A,f5(A)) | greater(age(A,f6(A)),eta). [factor(85,c,d)]. 156 -dissimilar(A,B,C) | -greater(age(A,f5(A)),eta) | -has_immunity(A,f5(A)) | has_immunity(A,f6(A)). [factor(86,c,d)]. 157 age(A,B) != zero | greater(age(A,C),sigma) | -dissimilar(A,B,C). [factor(93,c,d)]. 159 -smaller_or_equal(age(c1,A),eta) | smaller_or_equal(age(c1,f3(c1)),eta). [back_unit_del(115),unit_del(b,123),unit_del(d,123)]. 160 smaller_or_equal(age(c1,f1(c1)),eta). [back_unit_del(109),unit_del(b,123)]. 161 -smaller_or_equal(age(A,f8(A)),tau) | -positional_advantage(A,f8(A)) | smaller_or_equal(age(A,f7(A)),tau). [factor(137,b,d)]. 162 -smaller_or_equal(age(A,f8(A)),tau) | -positional_advantage(A,f8(A)) | positional_advantage(A,f7(A)). [factor(139,b,d)]. 163 -greater(age(A,f7(A)),tau) | positional_advantage(A,f7(A)) | greater(age(A,f8(A)),tau). [factor(142,b,c)]. 164 -greater(age(A,f7(A)),tau) | positional_advantage(A,f7(A)) | -positional_advantage(A,f8(A)). [factor(143,b,c)]. end_of_list. formulas(demodulators). 72 age(c1,c5) = zero. [assumption]. end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.01 seconds. given #1 (I,wt=6): 37 smaller_or_equal(A,B) | -smaller(A,B). [assumption]. given #2 (I,wt=6): 38 smaller_or_equal(A,B) | B != A. [assumption]. given #3 (I,wt=9): 39 smaller(A,B) | B = A | -smaller_or_equal(A,B). [assumption]. given #4 (I,wt=6): 40 smaller(A,B) | -greater(B,A). [assumption]. given #5 (I,wt=6): 41 greater(A,B) | -smaller(B,A). [assumption]. given #6 (I,wt=6): 42 -greater(A,B) | -greater(B,A). [assumption]. given #7 (I,wt=9): 43 -greater(A,B) | -greater(B,C) | greater(A,C). [assumption]. given #8 (I,wt=9): 44 smaller(A,B) | B = A | greater(A,B). [assumption]. given #9 (I,wt=10): 45 -smaller_or_equal(age(A,B),eta) | has_immunity(A,B) | -has_endowment(A). [assumption]. given #10 (I,wt=10): 46 -greater(age(A,B),eta) | -has_immunity(A,B) | -has_endowment(A). [assumption]. given #11 (I,wt=10): 47 is_aligned(A,B) | is_aligned(A,C) | -dissimilar(A,B,C). [assumption]. given #12 (I,wt=10): 48 -is_aligned(A,B) | -is_aligned(A,C) | -dissimilar(A,B,C). [assumption]. given #13 (I,wt=20): 49 -smaller_or_equal(age(A,B),tau) | -positional_advantage(A,B) | smaller_or_equal(age(A,f9(A)),tau) | greater(age(A,f10(A)),tau). [assumption]. given #14 (I,wt=18): 50 -smaller_or_equal(age(A,B),tau) | -positional_advantage(A,B) | smaller_or_equal(age(A,f9(A)),tau) | -positional_advantage(A,f10(A)). [assumption]. given #15 (I,wt=18): 51 -smaller_or_equal(age(A,B),tau) | -positional_advantage(A,B) | positional_advantage(A,f9(A)) | greater(age(A,f10(A)),tau). [assumption]. given #16 (I,wt=16): 52 -smaller_or_equal(age(A,B),tau) | -positional_advantage(A,B) | positional_advantage(A,f9(A)) | -positional_advantage(A,f10(A)). [assumption]. given #17 (I,wt=20): 53 -greater(age(A,B),tau) | positional_advantage(A,B) | smaller_or_equal(age(A,f11(A)),tau) | greater(age(A,f12(A)),tau). [assumption]. given #18 (I,wt=18): 54 -greater(age(A,B),tau) | positional_advantage(A,B) | smaller_or_equal(age(A,f11(A)),tau) | -positional_advantage(A,f12(A)). [assumption]. given #19 (I,wt=18): 55 -greater(age(A,B),tau) | positional_advantage(A,B) | positional_advantage(A,f11(A)) | greater(age(A,f12(A)),tau). [assumption]. given #20 (I,wt=16): 56 -greater(age(A,B),tau) | positional_advantage(A,B) | positional_advantage(A,f11(A)) | -positional_advantage(A,f12(A)). [assumption]. given #21 (I,wt=3): 57 greater(high,mod1). [assumption]. given #22 (I,wt=3): 58 greater(mod1,low). [assumption]. given #23 (I,wt=3): 59 greater(low,very_low). [assumption]. given #24 (I,wt=3): 60 greater(high,mod2). [assumption]. given #25 (I,wt=3): 61 greater(mod2,low). [assumption]. given #26 (I,wt=3): 62 greater(mod2,mod1). [assumption]. given #27 (I,wt=3): 63 greater(sigma,zero). [assumption]. given #28 (I,wt=3): 64 greater(tau,zero). [assumption]. given #29 (I,wt=3): 65 smaller(sigma,tau). [assumption]. given #30 (I,wt=2): 66 -has_endowment(c1). [assumption]. given #31 (I,wt=5): 67 greater(age(c1,c2),sigma). [assumption]. given #32 (I,wt=5): 68 smaller_or_equal(age(c1,c2),tau). [assumption]. given #33 (I,wt=5): 69 smaller_or_equal(age(c1,c3),sigma). [assumption]. given #34 (I,wt=5): 70 greater(age(c1,c4),tau). [assumption]. given #35 (I,wt=7): 71 -smaller(hazard_of_mortality(c1,c4),hazard_of_mortality(c1,c3)). [assumption]. given #36 (I,wt=5): 72 age(c1,c5) = zero. [assumption]. given #37 (I,wt=12): 73 is_aligned(A,B) | dissimilar(A,B,C) | -is_aligned(A,C) | -has_endowment(A). [resolve(18,a,4,a)]. given #38 (I,wt=12): 74 -is_aligned(A,B) | dissimilar(A,B,C) | is_aligned(A,C) | -has_endowment(A). [resolve(19,a,4,a)]. given #39 (I,wt=18): 75 -dissimilar(A,B,C) | has_endowment(A) | smaller_or_equal(age(A,f1(A)),eta) | greater(age(A,f2(A)),eta). [resolve(20,a,5,b)]. given #40 (I,wt=16): 76 -dissimilar(A,B,C) | has_endowment(A) | smaller_or_equal(age(A,f1(A)),eta) | has_immunity(A,f2(A)). [resolve(20,a,6,b)]. given #41 (I,wt=24): 79 -dissimilar(A,B,C) | -smaller_or_equal(age(A,D),eta) | has_immunity(A,D) | smaller_or_equal(age(A,f3(A)),eta) | greater(age(A,f4(A)),eta). [resolve(20,a,9,c)]. given #42 (I,wt=22): 80 -dissimilar(A,B,C) | -smaller_or_equal(age(A,D),eta) | has_immunity(A,D) | smaller_or_equal(age(A,f3(A)),eta) | has_immunity(A,f4(A)). [resolve(20,a,10,c)]. given #43 (I,wt=22): 81 -dissimilar(A,B,C) | -smaller_or_equal(age(A,D),eta) | has_immunity(A,D) | -has_immunity(A,f3(A)) | greater(age(A,f4(A)),eta). [resolve(20,a,11,c)]. given #44 (I,wt=20): 82 -dissimilar(A,B,C) | -smaller_or_equal(age(A,D),eta) | has_immunity(A,D) | -has_immunity(A,f3(A)) | has_immunity(A,f4(A)). [resolve(20,a,12,c)]. given #45 (I,wt=24): 83 -dissimilar(A,B,C) | -greater(age(A,D),eta) | -has_immunity(A,D) | smaller_or_equal(age(A,f5(A)),eta) | greater(age(A,f6(A)),eta). [resolve(20,a,13,c)]. given #46 (I,wt=22): 84 -dissimilar(A,B,C) | -greater(age(A,D),eta) | -has_immunity(A,D) | smaller_or_equal(age(A,f5(A)),eta) | has_immunity(A,f6(A)). [resolve(20,a,14,c)]. given #47 (I,wt=22): 85 -dissimilar(A,B,C) | -greater(age(A,D),eta) | -has_immunity(A,D) | -has_immunity(A,f5(A)) | greater(age(A,f6(A)),eta). [resolve(20,a,15,c)]. given #48 (I,wt=20): 86 -dissimilar(A,B,C) | -greater(age(A,D),eta) | -has_immunity(A,D) | -has_immunity(A,f5(A)) | has_immunity(A,f6(A)). [resolve(20,a,16,c)]. given #49 (I,wt=9): 87 -dissimilar(A,B,C) | has_endowment(A) | -has_immunity(A,D). [resolve(20,a,17,a)]. given #50 (I,wt=14): 88 -dissimilar(A,B,C) | is_aligned(A,D) | dissimilar(A,D,E) | -is_aligned(A,E). [resolve(20,a,18,a)]. given #51 (I,wt=14): 89 -dissimilar(A,B,C) | -is_aligned(A,D) | dissimilar(A,D,E) | is_aligned(A,E). [resolve(20,a,19,a)]. given #52 (I,wt=10): 90 age(A,B) != zero | is_aligned(A,B) | -has_endowment(A). [resolve(21,a,4,a)]. given #53 (I,wt=12): 91 age(A,B) != zero | is_aligned(A,B) | -dissimilar(A,C,D). [resolve(21,a,20,a)]. given #54 (I,wt=16): 94 age(A,B) != zero | dissimilar(A,B,C) | -greater(age(A,C),sigma) | -has_endowment(A). [resolve(23,a,4,a)]. given #55 (I,wt=18): 95 age(A,B) != zero | dissimilar(A,B,C) | -greater(age(A,C),sigma) | -dissimilar(A,D,E). [resolve(23,a,20,a)]. given #56 (I,wt=10): 96 -has_immunity(A,B) | hazard_of_mortality(A,B) = very_low | -has_endowment(A). [resolve(24,a,4,a)]. given #57 (I,wt=12): 97 -has_immunity(A,B) | hazard_of_mortality(A,B) = very_low | -dissimilar(A,C,D). [resolve(24,a,20,a)]. given #58 (I,wt=16): 98 has_immunity(A,B) | -is_aligned(A,B) | -positional_advantage(A,B) | hazard_of_mortality(A,B) = low | -has_endowment(A). [resolve(25,a,4,a)]. given #59 (I,wt=18): 99 has_immunity(A,B) | -is_aligned(A,B) | -positional_advantage(A,B) | hazard_of_mortality(A,B) = low | -dissimilar(A,C,D). [resolve(25,a,20,a)]. given #60 (I,wt=16): 100 has_immunity(A,B) | is_aligned(A,B) | -positional_advantage(A,B) | hazard_of_mortality(A,B) = mod1 | -has_endowment(A). [resolve(26,a,4,a)]. given #61 (I,wt=18): 101 has_immunity(A,B) | is_aligned(A,B) | -positional_advantage(A,B) | hazard_of_mortality(A,B) = mod1 | -dissimilar(A,C,D). [resolve(26,a,20,a)]. given #62 (I,wt=16): 102 has_immunity(A,B) | -is_aligned(A,B) | positional_advantage(A,B) | hazard_of_mortality(A,B) = mod2 | -has_endowment(A). [resolve(27,a,4,a)]. given #63 (I,wt=18): 103 has_immunity(A,B) | -is_aligned(A,B) | positional_advantage(A,B) | hazard_of_mortality(A,B) = mod2 | -dissimilar(A,C,D). [resolve(27,a,20,a)]. given #64 (I,wt=16): 104 has_immunity(A,B) | is_aligned(A,B) | positional_advantage(A,B) | hazard_of_mortality(A,B) = high | -has_endowment(A). [resolve(28,a,4,a)]. given #65 (I,wt=18): 105 has_immunity(A,B) | is_aligned(A,B) | positional_advantage(A,B) | hazard_of_mortality(A,B) = high | -dissimilar(A,C,D). [resolve(28,a,20,a)]. given #66 (I,wt=3): 123 -has_immunity(c1,A). [copy(122),unit_del(a,66)]. given #67 (I,wt=10): 124 is_aligned(c1,A) | dissimilar(c1,A,B) | -is_aligned(c1,B). [resolve(29,a,18,a)]. given #68 (I,wt=10): 125 -is_aligned(c1,A) | dissimilar(c1,A,B) | is_aligned(c1,B). [resolve(29,a,19,a)]. given #69 (I,wt=8): 126 age(c1,A) != zero | is_aligned(c1,A). [resolve(29,a,21,a)]. given #70 (I,wt=14): 127 age(c1,A) != zero | dissimilar(c1,A,B) | -greater(age(c1,B),sigma). [resolve(29,a,23,a)]. given #71 (I,wt=11): 129 -is_aligned(c1,A) | -positional_advantage(c1,A) | hazard_of_mortality(c1,A) = low. [copy(128),unit_del(a,123)]. given #72 (I,wt=11): 131 is_aligned(c1,A) | -positional_advantage(c1,A) | hazard_of_mortality(c1,A) = mod1. [copy(130),unit_del(a,123)]. given #73 (I,wt=11): 133 -is_aligned(c1,A) | positional_advantage(c1,A) | hazard_of_mortality(c1,A) = mod2. [copy(132),unit_del(a,123)]. given #74 (I,wt=11): 135 is_aligned(c1,A) | positional_advantage(c1,A) | hazard_of_mortality(c1,A) = high. [copy(134),unit_del(a,123)]. given #75 (I,wt=20): 136 -smaller_or_equal(age(A,B),tau) | -positional_advantage(A,B) | smaller_or_equal(age(A,f7(A)),tau) | greater(age(A,f8(A)),tau). [resolve(30,c,31,a)]. given #76 (I,wt=18): 137 -smaller_or_equal(age(A,B),tau) | -positional_advantage(A,B) | smaller_or_equal(age(A,f7(A)),tau) | -positional_advantage(A,f8(A)). [resolve(30,c,32,a)]. given #77 (I,wt=18): 138 -smaller_or_equal(age(A,B),tau) | -positional_advantage(A,B) | positional_advantage(A,f7(A)) | greater(age(A,f8(A)),tau). [resolve(30,c,33,a)]. given #78 (I,wt=16): 139 -smaller_or_equal(age(A,B),tau) | -positional_advantage(A,B) | positional_advantage(A,f7(A)) | -positional_advantage(A,f8(A)). [resolve(30,c,34,a)]. given #79 (I,wt=20): 140 -greater(age(A,B),tau) | positional_advantage(A,B) | smaller_or_equal(age(A,f7(A)),tau) | greater(age(A,f8(A)),tau). [resolve(35,c,31,a)]. given #80 (I,wt=18): 141 -greater(age(A,B),tau) | positional_advantage(A,B) | smaller_or_equal(age(A,f7(A)),tau) | -positional_advantage(A,f8(A)). [resolve(35,c,32,a)]. given #81 (I,wt=18): 142 -greater(age(A,B),tau) | positional_advantage(A,B) | positional_advantage(A,f7(A)) | greater(age(A,f8(A)),tau). [resolve(35,c,33,a)]. given #82 (I,wt=16): 143 -greater(age(A,B),tau) | positional_advantage(A,B) | positional_advantage(A,f7(A)) | -positional_advantage(A,f8(A)). [resolve(35,c,34,a)]. given #83 (I,wt=8): 144 -smaller_or_equal(age(c1,A),tau) | -positional_advantage(c1,A). [resolve(36,a,30,c)]. given #84 (I,wt=8): 145 -greater(age(c1,A),tau) | positional_advantage(c1,A). [resolve(36,a,35,c)]. given #85 (I,wt=3): 146 -greater(A,A). [factor(42,a,b)]. given #86 (I,wt=7): 147 is_aligned(A,B) | -dissimilar(A,B,B). [factor(47,a,b)]. given #87 (I,wt=7): 148 -is_aligned(A,B) | -dissimilar(A,B,B). [factor(48,a,b)]. given #88 (I,wt=16): 149 -smaller_or_equal(age(A,f10(A)),tau) | -positional_advantage(A,f10(A)) | smaller_or_equal(age(A,f9(A)),tau). [factor(50,b,d)]. given #89 (I,wt=14): 150 -smaller_or_equal(age(A,f10(A)),tau) | -positional_advantage(A,f10(A)) | positional_advantage(A,f9(A)). [factor(52,b,d)]. given #90 (I,wt=16): 151 -greater(age(A,f11(A)),tau) | positional_advantage(A,f11(A)) | greater(age(A,f12(A)),tau). [factor(55,b,c)]. given #91 (I,wt=14): 152 -greater(age(A,f11(A)),tau) | positional_advantage(A,f11(A)) | -positional_advantage(A,f12(A)). [factor(56,b,c)]. given #92 (I,wt=20): 153 -dissimilar(A,B,C) | -smaller_or_equal(age(A,f4(A)),eta) | has_immunity(A,f4(A)) | smaller_or_equal(age(A,f3(A)),eta). [factor(80,c,e)]. given #93 (I,wt=18): 154 -dissimilar(A,B,C) | -smaller_or_equal(age(A,f4(A)),eta) | has_immunity(A,f4(A)) | -has_immunity(A,f3(A)). [factor(82,c,e)]. given #94 (I,wt=20): 155 -dissimilar(A,B,C) | -greater(age(A,f5(A)),eta) | -has_immunity(A,f5(A)) | greater(age(A,f6(A)),eta). [factor(85,c,d)]. given #95 (I,wt=18): 156 -dissimilar(A,B,C) | -greater(age(A,f5(A)),eta) | -has_immunity(A,f5(A)) | has_immunity(A,f6(A)). [factor(86,c,d)]. given #96 (I,wt=14): 157 age(A,B) != zero | greater(age(A,C),sigma) | -dissimilar(A,B,C). [factor(93,c,d)]. given #97 (I,wt=11): 159 -smaller_or_equal(age(c1,A),eta) | smaller_or_equal(age(c1,f3(c1)),eta). [back_unit_del(115),unit_del(b,123),unit_del(d,123)]. given #98 (I,wt=6): 160 smaller_or_equal(age(c1,f1(c1)),eta). [back_unit_del(109),unit_del(b,123)]. given #99 (I,wt=16): 161 -smaller_or_equal(age(A,f8(A)),tau) | -positional_advantage(A,f8(A)) | smaller_or_equal(age(A,f7(A)),tau). [factor(137,b,d)]. given #100 (I,wt=14): 162 -smaller_or_equal(age(A,f8(A)),tau) | -positional_advantage(A,f8(A)) | positional_advantage(A,f7(A)). [factor(139,b,d)]. given #101 (I,wt=16): 163 -greater(age(A,f7(A)),tau) | positional_advantage(A,f7(A)) | greater(age(A,f8(A)),tau). [factor(142,b,c)]. given #102 (I,wt=14): 164 -greater(age(A,f7(A)),tau) | positional_advantage(A,f7(A)) | -positional_advantage(A,f8(A)). [factor(143,b,c)]. given #103 (F,wt=3): 170 -greater(mod1,high). [resolve(57,a,42,b)]. given #104 (T,wt=3): 165 smaller_or_equal(A,A). [xx_res(38,b)]. given #105 (T,wt=3): 171 smaller(mod1,high). [resolve(57,a,40,b)]. given #106 (A,wt=9): 166 smaller(A,B) | greater(A,B) | smaller_or_equal(A,B). [resolve(44,b,38,b)]. given #107 (F,wt=3): 174 -greater(low,mod1). [resolve(58,a,42,b)]. given #108 (F,wt=3): 178 -greater(very_low,low). [resolve(59,a,42,b)]. given #109 (T,wt=3): 175 smaller(low,mod1). [resolve(58,a,40,b)]. given #110 (T,wt=3): 179 smaller(very_low,low). [resolve(59,a,40,b)]. given #111 (A,wt=9): 167 smaller(A,B) | greater(A,B) | smaller_or_equal(B,A). [resolve(44,b,38,b(flip))]. given #112 (F,wt=3): 182 -greater(mod2,high). [resolve(60,a,42,b)]. given #113 (F,wt=3): 186 -greater(low,mod2). [resolve(61,a,42,b)]. given #114 (T,wt=3): 183 smaller(mod2,high). [resolve(60,a,40,b)]. given #115 (T,wt=3): 187 smaller(low,mod2). [resolve(61,a,40,b)]. given #116 (A,wt=6): 168 -greater(A,high) | greater(A,mod1). [resolve(57,a,43,b)]. given #117 (F,wt=3): 190 -greater(mod1,mod2). [resolve(62,a,42,b)]. given #118 (F,wt=3): 194 -greater(zero,sigma). [resolve(63,a,42,b)]. given #119 (T,wt=3): 191 smaller(mod1,mod2). [resolve(62,a,40,b)]. given #120 (T,wt=3): 195 smaller(zero,sigma). [resolve(63,a,40,b)]. given #121 (A,wt=6): 169 -greater(mod1,A) | greater(high,A). [resolve(57,a,43,a)]. given #122 (F,wt=3): 198 -greater(zero,tau). [resolve(64,a,42,b)]. given #123 (F,wt=3): 247 -positional_advantage(c1,c2). [ur(144,a,68,a)]. given #124 (T,wt=3): 199 smaller(zero,tau). [resolve(64,a,40,b)]. given #125 (T,wt=3): 200 greater(tau,sigma). [resolve(65,a,41,b)]. given #126 (A,wt=6): 172 -greater(A,mod1) | greater(A,low). [resolve(58,a,43,b)]. given #127 (F,wt=3): 250 -smaller(A,A). [ur(41,a,146,a)]. given #128 (F,wt=3): 257 -greater(low,high). [ur(43,a,58,a,c,170,a)]. given #129 (T,wt=3): 201 smaller_or_equal(sigma,tau). [resolve(65,a,37,b)]. given #130 (T,wt=3): 231 is_aligned(c1,c5). [resolve(126,a,72,a)]. given #131 (A,wt=6): 173 -greater(low,A) | greater(mod1,A). [resolve(58,a,43,a)]. given #132 (F,wt=3): 258 -smaller(high,mod1). [ur(41,a,170,a)]. given #133 (F,wt=3): 263 -greater(very_low,mod1). [ur(43,a,59,a,c,174,a)]. given #134 (T,wt=3): 249 positional_advantage(c1,c4). [resolve(145,a,70,a)]. given #135 (T,wt=3): 259 smaller_or_equal(mod1,high). [resolve(171,a,37,b)]. given #136 (A,wt=6): 176 -greater(A,low) | greater(A,very_low). [resolve(59,a,43,b)]. given #137 (F,wt=3): 264 -smaller(mod1,low). [ur(41,a,174,a)]. given #138 (F,wt=3): 265 -greater(very_low,mod2). [ur(43,b,61,a,c,178,a)]. given #139 (T,wt=3): 267 smaller_or_equal(low,mod1). [resolve(175,a,37,b)]. given #140 (T,wt=3): 268 smaller_or_equal(very_low,low). [resolve(179,a,37,b)]. given #141 (A,wt=6): 177 -greater(very_low,A) | greater(low,A). [resolve(59,a,43,a)]. given #142 (F,wt=3): 266 -smaller(low,very_low). [ur(41,a,178,a)]. given #143 (F,wt=3): 270 -smaller(high,mod2). [ur(41,a,182,a)]. given #144 (T,wt=3): 272 smaller_or_equal(mod2,high). [resolve(183,a,37,b)]. given #145 (T,wt=3): 273 smaller_or_equal(low,mod2). [resolve(187,a,37,b)]. given #146 (A,wt=6): 180 -greater(A,high) | greater(A,mod2). [resolve(60,a,43,b)]. given #147 (F,wt=3): 271 -smaller(mod2,low). [ur(41,a,186,a)]. given #148 (F,wt=3): 274 -smaller(mod2,mod1). [ur(41,a,190,a)]. given #149 (T,wt=3): 277 smaller_or_equal(mod1,mod2). [resolve(191,a,37,b)]. given #150 (T,wt=3): 278 smaller_or_equal(zero,sigma). [resolve(195,a,37,b)]. given #151 (A,wt=6): 181 -greater(mod2,A) | greater(high,A). [resolve(60,a,43,a)]. given #152 (F,wt=3): 276 -smaller(sigma,zero). [ur(41,a,194,a)]. given #153 (F,wt=3): 281 -smaller(tau,zero). [ur(41,a,198,a)]. given #154 (T,wt=3): 279 greater(high,low). [resolve(169,a,58,a)]. given #155 (T,wt=3): 283 smaller_or_equal(zero,tau). [resolve(199,a,37,b)]. given #156 (A,wt=6): 184 -greater(A,mod2) | greater(A,low). [resolve(61,a,43,b)]. given #157 (F,wt=3): 284 -positional_advantage(c1,c5). [back_unit_del(248),unit_del(a,283)]. given #158 (F,wt=3): 287 -greater(sigma,tau). [resolve(200,a,42,b)]. given #159 (T,wt=3): 294 greater(mod1,very_low). [resolve(173,a,59,a)]. given #160 (T,wt=3): 298 greater(mod2,very_low). [resolve(176,a,61,a)]. given #161 (A,wt=6): 185 -greater(low,A) | greater(mod2,A). [resolve(61,a,43,a)]. given #162 (F,wt=3): 288 -greater(very_low,high). [ur(43,a,59,a,c,257,a)]. given #163 (F,wt=3): 289 -smaller(high,low). [ur(41,a,257,a)]. given #164 (T,wt=3): 300 greater(high,very_low). [resolve(279,a,176,a)]. given #165 (T,wt=3): 303 smaller(low,high). [resolve(279,a,40,b)]. given #166 (A,wt=6): 188 -greater(A,mod2) | greater(A,mod1). [resolve(62,a,43,b)]. given #167 (F,wt=3): 295 -smaller(mod1,very_low). [ur(41,a,263,a)]. given #168 (F,wt=3): 299 -smaller(mod2,very_low). [ur(41,a,265,a)]. given #169 (T,wt=3): 308 smaller(very_low,mod1). [resolve(294,a,40,b)]. given #170 (T,wt=3): 311 smaller(very_low,mod2). [resolve(298,a,40,b)]. given #171 (A,wt=6): 189 -greater(mod1,A) | greater(mod2,A). [resolve(62,a,43,a)]. given #172 (F,wt=3): 305 -smaller(tau,sigma). [ur(41,a,287,a)]. given #173 (F,wt=3): 312 -smaller(high,very_low). [ur(41,a,288,a)]. given #174 (T,wt=3): 315 smaller(very_low,high). [resolve(300,a,40,b)]. given #175 (T,wt=3): 316 smaller_or_equal(low,high). [resolve(303,a,37,b)]. given #176 (A,wt=6): 192 -greater(A,sigma) | greater(A,zero). [resolve(63,a,43,b)]. given #177 (F,wt=4): 293 -dissimilar(c1,c5,c5). [ur(148,a,231,a)]. given #178 (F,wt=5): 204 -greater(sigma,age(c1,c2)). [resolve(67,a,42,b)]. given #179 (T,wt=3): 317 smaller_or_equal(very_low,mod1). [resolve(308,a,37,b)]. given #180 (T,wt=3): 318 smaller_or_equal(very_low,mod2). [resolve(311,a,37,b)]. given #181 (A,wt=6): 193 -greater(zero,A) | greater(sigma,A). [resolve(63,a,43,a)]. given #182 (F,wt=5): 212 -greater(tau,age(c1,c4)). [resolve(70,a,42,b)]. given #183 (F,wt=5): 275 -greater(zero,age(c1,c2)). [ur(43,b,67,a,c,194,a)]. given #184 (T,wt=3): 319 smaller_or_equal(very_low,high). [resolve(315,a,37,b)]. given #185 (T,wt=5): 205 smaller(sigma,age(c1,c2)). [resolve(67,a,40,b)]. given #186 (A,wt=6): 196 -greater(A,tau) | greater(A,zero). [resolve(64,a,43,b)]. given #187 (F,wt=5): 280 -greater(zero,age(c1,c4)). [ur(43,b,70,a,c,198,a)]. given #188 (F,wt=5): 282 -greater(age(c1,c2),tau). [ur(145,b,247,a)]. given #189 (T,wt=5): 213 smaller(tau,age(c1,c4)). [resolve(70,a,40,b)]. given #190 (T,wt=5): 290 hazard_of_mortality(c1,c5) = mod2. [resolve(231,a,133,a),unit_del(a,284)]. given #191 (A,wt=6): 197 -greater(zero,A) | greater(tau,A). [resolve(64,a,43,a)]. given #192 (F,wt=5): 296 -smaller_or_equal(age(c1,c4),tau). [resolve(249,a,144,b)]. given #193 (F,wt=5): 304 -greater(sigma,age(c1,c4)). [ur(43,b,70,a,c,287,a)]. given #194 (T,wt=5): 320 greater(age(c1,c2),zero). [resolve(192,a,67,a)]. given #195 (T,wt=5): 324 smaller_or_equal(sigma,age(c1,c2)). [resolve(205,a,37,b)]. given #196 (A,wt=8): 202 -greater(A,age(c1,c2)) | greater(A,sigma). [resolve(67,a,43,b)]. given #197 (F,wt=5): 321 -smaller(age(c1,c2),sigma). [ur(41,a,204,a)]. given #198 (F,wt=5): 322 -smaller(age(c1,c4),tau). [ur(41,a,212,a)]. given #199 (T,wt=5): 325 greater(age(c1,c4),zero). [resolve(196,a,70,a)]. given #200 (T,wt=5): 329 smaller_or_equal(tau,age(c1,c4)). [resolve(213,a,37,b)]. given #201 (A,wt=8): 203 -greater(sigma,A) | greater(age(c1,c2),A). [resolve(67,a,43,a)]. given #202 (F,wt=5): 323 -smaller(age(c1,c2),zero). [ur(41,a,275,a)]. given #203 (F,wt=5): 326 -smaller(age(c1,c4),zero). [ur(41,a,280,a)]. given #204 (T,wt=5): 334 smaller(zero,age(c1,c2)). [resolve(320,a,40,b)]. given #205 (T,wt=5): 337 smaller(zero,age(c1,c4)). [resolve(325,a,40,b)]. given #206 (A,wt=10): 206 smaller(age(c1,c2),tau) | age(c1,c2) = tau. [resolve(68,a,39,c),flip(b)]. given #207 (F,wt=5): 328 -smaller(tau,age(c1,c2)). [ur(41,a,282,a)]. given #208 (F,wt=5): 330 age(c1,c4) != tau. [ur(38,a,296,a),flip(a)]. given #209 (T,wt=5): 338 smaller_or_equal(zero,age(c1,c2)). [resolve(334,a,37,b)]. given #210 (T,wt=5): 339 smaller_or_equal(zero,age(c1,c4)). [resolve(337,a,37,b)]. given #211 (A,wt=10): 207 smaller(age(c1,c3),sigma) | age(c1,c3) = sigma. [resolve(69,a,39,c),flip(b)]. given #212 (F,wt=5): 331 -smaller(age(c1,c4),sigma). [ur(41,a,304,a)]. given #213 (F,wt=7): 214 -greater(hazard_of_mortality(c1,c3),hazard_of_mortality(c1,c4)). [ur(40,a,71,a)]. given #214 (T,wt=6): 255 smaller_or_equal(age(c1,f3(c1)),eta). [resolve(160,a,159,a)]. given #215 (T,wt=6): 262 greater(A,B) | smaller_or_equal(A,B). [resolve(166,a,37,b),merge(c)]. given #216 (A,wt=8): 210 -greater(A,age(c1,c4)) | greater(A,tau). [resolve(70,a,43,b)]. given #217 (F,wt=7): 327 -greater(age(c1,c2),age(c1,c4)). [ur(43,b,70,a,c,282,a)]. given #218 (F,wt=7): 367 -smaller(age(c1,c4),age(c1,c2)). [ur(41,a,327,a)]. given #219 (T,wt=6): 285 -greater(A,tau) | greater(A,sigma). [resolve(200,a,43,b)]. given #220 (T,wt=5): 369 greater(age(c1,c4),sigma). [resolve(285,a,70,a)]. given #221 (A,wt=8): 211 -greater(tau,A) | greater(age(c1,c4),A). [resolve(70,a,43,a)]. given #222 (F,wt=5): 372 smaller(sigma,age(c1,c4)). [resolve(369,a,40,b)]. given #223 (F,wt=5): 373 smaller_or_equal(sigma,age(c1,c4)). [resolve(372,a,37,b)]. given #224 (T,wt=6): 286 -greater(sigma,A) | greater(tau,A). [resolve(200,a,43,a)]. given #225 (T,wt=6): 301 -greater(A,high) | greater(A,low). [resolve(279,a,43,b)]. given #226 (A,wt=15): 221 is_aligned(A,B) | -has_endowment(A) | smaller(zero,age(A,B)) | greater(zero,age(A,B)). [resolve(90,a,44,b)]. given #227 (F,wt=6): 302 -greater(low,A) | greater(high,A). [resolve(279,a,43,a)]. given #228 (F,wt=6): 306 -greater(A,mod1) | greater(A,very_low). [resolve(294,a,43,b)]. given #229 (T,wt=6): 307 -greater(very_low,A) | greater(mod1,A). [resolve(294,a,43,a)]. given #230 (T,wt=6): 309 -greater(A,mod2) | greater(A,very_low). [resolve(298,a,43,b)]. given #231 (A,wt=15): 222 is_aligned(A,B) | -has_endowment(A) | smaller(age(A,B),zero) | greater(age(A,B),zero). [resolve(90,a,44,b(flip))]. given #232 (F,wt=6): 310 -greater(very_low,A) | greater(mod2,A). [resolve(298,a,43,a)]. given #233 (F,wt=6): 313 -greater(A,high) | greater(A,very_low). [resolve(300,a,43,b)]. given #234 (T,wt=6): 314 -greater(very_low,A) | greater(high,A). [resolve(300,a,43,a)]. given #235 (T,wt=7): 291 dissimilar(c1,c5,A) | is_aligned(c1,A). [resolve(231,a,125,a)]. given #236 (A,wt=17): 224 is_aligned(A,B) | -dissimilar(A,C,D) | smaller(zero,age(A,B)) | greater(zero,age(A,B)). [resolve(91,a,44,b)]. given #237 (F,wt=7): 292 is_aligned(c1,A) | dissimilar(c1,A,c5). [resolve(231,a,124,c)]. given #238 (F,wt=8): 297 is_aligned(c1,c4) | hazard_of_mortality(c1,c4) = mod1. [resolve(249,a,131,b)]. given #239 (T,wt=8): 332 -greater(A,age(c1,c2)) | greater(A,zero). [resolve(320,a,43,b)]. given #240 (T,wt=8): 333 -greater(zero,A) | greater(age(c1,c2),A). [resolve(320,a,43,a)]. given #241 (A,wt=17): 225 is_aligned(A,B) | -dissimilar(A,C,D) | smaller(age(A,B),zero) | greater(age(A,B),zero). [resolve(91,a,44,b(flip))]. given #242 (F,wt=8): 335 -greater(A,age(c1,c4)) | greater(A,zero). [resolve(325,a,43,b)]. given #243 (F,wt=8): 336 -greater(zero,A) | greater(age(c1,c4),A). [resolve(325,a,43,a)]. given #244 (T,wt=8): 361 smaller(age(c1,c3),sigma) | -positional_advantage(c1,c3). [para(207(b,1),144(a,1)),unit_del(b,201)]. given #245 (T,wt=8): 370 -greater(A,age(c1,c4)) | greater(A,sigma). [resolve(369,a,43,b)]. given #246 (A,wt=21): 226 dissimilar(A,B,C) | -greater(age(A,C),sigma) | -has_endowment(A) | smaller(zero,age(A,B)) | greater(zero,age(A,B)). [resolve(94,a,44,b)]. given #247 (F,wt=8): 371 -greater(sigma,A) | greater(age(c1,c4),A). [resolve(369,a,43,a)]. given #248 (F,wt=8): 374 is_aligned(c1,c4) | smaller_or_equal(mod1,hazard_of_mortality(c1,c4)). [resolve(297,b,38,b)]. given #249 (T,wt=8): 375 is_aligned(c1,c4) | smaller_or_equal(hazard_of_mortality(c1,c4),mod1). [resolve(297,b,38,b(flip))]. given #250 (T,wt=8): 376 is_aligned(c1,c4) | -smaller(mod1,hazard_of_mortality(c1,c3)). [para(297(b,1),71(a,1))]. given #251 (A,wt=21): 227 dissimilar(A,B,C) | -greater(age(A,C),sigma) | -has_endowment(A) | smaller(age(A,B),zero) | greater(age(A,B),zero). [resolve(94,a,44,b(flip))]. given #252 (F,wt=8): 377 is_aligned(c1,c4) | -greater(hazard_of_mortality(c1,c3),mod1). [para(297(b,1),214(a,2))]. given #253 (F,wt=9): 234 dissimilar(c1,c5,A) | -greater(age(c1,A),sigma). [resolve(127,a,72,a)]. given #254 (T,wt=4): 386 dissimilar(c1,c5,c4). [resolve(234,b,369,a)]. given #255 (T,wt=4): 387 dissimilar(c1,c5,c2). [resolve(234,b,67,a)]. given #256 (A,wt=23): 229 dissimilar(A,B,C) | -greater(age(A,C),sigma) | -dissimilar(A,D,E) | smaller(zero,age(A,B)) | greater(zero,age(A,B)). [resolve(95,a,44,b)]. given #257 (F,wt=3): 388 -is_aligned(c1,c4). [resolve(386,a,48,c),unit_del(a,231)]. given #258 (F,wt=3): 396 -is_aligned(c1,c2). [resolve(387,a,48,c),unit_del(a,231)]. given #259 (T,wt=5): 395 hazard_of_mortality(c1,c4) = mod1. [back_unit_del(297),unit_del(a,388)]. given #260 (T,wt=6): 389 is_aligned(c1,c3) | positional_advantage(c1,c3). [back_unit_del(385),unit_del(c,388)]. given #261 (A,wt=23): 230 dissimilar(A,B,C) | -greater(age(A,C),sigma) | -dissimilar(A,D,E) | smaller(age(A,B),zero) | greater(age(A,B),zero). [resolve(95,a,44,b(flip))]. given #262 (F,wt=4): 399 -dissimilar(c1,c4,c4). [ur(147,a,388,a)]. given #263 (F,wt=4): 401 -dissimilar(c1,c2,c2). [ur(147,a,396,a)]. given #264 (T,wt=8): 397 smaller(age(c1,c2),tau) | zero != tau. [back_unit_del(344),unit_del(c,396)]. given #265 (T,wt=8): 405 positional_advantage(c1,c3) | hazard_of_mortality(c1,c3) = mod2. [resolve(389,a,133,a),merge(b)]. given #266 (A,wt=13): 232 is_aligned(c1,A) | smaller(zero,age(c1,A)) | greater(zero,age(c1,A)). [resolve(126,a,44,b)]. given #267 (F,wt=4): 403 -dissimilar(c1,c4,c2). [ur(47,a,388,a,b,396,a)]. given #268 (F,wt=4): 404 -dissimilar(c1,c2,c4). [ur(47,a,396,a,b,388,a)]. given #269 (T,wt=8): 409 positional_advantage(c1,c3) | smaller_or_equal(mod2,hazard_of_mortality(c1,c3)). [resolve(405,b,38,b)]. given #270 (T,wt=8): 410 positional_advantage(c1,c3) | smaller_or_equal(hazard_of_mortality(c1,c3),mod2). [resolve(405,b,38,b(flip))]. given #271 (A,wt=13): 233 is_aligned(c1,A) | smaller(age(c1,A),zero) | greater(age(c1,A),zero). [resolve(126,a,44,b(flip))]. given #272 (F,wt=5): 391 -greater(hazard_of_mortality(c1,c3),mod1). [back_unit_del(377),unit_del(a,388)]. given #273 (F,wt=5): 392 -smaller(mod1,hazard_of_mortality(c1,c3)). [back_unit_del(376),unit_del(a,388)]. given #274 (T,wt=3): 421 positional_advantage(c1,c3). [para(405(b,1),391(a,1)),unit_del(b,62)]. given #275 (T,wt=5): 422 smaller(age(c1,c3),sigma). [back_unit_del(361),unit_del(b,421)]. given #276 (A,wt=19): 235 dissimilar(c1,A,B) | -greater(age(c1,B),sigma) | smaller(zero,age(c1,A)) | greater(zero,age(c1,A)). [resolve(127,a,44,b)]. given #277 (F,wt=5): 400 age(c1,c4) != zero. [ur(126,b,388,a)]. given #278 (F,wt=5): 402 age(c1,c2) != zero. [ur(126,b,396,a)]. given #279 (T,wt=5): 425 greater(sigma,age(c1,c3)). [resolve(422,a,41,b)]. given #280 (T,wt=5): 431 greater(tau,age(c1,c3)). [resolve(425,a,286,a)]. given #281 (A,wt=19): 236 dissimilar(c1,A,B) | -greater(age(c1,B),sigma) | smaller(age(c1,A),zero) | greater(age(c1,A),zero). [resolve(127,a,44,b(flip))]. given #282 (F,wt=5): 419 -greater(hazard_of_mortality(c1,c3),mod2). [ur(188,b,391,a)]. given #283 (F,wt=5): 420 -greater(hazard_of_mortality(c1,c3),high). [ur(168,b,391,a)]. given #284 (T,wt=5): 441 smaller(age(c1,c3),tau). [resolve(431,a,40,b)]. ============================== PROOF ================================= % Proof 1 at 0.04 (+ 0.01) seconds. % Length of proof is 64. % Level of proof is 14. % Maximum clause weight is 14. % Given clauses 284. 17 -organization(A) | has_endowment(A) | -has_immunity(A,B). [assumption]. 21 -organization(A) | age(A,B) != zero | is_aligned(A,B). [assumption]. 23 -organization(A) | age(A,B) != zero | dissimilar(A,B,C) | -greater(age(A,C),sigma). [assumption]. 26 -organization(A) | has_immunity(A,B) | is_aligned(A,B) | -positional_advantage(A,B) | hazard_of_mortality(A,B) = mod1. [assumption]. 27 -organization(A) | has_immunity(A,B) | -is_aligned(A,B) | positional_advantage(A,B) | hazard_of_mortality(A,B) = mod2. [assumption]. 28 -organization(A) | has_immunity(A,B) | is_aligned(A,B) | positional_advantage(A,B) | hazard_of_mortality(A,B) = high. [assumption]. 29 organization(c1). [assumption]. 30 -smaller_or_equal(age(A,B),tau) | -positional_advantage(A,B) | -robust_position(A). [assumption]. 35 -greater(age(A,B),tau) | positional_advantage(A,B) | -robust_position(A). [assumption]. 36 robust_position(c1). [assumption]. 37 smaller_or_equal(A,B) | -smaller(A,B). [assumption]. 39 smaller(A,B) | B = A | -smaller_or_equal(A,B). [assumption]. 40 smaller(A,B) | -greater(B,A). [assumption]. 41 greater(A,B) | -smaller(B,A). [assumption]. 43 -greater(A,B) | -greater(B,C) | greater(A,C). [assumption]. 48 -is_aligned(A,B) | -is_aligned(A,C) | -dissimilar(A,B,C). [assumption]. 57 greater(high,mod1). [assumption]. 62 greater(mod2,mod1). [assumption]. 65 smaller(sigma,tau). [assumption]. 66 -has_endowment(c1). [assumption]. 69 smaller_or_equal(age(c1,c3),sigma). [assumption]. 70 greater(age(c1,c4),tau). [assumption]. 71 -smaller(hazard_of_mortality(c1,c4),hazard_of_mortality(c1,c3)). [assumption]. 72 age(c1,c5) = zero. [assumption]. 122 has_endowment(c1) | -has_immunity(c1,A). [resolve(29,a,17,a)]. 123 -has_immunity(c1,A). [copy(122),unit_del(a,66)]. 126 age(c1,A) != zero | is_aligned(c1,A). [resolve(29,a,21,a)]. 127 age(c1,A) != zero | dissimilar(c1,A,B) | -greater(age(c1,B),sigma). [resolve(29,a,23,a)]. 130 has_immunity(c1,A) | is_aligned(c1,A) | -positional_advantage(c1,A) | hazard_of_mortality(c1,A) = mod1. [resolve(29,a,26,a)]. 131 is_aligned(c1,A) | -positional_advantage(c1,A) | hazard_of_mortality(c1,A) = mod1. [copy(130),unit_del(a,123)]. 132 has_immunity(c1,A) | -is_aligned(c1,A) | positional_advantage(c1,A) | hazard_of_mortality(c1,A) = mod2. [resolve(29,a,27,a)]. 133 -is_aligned(c1,A) | positional_advantage(c1,A) | hazard_of_mortality(c1,A) = mod2. [copy(132),unit_del(a,123)]. 134 has_immunity(c1,A) | is_aligned(c1,A) | positional_advantage(c1,A) | hazard_of_mortality(c1,A) = high. [resolve(29,a,28,a)]. 135 is_aligned(c1,A) | positional_advantage(c1,A) | hazard_of_mortality(c1,A) = high. [copy(134),unit_del(a,123)]. 144 -smaller_or_equal(age(c1,A),tau) | -positional_advantage(c1,A). [resolve(36,a,30,c)]. 145 -greater(age(c1,A),tau) | positional_advantage(c1,A). [resolve(36,a,35,c)]. 171 smaller(mod1,high). [resolve(57,a,40,b)]. 200 greater(tau,sigma). [resolve(65,a,41,b)]. 201 smaller_or_equal(sigma,tau). [resolve(65,a,37,b)]. 207 smaller(age(c1,c3),sigma) | age(c1,c3) = sigma. [resolve(69,a,39,c),flip(b)]. 214 -greater(hazard_of_mortality(c1,c3),hazard_of_mortality(c1,c4)). [ur(40,a,71,a)]. 231 is_aligned(c1,c5). [resolve(126,a,72,a)]. 234 dissimilar(c1,c5,A) | -greater(age(c1,A),sigma). [resolve(127,a,72,a)]. 249 positional_advantage(c1,c4). [resolve(145,a,70,a)]. 285 -greater(A,tau) | greater(A,sigma). [resolve(200,a,43,b)]. 286 -greater(sigma,A) | greater(tau,A). [resolve(200,a,43,a)]. 297 is_aligned(c1,c4) | hazard_of_mortality(c1,c4) = mod1. [resolve(249,a,131,b)]. 361 smaller(age(c1,c3),sigma) | -positional_advantage(c1,c3). [para(207(b,1),144(a,1)),unit_del(b,201)]. 369 greater(age(c1,c4),sigma). [resolve(285,a,70,a)]. 376 is_aligned(c1,c4) | -smaller(mod1,hazard_of_mortality(c1,c3)). [para(297(b,1),71(a,1))]. 377 is_aligned(c1,c4) | -greater(hazard_of_mortality(c1,c3),mod1). [para(297(b,1),214(a,2))]. 385 is_aligned(c1,c3) | positional_advantage(c1,c3) | is_aligned(c1,c4). [para(135(c,1),376(b,2)),unit_del(d,171)]. 386 dissimilar(c1,c5,c4). [resolve(234,b,369,a)]. 388 -is_aligned(c1,c4). [resolve(386,a,48,c),unit_del(a,231)]. 389 is_aligned(c1,c3) | positional_advantage(c1,c3). [back_unit_del(385),unit_del(c,388)]. 391 -greater(hazard_of_mortality(c1,c3),mod1). [back_unit_del(377),unit_del(a,388)]. 405 positional_advantage(c1,c3) | hazard_of_mortality(c1,c3) = mod2. [resolve(389,a,133,a),merge(b)]. 421 positional_advantage(c1,c3). [para(405(b,1),391(a,1)),unit_del(b,62)]. 422 smaller(age(c1,c3),sigma). [back_unit_del(361),unit_del(b,421)]. 423 -smaller_or_equal(age(c1,c3),tau). [resolve(421,a,144,b)]. 425 greater(sigma,age(c1,c3)). [resolve(422,a,41,b)]. 431 greater(tau,age(c1,c3)). [resolve(425,a,286,a)]. 441 smaller(age(c1,c3),tau). [resolve(431,a,40,b)]. 446 $F. [resolve(441,a,37,b),unit_del(a,423)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=284. Generated=1151. Kept=400. proofs=1. Usable=269. Sos=33. Demods=3. Limbo=0, Disabled=243. Hints=0. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=750. Back_subsumed=80. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=3 (0 lex), Back_demodulated=5. Back_unit_deleted=13. Demod_attempts=10022. Demod_rewrites=22. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=202. Nonunit_bsub_feature_tests=458. Megabytes=0.59. User_CPU=0.04, System_CPU=0.01, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 3770 exit (max_proofs) Wed Nov 22 11:23:39 2006 ============================== continuing FOF reduction multisearch == Subproblem 2 of 3 (negated): ((all X (all Y (smaller_or_equal(X,Y) | - smaller(X,Y)))) & (all X (all Y (smaller_or_equal(X,Y) | - =(Y,X)))) & (all X (all Y (smaller(X,Y) | =(Y,X) | - smaller_or_equal(X,Y)))) & (all X (all Y (greater_or_equal(X,Y) | - greater(X,Y)))) & (all X (all Y (greater_or_equal(X,Y) | - =(Y,X)))) & (all X (all Y (greater(X,Y) | =(Y,X) | - greater_or_equal(X,Y)))) & (all X (all Y (smaller(X,Y) | - greater(Y,X)))) & (all X (all Y (greater(Y,X) | - smaller(X,Y)))) & (all X (all Y (- greater(X,Y) | - greater(Y,X)))) & (all X (all Y (- greater(X,Y) | (all Z (- greater(Y,Z) | greater(X,Z)))))) & (all X (all Y (smaller(X,Y) | =(Y,X) | greater(X,Y)))) & (all X (has_endowment(X) | - organization(X) | (exists T (smaller_or_equal(age(X,T),eta) & - has_immunity(X,T))) | (exists T (greater(age(X,T),eta) & has_immunity(X,T))))) & (all X (organization(X) | - has_endowment(X))) & (all X ((all T (- smaller_or_equal(age(X,T),eta) | has_immunity(X,T))) | - has_endowment(X))) & (all X ((all T (- smaller_or_equal(age(X,T),eta) | has_immunity(X,T))) | - organization(X) | (exists T (smaller_or_equal(age(X,T),eta) & - has_immunity(X,T))) | (exists T (greater(age(X,T),eta) & has_immunity(X,T))))) & (all X ((all T (- greater(age(X,T),eta) | - has_immunity(X,T))) | - has_endowment(X))) & (all X ((all T (- greater(age(X,T),eta) | - has_immunity(X,T))) | - organization(X) | (exists T (smaller_or_equal(age(X,T),eta) & - has_immunity(X,T))) | (exists T (greater(age(X,T),eta) & has_immunity(X,T))))) & (all X (- organization(X) | has_endowment(X) | (all T (- has_immunity(X,T))))) & (all X (- organization(X) | (all T0 (is_aligned(X,T0) | (all T (dissimilar(X,T0,T) | - is_aligned(X,T))))))) & (all X (- organization(X) | (all T0 (- is_aligned(X,T0) | (all T (dissimilar(X,T0,T) | is_aligned(X,T))))))) & (all X (organization(X) | (all T0 ((all T (- dissimilar(X,T0,T))))))) & (all X (all T0 (is_aligned(X,T0) | (all T (is_aligned(X,T) | - dissimilar(X,T0,T)))))) & (all X (all T0 (- is_aligned(X,T0) | (all T (- is_aligned(X,T) | - dissimilar(X,T0,T)))))) & (all X (- organization(X) | (all T (- =(age(X,T),zero) | is_aligned(X,T))))) & (all X (- organization(X) | (all T0 (- =(age(X,T0),zero) | (all T (greater(age(X,T),sigma) | - dissimilar(X,T0,T))))))) & (all X (- organization(X) | (all T0 (- =(age(X,T0),zero) | (all T (dissimilar(X,T0,T) | - greater(age(X,T),sigma))))))) & (all X (robust_position(X) | (exists T (smaller_or_equal(age(X,T),tau) & positional_advantage(X,T))) | (exists T (greater(age(X,T),tau) & - positional_advantage(X,T))))) & (all X ((all T (- smaller_or_equal(age(X,T),tau) | - positional_advantage(X,T))) | - robust_position(X))) & (all X ((all T (- smaller_or_equal(age(X,T),tau) | - positional_advantage(X,T))) | (exists T (smaller_or_equal(age(X,T),tau) & positional_advantage(X,T))) | (exists T (greater(age(X,T),tau) & - positional_advantage(X,T))))) & (all X ((all T (- greater(age(X,T),tau) | positional_advantage(X,T))) | - robust_position(X))) & (all X ((all T (- greater(age(X,T),tau) | positional_advantage(X,T))) | (exists T (smaller_or_equal(age(X,T),tau) & positional_advantage(X,T))) | (exists T (greater(age(X,T),tau) & - positional_advantage(X,T))))) & (all X (- organization(X) | (all T (- has_immunity(X,T) | =(hazard_of_mortality(X,T),very_low))))) & (all X (- organization(X) | (all T (has_immunity(X,T) | - is_aligned(X,T) | - positional_advantage(X,T) | =(hazard_of_mortality(X,T),low))))) & (all X (- organization(X) | (all T (has_immunity(X,T) | is_aligned(X,T) | - positional_advantage(X,T) | =(hazard_of_mortality(X,T),mod1))))) & (all X (- organization(X) | (all T (has_immunity(X,T) | - is_aligned(X,T) | positional_advantage(X,T) | =(hazard_of_mortality(X,T),mod2))))) & (all X (- organization(X) | (all T (has_immunity(X,T) | is_aligned(X,T) | positional_advantage(X,T) | =(hazard_of_mortality(X,T),high))))) & greater(high,mod1) & greater(mod1,low) & greater(low,very_low) & greater(high,mod2) & greater(mod2,low) & greater(mod2,mod1) & greater(sigma,zero) & greater(tau,zero) & smaller(sigma,tau) & (exists X (organization(X) & robust_position(X) & - has_endowment(X) & (exists T3 (greater(age(X,T3),tau))) & (exists T1 (smaller_or_equal(age(X,T1),sigma) & (exists T2 (greater(age(X,T2),sigma) & smaller_or_equal(age(X,T2),tau) & - smaller(hazard_of_mortality(X,T1),hazard_of_mortality(X,T2)))))) & (exists T0 (=(age(X,T0),zero)))))). Child search process 3771 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). smaller_or_equal(A,B) | -smaller(A,B). [assumption]. smaller_or_equal(A,B) | B != A. [assumption]. smaller(A,B) | B = A | -smaller_or_equal(A,B). [assumption]. greater_or_equal(A,B) | -greater(A,B). [assumption]. greater_or_equal(A,B) | B != A. [assumption]. greater(A,B) | B = A | -greater_or_equal(A,B). [assumption]. smaller(A,B) | -greater(B,A). [assumption]. greater(A,B) | -smaller(B,A). [assumption]. -greater(A,B) | -greater(B,A). [assumption]. -greater(A,B) | -greater(B,C) | greater(A,C). [assumption]. smaller(A,B) | B = A | greater(A,B). [assumption]. has_endowment(A) | -organization(A) | smaller_or_equal(age(A,f1(A)),eta) | greater(age(A,f2(A)),eta). [assumption]. has_endowment(A) | -organization(A) | smaller_or_equal(age(A,f1(A)),eta) | has_immunity(A,f2(A)). [assumption]. has_endowment(A) | -organization(A) | -has_immunity(A,f1(A)) | greater(age(A,f2(A)),eta). [assumption]. has_endowment(A) | -organization(A) | -has_immunity(A,f1(A)) | has_immunity(A,f2(A)). [assumption]. organization(A) | -has_endowment(A). [assumption]. -smaller_or_equal(age(A,B),eta) | has_immunity(A,B) | -has_endowment(A). [assumption]. -smaller_or_equal(age(A,B),eta) | has_immunity(A,B) | -organization(A) | smaller_or_equal(age(A,f3(A)),eta) | greater(age(A,f4(A)),eta). [assumption]. -smaller_or_equal(age(A,B),eta) | has_immunity(A,B) | -organization(A) | smaller_or_equal(age(A,f3(A)),eta) | has_immunity(A,f4(A)). [assumption]. -smaller_or_equal(age(A,B),eta) | has_immunity(A,B) | -organization(A) | -has_immunity(A,f3(A)) | greater(age(A,f4(A)),eta). [assumption]. -smaller_or_equal(age(A,B),eta) | has_immunity(A,B) | -organization(A) | -has_immunity(A,f3(A)) | has_immunity(A,f4(A)). [assumption]. -greater(age(A,B),eta) | -has_immunity(A,B) | -has_endowment(A). [assumption]. -greater(age(A,B),eta) | -has_immunity(A,B) | -organization(A) | smaller_or_equal(age(A,f5(A)),eta) | greater(age(A,f6(A)),eta). [assumption]. -greater(age(A,B),eta) | -has_immunity(A,B) | -organization(A) | smaller_or_equal(age(A,f5(A)),eta) | has_immunity(A,f6(A)). [assumption]. -greater(age(A,B),eta) | -has_immunity(A,B) | -organization(A) | -has_immunity(A,f5(A)) | greater(age(A,f6(A)),eta). [assumption]. -greater(age(A,B),eta) | -has_immunity(A,B) | -organization(A) | -has_immunity(A,f5(A)) | has_immunity(A,f6(A)). [assumption]. -organization(A) | has_endowment(A) | -has_immunity(A,B). [assumption]. -organization(A) | is_aligned(A,B) | dissimilar(A,B,C) | -is_aligned(A,C). [assumption]. -organization(A) | -is_aligned(A,B) | dissimilar(A,B,C) | is_aligned(A,C). [assumption]. organization(A) | -dissimilar(A,B,C). [assumption]. is_aligned(A,B) | is_aligned(A,C) | -dissimilar(A,B,C). [assumption]. -is_aligned(A,B) | -is_aligned(A,C) | -dissimilar(A,B,C). [assumption]. -organization(A) | age(A,B) != zero | is_aligned(A,B). [assumption]. -organization(A) | age(A,B) != zero | greater(age(A,C),sigma) | -dissimilar(A,B,C). [assumption]. -organization(A) | age(A,B) != zero | dissimilar(A,B,C) | -greater(age(A,C),sigma). [assumption]. robust_position(A) | smaller_or_equal(age(A,f7(A)),tau) | greater(age(A,f8(A)),tau). [assumption]. robust_position(A) | smaller_or_equal(age(A,f7(A)),tau) | -positional_advantage(A,f8(A)). [assumption]. robust_position(A) | positional_advantage(A,f7(A)) | greater(age(A,f8(A)),tau). [assumption]. robust_position(A) | positional_advantage(A,f7(A)) | -positional_advantage(A,f8(A)). [assumption]. -smaller_or_equal(age(A,B),tau) | -positional_advantage(A,B) | -robust_position(A). [assumption]. -smaller_or_equal(age(A,B),tau) | -positional_advantage(A,B) | smaller_or_equal(age(A,f9(A)),tau) | greater(age(A,f10(A)),tau). [assumption]. -smaller_or_equal(age(A,B),tau) | -positional_advantage(A,B) | smaller_or_equal(age(A,f9(A)),tau) | -positional_advantage(A,f10(A)). [assumption]. -smaller_or_equal(age(A,B),tau) | -positional_advantage(A,B) | positional_advantage(A,f9(A)) | greater(age(A,f10(A)),tau). [assumption]. -smaller_or_equal(age(A,B),tau) | -positional_advantage(A,B) | positional_advantage(A,f9(A)) | -positional_advantage(A,f10(A)). [assumption]. -greater(age(A,B),tau) | positional_advantage(A,B) | -robust_position(A). [assumption]. -greater(age(A,B),tau) | positional_advantage(A,B) | smaller_or_equal(age(A,f11(A)),tau) | greater(age(A,f12(A)),tau). [assumption]. -greater(age(A,B),tau) | positional_advantage(A,B) | smaller_or_equal(age(A,f11(A)),tau) | -positional_advantage(A,f12(A)). [assumption]. -greater(age(A,B),tau) | positional_advantage(A,B) | positional_advantage(A,f11(A)) | greater(age(A,f12(A)),tau). [assumption]. -greater(age(A,B),tau) | positional_advantage(A,B) | positional_advantage(A,f11(A)) | -positional_advantage(A,f12(A)). [assumption]. -organization(A) | -has_immunity(A,B) | hazard_of_mortality(A,B) = very_low. [assumption]. -organization(A) | has_immunity(A,B) | -is_aligned(A,B) | -positional_advantage(A,B) | hazard_of_mortality(A,B) = low. [assumption]. -organization(A) | has_immunity(A,B) | is_aligned(A,B) | -positional_advantage(A,B) | hazard_of_mortality(A,B) = mod1. [assumption]. -organization(A) | has_immunity(A,B) | -is_aligned(A,B) | positional_advantage(A,B) | hazard_of_mortality(A,B) = mod2. [assumption]. -organization(A) | has_immunity(A,B) | is_aligned(A,B) | positional_advantage(A,B) | hazard_of_mortality(A,B) = high. [assumption]. greater(high,mod1). [assumption]. greater(mod1,low). [assumption]. greater(low,very_low). [assumption]. greater(high,mod2). [assumption]. greater(mod2,low). [assumption]. greater(mod2,mod1). [assumption]. greater(sigma,zero). [assumption]. greater(tau,zero). [assumption]. smaller(sigma,tau). [assumption]. organization(c1). [assumption]. robust_position(c1). [assumption]. -has_endowment(c1). [assumption]. greater(age(c1,c2),tau). [assumption]. smaller_or_equal(age(c1,c3),sigma). [assumption]. greater(age(c1,c4),sigma). [assumption]. smaller_or_equal(age(c1,c4),tau). [assumption]. -smaller(hazard_of_mortality(c1,c3),hazard_of_mortality(c1,c4)). [assumption]. age(c1,c5) = zero. [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= Eliminating greater_or_equal/2 1 greater(A,B) | B = A | -greater_or_equal(A,B). [assumption]. 2 greater_or_equal(A,B) | -greater(A,B). [assumption]. 3 greater_or_equal(A,B) | B != A. [assumption]. Eliminating organization/1 4 organization(A) | -has_endowment(A). [assumption]. 5 has_endowment(A) | -organization(A) | smaller_or_equal(age(A,f1(A)),eta) | greater(age(A,f2(A)),eta). [assumption]. 6 has_endowment(A) | -organization(A) | smaller_or_equal(age(A,f1(A)),eta) | has_immunity(A,f2(A)). [assumption]. 7 has_endowment(A) | -organization(A) | -has_immunity(A,f1(A)) | greater(age(A,f2(A)),eta). [assumption]. 8 has_endowment(A) | -organization(A) | -has_immunity(A,f1(A)) | has_immunity(A,f2(A)). [assumption]. 9 -smaller_or_equal(age(A,B),eta) | has_immunity(A,B) | -organization(A) | smaller_or_equal(age(A,f3(A)),eta) | greater(age(A,f4(A)),eta). [assumption]. Derived: -smaller_or_equal(age(A,B),eta) | has_immunity(A,B) | smaller_or_equal(age(A,f3(A)),eta) | greater(age(A,f4(A)),eta) | -has_endowment(A). [resolve(9,c,4,a)]. 10 -smaller_or_equal(age(A,B),eta) | has_immunity(A,B) | -organization(A) | smaller_or_equal(age(A,f3(A)),eta) | has_immunity(A,f4(A)). [assumption]. Derived: -smaller_or_equal(age(A,B),eta) | has_immunity(A,B) | smaller_or_equal(age(A,f3(A)),eta) | has_immunity(A,f4(A)) | -has_endowment(A). [resolve(10,c,4,a)]. 11 -smaller_or_equal(age(A,B),eta) | has_immunity(A,B) | -organization(A) | -has_immunity(A,f3(A)) | greater(age(A,f4(A)),eta). [assumption]. Derived: -smaller_or_equal(age(A,B),eta) | has_immunity(A,B) | -has_immunity(A,f3(A)) | greater(age(A,f4(A)),eta) | -has_endowment(A). [resolve(11,c,4,a)]. 12 -smaller_or_equal(age(A,B),eta) | has_immunity(A,B) | -organization(A) | -has_immunity(A,f3(A)) | has_immunity(A,f4(A)). [assumption]. Derived: -smaller_or_equal(age(A,B),eta) | has_immunity(A,B) | -has_immunity(A,f3(A)) | has_immunity(A,f4(A)) | -has_endowment(A). [resolve(12,c,4,a)]. 13 -greater(age(A,B),eta) | -has_immunity(A,B) | -organization(A) | smaller_or_equal(age(A,f5(A)),eta) | greater(age(A,f6(A)),eta). [assumption]. Derived: -greater(age(A,B),eta) | -has_immunity(A,B) | smaller_or_equal(age(A,f5(A)),eta) | greater(age(A,f6(A)),eta) | -has_endowment(A). [resolve(13,c,4,a)]. 14 -greater(age(A,B),eta) | -has_immunity(A,B) | -organization(A) | smaller_or_equal(age(A,f5(A)),eta) | has_immunity(A,f6(A)). [assumption]. Derived: -greater(age(A,B),eta) | -has_immunity(A,B) | smaller_or_equal(age(A,f5(A)),eta) | has_immunity(A,f6(A)) | -has_endowment(A). [resolve(14,c,4,a)]. 15 -greater(age(A,B),eta) | -has_immunity(A,B) | -organization(A) | -has_immunity(A,f5(A)) | greater(age(A,f6(A)),eta). [assumption]. Derived: -greater(age(A,B),eta) | -has_immunity(A,B) | -has_immunity(A,f5(A)) | greater(age(A,f6(A)),eta) | -has_endowment(A). [resolve(15,c,4,a)]. 16 -greater(age(A,B),eta) | -has_immunity(A,B) | -organization(A) | -has_immunity(A,f5(A)) | has_immunity(A,f6(A)). [assumption]. Derived: -greater(age(A,B),eta) | -has_immunity(A,B) | -has_immunity(A,f5(A)) | has_immunity(A,f6(A)) | -has_endowment(A). [resolve(16,c,4,a)]. 17 -organization(A) | has_endowment(A) | -has_immunity(A,B). [assumption]. 18 -organization(A) | is_aligned(A,B) | dissimilar(A,B,C) | -is_aligned(A,C). [assumption]. Derived: is_aligned(A,B) | dissimilar(A,B,C) | -is_aligned(A,C) | -has_endowment(A). [resolve(18,a,4,a)]. 19 -organization(A) | -is_aligned(A,B) | dissimilar(A,B,C) | is_aligned(A,C). [assumption]. Derived: -is_aligned(A,B) | dissimilar(A,B,C) | is_aligned(A,C) | -has_endowment(A). [resolve(19,a,4,a)]. 20 organization(A) | -dissimilar(A,B,C). [assumption]. Derived: -dissimilar(A,B,C) | has_endowment(A) | smaller_or_equal(age(A,f1(A)),eta) | greater(age(A,f2(A)),eta). [resolve(20,a,5,b)]. Derived: -dissimilar(A,B,C) | has_endowment(A) | smaller_or_equal(age(A,f1(A)),eta) | has_immunity(A,f2(A)). [resolve(20,a,6,b)]. Derived: -dissimilar(A,B,C) | has_endowment(A) | -has_immunity(A,f1(A)) | greater(age(A,f2(A)),eta). [resolve(20,a,7,b)]. Derived: -dissimilar(A,B,C) | has_endowment(A) | -has_immunity(A,f1(A)) | has_immunity(A,f2(A)). [resolve(20,a,8,b)]. Derived: -dissimilar(A,B,C) | -smaller_or_equal(age(A,D),eta) | has_immunity(A,D) | smaller_or_equal(age(A,f3(A)),eta) | greater(age(A,f4(A)),eta). [resolve(20,a,9,c)]. Derived: -dissimilar(A,B,C) | -smaller_or_equal(age(A,D),eta) | has_immunity(A,D) | smaller_or_equal(age(A,f3(A)),eta) | has_immunity(A,f4(A)). [resolve(20,a,10,c)]. Derived: -dissimilar(A,B,C) | -smaller_or_equal(age(A,D),eta) | has_immunity(A,D) | -has_immunity(A,f3(A)) | greater(age(A,f4(A)),eta). [resolve(20,a,11,c)]. Derived: -dissimilar(A,B,C) | -smaller_or_equal(age(A,D),eta) | has_immunity(A,D) | -has_immunity(A,f3(A)) | has_immunity(A,f4(A)). [resolve(20,a,12,c)]. Derived: -dissimilar(A,B,C) | -greater(age(A,D),eta) | -has_immunity(A,D) | smaller_or_equal(age(A,f5(A)),eta) | greater(age(A,f6(A)),eta). [resolve(20,a,13,c)]. Derived: -dissimilar(A,B,C) | -greater(age(A,D),eta) | -has_immunity(A,D) | smaller_or_equal(age(A,f5(A)),eta) | has_immunity(A,f6(A)). [resolve(20,a,14,c)]. Derived: -dissimilar(A,B,C) | -greater(age(A,D),eta) | -has_immunity(A,D) | -has_immunity(A,f5(A)) | greater(age(A,f6(A)),eta). [resolve(20,a,15,c)]. Derived: -dissimilar(A,B,C) | -greater(age(A,D),eta) | -has_immunity(A,D) | -has_immunity(A,f5(A)) | has_immunity(A,f6(A)). [resolve(20,a,16,c)]. Derived: -dissimilar(A,B,C) | has_endowment(A) | -has_immunity(A,D). [resolve(20,a,17,a)]. Derived: -dissimilar(A,B,C) | is_aligned(A,D) | dissimilar(A,D,E) | -is_aligned(A,E). [resolve(20,a,18,a)]. Derived: -dissimilar(A,B,C) | -is_aligned(A,D) | dissimilar(A,D,E) | is_aligned(A,E). [resolve(20,a,19,a)]. 21 -organization(A) | age(A,B) != zero | is_aligned(A,B). [assumption]. Derived: age(A,B) != zero | is_aligned(A,B) | -has_endowment(A). [resolve(21,a,4,a)]. Derived: age(A,B) != zero | is_aligned(A,B) | -dissimilar(A,C,D). [resolve(21,a,20,a)]. 22 -organization(A) | age(A,B) != zero | greater(age(A,C),sigma) | -dissimilar(A,B,C). [assumption]. Derived: age(A,B) != zero | greater(age(A,C),sigma) | -dissimilar(A,B,C) | -has_endowment(A). [resolve(22,a,4,a)]. Derived: age(A,B) != zero | greater(age(A,C),sigma) | -dissimilar(A,B,C) | -dissimilar(A,D,E). [resolve(22,a,20,a)]. 23 -organization(A) | age(A,B) != zero | dissimilar(A,B,C) | -greater(age(A,C),sigma). [assumption]. Derived: age(A,B) != zero | dissimilar(A,B,C) | -greater(age(A,C),sigma) | -has_endowment(A). [resolve(23,a,4,a)]. Derived: age(A,B) != zero | dissimilar(A,B,C) | -greater(age(A,C),sigma) | -dissimilar(A,D,E). [resolve(23,a,20,a)]. 24 -organization(A) | -has_immunity(A,B) | hazard_of_mortality(A,B) = very_low. [assumption]. Derived: -has_immunity(A,B) | hazard_of_mortality(A,B) = very_low | -has_endowment(A). [resolve(24,a,4,a)]. Derived: -has_immunity(A,B) | hazard_of_mortality(A,B) = very_low | -dissimilar(A,C,D). [resolve(24,a,20,a)]. 25 -organization(A) | has_immunity(A,B) | -is_aligned(A,B) | -positional_advantage(A,B) | hazard_of_mortality(A,B) = low. [assumption]. Derived: has_immunity(A,B) | -is_aligned(A,B) | -positional_advantage(A,B) | hazard_of_mortality(A,B) = low | -has_endowment(A). [resolve(25,a,4,a)]. Derived: has_immunity(A,B) | -is_aligned(A,B) | -positional_advantage(A,B) | hazard_of_mortality(A,B) = low | -dissimilar(A,C,D). [resolve(25,a,20,a)]. 26 -organization(A) | has_immunity(A,B) | is_aligned(A,B) | -positional_advantage(A,B) | hazard_of_mortality(A,B) = mod1. [assumption]. Derived: has_immunity(A,B) | is_aligned(A,B) | -positional_advantage(A,B) | hazard_of_mortality(A,B) = mod1 | -has_endowment(A). [resolve(26,a,4,a)]. Derived: has_immunity(A,B) | is_aligned(A,B) | -positional_advantage(A,B) | hazard_of_mortality(A,B) = mod1 | -dissimilar(A,C,D). [resolve(26,a,20,a)]. 27 -organization(A) | has_immunity(A,B) | -is_aligned(A,B) | positional_advantage(A,B) | hazard_of_mortality(A,B) = mod2. [assumption]. Derived: has_immunity(A,B) | -is_aligned(A,B) | positional_advantage(A,B) | hazard_of_mortality(A,B) = mod2 | -has_endowment(A). [resolve(27,a,4,a)]. Derived: has_immunity(A,B) | -is_aligned(A,B) | positional_advantage(A,B) | hazard_of_mortality(A,B) = mod2 | -dissimilar(A,C,D). [resolve(27,a,20,a)]. 28 -organization(A) | has_immunity(A,B) | is_aligned(A,B) | positional_advantage(A,B) | hazard_of_mortality(A,B) = high. [assumption]. Derived: has_immunity(A,B) | is_aligned(A,B) | positional_advantage(A,B) | hazard_of_mortality(A,B) = high | -has_endowment(A). [resolve(28,a,4,a)]. Derived: has_immunity(A,B) | is_aligned(A,B) | positional_advantage(A,B) | hazard_of_mortality(A,B) = high | -dissimilar(A,C,D). [resolve(28,a,20,a)]. 29 organization(c1). [assumption]. Derived: has_endowment(c1) | smaller_or_equal(age(c1,f1(c1)),eta) | greater(age(c1,f2(c1)),eta). [resolve(29,a,5,b)]. Derived: has_endowment(c1) | smaller_or_equal(age(c1,f1(c1)),eta) | has_immunity(c1,f2(c1)). [resolve(29,a,6,b)]. Derived: has_endowment(c1) | -has_immunity(c1,f1(c1)) | greater(age(c1,f2(c1)),eta). [resolve(29,a,7,b)]. Derived: has_endowment(c1) | -has_immunity(c1,f1(c1)) | has_immunity(c1,f2(c1)). [resolve(29,a,8,b)]. Derived: -smaller_or_equal(age(c1,A),eta) | has_immunity(c1,A) | smaller_or_equal(age(c1,f3(c1)),eta) | greater(age(c1,f4(c1)),eta). [resolve(29,a,9,c)]. Derived: -smaller_or_equal(age(c1,A),eta) | has_immunity(c1,A) | smaller_or_equal(age(c1,f3(c1)),eta) | has_immunity(c1,f4(c1)). [resolve(29,a,10,c)]. Derived: -smaller_or_equal(age(c1,A),eta) | has_immunity(c1,A) | -has_immunity(c1,f3(c1)) | greater(age(c1,f4(c1)),eta). [resolve(29,a,11,c)]. Derived: -smaller_or_equal(age(c1,A),eta) | has_immunity(c1,A) | -has_immunity(c1,f3(c1)) | has_immunity(c1,f4(c1)). [resolve(29,a,12,c)]. Derived: -greater(age(c1,A),eta) | -has_immunity(c1,A) | smaller_or_equal(age(c1,f5(c1)),eta) | greater(age(c1,f6(c1)),eta). [resolve(29,a,13,c)]. Derived: -greater(age(c1,A),eta) | -has_immunity(c1,A) | smaller_or_equal(age(c1,f5(c1)),eta) | has_immunity(c1,f6(c1)). [resolve(29,a,14,c)]. Derived: -greater(age(c1,A),eta) | -has_immunity(c1,A) | -has_immunity(c1,f5(c1)) | greater(age(c1,f6(c1)),eta). [resolve(29,a,15,c)]. Derived: -greater(age(c1,A),eta) | -has_immunity(c1,A) | -has_immunity(c1,f5(c1)) | has_immunity(c1,f6(c1)). [resolve(29,a,16,c)]. Derived: has_endowment(c1) | -has_immunity(c1,A). [resolve(29,a,17,a)]. Derived: is_aligned(c1,A) | dissimilar(c1,A,B) | -is_aligned(c1,B). [resolve(29,a,18,a)]. Derived: -is_aligned(c1,A) | dissimilar(c1,A,B) | is_aligned(c1,B). [resolve(29,a,19,a)]. Derived: age(c1,A) != zero | is_aligned(c1,A). [resolve(29,a,21,a)]. Derived: age(c1,A) != zero | dissimilar(c1,A,B) | -greater(age(c1,B),sigma). [resolve(29,a,23,a)]. Derived: -has_immunity(c1,A) | hazard_of_mortality(c1,A) = very_low. [resolve(29,a,24,a)]. Derived: has_immunity(c1,A) | -is_aligned(c1,A) | -positional_advantage(c1,A) | hazard_of_mortality(c1,A) = low. [resolve(29,a,25,a)]. Derived: has_immunity(c1,A) | is_aligned(c1,A) | -positional_advantage(c1,A) | hazard_of_mortality(c1,A) = mod1. [resolve(29,a,26,a)]. Derived: has_immunity(c1,A) | -is_aligned(c1,A) | positional_advantage(c1,A) | hazard_of_mortality(c1,A) = mod2. [resolve(29,a,27,a)]. Derived: has_immunity(c1,A) | is_aligned(c1,A) | positional_advantage(c1,A) | hazard_of_mortality(c1,A) = high. [resolve(29,a,28,a)]. Eliminating robust_position/1 30 -smaller_or_equal(age(A,B),tau) | -positional_advantage(A,B) | -robust_position(A). [assumption]. 31 robust_position(A) | smaller_or_equal(age(A,f7(A)),tau) | greater(age(A,f8(A)),tau). [assumption]. 32 robust_position(A) | smaller_or_equal(age(A,f7(A)),tau) | -positional_advantage(A,f8(A)). [assumption]. 33 robust_position(A) | positional_advantage(A,f7(A)) | greater(age(A,f8(A)),tau). [assumption]. 34 robust_position(A) | positional_advantage(A,f7(A)) | -positional_advantage(A,f8(A)). [assumption]. Derived: -smaller_or_equal(age(A,B),tau) | -positional_advantage(A,B) | smaller_or_equal(age(A,f7(A)),tau) | greater(age(A,f8(A)),tau). [resolve(30,c,31,a)]. Derived: -smaller_or_equal(age(A,B),tau) | -positional_advantage(A,B) | smaller_or_equal(age(A,f7(A)),tau) | -positional_advantage(A,f8(A)). [resolve(30,c,32,a)]. Derived: -smaller_or_equal(age(A,B),tau) | -positional_advantage(A,B) | positional_advantage(A,f7(A)) | greater(age(A,f8(A)),tau). [resolve(30,c,33,a)]. Derived: -smaller_or_equal(age(A,B),tau) | -positional_advantage(A,B) | positional_advantage(A,f7(A)) | -positional_advantage(A,f8(A)). [resolve(30,c,34,a)]. 35 -greater(age(A,B),tau) | positional_advantage(A,B) | -robust_position(A). [assumption]. Derived: -greater(age(A,B),tau) | positional_advantage(A,B) | smaller_or_equal(age(A,f7(A)),tau) | greater(age(A,f8(A)),tau). [resolve(35,c,31,a)]. Derived: -greater(age(A,B),tau) | positional_advantage(A,B) | smaller_or_equal(age(A,f7(A)),tau) | -positional_advantage(A,f8(A)). [resolve(35,c,32,a)]. Derived: -greater(age(A,B),tau) | positional_advantage(A,B) | positional_advantage(A,f7(A)) | greater(age(A,f8(A)),tau). [resolve(35,c,33,a)]. Derived: -greater(age(A,B),tau) | positional_advantage(A,B) | positional_advantage(A,f7(A)) | -positional_advantage(A,f8(A)). [resolve(35,c,34,a)]. 36 robust_position(c1). [assumption]. Derived: -smaller_or_equal(age(c1,A),tau) | -positional_advantage(c1,A). [resolve(36,a,30,c)]. Derived: -greater(age(c1,A),tau) | positional_advantage(c1,A). [resolve(36,a,35,c)]. ============================== end predicate elimination ============= Term ordering decisions: Relation symbol precedence: lex([ has_endowment, has_immunity, greater, smaller_or_equal, positional_advantage, is_aligned, smaller, dissimilar, =, robust_position, organization, greater_or_equal ]). Function symbol precedence: lex([ eta, tau, zero, sigma, low, mod1, mod2, high, very_low, c1, c2, c3, c4, c5, age, hazard_of_mortality, f1, f2, f3, f4, f5, f6, f7, f8, f9, f10, f11, f12 ]). 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). 37 smaller_or_equal(A,B) | -smaller(A,B). [assumption]. 38 smaller_or_equal(A,B) | B != A. [assumption]. 39 smaller(A,B) | B = A | -smaller_or_equal(A,B). [assumption]. 40 smaller(A,B) | -greater(B,A). [assumption]. 41 greater(A,B) | -smaller(B,A). [assumption]. 42 -greater(A,B) | -greater(B,A). [assumption]. 43 -greater(A,B) | -greater(B,C) | greater(A,C). [assumption]. 44 smaller(A,B) | B = A | greater(A,B). [assumption]. 45 -smaller_or_equal(age(A,B),eta) | has_immunity(A,B) | -has_endowment(A). [assumption]. 46 -greater(age(A,B),eta) | -has_immunity(A,B) | -has_endowment(A). [assumption]. 47 is_aligned(A,B) | is_aligned(A,C) | -dissimilar(A,B,C). [assumption]. 48 -is_aligned(A,B) | -is_aligned(A,C) | -dissimilar(A,B,C). [assumption]. 49 -smaller_or_equal(age(A,B),tau) | -positional_advantage(A,B) | smaller_or_equal(age(A,f9(A)),tau) | greater(age(A,f10(A)),tau). [assumption]. 50 -smaller_or_equal(age(A,B),tau) | -positional_advantage(A,B) | smaller_or_equal(age(A,f9(A)),tau) | -positional_advantage(A,f10(A)). [assumption]. 51 -smaller_or_equal(age(A,B),tau) | -positional_advantage(A,B) | positional_advantage(A,f9(A)) | greater(age(A,f10(A)),tau). [assumption]. 52 -smaller_or_equal(age(A,B),tau) | -positional_advantage(A,B) | positional_advantage(A,f9(A)) | -positional_advantage(A,f10(A)). [assumption]. 53 -greater(age(A,B),tau) | positional_advantage(A,B) | smaller_or_equal(age(A,f11(A)),tau) | greater(age(A,f12(A)),tau). [assumption]. 54 -greater(age(A,B),tau) | positional_advantage(A,B) | smaller_or_equal(age(A,f11(A)),tau) | -positional_advantage(A,f12(A)). [assumption]. 55 -greater(age(A,B),tau) | positional_advantage(A,B) | positional_advantage(A,f11(A)) | greater(age(A,f12(A)),tau). [assumption]. 56 -greater(age(A,B),tau) | positional_advantage(A,B) | positional_advantage(A,f11(A)) | -positional_advantage(A,f12(A)). [assumption]. 57 greater(high,mod1). [assumption]. 58 greater(mod1,low). [assumption]. 59 greater(low,very_low). [assumption]. 60 greater(high,mod2). [assumption]. 61 greater(mod2,low). [assumption]. 62 greater(mod2,mod1). [assumption]. 63 greater(sigma,zero). [assumption]. 64 greater(tau,zero). [assumption]. 65 smaller(sigma,tau). [assumption]. 66 -has_endowment(c1). [assumption]. 67 greater(age(c1,c2),tau). [assumption]. 68 smaller_or_equal(age(c1,c3),sigma). [assumption]. 69 greater(age(c1,c4),sigma). [assumption]. 70 smaller_or_equal(age(c1,c4),tau). [assumption]. 71 -smaller(hazard_of_mortality(c1,c3),hazard_of_mortality(c1,c4)). [assumption]. 72 age(c1,c5) = zero. [assumption]. 73 is_aligned(A,B) | dissimilar(A,B,C) | -is_aligned(A,C) | -has_endowment(A). [resolve(18,a,4,a)]. 74 -is_aligned(A,B) | dissimilar(A,B,C) | is_aligned(A,C) | -has_endowment(A). [resolve(19,a,4,a)]. 75 -dissimilar(A,B,C) | has_endowment(A) | smaller_or_equal(age(A,f1(A)),eta) | greater(age(A,f2(A)),eta). [resolve(20,a,5,b)]. 76 -dissimilar(A,B,C) | has_endowment(A) | smaller_or_equal(age(A,f1(A)),eta) | has_immunity(A,f2(A)). [resolve(20,a,6,b)]. 79 -dissimilar(A,B,C) | -smaller_or_equal(age(A,D),eta) | has_immunity(A,D) | smaller_or_equal(age(A,f3(A)),eta) | greater(age(A,f4(A)),eta). [resolve(20,a,9,c)]. 80 -dissimilar(A,B,C) | -smaller_or_equal(age(A,D),eta) | has_immunity(A,D) | smaller_or_equal(age(A,f3(A)),eta) | has_immunity(A,f4(A)). [resolve(20,a,10,c)]. 81 -dissimilar(A,B,C) | -smaller_or_equal(age(A,D),eta) | has_immunity(A,D) | -has_immunity(A,f3(A)) | greater(age(A,f4(A)),eta). [resolve(20,a,11,c)]. 82 -dissimilar(A,B,C) | -smaller_or_equal(age(A,D),eta) | has_immunity(A,D) | -has_immunity(A,f3(A)) | has_immunity(A,f4(A)). [resolve(20,a,12,c)]. 83 -dissimilar(A,B,C) | -greater(age(A,D),eta) | -has_immunity(A,D) | smaller_or_equal(age(A,f5(A)),eta) | greater(age(A,f6(A)),eta). [resolve(20,a,13,c)]. 84 -dissimilar(A,B,C) | -greater(age(A,D),eta) | -has_immunity(A,D) | smaller_or_equal(age(A,f5(A)),eta) | has_immunity(A,f6(A)). [resolve(20,a,14,c)]. 85 -dissimilar(A,B,C) | -greater(age(A,D),eta) | -has_immunity(A,D) | -has_immunity(A,f5(A)) | greater(age(A,f6(A)),eta). [resolve(20,a,15,c)]. 86 -dissimilar(A,B,C) | -greater(age(A,D),eta) | -has_immunity(A,D) | -has_immunity(A,f5(A)) | has_immunity(A,f6(A)). [resolve(20,a,16,c)]. 87 -dissimilar(A,B,C) | has_endowment(A) | -has_immunity(A,D). [resolve(20,a,17,a)]. 88 -dissimilar(A,B,C) | is_aligned(A,D) | dissimilar(A,D,E) | -is_aligned(A,E). [resolve(20,a,18,a)]. 89 -dissimilar(A,B,C) | -is_aligned(A,D) | dissimilar(A,D,E) | is_aligned(A,E). [resolve(20,a,19,a)]. 90 age(A,B) != zero | is_aligned(A,B) | -has_endowment(A). [resolve(21,a,4,a)]. 91 age(A,B) != zero | is_aligned(A,B) | -dissimilar(A,C,D). [resolve(21,a,20,a)]. 94 age(A,B) != zero | dissimilar(A,B,C) | -greater(age(A,C),sigma) | -has_endowment(A). [resolve(23,a,4,a)]. 95 age(A,B) != zero | dissimilar(A,B,C) | -greater(age(A,C),sigma) | -dissimilar(A,D,E). [resolve(23,a,20,a)]. 96 -has_immunity(A,B) | hazard_of_mortality(A,B) = very_low | -has_endowment(A). [resolve(24,a,4,a)]. 97 -has_immunity(A,B) | hazard_of_mortality(A,B) = very_low | -dissimilar(A,C,D). [resolve(24,a,20,a)]. 98 has_immunity(A,B) | -is_aligned(A,B) | -positional_advantage(A,B) | hazard_of_mortality(A,B) = low | -has_endowment(A). [resolve(25,a,4,a)]. 99 has_immunity(A,B) | -is_aligned(A,B) | -positional_advantage(A,B) | hazard_of_mortality(A,B) = low | -dissimilar(A,C,D). [resolve(25,a,20,a)]. 100 has_immunity(A,B) | is_aligned(A,B) | -positional_advantage(A,B) | hazard_of_mortality(A,B) = mod1 | -has_endowment(A). [resolve(26,a,4,a)]. 101 has_immunity(A,B) | is_aligned(A,B) | -positional_advantage(A,B) | hazard_of_mortality(A,B) = mod1 | -dissimilar(A,C,D). [resolve(26,a,20,a)]. 102 has_immunity(A,B) | -is_aligned(A,B) | positional_advantage(A,B) | hazard_of_mortality(A,B) = mod2 | -has_endowment(A). [resolve(27,a,4,a)]. 103 has_immunity(A,B) | -is_aligned(A,B) | positional_advantage(A,B) | hazard_of_mortality(A,B) = mod2 | -dissimilar(A,C,D). [resolve(27,a,20,a)]. 104 has_immunity(A,B) | is_aligned(A,B) | positional_advantage(A,B) | hazard_of_mortality(A,B) = high | -has_endowment(A). [resolve(28,a,4,a)]. 105 has_immunity(A,B) | is_aligned(A,B) | positional_advantage(A,B) | hazard_of_mortality(A,B) = high | -dissimilar(A,C,D). [resolve(28,a,20,a)]. 123 -has_immunity(c1,A). [copy(122),unit_del(a,66)]. 124 is_aligned(c1,A) | dissimilar(c1,A,B) | -is_aligned(c1,B). [resolve(29,a,18,a)]. 125 -is_aligned(c1,A) | dissimilar(c1,A,B) | is_aligned(c1,B). [resolve(29,a,19,a)]. 126 age(c1,A) != zero | is_aligned(c1,A). [resolve(29,a,21,a)]. 127 age(c1,A) != zero | dissimilar(c1,A,B) | -greater(age(c1,B),sigma). [resolve(29,a,23,a)]. 129 -is_aligned(c1,A) | -positional_advantage(c1,A) | hazard_of_mortality(c1,A) = low. [copy(128),unit_del(a,123)]. 131 is_aligned(c1,A) | -positional_advantage(c1,A) | hazard_of_mortality(c1,A) = mod1. [copy(130),unit_del(a,123)]. 133 -is_aligned(c1,A) | positional_advantage(c1,A) | hazard_of_mortality(c1,A) = mod2. [copy(132),unit_del(a,123)]. 135 is_aligned(c1,A) | positional_advantage(c1,A) | hazard_of_mortality(c1,A) = high. [copy(134),unit_del(a,123)]. 136 -smaller_or_equal(age(A,B),tau) | -positional_advantage(A,B) | smaller_or_equal(age(A,f7(A)),tau) | greater(age(A,f8(A)),tau). [resolve(30,c,31,a)]. 137 -smaller_or_equal(age(A,B),tau) | -positional_advantage(A,B) | smaller_or_equal(age(A,f7(A)),tau) | -positional_advantage(A,f8(A)). [resolve(30,c,32,a)]. 138 -smaller_or_equal(age(A,B),tau) | -positional_advantage(A,B) | positional_advantage(A,f7(A)) | greater(age(A,f8(A)),tau). [resolve(30,c,33,a)]. 139 -smaller_or_equal(age(A,B),tau) | -positional_advantage(A,B) | positional_advantage(A,f7(A)) | -positional_advantage(A,f8(A)). [resolve(30,c,34,a)]. 140 -greater(age(A,B),tau) | positional_advantage(A,B) | smaller_or_equal(age(A,f7(A)),tau) | greater(age(A,f8(A)),tau). [resolve(35,c,31,a)]. 141 -greater(age(A,B),tau) | positional_advantage(A,B) | smaller_or_equal(age(A,f7(A)),tau) | -positional_advantage(A,f8(A)). [resolve(35,c,32,a)]. 142 -greater(age(A,B),tau) | positional_advantage(A,B) | positional_advantage(A,f7(A)) | greater(age(A,f8(A)),tau). [resolve(35,c,33,a)]. 143 -greater(age(A,B),tau) | positional_advantage(A,B) | positional_advantage(A,f7(A)) | -positional_advantage(A,f8(A)). [resolve(35,c,34,a)]. 144 -smaller_or_equal(age(c1,A),tau) | -positional_advantage(c1,A). [resolve(36,a,30,c)]. 145 -greater(age(c1,A),tau) | positional_advantage(c1,A). [resolve(36,a,35,c)]. 146 -greater(A,A). [factor(42,a,b)]. 147 is_aligned(A,B) | -dissimilar(A,B,B). [factor(47,a,b)]. 148 -is_aligned(A,B) | -dissimilar(A,B,B). [factor(48,a,b)]. 149 -smaller_or_equal(age(A,f10(A)),tau) | -positional_advantage(A,f10(A)) | smaller_or_equal(age(A,f9(A)),tau). [factor(50,b,d)]. 150 -smaller_or_equal(age(A,f10(A)),tau) | -positional_advantage(A,f10(A)) | positional_advantage(A,f9(A)). [factor(52,b,d)]. 151 -greater(age(A,f11(A)),tau) | positional_advantage(A,f11(A)) | greater(age(A,f12(A)),tau). [factor(55,b,c)]. 152 -greater(age(A,f11(A)),tau) | positional_advantage(A,f11(A)) | -positional_advantage(A,f12(A)). [factor(56,b,c)]. 153 -dissimilar(A,B,C) | -smaller_or_equal(age(A,f4(A)),eta) | has_immunity(A,f4(A)) | smaller_or_equal(age(A,f3(A)),eta). [factor(80,c,e)]. 154 -dissimilar(A,B,C) | -smaller_or_equal(age(A,f4(A)),eta) | has_immunity(A,f4(A)) | -has_immunity(A,f3(A)). [factor(82,c,e)]. 155 -dissimilar(A,B,C) | -greater(age(A,f5(A)),eta) | -has_immunity(A,f5(A)) | greater(age(A,f6(A)),eta). [factor(85,c,d)]. 156 -dissimilar(A,B,C) | -greater(age(A,f5(A)),eta) | -has_immunity(A,f5(A)) | has_immunity(A,f6(A)). [factor(86,c,d)]. 157 age(A,B) != zero | greater(age(A,C),sigma) | -dissimilar(A,B,C). [factor(93,c,d)]. 159 -smaller_or_equal(age(c1,A),eta) | smaller_or_equal(age(c1,f3(c1)),eta). [back_unit_del(115),unit_del(b,123),unit_del(d,123)]. 160 smaller_or_equal(age(c1,f1(c1)),eta). [back_unit_del(109),unit_del(b,123)]. 161 -smaller_or_equal(age(A,f8(A)),tau) | -positional_advantage(A,f8(A)) | smaller_or_equal(age(A,f7(A)),tau). [factor(137,b,d)]. 162 -smaller_or_equal(age(A,f8(A)),tau) | -positional_advantage(A,f8(A)) | positional_advantage(A,f7(A)). [factor(139,b,d)]. 163 -greater(age(A,f7(A)),tau) | positional_advantage(A,f7(A)) | greater(age(A,f8(A)),tau). [factor(142,b,c)]. 164 -greater(age(A,f7(A)),tau) | positional_advantage(A,f7(A)) | -positional_advantage(A,f8(A)). [factor(143,b,c)]. end_of_list. formulas(demodulators). 72 age(c1,c5) = zero. [assumption]. end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.02 seconds. given #1 (I,wt=6): 37 smaller_or_equal(A,B) | -smaller(A,B). [assumption]. given #2 (I,wt=6): 38 smaller_or_equal(A,B) | B != A. [assumption]. given #3 (I,wt=9): 39 smaller(A,B) | B = A | -smaller_or_equal(A,B). [assumption]. given #4 (I,wt=6): 40 smaller(A,B) | -greater(B,A). [assumption]. given #5 (I,wt=6): 41 greater(A,B) | -smaller(B,A). [assumption]. given #6 (I,wt=6): 42 -greater(A,B) | -greater(B,A). [assumption]. given #7 (I,wt=9): 43 -greater(A,B) | -greater(B,C) | greater(A,C). [assumption]. given #8 (I,wt=9): 44 smaller(A,B) | B = A | greater(A,B). [assumption]. given #9 (I,wt=10): 45 -smaller_or_equal(age(A,B),eta) | has_immunity(A,B) | -has_endowment(A). [assumption]. given #10 (I,wt=10): 46 -greater(age(A,B),eta) | -has_immunity(A,B) | -has_endowment(A). [assumption]. given #11 (I,wt=10): 47 is_aligned(A,B) | is_aligned(A,C) | -dissimilar(A,B,C). [assumption]. given #12 (I,wt=10): 48 -is_aligned(A,B) | -is_aligned(A,C) | -dissimilar(A,B,C). [assumption]. given #13 (I,wt=20): 49 -smaller_or_equal(age(A,B),tau) | -positional_advantage(A,B) | smaller_or_equal(age(A,f9(A)),tau) | greater(age(A,f10(A)),tau). [assumption]. given #14 (I,wt=18): 50 -smaller_or_equal(age(A,B),tau) | -positional_advantage(A,B) | smaller_or_equal(age(A,f9(A)),tau) | -positional_advantage(A,f10(A)). [assumption]. given #15 (I,wt=18): 51 -smaller_or_equal(age(A,B),tau) | -positional_advantage(A,B) | positional_advantage(A,f9(A)) | greater(age(A,f10(A)),tau). [assumption]. given #16 (I,wt=16): 52 -smaller_or_equal(age(A,B),tau) | -positional_advantage(A,B) | positional_advantage(A,f9(A)) | -positional_advantage(A,f10(A)). [assumption]. given #17 (I,wt=20): 53 -greater(age(A,B),tau) | positional_advantage(A,B) | smaller_or_equal(age(A,f11(A)),tau) | greater(age(A,f12(A)),tau). [assumption]. given #18 (I,wt=18): 54 -greater(age(A,B),tau) | positional_advantage(A,B) | smaller_or_equal(age(A,f11(A)),tau) | -positional_advantage(A,f12(A)). [assumption]. given #19 (I,wt=18): 55 -greater(age(A,B),tau) | positional_advantage(A,B) | positional_advantage(A,f11(A)) | greater(age(A,f12(A)),tau). [assumption]. given #20 (I,wt=16): 56 -greater(age(A,B),tau) | positional_advantage(A,B) | positional_advantage(A,f11(A)) | -positional_advantage(A,f12(A)). [assumption]. given #21 (I,wt=3): 57 greater(high,mod1). [assumption]. given #22 (I,wt=3): 58 greater(mod1,low). [assumption]. given #23 (I,wt=3): 59 greater(low,very_low). [assumption]. given #24 (I,wt=3): 60 greater(high,mod2). [assumption]. given #25 (I,wt=3): 61 greater(mod2,low). [assumption]. given #26 (I,wt=3): 62 greater(mod2,mod1). [assumption]. given #27 (I,wt=3): 63 greater(sigma,zero). [assumption]. given #28 (I,wt=3): 64 greater(tau,zero). [assumption]. given #29 (I,wt=3): 65 smaller(sigma,tau). [assumption]. given #30 (I,wt=2): 66 -has_endowment(c1). [assumption]. given #31 (I,wt=5): 67 greater(age(c1,c2),tau). [assumption]. given #32 (I,wt=5): 68 smaller_or_equal(age(c1,c3),sigma). [assumption]. given #33 (I,wt=5): 69 greater(age(c1,c4),sigma). [assumption]. given #34 (I,wt=5): 70 smaller_or_equal(age(c1,c4),tau). [assumption]. given #35 (I,wt=7): 71 -smaller(hazard_of_mortality(c1,c3),hazard_of_mortality(c1,c4)). [assumption]. given #36 (I,wt=5): 72 age(c1,c5) = zero. [assumption]. given #37 (I,wt=12): 73 is_aligned(A,B) | dissimilar(A,B,C) | -is_aligned(A,C) | -has_endowment(A). [resolve(18,a,4,a)]. given #38 (I,wt=12): 74 -is_aligned(A,B) | dissimilar(A,B,C) | is_aligned(A,C) | -has_endowment(A). [resolve(19,a,4,a)]. given #39 (I,wt=18): 75 -dissimilar(A,B,C) | has_endowment(A) | smaller_or_equal(age(A,f1(A)),eta) | greater(age(A,f2(A)),eta). [resolve(20,a,5,b)]. given #40 (I,wt=16): 76 -dissimilar(A,B,C) | has_endowment(A) | smaller_or_equal(age(A,f1(A)),eta) | has_immunity(A,f2(A)). [resolve(20,a,6,b)]. given #41 (I,wt=24): 79 -dissimilar(A,B,C) | -smaller_or_equal(age(A,D),eta) | has_immunity(A,D) | smaller_or_equal(age(A,f3(A)),eta) | greater(age(A,f4(A)),eta). [resolve(20,a,9,c)]. given #42 (I,wt=22): 80 -dissimilar(A,B,C) | -smaller_or_equal(age(A,D),eta) | has_immunity(A,D) | smaller_or_equal(age(A,f3(A)),eta) | has_immunity(A,f4(A)). [resolve(20,a,10,c)]. given #43 (I,wt=22): 81 -dissimilar(A,B,C) | -smaller_or_equal(age(A,D),eta) | has_immunity(A,D) | -has_immunity(A,f3(A)) | greater(age(A,f4(A)),eta). [resolve(20,a,11,c)]. given #44 (I,wt=20): 82 -dissimilar(A,B,C) | -smaller_or_equal(age(A,D),eta) | has_immunity(A,D) | -has_immunity(A,f3(A)) | has_immunity(A,f4(A)). [resolve(20,a,12,c)]. given #45 (I,wt=24): 83 -dissimilar(A,B,C) | -greater(age(A,D),eta) | -has_immunity(A,D) | smaller_or_equal(age(A,f5(A)),eta) | greater(age(A,f6(A)),eta). [resolve(20,a,13,c)]. given #46 (I,wt=22): 84 -dissimilar(A,B,C) | -greater(age(A,D),eta) | -has_immunity(A,D) | smaller_or_equal(age(A,f5(A)),eta) | has_immunity(A,f6(A)). [resolve(20,a,14,c)]. given #47 (I,wt=22): 85 -dissimilar(A,B,C) | -greater(age(A,D),eta) | -has_immunity(A,D) | -has_immunity(A,f5(A)) | greater(age(A,f6(A)),eta). [resolve(20,a,15,c)]. given #48 (I,wt=20): 86 -dissimilar(A,B,C) | -greater(age(A,D),eta) | -has_immunity(A,D) | -has_immunity(A,f5(A)) | has_immunity(A,f6(A)). [resolve(20,a,16,c)]. given #49 (I,wt=9): 87 -dissimilar(A,B,C) | has_endowment(A) | -has_immunity(A,D). [resolve(20,a,17,a)]. given #50 (I,wt=14): 88 -dissimilar(A,B,C) | is_aligned(A,D) | dissimilar(A,D,E) | -is_aligned(A,E). [resolve(20,a,18,a)]. given #51 (I,wt=14): 89 -dissimilar(A,B,C) | -is_aligned(A,D) | dissimilar(A,D,E) | is_aligned(A,E). [resolve(20,a,19,a)]. given #52 (I,wt=10): 90 age(A,B) != zero | is_aligned(A,B) | -has_endowment(A). [resolve(21,a,4,a)]. given #53 (I,wt=12): 91 age(A,B) != zero | is_aligned(A,B) | -dissimilar(A,C,D). [resolve(21,a,20,a)]. given #54 (I,wt=16): 94 age(A,B) != zero | dissimilar(A,B,C) | -greater(age(A,C),sigma) | -has_endowment(A). [resolve(23,a,4,a)]. given #55 (I,wt=18): 95 age(A,B) != zero | dissimilar(A,B,C) | -greater(age(A,C),sigma) | -dissimilar(A,D,E). [resolve(23,a,20,a)]. given #56 (I,wt=10): 96 -has_immunity(A,B) | hazard_of_mortality(A,B) = very_low | -has_endowment(A). [resolve(24,a,4,a)]. given #57 (I,wt=12): 97 -has_immunity(A,B) | hazard_of_mortality(A,B) = very_low | -dissimilar(A,C,D). [resolve(24,a,20,a)]. given #58 (I,wt=16): 98 has_immunity(A,B) | -is_aligned(A,B) | -positional_advantage(A,B) | hazard_of_mortality(A,B) = low | -has_endowment(A). [resolve(25,a,4,a)]. given #59 (I,wt=18): 99 has_immunity(A,B) | -is_aligned(A,B) | -positional_advantage(A,B) | hazard_of_mortality(A,B) = low | -dissimilar(A,C,D). [resolve(25,a,20,a)]. given #60 (I,wt=16): 100 has_immunity(A,B) | is_aligned(A,B) | -positional_advantage(A,B) | hazard_of_mortality(A,B) = mod1 | -has_endowment(A). [resolve(26,a,4,a)]. given #61 (I,wt=18): 101 has_immunity(A,B) | is_aligned(A,B) | -positional_advantage(A,B) | hazard_of_mortality(A,B) = mod1 | -dissimilar(A,C,D). [resolve(26,a,20,a)]. given #62 (I,wt=16): 102 has_immunity(A,B) | -is_aligned(A,B) | positional_advantage(A,B) | hazard_of_mortality(A,B) = mod2 | -has_endowment(A). [resolve(27,a,4,a)]. given #63 (I,wt=18): 103 has_immunity(A,B) | -is_aligned(A,B) | positional_advantage(A,B) | hazard_of_mortality(A,B) = mod2 | -dissimilar(A,C,D). [resolve(27,a,20,a)]. given #64 (I,wt=16): 104 has_immunity(A,B) | is_aligned(A,B) | positional_advantage(A,B) | hazard_of_mortality(A,B) = high | -has_endowment(A). [resolve(28,a,4,a)]. given #65 (I,wt=18): 105 has_immunity(A,B) | is_aligned(A,B) | positional_advantage(A,B) | hazard_of_mortality(A,B) = high | -dissimilar(A,C,D). [resolve(28,a,20,a)]. given #66 (I,wt=3): 123 -has_immunity(c1,A). [copy(122),unit_del(a,66)]. given #67 (I,wt=10): 124 is_aligned(c1,A) | dissimilar(c1,A,B) | -is_aligned(c1,B). [resolve(29,a,18,a)]. given #68 (I,wt=10): 125 -is_aligned(c1,A) | dissimilar(c1,A,B) | is_aligned(c1,B). [resolve(29,a,19,a)]. given #69 (I,wt=8): 126 age(c1,A) != zero | is_aligned(c1,A). [resolve(29,a,21,a)]. given #70 (I,wt=14): 127 age(c1,A) != zero | dissimilar(c1,A,B) | -greater(age(c1,B),sigma). [resolve(29,a,23,a)]. given #71 (I,wt=11): 129 -is_aligned(c1,A) | -positional_advantage(c1,A) | hazard_of_mortality(c1,A) = low. [copy(128),unit_del(a,123)]. given #72 (I,wt=11): 131 is_aligned(c1,A) | -positional_advantage(c1,A) | hazard_of_mortality(c1,A) = mod1. [copy(130),unit_del(a,123)]. given #73 (I,wt=11): 133 -is_aligned(c1,A) | positional_advantage(c1,A) | hazard_of_mortality(c1,A) = mod2. [copy(132),unit_del(a,123)]. given #74 (I,wt=11): 135 is_aligned(c1,A) | positional_advantage(c1,A) | hazard_of_mortality(c1,A) = high. [copy(134),unit_del(a,123)]. given #75 (I,wt=20): 136 -smaller_or_equal(age(A,B),tau) | -positional_advantage(A,B) | smaller_or_equal(age(A,f7(A)),tau) | greater(age(A,f8(A)),tau). [resolve(30,c,31,a)]. given #76 (I,wt=18): 137 -smaller_or_equal(age(A,B),tau) | -positional_advantage(A,B) | smaller_or_equal(age(A,f7(A)),tau) | -positional_advantage(A,f8(A)). [resolve(30,c,32,a)]. given #77 (I,wt=18): 138 -smaller_or_equal(age(A,B),tau) | -positional_advantage(A,B) | positional_advantage(A,f7(A)) | greater(age(A,f8(A)),tau). [resolve(30,c,33,a)]. given #78 (I,wt=16): 139 -smaller_or_equal(age(A,B),tau) | -positional_advantage(A,B) | positional_advantage(A,f7(A)) | -positional_advantage(A,f8(A)). [resolve(30,c,34,a)]. given #79 (I,wt=20): 140 -greater(age(A,B),tau) | positional_advantage(A,B) | smaller_or_equal(age(A,f7(A)),tau) | greater(age(A,f8(A)),tau). [resolve(35,c,31,a)]. given #80 (I,wt=18): 141 -greater(age(A,B),tau) | positional_advantage(A,B) | smaller_or_equal(age(A,f7(A)),tau) | -positional_advantage(A,f8(A)). [resolve(35,c,32,a)]. given #81 (I,wt=18): 142 -greater(age(A,B),tau) | positional_advantage(A,B) | positional_advantage(A,f7(A)) | greater(age(A,f8(A)),tau). [resolve(35,c,33,a)]. given #82 (I,wt=16): 143 -greater(age(A,B),tau) | positional_advantage(A,B) | positional_advantage(A,f7(A)) | -positional_advantage(A,f8(A)). [resolve(35,c,34,a)]. given #83 (I,wt=8): 144 -smaller_or_equal(age(c1,A),tau) | -positional_advantage(c1,A). [resolve(36,a,30,c)]. given #84 (I,wt=8): 145 -greater(age(c1,A),tau) | positional_advantage(c1,A). [resolve(36,a,35,c)]. given #85 (I,wt=3): 146 -greater(A,A). [factor(42,a,b)]. given #86 (I,wt=7): 147 is_aligned(A,B) | -dissimilar(A,B,B). [factor(47,a,b)]. given #87 (I,wt=7): 148 -is_aligned(A,B) | -dissimilar(A,B,B). [factor(48,a,b)]. given #88 (I,wt=16): 149 -smaller_or_equal(age(A,f10(A)),tau) | -positional_advantage(A,f10(A)) | smaller_or_equal(age(A,f9(A)),tau). [factor(50,b,d)]. given #89 (I,wt=14): 150 -smaller_or_equal(age(A,f10(A)),tau) | -positional_advantage(A,f10(A)) | positional_advantage(A,f9(A)). [factor(52,b,d)]. given #90 (I,wt=16): 151 -greater(age(A,f11(A)),tau) | positional_advantage(A,f11(A)) | greater(age(A,f12(A)),tau). [factor(55,b,c)]. given #91 (I,wt=14): 152 -greater(age(A,f11(A)),tau) | positional_advantage(A,f11(A)) | -positional_advantage(A,f12(A)). [factor(56,b,c)]. given #92 (I,wt=20): 153 -dissimilar(A,B,C) | -smaller_or_equal(age(A,f4(A)),eta) | has_immunity(A,f4(A)) | smaller_or_equal(age(A,f3(A)),eta). [factor(80,c,e)]. given #93 (I,wt=18): 154 -dissimilar(A,B,C) | -smaller_or_equal(age(A,f4(A)),eta) | has_immunity(A,f4(A)) | -has_immunity(A,f3(A)). [factor(82,c,e)]. given #94 (I,wt=20): 155 -dissimilar(A,B,C) | -greater(age(A,f5(A)),eta) | -has_immunity(A,f5(A)) | greater(age(A,f6(A)),eta). [factor(85,c,d)]. given #95 (I,wt=18): 156 -dissimilar(A,B,C) | -greater(age(A,f5(A)),eta) | -has_immunity(A,f5(A)) | has_immunity(A,f6(A)). [factor(86,c,d)]. given #96 (I,wt=14): 157 age(A,B) != zero | greater(age(A,C),sigma) | -dissimilar(A,B,C). [factor(93,c,d)]. given #97 (I,wt=11): 159 -smaller_or_equal(age(c1,A),eta) | smaller_or_equal(age(c1,f3(c1)),eta). [back_unit_del(115),unit_del(b,123),unit_del(d,123)]. given #98 (I,wt=6): 160 smaller_or_equal(age(c1,f1(c1)),eta). [back_unit_del(109),unit_del(b,123)]. given #99 (I,wt=16): 161 -smaller_or_equal(age(A,f8(A)),tau) | -positional_advantage(A,f8(A)) | smaller_or_equal(age(A,f7(A)),tau). [factor(137,b,d)]. given #100 (I,wt=14): 162 -smaller_or_equal(age(A,f8(A)),tau) | -positional_advantage(A,f8(A)) | positional_advantage(A,f7(A)). [factor(139,b,d)]. given #101 (I,wt=16): 163 -greater(age(A,f7(A)),tau) | positional_advantage(A,f7(A)) | greater(age(A,f8(A)),tau). [factor(142,b,c)]. given #102 (I,wt=14): 164 -greater(age(A,f7(A)),tau) | positional_advantage(A,f7(A)) | -positional_advantage(A,f8(A)). [factor(143,b,c)]. given #103 (F,wt=3): 170 -greater(mod1,high). [resolve(57,a,42,b)]. given #104 (T,wt=3): 165 smaller_or_equal(A,A). [xx_res(38,b)]. given #105 (T,wt=3): 171 smaller(mod1,high). [resolve(57,a,40,b)]. given #106 (A,wt=9): 166 smaller(A,B) | greater(A,B) | smaller_or_equal(A,B). [resolve(44,b,38,b)]. given #107 (F,wt=3): 174 -greater(low,mod1). [resolve(58,a,42,b)]. given #108 (F,wt=3): 178 -greater(very_low,low). [resolve(59,a,42,b)]. given #109 (T,wt=3): 175 smaller(low,mod1). [resolve(58,a,40,b)]. given #110 (T,wt=3): 179 smaller(very_low,low). [resolve(59,a,40,b)]. given #111 (A,wt=9): 167 smaller(A,B) | greater(A,B) | smaller_or_equal(B,A). [resolve(44,b,38,b(flip))]. given #112 (F,wt=3): 182 -greater(mod2,high). [resolve(60,a,42,b)]. given #113 (F,wt=3): 186 -greater(low,mod2). [resolve(61,a,42,b)]. given #114 (T,wt=3): 183 smaller(mod2,high). [resolve(60,a,40,b)]. given #115 (T,wt=3): 187 smaller(low,mod2). [resolve(61,a,40,b)]. given #116 (A,wt=6): 168 -greater(A,high) | greater(A,mod1). [resolve(57,a,43,b)]. given #117 (F,wt=3): 190 -greater(mod1,mod2). [resolve(62,a,42,b)]. given #118 (F,wt=3): 194 -greater(zero,sigma). [resolve(63,a,42,b)]. given #119 (T,wt=3): 191 smaller(mod1,mod2). [resolve(62,a,40,b)]. given #120 (T,wt=3): 195 smaller(zero,sigma). [resolve(63,a,40,b)]. given #121 (A,wt=6): 169 -greater(mod1,A) | greater(high,A). [resolve(57,a,43,a)]. given #122 (F,wt=3): 198 -greater(zero,tau). [resolve(64,a,42,b)]. given #123 (F,wt=3): 247 -positional_advantage(c1,c4). [ur(144,a,70,a)]. given #124 (T,wt=3): 199 smaller(zero,tau). [resolve(64,a,40,b)]. given #125 (T,wt=3): 200 greater(tau,sigma). [resolve(65,a,41,b)]. given #126 (A,wt=6): 172 -greater(A,mod1) | greater(A,low). [resolve(58,a,43,b)]. given #127 (F,wt=3): 251 -smaller(A,A). [ur(41,a,146,a)]. given #128 (F,wt=3): 258 -greater(low,high). [ur(43,a,58,a,c,170,a)]. given #129 (T,wt=3): 201 smaller_or_equal(sigma,tau). [resolve(65,a,37,b)]. given #130 (T,wt=3): 231 is_aligned(c1,c5). [resolve(126,a,72,a)]. given #131 (A,wt=6): 173 -greater(low,A) | greater(mod1,A). [resolve(58,a,43,a)]. given #132 (F,wt=3): 259 -smaller(high,mod1). [ur(41,a,170,a)]. given #133 (F,wt=3): 264 -greater(very_low,mod1). [ur(43,a,59,a,c,174,a)]. given #134 (T,wt=3): 250 positional_advantage(c1,c2). [resolve(145,a,67,a)]. given #135 (T,wt=3): 260 smaller_or_equal(mod1,high). [resolve(171,a,37,b)]. given #136 (A,wt=6): 176 -greater(A,low) | greater(A,very_low). [resolve(59,a,43,b)]. given #137 (F,wt=3): 265 -smaller(mod1,low). [ur(41,a,174,a)]. given #138 (F,wt=3): 266 -greater(very_low,mod2). [ur(43,b,61,a,c,178,a)]. given #139 (T,wt=3): 268 smaller_or_equal(low,mod1). [resolve(175,a,37,b)]. given #140 (T,wt=3): 269 smaller_or_equal(very_low,low). [resolve(179,a,37,b)]. given #141 (A,wt=6): 177 -greater(very_low,A) | greater(low,A). [resolve(59,a,43,a)]. given #142 (F,wt=3): 267 -smaller(low,very_low). [ur(41,a,178,a)]. given #143 (F,wt=3): 271 -smaller(high,mod2). [ur(41,a,182,a)]. given #144 (T,wt=3): 273 smaller_or_equal(mod2,high). [resolve(183,a,37,b)]. given #145 (T,wt=3): 274 smaller_or_equal(low,mod2). [resolve(187,a,37,b)]. given #146 (A,wt=6): 180 -greater(A,high) | greater(A,mod2). [resolve(60,a,43,b)]. given #147 (F,wt=3): 272 -smaller(mod2,low). [ur(41,a,186,a)]. given #148 (F,wt=3): 275 -smaller(mod2,mod1). [ur(41,a,190,a)]. given #149 (T,wt=3): 278 smaller_or_equal(mod1,mod2). [resolve(191,a,37,b)]. given #150 (T,wt=3): 279 smaller_or_equal(zero,sigma). [resolve(195,a,37,b)]. given #151 (A,wt=6): 181 -greater(mod2,A) | greater(high,A). [resolve(60,a,43,a)]. given #152 (F,wt=3): 277 -smaller(sigma,zero). [ur(41,a,194,a)]. given #153 (F,wt=3): 282 -smaller(tau,zero). [ur(41,a,198,a)]. given #154 (T,wt=3): 280 greater(high,low). [resolve(169,a,58,a)]. given #155 (T,wt=3): 284 smaller_or_equal(zero,tau). [resolve(199,a,37,b)]. given #156 (A,wt=6): 184 -greater(A,mod2) | greater(A,low). [resolve(61,a,43,b)]. given #157 (F,wt=3): 285 -positional_advantage(c1,c5). [back_unit_del(248),unit_del(a,284)]. given #158 (F,wt=3): 288 -greater(sigma,tau). [resolve(200,a,42,b)]. given #159 (T,wt=3): 295 greater(mod1,very_low). [resolve(173,a,59,a)]. given #160 (T,wt=3): 299 greater(mod2,very_low). [resolve(176,a,61,a)]. given #161 (A,wt=6): 185 -greater(low,A) | greater(mod2,A). [resolve(61,a,43,a)]. given #162 (F,wt=3): 289 -greater(very_low,high). [ur(43,a,59,a,c,258,a)]. given #163 (F,wt=3): 290 -smaller(high,low). [ur(41,a,258,a)]. given #164 (T,wt=3): 301 greater(high,very_low). [resolve(280,a,176,a)]. given #165 (T,wt=3): 304 smaller(low,high). [resolve(280,a,40,b)]. given #166 (A,wt=6): 188 -greater(A,mod2) | greater(A,mod1). [resolve(62,a,43,b)]. given #167 (F,wt=3): 296 -smaller(mod1,very_low). [ur(41,a,264,a)]. given #168 (F,wt=3): 300 -smaller(mod2,very_low). [ur(41,a,266,a)]. given #169 (T,wt=3): 309 smaller(very_low,mod1). [resolve(295,a,40,b)]. given #170 (T,wt=3): 312 smaller(very_low,mod2). [resolve(299,a,40,b)]. given #171 (A,wt=6): 189 -greater(mod1,A) | greater(mod2,A). [resolve(62,a,43,a)]. given #172 (F,wt=3): 306 -smaller(tau,sigma). [ur(41,a,288,a)]. given #173 (F,wt=3): 313 -smaller(high,very_low). [ur(41,a,289,a)]. given #174 (T,wt=3): 316 smaller(very_low,high). [resolve(301,a,40,b)]. given #175 (T,wt=3): 317 smaller_or_equal(low,high). [resolve(304,a,37,b)]. given #176 (A,wt=6): 192 -greater(A,sigma) | greater(A,zero). [resolve(63,a,43,b)]. given #177 (F,wt=4): 294 -dissimilar(c1,c5,c5). [ur(148,a,231,a)]. given #178 (F,wt=5): 206 -greater(tau,age(c1,c2)). [resolve(67,a,42,b)]. given #179 (T,wt=3): 318 smaller_or_equal(very_low,mod1). [resolve(309,a,37,b)]. given #180 (T,wt=3): 319 smaller_or_equal(very_low,mod2). [resolve(312,a,37,b)]. given #181 (A,wt=6): 193 -greater(zero,A) | greater(sigma,A). [resolve(63,a,43,a)]. given #182 (F,wt=5): 211 -greater(sigma,age(c1,c4)). [resolve(69,a,42,b)]. given #183 (F,wt=5): 276 -greater(zero,age(c1,c4)). [ur(43,b,69,a,c,194,a)]. given #184 (T,wt=3): 320 smaller_or_equal(very_low,high). [resolve(316,a,37,b)]. given #185 (T,wt=5): 207 smaller(tau,age(c1,c2)). [resolve(67,a,40,b)]. given #186 (A,wt=6): 196 -greater(A,tau) | greater(A,zero). [resolve(64,a,43,b)]. given #187 (F,wt=5): 281 -greater(zero,age(c1,c2)). [ur(43,b,67,a,c,198,a)]. given #188 (F,wt=5): 283 -greater(age(c1,c4),tau). [ur(145,b,247,a)]. given #189 (T,wt=5): 212 smaller(sigma,age(c1,c4)). [resolve(69,a,40,b)]. given #190 (T,wt=5): 291 hazard_of_mortality(c1,c5) = mod2. [resolve(231,a,133,a),unit_del(a,285)]. given #191 (A,wt=6): 197 -greater(zero,A) | greater(tau,A). [resolve(64,a,43,a)]. given #192 (F,wt=5): 297 -smaller_or_equal(age(c1,c2),tau). [resolve(250,a,144,b)]. given #193 (F,wt=5): 305 -greater(sigma,age(c1,c2)). [ur(43,b,67,a,c,288,a)]. given #194 (T,wt=5): 321 greater(age(c1,c4),zero). [resolve(192,a,69,a)]. given #195 (T,wt=5): 325 smaller_or_equal(tau,age(c1,c2)). [resolve(207,a,37,b)]. given #196 (A,wt=8): 204 -greater(A,age(c1,c2)) | greater(A,tau). [resolve(67,a,43,b)]. given #197 (F,wt=5): 322 -smaller(age(c1,c2),tau). [ur(41,a,206,a)]. given #198 (F,wt=5): 323 -smaller(age(c1,c4),sigma). [ur(41,a,211,a)]. given #199 (T,wt=5): 326 greater(age(c1,c2),zero). [resolve(196,a,67,a)]. given #200 (T,wt=5): 330 smaller_or_equal(sigma,age(c1,c4)). [resolve(212,a,37,b)]. given #201 (A,wt=8): 205 -greater(tau,A) | greater(age(c1,c2),A). [resolve(67,a,43,a)]. given #202 (F,wt=5): 324 -smaller(age(c1,c4),zero). [ur(41,a,276,a)]. given #203 (F,wt=5): 327 -smaller(age(c1,c2),zero). [ur(41,a,281,a)]. given #204 (T,wt=5): 335 smaller(zero,age(c1,c4)). [resolve(321,a,40,b)]. given #205