%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SET617+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 : 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:59 EDT 2024 % Result : Theorem 91.52s 91.63s % Output : CNFRefutation 91.56s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.10 % Problem : SET617+3 : TPTP v8.2.0. Released v2.2.0. % 0.00/0.10 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.10/0.30 % Computer : n028.cluster.edu % 0.10/0.30 % Model : x86_64 x86_64 % 0.10/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.30 % Memory : 8042.1875MB % 0.10/0.30 % OS : Linux 3.10.0-693.el7.x86_64 % 0.10/0.30 % CPULimit : 300 % 0.10/0.30 % WCLimit : 300 % 0.10/0.30 % DateTime : Sun Jun 23 13:46:39 EDT 2024 % 0.10/0.30 % CPUTime : % 0.16/0.53 start to proof:theBenchmark % 91.48/91.61 %------------------------------------------- % 91.48/91.61 % File :CSE---1.7 % 91.48/91.61 % Problem :theBenchmark % 91.48/91.61 % Transform :cnf % 91.48/91.61 % Format :tptp:raw % 91.48/91.61 % Command :java -jar mcs_scs.jar %d %s % 91.48/91.61 % 91.48/91.61 % Result :Theorem 90.970000s % 91.48/91.61 % Output :CNFRefutation 90.970000s % 91.48/91.61 %------------------------------------------- % 91.52/91.63 %-------------------------------------------------------------------------- % 91.52/91.63 % File : SET617+3 : TPTP v8.2.0. Released v2.2.0. % 91.52/91.63 % Domain : Set Theory % 91.52/91.63 % Problem : X sym\ the empty set = X and the empty set sym\ X = X % 91.52/91.63 % Version : [Try90] axioms : Reduced > Incomplete. % 91.52/91.63 % English : The symmetric difference of X and the empty set is X and the % 91.52/91.63 % symmetric difference of the empty set and X is X. % 91.52/91.63 % 91.52/91.63 % Refs : [ILF] The ILF Group (1998), The ILF System: A Tool for the Int % 91.52/91.63 % : [Try90] Trybulec (1990), Tarski Grothendieck Set Theory % 91.52/91.63 % : [TS89] Trybulec & Swieczkowska (1989), Boolean Properties of % 91.52/91.63 % Source : [ILF] % 91.52/91.63 % Names : BOOLE (92) [TS89] % 91.52/91.63 % 91.52/91.63 % Status : Theorem % 91.52/91.63 % Rating : 0.11 v8.2.0, 0.14 v7.5.0, 0.16 v7.4.0, 0.07 v7.1.0, 0.09 v7.0.0, 0.07 v6.4.0, 0.12 v6.3.0, 0.08 v6.2.0, 0.16 v6.1.0, 0.23 v6.0.0, 0.22 v5.5.0, 0.15 v5.4.0, 0.14 v5.3.0, 0.19 v5.2.0, 0.05 v5.0.0, 0.12 v4.1.0, 0.13 v4.0.1, 0.17 v3.7.0, 0.05 v3.4.0, 0.11 v3.3.0, 0.14 v3.2.0, 0.27 v3.1.0, 0.22 v2.7.0, 0.17 v2.6.0, 0.14 v2.5.0, 0.12 v2.4.0, 0.25 v2.3.0, 0.33 v2.2.1 % 91.52/91.63 % Syntax : Number of formulae : 13 ( 8 unt; 0 def) % 91.52/91.63 % Number of atoms : 21 ( 10 equ) % 91.52/91.63 % Maximal formula atoms : 3 ( 1 avg) % 91.52/91.63 % Number of connectives : 10 ( 2 ~; 0 |; 2 &) % 91.52/91.63 % ( 5 <=>; 1 =>; 0 <=; 0 <~>) % 91.52/91.63 % Maximal formula depth : 6 ( 3 avg) % 91.52/91.63 % Maximal term depth : 3 ( 1 avg) % 91.52/91.63 % Number of predicates : 4 ( 3 usr; 0 prp; 1-2 aty) % 91.52/91.63 % Number of functors : 4 ( 4 usr; 1 con; 0-2 aty) % 91.52/91.63 % Number of variables : 22 ( 22 !; 0 ?) % 91.52/91.63 % SPC : FOF_THM_RFO_SEQ % 91.52/91.63 % 91.52/91.63 % Comments : % 91.52/91.63 %-------------------------------------------------------------------------- % 91.52/91.63 %---- line(boole - df(7),1833089) % 91.52/91.63 fof(symmetric_difference_defn,axiom, % 91.52/91.63 ! [B,C] : symmetric_difference(B,C) = union(difference(B,C),difference(C,B)) ). % 91.52/91.63 % 91.52/91.63 %---- line(boole - th(60),1833665) % 91.52/91.63 fof(union_empty_set,axiom, % 91.52/91.63 ! [B] : union(B,empty_set) = B ). % 91.52/91.63 % 91.52/91.63 %---- line(boole - th(74),1833858) % 91.52/91.63 fof(no_difference_with_empty_set1,axiom, % 91.52/91.63 ! [B] : difference(B,empty_set) = B ). % 91.52/91.63 % 91.52/91.63 %---- line(boole - th(75),1833864) % 91.52/91.63 fof(no_difference_with_empty_set2,axiom, % 91.52/91.63 ! [B] : difference(empty_set,B) = empty_set ). % 91.52/91.63 % 91.52/91.63 %---- line(hidden - axiom167,1832636) % 91.52/91.63 fof(empty_set_defn,axiom, % 91.52/91.63 ! [B] : ~ member(B,empty_set) ). % 91.52/91.63 % 91.52/91.63 %---- line(boole - df(8),1833103) % 91.52/91.63 fof(equal_defn,axiom, % 91.52/91.63 ! [B,C] : % 91.52/91.63 ( B = C % 91.52/91.63 <=> ( subset(B,C) % 91.52/91.63 & subset(C,B) ) ) ). % 91.52/91.63 % 91.52/91.63 %---- property(commutativity,op(union,2,function)) % 91.52/91.63 fof(commutativity_of_union,axiom, % 91.52/91.63 ! [B,C] : union(B,C) = union(C,B) ). % 91.52/91.63 % 91.52/91.63 %---- property(commutativity,op(symmetric_difference,2,function)) % 91.52/91.63 fof(commutativity_of_symmetric_difference,axiom, % 91.52/91.63 ! [B,C] : symmetric_difference(B,C) = symmetric_difference(C,B) ). % 91.52/91.63 % 91.52/91.63 %---- line(hidden - axiom168,1832615) % 91.52/91.63 fof(equal_member_defn,axiom, % 91.52/91.63 ! [B,C] : % 91.52/91.63 ( B = C % 91.52/91.63 <=> ! [D] : % 91.52/91.63 ( member(D,B) % 91.52/91.63 <=> member(D,C) ) ) ). % 91.52/91.63 % 91.52/91.63 %---- line(tarski - df(3),1832749) % 91.52/91.63 fof(subset_defn,axiom, % 91.52/91.63 ! [B,C] : % 91.52/91.63 ( subset(B,C) % 91.52/91.63 <=> ! [D] : % 91.52/91.63 ( member(D,B) % 91.52/91.63 => member(D,C) ) ) ). % 91.52/91.63 % 91.52/91.63 %---- property(reflexivity,op(subset,2,predicate)) % 91.52/91.63 fof(reflexivity_of_subset,axiom, % 91.52/91.63 ! [B] : subset(B,B) ). % 91.52/91.63 % 91.52/91.63 %---- line(hidden - axiom170,1832628) % 91.52/91.63 fof(empty_defn,axiom, % 91.52/91.63 ! [B] : % 91.52/91.63 ( empty(B) % 91.52/91.63 <=> ! [C] : ~ member(C,B) ) ). % 91.52/91.63 % 91.52/91.63 %---- line(boole - th(92),1834208) % 91.52/91.63 fof(prove_th92,conjecture, % 91.52/91.63 ! [B] : % 91.52/91.63 ( symmetric_difference(B,empty_set) = B % 91.52/91.63 & symmetric_difference(empty_set,B) = B ) ). % 91.52/91.63 % 91.52/91.63 %-------------------------------------------------------------------------- % 91.52/91.63 %------------------------------------------- % 91.52/91.63 % Proof found % 91.52/91.63 % SZS status Theorem for theBenchmark % 91.52/91.63 % SZS output start Proof % 91.56/91.65 %ClaNum:35(EqnAxiom:17) % 91.56/91.65 %VarNum:60(SingletonVarNum:25) % 91.56/91.65 %MaxLitNum:3 % 91.56/91.65 %MaxfuncDepth:2 % 91.56/91.65 %SharedTerms:11 % 91.56/91.65 %goalClause: 35 % 91.56/91.65 [21]P1(x211,x211) % 91.56/91.65 [24]~P2(x241,a1) % 91.56/91.65 [18]E(f2(a1,x181),a1) % 91.56/91.65 [19]E(f2(x191,a1),x191) % 91.56/91.65 [20]E(f3(x201,a1),x201) % 91.56/91.65 [22]E(f3(x221,x222),f3(x222,x221)) % 91.56/91.65 [35]~E(f3(f2(a1,a7),f2(a7,a1)),a7)+~E(f3(f2(a8,a1),f2(a1,a8)),a8) % 91.56/91.65 [27]P3(x271)+P2(f4(x271),x271) % 91.56/91.65 [26]~E(x261,x262)+P1(x261,x262) % 91.56/91.65 [28]~P3(x281)+~P2(x282,x281) % 91.56/91.65 [30]P1(x301,x302)+P2(f5(x301,x302),x301) % 91.56/91.65 [32]P1(x321,x322)+~P2(f5(x321,x322),x322) % 91.56/91.65 [29]~P1(x292,x291)+~P1(x291,x292)+E(x291,x292) % 91.56/91.65 [33]E(x331,x332)+P2(f6(x331,x332),x332)+P2(f6(x331,x332),x331) % 91.56/91.65 [34]E(x341,x342)+~P2(f6(x341,x342),x342)+~P2(f6(x341,x342),x341) % 91.56/91.65 [31]~P1(x313,x312)+P2(x311,x312)+~P2(x311,x313) % 91.56/91.65 %EqnAxiom % 91.56/91.65 [1]E(x11,x11) % 91.56/91.65 [2]E(x22,x21)+~E(x21,x22) % 91.56/91.65 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 91.56/91.65 [4]~E(x41,x42)+E(f2(x41,x43),f2(x42,x43)) % 91.56/91.65 [5]~E(x51,x52)+E(f2(x53,x51),f2(x53,x52)) % 91.56/91.65 [6]~E(x61,x62)+E(f3(x61,x63),f3(x62,x63)) % 91.56/91.65 [7]~E(x71,x72)+E(f3(x73,x71),f3(x73,x72)) % 91.56/91.65 [8]~E(x81,x82)+E(f6(x81,x83),f6(x82,x83)) % 91.56/91.65 [9]~E(x91,x92)+E(f6(x93,x91),f6(x93,x92)) % 91.56/91.65 [10]~E(x101,x102)+E(f5(x101,x103),f5(x102,x103)) % 91.56/91.65 [11]~E(x111,x112)+E(f5(x113,x111),f5(x113,x112)) % 91.56/91.65 [12]~E(x121,x122)+E(f4(x121),f4(x122)) % 91.56/91.65 [13]P1(x132,x133)+~E(x131,x132)+~P1(x131,x133) % 91.56/91.65 [14]P1(x143,x142)+~E(x141,x142)+~P1(x143,x141) % 91.56/91.65 [15]P2(x152,x153)+~E(x151,x152)+~P2(x151,x153) % 91.56/91.65 [16]P2(x163,x162)+~E(x161,x162)+~P2(x163,x161) % 91.56/91.65 [17]~P3(x171)+P3(x172)+~E(x171,x172) % 91.56/91.65 % 91.56/91.65 %------------------------------------------- % 91.56/91.67 cnf(37,plain, % 91.56/91.67 (E(a1,f2(a1,x371))), % 91.56/91.67 inference(scs_inference,[],[18,2])). % 91.56/91.67 cnf(38,plain, % 91.56/91.67 (P1(a1,x381)), % 91.56/91.67 inference(scs_inference,[],[18,24,2,30])). % 91.56/91.67 cnf(39,plain, % 91.56/91.67 (~P2(x391,a1)), % 91.56/91.67 inference(rename_variables,[],[24])). % 91.56/91.67 cnf(41,plain, % 91.56/91.67 (P3(a1)), % 91.56/91.67 inference(scs_inference,[],[18,24,39,2,30,27])). % 91.56/91.67 cnf(44,plain, % 91.56/91.67 (E(f2(f2(a1,x441),a1),a1)), % 91.56/91.67 inference(scs_inference,[],[18,24,39,19,2,30,27,3])). % 91.56/91.67 cnf(47,plain, % 91.56/91.67 (P3(f2(a1,x471))), % 91.56/91.67 inference(scs_inference,[],[18,24,39,19,2,30,27,3,13,17])). % 91.56/91.67 cnf(48,plain, % 91.56/91.67 (~P2(x481,f2(a1,x482))), % 91.56/91.67 inference(scs_inference,[],[18,24,39,19,2,30,27,3,13,17,28])). % 91.56/91.67 cnf(50,plain, % 91.56/91.67 (E(a1,f2(f2(a1,x501),a1))), % 91.56/91.67 inference(scs_inference,[],[44,2])). % 91.56/91.67 cnf(51,plain, % 91.56/91.67 (P3(f2(f2(a1,x511),a1))), % 91.56/91.67 inference(scs_inference,[],[44,41,2,17])). % 91.56/91.67 cnf(53,plain, % 91.56/91.67 (~P2(x531,f2(f2(a1,x532),a1))), % 91.56/91.67 inference(scs_inference,[],[18,37,44,41,2,17,3,28])). % 91.56/91.67 cnf(57,plain, % 91.56/91.67 (E(x571,f3(x571,a1))), % 91.56/91.67 inference(scs_inference,[],[20,2])). % 91.56/91.67 cnf(58,plain, % 91.56/91.67 (E(f2(a1,x581),f2(f2(a1,x582),a1))), % 91.56/91.67 inference(scs_inference,[],[48,53,20,2,33])). % 91.56/91.67 cnf(62,plain, % 91.56/91.67 (E(f3(a1,x621),x621)), % 91.56/91.67 inference(scs_inference,[],[48,53,22,20,2,33,3])). % 91.56/91.67 cnf(65,plain, % 91.56/91.67 (P3(f3(f2(a1,x651),a1))), % 91.56/91.67 inference(scs_inference,[],[48,53,47,22,20,2,33,3,17])). % 91.56/91.67 cnf(66,plain, % 91.56/91.67 (~P2(x661,f3(f2(a1,x662),a1))), % 91.56/91.67 inference(scs_inference,[],[48,53,47,22,20,2,33,3,17,28])). % 91.56/91.67 cnf(72,plain, % 91.56/91.67 (E(x721,f3(a1,x721))), % 91.56/91.67 inference(scs_inference,[],[62,2])). % 91.56/91.67 cnf(73,plain, % 91.56/91.67 (E(f3(f2(a1,x731),a1),f2(a1,x732))), % 91.56/91.67 inference(scs_inference,[],[62,66,48,2,33])). % 91.56/91.67 cnf(77,plain, % 91.56/91.67 (P1(f3(a1,a1),x771)), % 91.56/91.67 inference(scs_inference,[],[57,62,38,66,48,2,33,13])). % 91.56/91.67 cnf(83,plain, % 91.56/91.67 (~P2(x831,f3(a1,f2(a1,x832)))), % 91.56/91.67 inference(scs_inference,[],[18,57,62,38,66,65,48,22,2,33,13,3,17,28])). % 91.56/91.67 cnf(85,plain, % 91.56/91.67 (E(f2(a1,x851),f3(f2(a1,x852),a1))), % 91.56/91.67 inference(scs_inference,[],[73,2])). % 91.56/91.67 cnf(86,plain, % 91.56/91.67 (E(f3(a1,f2(a1,x861)),f2(f2(a1,x862),a1))), % 91.56/91.67 inference(scs_inference,[],[73,83,53,2,33])). % 91.56/91.67 cnf(91,plain, % 91.56/91.67 (E(x911,f3(a1,x911))), % 91.56/91.67 inference(rename_variables,[],[72])). % 91.56/91.67 cnf(92,plain, % 91.56/91.67 (E(f2(a1,x921),f3(a1,a1))), % 91.56/91.67 inference(scs_inference,[],[18,72,91,73,77,83,53,2,33,13,3])). % 91.56/91.67 cnf(94,plain, % 91.56/91.67 (P3(f3(a1,a1))), % 91.56/91.67 inference(scs_inference,[],[18,72,91,73,77,83,53,47,2,33,13,3,17])). % 91.56/91.67 cnf(95,plain, % 91.56/91.67 (~P2(x951,f3(a1,a1))), % 91.56/91.67 inference(scs_inference,[],[18,72,91,73,77,83,53,47,2,33,13,3,17,28])). % 91.56/91.67 cnf(97,plain, % 91.56/91.67 (E(f3(a1,a1),f2(a1,x971))), % 91.56/91.67 inference(scs_inference,[],[92,2])). % 91.56/91.67 cnf(98,plain, % 91.56/91.67 (E(f3(a1,a1),f3(f2(a1,x981),a1))), % 91.56/91.67 inference(scs_inference,[],[92,95,66,2,33])). % 91.56/91.67 cnf(103,plain, % 91.56/91.67 (E(x1031,f3(x1031,a1))), % 91.56/91.67 inference(rename_variables,[],[57])). % 91.56/91.67 cnf(104,plain, % 91.56/91.67 (P3(f3(f3(a1,a1),a1))), % 91.56/91.67 inference(scs_inference,[],[92,57,103,77,95,94,66,2,33,13,17])). % 91.56/91.67 cnf(106,plain, % 91.56/91.67 (~P2(x1061,f3(f3(a1,a1),a1))), % 91.56/91.67 inference(scs_inference,[],[92,57,103,77,95,94,66,2,33,13,17,28])). % 91.56/91.67 cnf(108,plain, % 91.56/91.67 (E(f3(f2(a1,x1081),a1),f3(a1,a1))), % 91.56/91.67 inference(scs_inference,[],[98,2])). % 91.56/91.67 cnf(109,plain, % 91.56/91.67 (E(f3(f3(a1,a1),a1),f3(a1,f2(a1,x1091)))), % 91.56/91.67 inference(scs_inference,[],[98,106,83,2,33])). % 91.56/91.67 cnf(117,plain, % 91.56/91.67 (~P2(x1171,f3(a1,f3(a1,a1)))), % 91.56/91.67 inference(scs_inference,[],[98,72,106,104,83,22,2,33,3,17,28])). % 91.56/91.67 cnf(119,plain, % 91.56/91.67 (E(f3(a1,f2(a1,x1191)),f3(f3(a1,a1),a1))), % 91.56/91.67 inference(scs_inference,[],[109,2])). % 91.56/91.67 cnf(124,plain, % 91.56/91.67 (E(f3(a1,a1),f3(a1,f2(a1,x1241)))), % 91.56/91.67 inference(scs_inference,[],[109,57,117,24,2,33,3])). % 91.56/91.67 cnf(126,plain, % 91.56/91.67 (E(f3(a1,f2(a1,x1261)),f3(a1,a1))), % 91.56/91.67 inference(scs_inference,[],[124,2])). % 91.56/91.67 cnf(127,plain, % 91.56/91.67 (E(f3(a1,a1),f2(f2(a1,x1271),a1))), % 91.56/91.67 inference(scs_inference,[],[124,95,53,2,33])). % 91.56/91.67 cnf(131,plain, % 91.56/91.67 (E(f3(f2(a1,x1311),a1),f3(a1,f2(a1,x1312)))), % 91.56/91.67 inference(scs_inference,[],[108,124,95,53,2,33,3])). % 91.56/91.67 cnf(133,plain, % 91.56/91.67 (E(f3(a1,f3(a1,a1)),f2(a1,x1331))), % 91.56/91.67 inference(scs_inference,[],[127,117,48,2,33])). % 91.56/91.67 cnf(137,plain, % 91.56/91.67 (E(f3(a1,f2(a1,x1371)),f2(a1,x1372))), % 91.56/91.67 inference(scs_inference,[],[97,126,127,117,48,2,33,3])). % 91.56/91.67 cnf(143,plain, % 91.56/91.67 (E(f3(f2(a1,x1431),a1),f3(f3(a1,a1),a1))), % 91.56/91.67 inference(scs_inference,[],[133,119,131,106,66,2,33,3])). % 91.56/91.67 cnf(148,plain, % 91.56/91.67 (E(f3(f2(a1,x1481),a1),f2(f2(a1,x1482),a1))), % 91.56/91.67 inference(scs_inference,[],[137,86,131,2,3])). % 91.56/91.67 cnf(151,plain, % 91.56/91.67 (E(f2(a1,x1511),f3(f3(a1,a1),a1))), % 91.56/91.67 inference(scs_inference,[],[58,85,143,2,3])). % 91.56/91.67 cnf(153,plain, % 91.56/91.67 (E(f3(f3(a1,a1),a1),f2(a1,x1531))), % 91.56/91.67 inference(scs_inference,[],[151,2])). % 91.56/91.67 cnf(156,plain, % 91.56/91.67 (E(f3(f3(a1,a1),a1),a1)), % 91.56/91.67 inference(scs_inference,[],[18,153,148,2,3])). % 91.56/91.67 cnf(158,plain, % 91.56/91.67 (E(f4(a1),f4(f2(a1,x1581)))), % 91.56/91.67 inference(scs_inference,[],[18,12,2])). % 91.56/91.67 cnf(160,plain, % 91.56/91.67 (E(f3(a1,f4(a1)),f4(f2(a1,x1601)))), % 91.56/91.67 inference(scs_inference,[],[156,62,158,2,3])). % 91.56/91.67 cnf(163,plain, % 91.56/91.67 (E(f4(f2(a1,x1631)),f3(a1,f4(a1)))), % 91.56/91.67 inference(scs_inference,[],[160,2])). % 91.56/91.67 cnf(188,plain, % 91.56/91.67 (P1(f2(x1881,a1),x1881)), % 91.56/91.67 inference(scs_inference,[],[19,21,14])). % 91.56/91.67 cnf(189,plain, % 91.56/91.67 (P1(x1891,x1891)), % 91.56/91.67 inference(rename_variables,[],[21])). % 91.56/91.67 cnf(190,plain, % 91.56/91.67 (P1(x1901,f2(x1901,a1))), % 91.56/91.67 inference(scs_inference,[],[19,21,189,14,13])). % 91.56/91.67 cnf(196,plain, % 91.56/91.67 (~P2(x1961,f2(f3(a1,a1),a1))), % 91.56/91.67 inference(scs_inference,[],[19,21,189,97,47,14,13,3,2,17,28])). % 91.56/91.67 cnf(202,plain, % 91.56/91.67 (P1(f2(f2(x2021,a1),a1),x2021)), % 91.56/91.67 inference(scs_inference,[],[19,188,196,30,14])). % 91.56/91.67 cnf(206,plain, % 91.56/91.67 (E(f2(x2061,a1),f3(a1,x2061))), % 91.56/91.67 inference(scs_inference,[],[19,72,188,190,196,30,14,13,3])). % 91.56/91.67 cnf(222,plain, % 91.56/91.67 (E(f2(x2221,a1),f3(x2221,a1))), % 91.56/91.67 inference(scs_inference,[],[19,57,3])). % 91.56/91.67 cnf(253,plain, % 91.56/91.67 (E(f2(f4(a1),a1),f4(f2(a1,x2531)))), % 91.56/91.67 inference(scs_inference,[],[19,158,3])). % 91.56/91.67 cnf(264,plain, % 91.56/91.67 (P1(f3(x2641,a1),x2641)), % 91.56/91.67 inference(scs_inference,[],[20,21,14])). % 91.56/91.67 cnf(273,plain, % 91.56/91.67 (P1(f2(x2731,a1),x2731)), % 91.56/91.67 inference(rename_variables,[],[188])). % 91.56/91.67 cnf(274,plain, % 91.56/91.67 (P1(f4(f2(a1,x2741)),f4(a1))), % 91.56/91.67 inference(scs_inference,[],[20,253,188,273,14,13])). % 91.56/91.67 cnf(280,plain, % 91.56/91.67 (P1(f4(a1),f4(f2(a1,x2801)))), % 91.56/91.67 inference(scs_inference,[],[253,190,14])). % 91.56/91.67 cnf(296,plain, % 91.56/91.67 (P1(f4(f2(a1,x2961)),f3(a1,f4(a1)))), % 91.56/91.67 inference(scs_inference,[],[72,274,14])). % 91.56/91.67 cnf(298,plain, % 91.56/91.67 (P1(f3(a1,f4(a1)),f4(a1))), % 91.56/91.67 inference(scs_inference,[],[163,72,274,14,13])). % 91.56/91.67 cnf(305,plain, % 91.56/91.67 (P1(f3(f4(a1),a1),f4(f2(a1,x3051)))), % 91.56/91.67 inference(scs_inference,[],[160,57,296,280,14,13])). % 91.56/91.67 cnf(314,plain, % 91.56/91.67 (P1(f3(a1,f4(a1)),f3(f4(a1),a1))), % 91.56/91.67 inference(scs_inference,[],[57,298,14])). % 91.56/91.67 cnf(316,plain, % 91.56/91.67 (E(f3(a1,f2(a1,x3161)),f3(a1,f3(a1,a1)))), % 91.56/91.67 inference(scs_inference,[],[57,298,83,117,14,33])). % 91.56/91.67 cnf(327,plain, % 91.56/91.67 (P1(f3(f4(a1),a1),f4(f2(a1,x3271)))), % 91.56/91.67 inference(rename_variables,[],[305])). % 91.56/91.67 cnf(329,plain, % 91.56/91.67 (E(f3(f2(x3291,a1),a1),f3(a1,x3291))), % 91.56/91.67 inference(scs_inference,[],[20,160,163,206,316,305,314,2,14,13,3])). % 91.56/91.67 cnf(331,plain, % 91.56/91.67 (E(f3(f4(a1),a1),f4(f2(a1,x3311)))), % 91.56/91.67 inference(scs_inference,[],[20,160,163,206,316,305,327,314,2,14,13,3,29])). % 91.56/91.67 cnf(338,plain, % 91.56/91.67 (E(f3(f2(x3381,a1),a1),f3(x3381,a1))), % 91.56/91.67 inference(scs_inference,[],[20,163,222,331,280,2,14,3])). % 91.56/91.67 cnf(343,plain, % 91.56/91.67 (E(f3(a1,x3431),f3(f2(x3431,a1),a1))), % 91.56/91.67 inference(scs_inference,[],[329,2])). % 91.56/91.67 cnf(370,plain, % 91.56/91.67 (E(x3701,f3(f2(x3701,a1),a1))), % 91.56/91.67 inference(scs_inference,[],[20,19,3,2])). % 91.56/91.67 cnf(384,plain, % 91.56/91.67 (P1(f3(a1,x3841),x3841)), % 91.56/91.67 inference(scs_inference,[],[22,188,264,14,13])). % 91.56/91.67 cnf(414,plain, % 91.56/91.67 (P1(f3(a1,f3(x4141,x4142)),f3(x4142,x4141))), % 91.56/91.67 inference(scs_inference,[],[22,384,14])). % 91.56/91.67 cnf(437,plain, % 91.56/91.68 (~E(a7,f3(f2(a1,a7),f2(a7,a1)))+~E(f3(f2(a8,a1),f2(a1,a8)),a8)), % 91.56/91.68 inference(scs_inference,[],[35,2])). % 91.56/91.68 cnf(441,plain, % 91.56/91.68 (~E(a7,f3(f2(a7,a1),f2(a1,a7)))+~E(f3(f2(a8,a1),f2(a1,a8)),a8)), % 91.56/91.68 inference(scs_inference,[],[22,437,3])). % 91.56/91.68 cnf(445,plain, % 91.56/91.68 (~E(f3(f2(a7,a1),f2(a1,a7)),a7)+~E(f3(f2(a8,a1),f2(a1,a8)),a8)), % 91.56/91.68 inference(scs_inference,[],[441,2])). % 91.56/91.68 cnf(449,plain, % 91.56/91.68 (~E(f3(f2(a7,a1),f2(a1,a7)),f3(a1,a7))+~E(f3(f2(a8,a1),f2(a1,a8)),a8)), % 91.56/91.68 inference(scs_inference,[],[62,445,3])). % 91.56/91.68 cnf(453,plain, % 91.56/91.68 (~E(f3(a1,a7),f3(f2(a7,a1),f2(a1,a7)))+~E(f3(f2(a8,a1),f2(a1,a8)),a8)), % 91.56/91.68 inference(scs_inference,[],[449,2])). % 91.56/91.68 cnf(457,plain, % 91.56/91.68 (~E(f3(a1,a7),f3(f2(a1,a7),f2(a7,a1)))+~E(f3(f2(a8,a1),f2(a1,a8)),a8)), % 91.56/91.68 inference(scs_inference,[],[22,453,3])). % 91.56/91.68 cnf(461,plain, % 91.56/91.68 (~E(f3(f2(a1,a7),f2(a7,a1)),f3(a1,a7))+~E(f3(f2(a8,a1),f2(a1,a8)),a8)), % 91.56/91.68 inference(scs_inference,[],[457,2])). % 91.56/91.68 cnf(465,plain, % 91.56/91.68 (~E(f3(f2(a1,a7),f2(a7,a1)),f3(a7,a1))+~E(f3(f2(a8,a1),f2(a1,a8)),a8)), % 91.56/91.68 inference(scs_inference,[],[22,461,3])). % 91.56/91.68 cnf(468,plain, % 91.56/91.68 (E(f3(a1,x4681),f3(a1,f2(x4681,a1)))), % 91.56/91.68 inference(scs_inference,[],[22,329,3,2])). % 91.56/91.68 cnf(473,plain, % 91.56/91.68 (E(f3(a1,f2(x4731,a1)),f3(x4731,a1))), % 91.56/91.68 inference(scs_inference,[],[22,468,3,2])). % 91.56/91.68 cnf(495,plain, % 91.56/91.68 (P1(x4951,f3(f2(x4951,a1),a1))), % 91.56/91.68 inference(scs_inference,[],[57,190,14])). % 91.56/91.68 cnf(502,plain, % 91.56/91.68 (P1(f2(f2(x5021,a1),a1),f3(x5021,a1))), % 91.56/91.68 inference(scs_inference,[],[57,202,14])). % 91.56/91.68 cnf(518,plain, % 91.56/91.68 (E(x5181,f3(x5181,a1))), % 91.56/91.68 inference(rename_variables,[],[57])). % 91.56/91.68 cnf(519,plain, % 91.56/91.68 (P1(f3(x5191,a1),f3(f2(x5191,a1),a1))), % 91.56/91.68 inference(scs_inference,[],[57,518,414,495,14,13])). % 91.56/91.68 cnf(531,plain, % 91.56/91.68 (E(f2(x5311,f3(x5312,a1)),f2(x5311,x5312))), % 91.56/91.68 inference(scs_inference,[],[57,2,5])). % 91.56/91.68 cnf(535,plain, % 91.56/91.68 (E(x5351,f3(x5351,a1))), % 91.56/91.68 inference(rename_variables,[],[57])). % 91.56/91.68 cnf(539,plain, % 91.56/91.68 (~P2(x5391,f2(f2(a1,x5392),f3(a1,a1)))), % 91.56/91.68 inference(scs_inference,[],[57,535,50,531,502,519,51,2,17,14,13,3,28])). % 91.56/91.68 cnf(544,plain, % 91.56/91.68 (E(f3(f3(x5441,a1),x5442),f3(x5441,x5442))), % 91.56/91.68 inference(scs_inference,[],[57,2,6])). % 91.56/91.68 cnf(548,plain, % 91.56/91.68 (E(f3(x5481,x5482),f3(f3(x5481,a1),x5482))), % 91.56/91.68 inference(scs_inference,[],[544,539,30,2])). % 91.56/91.68 cnf(773,plain, % 91.56/91.68 (E(x7731,f3(a1,x7731))), % 91.56/91.68 inference(rename_variables,[],[72])). % 91.56/91.68 cnf(776,plain, % 91.56/91.68 (E(x7761,f3(f3(a1,a1),x7761))), % 91.56/91.68 inference(scs_inference,[],[72,773,548,190,14,13,3])). % 91.56/91.68 cnf(1645,plain, % 91.56/91.68 (E(f3(f2(x16451,a1),a1),f3(f3(a1,a1),f3(x16451,a1)))), % 91.56/91.68 inference(scs_inference,[],[338,776,3])). % 91.56/91.68 cnf(1656,plain, % 91.56/91.68 (E(f3(f3(a1,a1),f3(x16561,a1)),f3(a1,x16561))), % 91.56/91.68 inference(scs_inference,[],[343,1645,3,2])). % 91.56/91.68 cnf(1671,plain, % 91.56/91.68 (E(f2(f2(x16711,a1),x16712),f2(x16711,x16712))), % 91.56/91.68 inference(scs_inference,[],[19,1656,26,12,4])). % 91.56/91.68 cnf(1673,plain, % 91.56/91.68 (E(f3(f2(x16731,a1),x16732),f3(x16731,x16732))), % 91.56/91.68 inference(scs_inference,[],[19,1656,26,12,4,5,6])). % 91.56/91.68 cnf(1690,plain, % 91.56/91.68 (E(f3(x16901,a1),f3(x16901,f2(a1,x16902)))), % 91.56/91.68 inference(scs_inference,[],[1671,37,26,8,6,4,9,10,7])). % 91.56/91.68 cnf(1702,plain, % 91.56/91.68 (E(f3(f2(a1,x17021),x17022),f3(a1,x17022))), % 91.56/91.68 inference(scs_inference,[],[1673,18,26,6])). % 91.56/91.68 cnf(1704,plain, % 91.56/91.68 (E(f6(x17041,f2(a1,x17042)),f6(x17041,a1))), % 91.56/91.68 inference(scs_inference,[],[1673,18,26,6,7,9])). % 91.56/91.68 cnf(2354,plain, % 91.56/91.68 (E(f3(f2(a1,x23541),f2(x23542,a1)),f3(x23542,a1))), % 91.56/91.68 inference(scs_inference,[],[473,1702,1704,26,3])). % 91.56/91.68 cnf(2357,plain, % 91.56/91.68 (~E(a8,f3(f2(a8,a1),f2(a1,a8)))), % 91.56/91.68 inference(scs_inference,[],[473,1702,1704,26,3,465,2])). % 91.56/91.68 cnf(2365,plain, % 91.56/91.68 ($false), % 91.56/91.68 inference(scs_inference,[],[2354,2357,370,1690,26,3]), % 91.56/91.68 ['proof']). % 91.56/91.68 % SZS output end Proof % 91.56/91.68 % Total time :90.970000s %------------------------------------------------------------------------------