%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SEU146+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 : n020.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:18 EDT 2024 % Result : Theorem 5.57s 5.71s % Output : CNFRefutation 5.57s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SEU146+1 : TPTP v8.2.0. Released v3.3.0. % 0.07/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n020.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Fri Jun 21 11:23:54 EDT 2024 % 0.12/0.34 % CPUTime : % 0.20/0.57 start to proof:theBenchmark % 5.57/5.70 %------------------------------------------- % 5.57/5.70 % File :CSE---1.7 % 5.57/5.70 % Problem :theBenchmark % 5.57/5.70 % Transform :cnf % 5.57/5.70 % Format :tptp:raw % 5.57/5.70 % Command :java -jar mcs_scs.jar %d %s % 5.57/5.70 % 5.57/5.70 % Result :Theorem 5.090000s % 5.57/5.70 % Output :CNFRefutation 5.090000s % 5.57/5.70 %------------------------------------------- % 5.57/5.70 %------------------------------------------------------------------------------ % 5.57/5.70 % File : SEU146+1 : TPTP v8.2.0. Released v3.3.0. % 5.57/5.70 % Domain : Set theory % 5.57/5.70 % Problem : MPTP bushy problem l4_zfmisc_1 % 5.57/5.70 % Version : [Urb07] axioms : Especial. % 5.57/5.70 % English : % 5.57/5.70 % 5.57/5.70 % Refs : [Ban01] Bancerek et al. (2001), On the Characterizations of Co % 5.57/5.70 % : [Urb07] Urban (2006), Email to G. Sutcliffe % 5.57/5.70 % Source : [Urb07] % 5.57/5.70 % Names : bushy-l4_zfmisc_1 [Urb07] % 5.57/5.70 % 5.57/5.70 % Status : Theorem % 5.57/5.70 % Rating : 0.14 v8.1.0, 0.17 v7.5.0, 0.19 v7.4.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.23 v6.0.0, 0.22 v5.4.0, 0.29 v5.3.0, 0.26 v5.2.0, 0.10 v5.0.0, 0.08 v4.1.0, 0.09 v4.0.1, 0.13 v4.0.0, 0.17 v3.7.0, 0.10 v3.5.0, 0.11 v3.4.0, 0.16 v3.3.0 % 5.57/5.70 % Syntax : Number of formulae : 15 ( 8 unt; 0 def) % 5.57/5.70 % Number of atoms : 25 ( 5 equ) % 5.57/5.70 % Maximal formula atoms : 3 ( 1 avg) % 5.57/5.70 % Number of connectives : 12 ( 2 ~; 2 |; 1 &) % 5.57/5.70 % ( 4 <=>; 3 =>; 0 <=; 0 <~>) % 5.57/5.70 % Maximal formula depth : 6 ( 3 avg) % 5.57/5.70 % Maximal term depth : 3 ( 1 avg) % 5.57/5.70 % Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty) % 5.57/5.70 % Number of functors : 3 ( 3 usr; 1 con; 0-2 aty) % 5.57/5.70 % Number of variables : 19 ( 17 !; 2 ?) % 5.57/5.70 % SPC : FOF_THM_RFO_SEQ % 5.57/5.70 % 5.57/5.70 % Comments : Translated by MPTP 0.2 from the original problem in the Mizar % 5.57/5.70 % library, www.mizar.org % 5.57/5.70 %------------------------------------------------------------------------------ % 5.57/5.70 fof(antisymmetry_r2_hidden,axiom, % 5.57/5.70 ! [A,B] : % 5.57/5.70 ( in(A,B) % 5.57/5.70 => ~ in(B,A) ) ). % 5.57/5.70 % 5.57/5.70 fof(d10_xboole_0,axiom, % 5.57/5.70 ! [A,B] : % 5.57/5.70 ( A = B % 5.57/5.70 <=> ( subset(A,B) % 5.57/5.70 & subset(B,A) ) ) ). % 5.57/5.70 % 5.57/5.70 fof(dt_k1_tarski,axiom, % 5.57/5.70 $true ). % 5.57/5.70 % 5.57/5.70 fof(dt_k1_xboole_0,axiom, % 5.57/5.70 $true ). % 5.57/5.70 % 5.57/5.70 fof(dt_k4_xboole_0,axiom, % 5.57/5.70 $true ). % 5.57/5.70 % 5.57/5.70 fof(fc1_xboole_0,axiom, % 5.57/5.70 empty(empty_set) ). % 5.57/5.70 % 5.57/5.70 fof(l2_zfmisc_1,axiom, % 5.57/5.70 ! [A,B] : % 5.57/5.70 ( subset(singleton(A),B) % 5.57/5.71 <=> in(A,B) ) ). % 5.57/5.71 % 5.57/5.71 fof(l3_zfmisc_1,axiom, % 5.57/5.71 ! [A,B,C] : % 5.57/5.71 ( subset(A,B) % 5.57/5.71 => ( in(C,A) % 5.57/5.71 | subset(A,set_difference(B,singleton(C))) ) ) ). % 5.57/5.71 % 5.57/5.71 fof(l4_zfmisc_1,conjecture, % 5.57/5.71 ! [A,B] : % 5.57/5.71 ( subset(A,singleton(B)) % 5.57/5.71 <=> ( A = empty_set % 5.57/5.71 | A = singleton(B) ) ) ). % 5.57/5.71 % 5.57/5.71 fof(rc1_xboole_0,axiom, % 5.57/5.71 ? [A] : empty(A) ). % 5.57/5.71 % 5.57/5.71 fof(rc2_xboole_0,axiom, % 5.57/5.71 ? [A] : ~ empty(A) ). % 5.57/5.71 % 5.57/5.71 fof(reflexivity_r1_tarski,axiom, % 5.57/5.71 ! [A,B] : subset(A,A) ). % 5.57/5.71 % 5.57/5.71 fof(t2_xboole_1,axiom, % 5.57/5.71 ! [A] : subset(empty_set,A) ). % 5.57/5.71 % 5.57/5.71 fof(t37_xboole_1,axiom, % 5.57/5.71 ! [A,B] : % 5.57/5.71 ( set_difference(A,B) = empty_set % 5.57/5.71 <=> subset(A,B) ) ). % 5.57/5.71 % 5.57/5.71 fof(t3_xboole_1,axiom, % 5.57/5.71 ! [A] : % 5.57/5.71 ( subset(A,empty_set) % 5.57/5.71 => A = empty_set ) ). % 5.57/5.71 % 5.57/5.71 %------------------------------------------------------------------------------ % 5.57/5.71 %------------------------------------------- % 5.57/5.71 % Proof found % 5.57/5.71 % SZS status Theorem for theBenchmark % 5.57/5.71 % SZS output start Proof % 5.57/5.71 %ClaNum:29(EqnAxiom:11) % 5.57/5.71 %VarNum:42(SingletonVarNum:20) % 5.57/5.71 %MaxLitNum:3 % 5.57/5.71 %MaxfuncDepth:2 % 5.57/5.71 %SharedTerms:15 % 5.57/5.71 %goalClause: 19 21 22 % 5.57/5.71 [12]P1(a1) % 5.57/5.71 [13]P1(a2) % 5.57/5.71 [16]~P1(a5) % 5.57/5.71 [14]P2(a1,x141) % 5.57/5.71 [15]P2(x151,x151) % 5.57/5.71 [21]~E(a3,a1)+~P2(a3,f6(a4)) % 5.57/5.71 [22]~P2(a3,f6(a4))+~E(f6(a4),a3) % 5.57/5.71 [20]~P2(x201,a1)+E(x201,a1) % 5.57/5.71 [18]~E(x181,x182)+P2(x181,x182) % 5.57/5.71 [26]~P3(x262,x261)+~P3(x261,x262) % 5.57/5.71 [23]~P2(x231,x232)+E(f7(x231,x232),a1) % 5.57/5.71 [24]P2(x241,x242)+~E(f7(x241,x242),a1) % 5.57/5.71 [25]~P3(x251,x252)+P2(f6(x251),x252) % 5.57/5.71 [27]P3(x271,x272)+~P2(f6(x271),x272) % 5.57/5.71 [19]E(a3,a1)+E(f6(a4),a3)+P2(a3,f6(a4)) % 5.57/5.71 [28]~P2(x282,x281)+~P2(x281,x282)+E(x281,x282) % 5.57/5.71 [29]~P2(x292,x293)+P3(x291,x292)+P2(x292,f7(x293,f6(x291))) % 5.57/5.71 %EqnAxiom % 5.57/5.71 [1]E(x11,x11) % 5.57/5.71 [2]E(x22,x21)+~E(x21,x22) % 5.57/5.71 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 5.57/5.71 [4]~E(x41,x42)+E(f6(x41),f6(x42)) % 5.57/5.71 [5]~E(x51,x52)+E(f7(x51,x53),f7(x52,x53)) % 5.57/5.71 [6]~E(x61,x62)+E(f7(x63,x61),f7(x63,x62)) % 5.57/5.71 [7]~P1(x71)+P1(x72)+~E(x71,x72) % 5.57/5.71 [8]P2(x82,x83)+~E(x81,x82)+~P2(x81,x83) % 5.57/5.71 [9]P2(x93,x92)+~E(x91,x92)+~P2(x93,x91) % 5.57/5.71 [10]P3(x102,x103)+~E(x101,x102)+~P3(x101,x103) % 5.57/5.71 [11]P3(x113,x112)+~E(x111,x112)+~P3(x113,x111) % 5.57/5.71 % 5.57/5.71 %------------------------------------------- % 5.57/5.71 cnf(31,plain, % 5.57/5.71 (P3(x311,f6(x311))), % 5.57/5.71 inference(scs_inference,[],[15,27])). % 5.57/5.71 cnf(32,plain, % 5.57/5.71 (P2(x321,x321)), % 5.57/5.71 inference(rename_variables,[],[15])). % 5.57/5.71 cnf(34,plain, % 5.57/5.71 (~P3(f6(x341),x341)), % 5.57/5.71 inference(scs_inference,[],[15,27,26])). % 5.57/5.71 cnf(36,plain, % 5.57/5.71 (P2(x361,x362)+~E(x362,x361)), % 5.57/5.71 inference(scs_inference,[],[15,32,27,26,8])). % 5.57/5.71 cnf(38,plain, % 5.57/5.71 (~E(f6(a4),a3)), % 5.57/5.71 inference(scs_inference,[],[15,32,27,26,8,21,22])). % 5.57/5.71 cnf(43,plain, % 5.57/5.71 (E(a3,a1)+P2(a3,f6(a4))), % 5.57/5.71 inference(scs_inference,[],[38,19])). % 5.57/5.71 cnf(44,plain, % 5.57/5.71 (~E(f6(f6(x441)),x441)), % 5.57/5.71 inference(scs_inference,[],[31,34,11])). % 5.57/5.71 cnf(45,plain, % 5.57/5.71 (P3(x451,f6(x451))), % 5.57/5.71 inference(rename_variables,[],[31])). % 5.57/5.71 cnf(48,plain, % 5.57/5.71 (~P2(f6(f6(a1)),a1)), % 5.57/5.71 inference(scs_inference,[],[31,45,34,14,11,10,28])). % 5.57/5.71 cnf(51,plain, % 5.57/5.71 (E(a1,f7(a1,x511))), % 5.57/5.71 inference(scs_inference,[],[14,2,23])). % 5.57/5.71 cnf(52,plain, % 5.57/5.71 (P2(f7(a1,x521),a1)), % 5.57/5.71 inference(scs_inference,[],[51,36])). % 5.57/5.71 cnf(53,plain, % 5.57/5.71 (E(f7(a1,x531),a1)), % 5.57/5.71 inference(scs_inference,[],[51,36,2])). % 5.57/5.71 cnf(58,plain, % 5.57/5.71 (E(f6(f7(a1,x581)),f6(a1))), % 5.57/5.71 inference(scs_inference,[],[52,20,4])). % 5.57/5.71 cnf(59,plain, % 5.57/5.71 (P2(f6(a1),f6(f7(a1,x591)))), % 5.57/5.71 inference(scs_inference,[],[58,36])). % 5.57/5.71 cnf(60,plain, % 5.57/5.71 (E(f6(a1),f6(f7(a1,x601)))), % 5.57/5.71 inference(scs_inference,[],[58,36,2])). % 5.57/5.71 cnf(67,plain, % 5.57/5.71 (E(f7(f6(x671),f6(x671)),a1)), % 5.57/5.71 inference(scs_inference,[],[31,25,23])). % 5.57/5.71 cnf(68,plain, % 5.57/5.71 (P2(f6(f7(a1,x681)),f6(a1))), % 5.57/5.71 inference(scs_inference,[],[60,36])). % 5.57/5.71 cnf(69,plain, % 5.57/5.71 (E(a1,f7(f6(x691),f6(x691)))), % 5.57/5.71 inference(scs_inference,[],[60,67,36,2])). % 5.57/5.71 cnf(72,plain, % 5.57/5.71 (P2(f6(f7(a1,x721)),f6(f7(a1,x722)))), % 5.57/5.71 inference(scs_inference,[],[59,60,44,67,36,2,3,8])). % 5.57/5.71 cnf(78,plain, % 5.57/5.71 (E(a1,a3)+P2(a3,f6(a4))), % 5.57/5.71 inference(scs_inference,[],[43,2])). % 5.57/5.71 cnf(81,plain, % 5.57/5.71 (P2(f7(f6(x811),f6(x811)),a1)), % 5.57/5.71 inference(scs_inference,[],[72,69,27,36])). % 5.57/5.71 cnf(86,plain, % 5.57/5.71 (E(f7(a1,x861),f7(f6(x862),f6(x862)))+~P2(f7(f6(x862),f6(x862)),f7(a1,x861))), % 5.57/5.71 inference(scs_inference,[],[52,72,69,48,27,36,26,9,8,28])). % 5.57/5.71 cnf(98,plain, % 5.57/5.71 (E(f7(x981,a1),f7(x981,f7(a1,x982)))), % 5.57/5.71 inference(scs_inference,[],[53,6,2])). % 5.57/5.71 cnf(100,plain, % 5.57/5.71 (E(f7(x1001,f7(a1,x1002)),f7(x1001,a1))), % 5.57/5.71 inference(scs_inference,[],[98,36,2])). % 5.57/5.71 cnf(105,plain, % 5.57/5.71 (E(f7(a1,x1051),f7(f6(x1052),f6(x1052)))), % 5.57/5.71 inference(scs_inference,[],[81,51,86,9])). % 5.57/5.71 cnf(107,plain, % 5.57/5.71 (E(f7(f6(x1071),f6(x1071)),f7(a1,x1072))), % 5.57/5.71 inference(scs_inference,[],[105,36,2])). % 5.57/5.71 cnf(110,plain, % 5.57/5.71 (E(f7(f7(a1,x1101),x1102),f7(a1,x1102))), % 5.57/5.71 inference(scs_inference,[],[51,2,5])). % 5.57/5.71 cnf(112,plain, % 5.57/5.71 (E(f7(a1,x1121),f7(f7(a1,x1122),x1121))), % 5.57/5.71 inference(scs_inference,[],[110,36,2])). % 5.57/5.71 cnf(117,plain, % 5.57/5.71 (P2(f7(f7(a1,x1171),x1172),f7(a1,x1172))), % 5.57/5.71 inference(scs_inference,[],[112,36])). % 5.57/5.71 cnf(127,plain, % 5.57/5.71 (P2(f7(f7(a1,x1271),x1272),a1)), % 5.57/5.71 inference(scs_inference,[],[53,117,9])). % 5.57/5.71 cnf(133,plain, % 5.57/5.71 (P2(f7(a1,x1331),x1332)), % 5.57/5.71 inference(scs_inference,[],[53,117,14,48,9,28,8,24])). % 5.57/5.71 cnf(136,plain, % 5.57/5.71 (E(a1,f7(f6(f7(a1,x1361)),f6(a1)))), % 5.57/5.71 inference(scs_inference,[],[68,2,23])). % 5.57/5.71 cnf(138,plain, % 5.57/5.71 (E(f7(f6(f7(a1,x1381)),f6(a1)),a1)), % 5.57/5.71 inference(scs_inference,[],[136,36,2])). % 5.57/5.71 cnf(141,plain, % 5.57/5.71 (E(f7(f7(a1,x1411),x1412),f7(a1,x1413))), % 5.57/5.71 inference(scs_inference,[],[51,127,136,133,12,36,2,9,7,28])). % 5.57/5.71 cnf(205,plain, % 5.57/5.71 (~P2(a3,a1)+~P2(a3,f6(a4))), % 5.57/5.71 inference(scs_inference,[],[21,20])). % 5.57/5.71 cnf(206,plain, % 5.57/5.71 (~E(f7(a3,a1),a1)+~P2(a3,f6(a4))), % 5.57/5.71 inference(scs_inference,[],[205,24])). % 5.57/5.71 cnf(207,plain, % 5.57/5.71 (~E(a1,f7(a3,a1))+~P2(a3,f6(a4))), % 5.57/5.72 inference(scs_inference,[],[206,2])). % 5.57/5.72 cnf(208,plain, % 5.57/5.72 (~E(a1,f7(a3,f7(a1,x2081)))+~P2(a3,f6(a4))), % 5.57/5.72 inference(scs_inference,[],[100,207,3])). % 5.57/5.72 cnf(209,plain, % 5.57/5.72 (~E(f7(a3,f7(a1,x2091)),a1)+~P2(a3,f6(a4))), % 5.57/5.72 inference(scs_inference,[],[208,2])). % 5.57/5.72 cnf(210,plain, % 5.57/5.72 (~P2(a3,f7(a1,x2101))+~P2(a3,f6(a4))), % 5.57/5.72 inference(scs_inference,[],[209,23])). % 5.57/5.72 cnf(211,plain, % 5.57/5.72 (~E(a3,f7(a1,x2111))+~P2(a3,f6(a4))), % 5.57/5.72 inference(scs_inference,[],[210,18])). % 5.57/5.72 cnf(212,plain, % 5.57/5.72 (~E(f7(a1,x2121),a3)+~P2(a3,f6(a4))), % 5.57/5.72 inference(scs_inference,[],[211,2])). % 5.57/5.72 cnf(213,plain, % 5.57/5.72 (~E(f7(a1,x2131),a3)+E(a3,a1)), % 5.57/5.72 inference(scs_inference,[],[212,43])). % 5.57/5.72 cnf(214,plain, % 5.57/5.72 (~E(a3,f7(a1,x2141))+E(a3,a1)), % 5.57/5.72 inference(scs_inference,[],[213,2])). % 5.57/5.72 cnf(221,plain, % 5.57/5.72 (~P2(a3,f7(a1,x2211))+E(a3,a1)), % 5.57/5.72 inference(scs_inference,[],[133,214,28])). % 5.57/5.72 cnf(224,plain, % 5.57/5.72 (E(a3,a1)+~E(f7(a3,f7(a1,x2241)),a1)), % 5.57/5.72 inference(scs_inference,[],[221,24])). % 5.57/5.72 cnf(225,plain, % 5.57/5.72 (~P2(f7(a3,f7(a1,x2251)),a1)+E(a3,a1)), % 5.57/5.72 inference(scs_inference,[],[224,20])). % 5.57/5.72 cnf(230,plain, % 5.57/5.72 (~E(a1,f7(a3,f7(a1,x2301)))+E(a3,a1)), % 5.57/5.72 inference(scs_inference,[],[225,36])). % 5.57/5.72 cnf(231,plain, % 5.57/5.72 (~E(a1,f7(a3,a1))+E(a3,a1)), % 5.57/5.72 inference(scs_inference,[],[98,230,3])). % 5.57/5.72 cnf(232,plain, % 5.57/5.72 (~E(f7(a3,a1),a1)+E(a3,a1)), % 5.57/5.72 inference(scs_inference,[],[231,2])). % 5.57/5.72 cnf(233,plain, % 5.57/5.72 (~P2(f7(a3,a1),a1)+E(a3,a1)), % 5.57/5.72 inference(scs_inference,[],[232,20])). % 5.57/5.72 cnf(234,plain, % 5.57/5.72 (E(a3,a1)+~E(f7(f7(a3,a1),a1),a1)), % 5.57/5.72 inference(scs_inference,[],[233,24])). % 5.57/5.72 cnf(235,plain, % 5.57/5.72 (~P2(f7(f7(a3,a1),a1),a1)+E(a3,a1)), % 5.57/5.72 inference(scs_inference,[],[234,20])). % 5.57/5.72 cnf(236,plain, % 5.57/5.72 (~E(a1,f7(f7(a3,a1),a1))+E(a3,a1)), % 5.57/5.72 inference(scs_inference,[],[235,36])). % 5.57/5.72 cnf(237,plain, % 5.57/5.72 (~E(a1,f7(f7(a3,a1),f7(a1,x2371)))+E(a3,a1)), % 5.57/5.72 inference(scs_inference,[],[100,236,3])). % 5.57/5.72 cnf(238,plain, % 5.57/5.72 (~E(f7(f7(a3,a1),f7(a1,x2381)),a1)+E(a3,a1)), % 5.57/5.72 inference(scs_inference,[],[237,2])). % 5.57/5.72 cnf(239,plain, % 5.57/5.72 (~P2(f7(a3,a1),f7(a1,x2391))+E(a3,a1)), % 5.57/5.72 inference(scs_inference,[],[238,23])). % 5.57/5.72 cnf(357,plain, % 5.57/5.72 (~P2(f7(a3,a1),f7(a1,x3571))+~P2(a3,f6(a4))), % 5.57/5.72 inference(scs_inference,[],[21,239])). % 5.57/5.72 cnf(358,plain, % 5.57/5.72 (~E(f7(a3,a1),f7(a1,x3581))+~P2(a3,f6(a4))), % 5.57/5.72 inference(scs_inference,[],[357,18])). % 5.57/5.72 cnf(403,plain, % 5.57/5.72 (~E(a1,a3)+~E(a3,a1)), % 5.57/5.72 inference(scs_inference,[],[14,21,8])). % 5.57/5.72 cnf(404,plain, % 5.57/5.72 (~E(a1,a3)), % 5.57/5.72 inference(scs_inference,[],[403,2])). % 5.57/5.72 cnf(405,plain, % 5.57/5.72 (P2(a3,f6(a4))), % 5.57/5.72 inference(scs_inference,[],[404,78])). % 5.57/5.72 cnf(406,plain, % 5.57/5.72 (~E(a3,a1)), % 5.57/5.72 inference(scs_inference,[],[405,21])). % 5.57/5.72 cnf(408,plain, % 5.57/5.72 (~P2(a3,a1)), % 5.57/5.72 inference(scs_inference,[],[405,205])). % 5.57/5.72 cnf(413,plain, % 5.57/5.72 (~P2(a3,f7(a1,x4131))), % 5.57/5.72 inference(scs_inference,[],[405,210])). % 5.57/5.72 cnf(428,plain, % 5.57/5.72 (~E(f7(a3,a1),f7(a1,x4281))), % 5.57/5.72 inference(scs_inference,[],[405,358])). % 5.57/5.72 cnf(439,plain, % 5.57/5.72 (P2(a3,f6(a4))), % 5.57/5.72 inference(scs_inference,[],[406,43])). % 5.57/5.72 cnf(477,plain, % 5.57/5.72 (E(a3,f6(a4))+~P2(f6(a4),a3)), % 5.57/5.72 inference(scs_inference,[],[406,138,81,405,408,3,8,9,20,28])). % 5.57/5.72 cnf(490,plain, % 5.57/5.72 (~P3(a4,a3)+E(a3,f6(a4))), % 5.57/5.72 inference(scs_inference,[],[477,25])). % 5.57/5.72 cnf(495,plain, % 5.57/5.72 (~E(a3,f7(f6(x4951),f6(x4951)))), % 5.57/5.72 inference(scs_inference,[],[406,67,3])). % 5.57/5.72 cnf(501,plain, % 5.57/5.72 (P2(x5011,f6(a4))+~E(a3,x5011)), % 5.57/5.72 inference(scs_inference,[],[428,439,141,3,8])). % 5.57/5.72 cnf(589,plain, % 5.57/5.72 (~P3(a4,a3)), % 5.57/5.72 inference(scs_inference,[],[38,490,2])). % 5.57/5.72 cnf(590,plain, % 5.57/5.72 (P2(a3,f7(f6(a4),f6(a4)))), % 5.57/5.72 inference(scs_inference,[],[589,501,29])). % 5.57/5.72 cnf(594,plain, % 5.57/5.72 ($false), % 5.57/5.72 inference(scs_inference,[],[107,495,413,590,28,9]), % 5.57/5.72 ['proof']). % 5.57/5.72 % SZS output end Proof % 5.57/5.72 % Total time :5.090000s %------------------------------------------------------------------------------