%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SET638+3 : TPTP v8.2.0. Released v2.2.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n029.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:22:05 EDT 2024 % Result : Theorem 2.25s 2.36s % Output : CNFRefutation 2.25s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SET638+3 : TPTP v8.2.0. Released v2.2.0. % 0.03/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n029.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 16:21:54 EDT 2024 % 0.12/0.33 % CPUTime : % 0.19/0.56 start to proof:theBenchmark % 2.25/2.35 %------------------------------------------- % 2.25/2.35 % File :CSE---1.7 % 2.25/2.35 % Problem :theBenchmark % 2.25/2.35 % Transform :cnf % 2.25/2.35 % Format :tptp:raw % 2.25/2.35 % Command :java -jar mcs_scs.jar %d %s % 2.25/2.35 % 2.25/2.35 % Result :Theorem 1.740000s % 2.25/2.35 % Output :CNFRefutation 1.740000s % 2.25/2.35 %------------------------------------------- % 2.25/2.35 %-------------------------------------------------------------------------- % 2.25/2.35 % File : SET638+3 : TPTP v8.2.0. Released v2.2.0. % 2.25/2.35 % Domain : Set Theory % 2.25/2.35 % Problem : If X (= Y U Z and X ^ Z = the empty set , then X (= Y % 2.25/2.35 % Version : [Try90] axioms : Reduced > Incomplete. % 2.25/2.35 % English : If X is a subset of the union of Y and Z and the intersection % 2.25/2.35 % of X and Z is the empty set, then X is a subset of Y. % 2.25/2.35 % 2.25/2.35 % Refs : [ILF] The ILF Group (1998), The ILF System: A Tool for the Int % 2.25/2.35 % : [Try90] Trybulec (1990), Tarski Grothendieck Set Theory % 2.25/2.35 % : [TS89] Trybulec & Swieczkowska (1989), Boolean Properties of % 2.25/2.35 % Source : [ILF] % 2.25/2.35 % Names : BOOLE (120) [TS89] % 2.25/2.35 % 2.25/2.35 % Status : Theorem % 2.25/2.35 % Rating : 0.08 v7.5.0, 0.09 v7.4.0, 0.00 v7.0.0, 0.03 v6.4.0, 0.08 v6.2.0, 0.16 v6.1.0, 0.13 v5.5.0, 0.22 v5.4.0, 0.21 v5.3.0, 0.26 v5.2.0, 0.05 v5.0.0, 0.12 v4.1.0, 0.13 v4.0.1, 0.17 v3.7.0, 0.10 v3.5.0, 0.11 v3.3.0, 0.07 v3.2.0, 0.18 v3.1.0, 0.11 v2.7.0, 0.17 v2.6.0, 0.14 v2.5.0, 0.00 v2.3.0, 0.33 v2.2.1 % 2.25/2.35 % Syntax : Number of formulae : 15 ( 7 unt; 0 def) % 2.25/2.35 % Number of atoms : 29 ( 8 equ) % 2.25/2.35 % Maximal formula atoms : 3 ( 1 avg) % 2.25/2.35 % Number of connectives : 16 ( 2 ~; 1 |; 3 &) % 2.25/2.35 % ( 7 <=>; 3 =>; 0 <=; 0 <~>) % 2.25/2.35 % Maximal formula depth : 6 ( 4 avg) % 2.25/2.35 % Maximal term depth : 3 ( 1 avg) % 2.25/2.35 % Number of predicates : 4 ( 3 usr; 0 prp; 1-2 aty) % 2.25/2.35 % Number of functors : 3 ( 3 usr; 1 con; 0-2 aty) % 2.25/2.35 % Number of variables : 33 ( 33 !; 0 ?) % 2.25/2.35 % SPC : FOF_THM_RFO_SEQ % 2.25/2.35 % 2.25/2.35 % Comments : % 2.25/2.35 %-------------------------------------------------------------------------- % 2.25/2.35 %---- line(boole - th(37),1833277) % 2.25/2.35 fof(intersection_is_subset,axiom, % 2.25/2.35 ! [B,C] : subset(intersection(B,C),B) ). % 2.25/2.35 % 2.25/2.35 %---- line(boole - th(42),1833351) % 2.25/2.35 fof(subset_intersection,axiom, % 2.25/2.35 ! [B,C] : % 2.25/2.35 ( subset(B,C) % 2.25/2.35 => intersection(B,C) = B ) ). % 2.25/2.35 % 2.25/2.35 %---- line(boole - th(60),1833665) % 2.25/2.35 fof(union_empty_set,axiom, % 2.25/2.35 ! [B] : union(B,empty_set) = B ). % 2.25/2.35 % 2.25/2.35 %---- line(boole - th(70),1833813) % 2.25/2.35 fof(intersection_distributes_over_union,axiom, % 2.25/2.35 ! [B,C,D] : intersection(B,union(C,D)) = union(intersection(B,C),intersection(B,D)) ). % 2.25/2.35 % 2.25/2.35 %---- line(boole - df(2),1833042) % 2.25/2.35 fof(union_defn,axiom, % 2.25/2.35 ! [B,C,D] : % 2.25/2.35 ( member(D,union(B,C)) % 2.25/2.35 <=> ( member(D,B) % 2.25/2.35 | member(D,C) ) ) ). % 2.25/2.35 % 2.25/2.35 %---- line(hidden - axiom228,1832636) % 2.25/2.35 fof(empty_set_defn,axiom, % 2.25/2.35 ! [B] : ~ member(B,empty_set) ). % 2.25/2.35 % 2.25/2.35 %---- line(boole - df(3),1833060) % 2.25/2.35 fof(intersection_defn,axiom, % 2.25/2.35 ! [B,C,D] : % 2.25/2.35 ( member(D,intersection(B,C)) % 2.25/2.35 <=> ( member(D,B) % 2.25/2.35 & member(D,C) ) ) ). % 2.25/2.35 % 2.25/2.35 %---- line(tarski - df(3),1832749) % 2.25/2.35 fof(subset_defn,axiom, % 2.25/2.35 ! [B,C] : % 2.25/2.35 ( subset(B,C) % 2.25/2.35 <=> ! [D] : % 2.25/2.35 ( member(D,B) % 2.25/2.35 => member(D,C) ) ) ). % 2.25/2.35 % 2.25/2.35 %---- line(boole - df(8),1833103) % 2.25/2.35 fof(equal_defn,axiom, % 2.25/2.35 ! [B,C] : % 2.25/2.35 ( B = C % 2.25/2.35 <=> ( subset(B,C) % 2.25/2.35 & subset(C,B) ) ) ). % 2.25/2.35 % 2.25/2.35 %---- property(commutativity,op(union,2,function)) % 2.25/2.35 fof(commutativity_of_union,axiom, % 2.25/2.35 ! [B,C] : union(B,C) = union(C,B) ). % 2.25/2.35 % 2.25/2.35 %---- property(commutativity,op(intersection,2,function)) % 2.25/2.35 fof(commutativity_of_intersection,axiom, % 2.25/2.35 ! [B,C] : intersection(B,C) = intersection(C,B) ). % 2.25/2.35 % 2.25/2.35 %---- property(reflexivity,op(subset,2,predicate)) % 2.25/2.35 fof(reflexivity_of_subset,axiom, % 2.25/2.35 ! [B] : subset(B,B) ). % 2.25/2.35 % 2.25/2.35 %---- line(hidden - axiom230,1832628) % 2.25/2.35 fof(empty_defn,axiom, % 2.25/2.36 ! [B] : % 2.25/2.36 ( empty(B) % 2.25/2.36 <=> ! [C] : ~ member(C,B) ) ). % 2.25/2.36 % 2.25/2.36 %---- line(hidden - axiom231,1832615) % 2.25/2.36 fof(equal_member_defn,axiom, % 2.25/2.36 ! [B,C] : % 2.25/2.36 ( B = C % 2.25/2.36 <=> ! [D] : % 2.25/2.36 ( member(D,B) % 2.25/2.36 <=> member(D,C) ) ) ). % 2.25/2.36 % 2.25/2.36 %---- line(boole - th(120),1834506) % 2.25/2.36 fof(prove_th120,conjecture, % 2.25/2.36 ! [B,C,D] : % 2.25/2.36 ( ( subset(B,union(C,D)) % 2.25/2.36 & intersection(B,D) = empty_set ) % 2.25/2.36 => subset(B,C) ) ). % 2.25/2.36 % 2.25/2.36 %-------------------------------------------------------------------------- % 2.25/2.36 %------------------------------------------- % 2.25/2.36 % Proof found % 2.25/2.36 % SZS status Theorem for theBenchmark % 2.25/2.36 % SZS output start Proof % 2.25/2.36 %ClaNum:44(EqnAxiom:17) % 2.25/2.36 %VarNum:110(SingletonVarNum:50) % 2.25/2.36 %MaxLitNum:3 % 2.25/2.36 %MaxfuncDepth:2 % 2.25/2.36 %SharedTerms:9 % 2.25/2.36 %goalClause: 18 23 26 % 2.25/2.36 %singleGoalClaCount:3 % 2.25/2.36 [26]~P1(a1,a7) % 2.25/2.36 [18]E(f8(a1,a6),a2) % 2.25/2.36 [23]P1(a1,f9(a7,a6)) % 2.25/2.36 [20]P1(x201,x201) % 2.25/2.36 [27]~P2(x271,a2) % 2.25/2.36 [19]E(f9(x191,a2),x191) % 2.25/2.36 [21]E(f8(x211,x212),f8(x212,x211)) % 2.25/2.36 [22]E(f9(x221,x222),f9(x222,x221)) % 2.25/2.36 [24]P1(f8(x241,x242),x241) % 2.25/2.36 [25]E(f9(f8(x251,x252),f8(x251,x253)),f8(x251,f9(x252,x253))) % 2.25/2.36 [30]P3(x301)+P2(f3(x301),x301) % 2.25/2.36 [29]~E(x291,x292)+P1(x291,x292) % 2.25/2.36 [31]~P3(x311)+~P2(x312,x311) % 2.25/2.36 [32]~P1(x321,x322)+E(f8(x321,x322),x321) % 2.25/2.36 [34]P1(x341,x342)+P2(f4(x341,x342),x341) % 2.25/2.36 [40]P1(x401,x402)+~P2(f4(x401,x402),x402) % 2.25/2.36 [36]~P2(x361,x363)+P2(x361,f9(x362,x363)) % 2.25/2.36 [37]~P2(x371,x372)+P2(x371,f9(x372,x373)) % 2.25/2.36 [38]P2(x381,x382)+~P2(x381,f8(x383,x382)) % 2.25/2.36 [39]P2(x391,x392)+~P2(x391,f8(x392,x393)) % 2.25/2.36 [33]~P1(x332,x331)+~P1(x331,x332)+E(x331,x332) % 2.25/2.36 [41]E(x411,x412)+P2(f5(x411,x412),x412)+P2(f5(x411,x412),x411) % 2.25/2.36 [44]E(x441,x442)+~P2(f5(x441,x442),x442)+~P2(f5(x441,x442),x441) % 2.25/2.36 [35]~P2(x351,x353)+P2(x351,x352)+~P1(x353,x352) % 2.25/2.36 [42]~P2(x421,x423)+~P2(x421,x422)+P2(x421,f8(x422,x423)) % 2.25/2.36 [43]P2(x431,x432)+P2(x431,x433)+~P2(x431,f9(x433,x432)) % 2.25/2.36 %EqnAxiom % 2.25/2.36 [1]E(x11,x11) % 2.25/2.36 [2]E(x22,x21)+~E(x21,x22) % 2.25/2.36 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 2.25/2.36 [4]~E(x41,x42)+E(f8(x41,x43),f8(x42,x43)) % 2.25/2.36 [5]~E(x51,x52)+E(f8(x53,x51),f8(x53,x52)) % 2.25/2.36 [6]~E(x61,x62)+E(f9(x61,x63),f9(x62,x63)) % 2.25/2.36 [7]~E(x71,x72)+E(f9(x73,x71),f9(x73,x72)) % 2.25/2.36 [8]~E(x81,x82)+E(f5(x81,x83),f5(x82,x83)) % 2.25/2.36 [9]~E(x91,x92)+E(f5(x93,x91),f5(x93,x92)) % 2.25/2.36 [10]~E(x101,x102)+E(f4(x101,x103),f4(x102,x103)) % 2.25/2.36 [11]~E(x111,x112)+E(f4(x113,x111),f4(x113,x112)) % 2.25/2.36 [12]~E(x121,x122)+E(f3(x121),f3(x122)) % 2.25/2.36 [13]P1(x132,x133)+~E(x131,x132)+~P1(x131,x133) % 2.25/2.36 [14]P1(x143,x142)+~E(x141,x142)+~P1(x143,x141) % 2.25/2.36 [15]P2(x152,x153)+~E(x151,x152)+~P2(x151,x153) % 2.25/2.36 [16]P2(x163,x162)+~E(x161,x162)+~P2(x163,x161) % 2.25/2.36 [17]~P3(x171)+P3(x172)+~E(x171,x172) % 2.25/2.36 % 2.25/2.36 %------------------------------------------- % 2.25/2.36 cnf(48,plain, % 2.25/2.36 (E(a2,f8(a1,a6))), % 2.25/2.36 inference(scs_inference,[],[18,26,29,2])). % 2.25/2.36 cnf(49,plain, % 2.25/2.36 (P3(a2)), % 2.25/2.36 inference(scs_inference,[],[18,26,27,29,2,30])). % 2.25/2.36 cnf(50,plain, % 2.25/2.36 (~P2(x501,a2)), % 2.25/2.36 inference(rename_variables,[],[27])). % 2.25/2.36 cnf(52,plain, % 2.25/2.36 (P1(a2,x521)), % 2.25/2.36 inference(scs_inference,[],[18,26,27,50,29,2,30,34])). % 2.25/2.36 cnf(53,plain, % 2.25/2.36 (~P2(x531,a2)), % 2.25/2.36 inference(rename_variables,[],[27])). % 2.25/2.36 cnf(55,plain, % 2.25/2.36 (E(f8(a6,a1),a2)), % 2.25/2.36 inference(scs_inference,[],[18,26,27,50,21,29,2,30,34,3])). % 2.25/2.36 cnf(61,plain, % 2.25/2.36 (P1(f8(x611,x612),x611)), % 2.25/2.36 inference(rename_variables,[],[24])). % 2.25/2.36 cnf(63,plain, % 2.25/2.36 (~P2(x631,f8(a2,x632))), % 2.25/2.36 inference(scs_inference,[],[18,26,23,20,27,50,53,21,24,61,29,2,30,34,3,13,14,33,35])). % 2.25/2.36 cnf(69,plain, % 2.25/2.36 (P3(f8(a1,a6))), % 2.25/2.36 inference(scs_inference,[],[18,26,23,20,27,50,53,21,24,61,29,2,30,34,3,13,14,33,35,41,17])). % 2.25/2.36 cnf(70,plain, % 2.25/2.36 (~P2(x701,f8(a1,a6))), % 2.25/2.36 inference(scs_inference,[],[18,26,23,20,27,50,53,21,24,61,29,2,30,34,3,13,14,33,35,41,17,31])). % 2.25/2.36 cnf(72,plain, % 2.25/2.36 (~P2(x721,a6)+~P2(x721,a1)), % 2.25/2.36 inference(scs_inference,[],[18,26,23,20,27,50,53,21,24,61,29,2,30,34,3,13,14,33,35,41,17,31,42])). % 2.25/2.36 cnf(74,plain, % 2.25/2.36 (P1(f8(a2,x741),x742)), % 2.25/2.36 inference(scs_inference,[],[63,34])). % 2.25/2.36 cnf(75,plain, % 2.25/2.36 (~P2(x751,f8(a2,x752))), % 2.25/2.36 inference(rename_variables,[],[63])). % 2.25/2.36 cnf(77,plain, % 2.25/2.36 (P3(f8(a2,x771))), % 2.25/2.36 inference(scs_inference,[],[63,75,34,30])). % 2.25/2.36 cnf(78,plain, % 2.25/2.36 (~P2(x781,f8(a2,x782))), % 2.25/2.36 inference(rename_variables,[],[63])). % 2.25/2.36 cnf(80,plain, % 2.25/2.36 (E(a2,f8(a6,a1))), % 2.25/2.36 inference(scs_inference,[],[55,63,75,34,30,2])). % 2.25/2.36 cnf(83,plain, % 2.25/2.36 (~P2(x831,f8(a2,x832))), % 2.25/2.36 inference(rename_variables,[],[63])). % 2.25/2.36 cnf(85,plain, % 2.25/2.36 (P1(f8(f8(a1,a6),x851),a2)), % 2.25/2.36 inference(scs_inference,[],[18,55,63,75,78,70,24,34,30,2,41,14])). % 2.25/2.36 cnf(86,plain, % 2.25/2.36 (P1(f8(x861,x862),x861)), % 2.25/2.36 inference(rename_variables,[],[24])). % 2.25/2.36 cnf(87,plain, % 2.25/2.36 (~P2(x871,f8(f8(a2,x872),x873))), % 2.25/2.36 inference(scs_inference,[],[18,55,63,75,78,83,70,24,86,34,30,2,41,14,35])). % 2.25/2.36 cnf(92,plain, % 2.25/2.36 (E(f9(f8(a6,a1),a2),a2)), % 2.25/2.36 inference(scs_inference,[],[18,55,63,75,78,83,70,69,19,21,24,86,34,30,2,41,14,35,17,3])). % 2.25/2.36 cnf(96,plain, % 2.25/2.36 (~P2(x961,f8(a6,a1))), % 2.25/2.36 inference(scs_inference,[],[18,26,55,63,75,78,83,70,52,69,19,21,24,86,34,30,2,41,14,35,17,3,13,31])). % 2.25/2.36 cnf(100,plain, % 2.25/2.36 (P1(f8(f8(a2,x1001),x1002),x1003)), % 2.25/2.36 inference(scs_inference,[],[87,34])). % 2.25/2.36 cnf(101,plain, % 2.25/2.36 (~P2(x1011,f8(f8(a2,x1012),x1013))), % 2.25/2.36 inference(rename_variables,[],[87])). % 2.25/2.36 cnf(103,plain, % 2.25/2.36 (P3(f8(f8(a2,x1031),x1032))), % 2.25/2.36 inference(scs_inference,[],[87,101,34,30])). % 2.25/2.36 cnf(104,plain, % 2.25/2.36 (~P2(x1041,f8(f8(a2,x1042),x1043))), % 2.25/2.36 inference(rename_variables,[],[87])). % 2.25/2.36 cnf(106,plain, % 2.25/2.36 (E(a2,f9(f8(a6,a1),a2))), % 2.25/2.36 inference(scs_inference,[],[92,87,101,34,30,2])). % 2.25/2.36 cnf(107,plain, % 2.25/2.36 (E(f8(f8(a2,x1071),x1072),f8(a6,a1))), % 2.25/2.36 inference(scs_inference,[],[92,87,101,104,96,34,30,2,41])). % 2.25/2.36 cnf(115,plain, % 2.25/2.36 (E(f8(x1151,x1152),f8(x1152,x1151))), % 2.25/2.36 inference(rename_variables,[],[21])). % 2.25/2.36 cnf(116,plain, % 2.25/2.36 (~P2(x1161,f8(f8(a1,a6),x1162))), % 2.25/2.36 inference(scs_inference,[],[85,92,87,101,104,96,77,27,52,21,34,30,2,41,33,17,35])). % 2.25/2.36 cnf(118,plain, % 2.25/2.36 (E(f9(a2,f8(a6,a1)),a2)), % 2.25/2.36 inference(scs_inference,[],[85,92,87,101,104,96,77,22,27,52,21,34,30,2,41,33,17,35,3])). % 2.25/2.36 cnf(120,plain, % 2.25/2.36 (P1(f8(x1201,f8(a1,a6)),a2)), % 2.25/2.36 inference(scs_inference,[],[85,92,87,101,104,96,77,22,27,52,21,115,34,30,2,41,33,17,35,3,13])). % 2.25/2.36 cnf(123,plain, % 2.25/2.36 (~P2(x1231,f8(x1232,a2))), % 2.25/2.36 inference(scs_inference,[],[85,92,87,101,104,96,77,22,27,52,21,115,34,30,2,41,33,17,35,3,13,31])). % 2.25/2.36 cnf(125,plain, % 2.25/2.36 (P1(f8(x1251,f8(a1,a6)),f8(a1,a6))), % 2.25/2.36 inference(scs_inference,[],[48,85,92,87,101,104,96,77,22,27,52,21,115,34,30,2,41,33,17,35,3,13,31,14])). % 2.25/2.36 cnf(127,plain, % 2.25/2.36 (~P2(x1271,f8(a1,a6))), % 2.25/2.36 inference(rename_variables,[],[70])). % 2.25/2.36 cnf(130,plain, % 2.25/2.36 (~P2(x1301,f8(f8(a1,a6),x1302))), % 2.25/2.36 inference(rename_variables,[],[116])). % 2.25/2.36 cnf(132,plain, % 2.25/2.36 (E(a2,f9(a2,f8(a6,a1)))), % 2.25/2.36 inference(scs_inference,[],[118,70,116,34,30,2])). % 2.25/2.36 cnf(137,plain, % 2.25/2.36 (E(f8(x1371,f8(a1,a6)),f8(a1,a6))), % 2.25/2.36 inference(scs_inference,[],[125,118,63,70,116,130,34,30,2,41,33])). % 2.25/2.36 cnf(139,plain, % 2.25/2.36 (~P2(x1391,f8(x1392,f8(a1,a6)))), % 2.25/2.36 inference(scs_inference,[],[125,118,63,70,127,116,130,34,30,2,41,33,35])). % 2.25/2.36 cnf(143,plain, % 2.25/2.36 (E(f8(a1,a6),f9(f8(a6,a1),a2))), % 2.25/2.36 inference(scs_inference,[],[18,125,120,118,106,63,70,127,116,130,49,34,30,2,41,33,35,14,17,3])). % 2.25/2.36 cnf(144,plain, % 2.25/2.36 (P1(f8(a6,a1),f8(a1,a6))), % 2.25/2.36 inference(scs_inference,[],[18,125,120,118,106,63,70,127,116,130,107,49,34,30,2,41,33,35,14,17,3,13])). % 2.25/2.36 cnf(150,plain, % 2.25/2.36 (~P2(x1501,f8(x1502,a2))), % 2.25/2.36 inference(rename_variables,[],[123])). % 2.25/2.36 cnf(156,plain, % 2.25/2.36 (E(f8(x1561,a2),f8(f8(a2,x1562),x1563))), % 2.25/2.36 inference(scs_inference,[],[143,123,150,87,139,34,30,2,41])). % 2.25/2.36 cnf(158,plain, % 2.25/2.36 (~P2(x1581,f8(x1582,a2))), % 2.25/2.36 inference(rename_variables,[],[123])). % 2.25/2.36 cnf(163,plain, % 2.25/2.36 (~P2(x1631,f8(f8(x1632,a2),x1633))), % 2.25/2.36 inference(scs_inference,[],[143,120,123,150,158,87,139,52,24,34,30,2,41,33,35])). % 2.25/2.36 cnf(168,plain, % 2.25/2.36 (E(f8(a1,a6),f9(a2,f8(a6,a1)))), % 2.25/2.36 inference(scs_inference,[],[18,144,143,132,120,123,150,158,87,139,49,52,24,34,30,2,41,33,35,14,17,3])). % 2.25/2.36 cnf(174,plain, % 2.25/2.36 (P1(f8(a6,a1),x1741)), % 2.25/2.36 inference(scs_inference,[],[96,34])). % 2.25/2.36 cnf(175,plain, % 2.25/2.36 (~P2(x1751,f8(a6,a1))), % 2.25/2.36 inference(rename_variables,[],[96])). % 2.25/2.36 cnf(177,plain, % 2.25/2.36 (P3(f8(f8(x1771,a2),x1772))), % 2.25/2.36 inference(scs_inference,[],[96,163,34,30])). % 2.25/2.36 cnf(181,plain, % 2.25/2.36 (E(f8(a6,a1),f8(a2,x1811))), % 2.25/2.36 inference(scs_inference,[],[168,96,175,63,163,34,30,2,41])). % 2.25/2.36 cnf(183,plain, % 2.25/2.36 (~P2(x1831,f8(a6,a1))), % 2.25/2.36 inference(rename_variables,[],[96])). % 2.25/2.36 cnf(185,plain, % 2.25/2.36 (E(f8(a2,x1851),f8(f8(a2,x1852),x1853))), % 2.25/2.36 inference(scs_inference,[],[168,96,175,63,100,163,74,34,30,2,41,33])). % 2.25/2.36 cnf(187,plain, % 2.25/2.37 (P1(f8(f8(a2,x1871),x1872),x1873)), % 2.25/2.37 inference(rename_variables,[],[100])). % 2.25/2.37 cnf(189,plain, % 2.25/2.37 (~P2(x1891,f8(f8(a6,a1),x1892))), % 2.25/2.37 inference(scs_inference,[],[168,96,175,183,63,100,163,74,24,34,30,2,41,33,35])). % 2.25/2.37 cnf(192,plain, % 2.25/2.37 (P1(f8(x1921,f8(a1,a6)),f8(a6,a1))), % 2.25/2.37 inference(scs_inference,[],[168,80,120,96,175,183,63,100,163,74,24,34,30,2,41,33,35,14])). % 2.25/2.37 cnf(197,plain, % 2.25/2.37 (E(f8(x1971,a2),f8(a1,a6))), % 2.25/2.37 inference(scs_inference,[],[26,168,80,120,96,175,183,63,100,187,163,103,74,156,137,21,24,34,30,2,41,33,35,14,17,13,3])). % 2.25/2.37 cnf(203,plain, % 2.25/2.37 (~P2(x2031,f8(f8(a1,a6),x2032))), % 2.25/2.37 inference(rename_variables,[],[116])). % 2.25/2.37 cnf(214,plain, % 2.25/2.37 (P1(f8(a6,a1),x2141)), % 2.25/2.37 inference(rename_variables,[],[174])). % 2.25/2.37 cnf(224,plain, % 2.25/2.37 (~P2(x2241,a1)+P2(x2241,f9(a7,a6))), % 2.25/2.37 inference(scs_inference,[],[26,23,192,197,70,116,203,189,174,214,177,185,181,21,34,30,2,41,33,17,3,13,31,35])). % 2.25/2.37 cnf(411,plain, % 2.25/2.37 (~P2(f4(a1,a7),a6)), % 2.25/2.37 inference(scs_inference,[],[26,72,34])). % 2.25/2.37 cnf(893,plain, % 2.25/2.37 (~P2(f4(a1,a7),f8(a7,x8931))), % 2.25/2.37 inference(scs_inference,[],[26,39,40])). % 2.25/2.37 cnf(894,plain, % 2.25/2.37 (~P2(f4(a1,a7),x8941)+~P2(f4(a1,a7),a7)), % 2.25/2.37 inference(scs_inference,[],[893,42])). % 2.25/2.37 cnf(900,plain, % 2.25/2.37 (~P2(f4(a1,a7),a7)), % 2.25/2.37 inference(factoring_inference,[],[894])). % 2.25/2.37 cnf(901,plain, % 2.25/2.37 (~P2(f4(a1,a7),a1)), % 2.25/2.37 inference(scs_inference,[],[411,900,224,43])). % 2.25/2.37 cnf(902,plain, % 2.25/2.37 ($false), % 2.25/2.37 inference(scs_inference,[],[26,901,34]), % 2.25/2.37 ['proof']). % 2.25/2.37 % SZS output end Proof % 2.25/2.37 % Total time :1.740000s %------------------------------------------------------------------------------