%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SET971+1 : TPTP v8.2.0. Released v3.2.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n019.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 14:23:07 EDT 2024 % Result : Theorem 87.15s 87.19s % Output : CNFRefutation 87.15s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SET971+1 : TPTP v8.2.0. Released v3.2.0. % 0.03/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.13/0.34 % Computer : n019.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Sun Jun 23 13:51:09 EDT 2024 % 0.13/0.34 % CPUTime : % 0.52/0.59 start to proof:theBenchmark % 87.08/87.18 %------------------------------------------- % 87.08/87.18 % File :CSE---1.7 % 87.08/87.18 % Problem :theBenchmark % 87.08/87.18 % Transform :cnf % 87.08/87.18 % Format :tptp:raw % 87.08/87.18 % Command :java -jar mcs_scs.jar %d %s % 87.08/87.18 % 87.08/87.18 % Result :Theorem 86.510000s % 87.08/87.18 % Output :CNFRefutation 86.510000s % 87.08/87.18 %------------------------------------------- % 87.15/87.19 %------------------------------------------------------------------------------ % 87.15/87.19 % File : SET971+1 : TPTP v8.2.0. Released v3.2.0. % 87.15/87.19 % Domain : Set theory % 87.15/87.19 % Problem : Basic properties of sets, theorem 124 % 87.15/87.19 % Version : [Urb06] axioms : Especial. % 87.15/87.19 % English : % 87.15/87.19 % 87.15/87.19 % Refs : [Byl90] Bylinski (1990), Some Basic Properties of Sets % 87.15/87.19 % : [Urb06] Urban (2006), Email to G. Sutcliffe % 87.15/87.19 % Source : [Urb06] % 87.15/87.19 % Names : zfmisc_1__t124_zfmisc_1 [Urb06] % 87.15/87.19 % 87.15/87.19 % Status : Theorem % 87.15/87.19 % Rating : 0.14 v7.5.0, 0.16 v7.4.0, 0.07 v7.1.0, 0.09 v7.0.0, 0.13 v6.4.0, 0.19 v6.3.0, 0.12 v6.2.0, 0.16 v6.1.0, 0.23 v6.0.0, 0.17 v5.5.0, 0.19 v5.4.0, 0.18 v5.3.0, 0.26 v5.2.0, 0.10 v5.0.0, 0.12 v4.1.0, 0.13 v4.0.0, 0.12 v3.7.0, 0.10 v3.5.0, 0.11 v3.3.0, 0.14 v3.2.0 % 87.15/87.19 % Syntax : Number of formulae : 8 ( 6 unt; 0 def) % 87.15/87.19 % Number of atoms : 11 ( 5 equ) % 87.15/87.19 % Maximal formula atoms : 3 ( 1 avg) % 87.15/87.19 % Number of connectives : 4 ( 1 ~; 0 |; 1 &) % 87.15/87.19 % ( 0 <=>; 2 =>; 0 <=; 0 <~>) % 87.15/87.19 % Maximal formula depth : 7 ( 4 avg) % 87.15/87.19 % Maximal term depth : 3 ( 1 avg) % 87.15/87.19 % Number of predicates : 3 ( 2 usr; 0 prp; 1-2 aty) % 87.15/87.19 % Number of functors : 2 ( 2 usr; 0 con; 2-2 aty) % 87.15/87.19 % Number of variables : 18 ( 16 !; 2 ?) % 87.15/87.19 % SPC : FOF_THM_RFO_SEQ % 87.15/87.19 % 87.15/87.19 % Comments : Translated by MPTP 0.2 from the original problem in the Mizar % 87.15/87.19 % library, www.mizar.org % 87.15/87.19 %------------------------------------------------------------------------------ % 87.15/87.19 fof(commutativity_k3_xboole_0,axiom, % 87.15/87.19 ! [A,B] : set_intersection2(A,B) = set_intersection2(B,A) ). % 87.15/87.19 % 87.15/87.19 fof(idempotence_k3_xboole_0,axiom, % 87.15/87.19 ! [A,B] : set_intersection2(A,A) = A ). % 87.15/87.19 % 87.15/87.19 fof(rc1_xboole_0,axiom, % 87.15/87.19 ? [A] : empty(A) ). % 87.15/87.19 % 87.15/87.19 fof(rc2_xboole_0,axiom, % 87.15/87.19 ? [A] : ~ empty(A) ). % 87.15/87.19 % 87.15/87.19 fof(reflexivity_r1_tarski,axiom, % 87.15/87.19 ! [A,B] : subset(A,A) ). % 87.15/87.19 % 87.15/87.19 fof(t123_zfmisc_1,axiom, % 87.15/87.19 ! [A,B,C,D] : cartesian_product2(set_intersection2(A,B),set_intersection2(C,D)) = set_intersection2(cartesian_product2(A,C),cartesian_product2(B,D)) ). % 87.15/87.19 % 87.15/87.19 fof(t124_zfmisc_1,conjecture, % 87.15/87.19 ! [A,B,C,D] : % 87.15/87.19 ( ( subset(A,B) % 87.15/87.19 & subset(C,D) ) % 87.15/87.19 => set_intersection2(cartesian_product2(A,D),cartesian_product2(B,C)) = cartesian_product2(A,C) ) ). % 87.15/87.19 % 87.15/87.19 fof(t28_xboole_1,axiom, % 87.15/87.19 ! [A,B] : % 87.15/87.19 ( subset(A,B) % 87.15/87.19 => set_intersection2(A,B) = A ) ). % 87.15/87.19 % 87.15/87.19 %------------------------------------------------------------------------------ % 87.15/87.19 %------------------------------------------- % 87.15/87.19 % Proof found % 87.15/87.19 % SZS status Theorem for theBenchmark % 87.15/87.19 % SZS output start Proof % 87.15/87.20 %ClaNum:20(EqnAxiom:10) % 87.15/87.20 %VarNum:22(SingletonVarNum:10) % 87.15/87.20 %MaxLitNum:2 % 87.15/87.20 %MaxfuncDepth:2 % 87.15/87.20 %SharedTerms:15 % 87.15/87.20 %goalClause: 12 13 19 % 87.15/87.20 %singleGoalClaCount:3 % 87.15/87.20 [11]P1(a1) % 87.15/87.20 [12]P2(a3,a5) % 87.15/87.20 [13]P2(a6,a7) % 87.15/87.20 [18]~P1(a4) % 87.15/87.20 [19]~E(f8(f2(a3,a7),f2(a5,a6)),f2(a3,a6)) % 87.15/87.20 [14]P2(x141,x141) % 87.15/87.20 [15]E(f8(x151,x151),x151) % 87.15/87.20 [16]E(f8(x161,x162),f8(x162,x161)) % 87.15/87.20 [17]E(f2(f8(x171,x172),f8(x173,x174)),f8(f2(x171,x173),f2(x172,x174))) % 87.15/87.20 [20]~P2(x201,x202)+E(f8(x201,x202),x201) % 87.15/87.20 %EqnAxiom % 87.15/87.20 [1]E(x11,x11) % 87.15/87.20 [2]E(x22,x21)+~E(x21,x22) % 87.15/87.20 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 87.15/87.20 [4]~E(x41,x42)+E(f8(x41,x43),f8(x42,x43)) % 87.15/87.20 [5]~E(x51,x52)+E(f8(x53,x51),f8(x53,x52)) % 87.15/87.20 [6]~E(x61,x62)+E(f2(x61,x63),f2(x62,x63)) % 87.15/87.20 [7]~E(x71,x72)+E(f2(x73,x71),f2(x73,x72)) % 87.15/87.20 [8]~P1(x81)+P1(x82)+~E(x81,x82) % 87.15/87.20 [9]P2(x92,x93)+~E(x91,x92)+~P2(x91,x93) % 87.15/87.20 [10]P2(x103,x102)+~E(x101,x102)+~P2(x103,x101) % 87.15/87.20 % 87.15/87.20 %------------------------------------------- % 87.15/87.21 cnf(21,plain, % 87.15/87.21 (E(x211,f8(x211,x211))), % 87.15/87.21 inference(scs_inference,[],[15,2])). % 87.15/87.21 cnf(22,plain, % 87.15/87.21 (~E(f8(f2(a3,a7),f2(a5,a6)),f8(f2(a3,a6),f2(a3,a6)))), % 87.15/87.21 inference(scs_inference,[],[19,15,2,3])). % 87.15/87.21 cnf(23,plain, % 87.15/87.21 (E(f8(x231,x231),x231)), % 87.15/87.21 inference(rename_variables,[],[15])). % 87.15/87.21 cnf(24,plain, % 87.15/87.21 (P2(x241,f8(x241,x241))), % 87.15/87.21 inference(scs_inference,[],[19,14,15,23,2,3,9])). % 87.15/87.21 cnf(25,plain, % 87.15/87.21 (P2(x251,x251)), % 87.15/87.21 inference(rename_variables,[],[14])). % 87.15/87.21 cnf(26,plain, % 87.15/87.21 (P2(f8(x261,x261),x261)), % 87.15/87.21 inference(scs_inference,[],[19,14,25,15,23,2,3,9,10])). % 87.15/87.21 cnf(28,plain, % 87.15/87.21 (~P1(f8(a4,a4))), % 87.15/87.21 inference(scs_inference,[],[19,14,25,15,23,18,2,3,9,10,8])). % 87.15/87.21 cnf(30,plain, % 87.15/87.21 (E(f8(f2(x301,x302),f2(x303,x304)),f2(f8(x301,x303),f8(x302,x304)))), % 87.15/87.21 inference(scs_inference,[],[17,2])). % 87.15/87.21 cnf(31,plain, % 87.15/87.21 (P2(a3,f8(a5,a5))), % 87.15/87.21 inference(scs_inference,[],[12,21,17,2,10])). % 87.15/87.21 cnf(32,plain, % 87.15/87.21 (E(x321,f8(x321,x321))), % 87.15/87.21 inference(rename_variables,[],[21])). % 87.15/87.21 cnf(33,plain, % 87.15/87.21 (P2(f8(a3,a3),a5)), % 87.15/87.21 inference(scs_inference,[],[12,21,32,17,2,10,9])). % 87.15/87.21 cnf(34,plain, % 87.15/87.21 (E(x341,f8(x341,x341))), % 87.15/87.21 inference(rename_variables,[],[21])). % 87.15/87.21 cnf(35,plain, % 87.15/87.21 (P1(f8(a1,a1))), % 87.15/87.21 inference(scs_inference,[],[12,21,32,34,11,17,2,10,9,8])). % 87.15/87.21 cnf(37,plain, % 87.15/87.21 (~E(f8(f2(a3,a7),f2(a5,a6)),f2(f8(a3,a3),f8(a6,a6)))), % 87.15/87.21 inference(scs_inference,[],[12,21,32,34,22,11,17,2,10,9,8,3])). % 87.15/87.21 cnf(39,plain, % 87.15/87.21 (P2(f8(a6,a6),a7)), % 87.15/87.21 inference(scs_inference,[],[13,21,9])). % 87.15/87.21 cnf(40,plain, % 87.15/87.21 (E(x401,f8(x401,x401))), % 87.15/87.21 inference(rename_variables,[],[21])). % 87.15/87.21 cnf(41,plain, % 87.15/87.21 (P1(f8(f8(a1,a1),f8(a1,a1)))), % 87.15/87.21 inference(scs_inference,[],[13,21,40,35,9,8])). % 87.15/87.21 cnf(42,plain, % 87.15/87.21 (E(x421,f8(x421,x421))), % 87.15/87.21 inference(rename_variables,[],[21])). % 87.15/87.21 cnf(43,plain, % 87.15/87.21 (P2(a6,f8(a7,a7))), % 87.15/87.21 inference(scs_inference,[],[13,21,40,42,35,9,8,10])). % 87.15/87.21 cnf(58,plain, % 87.15/87.21 (P2(f8(a3,a3),f8(a5,a5))), % 87.15/87.21 inference(scs_inference,[],[21,31,9])). % 87.15/87.21 cnf(63,plain, % 87.15/87.21 (E(x631,f8(x631,x631))), % 87.15/87.21 inference(rename_variables,[],[21])). % 87.15/87.21 cnf(64,plain, % 87.15/87.21 (P2(f8(a3,a3),f8(f8(a5,a5),f8(a5,a5)))), % 87.15/87.21 inference(scs_inference,[],[21,63,58,9,10])). % 87.15/87.21 cnf(67,plain, % 87.15/87.21 (E(x671,f8(x671,x671))), % 87.15/87.21 inference(rename_variables,[],[21])). % 87.15/87.21 cnf(68,plain, % 87.15/87.21 (P2(a6,f8(f8(a7,a7),f8(a7,a7)))), % 87.15/87.21 inference(scs_inference,[],[21,67,64,43,9,10])). % 87.15/87.21 cnf(71,plain, % 87.15/87.21 (E(x711,f8(x711,x711))), % 87.15/87.21 inference(rename_variables,[],[21])). % 87.15/87.21 cnf(72,plain, % 87.15/87.21 (P2(f8(a6,a6),f8(a7,a7))), % 87.15/87.21 inference(scs_inference,[],[21,71,33,39,9,10])). % 87.15/87.21 cnf(75,plain, % 87.15/87.21 (E(x751,f8(x751,x751))), % 87.15/87.21 inference(rename_variables,[],[21])). % 87.15/87.21 cnf(76,plain, % 87.15/87.21 (P2(f8(a6,a6),f8(f8(a7,a7),f8(a7,a7)))), % 87.15/87.21 inference(scs_inference,[],[21,75,72,9,10])). % 87.15/87.21 cnf(80,plain, % 87.15/87.21 (P2(f8(f2(x801,x802),f2(x803,x804)),f2(f8(x801,x803),f8(x802,x804)))), % 87.15/87.21 inference(scs_inference,[],[30,21,76,14,9,10])). % 87.15/87.21 cnf(84,plain, % 87.15/87.21 (P2(f2(f8(x841,x842),f8(x843,x844)),f8(f2(x841,x843),f2(x842,x844)))), % 87.15/87.21 inference(scs_inference,[],[30,14,9])). % 87.15/87.21 cnf(86,plain, % 87.15/87.21 (E(f8(f8(a6,a6),a7),f8(a6,a6))), % 87.15/87.21 inference(scs_inference,[],[13,21,20,9])). % 87.15/87.21 cnf(87,plain, % 87.15/87.21 (E(f8(a6,a6),f8(f8(a6,a6),a7))), % 87.15/87.21 inference(scs_inference,[],[86,2])). % 87.15/87.21 cnf(88,plain, % 87.15/87.21 (E(f8(a7,f8(a6,a6)),f8(a6,a6))), % 87.15/87.21 inference(scs_inference,[],[86,16,2,3])). % 87.15/87.21 cnf(92,plain, % 87.15/87.21 (E(f8(a6,a6),f8(a7,f8(a6,a6)))), % 87.15/87.21 inference(scs_inference,[],[88,2])). % 87.15/87.21 cnf(93,plain, % 87.15/87.21 (E(a6,f8(f8(a6,a6),a7))), % 87.15/87.21 inference(scs_inference,[],[21,88,87,2,3])). % 87.15/87.21 cnf(97,plain, % 87.15/87.21 (E(f8(f8(a6,a6),a7),a6)), % 87.15/87.21 inference(scs_inference,[],[93,2])). % 87.15/87.21 cnf(98,plain, % 87.15/87.21 (E(a6,f8(a7,f8(a6,a6)))), % 87.15/87.21 inference(scs_inference,[],[21,92,93,2,3])). % 87.15/87.21 cnf(102,plain, % 87.15/87.21 (E(f8(a7,f8(a6,a6)),a6)), % 87.15/87.21 inference(scs_inference,[],[98,2])). % 87.15/87.21 cnf(124,plain, % 87.15/87.21 (E(f8(x1241,x1241),x1241)), % 87.15/87.21 inference(rename_variables,[],[15])). % 87.15/87.21 cnf(127,plain, % 87.15/87.21 (P2(f8(f8(x1271,x1271),f8(x1271,x1271)),x1271)), % 87.15/87.21 inference(scs_inference,[],[15,124,92,24,26,3,9,10])). % 87.15/87.21 cnf(129,plain, % 87.15/87.21 (E(f8(a7,f8(a6,a6)),f8(f8(a6,a6),f8(a6,a6)))), % 87.15/87.21 inference(scs_inference,[],[15,124,92,24,26,3,9,10,2])). % 87.15/87.21 cnf(143,plain, % 87.15/87.21 (P2(f8(x1431,x1432),f8(x1432,x1431))), % 87.15/87.21 inference(scs_inference,[],[16,14,9])). % 87.15/87.21 cnf(145,plain, % 87.15/87.21 (P2(f8(f8(x1451,x1452),f8(x1451,x1452)),f8(x1452,x1451))), % 87.15/87.21 inference(scs_inference,[],[16,14,26,9,10])). % 87.15/87.21 cnf(147,plain, % 87.15/87.21 (P2(f8(x1471,x1472),f8(f8(x1472,x1471),f8(x1472,x1471)))), % 87.15/87.21 inference(scs_inference,[],[16,24,9])). % 87.15/87.21 cnf(149,plain, % 87.15/87.21 (P2(f2(f8(x1491,x1492),f8(x1493,x1494)),f8(f2(x1492,x1494),f2(x1491,x1493)))), % 87.15/87.21 inference(scs_inference,[],[16,24,84,9,10])). % 87.15/87.21 cnf(166,plain, % 87.15/87.21 (E(f2(f8(x1661,x1661),x1662),f2(x1661,x1662))), % 87.15/87.21 inference(scs_inference,[],[21,2,6])). % 87.15/87.21 cnf(167,plain, % 87.15/87.21 (E(f2(x1671,x1672),f2(f8(x1671,x1671),x1672))), % 87.15/87.21 inference(scs_inference,[],[166,2])). % 87.15/87.21 cnf(168,plain, % 87.15/87.21 (~E(f8(f2(a3,a7),f2(a5,a6)),f2(f8(a3,a3),a6))), % 87.15/87.21 inference(scs_inference,[],[19,166,2,3])). % 87.15/87.21 cnf(177,plain, % 87.15/87.21 (~E(f8(f2(a3,a7),f2(a5,a6)),f2(a3,f8(a6,a6)))), % 87.15/87.21 inference(scs_inference,[],[167,37,3])). % 87.15/87.21 cnf(198,plain, % 87.15/87.21 (P2(f8(f2(x1981,x1982),f2(x1981,x1983)),f2(x1981,f8(x1982,x1983)))), % 87.15/87.21 inference(scs_inference,[],[80,166,10])). % 87.15/87.21 cnf(200,plain, % 87.15/87.21 (E(f2(f8(x2001,x2001),x2002),f2(x2001,x2002))), % 87.15/87.21 inference(rename_variables,[],[166])). % 87.15/87.21 cnf(201,plain, % 87.15/87.21 (P2(f2(x2011,f8(x2012,x2013)),f8(f2(x2011,x2012),f2(x2011,x2013)))), % 87.15/87.21 inference(scs_inference,[],[80,84,166,200,10,9])). % 87.15/87.21 cnf(219,plain, % 87.15/87.21 (E(a3,f8(a3,a5))), % 87.15/87.21 inference(scs_inference,[],[12,2,20])). % 87.15/87.21 cnf(220,plain, % 87.15/87.21 (E(f8(a3,a5),a3)), % 87.15/87.21 inference(scs_inference,[],[219,2])). % 87.15/87.21 cnf(221,plain, % 87.15/87.21 (E(f8(a3,a3),f8(a3,a5))), % 87.15/87.21 inference(scs_inference,[],[219,15,2,3])). % 87.15/87.21 cnf(223,plain, % 87.15/87.21 (P2(f2(x2231,f8(x2232,x2233)),f2(f8(x2231,x2231),f8(x2232,x2233)))), % 87.15/87.21 inference(scs_inference,[],[30,201,219,15,2,3,10])). % 87.15/87.21 cnf(229,plain, % 87.15/87.21 (E(f8(a3,a5),f8(a3,a3))), % 87.15/87.21 inference(scs_inference,[],[221,2])). % 87.15/87.21 cnf(232,plain, % 87.15/87.21 (P2(f2(f8(x2321,x2321),f8(x2322,x2323)),f2(x2321,f8(x2322,x2323)))), % 87.15/87.21 inference(scs_inference,[],[30,167,198,223,221,2,10,9])). % 87.15/87.21 cnf(239,plain, % 87.15/87.21 (E(f2(f8(x2391,x2391),x2392),f2(x2391,x2392))), % 87.15/87.21 inference(rename_variables,[],[166])). % 87.15/87.21 cnf(243,plain, % 87.15/87.21 (E(f8(f8(a6,a6),f8(a6,a6)),a6)), % 87.15/87.21 inference(scs_inference,[],[98,129,166,239,232,149,3,10,9,2])). % 87.15/87.21 cnf(278,plain, % 87.15/87.21 (P2(f8(a3,a5),f8(a5,a5))), % 87.15/87.21 inference(scs_inference,[],[33,221,21,9,10])). % 87.15/87.21 cnf(285,plain, % 87.15/87.21 (~E(f2(a3,a6),f2(f8(a3,a5),f8(a7,a6)))), % 87.15/87.21 inference(scs_inference,[],[19,17,2,3])). % 87.15/87.21 cnf(286,plain, % 87.15/87.21 (E(f8(a3,a3),f8(f8(a3,a3),f8(a5,a5)))), % 87.15/87.21 inference(scs_inference,[],[58,20,2])). % 87.15/87.21 cnf(287,plain, % 87.15/87.21 (E(f8(f8(a3,a3),f8(a5,a5)),f8(a3,a3))), % 87.15/87.21 inference(scs_inference,[],[286,2])). % 87.15/87.21 cnf(288,plain, % 87.15/87.21 (E(f8(a3,a5),f8(f8(a3,a3),f8(a5,a5)))), % 87.15/87.21 inference(scs_inference,[],[229,286,2,3])). % 87.15/87.21 cnf(299,plain, % 87.15/87.21 (E(f8(f8(a6,a6),f8(f8(a7,a7),f8(a7,a7))),f8(a6,a6))), % 87.15/87.21 inference(scs_inference,[],[72,21,20,10])). % 87.15/87.21 cnf(300,plain, % 87.15/87.21 (E(f8(a6,a6),f8(f8(a6,a6),f8(f8(a7,a7),f8(a7,a7))))), % 87.15/87.21 inference(scs_inference,[],[299,2])). % 87.15/87.21 cnf(326,plain, % 87.15/87.21 (E(f8(f8(a3,a5),x3261),f8(a3,x3261))), % 87.15/87.21 inference(scs_inference,[],[12,20,4])). % 87.15/87.21 cnf(327,plain, % 87.15/87.21 (E(f8(a3,x3271),f8(f8(a3,a5),x3271))), % 87.15/87.21 inference(scs_inference,[],[326,2])). % 87.15/87.21 cnf(328,plain, % 87.15/87.21 (E(f8(a3,a5),f8(a3,f8(a3,a5)))), % 87.15/87.21 inference(scs_inference,[],[21,326,2,3])). % 87.15/87.21 cnf(334,plain, % 87.15/87.21 (E(f8(a3,a3),f8(f8(a3,a5),a5))), % 87.15/87.21 inference(scs_inference,[],[221,327,328,2,3])). % 87.15/87.21 cnf(383,plain, % 87.15/87.21 (E(f8(x3831,f8(a3,a5)),f8(x3831,a3))), % 87.15/87.21 inference(scs_inference,[],[12,20,5])). % 87.15/87.21 cnf(384,plain, % 87.15/87.21 (E(f8(x3841,a3),f8(x3841,f8(a3,a5)))), % 87.15/87.21 inference(scs_inference,[],[383,2])). % 87.15/87.21 cnf(407,plain, % 87.15/87.21 (E(a6,f8(a6,a7))), % 87.15/87.21 inference(scs_inference,[],[13,20,2])). % 87.15/87.21 cnf(408,plain, % 87.15/87.21 (E(f8(a6,a7),a6)), % 87.15/87.21 inference(scs_inference,[],[407,2])). % 87.15/87.21 cnf(409,plain, % 87.15/87.21 (E(a3,f8(f8(a3,a3),f8(a5,a5)))), % 87.15/87.21 inference(scs_inference,[],[219,288,407,2,3])). % 87.15/87.21 cnf(420,plain, % 87.15/87.21 (E(f8(f8(a3,a3),f8(a5,a5)),a3)), % 87.15/87.21 inference(scs_inference,[],[409,2])). % 87.15/87.21 cnf(421,plain, % 87.15/87.21 (E(a3,f8(f8(a3,a5),a5))), % 87.15/87.21 inference(scs_inference,[],[219,327,409,2,3])). % 87.15/87.21 cnf(423,plain, % 87.15/87.21 (P2(f8(a3,a5),f8(a3,a3))), % 87.15/87.21 inference(scs_inference,[],[219,327,24,409,2,3,9])). % 87.15/87.22 cnf(429,plain, % 87.15/87.22 (E(a3,f8(a3,f8(a3,a5)))), % 87.15/87.22 inference(scs_inference,[],[219,328,421,2,3])). % 87.15/87.22 cnf(436,plain, % 87.15/87.22 (E(f8(a3,f8(a3,a5)),a3)), % 87.15/87.22 inference(scs_inference,[],[429,2])). % 87.15/87.22 cnf(437,plain, % 87.15/87.22 (E(f8(f8(a6,a6),a7),f8(a6,a7))), % 87.15/87.22 inference(scs_inference,[],[97,429,407,2,3])). % 87.15/87.22 cnf(441,plain, % 87.15/87.22 (E(f8(a6,a6),f8(a6,a7))), % 87.15/87.22 inference(scs_inference,[],[87,437,2,3])). % 87.15/87.22 cnf(444,plain, % 87.15/87.22 (E(f8(a6,a7),f8(a6,a6))), % 87.15/87.22 inference(scs_inference,[],[441,2])). % 87.15/87.22 cnf(458,plain, % 87.15/87.22 (P2(f8(x4581,x4582),f8(x4582,x4581))), % 87.15/87.22 inference(rename_variables,[],[143])). % 87.15/87.22 cnf(459,plain, % 87.15/87.22 (P2(f8(a5,a3),a3)), % 87.15/87.22 inference(scs_inference,[],[220,143,458,9,10])). % 87.15/87.22 cnf(480,plain, % 87.15/87.22 (P2(f8(a3,a3),f8(a5,a3))), % 87.15/87.22 inference(scs_inference,[],[229,143,9])). % 87.15/87.22 cnf(481,plain, % 87.15/87.22 (P2(f8(x4811,x4812),f8(x4812,x4811))), % 87.15/87.22 inference(rename_variables,[],[143])). % 87.15/87.22 cnf(482,plain, % 87.15/87.22 (P2(f8(a5,a3),f8(a3,a3))), % 87.15/87.22 inference(scs_inference,[],[229,143,481,9,10])). % 87.15/87.22 cnf(493,plain, % 87.15/87.22 (E(f8(f8(a6,a6),f8(a6,a6)),f8(a6,a7))), % 87.15/87.22 inference(scs_inference,[],[243,407,3])). % 87.15/87.22 cnf(495,plain, % 87.15/87.22 (E(f8(a3,f8(a5,a5)),a3)), % 87.15/87.22 inference(scs_inference,[],[12,21,20,10])). % 87.15/87.22 cnf(496,plain, % 87.15/87.22 (E(a3,f8(a3,f8(a5,a5)))), % 87.15/87.22 inference(scs_inference,[],[495,2])). % 87.15/87.22 cnf(497,plain, % 87.15/87.22 (E(f8(f8(a3,a5),f8(a5,a5)),a3)), % 87.15/87.22 inference(scs_inference,[],[495,326,2,3])). % 87.15/87.22 cnf(502,plain, % 87.15/87.22 (E(a3,f8(f8(a3,a5),f8(a5,a5)))), % 87.15/87.22 inference(scs_inference,[],[497,2])). % 87.15/87.22 cnf(503,plain, % 87.15/87.22 (E(f8(a3,a5),f8(a3,f8(a5,a5)))), % 87.15/87.22 inference(scs_inference,[],[220,497,496,2,3])). % 87.15/87.22 cnf(515,plain, % 87.15/87.22 (E(f8(a3,a3),f8(a3,f8(a5,a5)))), % 87.15/87.22 inference(scs_inference,[],[221,503,2,3])). % 87.15/87.22 cnf(517,plain, % 87.15/87.22 (E(f8(a3,f8(a5,a5)),f8(a3,a3))), % 87.15/87.22 inference(scs_inference,[],[515,2])). % 87.15/87.22 cnf(518,plain, % 87.15/87.22 (E(f8(a3,a5),f8(f8(a3,a5),f8(a5,a5)))), % 87.15/87.22 inference(scs_inference,[],[220,502,515,2,3])). % 87.15/87.22 cnf(524,plain, % 87.15/87.22 (E(f8(a3,a3),f8(f8(a3,a5),f8(a5,a5)))), % 87.15/87.22 inference(scs_inference,[],[221,518,2,3])). % 87.15/87.22 cnf(541,plain, % 87.15/87.22 (~E(f2(a3,a6),f8(f2(a3,a7),f2(a5,a6)))), % 87.15/87.22 inference(scs_inference,[],[285,30,3])). % 87.15/87.22 cnf(547,plain, % 87.15/87.22 (~E(f2(a3,a6),f8(f2(a5,a6),f2(a3,a7)))), % 87.15/87.22 inference(scs_inference,[],[541,16,3])). % 87.15/87.22 cnf(550,plain, % 87.15/87.22 (~E(f2(a3,a6),f2(f8(a5,a3),f8(a6,a7)))), % 87.15/87.22 inference(scs_inference,[],[547,17,3])). % 87.15/87.22 cnf(558,plain, % 87.15/87.22 (P2(f8(f8(a3,a3),f8(a5,a5)),f8(a5,a5))), % 87.15/87.22 inference(scs_inference,[],[286,58,9])). % 87.15/87.22 cnf(589,plain, % 87.15/87.22 (P2(f8(x5891,x5892),f8(x5892,x5891))), % 87.15/87.22 inference(rename_variables,[],[143])). % 87.15/87.22 cnf(590,plain, % 87.15/87.22 (P2(f8(f8(a5,a5),f8(a3,a3)),f8(a3,a3))), % 87.15/87.22 inference(scs_inference,[],[287,334,143,589,3,9,10])). % 87.15/87.22 cnf(617,plain, % 87.15/87.22 (E(f8(f8(a6,a7),x6171),f8(a6,x6171))), % 87.15/87.22 inference(scs_inference,[],[13,20,4])). % 87.15/87.22 cnf(618,plain, % 87.15/87.22 (E(f8(a6,x6181),f8(f8(a6,a7),x6181))), % 87.15/87.22 inference(scs_inference,[],[617,2])). % 87.15/87.22 cnf(648,plain, % 87.15/87.22 (E(f8(a7,f8(a6,a6)),f8(f8(a6,a7),a6))), % 87.15/87.22 inference(scs_inference,[],[88,618,3])). % 87.15/87.22 cnf(659,plain, % 87.15/87.22 (E(a6,f8(f8(a6,a7),a6))), % 87.15/87.22 inference(scs_inference,[],[98,648,3])). % 87.15/87.22 cnf(661,plain, % 87.15/87.22 (E(f8(f8(a6,a7),a6),a6)), % 87.15/87.22 inference(scs_inference,[],[300,98,72,648,3,9,2])). % 87.15/87.22 cnf(665,plain, % 87.15/87.22 (P2(f8(f8(a6,a6),f8(f8(a7,a7),f8(a7,a7))),a6)), % 87.15/87.22 inference(scs_inference,[],[300,97,26,659,3,9])). % 87.15/87.22 cnf(679,plain, % 87.15/87.22 (E(f8(f8(a3,a5),x6791),f8(a3,x6791))), % 87.15/87.22 inference(rename_variables,[],[326])). % 87.15/87.22 cnf(681,plain, % 87.15/87.22 (P2(x6811,x6811)), % 87.15/87.22 inference(rename_variables,[],[14])). % 87.15/87.22 cnf(682,plain, % 87.15/87.22 (P2(f8(f8(a3,a5),x6821),f8(a3,x6821))), % 87.15/87.22 inference(scs_inference,[],[326,679,334,14,681,3,9,10])). % 87.15/87.22 cnf(687,plain, % 87.15/87.22 (E(f8(f8(a3,a5),x6871),f8(a3,x6871))), % 87.15/87.22 inference(rename_variables,[],[326])). % 87.15/87.22 cnf(688,plain, % 87.15/87.22 (P2(f8(a3,x6881),f8(x6881,f8(a3,a5)))), % 87.15/87.22 inference(scs_inference,[],[326,687,328,143,3,9])). % 87.15/87.22 cnf(689,plain, % 87.15/87.22 (P2(f8(x6891,x6892),f8(x6892,x6891))), % 87.15/87.22 inference(rename_variables,[],[143])). % 87.15/87.22 cnf(690,plain, % 87.15/87.22 (P2(f8(x6901,f8(a3,a5)),f8(a3,x6901))), % 87.15/87.22 inference(scs_inference,[],[326,687,328,143,689,3,9,10])). % 87.15/87.22 cnf(694,plain, % 87.15/87.22 (E(f8(f8(a3,a5),f8(a3,a5)),a3)), % 87.15/87.22 inference(scs_inference,[],[326,436,3])). % 87.15/87.22 cnf(712,plain, % 87.15/87.22 (E(f8(f8(a3,a5),a3),f8(a3,f8(a5,a5)))), % 87.15/87.22 inference(scs_inference,[],[326,515,3])). % 87.15/87.22 cnf(713,plain, % 87.15/87.22 (E(f8(f8(a3,a5),x7131),f8(a3,x7131))), % 87.15/87.22 inference(rename_variables,[],[326])). % 87.15/87.22 cnf(716,plain, % 87.15/87.22 (E(f8(f8(a3,a5),x7161),f8(a3,x7161))), % 87.15/87.22 inference(rename_variables,[],[326])). % 87.15/87.22 cnf(720,plain, % 87.15/87.22 (E(f8(a3,f8(a5,a5)),f8(f8(a3,a5),a3))), % 87.15/87.22 inference(scs_inference,[],[326,713,716,515,147,145,3,9,10,2])). % 87.15/87.22 cnf(722,plain, % 87.15/87.22 (E(f8(f8(a3,a5),a3),f8(f8(a3,a5),f8(a5,a5)))), % 87.15/87.22 inference(scs_inference,[],[326,524,3])). % 87.15/87.22 cnf(760,plain, % 87.15/87.22 (E(a3,f8(f8(a3,a5),a3))), % 87.15/87.22 inference(scs_inference,[],[496,720,3])). % 87.15/87.22 cnf(762,plain, % 87.15/87.22 (E(f8(a3,x7621),f8(f8(a3,a5),x7621))), % 87.15/87.22 inference(rename_variables,[],[327])). % 87.15/87.22 cnf(763,plain, % 87.15/87.22 (P2(f8(x7631,a3),f8(f8(a3,a5),x7631))), % 87.15/87.22 inference(scs_inference,[],[327,762,496,33,143,720,3,9,10])). % 87.15/87.22 cnf(765,plain, % 87.15/87.22 (E(f8(f8(a3,a5),a3),a3)), % 87.15/87.22 inference(scs_inference,[],[327,762,496,33,143,720,3,9,10,2])). % 87.15/87.22 cnf(773,plain, % 87.15/87.22 (P2(f8(f8(a3,a5),x7731),f8(x7731,a3))), % 87.15/87.22 inference(scs_inference,[],[327,143,9])). % 87.15/87.22 cnf(783,plain, % 87.15/87.22 (P2(f8(f8(a3,a5),a5),f8(a5,a5))), % 87.15/87.22 inference(scs_inference,[],[327,278,9])). % 87.15/87.22 cnf(784,plain, % 87.15/87.22 (E(f8(a3,x7841),f8(f8(a3,a5),x7841))), % 87.15/87.22 inference(rename_variables,[],[327])). % 87.15/87.22 cnf(785,plain, % 87.15/87.22 (P2(f8(a3,a5),f8(f8(a3,a5),a3))), % 87.15/87.22 inference(scs_inference,[],[327,784,278,423,9,10])). % 87.15/87.22 cnf(794,plain, % 87.15/87.22 (E(f8(a3,x7941),f8(f8(a3,a5),x7941))), % 87.15/87.22 inference(rename_variables,[],[327])). % 87.15/87.22 cnf(795,plain, % 87.15/87.22 (P2(f8(a5,a3),f8(f8(a3,a5),a3))), % 87.15/87.22 inference(scs_inference,[],[327,794,26,482,9,10])). % 87.15/87.22 cnf(821,plain, % 87.15/87.22 (E(f8(a3,x8211),f8(f8(a3,a5),x8211))), % 87.15/87.22 inference(rename_variables,[],[327])). % 87.15/87.22 cnf(822,plain, % 87.15/87.22 (P2(f8(f8(a3,a5),a3),f8(a5,a3))), % 87.15/87.22 inference(scs_inference,[],[327,821,480,590,10,9])). % 87.15/87.22 cnf(849,plain, % 87.15/87.22 (E(f2(f8(a3,a5),x8491),f2(a3,x8491))), % 87.15/87.22 inference(scs_inference,[],[12,20,6])). % 87.15/87.22 cnf(851,plain, % 87.15/87.22 (~E(f8(f2(a3,a7),f2(a5,a6)),f2(f8(a3,a5),a6))), % 87.15/87.22 inference(scs_inference,[],[19,849,2,3])). % 87.15/87.22 cnf(898,plain, % 87.15/87.22 (E(f8(a6,f8(a7,a7)),a6)), % 87.15/87.22 inference(scs_inference,[],[13,21,20,10])). % 87.15/87.22 cnf(899,plain, % 87.15/87.22 (E(a6,f8(a6,f8(a7,a7)))), % 87.15/87.22 inference(scs_inference,[],[898,2])). % 87.15/87.22 cnf(900,plain, % 87.15/87.22 (E(f8(f8(a3,a5),f8(a3,a5)),f8(a3,f8(a5,a5)))), % 87.15/87.22 inference(scs_inference,[],[383,712,898,2,3])). % 87.15/87.22 cnf(901,plain, % 87.15/87.22 (E(f8(x9011,f8(a3,a5)),f8(x9011,a3))), % 87.15/87.22 inference(rename_variables,[],[383])). % 87.15/87.22 cnf(902,plain, % 87.15/87.22 (P2(f8(x9021,f8(a3,a5)),f8(x9021,a3))), % 87.15/87.22 inference(scs_inference,[],[383,901,14,712,898,2,3,10])). % 87.15/87.22 cnf(910,plain, % 87.15/87.22 (E(f8(f8(a3,a5),f8(a3,a5)),f8(f8(a3,a5),f8(a5,a5)))), % 87.15/87.22 inference(scs_inference,[],[383,722,900,2,3])). % 87.15/87.22 cnf(926,plain, % 87.15/87.22 (E(f8(f8(a6,a6),a7),f8(a6,f8(a7,a7)))), % 87.15/87.22 inference(scs_inference,[],[97,910,899,2,3])). % 87.15/87.22 cnf(928,plain, % 87.15/87.22 (E(f8(a6,f8(a7,a7)),f8(f8(a6,a6),a7))), % 87.15/87.22 inference(scs_inference,[],[926,2])). % 87.15/87.22 cnf(929,plain, % 87.15/87.22 (E(f8(a6,a6),f8(a6,f8(a7,a7)))), % 87.15/87.22 inference(scs_inference,[],[87,926,2,3])). % 87.15/87.22 cnf(968,plain, % 87.15/87.22 (E(a6,f8(f8(a6,a7),a7))), % 87.15/87.22 inference(scs_inference,[],[407,618,3])). % 87.15/87.22 cnf(973,plain, % 87.15/87.22 (E(f8(f8(a6,a7),a7),a6)), % 87.15/87.22 inference(scs_inference,[],[407,13,618,14,3,10,9,2])). % 87.15/87.22 cnf(980,plain, % 87.15/87.22 (E(f8(f8(a6,a6),a7),f8(f8(a6,a7),a7))), % 87.15/87.22 inference(scs_inference,[],[97,968,3])). % 87.15/87.22 cnf(981,plain, % 87.15/87.22 (P2(f8(a6,a6),f8(a6,a7))), % 87.15/87.22 inference(scs_inference,[],[407,97,26,968,3,10])). % 87.15/87.22 cnf(987,plain, % 87.15/87.22 (E(f8(a6,a6),f8(f8(a6,a7),a7))), % 87.15/87.22 inference(scs_inference,[],[87,980,3])). % 87.15/87.22 cnf(1001,plain, % 87.15/87.22 (P2(f8(a6,a7),f8(f8(a7,a7),f8(a7,a7)))), % 87.15/87.22 inference(scs_inference,[],[407,68,665,10,9])). % 87.15/87.22 cnf(1012,plain, % 87.15/87.22 (P2(f8(a7,a6),a6)), % 87.15/87.22 inference(scs_inference,[],[408,659,143,3,10])). % 87.15/87.22 cnf(1013,plain, % 87.15/87.22 (P2(f8(x10131,x10132),f8(x10132,x10131))), % 87.15/87.22 inference(rename_variables,[],[143])). % 87.15/87.22 cnf(1014,plain, % 87.15/87.22 (P2(a6,f8(a7,a6))), % 87.15/87.22 inference(scs_inference,[],[408,659,143,1013,3,10,9])). % 87.15/87.22 cnf(1018,plain, % 87.15/87.22 (E(f8(a6,a7),f8(a6,f8(a7,a7)))), % 87.15/87.22 inference(scs_inference,[],[408,899,3])). % 87.15/87.22 cnf(1023,plain, % 87.15/87.22 (E(f8(a6,f8(a7,a7)),f8(a6,a7))), % 87.15/87.22 inference(scs_inference,[],[408,24,26,899,3,10,9,2])). % 87.15/87.22 cnf(1030,plain, % 87.15/87.22 (P2(f8(a7,a6),f8(a7,f8(a6,a6)))), % 87.15/87.22 inference(scs_inference,[],[98,1012,10])). % 87.15/87.22 cnf(1031,plain, % 87.15/87.22 (P2(f8(a7,f8(a6,a6)),f8(a7,a6))), % 87.15/87.22 inference(scs_inference,[],[98,1014,1012,10,9])). % 87.15/87.22 cnf(1035,plain, % 87.15/87.22 (P2(f8(a6,a6),f8(a7,a6))), % 87.15/87.22 inference(scs_inference,[],[88,21,1031,10,9])). % 87.15/87.22 cnf(1054,plain, % 87.15/87.22 (P2(f8(a7,a6),f8(a6,a6))), % 87.15/87.22 inference(scs_inference,[],[88,1030,10])). % 87.15/87.22 cnf(1125,plain, % 87.15/87.22 (E(f8(a6,f8(a7,a7)),f8(f8(a6,a6),f8(a6,a6)))), % 87.15/87.22 inference(scs_inference,[],[493,1018,3,2])). % 87.15/87.22 cnf(1145,plain, % 87.15/87.22 (P2(f8(a3,f8(a5,a5)),a3)), % 87.15/87.22 inference(scs_inference,[],[495,14,10])). % 87.15/87.22 cnf(1146,plain, % 87.15/87.22 (P2(x11461,x11461)), % 87.15/87.22 inference(rename_variables,[],[14])). % 87.15/87.22 cnf(1147,plain, % 87.15/87.22 (P2(a3,f8(a3,f8(a5,a5)))), % 87.15/87.22 inference(scs_inference,[],[495,14,1146,10,9])). % 87.15/87.22 cnf(1149,plain, % 87.15/87.22 (P2(f8(f8(a5,a5),a3),a3)), % 87.15/87.22 inference(scs_inference,[],[495,143,10])). % 87.15/87.22 cnf(1150,plain, % 87.15/87.22 (P2(f8(x11501,x11502),f8(x11502,x11501))), % 87.15/87.22 inference(rename_variables,[],[143])). % 87.15/87.22 cnf(1151,plain, % 87.15/87.22 (P2(a3,f8(f8(a5,a5),a3))), % 87.15/87.22 inference(scs_inference,[],[495,143,1150,10,9])). % 87.15/87.22 cnf(1157,plain, % 87.15/87.22 (E(f2(x11571,f8(a3,a5)),f2(x11571,a3))), % 87.15/87.22 inference(scs_inference,[],[12,20,7])). % 87.15/87.22 cnf(1158,plain, % 87.15/87.22 (E(f2(x11581,a3),f2(x11581,f8(a3,a5)))), % 87.15/87.22 inference(scs_inference,[],[1157,2])). % 87.15/87.22 cnf(1159,plain, % 87.15/87.22 (E(f8(f2(x11591,a3),f2(x11592,a5)),f2(f8(x11591,x11592),a3))), % 87.15/87.22 inference(scs_inference,[],[30,1157,2,3])). % 87.15/87.22 cnf(1162,plain, % 87.15/87.22 (P2(f8(f8(a3,a5),f8(a5,a5)),a3)), % 87.15/87.22 inference(scs_inference,[],[495,30,682,1157,2,3,10])). % 87.15/87.22 cnf(1173,plain, % 87.15/87.22 (E(f2(x11731,a3),f2(f8(x11731,x11731),f8(a3,a5)))), % 87.15/87.22 inference(scs_inference,[],[167,1158,1159,2,3])). % 87.15/87.22 cnf(1176,plain, % 87.15/87.22 (P2(f8(a3,f8(a5,a5)),f8(a3,a5))), % 87.15/87.22 inference(scs_inference,[],[167,219,1145,1158,1159,2,3,10])). % 87.15/87.22 cnf(1177,plain, % 87.15/87.22 (P2(f8(a3,a5),f8(a3,f8(a5,a5)))), % 87.15/87.22 inference(scs_inference,[],[167,219,1147,1145,1158,1159,2,3,10,9])). % 87.15/87.22 cnf(1184,plain, % 87.15/87.22 (E(f2(f8(x11841,x11841),f8(a3,a5)),f2(x11841,a3))), % 87.15/87.22 inference(scs_inference,[],[1173,2])). % 87.15/87.22 cnf(1185,plain, % 87.15/87.22 (E(f2(x11851,a3),f2(f8(f8(x11851,x11851),f8(x11851,x11851)),f8(a3,a5)))), % 87.15/87.22 inference(scs_inference,[],[167,1173,2,3])). % 87.15/87.22 cnf(1188,plain, % 87.15/87.22 (P2(f8(f8(a5,a5),a3),f8(a3,a5))), % 87.15/87.22 inference(scs_inference,[],[167,219,1149,1173,2,3,10])). % 87.15/87.22 cnf(1189,plain, % 87.15/87.22 (P2(f8(a3,a5),f8(f8(a5,a5),a3))), % 87.15/87.22 inference(scs_inference,[],[167,219,1151,1149,1173,2,3,10,9])). % 87.15/87.22 cnf(1200,plain, % 87.15/87.22 (E(f8(f2(x12001,a3),f2(x12001,a5)),f2(x12001,a3))), % 87.15/87.22 inference(scs_inference,[],[30,1184,1185,2,3])). % 87.15/87.22 cnf(1203,plain, % 87.15/87.22 (P2(f8(a3,a5),f8(f8(a5,a5),f8(a3,a5)))), % 87.15/87.22 inference(scs_inference,[],[30,384,1189,1184,1185,2,3,10])). % 87.15/87.22 cnf(1204,plain, % 87.15/87.22 (E(f8(x12041,a3),f8(x12041,f8(a3,a5)))), % 87.15/87.22 inference(rename_variables,[],[384])). % 87.15/87.22 cnf(1205,plain, % 87.15/87.22 (P2(f8(f8(a5,a5),f8(a3,a5)),f8(a3,a5))), % 87.15/87.22 inference(scs_inference,[],[30,384,1204,1189,1188,1184,1185,2,3,10,9])). % 87.15/87.22 cnf(1212,plain, % 87.15/87.22 (P2(f8(f8(a3,a5),f8(a5,a5)),f8(a3,a5))), % 87.15/87.22 inference(scs_inference,[],[219,1162,1200,2,10])). % 87.15/87.22 cnf(1219,plain, % 87.15/87.22 (P2(f8(a3,a3),f8(a3,f8(a5,a5)))), % 87.15/87.22 inference(scs_inference,[],[496,26,10])). % 87.15/87.22 cnf(1222,plain, % 87.15/87.22 (P2(f8(f8(a3,a3),f8(a3,a3)),f8(a3,f8(a5,a5)))), % 87.15/87.22 inference(scs_inference,[],[496,127,10])). % 87.15/87.22 cnf(1224,plain, % 87.15/87.22 (P2(f8(a3,f8(a5,a5)),f8(a5,a5))), % 87.15/87.22 inference(scs_inference,[],[496,31,127,10,9])). % 87.15/87.22 cnf(1227,plain, % 87.15/87.22 (P2(f8(a3,f8(a5,a5)),f8(a3,a3))), % 87.15/87.22 inference(scs_inference,[],[496,24,459,10,9])). % 87.15/87.22 cnf(1258,plain, % 87.15/87.22 (P2(f8(a3,a3),f8(f8(a3,a5),f8(a5,a5)))), % 87.15/87.22 inference(scs_inference,[],[327,1219,10])). % 87.15/87.22 cnf(1263,plain, % 87.15/87.22 (E(f8(a3,x12631),f8(f8(a3,a5),x12631))), % 87.15/87.22 inference(rename_variables,[],[327])). % 87.15/87.22 cnf(1264,plain, % 87.15/87.22 (P2(f8(f8(a3,a5),f8(a5,a5)),f8(a5,a5))), % 87.15/87.22 inference(scs_inference,[],[327,1263,1224,1222,10,9])). % 87.15/87.22 cnf(1269,plain, % 87.15/87.22 (P2(f8(f8(a3,a5),f8(a5,a5)),f8(a3,a3))), % 87.15/87.22 inference(scs_inference,[],[327,21,1227,1264,10,9])). % 87.15/87.22 cnf(1333,plain, % 87.15/87.22 (P2(f8(x13331,x13332),f8(x13332,x13331))), % 87.15/87.22 inference(rename_variables,[],[143])). % 87.15/87.22 cnf(1334,plain, % 87.15/87.22 (P2(f8(a3,a3),f8(f8(a5,a5),a3))), % 87.15/87.22 inference(scs_inference,[],[517,143,1333,10,9])). % 87.15/87.22 cnf(1337,plain, % 87.15/87.22 (P2(f8(f8(a5,a5),f8(a3,a5)),f8(a3,a3))), % 87.15/87.22 inference(scs_inference,[],[517,690,10])). % 87.15/87.22 cnf(1339,plain, % 87.15/87.22 (P2(f8(a3,a3),f8(f8(a5,a5),f8(a3,a5)))), % 87.15/87.22 inference(scs_inference,[],[517,690,688,10,9])). % 87.15/87.22 cnf(1434,plain, % 87.15/87.22 (E(f8(f8(a6,a7),x14341),f8(a6,x14341))), % 87.15/87.22 inference(rename_variables,[],[617])). % 87.15/87.22 cnf(1435,plain, % 87.15/87.22 (P2(f8(f8(a6,a7),x14351),f8(a6,x14351))), % 87.15/87.22 inference(scs_inference,[],[617,1434,928,14,3,10])). % 87.15/87.22 cnf(1442,plain, % 87.15/87.22 (E(f8(f8(a6,a7),x14421),f8(a6,x14421))), % 87.15/87.22 inference(rename_variables,[],[617])). % 87.15/87.22 cnf(1444,plain, % 87.15/87.22 (P2(f8(x14441,x14442),f8(x14442,x14441))), % 87.15/87.22 inference(rename_variables,[],[143])). % 87.15/87.22 cnf(1447,plain, % 87.15/87.22 (E(f8(a6,f8(a7,a7)),f8(f8(a6,a7),a6))), % 87.15/87.22 inference(scs_inference,[],[617,1442,929,143,1444,3,10,9,2])). % 87.15/87.22 cnf(1468,plain, % 87.15/87.22 (E(f8(f8(a6,a7),f8(a7,a7)),a6)), % 87.15/87.22 inference(scs_inference,[],[617,898,3])). % 87.15/87.22 cnf(1469,plain, % 87.15/87.22 (E(f8(f8(a6,a7),x14691),f8(a6,x14691))), % 87.15/87.22 inference(rename_variables,[],[617])). % 87.15/87.22 cnf(1472,plain, % 87.15/87.22 (E(f8(f8(a6,a7),x14721),f8(a6,x14721))), % 87.15/87.22 inference(rename_variables,[],[617])). % 87.15/87.22 cnf(1476,plain, % 87.15/87.22 (E(a6,f8(f8(a6,a7),f8(a7,a7)))), % 87.15/87.22 inference(scs_inference,[],[617,1469,1472,898,147,145,3,10,9,2])). % 87.15/87.22 cnf(1478,plain, % 87.15/87.22 (E(f8(f8(a6,a7),x14781),f8(a6,x14781))), % 87.15/87.22 inference(rename_variables,[],[617])). % 87.15/87.22 cnf(1479,plain, % 87.15/87.22 (P2(f8(f8(a3,a5),f8(a6,a7)),f8(a6,a3))), % 87.15/87.22 inference(scs_inference,[],[617,1478,987,773,3,10])). % 87.15/87.22 cnf(1481,plain, % 87.15/87.22 (E(f8(f8(a6,a7),x14811),f8(a6,x14811))), % 87.15/87.22 inference(rename_variables,[],[617])). % 87.15/87.22 cnf(1482,plain, % 87.15/87.22 (P2(f8(a6,a3),f8(f8(a3,a5),f8(a6,a7)))), % 87.15/87.22 inference(scs_inference,[],[617,1478,1481,987,773,763,3,10,9])). % 87.15/87.22 cnf(1487,plain, % 87.15/87.22 (E(f8(f8(a6,a7),x14871),f8(a6,x14871))), % 87.15/87.22 inference(rename_variables,[],[617])). % 87.15/87.22 cnf(1490,plain, % 87.15/87.22 (E(f8(f8(a6,a7),x14901),f8(a6,x14901))), % 87.15/87.22 inference(rename_variables,[],[617])). % 87.15/87.22 cnf(1494,plain, % 87.15/87.22 (E(f8(a6,a7),f8(f8(a6,a7),f8(a7,a7)))), % 87.15/87.22 inference(scs_inference,[],[617,1487,1490,1023,690,688,3,10,9,2])). % 87.15/87.22 cnf(1495,plain, % 87.15/87.22 (E(f8(x14951,f8(a6,a7)),f8(x14951,a6))), % 87.15/87.22 inference(scs_inference,[],[13,20,5])). % 87.15/87.22 cnf(1496,plain, % 87.15/87.22 (E(f8(x14961,a6),f8(x14961,f8(a6,a7)))), % 87.15/87.22 inference(scs_inference,[],[1495,2])). % 87.15/87.22 cnf(1497,plain, % 87.15/87.22 (E(f8(f8(a6,a7),a7),f8(a6,f8(a7,a7)))), % 87.15/87.22 inference(scs_inference,[],[617,1018,1495,2,3])). % 87.15/87.22 cnf(1498,plain, % 87.15/87.22 (E(f8(f8(a6,a7),x14981),f8(a6,x14981))), % 87.15/87.22 inference(rename_variables,[],[617])). % 87.15/87.22 cnf(1499,plain, % 87.15/87.22 (P2(f8(f8(a6,a7),f8(a3,a5)),f8(a6,a3))), % 87.15/87.22 inference(scs_inference,[],[617,1498,1018,902,1495,2,3,10])). % 87.15/87.22 cnf(1509,plain, % 87.15/87.22 (E(f8(f8(a6,a7),f8(a7,a7)),f8(f8(a6,a6),f8(a6,a6)))), % 87.15/87.22 inference(scs_inference,[],[617,1125,1497,2,3])). % 87.15/87.22 cnf(1524,plain, % 87.15/87.22 (E(f8(f8(a6,a7),f8(a7,a7)),f8(f8(a6,a7),a6))), % 87.15/87.22 inference(scs_inference,[],[617,1447,1509,2,3])). % 87.15/87.22 cnf(1532,plain, % 87.15/87.22 (E(f8(f8(a6,a7),a7),f8(f8(a6,a7),f8(a7,a7)))), % 87.15/87.22 inference(scs_inference,[],[617,1494,1524,2,3])). % 87.15/87.22 cnf(1540,plain, % 87.15/87.22 (E(f8(f8(a6,a7),f8(a6,a7)),f8(a6,a6))), % 87.15/87.22 inference(scs_inference,[],[617,1532,1495,2,3])). % 87.15/87.22 cnf(1548,plain, % 87.15/87.22 (E(f8(a6,a6),f8(f8(a6,a7),f8(a6,a7)))), % 87.15/87.22 inference(scs_inference,[],[1540,2])). % 87.15/87.22 cnf(1567,plain, % 87.15/87.22 (E(f8(a7,f8(a6,a6)),f8(f8(a6,a7),f8(a6,a7)))), % 87.15/87.22 inference(scs_inference,[],[88,1548,3])). % 87.15/87.22 cnf(1582,plain, % 87.15/87.22 (E(f8(f8(a6,a7),f8(a6,a7)),a6)), % 87.15/87.22 inference(scs_inference,[],[618,98,72,26,1567,3,10,9,2])). % 87.15/87.22 cnf(1610,plain, % 87.15/87.22 (E(f8(a6,f8(a6,a7)),a6)), % 87.15/87.22 inference(scs_inference,[],[618,1582,3])). % 87.15/87.22 cnf(1611,plain, % 87.15/87.22 (E(f8(a6,x16111),f8(f8(a6,a7),x16111))), % 87.15/87.22 inference(rename_variables,[],[618])). % 87.15/87.22 cnf(1612,plain, % 87.15/87.22 (P2(f8(a3,a6),f8(f8(a6,a7),f8(a3,a5)))), % 87.15/87.22 inference(scs_inference,[],[618,1611,688,1582,3,10])). % 87.15/87.22 cnf(1630,plain, % 87.15/87.22 (P2(f8(a6,a6),f8(f8(a6,a7),a7))), % 87.15/87.22 inference(scs_inference,[],[618,981,10])). % 87.15/87.22 cnf(1631,plain, % 87.15/87.22 (E(f8(a6,x16311),f8(f8(a6,a7),x16311))), % 87.15/87.22 inference(rename_variables,[],[618])). % 87.15/87.22 cnf(1632,plain, % 87.15/87.22 (P2(f8(f8(a6,a7),f8(a3,a5)),f8(a3,a6))), % 87.15/87.22 inference(scs_inference,[],[618,1631,690,981,10,9])). % 87.15/87.22 cnf(1695,plain, % 87.15/87.22 (P2(a6,f8(a7,f8(a6,a7)))), % 87.15/87.22 inference(scs_inference,[],[1496,1014,10])). % 87.15/87.22 cnf(1705,plain, % 87.15/87.22 (E(f8(x17051,a6),f8(x17051,f8(a6,a7)))), % 87.15/87.22 inference(rename_variables,[],[1496])). % 87.15/87.22 cnf(1706,plain, % 87.15/87.22 (P2(f8(a7,f8(a6,a7)),f8(a6,a6))), % 87.15/87.22 inference(scs_inference,[],[1496,1705,1031,1054,10,9])). % 87.15/87.22 cnf(1709,plain, % 87.15/87.22 (P2(f8(a6,a6),f8(a7,f8(a6,a7)))), % 87.15/87.22 inference(scs_inference,[],[1496,1035,10])). % 87.15/87.22 cnf(1789,plain, % 87.15/87.22 (~E(f8(f8(a1,a1),f8(a1,a1)),f8(a4,a4))), % 87.15/87.22 inference(scs_inference,[],[28,41,168,1479,1610,20,4,5,6,7,2,8])). % 87.15/87.22 cnf(1800,plain, % 87.15/87.22 (~E(a1,a4)), % 87.15/87.22 inference(scs_inference,[],[1789,1706,1476,11,18,20,7,5,6,4,2,8])). % 87.15/87.22 cnf(1811,plain, % 87.15/87.22 (~E(f8(f8(a1,a1),f8(a1,a1)),a4)), % 87.15/87.22 inference(scs_inference,[],[1800,1482,973,41,18,20,5,6,4,7,2,8])). % 87.15/87.22 cnf(1821,plain, % 87.15/87.22 (E(f2(a3,x18211),f2(f8(f8(a3,a5),a3),x18211))), % 87.15/87.22 inference(scs_inference,[],[1695,760,20,6])). % 87.15/87.22 cnf(1835,plain, % 87.15/87.22 (E(f2(f8(f8(a3,a5),a3),x18351),f2(a3,x18351))), % 87.15/87.22 inference(scs_inference,[],[1709,765,20,7,4,5,6])). % 87.15/87.22 cnf(1837,plain, % 87.15/87.22 (~E(f8(a1,a1),a4)), % 87.15/87.22 inference(scs_inference,[],[1811,1709,765,35,18,20,7,4,5,6,2,8])). % 87.15/87.22 cnf(1848,plain, % 87.15/87.22 (~E(f8(f2(a5,a6),f2(a3,a7)),f2(f8(a3,a5),a6))), % 87.15/87.22 inference(scs_inference,[],[1837,851,1499,694,16,20,4,5,6,7,2,3])). % 87.15/87.22 cnf(1874,plain, % 87.15/87.22 (~E(f8(f2(a5,a6),f2(a3,a7)),f2(a3,f8(a6,a6)))), % 87.15/87.22 inference(scs_inference,[],[1848,177,1632,420,16,20,6,7,4,5,2,3])). % 87.15/87.22 cnf(1917,plain, % 87.15/87.22 (~E(f2(a3,f8(a6,a6)),f8(f2(a5,a6),f2(a3,a7)))), % 87.15/87.22 inference(scs_inference,[],[1874,1630,968,20,6,4,7,5,2])). % 87.15/87.22 cnf(1937,plain, % 87.15/87.22 (~E(f2(f8(f8(a3,a5),a3),f8(a6,a6)),f8(f2(a5,a6),f2(a3,a7)))), % 87.15/87.22 inference(scs_inference,[],[1917,1612,550,1821,102,20,5,7,6,4,2,3])). % 87.15/87.22 cnf(1942,plain, % 87.15/87.22 (E(f2(x19421,f8(f8(a6,a7),f8(a6,a7))),f2(x19421,a6))), % 87.15/87.22 inference(scs_inference,[],[1205,1582,20,7])). % 87.15/87.22 cnf(1946,plain, % 87.15/87.22 (~E(f8(f2(a5,a6),f2(a3,a7)),f2(f8(f8(a3,a5),a3),f8(a6,a6)))), % 87.15/87.22 inference(scs_inference,[],[1937,1205,1582,20,7,4,6,5,2])). % 87.15/87.22 cnf(1961,plain, % 87.15/87.22 (~E(f8(f2(a3,a7),f2(a5,a6)),f2(f8(f8(a3,a5),a3),f8(a6,a6)))), % 87.15/87.22 inference(scs_inference,[],[1946,1337,22,1468,16,20,4,5,6,7,2,3])). % 87.15/87.22 cnf(1970,plain, % 87.15/87.22 (~E(f2(f8(f8(a3,a5),a3),f8(a6,a6)),f8(f2(a3,a7),f2(a5,a6)))), % 87.15/87.22 inference(scs_inference,[],[1961,1203,661,20,5,7,6,4,2])). % 87.15/87.22 cnf(1979,plain, % 87.15/87.22 (E(f2(a3,x19791),f2(f8(f8(a3,a5),f8(a5,a5)),x19791))), % 87.15/87.22 inference(scs_inference,[],[1339,502,20,7,4,5,6])). % 87.15/87.22 cnf(1981,plain, % 87.15/87.22 (~E(f2(a3,f8(a6,a6)),f8(f2(a3,a7),f2(a5,a6)))), % 87.15/87.22 inference(scs_inference,[],[1835,1970,1339,851,502,20,7,4,5,6,2,3])). % 87.15/87.22 cnf(1990,plain, % 87.15/87.22 (~E(f2(f8(a3,a3),f8(a6,a6)),f8(f2(a3,a7),f2(a5,a6)))), % 87.15/87.22 inference(scs_inference,[],[1176,497,37,20,4,6,7,5,2])). % 87.15/87.22 cnf(2001,plain, % 87.15/87.22 (E(f2(f8(a6,a7),x20011),f2(f8(a6,a6),x20011))), % 87.15/87.22 inference(scs_inference,[],[1212,444,20,6])). % 87.15/87.22 cnf(2003,plain, % 87.15/87.22 (E(f2(x20031,f8(a6,a7)),f2(x20031,f8(a6,a6)))), % 87.15/87.22 inference(scs_inference,[],[1212,444,20,6,5,7])). % 87.15/87.22 cnf(2005,plain, % 87.15/87.22 (~E(f2(f8(a3,a5),f8(a7,a6)),f2(a3,a6))), % 87.15/87.22 inference(scs_inference,[],[1212,444,285,20,6,5,7,4,2])). % 87.15/87.22 cnf(2006,plain, % 87.15/87.22 (~E(f2(f8(f8(a3,a5),f8(a5,a5)),f8(a6,a6)),f8(f2(a3,a7),f2(a5,a6)))), % 87.15/87.22 inference(scs_inference,[],[1981,1979,1212,444,285,20,6,5,7,4,2,3])). % 87.15/87.22 cnf(2016,plain, % 87.15/87.22 (E(f2(f8(a6,a7),f8(a6,a7)),f2(f8(a6,a6),f8(a6,a6)))), % 87.15/87.22 inference(scs_inference,[],[2001,2003,2006,1269,436,20,5,4,6,7,2,3])). % 87.15/87.22 cnf(2049,plain, % 87.15/87.22 (E(f2(f8(a6,a7),f8(a6,a7)),f8(f2(a6,a6),f2(a6,a6)))), % 87.15/87.22 inference(scs_inference,[],[2016,1001,421,17,20,4,7,5,6,3])). % 87.15/87.22 cnf(2068,plain, % 87.15/87.22 (E(f2(f8(a6,a7),f8(a6,a7)),f2(a6,a6))), % 87.15/87.22 inference(scs_inference,[],[2049,1177,898,15,20,4,7,5,6,3])). % 87.15/87.22 cnf(2098,plain, % 87.15/87.22 (E(f2(x20981,f8(a6,a6)),f2(x20981,f8(a6,a7)))), % 87.15/87.22 inference(scs_inference,[],[1258,441,20,4,7])). % 87.15/87.22 cnf(2121,plain, % 87.15/87.22 (~E(f2(f8(a3,a3),f8(a6,a7)),f8(f2(a3,a7),f2(a5,a6)))), % 87.15/87.22 inference(scs_inference,[],[2098,1990,1334,408,229,20,4,7,5,6,3])). % 87.15/87.22 cnf(2145,plain, % 87.15/87.22 (E(f2(f8(a3,a3),x21451),f2(f8(a3,a5),x21451))), % 87.15/87.22 inference(scs_inference,[],[783,221,20,4,7,6])). % 87.15/87.22 cnf(2153,plain, % 87.15/87.22 (E(f8(f8(x21531,x21531),x21532),f8(x21531,x21532))), % 87.15/87.22 inference(scs_inference,[],[822,15,20,4])). % 87.15/87.22 cnf(2166,plain, % 87.15/87.22 (E(f2(f8(a3,a5),x21661),f2(f8(a3,a3),x21661))), % 87.15/87.22 inference(scs_inference,[],[785,229,495,20,4,7,5,6])). % 87.15/87.22 cnf(2170,plain, % 87.15/87.22 (P2(f8(x21701,x21702),f8(f8(x21701,x21701),x21702))), % 87.15/87.22 inference(scs_inference,[],[14,2153,2145,2121,785,229,495,20,4,7,5,6,3,2,9])). % 87.15/87.22 cnf(2171,plain, % 87.15/87.22 (P2(x21711,x21711)), % 87.15/87.22 inference(rename_variables,[],[14])). % 87.15/87.22 cnf(2172,plain, % 87.15/87.22 (P2(f8(f8(x21721,x21721),x21722),f8(x21721,x21722))), % 87.15/87.22 inference(scs_inference,[],[14,2171,2153,2145,2121,785,229,495,20,4,7,5,6,3,2,9,10])). % 87.15/87.22 cnf(2179,plain, % 87.15/87.22 (E(f2(x21791,f8(x21792,x21793)),f2(x21791,f8(x21793,x21792)))), % 87.15/87.22 inference(scs_inference,[],[2172,16,20,4,5,7])). % 87.15/87.22 cnf(2191,plain, % 87.15/87.22 (~E(f2(f8(a3,a3),f8(a7,a6)),f2(a3,a6))), % 87.15/87.22 inference(scs_inference,[],[2005,2170,2166,495,98,20,4,6,5,7,3])). % 87.15/87.22 cnf(2211,plain, % 87.15/87.22 (~E(f2(f8(a3,a3),f8(a6,a7)),f2(a3,a6))), % 87.15/87.22 inference(scs_inference,[],[2191,2179,795,407,496,21,20,4,5,6,7,3])). % 87.15/87.22 cnf(2214,plain, % 87.15/87.22 (P2(f2(a6,a6),f2(f8(a6,a7),f8(a6,a7)))), % 87.15/87.22 inference(scs_inference,[],[14,2191,2068,2179,795,407,496,21,20,4,5,6,7,3,2,9])). % 87.15/87.22 cnf(2228,plain, % 87.15/87.22 (E(f2(x22281,x22282),f2(x22281,f8(x22282,x22282)))), % 87.15/87.22 inference(scs_inference,[],[2214,21,20,7])). % 87.15/87.22 cnf(2235,plain, % 87.15/87.22 (~E(f2(f8(a3,a3),f8(f8(a6,a7),f8(a6,a7))),f2(a3,a6))), % 87.15/87.22 inference(scs_inference,[],[2211,2228,558,20,3])). % 87.15/87.22 cnf(2319,plain, % 87.15/87.22 ($false), % 87.15/87.22 inference(scs_inference,[],[2235,1942,1435,166,20,3]), % 87.15/87.22 ['proof']). % 87.15/87.22 % SZS output end Proof % 87.15/87.22 % Total time :86.510000s %------------------------------------------------------------------------------