============================== FOF-Prover9 =========================== FOF-Prover9 (32) version March-2007, March 2007. Process 20937 was started by mccune on cleo, Mon Mar 19 17:01:22 2007 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 20938 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) 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 (A,wt=3): 165 smaller_or_equal(A,A). [xx_res(38,b)]. given #104 (F,wt=3): 170 -greater(mod1,high). [resolve(57,a,42,b)]. given #105 (F,wt=3): 174 -greater(low,mod1). [resolve(58,a,42,b)]. given #106 (F,wt=3): 178 -greater(very_low,low). [resolve(59,a,42,b)]. given #107 (F,wt=3): 182 -greater(mod2,high). [resolve(60,a,42,b)]. given #108 (T,wt=3): 171 smaller(mod1,high). [resolve(57,a,40,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 (T,wt=3): 183 smaller(mod2,high). [resolve(60,a,40,b)]. given #112 (A,wt=9): 166 smaller(A,B) | greater(A,B) | smaller_or_equal(A,B). [resolve(44,b,38,b)]. given #113 (F,wt=3): 186 -greater(low,mod2). [resolve(61,a,42,b)]. given #114 (F,wt=3): 190 -greater(mod1,mod2). [resolve(62,a,42,b)]. given #115 (F,wt=3): 194 -greater(zero,sigma). [resolve(63,a,42,b)]. given #116 (F,wt=3): 198 -greater(zero,tau). [resolve(64,a,42,b)]. given #117 (T,wt=3): 187 smaller(low,mod2). [resolve(61,a,40,b)]. given #118 (T,wt=3): 191 smaller(mod1,mod2). [resolve(62,a,40,b)]. given #119 (T,wt=3): 195 smaller(zero,sigma). [resolve(63,a,40,b)]. given #120 (T,wt=3): 199 smaller(zero,tau). [resolve(64,a,40,b)]. given #121 (A,wt=9): 167 smaller(A,B) | greater(A,B) | smaller_or_equal(B,A). [resolve(44,b,38,b(flip))]. given #122 (F,wt=3): 265 -positional_advantage(c1,c5). [back_unit_del(246),unit_del(a,264)]. given #123 (F,wt=5): 204 -greater(sigma,age(c1,c2)). [resolve(67,a,42,b)]. given #124 (F,wt=5): 212 -greater(tau,age(c1,c4)). [resolve(70,a,42,b)]. given #125 (T,wt=3): 200 greater(tau,sigma). [resolve(65,a,41,b)]. given #126 (T,wt=3): 201 smaller_or_equal(sigma,tau). [resolve(65,a,37,b)]. given #127 (T,wt=3): 230 is_aligned(c1,c5). [resolve(126,a,72,a)]. given #128 (T,wt=3): 247 positional_advantage(c1,c4). [resolve(145,a,70,a)]. given #129 (A,wt=6): 168 -greater(A,high) | greater(A,mod1). [resolve(57,a,43,b)]. given #130 (F,wt=3): 269 -greater(sigma,tau). [resolve(200,a,42,b)]. given #131 (F,wt=5): 273 -smaller_or_equal(age(c1,c4),tau). [resolve(247,a,144,b)]. given #132 (T,wt=3): 254 smaller_or_equal(mod1,high). [resolve(171,a,37,b)]. given #133 (T,wt=3): 255 smaller_or_equal(low,mod1). [resolve(175,a,37,b)]. given #134 (T,wt=3): 256 smaller_or_equal(very_low,low). [resolve(179,a,37,b)]. given #135 (T,wt=3): 257 smaller_or_equal(mod2,high). [resolve(183,a,37,b)]. given #136 (A,wt=6): 169 -greater(mod1,A) | greater(high,A). [resolve(57,a,43,a)]. given #137 (T,wt=3): 261 smaller_or_equal(low,mod2). [resolve(187,a,37,b)]. given #138 (T,wt=3): 262 smaller_or_equal(mod1,mod2). [resolve(191,a,37,b)]. given #139 (T,wt=3): 263 smaller_or_equal(zero,sigma). [resolve(195,a,37,b)]. given #140 (T,wt=3): 264 smaller_or_equal(zero,tau). [resolve(199,a,37,b)]. given #141 (A,wt=6): 172 -greater(A,mod1) | greater(A,low). [resolve(58,a,43,b)]. given #142 (T,wt=3): 275 greater(high,low). [resolve(169,a,58,a)]. given #143 (T,wt=3): 279 smaller(low,high). [resolve(275,a,40,b)]. given #144 (T,wt=3): 280 smaller_or_equal(low,high). [resolve(279,a,37,b)]. given #145 (T,wt=5): 205 smaller(sigma,age(c1,c2)). [resolve(67,a,40,b)]. given #146 (A,wt=6): 173 -greater(low,A) | greater(mod1,A). [resolve(58,a,43,a)]. given #147 (F,wt=3): 278 -greater(low,high). [resolve(275,a,42,b)]. given #148 (T,wt=3): 282 greater(mod1,very_low). [resolve(173,a,59,a)]. given #149 (T,wt=3): 283 greater(high,very_low). [resolve(282,a,169,a)]. given #150 (T,wt=3): 287 smaller(very_low,mod1). [resolve(282,a,40,b)]. given #151 (T,wt=3): 291 smaller(very_low,high). [resolve(283,a,40,b)]. given #152 (A,wt=6): 176 -greater(A,low) | greater(A,very_low). [resolve(59,a,43,b)]. given #153 (F,wt=3): 286 -greater(very_low,mod1). [resolve(282,a,42,b)]. given #154 (F,wt=3): 290 -greater(very_low,high). [resolve(283,a,42,b)]. given #155 (T,wt=3): 292 smaller_or_equal(very_low,mod1). [resolve(287,a,37,b)]. given #156 (T,wt=3): 293 smaller_or_equal(very_low,high). [resolve(291,a,37,b)]. given #157 (T,wt=3): 294 greater(mod2,very_low). [resolve(176,a,61,a)]. given #158 (T,wt=3): 298 smaller(very_low,mod2). [resolve(294,a,40,b)]. given #159 (A,wt=6): 177 -greater(very_low,A) | greater(low,A). [resolve(59,a,43,a)]. given #160 (F,wt=3): 297 -greater(very_low,mod2). [resolve(294,a,42,b)]. given #161 (T,wt=3): 299 smaller_or_equal(very_low,mod2). [resolve(298,a,37,b)]. given #162 (T,wt=5): 213 smaller(tau,age(c1,c4)). [resolve(70,a,40,b)]. given #163 (T,wt=5): 270 hazard_of_mortality(c1,c5) = mod2. [resolve(230,a,133,a),unit_del(a,265)]. given #164 (T,wt=5): 281 smaller_or_equal(sigma,age(c1,c2)). [resolve(205,a,37,b)]. given #165 (A,wt=6): 180 -greater(A,high) | greater(A,mod2). [resolve(60,a,43,b)]. given #166 (T,wt=5): 300 smaller_or_equal(tau,age(c1,c4)). [resolve(213,a,37,b)]. given #167 (T,wt=6): 181 -greater(mod2,A) | greater(high,A). [resolve(60,a,43,a)]. given #168 (T,wt=6): 184 -greater(A,mod2) | greater(A,low). [resolve(61,a,43,b)]. given #169 (T,wt=6): 185 -greater(low,A) | greater(mod2,A). [resolve(61,a,43,a)]. given #170 (A,wt=6): 188 -greater(A,mod2) | greater(A,mod1). [resolve(62,a,43,b)]. given #171 (T,wt=6): 189 -greater(mod1,A) | greater(mod2,A). [resolve(62,a,43,a)]. given #172 (T,wt=6): 192 -greater(A,sigma) | greater(A,zero). [resolve(63,a,43,b)]. given #173 (T,wt=5): 301 greater(age(c1,c2),zero). [resolve(192,a,67,a)]. given #174 (T,wt=5): 305 smaller(zero,age(c1,c2)). [resolve(301,a,40,b)]. given #175 (A,wt=6): 193 -greater(zero,A) | greater(sigma,A). [resolve(63,a,43,a)]. given #176 (F,wt=5): 304 -greater(zero,age(c1,c2)). [resolve(301,a,42,b)]. given #177 (T,wt=5): 306 smaller_or_equal(zero,age(c1,c2)). [resolve(305,a,37,b)]. given #178 (T,wt=6): 196 -greater(A,tau) | greater(A,zero). [resolve(64,a,43,b)]. given #179 (T,wt=5): 307 greater(age(c1,c4),zero). [resolve(196,a,70,a)]. given #180 (T,wt=5): 311 smaller(zero,age(c1,c4)). [resolve(307,a,40,b)]. given #181 (A,wt=6): 197 -greater(zero,A) | greater(tau,A). [resolve(64,a,43,a)]. given #182 (F,wt=5): 310 -greater(zero,age(c1,c4)). [resolve(307,a,42,b)]. given #183 (T,wt=5): 312 smaller_or_equal(zero,age(c1,c4)). [resolve(311,a,37,b)]. given #184 (T,wt=6): 252 smaller_or_equal(age(c1,f3(c1)),eta). [resolve(160,a,159,a)]. given #185 (T,wt=6): 260 greater(A,B) | smaller_or_equal(A,B). [resolve(166,a,37,b),merge(c)]. given #186 (T,wt=6): 267 -greater(A,tau) | greater(A,sigma). [resolve(200,a,43,b)]. given #187 (A,wt=8): 202 -greater(A,age(c1,c2)) | greater(A,sigma). [resolve(67,a,43,b)]. given #188 (T,wt=5): 315 greater(age(c1,c4),sigma). [resolve(267,a,70,a)]. given #189 (T,wt=5): 319 smaller(sigma,age(c1,c4)). [resolve(315,a,40,b)]. given #190 (T,wt=5): 320 smaller_or_equal(sigma,age(c1,c4)). [resolve(319,a,37,b)]. given #191 (T,wt=6): 268 -greater(sigma,A) | greater(tau,A). [resolve(200,a,43,a)]. given #192 (A,wt=8): 203 -greater(sigma,A) | greater(age(c1,c2),A). [resolve(67,a,43,a)]. given #193 (F,wt=5): 318 -greater(sigma,age(c1,c4)). [resolve(315,a,42,b)]. given #194 (T,wt=6): 276 -greater(A,high) | greater(A,low). [resolve(275,a,43,b)]. given #195 (T,wt=6): 277 -greater(low,A) | greater(high,A). [resolve(275,a,43,a)]. given #196 (T,wt=6): 284 -greater(A,mod1) | greater(A,very_low). [resolve(282,a,43,b)]. given #197 (T,wt=6): 285 -greater(very_low,A) | greater(mod1,A). [resolve(282,a,43,a)]. given #198 (A,wt=10): 206 smaller(age(c1,c2),tau) | age(c1,c2) = tau. [resolve(68,a,39,c),flip(b)]. given #199 (T,wt=6): 288 -greater(A,high) | greater(A,very_low). [resolve(283,a,43,b)]. given #200 (T,wt=6): 289 -greater(very_low,A) | greater(high,A). [resolve(283,a,43,a)]. given #201 (T,wt=6): 295 -greater(A,mod2) | greater(A,very_low). [resolve(294,a,43,b)]. given #202 (T,wt=6): 296 -greater(very_low,A) | greater(mod2,A). [resolve(294,a,43,a)]. given #203 (A,wt=10): 207 smaller(age(c1,c3),sigma) | age(c1,c3) = sigma. [resolve(69,a,39,c),flip(b)]. given #204 (T,wt=7): 271 dissimilar(c1,c5,A) | is_aligned(c1,A). [resolve(230,a,125,a)]. given #205 (T,wt=7): 272 is_aligned(c1,A) | dissimilar(c1,A,c5). [resolve(230,a,124,c)]. given #206 (T,wt=8): 210 -greater(A,age(c1,c4)) | greater(A,tau). [resolve(70,a,43,b)]. given #207 (T,wt=8): 211 -greater(tau,A) | greater(age(c1,c4),A). [resolve(70,a,43,a)]. given #208 (A,wt=15): 220 is_aligned(A,B) | -has_endowment(A) | smaller(zero,age(A,B)) | greater(zero,age(A,B)). [resolve(90,a,44,b)]. given #209 (T,wt=8): 274 is_aligned(c1,c4) | hazard_of_mortality(c1,c4) = mod1. [resolve(247,a,131,b)]. given #210 (T,wt=8): 302 -greater(A,age(c1,c2)) | greater(A,zero). [resolve(301,a,43,b)]. given #211 (T,wt=8): 303 -greater(zero,A) | greater(age(c1,c2),A). [resolve(301,a,43,a)]. given #212 (T,wt=8): 308 -greater(A,age(c1,c4)) | greater(A,zero). [resolve(307,a,43,b)]. given #213 (A,wt=15): 221 is_aligned(A,B) | -has_endowment(A) | smaller(age(A,B),zero) | greater(age(A,B),zero). [resolve(90,a,44,b(flip))]. given #214 (T,wt=8): 309 -greater(zero,A) | greater(age(c1,c4),A). [resolve(307,a,43,a)]. given #215 (T,wt=8): 316 -greater(A,age(c1,c4)) | greater(A,sigma). [resolve(315,a,43,b)]. given #216 (T,wt=8): 317 -greater(sigma,A) | greater(age(c1,c4),A). [resolve(315,a,43,a)]. given #217 (T,wt=8): 336 smaller(age(c1,c2),tau) | -positional_advantage(c1,c2). [para(206(b,1),144(a,1)),unit_del(b,165)]. given #218 (A,wt=17): 223 is_aligned(A,B) | -dissimilar(A,C,D) | smaller(zero,age(A,B)) | greater(zero,age(A,B)). [resolve(91,a,44,b)]. given #219 (T,wt=8): 351 smaller(age(c1,c3),sigma) | -positional_advantage(c1,c3). [para(207(b,1),144(a,1)),unit_del(b,201)]. given #220 (T,wt=8): 353 is_aligned(c1,c4) | smaller_or_equal(mod1,hazard_of_mortality(c1,c4)). [resolve(274,b,38,b)]. given #221 (T,wt=8): 354 is_aligned(c1,c4) | smaller_or_equal(hazard_of_mortality(c1,c4),mod1). [resolve(274,b,38,b(flip))]. given #222 (T,wt=8): 355 is_aligned(c1,c4) | -smaller(mod1,hazard_of_mortality(c1,c3)). [para(274(b,1),71(a,1))]. given #223 (A,wt=17): 224 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 #224 (T,wt=9): 233 dissimilar(c1,c5,A) | -greater(age(c1,A),sigma). [resolve(127,a,72,a)]. given #225 (T,wt=4): 364 dissimilar(c1,c5,c4). [resolve(233,b,315,a)]. given #226 (T,wt=4): 365 dissimilar(c1,c5,c2). [resolve(233,b,67,a)]. given #227 (T,wt=5): 372 hazard_of_mortality(c1,c4) = mod1. [back_unit_del(274),unit_del(a,366)]. given #228 (A,wt=21): 225 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 #229 (F,wt=3): 366 -is_aligned(c1,c4). [resolve(364,a,48,c),unit_del(a,230)]. given #230 (F,wt=3): 373 -is_aligned(c1,c2). [resolve(365,a,48,c),unit_del(a,230)]. given #231 (F,wt=5): 369 -smaller(mod1,hazard_of_mortality(c1,c3)). [back_unit_del(355),unit_del(a,366)]. given #232 (T,wt=6): 367 is_aligned(c1,c3) | positional_advantage(c1,c3). [back_unit_del(363),unit_del(c,366)]. given #233 (T,wt=8): 374 smaller(age(c1,c2),tau) | zero != tau. [back_unit_del(329),unit_del(c,373)]. given #234 (T,wt=8): 375 positional_advantage(c1,c3) | hazard_of_mortality(c1,c3) = mod2. [resolve(367,a,133,a),merge(b)]. given #235 (T,wt=3): 380 positional_advantage(c1,c3). [para(375(b,1),369(a,2)),unit_del(b,191)]. given #236 (A,wt=21): 226 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 #237 (F,wt=5): 382 -smaller_or_equal(age(c1,c3),tau). [resolve(380,a,144,b)]. given #238 (T,wt=5): 381 smaller(age(c1,c3),sigma). [back_unit_del(351),unit_del(b,380)]. given #239 (T,wt=5): 384 greater(age(c1,c3),tau). [resolve(382,a,260,b)]. given #240 (T,wt=5): 385 greater(sigma,age(c1,c3)). [resolve(381,a,41,b)]. ============================== PROOF ================================= % Proof 1 at 0.03 (+ 0.01) seconds. % Length of proof is 68. % Level of proof is 13. % Maximum clause weight is 14. % Given clauses 240. 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]. 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]. 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)]. 166 smaller(A,B) | greater(A,B) | smaller_or_equal(A,B). [resolve(44,b,38,b)]. 171 smaller(mod1,high). [resolve(57,a,40,b)]. 191 smaller(mod1,mod2). [resolve(62,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)]. 230 is_aligned(c1,c5). [resolve(126,a,72,a)]. 233 dissimilar(c1,c5,A) | -greater(age(c1,A),sigma). [resolve(127,a,72,a)]. 247 positional_advantage(c1,c4). [resolve(145,a,70,a)]. 260 greater(A,B) | smaller_or_equal(A,B). [resolve(166,a,37,b),merge(c)]. 267 -greater(A,tau) | greater(A,sigma). [resolve(200,a,43,b)]. 268 -greater(sigma,A) | greater(tau,A). [resolve(200,a,43,a)]. 274 is_aligned(c1,c4) | hazard_of_mortality(c1,c4) = mod1. [resolve(247,a,131,b)]. 315 greater(age(c1,c4),sigma). [resolve(267,a,70,a)]. 351 smaller(age(c1,c3),sigma) | -positional_advantage(c1,c3). [para(207(b,1),144(a,1)),unit_del(b,201)]. 355 is_aligned(c1,c4) | -smaller(mod1,hazard_of_mortality(c1,c3)). [para(274(b,1),71(a,1))]. 363 is_aligned(c1,c3) | positional_advantage(c1,c3) | is_aligned(c1,c4). [para(135(c,1),355(b,2)),unit_del(d,171)]. 364 dissimilar(c1,c5,c4). [resolve(233,b,315,a)]. 366 -is_aligned(c1,c4). [resolve(364,a,48,c),unit_del(a,230)]. 367 is_aligned(c1,c3) | positional_advantage(c1,c3). [back_unit_del(363),unit_del(c,366)]. 369 -smaller(mod1,hazard_of_mortality(c1,c3)). [back_unit_del(355),unit_del(a,366)]. 375 positional_advantage(c1,c3) | hazard_of_mortality(c1,c3) = mod2. [resolve(367,a,133,a),merge(b)]. 380 positional_advantage(c1,c3). [para(375(b,1),369(a,2)),unit_del(b,191)]. 381 smaller(age(c1,c3),sigma). [back_unit_del(351),unit_del(b,380)]. 382 -smaller_or_equal(age(c1,c3),tau). [resolve(380,a,144,b)]. 384 greater(age(c1,c3),tau). [resolve(382,a,260,b)]. 385 greater(sigma,age(c1,c3)). [resolve(381,a,41,b)]. 390 -greater(tau,age(c1,c3)). [resolve(384,a,42,b)]. 393 $F. [resolve(385,a,268,a),unit_del(a,390)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=240. Generated=725. Kept=347. proofs=1. Usable=229. Sos=24. Demods=3. Limbo=1, Disabled=238. Hints=0. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=377. Back_subsumed=77. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=3 (0 lex), Back_demodulated=4. Back_unit_deleted=12. Demod_attempts=7512. Demod_rewrites=14. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=131. Nonunit_bsub_feature_tests=434. Megabytes=0.57. User_CPU=0.03, System_CPU=0.01, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 20938 exit (max_proofs) Mon Mar 19 17:01:22 2007 ============================== 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 20939 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) 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.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),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 (A,wt=3): 165 smaller_or_equal(A,A). [xx_res(38,b)]. given #104 (F,wt=3): 170 -greater(mod1,high). [resolve(57,a,42,b)]. given #105 (F,wt=3): 174 -greater(low,mod1). [resolve(58,a,42,b)]. given #106 (F,wt=3): 178 -greater(very_low,low). [resolve(59,a,42,b)]. given #107 (F,wt=3): 182 -greater(mod2,high). [resolve(60,a,42,b)]. given #108 (T,wt=3): 171 smaller(mod1,high). [resolve(57,a,40,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 (T,wt=3): 183 smaller(mod2,high). [resolve(60,a,40,b)]. given #112 (A,wt=9): 166 smaller(A,B) | greater(A,B) | smaller_or_equal(A,B). [resolve(44,b,38,b)]. given #113 (F,wt=3): 186 -greater(low,mod2). [resolve(61,a,42,b)]. given #114 (F,wt=3): 190 -greater(mod1,mod2). [resolve(62,a,42,b)]. given #115 (F,wt=3): 194 -greater(zero,sigma). [resolve(63,a,42,b)]. given #116 (F,wt=3): 198 -greater(zero,tau). [resolve(64,a,42,b)]. given #117 (T,wt=3): 187 smaller(low,mod2). [resolve(61,a,40,b)]. given #118 (T,wt=3): 191 smaller(mod1,mod2). [resolve(62,a,40,b)]. given #119 (T,wt=3): 195 smaller(zero,sigma). [resolve(63,a,40,b)]. given #120 (T,wt=3): 199 smaller(zero,tau). [resolve(64,a,40,b)]. given #121 (A,wt=9): 167 smaller(A,B) | greater(A,B) | smaller_or_equal(B,A). [resolve(44,b,38,b(flip))]. given #122 (F,wt=3): 265 -positional_advantage(c1,c5). [back_unit_del(246),unit_del(a,264)]. given #123 (F,wt=5): 206 -greater(tau,age(c1,c2)). [resolve(67,a,42,b)]. given #124 (F,wt=5): 211 -greater(sigma,age(c1,c4)). [resolve(69,a,42,b)]. given #125 (T,wt=3): 200 greater(tau,sigma). [resolve(65,a,41,b)]. given #126 (T,wt=3): 201 smaller_or_equal(sigma,tau). [resolve(65,a,37,b)]. given #127 (T,wt=3): 230 is_aligned(c1,c5). [resolve(126,a,72,a)]. given #128 (T,wt=3): 247 positional_advantage(c1,c2). [resolve(145,a,67,a)]. given #129 (A,wt=6): 168 -greater(A,high) | greater(A,mod1). [resolve(57,a,43,b)]. given #130 (F,wt=3): 269 -greater(sigma,tau). [resolve(200,a,42,b)]. given #131 (F,wt=5): 273 -smaller_or_equal(age(c1,c2),tau). [resolve(247,a,144,b)]. given #132 (T,wt=3): 254 smaller_or_equal(mod1,high). [resolve(171,a,37,b)]. given #133 (T,wt=3): 255 smaller_or_equal(low,mod1). [resolve(175,a,37,b)]. given #134 (T,wt=3): 256 smaller_or_equal(very_low,low). [resolve(179,a,37,b)]. given #135 (T,wt=3): 257 smaller_or_equal(mod2,high). [resolve(183,a,37,b)]. given #136 (A,wt=6): 169 -greater(mod1,A) | greater(high,A). [resolve(57,a,43,a)]. given #137 (T,wt=3): 261 smaller_or_equal(low,mod2). [resolve(187,a,37,b)]. given #138 (T,wt=3): 262 smaller_or_equal(mod1,mod2). [resolve(191,a,37,b)]. given #139 (T,wt=3): 263 smaller_or_equal(zero,sigma). [resolve(195,a,37,b)]. given #140 (T,wt=3): 264 smaller_or_equal(zero,tau). [resolve(199,a,37,b)]. given #141 (A,wt=6): 172 -greater(A,mod1) | greater(A,low). [resolve(58,a,43,b)]. given #142 (T,wt=3): 275 greater(high,low). [resolve(169,a,58,a)]. given #143 (T,wt=3): 279 smaller(low,high). [resolve(275,a,40,b)]. given #144 (T,wt=3): 280 smaller_or_equal(low,high). [resolve(279,a,37,b)]. given #145 (T,wt=5): 207 smaller(tau,age(c1,c2)). [resolve(67,a,40,b)]. given #146 (A,wt=6): 173 -greater(low,A) | greater(mod1,A). [resolve(58,a,43,a)]. given #147 (F,wt=3): 278 -greater(low,high). [resolve(275,a,42,b)]. given #148 (T,wt=3): 282 greater(mod1,very_low). [resolve(173,a,59,a)]. given #149 (T,wt=3): 283 greater(high,very_low). [resolve(282,a,169,a)]. given #150 (T,wt=3): 287 smaller(very_low,mod1). [resolve(282,a,40,b)]. given #151 (T,wt=3): 291 smaller(very_low,high). [resolve(283,a,40,b)]. given #152 (A,wt=6): 176 -greater(A,low) | greater(A,very_low). [resolve(59,a,43,b)]. given #153 (F,wt=3): 286 -greater(very_low,mod1). [resolve(282,a,42,b)]. given #154 (F,wt=3): 290 -greater(very_low,high). [resolve(283,a,42,b)]. given #155 (T,wt=3): 292 smaller_or_equal(very_low,mod1). [resolve(287,a,37,b)]. given #156 (T,wt=3): 293 smaller_or_equal(very_low,high). [resolve(291,a,37,b)]. given #157 (T,wt=3): 294 greater(mod2,very_low). [resolve(176,a,61,a)]. given #158 (T,wt=3): 298 smaller(very_low,mod2). [resolve(294,a,40,b)]. given #159 (A,wt=6): 177 -greater(very_low,A) | greater(low,A). [resolve(59,a,43,a)]. given #160 (F,wt=3): 297 -greater(very_low,mod2). [resolve(294,a,42,b)]. given #161 (T,wt=3): 299 smaller_or_equal(very_low,mod2). [resolve(298,a,37,b)]. given #162 (T,wt=5): 212 smaller(sigma,age(c1,c4)). [resolve(69,a,40,b)]. given #163 (T,wt=5): 270 hazard_of_mortality(c1,c5) = mod2. [resolve(230,a,133,a),unit_del(a,265)]. given #164 (T,wt=5): 281 smaller_or_equal(tau,age(c1,c2)). [resolve(207,a,37,b)]. given #165 (A,wt=6): 180 -greater(A,high) | greater(A,mod2). [resolve(60,a,43,b)]. given #166 (T,wt=5): 300 smaller_or_equal(sigma,age(c1,c4)). [resolve(212,a,37,b)]. given #167 (T,wt=6): 181 -greater(mod2,A) | greater(high,A). [resolve(60,a,43,a)]. given #168 (T,wt=6): 184 -greater(A,mod2) | greater(A,low). [resolve(61,a,43,b)]. given #169 (T,wt=6): 185 -greater(low,A) | greater(mod2,A). [resolve(61,a,43,a)]. given #170 (A,wt=6): 188 -greater(A,mod2) | greater(A,mod1). [resolve(62,a,43,b)]. given #171 (T,wt=6): 189 -greater(mod1,A) | greater(mod2,A). [resolve(62,a,43,a)]. given #172 (T,wt=6): 192 -greater(A,sigma) | greater(A,zero). [resolve(63,a,43,b)]. given #173 (T,wt=5): 301 greater(age(c1,c4),zero). [resolve(192,a,69,a)]. given #174 (T,wt=5): 305 smaller(zero,age(c1,c4)). [resolve(301,a,40,b)]. given #175 (A,wt=6): 193 -greater(zero,A) | greater(sigma,A). [resolve(63,a,43,a)]. given #176 (F,wt=5): 304 -greater(zero,age(c1,c4)). [resolve(301,a,42,b)]. given #177 (T,wt=5): 306 smaller_or_equal(zero,age(c1,c4)). [resolve(305,a,37,b)]. given #178 (T,wt=6): 196 -greater(A,tau) | greater(A,zero). [resolve(64,a,43,b)]. given #179 (T,wt=5): 307 greater(age(c1,c2),zero). [resolve(196,a,67,a)]. given #180 (T,wt=5): 311 smaller(zero,age(c1,c2)). [resolve(307,a,40,b)]. given #181 (A,wt=6): 197 -greater(zero,A) | greater(tau,A). [resolve(64,a,43,a)]. given #182 (F,wt=5): 310 -greater(zero,age(c1,c2)). [resolve(307,a,42,b)]. given #183 (T,wt=5): 312 smaller_or_equal(zero,age(c1,c2)). [resolve(311,a,37,b)]. given #184 (T,wt=6): 252 smaller_or_equal(age(c1,f3(c1)),eta). [resolve(160,a,159,a)]. given #185 (T,wt=6): 260 greater(A,B) | smaller_or_equal(A,B). [resolve(166,a,37,b),merge(c)]. given #186 (T,wt=6): 267 -greater(A,tau) | greater(A,sigma). [resolve(200,a,43,b)]. given #187 (A,wt=8): 204 -greater(A,age(c1,c2)) | greater(A,tau). [resolve(67,a,43,b)]. given #188 (T,wt=5): 315 greater(age(c1,c2),sigma). [resolve(267,a,67,a)]. given #189 (T,wt=5): 319 smaller(sigma,age(c1,c2)). [resolve(315,a,40,b)]. given #190 (T,wt=5): 320 smaller_or_equal(sigma,age(c1,c2)). [resolve(319,a,37,b)]. given #191 (T,wt=6): 268 -greater(sigma,A) | greater(tau,A). [resolve(200,a,43,a)]. given #192 (A,wt=8): 205 -greater(tau,A) | greater(age(c1,c2),A). [resolve(67,a,43,a)]. given #193 (F,wt=5): 318 -greater(sigma,age(c1,c2)). [resolve(315,a,42,b)]. given #194 (T,wt=6): 276 -greater(A,high) | greater(A,low). [resolve(275,a,43,b)]. given #195 (T,wt=6): 277 -greater(low,A) | greater(high,A). [resolve(275,a,43,a)]. given #196 (T,wt=6): 284 -greater(A,mod1) | greater(A,very_low). [resolve(282,a,43,b)]. given #197 (T,wt=6): 285 -greater(very_low,A) | greater(mod1,A). [resolve(282,a,43,a)]. given #198 (A,wt=10): 208 smaller(age(c1,c3),sigma) | age(c1,c3) = sigma. [resolve(68,a,39,c),flip(b)]. given #199 (T,wt=6): 288 -greater(A,high) | greater(A,very_low). [resolve(283,a,43,b)]. given #200 (T,wt=6): 289 -greater(very_low,A) | greater(high,A). [resolve(283,a,43,a)]. given #201 (T,wt=6): 295 -greater(A,mod2) | greater(A,very_low). [resolve(294,a,43,b)]. given #202 (T,wt=6): 296 -greater(very_low,A) | greater(mod2,A). [resolve(294,a,43,a)]. given #203 (A,wt=8): 209 -greater(A,age(c1,c4)) | greater(A,sigma). [resolve(69,a,43,b)]. given #204 (T,wt=7): 271 dissimilar(c1,c5,A) | is_aligned(c1,A). [resolve(230,a,125,a)]. given #205 (T,wt=7): 272 is_aligned(c1,A) | dissimilar(c1,A,c5). [resolve(230,a,124,c)]. given #206 (T,wt=8): 210 -greater(sigma,A) | greater(age(c1,c4),A). [resolve(69,a,43,a)]. given #207 (T,wt=8): 274 is_aligned(c1,c2) | hazard_of_mortality(c1,c2) = mod1. [resolve(247,a,131,b)]. given #208 (A,wt=10): 213 smaller(age(c1,c4),tau) | age(c1,c4) = tau. [resolve(70,a,39,c),flip(b)]. given #209 (T,wt=8): 302 -greater(A,age(c1,c4)) | greater(A,zero). [resolve(301,a,43,b)]. given #210 (T,wt=8): 303 -greater(zero,A) | greater(age(c1,c4),A). [resolve(301,a,43,a)]. given #211 (T,wt=8): 308 -greater(A,age(c1,c2)) | greater(A,zero). [resolve(307,a,43,b)]. given #212 (T,wt=8): 309 -greater(zero,A) | greater(age(c1,c2),A). [resolve(307,a,43,a)]. given #213 (A,wt=15): 220 is_aligned(A,B) | -has_endowment(A) | smaller(zero,age(A,B)) | greater(zero,age(A,B)). [resolve(90,a,44,b)]. given #214 (T,wt=8): 316 -greater(A,age(c1,c2)) | greater(A,sigma). [resolve(315,a,43,b)]. given #215 (T,wt=8): 317 -greater(sigma,A) | greater(age(c1,c2),A). [resolve(315,a,43,a)]. given #216 (T,wt=8): 334 smaller(age(c1,c3),sigma) | -positional_advantage(c1,c3). [para(208(b,1),144(a,1)),unit_del(b,201)]. given #217 (T,wt=8): 336 is_aligned(c1,c2) | smaller_or_equal(mod1,hazard_of_mortality(c1,c2)). [resolve(274,b,38,b)]. given #218 (A,wt=15): 221 is_aligned(A,B) | -has_endowment(A) | smaller(age(A,B),zero) | greater(age(A,B),zero). [resolve(90,a,44,b(flip))]. given #219 (T,wt=8): 337 is_aligned(c1,c2) | smaller_or_equal(hazard_of_mortality(c1,c2),mod1). [resolve(274,b,38,b(flip))]. given #220 (T,wt=8): 353 smaller(age(c1,c4),tau) | -positional_advantage(c1,c4). [para(213(b,1),144(a,1)),unit_del(b,165)]. given #221 (T,wt=9): 233 dissimilar(c1,c5,A) | -greater(age(c1,A),sigma). [resolve(127,a,72,a)]. given #222 (T,wt=4): 361 dissimilar(c1,c5,c2). [resolve(233,b,315,a)]. given #223 (A,wt=17): 223 is_aligned(A,B) | -dissimilar(A,C,D) | smaller(zero,age(A,B)) | greater(zero,age(A,B)). [resolve(91,a,44,b)]. given #224 (F,wt=3): 363 -is_aligned(c1,c2). [resolve(361,a,48,c),unit_del(a,230)]. given #225 (T,wt=4): 362 dissimilar(c1,c5,c4). [resolve(233,b,69,a)]. given #226 (T,wt=5): 366 hazard_of_mortality(c1,c2) = mod1. [back_unit_del(274),unit_del(a,363)]. given #227 (T,wt=8): 368 smaller(age(c1,c4),tau) | zero != tau. [back_unit_del(346),unit_del(c,367)]. given #228 (T,wt=8): 369 positional_advantage(c1,c4) | -smaller(hazard_of_mortality(c1,c3),high). [back_unit_del(239),unit_del(a,367)]. given #229 (A,wt=17): 224 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 #230 (F,wt=3): 367 -is_aligned(c1,c4). [resolve(362,a,48,c),unit_del(a,230)]. given #231 (T,wt=9): 248 greater(age(c1,A),sigma) | -dissimilar(c1,c5,A). [resolve(157,a,72,a)]. given #232 (T,wt=8): 372 greater(age(c1,A),sigma) | is_aligned(c1,A). [resolve(248,b,271,a)]. given #233 (T,wt=10): 314 greater(age(A,B),eta) | has_immunity(A,B) | -has_endowment(A). [resolve(260,b,45,a)]. given #234 (T,wt=10): 321 smaller(age(c1,c3),sigma) | smaller_or_equal(sigma,age(c1,c3)). [resolve(208,b,38,b)]. given #235 (A,wt=21): 225 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 #236 (T,w