%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SEU140+1 : TPTP v8.2.0. Released v3.3.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n032.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Jun 24 15:01:16 EDT 2024 % Result : Theorem 7.07s 7.17s % Output : CNFRefutation 7.07s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.05/0.09 % Problem : SEU140+1 : TPTP v8.2.0. Released v3.3.0. % 0.05/0.09 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.08/0.28 % Computer : n032.cluster.edu % 0.08/0.28 % Model : x86_64 x86_64 % 0.08/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.28 % Memory : 8042.1875MB % 0.08/0.28 % OS : Linux 3.10.0-693.el7.x86_64 % 0.08/0.28 % CPULimit : 300 % 0.08/0.28 % WCLimit : 300 % 0.08/0.28 % DateTime : Fri Jun 21 12:28:08 EDT 2024 % 0.08/0.28 % CPUTime : % 0.13/0.47 start to proof:theBenchmark % 7.07/7.16 %------------------------------------------- % 7.07/7.16 % File :CSE---1.7 % 7.07/7.16 % Problem :theBenchmark % 7.07/7.16 % Transform :cnf % 7.07/7.16 % Format :tptp:raw % 7.07/7.16 % Command :java -jar mcs_scs.jar %d %s % 7.07/7.16 % 7.07/7.16 % Result :Theorem 6.660000s % 7.07/7.16 % Output :CNFRefutation 6.660000s % 7.07/7.16 %------------------------------------------- % 7.07/7.16 %------------------------------------------------------------------------------ % 7.07/7.16 % File : SEU140+1 : TPTP v8.2.0. Released v3.3.0. % 7.07/7.16 % Domain : Set theory % 7.07/7.16 % Problem : MPTP bushy problem t63_xboole_1 % 7.07/7.16 % Version : [Urb07] axioms : Especial. % 7.07/7.16 % English : % 7.07/7.16 % 7.07/7.16 % Refs : [Ban01] Bancerek et al. (2001), On the Characterizations of Co % 7.07/7.16 % : [Urb07] Urban (2006), Email to G. Sutcliffe % 7.07/7.16 % Source : [Urb07] % 7.07/7.17 % Names : bushy-t63_xboole_1 [Urb07] % 7.07/7.17 % 7.07/7.17 % Status : Theorem % 7.07/7.17 % Rating : 0.11 v8.1.0, 0.14 v7.5.0, 0.16 v7.4.0, 0.07 v7.1.0, 0.09 v7.0.0, 0.10 v6.4.0, 0.15 v6.3.0, 0.17 v6.2.0, 0.20 v6.1.0, 0.23 v6.0.0, 0.26 v5.5.0, 0.22 v5.4.0, 0.32 v5.3.0, 0.37 v5.2.0, 0.10 v5.0.0, 0.12 v4.1.0, 0.13 v4.0.0, 0.17 v3.7.0, 0.15 v3.5.0, 0.16 v3.3.0 % 7.07/7.17 % Syntax : Number of formulae : 18 ( 9 unt; 0 def) % 7.07/7.17 % Number of atoms : 29 ( 7 equ) % 7.07/7.17 % Maximal formula atoms : 3 ( 1 avg) % 7.07/7.17 % Number of connectives : 16 ( 5 ~; 0 |; 4 &) % 7.07/7.17 % ( 1 <=>; 6 =>; 0 <=; 0 <~>) % 7.07/7.17 % Maximal formula depth : 7 ( 3 avg) % 7.07/7.17 % Maximal term depth : 2 ( 1 avg) % 7.07/7.17 % Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty) % 7.07/7.17 % Number of functors : 2 ( 2 usr; 1 con; 0-2 aty) % 7.07/7.17 % Number of variables : 27 ( 25 !; 2 ?) % 7.07/7.17 % SPC : FOF_THM_RFO_SEQ % 7.07/7.17 % 7.07/7.17 % Comments : Translated by MPTP 0.2 from the original problem in the Mizar % 7.07/7.17 % library, www.mizar.org % 7.07/7.17 %------------------------------------------------------------------------------ % 7.07/7.17 fof(antisymmetry_r2_hidden,axiom, % 7.07/7.17 ! [A,B] : % 7.07/7.17 ( in(A,B) % 7.07/7.17 => ~ in(B,A) ) ). % 7.07/7.17 % 7.07/7.17 fof(commutativity_k3_xboole_0,axiom, % 7.07/7.17 ! [A,B] : set_intersection2(A,B) = set_intersection2(B,A) ). % 7.07/7.17 % 7.07/7.17 fof(d7_xboole_0,axiom, % 7.07/7.17 ! [A,B] : % 7.07/7.17 ( disjoint(A,B) % 7.07/7.17 <=> set_intersection2(A,B) = empty_set ) ). % 7.07/7.17 % 7.07/7.17 fof(dt_k1_xboole_0,axiom, % 7.07/7.17 $true ). % 7.07/7.17 % 7.07/7.17 fof(dt_k3_xboole_0,axiom, % 7.07/7.17 $true ). % 7.07/7.17 % 7.07/7.17 fof(fc1_xboole_0,axiom, % 7.07/7.17 empty(empty_set) ). % 7.07/7.17 % 7.07/7.17 fof(idempotence_k3_xboole_0,axiom, % 7.07/7.17 ! [A,B] : set_intersection2(A,A) = A ). % 7.07/7.17 % 7.07/7.17 fof(rc1_xboole_0,axiom, % 7.07/7.17 ? [A] : empty(A) ). % 7.07/7.17 % 7.07/7.17 fof(rc2_xboole_0,axiom, % 7.07/7.17 ? [A] : ~ empty(A) ). % 7.07/7.17 % 7.07/7.17 fof(reflexivity_r1_tarski,axiom, % 7.07/7.17 ! [A,B] : subset(A,A) ). % 7.07/7.17 % 7.07/7.17 fof(symmetry_r1_xboole_0,axiom, % 7.07/7.17 ! [A,B] : % 7.07/7.17 ( disjoint(A,B) % 7.07/7.17 => disjoint(B,A) ) ). % 7.07/7.17 % 7.07/7.17 fof(t26_xboole_1,axiom, % 7.07/7.17 ! [A,B,C] : % 7.07/7.17 ( subset(A,B) % 7.07/7.17 => subset(set_intersection2(A,C),set_intersection2(B,C)) ) ). % 7.07/7.17 % 7.07/7.17 fof(t2_boole,axiom, % 7.07/7.17 ! [A] : set_intersection2(A,empty_set) = empty_set ). % 7.07/7.17 % 7.07/7.17 fof(t3_xboole_1,axiom, % 7.07/7.17 ! [A] : % 7.07/7.17 ( subset(A,empty_set) % 7.07/7.17 => A = empty_set ) ). % 7.07/7.17 % 7.07/7.17 fof(t63_xboole_1,conjecture, % 7.07/7.17 ! [A,B,C] : % 7.07/7.17 ( ( subset(A,B) % 7.07/7.17 & disjoint(B,C) ) % 7.07/7.17 => disjoint(A,C) ) ). % 7.07/7.17 % 7.07/7.17 fof(t6_boole,axiom, % 7.07/7.17 ! [A] : % 7.07/7.17 ( empty(A) % 7.07/7.17 => A = empty_set ) ). % 7.07/7.17 % 7.07/7.17 fof(t7_boole,axiom, % 7.07/7.17 ! [A,B] : % 7.07/7.17 ~ ( in(A,B) % 7.07/7.17 & empty(B) ) ). % 7.07/7.17 % 7.07/7.17 fof(t8_boole,axiom, % 7.07/7.17 ! [A,B] : % 7.07/7.17 ~ ( empty(A) % 7.07/7.17 & A != B % 7.07/7.17 & empty(B) ) ). % 7.07/7.17 % 7.07/7.17 %------------------------------------------------------------------------------ % 7.07/7.17 %------------------------------------------- % 7.07/7.17 % Proof found % 7.07/7.17 % SZS status Theorem for theBenchmark % 7.07/7.17 % SZS output start Proof % 7.07/7.17 %ClaNum:31(EqnAxiom:12) % 7.07/7.17 %VarNum:43(SingletonVarNum:22) % 7.07/7.17 %MaxLitNum:3 % 7.07/7.17 %MaxfuncDepth:1 % 7.07/7.17 %SharedTerms:12 % 7.07/7.17 %goalClause: 15 16 22 % 7.07/7.17 %singleGoalClaCount:3 % 7.07/7.17 [13]P1(a1) % 7.07/7.17 [14]P1(a2) % 7.07/7.17 [15]P2(a3,a6) % 7.07/7.17 [16]P3(a4,a3) % 7.07/7.17 [21]~P1(a5) % 7.07/7.17 [22]~P2(a4,a6) % 7.07/7.17 [18]P3(x181,x181) % 7.07/7.17 [17]E(f7(x171,a1),a1) % 7.07/7.17 [19]E(f7(x191,x191),x191) % 7.07/7.17 [20]E(f7(x201,x202),f7(x202,x201)) % 7.07/7.17 [23]~P1(x231)+E(x231,a1) % 7.07/7.17 [25]~P3(x251,a1)+E(x251,a1) % 7.07/7.17 [26]~P1(x261)+~P4(x262,x261) % 7.07/7.17 [29]~P2(x292,x291)+P2(x291,x292) % 7.07/7.17 [30]~P4(x302,x301)+~P4(x301,x302) % 7.07/7.17 [27]~P2(x271,x272)+E(f7(x271,x272),a1) % 7.07/7.17 [28]P2(x281,x282)+~E(f7(x281,x282),a1) % 7.07/7.17 [31]~P3(x311,x313)+P3(f7(x311,x312),f7(x313,x312)) % 7.07/7.17 [24]~P1(x242)+~P1(x241)+E(x241,x242) % 7.07/7.17 %EqnAxiom % 7.07/7.17 [1]E(x11,x11) % 7.07/7.17 [2]E(x22,x21)+~E(x21,x22) % 7.07/7.17 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 7.07/7.17 [4]~E(x41,x42)+E(f7(x41,x43),f7(x42,x43)) % 7.07/7.17 [5]~E(x51,x52)+E(f7(x53,x51),f7(x53,x52)) % 7.07/7.17 [6]~P1(x61)+P1(x62)+~E(x61,x62) % 7.07/7.17 [7]P3(x72,x73)+~E(x71,x72)+~P3(x71,x73) % 7.07/7.17 [8]P3(x83,x82)+~E(x81,x82)+~P3(x83,x81) % 7.07/7.17 [9]P2(x92,x93)+~E(x91,x92)+~P2(x91,x93) % 7.07/7.17 [10]P2(x103,x102)+~E(x101,x102)+~P2(x103,x101) % 7.07/7.17 [11]P4(x112,x113)+~E(x111,x112)+~P4(x111,x113) % 7.07/7.17 [12]P4(x123,x122)+~E(x121,x122)+~P4(x123,x121) % 7.07/7.17 % 7.07/7.17 %------------------------------------------- % 7.07/7.17 cnf(32,plain, % 7.07/7.17 (~P2(a6,a4)), % 7.07/7.17 inference(scs_inference,[],[22,29])). % 7.07/7.17 cnf(34,plain, % 7.07/7.17 (P2(a1,a1)), % 7.07/7.17 inference(scs_inference,[],[22,19,29,28])). % 7.07/7.17 cnf(35,plain, % 7.07/7.17 (E(f7(x351,x351),x351)), % 7.07/7.17 inference(rename_variables,[],[19])). % 7.07/7.17 cnf(37,plain, % 7.07/7.17 (E(x371,f7(x371,x371))), % 7.07/7.17 inference(scs_inference,[],[22,19,35,29,28,2])). % 7.07/7.17 cnf(40,plain, % 7.07/7.17 (P3(f7(a4,a4),a3)), % 7.07/7.17 inference(scs_inference,[],[16,22,19,35,13,29,28,2,26,7])). % 7.07/7.17 cnf(43,plain, % 7.07/7.17 (E(f7(x431,x431),x431)), % 7.07/7.17 inference(rename_variables,[],[19])). % 7.07/7.17 cnf(46,plain, % 7.07/7.17 (E(f7(x461,x461),x461)), % 7.07/7.17 inference(rename_variables,[],[19])). % 7.07/7.17 cnf(47,plain, % 7.07/7.17 (~P1(f7(a5,a5))), % 7.07/7.17 inference(scs_inference,[],[15,16,22,18,19,35,43,46,13,21,29,28,2,26,7,8,9,3,6])). % 7.07/7.17 cnf(49,plain, % 7.07/7.17 (P2(a3,x491)+~E(a6,x491)), % 7.07/7.17 inference(scs_inference,[],[15,16,22,18,19,35,43,46,13,21,29,28,2,26,7,8,9,3,6,10])). % 7.07/7.17 cnf(54,plain, % 7.07/7.17 (E(x541,f7(x541,x541))), % 7.07/7.17 inference(rename_variables,[],[37])). % 7.07/7.17 cnf(55,plain, % 7.07/7.17 (P2(x551,a1)), % 7.07/7.17 inference(scs_inference,[],[37,17,49,28])). % 7.07/7.18 cnf(59,plain, % 7.07/7.18 (E(a1,f7(x591,a1))), % 7.07/7.18 inference(scs_inference,[],[37,14,17,49,28,26,2])). % 7.07/7.18 cnf(60,plain, % 7.07/7.18 (P1(f7(a2,a2))), % 7.07/7.18 inference(scs_inference,[],[37,54,14,17,49,28,26,2,6])). % 7.07/7.18 cnf(61,plain, % 7.07/7.18 (E(x611,f7(x611,x611))), % 7.07/7.18 inference(rename_variables,[],[37])). % 7.07/7.18 cnf(62,plain, % 7.07/7.18 (P3(a4,f7(a3,a3))), % 7.07/7.18 inference(scs_inference,[],[16,37,54,61,14,17,49,28,26,2,6,8])). % 7.07/7.18 cnf(63,plain, % 7.07/7.18 (E(x631,f7(x631,x631))), % 7.07/7.18 inference(rename_variables,[],[37])). % 7.07/7.18 cnf(64,plain, % 7.07/7.18 (P2(f7(a3,a3),f7(a6,a6))), % 7.07/7.18 inference(scs_inference,[],[16,37,54,61,63,14,17,49,28,26,2,6,8,9])). % 7.07/7.18 cnf(65,plain, % 7.07/7.18 (E(x651,f7(x651,x651))), % 7.07/7.18 inference(rename_variables,[],[37])). % 7.07/7.18 cnf(66,plain, % 7.07/7.18 (P2(a1,f7(a1,a1))), % 7.07/7.18 inference(scs_inference,[],[16,37,54,61,63,65,34,14,17,49,28,26,2,6,8,9,10])). % 7.07/7.18 cnf(76,plain, % 7.07/7.18 (P3(f7(a4,a4),f7(a3,a3))), % 7.07/7.18 inference(scs_inference,[],[40,59,37,60,19,26,3,8])). % 7.07/7.18 cnf(77,plain, % 7.07/7.18 (E(x771,f7(x771,x771))), % 7.07/7.18 inference(rename_variables,[],[37])). % 7.07/7.18 cnf(79,plain, % 7.07/7.18 (E(x791,f7(x791,x791))), % 7.07/7.18 inference(rename_variables,[],[37])). % 7.07/7.18 cnf(81,plain, % 7.07/7.18 (E(x811,f7(x811,x811))), % 7.07/7.18 inference(rename_variables,[],[37])). % 7.07/7.18 cnf(82,plain, % 7.07/7.18 (P1(f7(x821,a1))), % 7.07/7.18 inference(scs_inference,[],[64,40,59,37,77,79,60,19,13,26,3,8,9,10,6])). % 7.07/7.18 cnf(85,plain, % 7.07/7.18 (E(f7(x851,a1),f7(a1,a1))), % 7.07/7.18 inference(scs_inference,[],[64,40,59,37,77,79,81,60,19,13,26,3,8,9,10,6,7,2])). % 7.07/7.18 cnf(89,plain, % 7.07/7.18 (E(x891,f7(x891,x891))), % 7.07/7.18 inference(rename_variables,[],[37])). % 7.07/7.18 cnf(90,plain, % 7.07/7.18 (P1(f7(f7(x901,a1),f7(x901,a1)))), % 7.07/7.18 inference(scs_inference,[],[76,37,89,82,26,8,6])). % 7.07/7.18 cnf(100,plain, % 7.07/7.18 (P3(a4,f7(f7(a3,a3),f7(a3,a3)))), % 7.07/7.18 inference(scs_inference,[],[62,37,90,26,8])). % 7.07/7.18 cnf(102,plain, % 7.07/7.18 (~E(a1,a4)), % 7.07/7.18 inference(scs_inference,[],[32,62,55,37,90,26,8,10])). % 7.07/7.18 cnf(104,plain, % 7.07/7.18 (P3(f7(a1,a1),f7(x1041,a1))), % 7.07/7.18 inference(scs_inference,[],[32,85,62,55,37,90,18,26,8,10,7])). % 7.07/7.18 cnf(106,plain, % 7.07/7.18 (P2(f7(x1061,a1),f7(a1,a1))), % 7.07/7.18 inference(scs_inference,[],[32,85,62,55,66,59,37,90,18,26,8,10,7,9])). % 7.07/7.18 cnf(111,plain, % 7.07/7.18 (P3(f7(x1111,a1),f7(a1,a1))), % 7.07/7.18 inference(scs_inference,[],[85,18,8])). % 7.07/7.18 cnf(113,plain, % 7.07/7.18 (E(a1,f7(f7(x1131,a1),f7(x1131,a1)))), % 7.07/7.18 inference(scs_inference,[],[90,23,2])). % 7.07/7.18 cnf(114,plain, % 7.07/7.18 (E(f7(f7(x1141,a1),f7(x1141,a1)),a1)), % 7.07/7.18 inference(scs_inference,[],[113,2])). % 7.07/7.18 cnf(115,plain, % 7.07/7.18 (E(f7(a1,a1),f7(f7(x1151,a1),f7(x1151,a1)))), % 7.07/7.18 inference(scs_inference,[],[113,19,2,3])). % 7.07/7.18 cnf(117,plain, % 7.07/7.18 (P1(f7(f7(a2,a2),f7(a2,a2)))), % 7.07/7.18 inference(scs_inference,[],[113,37,60,19,2,3,6])). % 7.07/7.18 cnf(119,plain, % 7.07/7.18 (P3(f7(f7(x1191,a1),f7(x1191,a1)),a1)), % 7.07/7.18 inference(scs_inference,[],[113,37,60,19,18,2,3,6,7])). % 7.07/7.18 cnf(120,plain, % 7.07/7.18 (P3(x1201,x1201)), % 7.07/7.18 inference(rename_variables,[],[18])). % 7.07/7.18 cnf(122,plain, % 7.07/7.18 (P3(a1,f7(f7(x1221,a1),f7(x1221,a1)))), % 7.07/7.18 inference(scs_inference,[],[113,66,37,60,19,18,120,2,3,6,7,9,8])). % 7.07/7.18 cnf(124,plain, % 7.07/7.18 (P2(f7(x1241,a1),f7(x1241,a1))), % 7.07/7.18 inference(scs_inference,[],[113,66,37,60,19,18,120,2,3,6,7,9,8,28])). % 7.07/7.18 cnf(130,plain, % 7.07/7.18 (E(f7(f7(x1301,a1),f7(x1301,a1)),f7(x1302,a1))), % 7.07/7.18 inference(scs_inference,[],[114,59,115,2,3])). % 7.07/7.18 cnf(131,plain, % 7.07/7.18 (P3(f7(x1311,a1),f7(f7(x1312,a1),f7(x1312,a1)))), % 7.07/7.18 inference(scs_inference,[],[114,122,59,115,2,3,7])). % 7.07/7.18 cnf(132,plain, % 7.07/7.18 (P3(f7(f7(x1321,a1),f7(x1321,a1)),f7(x1322,a1))), % 7.07/7.18 inference(scs_inference,[],[114,122,119,59,115,2,3,7,8])). % 7.07/7.18 cnf(133,plain, % 7.07/7.18 (P2(f7(a1,a1),f7(x1331,a1))), % 7.07/7.18 inference(scs_inference,[],[124,114,122,119,85,59,115,2,3,7,8,9])). % 7.07/7.18 cnf(135,plain, % 7.07/7.18 (E(f7(x1351,a1),f7(f7(x1352,a1),f7(x1352,a1)))), % 7.07/7.18 inference(scs_inference,[],[130,2])). % 7.07/7.18 cnf(136,plain, % 7.07/7.18 (P3(a1,f7(x1361,a1))), % 7.07/7.18 inference(scs_inference,[],[132,114,130,2,7])). % 7.07/7.18 cnf(138,plain, % 7.07/7.18 (P3(f7(x1381,a1),a1)), % 7.07/7.18 inference(scs_inference,[],[132,131,114,130,2,7,8])). % 7.07/7.18 cnf(146,plain, % 7.07/7.18 (P2(f7(a1,a1),f7(x1461,a1))), % 7.07/7.18 inference(rename_variables,[],[133])). % 7.07/7.18 cnf(147,plain, % 7.07/7.18 (P2(f7(f7(x1471,a1),f7(x1471,a1)),f7(x1472,a1))), % 7.07/7.18 inference(scs_inference,[],[133,146,135,47,130,19,3,6,10,9])). % 7.07/7.18 cnf(149,plain, % 7.07/7.18 (E(f7(a6,a3),a1)), % 7.07/7.18 inference(scs_inference,[],[15,27,29])). % 7.07/7.18 cnf(150,plain, % 7.07/7.18 (P2(a6,a3)), % 7.07/7.18 inference(scs_inference,[],[149,28])). % 7.07/7.18 cnf(152,plain, % 7.07/7.18 (E(a1,f7(a6,a3))), % 7.07/7.18 inference(scs_inference,[],[149,28,2])). % 7.07/7.18 cnf(153,plain, % 7.07/7.18 (E(f7(a3,a6),a1)), % 7.07/7.18 inference(scs_inference,[],[149,20,28,2,3])). % 7.07/7.18 cnf(155,plain, % 7.07/7.18 (P1(f7(a6,a3))), % 7.07/7.18 inference(scs_inference,[],[149,20,13,28,2,3,6])). % 7.07/7.18 cnf(158,plain, % 7.07/7.18 (P3(a1,f7(a6,a3))), % 7.07/7.18 inference(scs_inference,[],[106,149,135,20,13,18,28,2,3,6,10,7])). % 7.07/7.18 cnf(159,plain, % 7.07/7.18 (P3(x1591,x1591)), % 7.07/7.18 inference(rename_variables,[],[18])). % 7.07/7.18 cnf(160,plain, % 7.07/7.18 (P3(f7(a6,a3),a1)), % 7.07/7.18 inference(scs_inference,[],[106,149,135,20,13,18,159,28,2,3,6,10,7,8])). % 7.07/7.18 cnf(162,plain, % 7.07/7.18 (P2(a1,f7(x1621,a1))), % 7.07/7.18 inference(scs_inference,[],[106,147,149,135,114,20,13,18,159,28,2,3,6,10,7,8,9])). % 7.07/7.18 cnf(166,plain, % 7.07/7.18 (E(a1,f7(a3,a6))), % 7.07/7.18 inference(scs_inference,[],[153,2])). % 7.07/7.18 cnf(168,plain, % 7.07/7.18 (P1(f7(a3,a6))), % 7.07/7.18 inference(scs_inference,[],[152,114,153,13,2,3,6])). % 7.07/7.18 cnf(169,plain, % 7.07/7.18 (P2(a1,f7(f7(x1691,a1),f7(x1691,a1)))), % 7.07/7.18 inference(scs_inference,[],[162,152,135,114,153,13,2,3,6,10])). % 7.07/7.18 cnf(170,plain, % 7.07/7.18 (P2(a1,f7(x1701,a1))), % 7.07/7.18 inference(rename_variables,[],[162])). % 7.07/7.18 cnf(171,plain, % 7.07/7.18 (P3(f7(a6,a3),f7(x1711,a1))), % 7.07/7.18 inference(scs_inference,[],[136,162,152,135,114,153,13,2,3,6,10,7])). % 7.07/7.18 cnf(172,plain, % 7.07/7.18 (P3(f7(x1721,a1),f7(a6,a3))), % 7.07/7.18 inference(scs_inference,[],[136,138,162,152,135,114,153,13,2,3,6,10,7,8])). % 7.07/7.18 cnf(173,plain, % 7.07/7.18 (P2(f7(a6,a3),f7(x1731,a1))), % 7.07/7.18 inference(scs_inference,[],[136,138,162,170,152,135,114,153,13,2,3,6,10,7,8,9])). % 7.07/7.18 cnf(176,plain, % 7.07/7.18 (E(f7(x1761,f7(a3,a6)),f7(x1761,a1))), % 7.07/7.18 inference(scs_inference,[],[166,5,2])). % 7.07/7.18 cnf(177,plain, % 7.07/7.18 (E(f7(x1771,a1),f7(x1771,f7(a3,a6)))), % 7.07/7.18 inference(scs_inference,[],[176,2])). % 7.07/7.18 cnf(186,plain, % 7.07/7.18 (P2(f7(a6,a6),a3)), % 7.07/7.18 inference(scs_inference,[],[150,171,172,173,135,149,113,37,176,82,2,3,6,10,7,8,9])). % 7.07/7.18 cnf(190,plain, % 7.07/7.18 (P3(f7(f7(a4,a4),x1901),f7(a3,x1901))), % 7.07/7.18 inference(scs_inference,[],[16,37,31,7])). % 7.07/7.18 cnf(192,plain, % 7.07/7.18 (E(f7(x1921,a1),f7(x1921,f7(a3,a6)))), % 7.07/7.18 inference(rename_variables,[],[177])). % 7.07/7.18 cnf(193,plain, % 7.07/7.18 (P2(f7(a6,a6),f7(a3,a3))), % 7.07/7.18 inference(scs_inference,[],[177,186,59,37,3,10])). % 7.07/7.18 cnf(194,plain, % 7.07/7.18 (E(x1941,f7(x1941,x1941))), % 7.07/7.18 inference(rename_variables,[],[37])). % 7.07/7.18 cnf(195,plain, % 7.07/7.18 (P3(f7(x1951,a1),f7(a1,f7(a3,a6)))), % 7.07/7.18 inference(scs_inference,[],[111,177,192,186,59,37,3,10,8])). % 7.07/7.18 cnf(196,plain, % 7.07/7.18 (E(f7(x1961,a1),f7(x1961,f7(a3,a6)))), % 7.07/7.18 inference(rename_variables,[],[177])). % 7.07/7.18 cnf(202,plain, % 7.07/7.18 (E(f7(x2021,f7(a3,a6)),a1)), % 7.07/7.18 inference(scs_inference,[],[190,111,177,192,196,186,59,37,194,3,10,8,7,9,2])). % 7.07/7.18 cnf(203,plain, % 7.07/7.18 (P2(x2031,f7(a3,a6))), % 7.07/7.18 inference(scs_inference,[],[190,111,177,192,196,186,59,37,194,3,10,8,7,9,2,28])). % 7.07/7.18 cnf(205,plain, % 7.07/7.18 (E(f7(x2051,f7(a3,a6)),f7(a3,a6))), % 7.07/7.18 inference(scs_inference,[],[202,166,3])). % 7.07/7.18 cnf(207,plain, % 7.07/7.18 (E(x2071,f7(x2071,x2071))), % 7.07/7.18 inference(rename_variables,[],[37])). % 7.07/7.18 cnf(209,plain, % 7.07/7.18 (P3(f7(a1,a1),f7(x2091,a1))), % 7.07/7.18 inference(rename_variables,[],[104])). % 7.07/7.18 cnf(210,plain, % 7.07/7.18 (P3(f7(a1,f7(a3,a6)),f7(x2101,a1))), % 7.07/7.18 inference(scs_inference,[],[193,104,209,202,166,177,37,3,10,8,7])). % 7.07/7.18 cnf(214,plain, % 7.07/7.18 (E(f7(a3,a6),f7(x2141,f7(a3,a6)))), % 7.07/7.18 inference(scs_inference,[],[193,104,209,202,166,177,37,207,3,10,8,7,9,2])). % 7.07/7.18 cnf(219,plain, % 7.07/7.18 (P3(f7(a6,a3),f7(a3,a6))), % 7.07/7.18 inference(scs_inference,[],[32,203,160,202,166,152,3,10,8])). % 7.07/7.18 cnf(220,plain, % 7.07/7.18 (P3(f7(a3,a6),f7(a6,a3))), % 7.07/7.18 inference(scs_inference,[],[32,203,158,160,202,166,152,3,10,8,7])). % 7.07/7.18 cnf(222,plain, % 7.07/7.18 (E(f7(a6,a3),f7(x2221,f7(a3,a6)))), % 7.07/7.18 inference(scs_inference,[],[32,203,169,158,160,202,166,152,3,10,8,7,9,2])). % 7.07/7.18 cnf(226,plain, % 7.07/7.18 (P2(f7(a1,a1),f7(x2261,a1))), % 7.07/7.18 inference(rename_variables,[],[133])). % 7.07/7.18 cnf(228,plain, % 7.07/7.18 (P3(f7(x2281,f7(a3,a6)),f7(a3,a6))), % 7.07/7.18 inference(scs_inference,[],[214,222,219,133,202,177,59,3,10,8,7])). % 7.07/7.18 cnf(231,plain, % 7.07/7.18 (E(f7(x2311,a1),f7(x2312,f7(a3,a6)))), % 7.07/7.18 inference(scs_inference,[],[214,222,219,133,226,202,177,59,3,10,8,7,9,2])). % 7.07/7.18 cnf(232,plain, % 7.07/7.18 (E(a1,f7(f7(a2,a2),f7(a2,a2)))), % 7.07/7.18 inference(scs_inference,[],[117,23,2])). % 7.07/7.18 cnf(233,plain, % 7.07/7.18 (E(f7(f7(a2,a2),f7(a2,a2)),a1)), % 7.07/7.18 inference(scs_inference,[],[232,2])). % 7.07/7.18 cnf(234,plain, % 7.07/7.18 (E(f7(x2341,a1),f7(a3,a6))), % 7.07/7.18 inference(scs_inference,[],[231,232,205,2,3])). % 7.07/7.18 cnf(237,plain, % 7.07/7.18 (E(f7(x2371,a1),f7(x2372,f7(a3,a6)))), % 7.07/7.18 inference(rename_variables,[],[231])). % 7.07/7.18 cnf(238,plain, % 7.07/7.18 (P3(f7(a3,a6),f7(x2381,f7(a3,a6)))), % 7.07/7.18 inference(scs_inference,[],[231,220,232,106,222,205,2,3,10,8])). % 7.07/7.18 cnf(239,plain, % 7.07/7.18 (P3(a1,f7(a3,a6))), % 7.07/7.18 inference(scs_inference,[],[228,231,220,232,106,222,202,205,2,3,10,8,7])). % 7.07/7.18 cnf(243,plain, % 7.07/7.18 (P2(f7(a2,a2),f7(a2,a2))), % 7.07/7.18 inference(scs_inference,[],[228,231,237,220,232,106,222,202,205,2,3,10,8,7,9,28])). % 7.07/7.18 cnf(245,plain, % 7.07/7.18 (E(f7(f7(a6,a3),x2451),f7(a1,x2451))), % 7.07/7.18 inference(scs_inference,[],[155,23,4])). % 7.07/7.18 cnf(246,plain, % 7.07/7.18 (E(f7(a1,x2461),f7(f7(a6,a3),x2461))), % 7.07/7.18 inference(scs_inference,[],[245,2])). % 7.07/7.18 cnf(247,plain, % 7.07/7.18 (E(f7(f7(a2,a2),f7(a2,a2)),f7(a6,a3))), % 7.07/7.18 inference(scs_inference,[],[233,152,245,2,3])). % 7.07/7.18 cnf(249,plain, % 7.07/7.18 (E(x2491,f7(x2491,x2491))), % 7.07/7.18 inference(rename_variables,[],[37])). % 7.07/7.18 cnf(250,plain, % 7.07/7.18 (P3(f7(a3,a6),a1)), % 7.07/7.18 inference(scs_inference,[],[238,243,233,202,152,37,245,2,3,10,8])). % 7.07/7.18 cnf(252,plain, % 7.07/7.18 (P3(f7(f7(a2,a2),f7(a2,a2)),f7(a3,a6))), % 7.07/7.18 inference(scs_inference,[],[238,243,233,239,232,202,152,37,245,2,3,10,8,7])). % 7.07/7.18 cnf(253,plain, % 7.07/7.18 (P2(f7(f7(a2,a2),f7(a2,a2)),f7(a2,a2))), % 7.07/7.18 inference(scs_inference,[],[238,243,233,239,232,202,152,37,249,245,2,3,10,8,7,9])). % 7.07/7.18 cnf(255,plain, % 7.07/7.18 (E(f7(f7(a3,a6),x2551),f7(a1,x2551))), % 7.07/7.18 inference(scs_inference,[],[168,23,4])). % 7.07/7.18 cnf(256,plain, % 7.07/7.18 (E(f7(a1,x2561),f7(f7(a3,a6),x2561))), % 7.07/7.18 inference(scs_inference,[],[255,2])). % 7.07/7.18 cnf(257,plain, % 7.07/7.18 (E(f7(f7(a2,a2),f7(a2,a2)),f7(a3,a6))), % 7.07/7.18 inference(scs_inference,[],[233,166,255,2,3])). % 7.07/7.18 cnf(262,plain, % 7.07/7.18 (P2(a1,f7(a2,a2))), % 7.07/7.18 inference(scs_inference,[],[22,253,246,195,203,233,166,255,2,3,10,8,9])). % 7.07/7.18 cnf(268,plain, % 7.07/7.18 (E(f7(a3,a6),f7(f7(a2,a2),f7(a2,a2)))), % 7.07/7.18 inference(scs_inference,[],[257,2])). % 7.07/7.18 cnf(269,plain, % 7.07/7.18 (E(f7(f7(a2,a2),f7(a2,a2)),f7(x2691,a1))), % 7.07/7.18 inference(scs_inference,[],[233,59,257,2,3])). % 7.07/7.18 cnf(272,plain, % 7.07/7.18 (P3(f7(a3,a6),f7(f7(a2,a2),f7(a2,a2)))), % 7.07/7.18 inference(scs_inference,[],[250,262,232,233,59,37,257,2,3,10,8])). % 7.07/7.18 cnf(277,plain, % 7.07/7.18 (E(f7(x2771,a1),f7(f7(a2,a2),f7(a2,a2)))), % 7.07/7.18 inference(scs_inference,[],[269,2])). % 7.07/7.18 cnf(279,plain, % 7.07/7.18 (P2(f7(x2791,a1),f7(f7(a3,a6),a1))), % 7.07/7.18 inference(scs_inference,[],[268,256,106,269,2,3,10])). % 7.07/7.18 cnf(281,plain, % 7.07/7.18 (P3(f7(a6,a3),f7(f7(a2,a2),f7(a2,a2)))), % 7.07/7.18 inference(scs_inference,[],[268,160,256,232,106,269,2,3,10,8])). % 7.07/7.18 cnf(283,plain, % 7.07/7.18 (P3(f7(f7(a2,a2),f7(a2,a2)),f7(a6,a3))), % 7.07/7.18 inference(scs_inference,[],[268,160,158,256,173,222,232,106,269,2,3,10,8,9,7])). % 7.07/7.18 cnf(284,plain, % 7.07/7.18 (E(f7(x2841,f7(a6,a3)),f7(x2841,a1))), % 7.07/7.18 inference(scs_inference,[],[155,23,5])). % 7.07/7.18 cnf(285,plain, % 7.07/7.18 (E(f7(a6,a3),f7(f7(a2,a2),f7(a2,a2)))), % 7.07/7.18 inference(scs_inference,[],[247,2])). % 7.07/7.18 cnf(289,plain, % 7.07/7.18 (P3(a1,f7(f7(a2,a2),f7(a2,a2)))), % 7.07/7.18 inference(scs_inference,[],[277,279,239,268,247,2,3,10,8])). % 7.07/7.18 cnf(296,plain, % 7.07/7.18 (E(f7(x2961,a1),f7(x2961,f7(a6,a3)))), % 7.07/7.18 inference(scs_inference,[],[284,2])). % 7.07/7.18 cnf(300,plain, % 7.07/7.18 (E(f7(a1,x3001),f7(f7(a6,a3),x3001))), % 7.07/7.18 inference(rename_variables,[],[246])). % 7.07/7.18 cnf(302,plain, % 7.07/7.18 (E(f7(a1,x3021),f7(f7(a6,a3),x3021))), % 7.07/7.18 inference(rename_variables,[],[246])). % 7.07/7.18 cnf(303,plain, % 7.07/7.18 (P3(f7(x3031,a1),f7(f7(a6,a3),a1))), % 7.07/7.18 inference(scs_inference,[],[285,111,246,300,302,133,106,284,269,82,2,6,3,10,9,8])). % 7.07/7.18 cnf(304,plain, % 7.07/7.18 (E(f7(a1,x3041),f7(f7(a6,a3),x3041))), % 7.07/7.18 inference(rename_variables,[],[246])). % 7.07/7.18 cnf(305,plain, % 7.07/7.18 (P3(f7(f7(a6,a3),a1),f7(x3051,a1))), % 7.07/7.18 inference(scs_inference,[],[285,111,104,246,300,302,304,133,106,284,269,82,2,6,3,10,9,8,7])). % 7.07/7.18 cnf(309,plain, % 7.07/7.18 (E(f7(x3091,f7(a6,a3)),a1)), % 7.07/7.18 inference(scs_inference,[],[296,82,23,6])). % 7.07/7.18 cnf(310,plain, % 7.07/7.18 (P2(x3101,f7(a6,a3))), % 7.07/7.18 inference(scs_inference,[],[309,28])). % 7.07/7.18 cnf(312,plain, % 7.07/7.18 (E(a1,f7(x3121,f7(a6,a3)))), % 7.07/7.18 inference(scs_inference,[],[309,28,2])). % 7.07/7.18 cnf(313,plain, % 7.07/7.18 (E(f7(a1,a1),f7(f7(a3,a6),f7(a6,a3)))), % 7.07/7.18 inference(scs_inference,[],[296,256,309,28,2,3])). % 7.07/7.18 cnf(325,plain, % 7.07/7.18 (E(f7(f7(a3,a6),f7(a6,a3)),f7(a1,a1))), % 7.07/7.18 inference(scs_inference,[],[313,2])). % 7.07/7.18 cnf(326,plain, % 7.07/7.18 (E(f7(a1,a1),f7(f7(a6,a3),f7(a6,a3)))), % 7.07/7.18 inference(scs_inference,[],[246,296,313,2,3])). % 7.07/7.18 cnf(331,plain, % 7.07/7.18 (P3(f7(f7(a2,a2),f7(a2,a2)),f7(x3311,a1))), % 7.07/7.18 inference(scs_inference,[],[32,310,305,277,246,296,313,2,3,10,7])). % 7.07/7.18 cnf(332,plain, % 7.07/7.18 (E(f7(x3321,a1),f7(f7(a2,a2),f7(a2,a2)))), % 7.07/7.18 inference(rename_variables,[],[277])). % 7.07/7.18 cnf(333,plain, % 7.07/7.18 (P2(f7(x3331,f7(a6,a3)),f7(a2,a2))), % 7.07/7.18 inference(scs_inference,[],[32,310,312,262,305,277,246,296,313,2,3,10,7,9])). % 7.07/7.18 cnf(334,plain, % 7.07/7.18 (P3(f7(x3341,a1),f7(f7(a2,a2),f7(a2,a2)))), % 7.07/7.18 inference(scs_inference,[],[32,310,312,262,305,303,277,332,246,296,313,2,3,10,7,9,8])). % 7.07/7.18 cnf(337,plain, % 7.07/7.18 (E(f7(f7(a6,a3),f7(a6,a3)),f7(a1,a1))), % 7.07/7.18 inference(scs_inference,[],[326,2])). % 7.07/7.18 cnf(338,plain, % 7.07/7.18 (E(f7(f7(a3,a6),f7(a6,a3)),f7(a3,a6))), % 7.07/7.18 inference(scs_inference,[],[325,326,234,2,3])). % 7.07/7.18 cnf(343,plain, % 7.07/7.18 (E(f7(a1,x3431),f7(f7(a3,a6),x3431))), % 7.07/7.18 inference(rename_variables,[],[256])). % 7.07/7.18 cnf(346,plain, % 7.07/7.18 (P2(f7(a1,a1),f7(a2,a2))), % 7.07/7.18 inference(scs_inference,[],[22,325,333,210,310,195,256,343,326,234,2,3,10,8,7,9])). % 7.07/7.18 cnf(355,plain, % 7.07/7.18 (E(f7(x3551,a1),f7(x3552,f7(a3,a6)))), % 7.07/7.18 inference(rename_variables,[],[231])). % 7.07/7.18 cnf(356,plain, % 7.07/7.18 (P3(a1,f7(x3561,f7(a3,a6)))), % 7.07/7.18 inference(scs_inference,[],[337,346,136,162,231,355,338,234,2,3,10,9,8])). % 7.07/7.18 cnf(376,plain, % 7.07/7.18 (P2(a2,a2)), % 7.07/7.18 inference(scs_inference,[],[60,23,28])). % 7.07/7.18 cnf(377,plain, % 7.07/7.18 (P2(a2,f7(a2,a2))), % 7.07/7.18 inference(scs_inference,[],[376,37,10])). % 7.07/7.18 cnf(378,plain, % 7.07/7.18 (E(x3781,f7(x3781,x3781))), % 7.07/7.18 inference(rename_variables,[],[37])). % 7.07/7.18 cnf(379,plain, % 7.07/7.18 (P2(f7(a2,a2),a2)), % 7.07/7.18 inference(scs_inference,[],[376,37,378,10,9])). % 7.07/7.18 cnf(384,plain, % 7.07/7.18 (E(x3841,f7(x3841,x3841))), % 7.07/7.18 inference(rename_variables,[],[37])). % 7.07/7.18 cnf(385,plain, % 7.07/7.18 (P2(f7(f7(a2,a2),f7(a2,a2)),a2)), % 7.07/7.18 inference(scs_inference,[],[379,377,37,384,10,9])). % 7.07/7.18 cnf(391,plain, % 7.07/7.18 (P2(a1,a2)), % 7.07/7.18 inference(scs_inference,[],[385,233,9])). % 7.07/7.18 cnf(403,plain, % 7.07/7.18 (~P3(a4,a1)), % 7.07/7.18 inference(scs_inference,[],[102,2,25])). % 7.07/7.18 cnf(411,plain, % 7.07/7.18 (~E(f7(f7(a3,a3),f7(a3,a3)),a1)), % 7.07/7.18 inference(scs_inference,[],[100,403,8])). % 7.07/7.18 cnf(427,plain, % 7.07/7.18 (~E(f7(a3,a3),a1)), % 7.07/7.18 inference(scs_inference,[],[285,152,391,62,19,403,3,9,8])). % 7.07/7.18 cnf(488,plain, % 7.07/7.18 (E(f7(a2,a2),f7(a3,a6))), % 7.07/7.18 inference(scs_inference,[],[268,222,171,19,3,7,2])). % 7.07/7.18 cnf(493,plain, % 7.07/7.18 (~E(f7(a4,a6),a1)), % 7.07/7.18 inference(scs_inference,[],[32,29,28])). % 7.07/7.18 cnf(496,plain, % 7.07/7.18 (~P3(f7(a4,a6),a1)), % 7.07/7.18 inference(scs_inference,[],[493,23,25])). % 7.07/7.18 cnf(505,plain, % 7.07/7.18 (E(f7(a3,f7(a6,a6)),a1)), % 7.07/7.18 inference(scs_inference,[],[37,49,27])). % 7.07/7.18 cnf(508,plain, % 7.07/7.18 (E(f7(f7(a6,a6),a3),a1)), % 7.07/7.18 inference(scs_inference,[],[505,20,13,2,6,3])). % 7.07/7.18 cnf(514,plain, % 7.07/7.18 (E(a1,f7(f7(a6,a6),a3))), % 7.07/7.18 inference(scs_inference,[],[508,2])). % 7.07/7.18 cnf(515,plain, % 7.07/7.18 (P1(f7(f7(a6,a6),a3))), % 7.07/7.18 inference(scs_inference,[],[508,13,2,6])). % 7.07/7.18 cnf(548,plain, % 7.07/7.18 (~E(f7(a4,a6),f7(f7(a2,a2),f7(a2,a2)))), % 7.07/7.18 inference(scs_inference,[],[22,233,28,3])). % 7.07/7.18 cnf(554,plain, % 7.07/7.18 (P3(f7(x5541,f7(a6,a3)),f7(a1,a1))), % 7.07/7.18 inference(scs_inference,[],[285,296,111,124,136,548,10,3,8,7])). % 7.07/7.18 cnf(556,plain, % 7.07/7.18 (P2(f7(a3,a6),x5561)), % 7.07/7.18 inference(scs_inference,[],[202,28,29])). % 7.07/7.18 cnf(557,plain, % 7.07/7.18 (~E(f7(a4,a6),f7(a3,a6))), % 7.07/7.18 inference(scs_inference,[],[268,548,3])). % 7.07/7.18 cnf(560,plain, % 7.07/7.18 (~E(f7(a6,a4),f7(f7(a2,a2),f7(a2,a2)))), % 7.07/7.18 inference(scs_inference,[],[32,233,28,3])). % 7.07/7.18 cnf(561,plain, % 7.07/7.18 (~E(f7(a6,a4),f7(a6,a3))), % 7.07/7.18 inference(scs_inference,[],[285,560,3])). % 7.07/7.18 cnf(563,plain, % 7.07/7.18 (~E(f7(a4,a6),f7(x5631,f7(a3,a6)))), % 7.07/7.18 inference(scs_inference,[],[22,202,28,3])). % 7.07/7.18 cnf(564,plain, % 7.07/7.18 (~E(a6,f7(a3,a6))), % 7.07/7.18 inference(scs_inference,[],[563,5])). % 7.07/7.18 cnf(588,plain, % 7.07/7.18 (~P3(a6,a1)), % 7.07/7.18 inference(scs_inference,[],[166,564,3,25])). % 7.07/7.18 cnf(632,plain, % 7.07/7.18 (P2(f7(f7(a2,a2),f7(a2,a2)),x6321)), % 7.07/7.18 inference(scs_inference,[],[268,556,9])). % 7.07/7.18 cnf(636,plain, % 7.07/7.18 (P2(a1,x6361)), % 7.07/7.18 inference(scs_inference,[],[233,632,9])). % 7.07/7.18 cnf(653,plain, % 7.07/7.18 (P2(x6531,f7(f7(a2,a2),f7(a2,a2)))), % 7.07/7.18 inference(scs_inference,[],[268,203,10])). % 7.07/7.18 cnf(654,plain, % 7.07/7.18 (P3(f7(x6541,a1),f7(a3,a6))), % 7.07/7.18 inference(scs_inference,[],[166,268,203,138,10,8])). % 7.07/7.18 cnf(688,plain, % 7.07/7.18 (P3(f7(x6881,f7(a6,a3)),a1)), % 7.07/7.18 inference(scs_inference,[],[17,554,8])). % 7.07/7.18 cnf(701,plain, % 7.07/7.18 (P3(f7(x7011,f7(a6,a3)),f7(x7012,a1))), % 7.07/7.18 inference(scs_inference,[],[59,636,688,9,8])). % 7.07/7.18 cnf(709,plain, % 7.07/7.18 (P2(x7091,f7(a2,a2))), % 7.07/7.18 inference(scs_inference,[],[19,653,10])). % 7.07/7.18 cnf(710,plain, % 7.07/7.18 (E(f7(x7101,x7101),x7101)), % 7.07/7.18 inference(rename_variables,[],[19])). % 7.07/7.18 cnf(711,plain, % 7.07/7.18 (P2(f7(a2,a2),x7111)), % 7.07/7.18 inference(scs_inference,[],[19,710,653,632,10,9])). % 7.07/7.18 cnf(712,plain, % 7.07/7.18 (E(f7(x7121,x7121),x7121)), % 7.07/7.18 inference(rename_variables,[],[19])). % 7.07/7.18 cnf(713,plain, % 7.07/7.18 (P3(f7(a3,a6),f7(a2,a2))), % 7.07/7.18 inference(scs_inference,[],[19,710,712,272,653,632,10,9,8])). % 7.07/7.18 cnf(714,plain, % 7.07/7.18 (E(f7(x7141,x7141),x7141)), % 7.07/7.18 inference(rename_variables,[],[19])). % 7.07/7.18 cnf(715,plain, % 7.07/7.18 (P3(f7(a2,a2),f7(a6,a3))), % 7.07/7.18 inference(scs_inference,[],[19,710,712,714,283,272,653,632,10,9,8,7])). % 7.07/7.18 cnf(717,plain, % 7.07/7.18 (P3(a4,f7(a3,a4))), % 7.07/7.18 inference(scs_inference,[],[16,19,31,7])). % 7.07/7.18 cnf(719,plain, % 7.07/7.18 (E(f7(x7191,x7191),x7191)), % 7.07/7.18 inference(rename_variables,[],[19])). % 7.07/7.18 cnf(721,plain, % 7.07/7.18 (E(f7(x7211,x7211),x7211)), % 7.07/7.18 inference(rename_variables,[],[19])). % 7.07/7.18 cnf(723,plain, % 7.07/7.18 (E(f7(x7231,x7231),x7231)), % 7.07/7.18 inference(rename_variables,[],[19])). % 7.07/7.18 cnf(724,plain, % 7.07/7.18 (P3(f7(a2,a2),f7(a3,a6))), % 7.07/7.18 inference(scs_inference,[],[19,719,721,723,709,711,281,252,10,9,8,7])). % 7.07/7.18 cnf(726,plain, % 7.07/7.18 (P3(f7(a4,x7261),f7(f7(a3,a3),x7261))), % 7.07/7.18 inference(scs_inference,[],[16,37,31,8])). % 7.07/7.18 cnf(728,plain, % 7.07/7.18 (E(f7(x7281,x7281),x7281)), % 7.07/7.18 inference(rename_variables,[],[19])). % 7.07/7.18 cnf(729,plain, % 7.07/7.18 (P3(a2,f7(a3,a6))), % 7.07/7.18 inference(scs_inference,[],[19,728,289,724,8,7])). % 7.07/7.18 cnf(733,plain, % 7.07/7.18 (P3(f7(x7331,f7(a3,a6)),f7(a2,a2))), % 7.07/7.18 inference(scs_inference,[],[19,214,713,8,7])). % 7.07/7.18 cnf(736,plain, % 7.07/7.18 (E(f7(x7361,x7361),x7361)), % 7.07/7.18 inference(rename_variables,[],[19])). % 7.07/7.18 cnf(737,plain, % 7.07/7.18 (P3(a2,f7(a6,a3))), % 7.07/7.19 inference(scs_inference,[],[19,736,733,715,8,7])). % 7.07/7.19 cnf(752,plain, % 7.07/7.19 (P3(f7(x7521,a1),f7(a2,a2))), % 7.07/7.19 inference(scs_inference,[],[19,334,8])). % 7.07/7.19 cnf(756,plain, % 7.07/7.19 (~E(f7(a5,a5),f7(f7(a6,a6),a3))), % 7.07/7.19 inference(scs_inference,[],[515,47,6,2])). % 7.07/7.19 cnf(764,plain, % 7.07/7.19 (~P3(f7(a5,a5),a1)), % 7.07/7.19 inference(scs_inference,[],[19,37,752,717,514,756,8,7,3,27,25])). % 7.07/7.19 cnf(785,plain, % 7.07/7.19 (P3(f7(a2,a2),f7(x7851,a1))), % 7.07/7.19 inference(scs_inference,[],[19,268,729,331,8,7])). % 7.07/7.19 cnf(789,plain, % 7.07/7.19 (P1(f7(f7(a6,a6),f7(a3,a3)))), % 7.07/7.19 inference(scs_inference,[],[515,37,6,5])). % 7.07/7.19 cnf(792,plain, % 7.07/7.19 (P3(f7(a2,a2),a1)), % 7.07/7.19 inference(scs_inference,[],[19,785,789,26,8])). % 7.07/7.19 cnf(802,plain, % 7.07/7.19 (P3(a2,a1)), % 7.07/7.19 inference(scs_inference,[],[19,222,737,792,8,7])). % 7.07/7.19 cnf(837,plain, % 7.07/7.19 (P1(f7(a2,f7(a2,a2)))), % 7.07/7.19 inference(scs_inference,[],[117,19,6,4])). % 7.07/7.19 cnf(840,plain, % 7.07/7.19 (P3(f7(x8401,x8401),x8401)), % 7.07/7.19 inference(scs_inference,[],[19,837,18,26,8])). % 7.07/7.19 cnf(843,plain, % 7.07/7.19 (P3(f7(f7(x8431,x8431),f7(x8431,x8431)),x8431)), % 7.07/7.19 inference(scs_inference,[],[19,840,8])). % 7.07/7.19 cnf(896,plain, % 7.07/7.19 (E(f7(x8961,x8962),f7(x8962,x8961))), % 7.07/7.19 inference(rename_variables,[],[20])). % 7.07/7.19 cnf(898,plain, % 7.07/7.19 (P3(f7(a1,x8981),f7(a3,a6))), % 7.07/7.19 inference(scs_inference,[],[20,896,488,654,701,557,8,3,7])). % 7.07/7.19 cnf(901,plain, % 7.07/7.19 (P3(f7(a1,x9011),f7(a6,a3))), % 7.07/7.19 inference(scs_inference,[],[20,898,8])). % 7.07/7.19 cnf(1043,plain, % 7.07/7.19 (E(f7(x10431,x10432),f7(x10432,x10431))), % 7.07/7.19 inference(rename_variables,[],[20])). % 7.07/7.19 cnf(1044,plain, % 7.07/7.19 (P3(f7(x10441,a4),f7(f7(a3,a3),x10441))), % 7.07/7.19 inference(scs_inference,[],[20,1043,356,726,8,7])). % 7.07/7.19 cnf(1047,plain, % 7.07/7.19 (E(f7(a1,x10471),a1)), % 7.07/7.19 inference(scs_inference,[],[149,901,8,25])). % 7.07/7.19 cnf(1053,plain, % 7.07/7.19 (E(f7(x10531,x10532),f7(x10532,x10531))), % 7.07/7.19 inference(rename_variables,[],[20])). % 7.07/7.19 cnf(1054,plain, % 7.07/7.19 (P3(f7(f7(a6,a3),x10541),a1)), % 7.07/7.19 inference(scs_inference,[],[20,1053,411,1044,688,13,1047,2,6,3,8,7])). % 7.07/7.19 cnf(1069,plain, % 7.07/7.19 (P3(f7(f7(a4,a4),x10691),f7(x10691,a3))), % 7.07/7.19 inference(scs_inference,[],[20,427,190,508,3,8])). % 7.07/7.19 cnf(1073,plain, % 7.07/7.19 (E(f7(f7(a4,a4),a6),a1)), % 7.07/7.19 inference(scs_inference,[],[149,1069,8,25])). % 7.07/7.19 cnf(1076,plain, % 7.07/7.19 (E(a1,f7(f7(a4,a4),a6))), % 7.07/7.19 inference(scs_inference,[],[1073,28,2])). % 7.07/7.19 cnf(1094,plain, % 7.07/7.19 (E(f7(f7(a4,a4),a6),f7(a6,a3))), % 7.07/7.19 inference(scs_inference,[],[20,149,1054,1076,764,18,3,8,7,4,2])). % 7.07/7.19 cnf(1097,plain, % 7.07/7.19 (P3(f7(x10971,f7(a4,a4)),f7(x10971,a3))), % 7.07/7.19 inference(scs_inference,[],[20,1094,1069,561,3,7])). % 7.07/7.19 cnf(1102,plain, % 7.07/7.19 (E(f7(a6,f7(a4,a4)),a1)), % 7.07/7.19 inference(scs_inference,[],[149,1097,8,25])). % 7.07/7.19 cnf(1105,plain, % 7.07/7.19 (E(a1,f7(a6,f7(a4,a4)))), % 7.07/7.19 inference(scs_inference,[],[1102,28,2])). % 7.07/7.19 cnf(1117,plain, % 7.07/7.19 (E(f7(a6,f7(a4,a4)),f7(a6,a3))), % 7.07/7.19 inference(scs_inference,[],[149,1105,843,588,3,7,2])). % 7.07/7.19 cnf(1121,plain, % 7.07/7.19 ($false), % 7.07/7.19 inference(scs_inference,[],[37,1117,802,561,496,3,7,5]), % 7.07/7.19 ['proof']). % 7.07/7.19 % SZS output end Proof % 7.07/7.19 % Total time :6.660000s %------------------------------------------------------------------------------