============================== Prover9 =============================== Prover9 (32) version June-2006B, June 2006. Process 3674 was started by zalta on mally, Wed Jun 14 16:57:37 2006 The command was "prove". ============================== end of head =========================== ============================== INPUT ================================= set(auto2). % set(auto2) -> set(auto). % set(auto) -> set(auto_inference). % set(auto_inference) -> set(predicate_elim). % set(auto_inference) -> assign(eq_defs, unfold). % set(auto) -> set(auto_limits). % set(auto_limits) -> assign(max_weight, 100). % set(auto_limits) -> assign(sos_limit, 10000). % set(auto2) -> set(fof_reduction). % set(auto2) -> assign(new_constants, 1). % set(auto2) -> assign(fold_denial_max, 3). % set(auto2) -> assign(max_weight, 200). % set(auto2) -> assign(nest_penalty, 1). % set(auto2) -> assign(skolem_penalty, 3). % set(auto2) -> assign(sk_constant_weight, 0). % set(auto2) -> assign(prop_atom_weight, 5). % set(auto2) -> set(sort_initial_sos). % set(auto2) -> assign(sos_limit, -1). % set(auto2) -> assign(lrs_ticks, 3000). % set(auto2) -> assign(max_megs, 400). % set(auto2) -> assign(stats, some). % set(auto2) -> clear(echo_input). % set(auto2) -> set(quiet). % set(auto2) -> clear(print_subproblems). % set(auto2) -> clear(print_initial_clauses). % set(auto2) -> clear(print_given). set(print_initial_clauses). set(print_given). % formulas(sos). % not echoed (3 formulas) ============================== end of input ========================== Attempting problem reduction; original problem has = <94,53>. Problem reduction (0.00 sec) gives 2 independent subproblems: ( ). Max nnf_size of subproblems is 202; max cnf_max is 42. ============================== FOF REDUCTION MULTISEARCH ============= Starting Subproblem 1 of 2. Child search process 3675 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: clauses(usable). end_of_list. clauses(sos). 1 Object(c1). [clausify]. 2 Property(c2). [clausify]. 3 Property(c3). [clausify]. 4 IsTheFormOf(c1,c2). [clausify]. 5 Enc(c1,c3). [clausify]. 6 - Implies(c2,c3). [clausify]. 7 - Object(x) | - Property(y) | IsAFormOf(x,y) | - IsTheFormOf(x,y). [clausify]. 8 - Object(x) | Ex1(A,x,W) | - Property(y) | - IsAFormOf(x,y). [clausify]. 9 - Object(x) | - Property(y) | - IsAFormOf(z,y) | z = x | - IsTheFormOf(x,y). [clausify]. 10 - Object(x) | - Property(y) | - Property(z) | Enc(x,z) | - Implies(y,z) | - IsAFormOf(x,y). [clausify]. 11 - Object(x) | - Property(y) | - Property(z) | Implies(y,z) | - Enc(x,z) | - IsAFormOf(x,y). [clausify]. 12 - Object(x) | - Property(y) | IsTheFormOf(x,y) | - IsAFormOf(x,y) | IsAFormOf(f7(x,y),y). [clausify]. 13 - Object(x) | - Property(y) | IsTheFormOf(x,y) | - IsAFormOf(x,y) | f7(x,y) != x. [clausify]. 14 - Object(x) | - Property(y) | - IsAFormOf(z,y) | z = x | - IsAFormOf(x,y) | IsAFormOf(f8(x,y),y). [clausify]. 15 - Object(x) | - Property(y) | - IsAFormOf(z,y) | z = x | - IsAFormOf(x,y) | f8(x,y) != x. [clausify]. 16 - Object(x) | - Ex1(A,x,W) | - Property(y) | IsAFormOf(x,y) | Property(f1(x,y)) | Property(f2(x,y)). [clausify]. 17 - Object(x) | - Ex1(A,x,W) | - Property(y) | IsAFormOf(x,y) | Property(f1(x,y)) | - Enc(x,f2(x,y)). [clausify]. 18 - Object(x) | - Ex1(A,x,W) | - Property(y) | IsAFormOf(x,y) | Property(f1(x,y)) | Implies(y,f2(x,y)). [clausify]. 19 - Object(x) | - Ex1(A,x,W) | - Property(y) | IsAFormOf(x,y) | Enc(x,f1(x,y)) | Property(f2(x,y)). [clausify]. 20 - Object(x) | - Ex1(A,x,W) | - Property(y) | IsAFormOf(x,y) | - Implies(y,f1(x,y)) | Property(f2(x,y)). [clausify]. 21 - Object(x) | - Ex1(A,x,W) | - Property(y) | IsAFormOf(x,y) | Enc(x,f1(x,y)) | - Enc(x,f2(x,y)). [clausify]. 22 - Object(x) | - Ex1(A,x,W) | - Property(y) | IsAFormOf(x,y) | Enc(x,f1(x,y)) | Implies(y,f2(x,y)). [clausify]. 23 - Object(x) | - Ex1(A,x,W) | - Property(y) | IsAFormOf(x,y) | - Implies(y,f1(x,y)) | - Enc(x,f2(x,y)). [clausify]. 24 - Object(x) | - Ex1(A,x,W) | - Property(y) | IsAFormOf(x,y) | - Implies(y,f1(x,y)) | Implies(y,f2(x,y)). [clausify]. 25 - Object(x) | - Ex1(A,x,W) | - Property(y) | - Property(z) | Enc(x,z) | - Implies(y,z) | Property(f3(x,y)) | Property(f4(x,y)). [clausify]. 26 - Object(x) | - Ex1(A,x,W) | - Property(y) | - Property(z) | Implies(y,z) | - Enc(x,z) | Property(f5(x,y)) | Property(f6(x,y)). [clausify]. 27 - Object(x) | - Ex1(A,x,W) | - Property(y) | - Property(z) | Enc(x,z) | - Implies(y,z) | Property(f3(x,y)) | - Enc(x,f4(x,y)). [clausify]. 28 - Object(x) | - Ex1(A,x,W) | - Property(y) | - Property(z) | Enc(x,z) | - Implies(y,z) | Property(f3(x,y)) | Implies(y,f4(x,y)). [clausify]. 29 - Object(x) | - Ex1(A,x,W) | - Property(y) | - Property(z) | Enc(x,z) | - Implies(y,z) | Enc(x,f3(x,y)) | Property(f4(x,y)). [clausify]. 30 - Object(x) | - Ex1(A,x,W) | - Property(y) | - Property(z) | Enc(x,z) | - Implies(y,z) | - Implies(y,f3(x,y)) | Property(f4(x,y)). [clausify]. 31 - Object(x) | - Ex1(A,x,W) | - Property(y) | - Property(z) | Implies(y,z) | - Enc(x,z) | Property(f5(x,y)) | - Enc(x,f6(x,y)). [clausify]. 32 - Object(x) | - Ex1(A,x,W) | - Property(y) | - Property(z) | Implies(y,z) | - Enc(x,z) | Property(f5(x,y)) | Implies(y,f6(x,y)). [clausify]. 33 - Object(x) | - Ex1(A,x,W) | - Property(y) | - Property(z) | Implies(y,z) | - Enc(x,z) | Enc(x,f5(x,y)) | Property(f6(x,y)). [clausify]. 34 - Object(x) | - Ex1(A,x,W) | - Property(y) | - Property(z) | Implies(y,z) | - Enc(x,z) | - Implies(y,f5(x,y)) | Property(f6(x,y)). [clausify]. 35 - Object(x) | - Ex1(A,x,W) | - Property(y) | - Property(z) | Enc(x,z) | - Implies(y,z) | Enc(x,f3(x,y)) | - Enc(x,f4(x,y)). [clausify]. 36 - Object(x) | - Ex1(A,x,W) | - Property(y) | - Property(z) | Enc(x,z) | - Implies(y,z) | Enc(x,f3(x,y)) | Implies(y,f4(x,y)). [clausify]. 37 - Object(x) | - Ex1(A,x,W) | - Property(y) | - Property(z) | Enc(x,z) | - Implies(y,z) | - Implies(y,f3(x,y)) | - Enc(x,f4(x,y)). [clausify]. 38 - Object(x) | - Ex1(A,x,W) | - Property(y) | - Property(z) | Enc(x,z) | - Implies(y,z) | - Implies(y,f3(x,y)) | Implies(y,f4(x,y)). [clausify]. 39 - Object(x) | - Ex1(A,x,W) | - Property(y) | - Property(z) | Implies(y,z) | - Enc(x,z) | Enc(x,f5(x,y)) | - Enc(x,f6(x,y)). [clausify]. 40 - Object(x) | - Ex1(A,x,W) | - Property(y) | - Property(z) | Implies(y,z) | - Enc(x,z) | Enc(x,f5(x,y)) | Implies(y,f6(x,y)). [clausify]. 41 - Object(x) | - Ex1(A,x,W) | - Property(y) | - Property(z) | Implies(y,z) | - Enc(x,z) | - Implies(y,f5(x,y)) | - Enc(x,f6(x,y)). [clausify]. 42 - Object(x) | - Ex1(A,x,W) | - Property(y) | - Property(z) | Implies(y,z) | - Enc(x,z) | - Implies(y,f5(x,y)) | Implies(y,f6(x,y)). [clausify]. end_of_list. clauses(demodulators). end_of_list. Term ordering decisions: ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: clauses(usable). end_of_list. clauses(sos). 79 Property(c2). [clausify]. 80 Property(c3). [clausify]. 81 IsTheFormOf(c1,c2). [clausify]. 82 Enc(c1,c3). [clausify]. 83 - Implies(c2,c3). [clausify]. 84 - Property(x) | IsAFormOf(c1,x) | - IsTheFormOf(c1,x). [resolve(7,a,1,a)]. 85 Ex1(A,c1,W) | - Property(x) | - IsAFormOf(c1,x). [resolve(8,a,1,a)]. 86 - Property(x) | - IsAFormOf(y,x) | c1 = y | - IsTheFormOf(c1,x). [copy(45),flip(c)]. 87 - Property(x) | - Property(y) | Enc(c1,y) | - Implies(x,y) | - IsAFormOf(c1,x). [resolve(10,a,1,a)]. 88 - Property(x) | - Property(y) | Implies(x,y) | - Enc(c1,y) | - IsAFormOf(c1,x). [resolve(11,a,1,a)]. 89 - Property(x) | IsTheFormOf(c1,x) | - IsAFormOf(c1,x) | IsAFormOf(f7(c1,x),x). [resolve(12,a,1,a)]. 90 - Property(x) | IsTheFormOf(c1,x) | - IsAFormOf(c1,x) | f7(c1,x) != c1. [resolve(13,a,1,a)]. 91 - Property(x) | - IsAFormOf(y,x) | c1 = y | - IsAFormOf(c1,x) | IsAFormOf(f8(c1,x),x). [copy(50),flip(c)]. 92 - Property(x) | - IsAFormOf(y,x) | c1 = y | - IsAFormOf(c1,x) | f8(c1,x) != c1. [copy(51),flip(c)]. 93 - Ex1(A,c1,W) | - Property(x) | IsAFormOf(c1,x) | Property(f1(c1,x)) | Property(f2(c1,x)). [resolve(16,a,1,a)]. 94 - Ex1(A,c1,W) | - Property(x) | IsAFormOf(c1,x) | Property(f1(c1,x)) | - Enc(c1,f2(c1,x)). [resolve(17,a,1,a)]. 95 - Ex1(A,c1,W) | - Property(x) | IsAFormOf(c1,x) | Property(f1(c1,x)) | Implies(x,f2(c1,x)). [resolve(18,a,1,a)]. 96 - Ex1(A,c1,W) | - Property(x) | IsAFormOf(c1,x) | Enc(c1,f1(c1,x)) | Property(f2(c1,x)). [resolve(19,a,1,a)]. 97 - Ex1(A,c1,W) | - Property(x) | IsAFormOf(c1,x) | - Implies(x,f1(c1,x)) | Property(f2(c1,x)). [resolve(20,a,1,a)]. 98 - Ex1(A,c1,W) | - Property(x) | IsAFormOf(c1,x) | Enc(c1,f1(c1,x)) | - Enc(c1,f2(c1,x)). [resolve(21,a,1,a)]. 99 - Ex1(A,c1,W) | - Property(x) | IsAFormOf(c1,x) | Enc(c1,f1(c1,x)) | Implies(x,f2(c1,x)). [resolve(22,a,1,a)]. 100 - Ex1(A,c1,W) | - Property(x) | IsAFormOf(c1,x) | - Implies(x,f1(c1,x)) | - Enc(c1,f2(c1,x)). [resolve(23,a,1,a)]. 101 - Ex1(A,c1,W) | - Property(x) | IsAFormOf(c1,x) | - Implies(x,f1(c1,x)) | Implies(x,f2(c1,x)). [resolve(24,a,1,a)]. 102 - Ex1(A,c1,W) | - Property(x) | - Property(y) | Enc(c1,y) | - Implies(x,y) | Property(f3(c1,x)) | Property(f4(c1,x)). [resolve(25,a,1,a)]. 103 - Ex1(A,c1,W) | - Property(x) | - Property(y) | Implies(x,y) | - Enc(c1,y) | Property(f5(c1,x)) | Property(f6(c1,x)). [resolve(26,a,1,a)]. 104 - Ex1(A,c1,W) | - Property(x) | - Property(y) | Enc(c1,y) | - Implies(x,y) | Property(f3(c1,x)) | - Enc(c1,f4(c1,x)). [resolve(27,a,1,a)]. 105 - Ex1(A,c1,W) | - Property(x) | - Property(y) | Enc(c1,y) | - Implies(x,y) | Property(f3(c1,x)) | Implies(x,f4(c1,x)). [resolve(28,a,1,a)]. 106 - Ex1(A,c1,W) | - Property(x) | - Property(y) | Enc(c1,y) | - Implies(x,y) | Enc(c1,f3(c1,x)) | Property(f4(c1,x)). [resolve(29,a,1,a)]. 107 - Ex1(A,c1,W) | - Property(x) | - Property(y) | Enc(c1,y) | - Implies(x,y) | - Implies(x,f3(c1,x)) | Property(f4(c1,x)). [resolve(30,a,1,a)]. 108 - Ex1(A,c1,W) | - Property(x) | - Property(y) | Implies(x,y) | - Enc(c1,y) | Property(f5(c1,x)) | - Enc(c1,f6(c1,x)). [resolve(31,a,1,a)]. 109 - Ex1(A,c1,W) | - Property(x) | - Property(y) | Implies(x,y) | - Enc(c1,y) | Property(f5(c1,x)) | Implies(x,f6(c1,x)). [resolve(32,a,1,a)]. 110 - Ex1(A,c1,W) | - Property(x) | - Property(y) | Implies(x,y) | - Enc(c1,y) | Enc(c1,f5(c1,x)) | Property(f6(c1,x)). [resolve(33,a,1,a)]. 111 - Ex1(A,c1,W) | - Property(x) | - Property(y) | Implies(x,y) | - Enc(c1,y) | - Implies(x,f5(c1,x)) | Property(f6(c1,x)). [resolve(34,a,1,a)]. 112 - Ex1(A,c1,W) | - Property(x) | - Property(y) | Enc(c1,y) | - Implies(x,y) | Enc(c1,f3(c1,x)) | - Enc(c1,f4(c1,x)). [resolve(35,a,1,a)]. 113 - Ex1(A,c1,W) | - Property(x) | - Property(y) | Enc(c1,y) | - Implies(x,y) | Enc(c1,f3(c1,x)) | Implies(x,f4(c1,x)). [resolve(36,a,1,a)]. 114 - Ex1(A,c1,W) | - Property(x) | - Property(y) | Enc(c1,y) | - Implies(x,y) | - Implies(x,f3(c1,x)) | - Enc(c1,f4(c1,x)). [resolve(37,a,1,a)]. 115 - Ex1(A,c1,W) | - Property(x) | - Property(y) | Enc(c1,y) | - Implies(x,y) | - Implies(x,f3(c1,x)) | Implies(x,f4(c1,x)). [resolve(38,a,1,a)]. 116 - Ex1(A,c1,W) | - Property(x) | - Property(y) | Implies(x,y) | - Enc(c1,y) | Enc(c1,f5(c1,x)) | - Enc(c1,f6(c1,x)). [resolve(39,a,1,a)]. 117 - Ex1(A,c1,W) | - Property(x) | - Property(y) | Implies(x,y) | - Enc(c1,y) | Enc(c1,f5(c1,x)) | Implies(x,f6(c1,x)). [resolve(40,a,1,a)]. 118 - Ex1(A,c1,W) | - Property(x) | - Property(y) | Implies(x,y) | - Enc(c1,y) | - Implies(x,f5(c1,x)) | - Enc(c1,f6(c1,x)). [resolve(41,a,1,a)]. 119 - Ex1(A,c1,W) | - Property(x) | - Property(y) | Implies(x,y) | - Enc(c1,y) | - Implies(x,f5(c1,x)) | Implies(x,f6(c1,x)). [resolve(42,a,1,a)]. 120 - Property(x) | Enc(c1,x) | - Implies(x,x) | - IsAFormOf(c1,x). [factor(87,a,b)]. 121 - Property(x) | Implies(x,x) | - Enc(c1,x) | - IsAFormOf(c1,x). [factor(88,a,b)]. 122 - Ex1(A,c1,W) | - Property(x) | Enc(c1,x) | - Implies(x,x) | Property(f3(c1,x)) | Property(f4(c1,x)). [factor(102,b,c)]. 123 - Ex1(A,c1,W) | - Property(x) | Implies(x,x) | - Enc(c1,x) | Property(f5(c1,x)) | Property(f6(c1,x)). [factor(103,b,c)]. 124 - Ex1(A,c1,W) | - Property(x) | Enc(c1,x) | - Implies(x,x) | Property(f3(c1,x)) | - Enc(c1,f4(c1,x)). [factor(104,b,c)]. 125 - Ex1(A,c1,W) | - Property(x) | Enc(c1,x) | - Implies(x,x) | Property(f3(c1,x)) | Implies(x,f4(c1,x)). [factor(105,b,c)]. 126 - Ex1(A,c1,W) | - Property(x) | Enc(c1,x) | - Implies(x,x) | Enc(c1,f3(c1,x)) | Property(f4(c1,x)). [factor(106,b,c)]. 127 - Ex1(A,c1,W) | - Property(x) | - Property(f3(c1,x)) | Enc(c1,f3(c1,x)) | - Implies(x,f3(c1,x)) | Property(f4(c1,x)). [factor(106,d,f)]. 128 - Ex1(A,c1,W) | - Property(x) | Enc(c1,x) | - Implies(x,x) | - Implies(x,f3(c1,x)) | Property(f4(c1,x)). [factor(107,b,c)]. 129 - Ex1(A,c1,W) | - Property(x) | Implies(x,x) | - Enc(c1,x) | Property(f5(c1,x)) | - Enc(c1,f6(c1,x)). [factor(108,b,c)]. 130 - Ex1(A,c1,W) | - Property(x) | - Property(f6(c1,x)) | Implies(x,f6(c1,x)) | - Enc(c1,f6(c1,x)) | Property(f5(c1,x)). [factor(108,e,g)]. 131 - Ex1(A,c1,W) | - Property(x) | Implies(x,x) | - Enc(c1,x) | Property(f5(c1,x)) | Implies(x,f6(c1,x)). [factor(109,b,c)]. 132 - Ex1(A,c1,W) | - Property(x) | Implies(x,x) | - Enc(c1,x) | Enc(c1,f5(c1,x)) | Property(f6(c1,x)). [factor(110,b,c)]. 133 - Ex1(A,c1,W) | - Property(x) | Implies(x,x) | - Enc(c1,x) | - Implies(x,f5(c1,x)) | Property(f6(c1,x)). [factor(111,b,c)]. 134 - Ex1(A,c1,W) | - Property(x) | Enc(c1,x) | - Implies(x,x) | Enc(c1,f3(c1,x)) | - Enc(c1,f4(c1,x)). [factor(112,b,c)]. 135 - Ex1(A,c1,W) | - Property(x) | - Property(f3(c1,x)) | Enc(c1,f3(c1,x)) | - Implies(x,f3(c1,x)) | - Enc(c1,f4(c1,x)). [factor(112,d,f)]. 136 - Ex1(A,c1,W) | - Property(x) | Enc(c1,x) | - Implies(x,x) | Enc(c1,f3(c1,x)) | Implies(x,f4(c1,x)). [factor(113,b,c)]. 137 - Ex1(A,c1,W) | - Property(x) | - Property(f3(c1,x)) | Enc(c1,f3(c1,x)) | - Implies(x,f3(c1,x)) | Implies(x,f4(c1,x)). [factor(113,d,f)]. 138 - Ex1(A,c1,W) | - Property(x) | Enc(c1,x) | - Implies(x,x) | - Implies(x,f3(c1,x)) | - Enc(c1,f4(c1,x)). [factor(114,b,c)]. 139 - Ex1(A,c1,W) | - Property(x) | Enc(c1,x) | - Implies(x,x) | - Implies(x,f3(c1,x)) | Implies(x,f4(c1,x)). [factor(115,b,c)]. 140 - Ex1(A,c1,W) | - Property(x) | Implies(x,x) | - Enc(c1,x) | Enc(c1,f5(c1,x)) | - Enc(c1,f6(c1,x)). [factor(116,b,c)]. 141 - Ex1(A,c1,W) | - Property(x) | - Property(f6(c1,x)) | Implies(x,f6(c1,x)) | - Enc(c1,f6(c1,x)) | Enc(c1,f5(c1,x)). [factor(116,e,g)]. 142 - Ex1(A,c1,W) | - Property(x) | Implies(x,x) | - Enc(c1,x) | Enc(c1,f5(c1,x)) | Implies(x,f6(c1,x)). [factor(117,b,c)]. 143 - Ex1(A,c1,W) | - Property(x) | Implies(x,x) | - Enc(c1,x) | - Implies(x,f5(c1,x)) | - Enc(c1,f6(c1,x)). [factor(118,b,c)]. 144 - Ex1(A,c1,W) | - Property(x) | - Property(f6(c1,x)) | Implies(x,f6(c1,x)) | - Enc(c1,f6(c1,x)) | - Implies(x,f5(c1,x)). [factor(118,e,g)]. 145 - Ex1(A,c1,W) | - Property(x) | Implies(x,x) | - Enc(c1,x) | - Implies(x,f5(c1,x)) | Implies(x,f6(c1,x)). [factor(119,b,c)]. end_of_list. clauses(demodulators). end_of_list. clauses(denials). end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.01 seconds. given #1 (I,wt=1): 79 Property(c2). [clausify]. given #2 (I,wt=1): 80 Property(c3). [clausify]. given #3 (I,wt=1): 81 IsTheFormOf(c1,c2). [clausify]. given #4 (I,wt=1): 82 Enc(c1,c3). [clausify]. given #5 (I,wt=1): 83 - Implies(c2,c3). [clausify]. given #6 (I,wt=6): 84 - Property(x) | IsAFormOf(c1,x) | - IsTheFormOf(c1,x). [resolve(7,a,1,a)]. given #7 (I,wt=7): 85 Ex1(A,c1,W) | - Property(x) | - IsAFormOf(c1,x). [resolve(8,a,1,a)]. given #8 (I,wt=9): 86 - Property(x) | - IsAFormOf(y,x) | c1 = y | - IsTheFormOf(c1,x). [copy(45),flip(c)]. given #9 (I,wt=11): 87 - Property(x) | - Property(y) | Enc(c1,y) | - Implies(x,y) | - IsAFormOf(c1,x). [resolve(10,a,1,a)]. given #10 (I,wt=11): 88 - Property(x) | - Property(y) | Implies(x,y) | - Enc(c1,y) | - IsAFormOf(c1,x). [resolve(11,a,1,a)]. ============================== PROOF ================================= % Proof 1 at 0.01 (+ 0.00) seconds. % Length of proof is 12. % Level of proof is 3. % Maximum clause weight is 11. % Given clauses 10. 1 Object(c1). [clausify]. 7 - Object(x) | - Property(y) | IsAFormOf(x,y) | - IsTheFormOf(x,y). [clausify]. 11 - Object(x) | - Property(y) | - Property(z) | Implies(y,z) | - Enc(x,z) | - IsAFormOf(x,y). [clausify]. 79 Property(c2). [clausify]. 80 Property(c3). [clausify]. 81 IsTheFormOf(c1,c2). [clausify]. 82 Enc(c1,c3). [clausify]. 83 - Implies(c2,c3). [clausify]. 84 - Property(x) | IsAFormOf(c1,x) | - IsTheFormOf(c1,x). [resolve(7,a,1,a)]. 88 - Property(x) | - Property(y) | Implies(x,y) | - Enc(c1,y) | - IsAFormOf(c1,x). [resolve(11,a,1,a)]. 146 IsAFormOf(c1,c2). [resolve(84,c,81,a),unit_del(a,79)]. 148 $F. [ur(88,a,79,a,b,80,a,c,83,a,d,82,a),unit_del(a,146)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=10. Generated=78. Kept=69. proofs=1. Usable=10. Sos=59. Demods=0. Denials=0. Limbo=0, Disabled=78. Hints=0. Megabytes=0.20. User_CPU=0.01, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 3675 exit (max_proofs) Wed Jun 14 16:57:37 2006 ============================== continuing FOF reduction multisearch == Starting Subproblem 2 of 2. Child search process 3676 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: clauses(usable). end_of_list. clauses(sos). 1 Object(c1). [clausify]. 2 Property(c2). [clausify]. 3 Property(c3). [clausify]. 4 IsTheFormOf(c1,c2). [clausify]. 5 Implies(c2,c3). [clausify]. 6 - Enc(c1,c3). [clausify]. 7 - Object(x) | - Property(y) | IsAFormOf(x,y) | - IsTheFormOf(x,y). [clausify]. 8 - Object(x) | Ex1(A,x,W) | - Property(y) | - IsAFormOf(x,y). [clausify]. 9 - Object(x) | - Property(y) | - IsAFormOf(z,y) | z = x | - IsTheFormOf(x,y). [clausify]. 10 - Object(x) | - Property(y) | - Property(z) | Enc(x,z) | - Implies(y,z) | - IsAFormOf(x,y). [clausify]. 11 - Object(x) | - Property(y) | - Property(z) | Implies(y,z) | - Enc(x,z) | - IsAFormOf(x,y). [clausify]. 12 - Object(x) | - Property(y) | IsTheFormOf(x,y) | - IsAFormOf(x,y) | IsAFormOf(f7(x,y),y). [clausify]. 13 - Object(x) | - Property(y) | IsTheFormOf(x,y) | - IsAFormOf(x,y) | f7(x,y) != x. [clausify]. 14 - Object(x) | - Property(y) | - IsAFormOf(z,y) | z = x | - IsAFormOf(x,y) | IsAFormOf(f8(x,y),y). [clausify]. 15 - Object(x) | - Property(y) | - IsAFormOf(z,y) | z = x | - IsAFormOf(x,y) | f8(x,y) != x. [clausify]. 16 - Object(x) | - Ex1(A,x,W) | - Property(y) | IsAFormOf(x,y) | Property(f1(x,y)) | Property(f2(x,y)). [clausify]. 17 - Object(x) | - Ex1(A,x,W) | - Property(y) | IsAFormOf(x,y) | Property(f1(x,y)) | - Enc(x,f2(x,y)). [clausify]. 18 - Object(x) | - Ex1(A,x,W) | - Property(y) | IsAFormOf(x,y) | Property(f1(x,y)) | Implies(y,f2(x,y)). [clausify]. 19 - Object(x) | - Ex1(A,x,W) | - Property(y) | IsAFormOf(x,y) | Enc(x,f1(x,y)) | Property(f2(x,y)). [clausify]. 20 - Object(x) | - Ex1(A,x,W) | - Property(y) | IsAFormOf(x,y) | - Implies(y,f1(x,y)) | Property(f2(x,y)). [clausify]. 21 - Object(x) | - Ex1(A,x,W) | - Property(y) | IsAFormOf(x,y) | Enc(x,f1(x,y)) | - Enc(x,f2(x,y)). [clausify]. 22 - Object(x) | - Ex1(A,x,W) | - Property(y) | IsAFormOf(x,y) | Enc(x,f1(x,y)) | Implies(y,f2(x,y)). [clausify]. 23 - Object(x) | - Ex1(A,x,W) | - Property(y) | IsAFormOf(x,y) | - Implies(y,f1(x,y)) | - Enc(x,f2(x,y)). [clausify]. 24 - Object(x) | - Ex1(A,x,W) | - Property(y) | IsAFormOf(x,y) | - Implies(y,f1(x,y)) | Implies(y,f2(x,y)). [clausify]. 25 - Object(x) | - Ex1(A,x,W) | - Property(y) | - Property(z) | Enc(x,z) | - Implies(y,z) | Property(f3(x,y)) | Property(f4(x,y)). [clausify]. 26 - Object(x) | - Ex1(A,x,W) | - Property(y) | - Property(z) | Implies(y,z) | - Enc(x,z) | Property(f5(x,y)) | Property(f6(x,y)). [clausify]. 27 - Object(x) | - Ex1(A,x,W) | - Property(y) | - Property(z) | Enc(x,z) | - Implies(y,z) | Property(f3(x,y)) | - Enc(x,f4(x,y)). [clausify]. 28 - Object(x) | - Ex1(A,x,W) | - Property(y) | - Property(z) | Enc(x,z) | - Implies(y,z) | Property(f3(x,y)) | Implies(y,f4(x,y)). [clausify]. 29 - Object(x) | - Ex1(A,x,W) | - Property(y) | - Property(z) | Enc(x,z) | - Implies(y,z) | Enc(x,f3(x,y)) | Property(f4(x,y)). [clausify]. 30 - Object(x) | - Ex1(A,x,W) | - Property(y) | - Property(z) | Enc(x,z) | - Implies(y,z) | - Implies(y,f3(x,y)) | Property(f4(x,y)). [clausify]. 31 - Object(x) | - Ex1(A,x,W) | - Property(y) | - Property(z) | Implies(y,z) | - Enc(x,z) | Property(f5(x,y)) | - Enc(x,f6(x,y)). [clausify]. 32 - Object(x) | - Ex1(A,x,W) | - Property(y) | - Property(z) | Implies(y,z) | - Enc(x,z) | Property(f5(x,y)) | Implies(y,f6(x,y)). [clausify]. 33 - Object(x) | - Ex1(A,x,W) | - Property(y) | - Property(z) | Implies(y,z) | - Enc(x,z) | Enc(x,f5(x,y)) | Property(f6(x,y)). [clausify]. 34 - Object(x) | - Ex1(A,x,W) | - Property(y) | - Property(z) | Implies(y,z) | - Enc(x,z) | - Implies(y,f5(x,y)) | Property(f6(x,y)). [clausify]. 35 - Object(x) | - Ex1(A,x,W) | - Property(y) | - Property(z) | Enc(x,z) | - Implies(y,z) | Enc(x,f3(x,y)) | - Enc(x,f4(x,y)). [clausify]. 36 - Object(x) | - Ex1(A,x,W) | - Property(y) | - Property(z) | Enc(x,z) | - Implies(y,z) | Enc(x,f3(x,y)) | Implies(y,f4(x,y)). [clausify]. 37 - Object(x) | - Ex1(A,x,W) | - Property(y) | - Property(z) | Enc(x,z) | - Implies(y,z) | - Implies(y,f3(x,y)) | - Enc(x,f4(x,y)). [clausify]. 38 - Object(x) | - Ex1(A,x,W) | - Property(y) | - Property(z) | Enc(x,z) | - Implies(y,z) | - Implies(y,f3(x,y)) | Implies(y,f4(x,y)). [clausify]. 39 - Object(x) | - Ex1(A,x,W) | - Property(y) | - Property(z) | Implies(y,z) | - Enc(x,z) | Enc(x,f5(x,y)) | - Enc(x,f6(x,y)). [clausify]. 40 - Object(x) | - Ex1(A,x,W) | - Property(y) | - Property(z) | Implies(y,z) | - Enc(x,z) | Enc(x,f5(x,y)) | Implies(y,f6(x,y)). [clausify]. 41 - Object(x) | - Ex1(A,x,W) | - Property(y) | - Property(z) | Implies(y,z) | - Enc(x,z) | - Implies(y,f5(x,y)) | - Enc(x,f6(x,y)). [clausify]. 42 - Object(x) | - Ex1(A,x,W) | - Property(y) | - Property(z) | Implies(y,z) | - Enc(x,z) | - Implies(y,f5(x,y)) | Implies(y,f6(x,y)). [clausify]. end_of_list. clauses(demodulators). end_of_list. Term ordering decisions: ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: clauses(usable). end_of_list. clauses(sos). 79 Property(c2). [clausify]. 80 Property(c3). [clausify]. 81 IsTheFormOf(c1,c2). [clausify]. 82 Implies(c2,c3). [clausify]. 83 - Enc(c1,c3). [clausify]. 84 - Property(x) | IsAFormOf(c1,x) | - IsTheFormOf(c1,x). [resolve(7,a,1,a)]. 85 Ex1(A,c1,W) | - Property(x) | - IsAFormOf(c1,x). [resolve(8,a,1,a)]. 86 - Property(x) | - IsAFormOf(y,x) | c1 = y | - IsTheFormOf(c1,x). [copy(45),flip(c)]. 87 - Property(x) | - Property(y) | Enc(c1,y) | - Implies(x,y) | - IsAFormOf(c1,x). [resolve(10,a,1,a)]. 88 - Property(x) | - Property(y) | Implies(x,y) | - Enc(c1,y) | - IsAFormOf(c1,x). [resolve(11,a,1,a)]. 89 - Property(x) | IsTheFormOf(c1,x) | - IsAFormOf(c1,x) | IsAFormOf(f7(c1,x),x). [resolve(12,a,1,a)]. 90 - Property(x) | IsTheFormOf(c1,x) | - IsAFormOf(c1,x) | f7(c1,x) != c1. [resolve(13,a,1,a)]. 91 - Property(x) | - IsAFormOf(y,x) | c1 = y | - IsAFormOf(c1,x) | IsAFormOf(f8(c1,x),x). [copy(50),flip(c)]. 92 - Property(x) | - IsAFormOf(y,x) | c1 = y | - IsAFormOf(c1,x) | f8(c1,x) != c1. [copy(51),flip(c)]. 93 - Ex1(A,c1,W) | - Property(x) | IsAFormOf(c1,x) | Property(f1(c1,x)) | Property(f2(c1,x)). [resolve(16,a,1,a)]. 94 - Ex1(A,c1,W) | - Property(x) | IsAFormOf(c1,x) | Property(f1(c1,x)) | - Enc(c1,f2(c1,x)). [resolve(17,a,1,a)]. 95 - Ex1(A,c1,W) | - Property(x) | IsAFormOf(c1,x) | Property(f1(c1,x)) | Implies(x,f2(c1,x)). [resolve(18,a,1,a)]. 96 - Ex1(A,c1,W) | - Property(x) | IsAFormOf(c1,x) | Enc(c1,f1(c1,x)) | Property(f2(c1,x)). [resolve(19,a,1,a)]. 97 - Ex1(A,c1,W) | - Property(x) | IsAFormOf(c1,x) | - Implies(x,f1(c1,x)) | Property(f2(c1,x)). [resolve(20,a,1,a)]. 98 - Ex1(A,c1,W) | - Property(x) | IsAFormOf(c1,x) | Enc(c1,f1(c1,x)) | - Enc(c1,f2(c1,x)). [resolve(21,a,1,a)]. 99 - Ex1(A,c1,W) | - Property(x) | IsAFormOf(c1,x) | Enc(c1,f1(c1,x)) | Implies(x,f2(c1,x)). [resolve(22,a,1,a)]. 100 - Ex1(A,c1,W) | - Property(x) | IsAFormOf(c1,x) | - Implies(x,f1(c1,x)) | - Enc(c1,f2(c1,x)). [resolve(23,a,1,a)]. 101 - Ex1(A,c1,W) | - Property(x) | IsAFormOf(c1,x) | - Implies(x,f1(c1,x)) | Implies(x,f2(c1,x)). [resolve(24,a,1,a)]. 102 - Ex1(A,c1,W) | - Property(x) | - Property(y) | Enc(c1,y) | - Implies(x,y) | Property(f3(c1,x)) | Property(f4(c1,x)). [resolve(25,a,1,a)]. 103 - Ex1(A,c1,W) | - Property(x) | - Property(y) | Implies(x,y) | - Enc(c1,y) | Property(f5(c1,x)) | Property(f6(c1,x)). [resolve(26,a,1,a)]. 104 - Ex1(A,c1,W) | - Property(x) | - Property(y) | Enc(c1,y) | - Implies(x,y) | Property(f3(c1,x)) | - Enc(c1,f4(c1,x)). [resolve(27,a,1,a)]. 105 - Ex1(A,c1,W) | - Property(x) | - Property(y) | Enc(c1,y) | - Implies(x,y) | Property(f3(c1,x)) | Implies(x,f4(c1,x)). [resolve(28,a,1,a)]. 106 - Ex1(A,c1,W) | - Property(x) | - Property(y) | Enc(c1,y) | - Implies(x,y) | Enc(c1,f3(c1,x)) | Property(f4(c1,x)). [resolve(29,a,1,a)]. 107 - Ex1(A,c1,W) | - Property(x) | - Property(y) | Enc(c1,y) | - Implies(x,y) | - Implies(x,f3(c1,x)) | Property(f4(c1,x)). [resolve(30,a,1,a)]. 108 - Ex1(A,c1,W) | - Property(x) | - Property(y) | Implies(x,y) | - Enc(c1,y) | Property(f5(c1,x)) | - Enc(c1,f6(c1,x)). [resolve(31,a,1,a)]. 109 - Ex1(A,c1,W) | - Property(x) | - Property(y) | Implies(x,y) | - Enc(c1,y) | Property(f5(c1,x)) | Implies(x,f6(c1,x)). [resolve(32,a,1,a)]. 110 - Ex1(A,c1,W) | - Property(x) | - Property(y) | Implies(x,y) | - Enc(c1,y) | Enc(c1,f5(c1,x)) | Property(f6(c1,x)). [resolve(33,a,1,a)]. 111 - Ex1(A,c1,W) | - Property(x) | - Property(y) | Implies(x,y) | - Enc(c1,y) | - Implies(x,f5(c1,x)) | Property(f6(c1,x)). [resolve(34,a,1,a)]. 112 - Ex1(A,c1,W) | - Property(x) | - Property(y) | Enc(c1,y) | - Implies(x,y) | Enc(c1,f3(c1,x)) | - Enc(c1,f4(c1,x)). [resolve(35,a,1,a)]. 113 - Ex1(A,c1,W) | - Property(x) | - Property(y) | Enc(c1,y) | - Implies(x,y) | Enc(c1,f3(c1,x)) | Implies(x,f4(c1,x)). [resolve(36,a,1,a)]. 114 - Ex1(A,c1,W) | - Property(x) | - Property(y) | Enc(c1,y) | - Implies(x,y) | - Implies(x,f3(c1,x)) | - Enc(c1,f4(c1,x)). [resolve(37,a,1,a)]. 115 - Ex1(A,c1,W) | - Property(x) | - Property(y) | Enc(c1,y) | - Implies(x,y) | - Implies(x,f3(c1,x)) | Implies(x,f4(c1,x)). [resolve(38,a,1,a)]. 116 - Ex1(A,c1,W) | - Property(x) | - Property(y) | Implies(x,y) | - Enc(c1,y) | Enc(c1,f5(c1,x)) | - Enc(c1,f6(c1,x)). [resolve(39,a,1,a)]. 117 - Ex1(A,c1,W) | - Property(x) | - Property(y) | Implies(x,y) | - Enc(c1,y) | Enc(c1,f5(c1,x)) | Implies(x,f6(c1,x)). [resolve(40,a,1,a)]. 118 - Ex1(A,c1,W) | - Property(x) | - Property(y) | Implies(x,y) | - Enc(c1,y) | - Implies(x,f5(c1,x)) | - Enc(c1,f6(c1,x)). [resolve(41,a,1,a)]. 119 - Ex1(A,c1,W) | - Property(x) | - Property(y) | Implies(x,y) | - Enc(c1,y) | - Implies(x,f5(c1,x)) | Implies(x,f6(c1,x)). [resolve(42,a,1,a)]. 120 - Property(x) | Enc(c1,x) | - Implies(x,x) | - IsAFormOf(c1,x). [factor(87,a,b)]. 121 - Property(x) | Implies(x,x) | - Enc(c1,x) | - IsAFormOf(c1,x). [factor(88,a,b)]. 122 - Ex1(A,c1,W) | - Property(x) | Enc(c1,x) | - Implies(x,x) | Property(f3(c1,x)) | Property(f4(c1,x)). [factor(102,b,c)]. 123 - Ex1(A,c1,W) | - Property(x) | Implies(x,x) | - Enc(c1,x) | Property(f5(c1,x)) | Property(f6(c1,x)). [factor(103,b,c)]. 124 - Ex1(A,c1,W) | - Property(x) | Enc(c1,x) | - Implies(x,x) | Property(f3(c1,x)) | - Enc(c1,f4(c1,x)). [factor(104,b,c)]. 125 - Ex1(A,c1,W) | - Property(x) | Enc(c1,x) | - Implies(x,x) | Property(f3(c1,x)) | Implies(x,f4(c1,x)). [factor(105,b,c)]. 126 - Ex1(A,c1,W) | - Property(x) | Enc(c1,x) | - Implies(x,x) | Enc(c1,f3(c1,x)) | Property(f4(c1,x)). [factor(106,b,c)]. 127 - Ex1(A,c1,W) | - Property(x) | - Property(f3(c1,x)) | Enc(c1,f3(c1,x)) | - Implies(x,f3(c1,x)) | Property(f4(c1,x)). [factor(106,d,f)]. 128 - Ex1(A,c1,W) | - Property(x) | Enc(c1,x) | - Implies(x,x) | - Implies(x,f3(c1,x)) | Property(f4(c1,x)). [factor(107,b,c)]. 129 - Ex1(A,c1,W) | - Property(x) | Implies(x,x) | - Enc(c1,x) | Property(f5(c1,x)) | - Enc(c1,f6(c1,x)). [factor(108,b,c)]. 130 - Ex1(A,c1,W) | - Property(x) | - Property(f6(c1,x)) | Implies(x,f6(c1,x)) | - Enc(c1,f6(c1,x)) | Property(f5(c1,x)). [factor(108,e,g)]. 131 - Ex1(A,c1,W) | - Property(x) | Implies(x,x) | - Enc(c1,x) | Property(f5(c1,x)) | Implies(x,f6(c1,x)). [factor(109,b,c)]. 132 - Ex1(A,c1,W) | - Property(x) | Implies(x,x) | - Enc(c1,x) | Enc(c1,f5(c1,x)) | Property(f6(c1,x)). [factor(110,b,c)]. 133 - Ex1(A,c1,W) | - Property(x) | Implies(x,x) | - Enc(c1,x) | - Implies(x,f5(c1,x)) | Property(f6(c1,x)). [factor(111,b,c)]. 134 - Ex1(A,c1,W) | - Property(x) | Enc(c1,x) | - Implies(x,x) | Enc(c1,f3(c1,x)) | - Enc(c1,f4(c1,x)). [factor(112,b,c)]. 135 - Ex1(A,c1,W) | - Property(x) | - Property(f3(c1,x)) | Enc(c1,f3(c1,x)) | - Implies(x,f3(c1,x)) | - Enc(c1,f4(c1,x)). [factor(112,d,f)]. 136 - Ex1(A,c1,W) | - Property(x) | Enc(c1,x) | - Implies(x,x) | Enc(c1,f3(c1,x)) | Implies(x,f4(c1,x)). [factor(113,b,c)]. 137 - Ex1(A,c1,W) | - Property(x) | - Property(f3(c1,x)) | Enc(c1,f3(c1,x)) | - Implies(x,f3(c1,x)) | Implies(x,f4(c1,x)). [factor(113,d,f)]. 138 - Ex1(A,c1,W) | - Property(x) | Enc(c1,x) | - Implies(x,x) | - Implies(x,f3(c1,x)) | - Enc(c1,f4(c1,x)). [factor(114,b,c)]. 139 - Ex1(A,c1,W) | - Property(x) | Enc(c1,x) | - Implies(x,x) | - Implies(x,f3(c1,x)) | Implies(x,f4(c1,x)). [factor(115,b,c)]. 140 - Ex1(A,c1,W) | - Property(x) | Implies(x,x) | - Enc(c1,x) | Enc(c1,f5(c1,x)) | - Enc(c1,f6(c1,x)). [factor(116,b,c)]. 141 - Ex1(A,c1,W) | - Property(x) | - Property(f6(c1,x)) | Implies(x,f6(c1,x)) | - Enc(c1,f6(c1,x)) | Enc(c1,f5(c1,x)). [factor(116,e,g)]. 142 - Ex1(A,c1,W) | - Property(x) | Implies(x,x) | - Enc(c1,x) | Enc(c1,f5(c1,x)) | Implies(x,f6(c1,x)). [factor(117,b,c)]. 143 - Ex1(A,c1,W) | - Property(x) | Implies(x,x) | - Enc(c1,x) | - Implies(x,f5(c1,x)) | - Enc(c1,f6(c1,x)). [factor(118,b,c)]. 144 - Ex1(A,c1,W) | - Property(x) | - Property(f6(c1,x)) | Implies(x,f6(c1,x)) | - Enc(c1,f6(c1,x)) | - Implies(x,f5(c1,x)). [factor(118,e,g)]. 145 - Ex1(A,c1,W) | - Property(x) | Implies(x,x) | - Enc(c1,x) | - Implies(x,f5(c1,x)) | Implies(x,f6(c1,x)). [factor(119,b,c)]. end_of_list. clauses(demodulators). end_of_list. clauses(denials). end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.01 seconds. given #1 (I,wt=1): 79 Property(c2). [clausify]. given #2 (I,wt=1): 80 Property(c3). [clausify]. given #3 (I,wt=1): 81 IsTheFormOf(c1,c2). [clausify]. given #4 (I,wt=1): 82 Implies(c2,c3). [clausify]. given #5 (I,wt=1): 83 - Enc(c1,c3). [clausify]. given #6 (I,wt=6): 84 - Property(x) | IsAFormOf(c1,x) | - IsTheFormOf(c1,x). [resolve(7,a,1,a)]. given #7 (I,wt=7): 85 Ex1(A,c1,W) | - Property(x) | - IsAFormOf(c1,x). [resolve(8,a,1,a)]. given #8 (I,wt=9): 86 - Property(x) | - IsAFormOf(y,x) | c1 = y | - IsTheFormOf(c1,x). [copy(45),flip(c)]. given #9 (I,wt=11): 87 - Property(x) | - Property(y) | Enc(c1,y) | - Implies(x,y) | - IsAFormOf(c1,x). [resolve(10,a,1,a)]. ============================== PROOF ================================= % Proof 1 at 0.01 (+ 0.00) seconds. % Length of proof is 12. % Level of proof is 3. % Maximum clause weight is 11. % Given clauses 9. 1 Object(c1). [clausify]. 7 - Object(x) | - Property(y) | IsAFormOf(x,y) | - IsTheFormOf(x,y). [clausify]. 10 - Object(x) | - Property(y) | - Property(z) | Enc(x,z) | - Implies(y,z) | - IsAFormOf(x,y). [clausify]. 79 Property(c2). [clausify]. 80 Property(c3). [clausify]. 81 IsTheFormOf(c1,c2). [clausify]. 82 Implies(c2,c3). [clausify]. 83 - Enc(c1,c3). [clausify]. 84 - Property(x) | IsAFormOf(c1,x) | - IsTheFormOf(c1,x). [resolve(7,a,1,a)]. 87 - Property(x) | - Property(y) | Enc(c1,y) | - Implies(x,y) | - IsAFormOf(c1,x). [resolve(10,a,1,a)]. 146 IsAFormOf(c1,c2). [resolve(84,c,81,a),unit_del(a,79)]. 148 $F. [ur(87,a,79,a,b,80,a,c,83,a,d,82,a),unit_del(a,146)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=9. Generated=78. Kept=69. proofs=1. Usable=9. Sos=60. Demods=0. Denials=0. Limbo=0, Disabled=78. Hints=0. Megabytes=0.20. User_CPU=0.01, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 3676 exit (max_proofs) Wed Jun 14 16:57:37 2006 ============================== end of multisearch ==================== All 2 subproblems have been proved, so we are done. Total user_CPU=0.02, system_CPU=0.01, wall_clock=0. THEOREM PROVED Exiting. Process 3674 exit (max_proofs) Wed Jun 14 16:57:37 2006