%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SEU133+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 : n028.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:13 EDT 2024 % Result : Theorem 116.36s 116.39s % Output : CNFRefutation 116.36s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.13/0.15 % Problem : SEU133+1 : TPTP v8.2.0. Released v3.3.0. % 0.13/0.15 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.16/0.36 % Computer : n028.cluster.edu % 0.16/0.36 % Model : x86_64 x86_64 % 0.16/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.36 % Memory : 8042.1875MB % 0.16/0.36 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.36 % CPULimit : 300 % 0.16/0.36 % WCLimit : 300 % 0.16/0.36 % DateTime : Fri Jun 21 13:45:39 EDT 2024 % 0.22/0.36 % CPUTime : % 0.53/0.58 start to proof:theBenchmark % 116.36/116.37 %------------------------------------------- % 116.36/116.37 % File :CSE---1.7 % 116.36/116.37 % Problem :theBenchmark % 116.36/116.37 % Transform :cnf % 116.36/116.37 % Format :tptp:raw % 116.36/116.37 % Command :java -jar mcs_scs.jar %d %s % 116.36/116.37 % 116.36/116.37 % Result :Theorem 115.770000s % 116.36/116.37 % Output :CNFRefutation 115.770000s % 116.36/116.37 %------------------------------------------- % 116.36/116.38 %------------------------------------------------------------------------------ % 116.36/116.38 % File : SEU133+1 : TPTP v8.2.0. Released v3.3.0. % 116.36/116.38 % Domain : Set theory % 116.36/116.38 % Problem : MPTP bushy problem t36_xboole_1 % 116.36/116.38 % Version : [Urb07] axioms : Especial. % 116.36/116.38 % English : % 116.36/116.38 % 116.36/116.38 % Refs : [Ban01] Bancerek et al. (2001), On the Characterizations of Co % 116.36/116.38 % : [Urb07] Urban (2006), Email to G. Sutcliffe % 116.36/116.38 % Source : [Urb07] % 116.36/116.38 % Names : bushy-t36_xboole_1 [Urb07] % 116.36/116.38 % 116.36/116.38 % Status : Theorem % 116.36/116.38 % Rating : 0.17 v7.5.0, 0.19 v7.4.0, 0.07 v7.3.0, 0.10 v7.2.0, 0.07 v7.1.0, 0.09 v7.0.0, 0.10 v6.4.0, 0.15 v6.3.0, 0.12 v6.2.0, 0.20 v6.1.0, 0.27 v6.0.0, 0.17 v5.5.0, 0.15 v5.4.0, 0.25 v5.3.0, 0.30 v5.2.0, 0.05 v5.0.0, 0.21 v4.1.0, 0.22 v4.0.0, 0.25 v3.7.0, 0.20 v3.5.0, 0.21 v3.3.0 % 116.36/116.38 % Syntax : Number of formulae : 15 ( 9 unt; 0 def) % 116.36/116.38 % Number of atoms : 25 ( 5 equ) % 116.36/116.38 % Maximal formula atoms : 4 ( 1 avg) % 116.36/116.38 % Number of connectives : 16 ( 6 ~; 0 |; 4 &) % 116.36/116.38 % ( 3 <=>; 3 =>; 0 <=; 0 <~>) % 116.36/116.38 % Maximal formula depth : 9 ( 4 avg) % 116.36/116.38 % Maximal term depth : 2 ( 1 avg) % 116.36/116.38 % Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty) % 116.36/116.38 % Number of functors : 2 ( 2 usr; 1 con; 0-2 aty) % 116.36/116.38 % Number of variables : 22 ( 20 !; 2 ?) % 116.36/116.38 % SPC : FOF_THM_RFO_SEQ % 116.36/116.38 % 116.36/116.38 % Comments : Translated by MPTP 0.2 from the original problem in the Mizar % 116.36/116.38 % library, www.mizar.org % 116.36/116.38 %------------------------------------------------------------------------------ % 116.36/116.38 fof(antisymmetry_r2_hidden,axiom, % 116.36/116.38 ! [A,B] : % 116.36/116.38 ( in(A,B) % 116.36/116.38 => ~ in(B,A) ) ). % 116.36/116.38 % 116.36/116.38 fof(d3_tarski,axiom, % 116.36/116.38 ! [A,B] : % 116.36/116.38 ( subset(A,B) % 116.36/116.38 <=> ! [C] : % 116.36/116.38 ( in(C,A) % 116.36/116.38 => in(C,B) ) ) ). % 116.36/116.38 % 116.36/116.38 fof(d4_xboole_0,axiom, % 116.36/116.38 ! [A,B,C] : % 116.36/116.38 ( C = set_difference(A,B) % 116.36/116.38 <=> ! [D] : % 116.36/116.38 ( in(D,C) % 116.36/116.38 <=> ( in(D,A) % 116.36/116.38 & ~ in(D,B) ) ) ) ). % 116.36/116.38 % 116.36/116.38 fof(dt_k1_xboole_0,axiom, % 116.36/116.38 $true ). % 116.36/116.38 % 116.36/116.38 fof(dt_k4_xboole_0,axiom, % 116.36/116.38 $true ). % 116.36/116.38 % 116.36/116.38 fof(fc1_xboole_0,axiom, % 116.36/116.38 empty(empty_set) ). % 116.36/116.38 % 116.36/116.38 fof(rc1_xboole_0,axiom, % 116.36/116.38 ? [A] : empty(A) ). % 116.36/116.38 % 116.36/116.38 fof(rc2_xboole_0,axiom, % 116.36/116.38 ? [A] : ~ empty(A) ). % 116.36/116.38 % 116.36/116.38 fof(reflexivity_r1_tarski,axiom, % 116.36/116.38 ! [A,B] : subset(A,A) ). % 116.36/116.38 % 116.36/116.38 fof(t36_xboole_1,conjecture, % 116.36/116.38 ! [A,B] : subset(set_difference(A,B),A) ). % 116.36/116.38 % 116.36/116.38 fof(t3_boole,axiom, % 116.36/116.38 ! [A] : set_difference(A,empty_set) = A ). % 116.36/116.38 % 116.36/116.38 fof(t4_boole,axiom, % 116.36/116.38 ! [A] : set_difference(empty_set,A) = empty_set ). % 116.36/116.38 % 116.36/116.38 fof(t6_boole,axiom, % 116.36/116.38 ! [A] : % 116.36/116.38 ( empty(A) % 116.36/116.38 => A = empty_set ) ). % 116.36/116.38 % 116.36/116.38 fof(t7_boole,axiom, % 116.36/116.39 ! [A,B] : % 116.36/116.39 ~ ( in(A,B) % 116.36/116.39 & empty(B) ) ). % 116.36/116.39 % 116.36/116.39 fof(t8_boole,axiom, % 116.36/116.39 ! [A,B] : % 116.36/116.39 ~ ( empty(A) % 116.36/116.39 & A != B % 116.36/116.39 & empty(B) ) ). % 116.36/116.39 % 116.36/116.39 %------------------------------------------------------------------------------ % 116.36/116.39 %------------------------------------------- % 116.36/116.39 % Proof found % 116.36/116.39 % SZS status Theorem for theBenchmark % 116.36/116.39 % SZS output start Proof % 116.36/116.39 %ClaNum:35(EqnAxiom:15) % 116.36/116.39 %VarNum:94(SingletonVarNum:38) % 116.36/116.39 %MaxLitNum:4 % 116.36/116.39 %MaxfuncDepth:1 % 116.36/116.39 %SharedTerms:10 % 116.36/116.39 %goalClause: 22 % 116.36/116.39 %singleGoalClaCount:1 % 116.36/116.39 [16]P1(a1) % 116.36/116.39 [17]P1(a2) % 116.36/116.39 [21]~P1(a6) % 116.36/116.39 [22]~P2(f5(a7,a8),a7) % 116.36/116.39 [20]P2(x201,x201) % 116.36/116.39 [18]E(f5(a1,x181),a1) % 116.36/116.39 [19]E(f5(x191,a1),x191) % 116.36/116.39 [23]~P1(x231)+E(x231,a1) % 116.36/116.39 [25]~P1(x251)+~P3(x252,x251) % 116.36/116.39 [26]~P3(x262,x261)+~P3(x261,x262) % 116.36/116.39 [27]P2(x271,x272)+P3(f3(x271,x272),x271) % 116.36/116.39 [32]P2(x321,x322)+~P3(f3(x321,x322),x322) % 116.36/116.39 [24]~P1(x242)+~P1(x241)+E(x241,x242) % 116.36/116.39 [28]~P2(x283,x282)+P3(x281,x282)+~P3(x281,x283) % 116.36/116.39 [33]P3(f4(x332,x333,x331),x331)+P3(f4(x332,x333,x331),x332)+E(x331,f5(x332,x333)) % 116.36/116.39 [34]P3(f4(x342,x343,x341),x341)+~P3(f4(x342,x343,x341),x343)+E(x341,f5(x342,x343)) % 116.36/116.39 [29]~P3(x291,x293)+P3(x291,x292)+~E(x293,f5(x292,x294)) % 116.36/116.39 [30]~P3(x304,x303)+~P3(x304,x301)+~E(x301,f5(x302,x303)) % 116.36/116.39 [35]P3(f4(x352,x353,x351),x353)+~P3(f4(x352,x353,x351),x351)+~P3(f4(x352,x353,x351),x352)+E(x351,f5(x352,x353)) % 116.36/116.39 [31]~P3(x311,x314)+P3(x311,x312)+P3(x311,x313)+~E(x312,f5(x314,x313)) % 116.36/116.39 %EqnAxiom % 116.36/116.39 [1]E(x11,x11) % 116.36/116.39 [2]E(x22,x21)+~E(x21,x22) % 116.36/116.39 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 116.36/116.39 [4]~E(x41,x42)+E(f5(x41,x43),f5(x42,x43)) % 116.36/116.39 [5]~E(x51,x52)+E(f5(x53,x51),f5(x53,x52)) % 116.36/116.39 [6]~E(x61,x62)+E(f4(x61,x63,x64),f4(x62,x63,x64)) % 116.36/116.39 [7]~E(x71,x72)+E(f4(x73,x71,x74),f4(x73,x72,x74)) % 116.36/116.39 [8]~E(x81,x82)+E(f4(x83,x84,x81),f4(x83,x84,x82)) % 116.36/116.39 [9]~E(x91,x92)+E(f3(x91,x93),f3(x92,x93)) % 116.36/116.39 [10]~E(x101,x102)+E(f3(x103,x101),f3(x103,x102)) % 116.36/116.39 [11]~P1(x111)+P1(x112)+~E(x111,x112) % 116.36/116.39 [12]P3(x122,x123)+~E(x121,x122)+~P3(x121,x123) % 116.36/116.39 [13]P3(x133,x132)+~E(x131,x132)+~P3(x133,x131) % 116.36/116.39 [14]P2(x142,x143)+~E(x141,x142)+~P2(x141,x143) % 116.36/116.39 [15]P2(x153,x152)+~E(x151,x152)+~P2(x153,x151) % 116.36/116.39 % 116.36/116.39 %------------------------------------------- % 116.36/116.40 cnf(36,plain, % 116.36/116.40 (~P3(x361,f5(x362,x363))+P3(x361,x362)), % 116.36/116.40 inference(equality_inference,[],[29])). % 116.36/116.40 cnf(37,plain, % 116.36/116.40 (~P3(x371,x372)+~P3(x371,f5(x373,x372))), % 116.36/116.40 inference(equality_inference,[],[30])). % 116.36/116.40 cnf(38,plain, % 116.36/116.40 (~P3(x381,x382)+P3(x381,f5(x382,x383))+P3(x381,x383)), % 116.36/116.40 inference(equality_inference,[],[31])). % 116.36/116.40 cnf(39,plain, % 116.36/116.40 (~P3(x391,a1)), % 116.36/116.41 inference(scs_inference,[],[16,25])). % 116.36/116.41 cnf(41,plain, % 116.36/116.41 (~P3(x411,f5(a1,x412))), % 116.36/116.41 inference(scs_inference,[],[16,25,36])). % 116.36/116.41 cnf(43,plain, % 116.36/116.41 (E(x431,f5(x431,a1))), % 116.36/116.41 inference(scs_inference,[],[19,16,25,36,2])). % 116.36/116.41 cnf(45,plain, % 116.36/116.41 (P2(x451,x451)), % 116.36/116.41 inference(rename_variables,[],[20])). % 116.36/116.41 cnf(49,plain, % 116.36/116.41 (E(f5(x491,a1),x491)), % 116.36/116.41 inference(rename_variables,[],[19])). % 116.36/116.41 cnf(51,plain, % 116.36/116.41 (P3(f4(a7,a8,a7),a7)), % 116.36/116.41 inference(scs_inference,[],[22,20,45,19,16,25,36,2,14,15,29,33])). % 116.36/116.41 cnf(53,plain, % 116.36/116.41 (P3(f4(a7,a8,a7),f5(a7,a1))), % 116.36/116.41 inference(scs_inference,[],[22,20,45,19,16,25,36,2,14,15,29,33,38])). % 116.36/116.41 cnf(56,plain, % 116.36/116.41 (E(f5(x561,a1),x561)), % 116.36/116.41 inference(rename_variables,[],[19])). % 116.36/116.41 cnf(57,plain, % 116.36/116.41 (~E(a7,a1)), % 116.36/116.41 inference(scs_inference,[],[22,20,45,19,49,16,25,36,2,14,15,29,33,38,3,13])). % 116.36/116.41 cnf(59,plain, % 116.36/116.41 (E(f5(x591,a1),x591)), % 116.36/116.41 inference(rename_variables,[],[19])). % 116.36/116.41 cnf(60,plain, % 116.36/116.41 (P3(f4(a7,a8,a7),f5(f5(a7,a1),a1))), % 116.36/116.41 inference(scs_inference,[],[22,20,45,19,49,56,59,16,21,25,36,2,14,15,29,33,38,3,13,11,31])). % 116.36/116.41 cnf(63,plain, % 116.36/116.41 (P3(f4(a7,a8,a7),a8)), % 116.36/116.41 inference(scs_inference,[],[22,20,45,19,49,56,59,16,21,25,36,2,14,15,29,33,38,3,13,11,31,35])). % 116.36/116.41 cnf(67,plain, % 116.36/116.41 (~P3(a7,f4(a7,a8,a7))), % 116.36/116.41 inference(scs_inference,[],[22,20,45,19,49,56,59,16,21,25,36,2,14,15,29,33,38,3,13,11,31,35,23,26])). % 116.36/116.41 cnf(69,plain, % 116.36/116.41 (~P3(f4(a7,a8,a7),f5(x691,a7))), % 116.36/116.41 inference(scs_inference,[],[22,20,45,19,49,56,59,16,21,25,36,2,14,15,29,33,38,3,13,11,31,35,23,26,37])). % 116.36/116.41 cnf(79,plain, % 116.36/116.41 (~P3(x791,f5(a1,x792))), % 116.36/116.41 inference(rename_variables,[],[41])). % 116.36/116.41 cnf(81,plain, % 116.36/116.41 (~P3(x811,f5(f5(a1,x812),x813))), % 116.36/116.41 inference(scs_inference,[],[41,79,27,36])). % 116.36/116.41 cnf(83,plain, % 116.36/116.41 (~P3(f4(a7,a8,a7),f5(x831,f5(a7,a1)))), % 116.36/116.41 inference(scs_inference,[],[41,79,53,27,36,37])). % 116.36/116.41 cnf(87,plain, % 116.36/116.41 (~P3(x871,a2)), % 116.36/116.41 inference(scs_inference,[],[41,79,60,53,17,27,36,37,26,25])). % 116.36/116.41 cnf(89,plain, % 116.36/116.41 (E(a1,f5(a1,x891))), % 116.36/116.41 inference(scs_inference,[],[41,79,60,53,18,17,27,36,37,26,25,2])). % 116.36/116.41 cnf(90,plain, % 116.36/116.41 (P3(f4(a7,a8,a7),f5(a7,f5(a1,x901)))), % 116.36/116.41 inference(scs_inference,[],[51,41,79,60,53,18,17,27,36,37,26,25,2,38])). % 116.36/116.41 cnf(91,plain, % 116.36/116.41 (~P3(x911,f5(a1,x912))), % 116.36/116.41 inference(rename_variables,[],[41])). % 116.36/116.41 cnf(93,plain, % 116.36/116.41 (~E(f5(a1,x931),f5(a7,a8))), % 116.36/116.41 inference(scs_inference,[],[22,51,41,79,60,53,18,17,27,36,37,26,25,2,38,14])). % 116.36/116.41 cnf(94,plain, % 116.36/116.41 (~E(a7,f5(a1,x941))), % 116.36/116.41 inference(scs_inference,[],[22,51,41,79,60,53,57,18,17,27,36,37,26,25,2,38,14,3])). % 116.36/116.41 cnf(95,plain, % 116.36/116.41 (~E(f5(f5(a7,a1),a1),f5(a1,x951))), % 116.36/116.41 inference(scs_inference,[],[22,51,41,79,91,60,53,57,18,17,27,36,37,26,25,2,38,14,3,13])). % 116.36/116.41 cnf(97,plain, % 116.36/116.41 (P3(f5(f4(a7,a8,a7),a1),a7)), % 116.36/116.41 inference(scs_inference,[],[22,51,43,41,79,91,60,53,57,18,17,27,36,37,26,25,2,38,14,3,13,12])). % 116.36/116.41 cnf(98,plain, % 116.36/116.41 (E(x981,f5(x981,a1))), % 116.36/116.41 inference(rename_variables,[],[43])). % 116.36/116.41 cnf(99,plain, % 116.36/116.41 (P1(f5(a1,a1))), % 116.36/116.41 inference(scs_inference,[],[22,51,43,98,41,79,91,60,53,57,18,16,17,27,36,37,26,25,2,38,14,3,13,12,11])). % 116.36/116.41 cnf(118,plain, % 116.36/116.41 (~P3(a8,f4(a7,a8,a7))), % 116.36/116.41 inference(scs_inference,[],[69,63,87,36,27,26])). % 116.36/116.41 cnf(120,plain, % 116.36/116.41 (~P3(f4(a7,a8,a7),f5(x1201,a8))), % 116.36/116.41 inference(scs_inference,[],[69,63,87,36,27,26,37])). % 116.36/116.41 cnf(123,plain, % 116.36/116.41 (~E(f5(f5(a7,a1),a1),f5(a1,x1231))), % 116.36/116.41 inference(rename_variables,[],[95])). % 116.36/116.41 cnf(128,plain, % 116.36/116.41 (~E(f5(a1,x1281),f5(a7,a8))), % 116.36/116.41 inference(rename_variables,[],[93])). % 116.36/116.41 cnf(130,plain, % 116.36/116.41 (P3(f4(a7,a8,f5(a1,x1301)),a7)), % 116.36/116.41 inference(scs_inference,[],[93,128,19,69,63,95,87,41,99,36,27,26,37,4,30,24,33])). % 116.36/116.41 cnf(131,plain, % 116.36/116.41 (~E(f5(a1,x1311),f5(a7,a8))), % 116.36/116.41 inference(rename_variables,[],[93])). % 116.36/116.41 cnf(132,plain, % 116.36/116.41 (~P3(x1321,f5(a1,x1322))), % 116.36/116.41 inference(rename_variables,[],[41])). % 116.36/116.41 cnf(134,plain, % 116.36/116.41 (~P3(f4(a7,a8,f5(a1,x1341)),a8)), % 116.36/116.41 inference(scs_inference,[],[93,128,131,19,69,63,95,87,41,132,99,36,27,26,37,4,30,24,33,34])). % 116.36/116.41 cnf(138,plain, % 116.36/116.41 (P3(f4(a7,a8,a7),f5(a8,f5(x1381,a7)))), % 116.36/116.41 inference(scs_inference,[],[93,128,131,19,69,63,95,87,41,132,99,36,27,26,37,4,30,24,33,34,38])). % 116.36/116.41 cnf(140,plain, % 116.36/116.41 (~E(a2,f5(a7,a8))), % 116.36/116.41 inference(scs_inference,[],[22,93,128,131,19,69,63,95,87,41,132,99,36,27,26,37,4,30,24,33,34,38,14])). % 116.36/116.41 cnf(142,plain, % 116.36/116.41 (E(a1,f5(a1,x1421))), % 116.36/116.41 inference(rename_variables,[],[89])). % 116.36/116.41 cnf(143,plain, % 116.36/116.41 (~E(a8,f5(f5(a1,x1431),x1432))), % 116.36/116.41 inference(scs_inference,[],[22,93,128,131,19,81,69,63,95,123,87,89,41,132,99,36,27,26,37,4,30,24,33,34,38,14,3,13])). % 116.36/116.41 cnf(145,plain, % 116.36/116.41 (P1(f5(a1,x1451))), % 116.36/116.41 inference(scs_inference,[],[22,93,128,131,19,81,69,63,95,123,87,89,142,41,132,16,99,36,27,26,37,4,30,24,33,34,38,14,3,13,11])). % 116.36/116.41 cnf(158,plain, % 116.36/116.41 (~P3(f5(f4(a7,a8,a7),a1),f5(x1581,a7))), % 116.36/116.41 inference(scs_inference,[],[120,97,39,27,36,37])). % 116.36/116.41 cnf(162,plain, % 116.36/116.41 (P3(f4(a7,a8,a2),a7)), % 116.36/116.41 inference(scs_inference,[],[140,120,138,97,87,39,27,36,37,26,33])). % 116.36/116.41 cnf(163,plain, % 116.36/116.41 (~P3(x1631,a2)), % 116.36/116.41 inference(rename_variables,[],[87])). % 116.36/116.41 cnf(165,plain, % 116.36/116.41 (~P3(f4(a7,a8,a2),a8)), % 116.36/116.41 inference(scs_inference,[],[140,120,138,97,87,163,39,27,36,37,26,33,34])). % 116.36/116.41 cnf(168,plain, % 116.36/116.41 (P3(f4(a7,a8,f5(a1,x1681)),f5(a7,a8))), % 116.36/116.41 inference(scs_inference,[],[140,120,138,97,130,134,87,163,39,27,36,37,26,33,34,38])). % 116.36/116.41 cnf(171,plain, % 116.36/116.41 (~E(a1,f5(a7,a8))), % 116.36/116.41 inference(scs_inference,[],[22,140,120,138,97,130,134,87,163,39,27,36,37,26,33,34,38,14])). % 116.36/116.41 cnf(172,plain, % 116.36/116.41 (P3(f5(f4(a7,a8,a7),a1),f5(a7,a1))), % 116.36/116.41 inference(scs_inference,[],[22,140,43,120,138,97,130,134,53,87,163,39,27,36,37,26,33,34,38,14,12])). % 116.36/116.41 cnf(173,plain, % 116.36/116.41 (E(x1731,f5(x1731,a1))), % 116.36/116.41 inference(rename_variables,[],[43])). % 116.36/116.41 cnf(174,plain, % 116.36/116.41 (~E(a7,f5(f5(a1,x1741),x1742))), % 116.36/116.41 inference(scs_inference,[],[22,140,43,120,138,97,130,134,81,53,87,163,39,27,36,37,26,33,34,38,14,12,13])). % 116.36/116.41 cnf(176,plain, % 116.36/116.41 (~E(a8,f5(a1,x1761))), % 116.36/116.41 inference(scs_inference,[],[22,140,43,173,120,138,143,97,130,134,81,53,87,163,39,27,36,37,26,33,34,38,14,12,13,3])). % 116.36/116.41 cnf(185,plain, % 116.36/116.41 (~P3(f4(a7,a8,a2),f5(x1851,a7))), % 116.36/116.41 inference(scs_inference,[],[172,67,162,36,26,37])). % 116.36/116.41 cnf(187,plain, % 116.36/116.41 (~P3(f4(a7,a8,a1),a8)), % 116.36/116.41 inference(scs_inference,[],[171,172,67,162,39,36,26,37,34])). % 116.36/116.41 cnf(188,plain, % 116.36/116.41 (~P3(x1881,a1)), % 116.36/116.41 inference(rename_variables,[],[39])). % 116.36/116.41 cnf(193,plain, % 116.36/116.41 (P3(f4(a7,a8,a1),a7)), % 116.36/116.41 inference(scs_inference,[],[171,172,67,176,162,39,188,145,36,26,37,34,24,33])). % 116.36/116.41 cnf(196,plain, % 116.36/116.41 (P3(f4(a7,a8,a2),f5(a7,a8))), % 116.36/116.41 inference(scs_inference,[],[171,172,67,165,176,162,39,188,145,36,26,37,34,24,33,38])). % 116.36/116.41 cnf(200,plain, % 116.36/116.41 (~E(f5(a7,a1),f5(x2001,a7))), % 116.36/116.41 inference(scs_inference,[],[171,172,158,67,168,165,176,162,120,39,188,145,36,26,37,34,24,33,38,12,13])). % 116.36/116.41 cnf(206,plain, % 116.36/116.41 (~P3(f5(a7,a8),f4(a7,a8,a2))), % 116.36/116.41 inference(scs_inference,[],[196,185,36,26])). % 116.36/116.41 cnf(210,plain, % 116.36/116.41 (P3(f4(f5(a1,x2101),x2102,a7),a7)), % 116.36/116.41 inference(scs_inference,[],[196,185,174,41,36,26,37,33])). % 116.36/116.41 cnf(214,plain, % 116.36/116.41 (P3(f4(a7,a8,a2),f5(f5(a7,a8),f5(x2141,a7)))), % 116.36/116.41 inference(scs_inference,[],[196,185,174,41,36,26,37,33,38])). % 116.36/116.41 cnf(218,plain, % 116.36/116.41 (~E(f5(a7,a8),f5(x2181,a7))), % 116.36/116.41 inference(scs_inference,[],[196,185,174,41,120,36,26,37,33,38,12,13])). % 116.36/116.41 cnf(227,plain, % 116.36/116.41 (~P3(x2271,f5(a2,x2272))), % 116.36/116.41 inference(scs_inference,[],[87,36])). % 116.36/116.41 cnf(231,plain, % 116.36/116.41 (~P3(f4(a7,a8,a1),f5(x2311,a7))), % 116.36/116.41 inference(scs_inference,[],[87,214,193,36,26,37])). % 116.36/116.41 cnf(233,plain, % 116.36/116.41 (P3(f4(a1,x2331,a7),a7)), % 116.36/116.41 inference(scs_inference,[],[94,87,39,214,193,36,26,37,33])). % 116.36/116.41 cnf(236,plain, % 116.36/116.41 (P3(f4(a7,a8,a1),f5(a7,a8))), % 116.36/116.41 inference(scs_inference,[],[94,87,39,214,187,193,36,26,37,33,38])). % 116.36/116.41 cnf(238,plain, % 116.36/116.41 (~E(f5(a1,x2381),f5(f5(a7,a8),a1))), % 116.36/116.41 inference(scs_inference,[],[93,19,94,87,39,214,187,193,36,26,37,33,38,3])). % 116.36/116.41 cnf(240,plain, % 116.36/116.41 (P3(f5(f4(a7,a8,a1),a1),a7)), % 116.36/116.41 inference(scs_inference,[],[93,19,43,94,87,39,214,187,193,36,26,37,33,38,3,12])). % 116.36/116.41 cnf(242,plain, % 116.36/116.41 (~E(f5(f5(a7,a8),f5(x2421,a7)),a2)), % 116.36/116.41 inference(scs_inference,[],[93,19,43,94,87,39,214,187,193,36,26,37,33,38,3,12,13])). % 116.36/116.41 cnf(253,plain, % 116.36/116.41 (~P3(x2531,f5(a2,x2532))), % 116.36/116.41 inference(rename_variables,[],[227])). % 116.36/116.41 cnf(257,plain, % 116.36/116.41 (~P3(f5(a7,a8),f4(a7,a8,a1))), % 116.36/116.41 inference(scs_inference,[],[236,227,253,27,36,26])). % 116.36/116.41 cnf(261,plain, % 116.36/116.41 (P3(f4(f5(a1,x2611),a7,f5(a7,a1)),f5(a7,a1))), % 116.36/116.41 inference(scs_inference,[],[200,41,236,227,253,27,36,26,37,33])). % 116.36/116.41 cnf(263,plain, % 116.36/116.41 (~P3(x2631,f5(a1,x2632))), % 116.36/116.41 inference(rename_variables,[],[41])). % 116.36/116.41 cnf(265,plain, % 116.36/116.41 (~E(f5(a2,x2651),f5(a7,a8))), % 116.36/116.41 inference(scs_inference,[],[22,200,41,236,227,253,27,36,26,37,33,14])). % 116.36/116.41 cnf(268,plain, % 116.36/116.41 (P3(f4(a7,a8,a1),f5(f5(a7,a8),f5(a1,x2681)))), % 116.36/116.41 inference(scs_inference,[],[22,200,41,263,236,227,253,242,17,27,36,26,37,33,14,24,38])). % 116.36/116.41 cnf(269,plain, % 116.36/116.41 (~P3(x2691,f5(a1,x2692))), % 116.36/116.41 inference(rename_variables,[],[41])). % 116.36/116.41 cnf(273,plain, % 116.36/116.41 (~E(f5(a7,a8),f5(a1,x2731))), % 116.36/116.41 inference(scs_inference,[],[22,200,41,263,269,236,227,253,242,120,17,27,36,26,37,33,14,24,38,12,13])). % 116.36/116.41 cnf(287,plain, % 116.36/116.41 (P3(f4(a7,a8,f5(a2,x2871)),a7)), % 116.36/116.41 inference(scs_inference,[],[265,257,268,210,227,36,26,37,33])). % 116.36/116.41 cnf(288,plain, % 116.36/116.41 (~E(f5(a2,x2881),f5(a7,a8))), % 116.36/116.41 inference(rename_variables,[],[265])). % 116.36/116.41 cnf(289,plain, % 116.36/116.41 (~P3(x2891,f5(a2,x2892))), % 116.36/116.41 inference(rename_variables,[],[227])). % 116.36/116.41 cnf(291,plain, % 116.36/116.41 (~P3(f4(a7,a8,f5(a2,x2911)),a8)), % 116.36/116.41 inference(scs_inference,[],[265,288,257,268,210,227,289,36,26,37,33,34])). % 116.36/116.41 cnf(297,plain, % 116.36/116.41 (P3(f5(f4(a1,x2971,a7),a1),a7)), % 116.36/116.41 inference(scs_inference,[],[265,288,43,257,268,210,233,227,289,162,185,36,26,37,33,34,38,12])). % 116.36/116.41 cnf(299,plain, % 116.36/116.41 (~E(f5(f5(a7,a8),f5(a1,x2991)),f5(a1,x2992))), % 116.36/116.41 inference(scs_inference,[],[265,288,43,41,257,268,210,233,227,289,162,185,36,26,37,33,34,38,12,13])). % 116.36/116.41 cnf(311,plain, % 116.36/116.41 (P3(f4(a2,a7,f5(a7,a1)),f5(a7,a1))), % 116.36/116.41 inference(scs_inference,[],[200,87,261,231,240,36,26,37,33])). % 116.36/116.41 cnf(321,plain, % 116.36/116.41 (P3(f5(f4(a7,a8,a2),a1),a7)), % 116.36/116.41 inference(scs_inference,[],[43,200,87,261,231,299,240,287,291,162,145,36,26,37,33,38,24,12])). % 116.36/116.41 cnf(337,plain, % 116.36/116.41 (P3(f4(a1,a7,f5(a7,a8)),f5(a7,a8))), % 116.36/116.41 inference(scs_inference,[],[218,39,206,90,321,36,26,37,33])). % 116.36/116.41 cnf(361,plain, % 116.36/116.41 (P3(f4(f5(a7,a8),a1,f5(a1,x3611)),f5(a7,a8))), % 116.36/116.41 inference(scs_inference,[],[238,41,118,337,297,26,36,37,33])). % 116.36/116.41 cnf(371,plain, % 116.36/116.41 (~P3(f4(a7,a8,a2),f5(a8,x3711))), % 116.36/116.41 inference(scs_inference,[],[165,36])). % 116.36/116.41 cnf(375,plain, % 116.36/116.41 (~P3(f4(a1,x3751,a7),f5(x3752,a7))), % 116.36/116.41 inference(scs_inference,[],[361,165,233,36,26,37])). % 116.36/116.41 cnf(396,plain, % 116.36/116.41 (P3(f4(a1,a7,f5(a7,a1)),f5(a7,a1))), % 116.36/116.41 inference(scs_inference,[],[200,39,311,371,130,26,36,37,33])). % 116.36/116.41 cnf(412,plain, % 116.36/116.41 (P3(f4(a1,x4121,f5(a7,a8)),f5(a7,a8))), % 116.36/116.41 inference(scs_inference,[],[273,39,396,375,287,36,26,37,33])). % 116.36/116.41 cnf(417,plain, % 116.36/116.41 (~E(f5(a8,f5(x4171,a7)),a2)), % 116.36/116.41 inference(scs_inference,[],[273,87,39,396,375,371,138,287,36,26,37,33,12,13])). % 116.36/116.41 cnf(424,plain, % 116.36/116.41 (~P3(f4(a7,a8,a1),f5(a8,x4241))), % 116.36/116.41 inference(scs_inference,[],[412,187,26,36])). % 116.36/116.41 cnf(426,plain, % 116.36/116.41 (P3(f4(a7,a8,a7),f5(a7,f5(x4261,a7)))), % 116.36/116.41 inference(scs_inference,[],[412,187,51,69,26,36,38])). % 116.36/116.41 cnf(428,plain, % 116.36/116.41 (P3(f4(f5(a1,x4281),x4282,a8),a8)), % 116.36/116.41 inference(scs_inference,[],[143,41,412,187,51,69,26,36,38,33])). % 116.36/116.41 cnf(434,plain, % 116.36/116.41 (~E(f5(a7,a8),f5(a2,x4341))), % 116.36/116.41 inference(scs_inference,[],[143,227,41,412,417,187,51,69,17,26,36,38,33,24,13])). % 116.36/116.41 cnf(443,plain, % 116.36/116.41 (E(f3(f5(a1,x4431),x4432),f3(a1,x4432))), % 116.36/116.41 inference(scs_inference,[],[89,9,2])). % 116.36/116.41 cnf(449,plain, % 116.36/116.41 (P3(f4(a1,x4491,a8),a8)), % 116.36/116.41 inference(scs_inference,[],[176,39,424,443,426,2,36,26,33])). % 116.36/116.41 cnf(456,plain, % 116.36/116.41 (~P3(f4(a1,x4561,a8),f5(x4562,a8))), % 116.36/116.41 inference(scs_inference,[],[176,87,39,424,443,426,138,2,36,26,33,13,12,37])). % 116.36/116.41 cnf(459,plain, % 116.36/116.41 (P3(f4(a1,x4591,a8),f5(a8,f5(x4592,a8)))), % 116.36/116.41 inference(scs_inference,[],[176,87,39,424,443,426,138,2,36,26,33,13,12,37,11,38])). % 116.36/116.41 cnf(467,plain, % 116.36/116.41 (P3(f4(a7,a8,a7),f5(f5(a7,a1),f5(x4671,a7)))), % 116.36/116.41 inference(scs_inference,[],[456,459,53,69,36,26,38])). % 116.36/116.41 cnf(488,plain, % 116.36/116.41 (P3(f4(f5(a1,x4881),x4882,a8),f5(a8,a2))), % 116.36/116.41 inference(scs_inference,[],[87,428,134,36,26,38])). % 116.36/116.41 cnf(491,plain, % 116.36/116.41 (P3(f4(f5(a1,x4911),a7,f5(a7,a8)),f5(a7,a8))), % 116.36/116.41 inference(scs_inference,[],[218,41,87,428,134,36,26,38,33])). % 116.36/116.41 cnf(493,plain, % 116.36/116.41 (~P3(x4931,f5(a1,x4932))), % 116.36/116.41 inference(rename_variables,[],[41])). % 116.36/116.41 cnf(496,plain, % 116.36/116.41 (~E(f5(a7,a1),f5(a1,x4961))), % 116.36/116.41 inference(scs_inference,[],[218,41,493,87,428,449,53,134,36,26,38,33,12,13])). % 116.36/116.41 cnf(506,plain, % 116.36/116.41 (P3(f5(f4(a7,a8,a1),a1),f5(a7,a2))), % 116.36/116.41 inference(scs_inference,[],[87,240,291,36,26,38])). % 116.36/116.41 cnf(511,plain, % 116.36/116.41 (~P3(x5111,f5(a2,x5112))), % 116.36/116.41 inference(rename_variables,[],[227])). % 116.36/116.41 cnf(513,plain, % 116.36/116.41 (~E(a7,f5(a2,x5131))), % 116.36/116.41 inference(scs_inference,[],[218,227,511,87,240,291,36,26,38,33,13])). % 116.36/116.41 cnf(531,plain, % 116.36/116.41 (~E(f5(f5(a7,a1),f5(x5311,a7)),f5(a1,x5312))), % 116.36/116.41 inference(scs_inference,[],[434,41,39,87,321,428,467,165,26,38,33,12,13])). % 116.36/116.41 cnf(538,plain, % 116.36/116.41 (~P3(x5381,a1)), % 116.36/116.41 inference(rename_variables,[],[39])). % 116.36/116.41 cnf(547,plain, % 116.36/116.41 (~E(a8,f5(a2,x5471))), % 116.36/116.41 inference(scs_inference,[],[227,496,39,538,210,449,428,187,531,145,26,38,33,24,12,13])). % 116.36/116.41 cnf(559,plain, % 116.36/116.41 (~P3(x5591,a2)), % 116.36/116.41 inference(rename_variables,[],[87])). % 116.36/116.41 cnf(561,plain, % 116.36/116.41 (P3(f4(a2,x5611,a7),a7)), % 116.36/116.41 inference(scs_inference,[],[87,559,297,513,26,38,33])). % 116.36/116.41 cnf(567,plain, % 116.36/116.41 (~P3(f4(a2,x5671,a7),f5(x5672,a7))), % 116.36/116.41 inference(scs_inference,[],[41,87,559,297,449,513,165,506,26,38,33,12,13,37])). % 116.36/116.41 cnf(583,plain, % 116.36/116.41 (~P3(x5831,a2)), % 116.36/116.41 inference(rename_variables,[],[87])). % 116.36/116.41 cnf(585,plain, % 116.36/116.41 (P3(f4(a2,x5851,a8),a8)), % 116.36/116.41 inference(scs_inference,[],[87,583,97,130,547,567,26,36,38,33])). % 116.36/116.41 cnf(695,plain, % 116.36/116.41 (~P3(a7,f4(a2,x6951,a7))), % 116.36/116.41 inference(scs_inference,[],[561,26])). % 116.36/116.41 cnf(824,plain, % 116.36/116.41 (P3(f4(f5(a1,x8241),x8242,a8),f5(a8,a1))), % 116.36/116.41 inference(scs_inference,[],[39,428,488,26,38])). % 116.36/116.41 cnf(850,plain, % 116.36/116.41 (P3(f4(a7,a8,a7),f5(a7,a2))), % 116.36/116.41 inference(scs_inference,[],[87,51,491,26,38])). % 116.36/116.41 cnf(970,plain, % 116.36/116.41 (~E(f5(a8,a1),a2)), % 116.36/116.41 inference(scs_inference,[],[87,824,13])). % 116.36/116.41 cnf(1298,plain, % 116.36/116.41 (~E(a1,f5(a7,a1))), % 116.36/116.41 inference(scs_inference,[],[83,227,162,53,38,13,5])). % 116.36/116.41 cnf(1316,plain, % 116.36/116.41 (P3(f4(a7,a8,a1),f5(a7,f5(a2,x13161)))), % 116.36/116.41 inference(scs_inference,[],[39,227,193,1298,33,38])). % 116.36/116.41 cnf(1319,plain, % 116.36/116.41 (P3(f5(f4(a7,a1,a1),a1),a7)), % 116.36/116.41 inference(scs_inference,[],[43,39,227,193,1298,33,38,12])). % 116.36/116.41 cnf(1324,plain, % 116.36/116.41 (~P3(a7,f4(a7,a1,a1))), % 116.36/116.41 inference(scs_inference,[],[83,43,39,227,193,63,1298,33,38,12,13,37,26])). % 116.36/116.41 cnf(1342,plain, % 116.36/116.41 (~E(a2,f5(a7,a1))), % 116.36/116.41 inference(scs_inference,[],[83,87,236,850,1316,1319,1324,36,37,26,38,13,5])). % 116.36/116.41 cnf(1949,plain, % 116.36/116.41 (~P3(f5(a7,a1),f4(a2,x19491,a7))), % 116.36/116.41 inference(scs_inference,[],[970,695,17,19,2,23,12])). % 116.36/116.41 cnf(1950,plain, % 116.36/116.41 (E(f5(x19501,a1),x19501)), % 116.36/116.41 inference(rename_variables,[],[19])). % 116.36/116.41 cnf(1951,plain, % 116.36/116.41 (~E(a8,f5(x19511,a8))), % 116.36/116.41 inference(scs_inference,[],[970,695,585,17,19,2,23,12,30])). % 116.36/116.41 cnf(1953,plain, % 116.36/116.41 (~P2(f5(a7,a8),f5(a7,a1))), % 116.36/116.42 inference(scs_inference,[],[22,970,695,585,17,19,1950,2,23,12,30,15])). % 116.36/116.42 cnf(1963,plain, % 116.36/116.42 (E(f5(x19631,a2),f5(x19631,a1))), % 116.36/116.42 inference(scs_inference,[],[22,970,1342,695,585,17,43,19,1950,2,23,12,30,15,3,9,10,6,7,8,4,5])). % 116.36/116.42 cnf(1999,plain, % 116.36/116.42 (E(f5(x19991,a2),f5(x19991,a1))), % 116.36/116.42 inference(rename_variables,[],[1963])). % 116.36/116.42 cnf(2000,plain, % 116.36/116.42 (~P2(f5(a7,a8),f5(a7,a2))), % 116.36/116.42 inference(scs_inference,[],[1953,1949,1963,1999,1951,227,39,2,33,12,15])). % 116.36/116.42 cnf(2736,plain, % 116.36/116.42 (P3(f3(f5(a7,a8),f5(a7,a2)),a7)), % 116.36/116.42 inference(scs_inference,[],[2000,27,36])). % 116.36/116.42 cnf(2827,plain, % 116.36/116.42 (~P3(f3(f5(a7,a8),f5(a7,a2)),a7)), % 116.36/116.42 inference(scs_inference,[],[2000,87,32,38])). % 116.36/116.42 cnf(2849,plain, % 116.36/116.42 ($false), % 116.36/116.42 inference(scs_inference,[],[2736,2827]), % 116.36/116.42 ['proof']). % 116.36/116.42 % SZS output end Proof % 116.36/116.42 % Total time :115.770000s %------------------------------------------------------------------------------