%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SET600+3 : TPTP v8.2.0. Released v2.2.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/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 14:21:55 EDT 2024 % Result : Theorem 33.01s 33.11s % Output : CNFRefutation 33.10s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.12 % Problem : SET600+3 : TPTP v8.2.0. Released v2.2.0. % 0.08/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n028.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 : Sun Jun 23 12:21:39 EDT 2024 % 0.12/0.33 % CPUTime : % 0.19/0.57 start to proof:theBenchmark % 33.01/33.10 %------------------------------------------- % 33.01/33.10 % File :CSE---1.7 % 33.01/33.10 % Problem :theBenchmark % 33.01/33.10 % Transform :cnf % 33.01/33.10 % Format :tptp:raw % 33.01/33.10 % Command :java -jar mcs_scs.jar %d %s % 33.01/33.10 % 33.01/33.10 % Result :Theorem 32.500000s % 33.01/33.10 % Output :CNFRefutation 32.500000s % 33.01/33.10 %------------------------------------------- % 33.01/33.11 %-------------------------------------------------------------------------- % 33.01/33.11 % File : SET600+3 : TPTP v8.2.0. Released v2.2.0. % 33.01/33.11 % Domain : Set Theory % 33.01/33.11 % Problem : X U Y = empty set iff X = empty set & Y = empty set % 33.01/33.11 % Version : [Try90] axioms : Reduced > Incomplete. % 33.01/33.11 % English : The union of X and Y is the empty set iff X is the empty set % 33.01/33.11 % and Y is the empty set. % 33.01/33.11 % 33.01/33.11 % Refs : [ILF] The ILF Group (1998), The ILF System: A Tool for the Int % 33.01/33.11 % : [Try90] Trybulec (1990), Tarski Grothendieck Set Theory % 33.01/33.11 % : [TS89] Trybulec & Swieczkowska (1989), Boolean Properties of % 33.01/33.11 % Source : [ILF] % 33.01/33.11 % Names : BOOLE (59) [TS89] % 33.01/33.11 % 33.01/33.11 % Status : Theorem % 33.01/33.11 % Rating : 0.14 v8.2.0, 0.11 v8.1.0, 0.06 v7.4.0, 0.07 v7.2.0, 0.03 v7.1.0, 0.04 v7.0.0, 0.03 v6.4.0, 0.08 v6.3.0, 0.12 v6.2.0, 0.08 v6.1.0, 0.07 v6.0.0, 0.17 v5.5.0, 0.11 v5.4.0, 0.18 v5.3.0, 0.19 v5.2.0, 0.00 v5.0.0, 0.08 v4.1.0, 0.09 v4.0.1, 0.13 v4.0.0, 0.12 v3.7.0, 0.05 v3.4.0, 0.11 v3.3.0, 0.07 v3.2.0, 0.18 v3.1.0, 0.11 v2.7.0, 0.00 v2.6.0, 0.14 v2.5.0, 0.25 v2.4.0, 0.25 v2.3.0, 0.33 v2.2.1 % 33.01/33.11 % Syntax : Number of formulae : 9 ( 3 unt; 0 def) % 33.01/33.11 % Number of atoms : 20 ( 6 equ) % 33.01/33.11 % Maximal formula atoms : 3 ( 2 avg) % 33.01/33.11 % Number of connectives : 13 ( 2 ~; 1 |; 2 &) % 33.01/33.11 % ( 7 <=>; 1 =>; 0 <=; 0 <~>) % 33.01/33.11 % Maximal formula depth : 6 ( 5 avg) % 33.01/33.11 % Maximal term depth : 2 ( 1 avg) % 33.01/33.11 % Number of predicates : 4 ( 3 usr; 0 prp; 1-2 aty) % 33.01/33.11 % Number of functors : 2 ( 2 usr; 1 con; 0-2 aty) % 33.01/33.11 % Number of variables : 19 ( 19 !; 0 ?) % 33.01/33.11 % SPC : FOF_THM_RFO_SEQ % 33.01/33.11 % 33.01/33.11 % Comments : % 33.01/33.11 %-------------------------------------------------------------------------- % 33.01/33.11 %---- line(boole - df(2),1833042) % 33.01/33.11 fof(union_defn,axiom, % 33.01/33.11 ! [B,C,D] : % 33.01/33.11 ( member(D,union(B,C)) % 33.01/33.11 <=> ( member(D,B) % 33.01/33.11 | member(D,C) ) ) ). % 33.01/33.11 % 33.01/33.11 %---- line(hidden - axiom89,1832636) % 33.01/33.11 fof(empty_set_defn,axiom, % 33.01/33.11 ! [B] : ~ member(B,empty_set) ). % 33.01/33.11 % 33.01/33.11 %---- line(boole - df(8),1833103) % 33.01/33.11 fof(equal_defn,axiom, % 33.01/33.11 ! [B,C] : % 33.01/33.11 ( B = C % 33.01/33.11 <=> ( subset(B,C) % 33.01/33.11 & subset(C,B) ) ) ). % 33.01/33.11 % 33.01/33.11 %---- property(commutativity,op(union,2,function)) % 33.01/33.11 fof(commutativity_of_union,axiom, % 33.01/33.11 ! [B,C] : union(B,C) = union(C,B) ). % 33.01/33.11 % 33.01/33.11 %---- line(tarski - df(3),1832749) % 33.01/33.11 fof(subset_defn,axiom, % 33.01/33.11 ! [B,C] : % 33.01/33.11 ( subset(B,C) % 33.01/33.11 <=> ! [D] : % 33.01/33.11 ( member(D,B) % 33.01/33.11 => member(D,C) ) ) ). % 33.01/33.11 % 33.01/33.11 %---- property(reflexivity,op(subset,2,predicate)) % 33.01/33.11 fof(reflexivity_of_subset,axiom, % 33.01/33.11 ! [B] : subset(B,B) ). % 33.01/33.11 % 33.01/33.11 %---- line(hidden - axiom91,1832628) % 33.01/33.11 fof(empty_defn,axiom, % 33.01/33.11 ! [B] : % 33.01/33.11 ( empty(B) % 33.01/33.11 <=> ! [C] : ~ member(C,B) ) ). % 33.01/33.11 % 33.01/33.11 %---- line(hidden - axiom92,1832615) % 33.01/33.11 fof(equal_member_defn,axiom, % 33.01/33.11 ! [B,C] : % 33.01/33.11 ( B = C % 33.01/33.11 <=> ! [D] : % 33.01/33.11 ( member(D,B) % 33.01/33.11 <=> member(D,C) ) ) ). % 33.01/33.11 % 33.01/33.11 %---- line(boole - th(59),1833646) % 33.01/33.11 fof(prove_th59,conjecture, % 33.01/33.11 ! [B,C] : % 33.01/33.11 ( union(B,C) = empty_set % 33.01/33.11 <=> ( B = empty_set % 33.01/33.11 & C = empty_set ) ) ). % 33.01/33.11 % 33.01/33.11 %-------------------------------------------------------------------------- % 33.01/33.11 %------------------------------------------- % 33.01/33.11 % Proof found % 33.01/33.11 % SZS status Theorem for theBenchmark % 33.01/33.11 % SZS output start Proof % 33.01/33.11 %ClaNum:34(EqnAxiom:15) % 33.01/33.11 %VarNum:72(SingletonVarNum:31) % 33.01/33.11 %MaxLitNum:3 % 33.01/33.11 %MaxfuncDepth:1 % 33.01/33.11 %SharedTerms:10 % 33.01/33.11 %goalClause: 19 20 23 % 33.01/33.11 [16]P1(x161,x161) % 33.01/33.11 [18]~P2(x181,a2) % 33.01/33.11 [17]E(f1(x171,x172),f1(x172,x171)) % 33.01/33.11 [19]E(a2,a3)+E(f1(a3,a7),a2) % 33.01/33.11 [20]E(a7,a2)+E(f1(a3,a7),a2) % 33.01/33.11 [24]P3(x241)+P2(f4(x241),x241) % 33.01/33.11 [22]~E(x221,x222)+P1(x221,x222) % 33.01/33.11 [25]~P3(x251)+~P2(x252,x251) % 33.01/33.11 [27]P1(x271,x272)+P2(f5(x271,x272),x271) % 33.01/33.11 [31]P1(x311,x312)+~P2(f5(x311,x312),x312) % 33.01/33.11 [29]~P2(x291,x293)+P2(x291,f1(x292,x293)) % 33.01/33.11 [30]~P2(x301,x302)+P2(x301,f1(x302,x303)) % 33.01/33.11 [23]~E(a2,a3)+~E(a7,a2)+~E(f1(a3,a7),a2) % 33.01/33.11 [26]~P1(x262,x261)+~P1(x261,x262)+E(x261,x262) % 33.01/33.11 [32]E(x321,x322)+P2(f6(x321,x322),x322)+P2(f6(x321,x322),x321) % 33.01/33.11 [34]E(x341,x342)+~P2(f6(x341,x342),x342)+~P2(f6(x341,x342),x341) % 33.01/33.11 [28]~P1(x283,x282)+P2(x281,x282)+~P2(x281,x283) % 33.01/33.11 [33]P2(x331,x332)+P2(x331,x333)+~P2(x331,f1(x333,x332)) % 33.01/33.11 %EqnAxiom % 33.01/33.11 [1]E(x11,x11) % 33.01/33.11 [2]E(x22,x21)+~E(x21,x22) % 33.01/33.11 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 33.01/33.11 [4]~E(x41,x42)+E(f1(x41,x43),f1(x42,x43)) % 33.01/33.11 [5]~E(x51,x52)+E(f1(x53,x51),f1(x53,x52)) % 33.01/33.11 [6]~E(x61,x62)+E(f6(x61,x63),f6(x62,x63)) % 33.01/33.11 [7]~E(x71,x72)+E(f6(x73,x71),f6(x73,x72)) % 33.01/33.11 [8]~E(x81,x82)+E(f5(x81,x83),f5(x82,x83)) % 33.01/33.11 [9]~E(x91,x92)+E(f5(x93,x91),f5(x93,x92)) % 33.01/33.11 [10]~E(x101,x102)+E(f4(x101),f4(x102)) % 33.01/33.11 [11]P1(x112,x113)+~E(x111,x112)+~P1(x111,x113) % 33.01/33.11 [12]P1(x123,x122)+~E(x121,x122)+~P1(x123,x121) % 33.01/33.11 [13]P2(x132,x133)+~E(x131,x132)+~P2(x131,x133) % 33.01/33.11 [14]P2(x143,x142)+~E(x141,x142)+~P2(x143,x141) % 33.01/33.11 [15]~P3(x151)+P3(x152)+~E(x151,x152) % 33.01/33.11 % 33.01/33.11 %------------------------------------------- % 33.10/33.12 cnf(36,plain, % 33.10/33.12 (P3(a2)), % 33.10/33.12 inference(scs_inference,[],[18,24])). % 33.10/33.12 cnf(37,plain, % 33.10/33.12 (~P2(x371,a2)), % 33.10/33.12 inference(rename_variables,[],[18])). % 33.10/33.12 cnf(39,plain, % 33.10/33.12 (P1(a2,x391)), % 33.10/33.12 inference(scs_inference,[],[18,37,24,27])). % 33.10/33.12 cnf(42,plain, % 33.10/33.12 (P1(f1(x421,x422),f1(x422,x421))), % 33.10/33.12 inference(scs_inference,[],[16,18,37,17,24,27,11])). % 33.10/33.12 cnf(44,plain, % 33.10/33.12 (~P3(f1(x441,x442))+P3(f1(x442,x441))), % 33.10/33.12 inference(scs_inference,[],[16,18,37,17,24,27,11,15])). % 33.10/33.12 cnf(47,plain, % 33.10/33.12 (~P2(x471,f1(x472,x473))+~P3(f1(x473,x472))), % 33.10/33.12 inference(scs_inference,[],[25,44])). % 33.10/33.12 cnf(50,plain, % 33.10/33.12 (P3(a3)+E(f1(a3,a7),a2)), % 33.10/33.12 inference(scs_inference,[],[36,19,15])). % 33.10/33.12 cnf(51,plain, % 33.10/33.12 (~P2(x511,a3)+E(f1(a3,a7),a2)), % 33.10/33.12 inference(scs_inference,[],[50,25])). % 33.10/33.12 cnf(52,plain, % 33.10/33.12 (P1(a7,a2)+E(f1(a3,a7),a2)), % 33.10/33.12 inference(scs_inference,[],[16,20,12])). % 33.10/33.12 cnf(54,plain, % 33.10/33.12 (P1(x541,x542)+P2(f5(x541,x542),f1(x541,x543))), % 33.10/33.12 inference(scs_inference,[],[30,27])). % 33.10/33.12 cnf(55,plain, % 33.10/33.12 (P1(f1(x551,x552),x553)+~P2(f5(f1(x552,x551),x553),x553)), % 33.10/33.12 inference(scs_inference,[],[17,31,11])). % 33.10/33.12 cnf(56,plain, % 33.10/33.12 (P1(a3,x561)+E(f1(a3,a7),a2)), % 33.10/33.12 inference(scs_inference,[],[51,27])). % 33.10/33.12 cnf(57,plain, % 33.10/33.12 (E(a2,a7)+E(f1(a3,a7),a2)), % 33.10/33.12 inference(scs_inference,[],[39,52,26])). % 33.10/33.12 cnf(59,plain, % 33.10/33.12 (E(a3,a2)+E(f1(a3,a7),a2)), % 33.10/33.12 inference(scs_inference,[],[39,56,26])). % 33.10/33.12 cnf(60,plain, % 33.10/33.12 (P3(a7)+E(f1(a3,a7),a2)), % 33.10/33.12 inference(scs_inference,[],[36,57,15])). % 33.10/33.12 cnf(61,plain, % 33.10/33.12 (~P2(x611,a7)+E(f1(a3,a7),a2)), % 33.10/33.12 inference(scs_inference,[],[60,25])). % 33.10/33.12 cnf(63,plain, % 33.10/33.12 (P1(a7,x631)+E(f1(a3,a7),a2)), % 33.10/33.12 inference(scs_inference,[],[61,27])). % 33.10/33.12 cnf(64,plain, % 33.10/33.12 (P1(f1(a3,a7),a2)+P1(a7,x641)), % 33.10/33.12 inference(scs_inference,[],[16,63,12])). % 33.10/33.12 cnf(65,plain, % 33.10/33.12 (~P2(x651,a7)+P1(f1(a3,a7),a2)), % 33.10/33.12 inference(scs_inference,[],[18,64,28])). % 33.10/33.12 cnf(66,plain, % 33.10/33.12 (P3(a7)+P1(f1(a3,a7),a2)), % 33.10/33.12 inference(scs_inference,[],[65,24])). % 33.10/33.12 cnf(67,plain, % 33.10/33.12 (P1(f1(a7,a3),a2)+P3(a7)), % 33.10/33.12 inference(scs_inference,[],[17,66,11])). % 33.10/33.12 cnf(68,plain, % 33.10/33.12 (~P2(x681,f1(a7,a3))+P3(a7)), % 33.10/33.12 inference(scs_inference,[],[18,67,28])). % 33.10/33.12 cnf(69,plain, % 33.10/33.12 (P1(a7,x691)+P3(a7)), % 33.10/33.12 inference(scs_inference,[],[68,54])). % 33.10/33.12 cnf(70,plain, % 33.10/33.12 (~P2(x701,a7)+P3(a7)), % 33.10/33.12 inference(scs_inference,[],[18,69,28])). % 33.10/33.12 cnf(71,plain, % 33.10/33.12 (P3(a7)), % 33.10/33.12 inference(scs_inference,[],[70,24])). % 33.10/33.12 cnf(72,plain, % 33.10/33.12 (~P2(x721,a7)), % 33.10/33.12 inference(scs_inference,[],[71,25])). % 33.10/33.12 cnf(74,plain, % 33.10/33.12 (P1(a7,x741)), % 33.10/33.12 inference(scs_inference,[],[71,25,27])). % 33.10/33.12 cnf(76,plain, % 33.10/33.12 (E(a7,a2)), % 33.10/33.12 inference(scs_inference,[],[39,71,25,27,26])). % 33.10/33.12 cnf(79,plain, % 33.10/33.12 (E(a2,a7)), % 33.10/33.12 inference(scs_inference,[],[39,71,25,27,26,2])). % 33.10/33.12 cnf(80,plain, % 33.10/33.12 (~E(a2,a3)+~E(f1(a3,a7),a2)), % 33.10/33.12 inference(scs_inference,[],[76,23])). % 33.10/33.12 cnf(81,plain, % 33.10/33.12 (~E(a3,a2)+~E(f1(a3,a7),a2)), % 33.10/33.12 inference(scs_inference,[],[80,2])). % 33.10/33.12 cnf(85,plain, % 33.10/33.12 (P1(f1(x851,x852),f1(x853,x854))+~P2(f5(f1(x852,x851),f1(x853,x854)),x854)), % 33.10/33.12 inference(scs_inference,[],[55,29])). % 33.10/33.12 cnf(88,plain, % 33.10/33.12 (P1(f1(x881,x882),f1(x883,f1(x882,x881)))+P1(f1(x882,x881),f1(x883,f1(x882,x881)))), % 33.10/33.12 inference(scs_inference,[],[85,27])). % 33.10/33.12 cnf(89,plain, % 33.10/33.12 (P1(f1(x891,x892),f1(x893,f1(x891,x892)))), % 33.10/33.12 inference(scs_inference,[],[17,88,11])). % 33.10/33.12 cnf(90,plain, % 33.10/33.12 (P1(f1(x901,x902),f1(f1(x901,x902),x903))), % 33.10/33.12 inference(scs_inference,[],[17,89,12])). % 33.10/33.12 cnf(91,plain, % 33.10/33.12 (P1(f1(x911,x912),f1(x913,f1(x911,x912)))), % 33.10/33.12 inference(rename_variables,[],[89])). % 33.10/33.12 cnf(92,plain, % 33.10/33.12 (E(f1(x921,x922),f1(x922,x921))), % 33.10/33.12 inference(rename_variables,[],[17])). % 33.10/33.12 cnf(93,plain, % 33.10/33.12 (P1(f1(x931,x932),f1(x933,f1(x932,x931)))), % 33.10/33.12 inference(scs_inference,[],[17,92,89,91,12,11])). % 33.10/33.12 cnf(94,plain, % 33.10/33.12 (P1(f1(x941,x942),f1(x943,f1(x941,x942)))), % 33.10/33.12 inference(rename_variables,[],[89])). % 33.10/33.12 cnf(95,plain, % 33.10/33.12 (E(f1(x951,x952),f1(x953,f1(x951,x952)))+~P1(f1(x953,f1(x951,x952)),f1(x951,x952))), % 33.10/33.12 inference(scs_inference,[],[17,92,89,91,94,12,11,26])). % 33.10/33.12 cnf(97,plain, % 33.10/33.12 (~P1(f1(x971,f1(x972,x973)),f1(x972,x973))+E(f1(x971,f1(x972,x973)),f1(x972,x973))), % 33.10/33.12 inference(scs_inference,[],[95,2])). % 33.10/33.12 cnf(98,plain, % 33.10/33.12 (P1(f1(x981,x982),f1(f1(x982,x981),x983))), % 33.10/33.12 inference(scs_inference,[],[17,93,12])). % 33.10/33.12 cnf(100,plain, % 33.10/33.12 (E(f1(x1001,x1002),f1(x1002,x1001))), % 33.10/33.12 inference(rename_variables,[],[17])). % 33.10/33.12 cnf(103,plain, % 33.10/33.12 (E(f1(x1031,x1032),f1(f1(x1031,x1032),x1033))+~E(f1(x1032,x1031),f1(f1(x1031,x1032),x1033))), % 33.10/33.12 inference(scs_inference,[],[17,42,90,93,12,26,11])). % 33.10/33.12 cnf(106,plain, % 33.10/33.12 (E(f1(x1061,x1062),f1(f1(x1061,x1062),x1061))+~E(f1(x1062,x1061),f1(x1061,f1(x1061,x1062)))), % 33.10/33.12 inference(scs_inference,[],[17,100,42,90,93,12,26,11,4,3])). % 33.10/33.12 cnf(116,plain, % 33.10/33.12 (E(f1(x1161,x1162),f1(f1(x1162,x1161),x1162))+~E(f1(x1161,x1162),f1(x1162,f1(x1162,x1161)))), % 33.10/33.12 inference(scs_inference,[],[42,98,26,11,103,106])). % 33.10/33.12 cnf(134,plain, % 33.10/33.12 (~E(f1(x1341,x1342),f1(x1342,f1(x1342,x1341)))+E(f1(f1(x1342,x1341),x1342),f1(x1341,x1342))), % 33.10/33.12 inference(scs_inference,[],[116,2])). % 33.10/33.12 cnf(147,plain, % 33.10/33.12 (~P2(x1471,f1(a7,a2))), % 33.10/33.12 inference(scs_inference,[],[72,79,14,33])). % 33.10/33.12 cnf(148,plain, % 33.10/33.12 (P3(f1(a7,a2))), % 33.10/33.12 inference(scs_inference,[],[147,24])). % 33.10/33.12 cnf(149,plain, % 33.10/33.12 (~P2(x1491,f1(a7,a2))), % 33.10/33.12 inference(rename_variables,[],[147])). % 33.10/33.12 cnf(152,plain, % 33.10/33.12 (~P2(x1521,f1(a7,a2))), % 33.10/33.12 inference(rename_variables,[],[147])). % 33.10/33.12 cnf(154,plain, % 33.10/33.12 (E(a7,f1(a7,a2))), % 33.10/33.12 inference(scs_inference,[],[72,147,149,152,24,27,32])). % 33.10/33.12 cnf(158,plain, % 33.10/33.12 (E(a2,f1(a7,a2))), % 33.10/33.12 inference(scs_inference,[],[79,72,147,149,152,24,27,32,3])). % 33.10/33.12 cnf(159,plain, % 33.10/33.12 (P3(f1(a2,a7))), % 33.10/33.12 inference(scs_inference,[],[79,17,72,147,149,152,24,27,32,3,15])). % 33.10/33.12 cnf(160,plain, % 33.10/33.12 (E(f1(x1601,x1602),f1(x1602,x1601))), % 33.10/33.12 inference(rename_variables,[],[17])). % 33.10/33.12 cnf(161,plain, % 33.10/33.12 (P1(f1(a2,a7),x1611)), % 33.10/33.12 inference(scs_inference,[],[79,17,160,72,147,149,152,24,27,32,3,15,11])). % 33.10/33.12 cnf(163,plain, % 33.10/33.12 (~P2(x1631,f1(a2,a7))), % 33.10/33.12 inference(scs_inference,[],[79,17,160,72,147,149,152,24,27,32,3,15,11,47])). % 33.10/33.12 cnf(168,plain, % 33.10/33.12 (E(a2,f1(a2,a7))), % 33.10/33.12 inference(scs_inference,[],[158,18,163,2,32])). % 33.10/33.12 cnf(172,plain, % 33.10/33.12 (E(a7,f1(a2,a7))), % 33.10/33.12 inference(scs_inference,[],[161,158,18,74,163,2,32,26])). % 33.10/33.12 cnf(177,plain, % 33.10/33.12 (E(f1(a2,a7),a7)), % 33.10/33.12 inference(scs_inference,[],[172,2])). % 33.10/33.12 cnf(179,plain, % 33.10/33.12 (E(f1(a2,a7),a2)), % 33.10/33.12 inference(scs_inference,[],[168,2])). % 33.10/33.12 cnf(183,plain, % 33.10/33.12 (~P2(x1831,f1(a7,f1(a7,a2)))), % 33.10/33.12 inference(scs_inference,[],[148,72,25,33])). % 33.10/33.12 cnf(184,plain, % 33.10/33.12 (~P2(x1841,f1(a2,a2))), % 33.10/33.12 inference(scs_inference,[],[36,18,25,33])). % 33.10/33.12 cnf(186,plain, % 33.10/33.12 (~P2(x1861,f1(a2,a2))), % 33.10/33.12 inference(rename_variables,[],[184])). % 33.10/33.12 cnf(188,plain, % 33.10/33.12 (P1(f1(a2,a2),x1881)), % 33.10/33.12 inference(scs_inference,[],[184,186,24,27])). % 33.10/33.12 cnf(201,plain, % 33.10/33.12 (E(f1(a7,x2011),f1(a2,x2011))), % 33.10/33.12 inference(scs_inference,[],[79,2,4])). % 33.10/33.12 cnf(202,plain, % 33.10/33.12 (E(f1(a2,x2021),f1(a7,x2021))), % 33.10/33.12 inference(scs_inference,[],[201,2])). % 33.10/33.12 cnf(205,plain, % 33.10/33.12 (P3(f1(a7,a7))), % 33.10/33.12 inference(scs_inference,[],[177,201,159,2,3,15])). % 33.10/33.12 cnf(206,plain, % 33.10/33.12 (~P2(x2061,f1(a7,a7))), % 33.10/33.12 inference(scs_inference,[],[177,201,159,2,3,15,47])). % 33.10/33.12 cnf(213,plain, % 33.10/33.12 (E(f1(x2131,f1(a7,a2)),f1(x2131,a7))), % 33.10/33.12 inference(scs_inference,[],[154,2,5])). % 33.10/33.12 cnf(214,plain, % 33.10/33.12 (E(f1(x2141,a7),f1(x2141,f1(a7,a2)))), % 33.10/33.12 inference(scs_inference,[],[213,2])). % 33.10/33.12 cnf(228,plain, % 33.10/33.12 (E(f6(f1(a7,a2),x2281),f6(a7,x2281))), % 33.10/33.12 inference(scs_inference,[],[154,2,6])). % 33.10/33.12 cnf(234,plain, % 33.10/33.12 (E(f1(a2,a7),f1(a7,f1(a7,a2)))), % 33.10/33.12 inference(scs_inference,[],[228,214,202,72,206,2,32,3])). % 33.10/33.12 cnf(235,plain, % 33.10/33.12 (E(f1(x2351,a7),f1(x2351,f1(a7,a2)))), % 33.10/33.12 inference(rename_variables,[],[214])). % 33.10/33.12 cnf(238,plain, % 33.10/33.12 (E(f1(x2381,a7),f1(x2381,f1(a7,a2)))), % 33.10/33.12 inference(rename_variables,[],[214])). % 33.10/33.12 cnf(239,plain, % 33.10/33.12 (P1(f1(a2,f1(a7,a2)),x2391)), % 33.10/33.12 inference(scs_inference,[],[228,214,235,238,202,161,72,205,206,2,32,3,15,11])). % 33.10/33.12 cnf(243,plain, % 33.10/33.12 (E(f1(f1(a7,a2),a7),f1(a2,a7))), % 33.10/33.12 inference(scs_inference,[],[228,214,235,238,202,161,72,205,206,2,32,3,15,11,97,134])). % 33.10/33.12 cnf(247,plain, % 33.10/33.12 (P3(f1(f1(a7,a2),a7))), % 33.10/33.13 inference(scs_inference,[],[228,214,235,238,202,161,72,205,206,2,32,3,15,11,97,134,47,24])). % 33.10/33.13 cnf(253,plain, % 33.10/33.13 (E(f1(a7,f1(a7,a2)),f1(a2,a7))), % 33.10/33.13 inference(scs_inference,[],[234,2])). % 33.10/33.13 cnf(258,plain, % 33.10/33.13 (E(f1(f1(a7,a2),f1(a7,a2)),f1(a2,a7))), % 33.10/33.13 inference(scs_inference,[],[239,234,243,213,39,2,26,3])). % 33.10/33.13 cnf(262,plain, % 33.10/33.13 (P1(f1(a7,f1(a7,a2)),x2621)), % 33.10/33.13 inference(scs_inference,[],[239,234,243,214,161,213,39,247,2,26,3,15,11])). % 33.10/33.13 cnf(275,plain, % 33.10/33.13 (E(f1(f1(a7,a2),f1(a7,a2)),a7)), % 33.10/33.13 inference(scs_inference,[],[42,258,262,177,89,2,12,26,3])). % 33.10/33.13 cnf(293,plain, % 33.10/33.13 (E(f1(a7,f1(a7,a2)),a7)), % 33.10/33.13 inference(scs_inference,[],[161,253,275,177,188,2,26,3])). % 33.10/33.13 cnf(297,plain, % 33.10/33.13 (E(a7,f1(a7,f1(a7,a2)))), % 33.10/33.13 inference(scs_inference,[],[293,2])). % 33.10/33.13 cnf(1444,plain, % 33.10/33.13 (~P2(x14441,f1(a3,a7))+P3(a3)), % 33.10/33.13 inference(scs_inference,[],[18,50,14])). % 33.10/33.13 cnf(1445,plain, % 33.10/33.13 (P3(f1(a3,a7))+P3(a3)), % 33.10/33.13 inference(scs_inference,[],[1444,24])). % 33.10/33.13 cnf(1446,plain, % 33.10/33.13 (P3(f1(a7,a3))+P3(a3)), % 33.10/33.13 inference(scs_inference,[],[1445,44])). % 33.10/33.13 cnf(1447,plain, % 33.10/33.13 (~P2(x14471,f1(a7,a3))+P3(a3)), % 33.10/33.13 inference(scs_inference,[],[1446,25])). % 33.10/33.13 cnf(1448,plain, % 33.10/33.13 (P1(f1(a7,a3),x14481)+P3(a3)), % 33.10/33.13 inference(scs_inference,[],[1447,27])). % 33.10/33.13 cnf(1449,plain, % 33.10/33.13 (P1(f1(a2,a3),x14491)+P3(a3)), % 33.10/33.13 inference(scs_inference,[],[201,1448,11])). % 33.10/33.13 cnf(1450,plain, % 33.10/33.13 (E(f1(a7,f1(a7,a2)),f1(a2,a3))+P3(a3)), % 33.10/33.13 inference(scs_inference,[],[262,1449,26])). % 33.10/33.13 cnf(1451,plain, % 33.10/33.13 (E(f1(a2,a3),f1(a7,f1(a7,a2)))+P3(a3)), % 33.10/33.13 inference(scs_inference,[],[1450,2])). % 33.10/33.13 cnf(1452,plain, % 33.10/33.13 (~P2(x14521,f1(a2,a3))+P3(a3)), % 33.10/33.13 inference(scs_inference,[],[183,1451,14])). % 33.10/33.13 cnf(1453,plain, % 33.10/33.13 (~P2(x14531,a3)+P3(a3)), % 33.10/33.13 inference(scs_inference,[],[1452,29])). % 33.10/33.13 cnf(1454,plain, % 33.10/33.13 (P3(a3)), % 33.10/33.13 inference(scs_inference,[],[1453,24])). % 33.10/33.13 cnf(1455,plain, % 33.10/33.13 (~P2(x14551,a3)), % 33.10/33.13 inference(scs_inference,[],[1454,25])). % 33.10/33.13 cnf(1463,plain, % 33.10/33.13 (E(a7,a3)), % 33.10/33.13 inference(scs_inference,[],[262,297,1454,25,27,26,2,3])). % 33.10/33.13 cnf(1470,plain, % 33.10/33.13 (E(a2,a3)), % 33.10/33.13 inference(scs_inference,[],[79,1463,184,1455,2,32,3])). % 33.10/33.13 cnf(1471,plain, % 33.10/33.13 (~E(f1(a3,a7),a2)), % 33.10/33.13 inference(scs_inference,[],[1470,80])). % 33.10/33.13 cnf(1472,plain, % 33.10/33.13 (E(a3,a2)), % 33.10/33.13 inference(scs_inference,[],[1471,59])). % 33.10/33.13 cnf(1483,plain, % 33.10/33.13 (~E(f1(a3,a7),a2)), % 33.10/33.13 inference(scs_inference,[],[1472,81])). % 33.10/33.13 cnf(1491,plain, % 33.10/33.13 ($false), % 33.10/33.13 inference(scs_inference,[],[179,1483,1472,3,4]), % 33.10/33.13 ['proof']). % 33.10/33.13 % SZS output end Proof % 33.10/33.13 % Total time :32.500000s %------------------------------------------------------------------------------