%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SET173+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 : n025.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:00 EDT 2024 % Result : Theorem 232.41s 232.61s % Output : CNFRefutation 232.54s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.13 % Problem : SET173+3 : TPTP v8.2.0. Released v2.2.0. % 0.03/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.34 % Computer : n025.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Sun Jun 23 18:00:39 EDT 2024 % 0.12/0.34 % CPUTime : % 0.53/0.57 start to proof:theBenchmark % 232.36/232.58 %------------------------------------------- % 232.36/232.58 % File :CSE---1.7 % 232.36/232.58 % Problem :theBenchmark % 232.36/232.58 % Transform :cnf % 232.36/232.58 % Format :tptp:raw % 232.36/232.58 % Command :java -jar mcs_scs.jar %d %s % 232.36/232.58 % 232.36/232.58 % Result :Theorem 231.720000s % 232.36/232.58 % Output :CNFRefutation 231.720000s % 232.36/232.58 %------------------------------------------- % 232.41/232.61 %-------------------------------------------------------------------------- % 232.41/232.61 % File : SET173+3 : TPTP v8.2.0. Released v2.2.0. % 232.41/232.61 % Domain : Set Theory % 232.41/232.61 % Problem : Absorbtion for intersection % 232.41/232.61 % Version : [Try90] axioms : Reduced > Incomplete. % 232.41/232.61 % English : The intersection of X and the union of X and Y is X. % 232.41/232.61 % 232.41/232.61 % Refs : [ILF] The ILF Group (1998), The ILF System: A Tool for the Int % 232.41/232.61 % : [Try90] Trybulec (1990), Tarski Grothendieck Set Theory % 232.41/232.61 % : [TS89] Trybulec & Swieczkowska (1989), Boolean Properties of % 232.41/232.61 % Source : [ILF] % 232.41/232.61 % Names : BOOLE (68) [TS89] % 232.41/232.61 % 232.41/232.61 % Status : Theorem % 232.41/232.61 % Rating : 0.19 v8.1.0, 0.14 v7.5.0, 0.16 v7.4.0, 0.13 v7.3.0, 0.17 v7.2.0, 0.14 v7.1.0, 0.13 v7.0.0, 0.17 v6.4.0, 0.15 v6.3.0, 0.17 v6.2.0, 0.16 v6.1.0, 0.27 v6.0.0, 0.30 v5.5.0, 0.26 v5.4.0, 0.36 v5.3.0, 0.37 v5.2.0, 0.20 v5.1.0, 0.19 v5.0.0, 0.29 v4.1.0, 0.26 v4.0.0, 0.25 v3.7.0, 0.20 v3.5.0, 0.21 v3.2.0, 0.18 v3.1.0, 0.22 v2.7.0, 0.00 v2.6.0, 0.14 v2.5.0, 0.12 v2.4.0, 0.00 v2.2.1 % 232.41/232.61 % Syntax : Number of formulae : 9 ( 4 unt; 0 def) % 232.41/232.61 % Number of atoms : 19 ( 5 equ) % 232.41/232.61 % Maximal formula atoms : 3 ( 2 avg) % 232.41/232.61 % Number of connectives : 10 ( 0 ~; 1 |; 2 &) % 232.41/232.61 % ( 6 <=>; 1 =>; 0 <=; 0 <~>) % 232.41/232.61 % Maximal formula depth : 6 ( 4 avg) % 232.41/232.61 % Maximal term depth : 3 ( 1 avg) % 232.41/232.61 % Number of predicates : 3 ( 2 usr; 0 prp; 2-2 aty) % 232.41/232.61 % Number of functors : 2 ( 2 usr; 0 con; 2-2 aty) % 232.41/232.61 % Number of variables : 21 ( 21 !; 0 ?) % 232.41/232.61 % SPC : FOF_THM_RFO_SEQ % 232.41/232.61 % 232.41/232.61 % Comments : % 232.41/232.61 %-------------------------------------------------------------------------- % 232.41/232.61 %---- line(boole - df(2),1833042) % 232.41/232.61 fof(union_defn,axiom, % 232.41/232.61 ! [B,C,D] : % 232.41/232.61 ( member(D,union(B,C)) % 232.41/232.61 <=> ( member(D,B) % 232.41/232.61 | member(D,C) ) ) ). % 232.41/232.61 % 232.41/232.61 %---- line(boole - df(3),1833060) % 232.41/232.61 fof(intersection_defn,axiom, % 232.41/232.61 ! [B,C,D] : % 232.41/232.61 ( member(D,intersection(B,C)) % 232.41/232.61 <=> ( member(D,B) % 232.41/232.61 & member(D,C) ) ) ). % 232.41/232.61 % 232.41/232.61 %---- line(boole - df(8),1833103) % 232.41/232.61 fof(equal_defn,axiom, % 232.41/232.61 ! [B,C] : % 232.41/232.61 ( B = C % 232.41/232.61 <=> ( subset(B,C) % 232.41/232.61 & subset(C,B) ) ) ). % 232.41/232.61 % 232.41/232.61 %---- property(commutativity,op(union,2,function)) % 232.41/232.61 fof(commutativity_of_union,axiom, % 232.41/232.61 ! [B,C] : union(B,C) = union(C,B) ). % 232.41/232.61 % 232.41/232.61 %---- property(commutativity,op(intersection,2,function)) % 232.41/232.61 fof(commutativity_of_intersection,axiom, % 232.41/232.61 ! [B,C] : intersection(B,C) = intersection(C,B) ). % 232.41/232.61 % 232.41/232.61 %---- line(tarski - df(3),1832749) % 232.41/232.61 fof(subset_defn,axiom, % 232.41/232.61 ! [B,C] : % 232.41/232.61 ( subset(B,C) % 232.41/232.61 <=> ! [D] : % 232.41/232.61 ( member(D,B) % 232.41/232.61 => member(D,C) ) ) ). % 232.41/232.61 % 232.41/232.61 %---- property(reflexivity,op(subset,2,predicate)) % 232.41/232.61 fof(reflexivity_of_subset,axiom, % 232.41/232.61 ! [B] : subset(B,B) ). % 232.41/232.61 % 232.41/232.61 %---- line(hidden - axiom110,1832615) % 232.41/232.61 fof(equal_member_defn,axiom, % 232.41/232.61 ! [B,C] : % 232.41/232.61 ( B = C % 232.41/232.61 <=> ! [D] : % 232.41/232.61 ( member(D,B) % 232.41/232.61 <=> member(D,C) ) ) ). % 232.41/232.61 % 232.41/232.61 %---- line(boole - th(68),1833762) % 232.41/232.61 fof(prove_absorbtion_for_intersection,conjecture, % 232.41/232.61 ! [B,C] : intersection(B,union(B,C)) = B ). % 232.41/232.61 % 232.41/232.61 %-------------------------------------------------------------------------- % 232.41/232.61 %------------------------------------------- % 232.41/232.61 % Proof found % 232.41/232.61 % SZS status Theorem for theBenchmark % 232.41/232.61 % SZS output start Proof % 232.41/232.64 %ClaNum:33(EqnAxiom:15) % 232.41/232.64 %VarNum:86(SingletonVarNum:38) % 232.41/232.64 %MaxLitNum:3 % 232.41/232.64 %MaxfuncDepth:2 % 232.41/232.64 %SharedTerms:5 % 232.41/232.64 %goalClause: 19 % 232.41/232.64 %singleGoalClaCount:1 % 232.41/232.64 [19]~E(f2(a3,f1(a3,a6)),a3) % 232.41/232.64 [16]P1(x161,x161) % 232.41/232.64 [17]E(f1(x171,x172),f1(x172,x171)) % 232.41/232.64 [18]E(f2(x181,x182),f2(x182,x181)) % 232.41/232.64 [21]~E(x211,x212)+P1(x211,x212) % 232.41/232.64 [23]P1(x231,x232)+P2(f4(x231,x232),x231) % 232.41/232.64 [29]P1(x291,x292)+~P2(f4(x291,x292),x292) % 232.41/232.64 [25]~P2(x251,x253)+P2(x251,f1(x252,x253)) % 232.41/232.64 [26]~P2(x261,x262)+P2(x261,f1(x262,x263)) % 232.41/232.64 [27]P2(x271,x272)+~P2(x271,f2(x273,x272)) % 232.41/232.64 [28]P2(x281,x282)+~P2(x281,f2(x282,x283)) % 232.41/232.64 [22]~P1(x222,x221)+~P1(x221,x222)+E(x221,x222) % 232.41/232.64 [30]E(x301,x302)+P2(f5(x301,x302),x302)+P2(f5(x301,x302),x301) % 232.41/232.64 [33]E(x331,x332)+~P2(f5(x331,x332),x332)+~P2(f5(x331,x332),x331) % 232.41/232.64 [24]~P1(x243,x242)+P2(x241,x242)+~P2(x241,x243) % 232.41/232.64 [31]~P2(x311,x313)+~P2(x311,x312)+P2(x311,f2(x312,x313)) % 232.41/232.64 [32]P2(x321,x322)+P2(x321,x323)+~P2(x321,f1(x323,x322)) % 232.41/232.64 %EqnAxiom % 232.41/232.64 [1]E(x11,x11) % 232.41/232.64 [2]E(x22,x21)+~E(x21,x22) % 232.41/232.64 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 232.41/232.64 [4]~E(x41,x42)+E(f1(x41,x43),f1(x42,x43)) % 232.41/232.64 [5]~E(x51,x52)+E(f1(x53,x51),f1(x53,x52)) % 232.41/232.64 [6]~E(x61,x62)+E(f5(x61,x63),f5(x62,x63)) % 232.41/232.64 [7]~E(x71,x72)+E(f5(x73,x71),f5(x73,x72)) % 232.41/232.64 [8]~E(x81,x82)+E(f2(x81,x83),f2(x82,x83)) % 232.41/232.64 [9]~E(x91,x92)+E(f2(x93,x91),f2(x93,x92)) % 232.41/232.64 [10]~E(x101,x102)+E(f4(x101,x103),f4(x102,x103)) % 232.41/232.64 [11]~E(x111,x112)+E(f4(x113,x111),f4(x113,x112)) % 232.41/232.64 [12]P1(x122,x123)+~E(x121,x122)+~P1(x121,x123) % 232.41/232.64 [13]P1(x133,x132)+~E(x131,x132)+~P1(x133,x131) % 232.41/232.64 [14]P2(x142,x143)+~E(x141,x142)+~P2(x141,x143) % 232.41/232.64 [15]P2(x153,x152)+~E(x151,x152)+~P2(x153,x151) % 232.41/232.64 % 232.41/232.64 %------------------------------------------- % 232.50/232.68 cnf(35,plain, % 232.50/232.68 (P1(f1(x351,x352),f1(x352,x351))), % 232.50/232.68 inference(scs_inference,[],[16,17,12])). % 232.50/232.68 cnf(37,plain, % 232.50/232.68 (P1(f2(x371,x372),f2(x372,x371))), % 232.50/232.68 inference(scs_inference,[],[18,16,13])). % 232.50/232.68 cnf(39,plain, % 232.50/232.68 (E(f1(f1(x391,x392),x393),f1(f1(x392,x391),x393))), % 232.50/232.68 inference(scs_inference,[],[17,2,4])). % 232.50/232.68 cnf(40,plain, % 232.50/232.68 (P1(f1(f1(x401,x402),x403),f1(f1(x402,x401),x403))), % 232.50/232.68 inference(scs_inference,[],[16,39,13])). % 232.50/232.68 cnf(42,plain, % 232.50/232.68 (P1(f1(f1(x421,x422),x423),f1(x423,f1(x422,x421)))), % 232.50/232.68 inference(scs_inference,[],[16,39,35,13,12])). % 232.50/232.68 cnf(45,plain, % 232.50/232.68 (P1(f1(f1(x451,x452),f1(x453,x454)),f1(f1(x454,x453),f1(x452,x451)))), % 232.50/232.68 inference(scs_inference,[],[39,42,13])). % 232.50/232.68 cnf(50,plain, % 232.50/232.68 (~P2(x501,x502)+P2(x501,f1(x503,f1(x502,x504)))), % 232.50/232.68 inference(scs_inference,[],[25,26])). % 232.50/232.68 cnf(51,plain, % 232.50/232.68 (P1(f1(x511,f1(x512,x513)),f1(f1(x513,x512),x511))), % 232.50/232.68 inference(scs_inference,[],[39,35,13])). % 232.50/232.68 cnf(53,plain, % 232.50/232.68 (P2(x531,x532)+~P2(x531,f2(x533,f2(x532,x534)))), % 232.50/232.68 inference(scs_inference,[],[27,28])). % 232.50/232.68 cnf(56,plain, % 232.50/232.68 (E(f1(x561,x562),f1(x562,x561))), % 232.50/232.68 inference(rename_variables,[],[17])). % 232.50/232.68 cnf(57,plain, % 232.50/232.68 (P1(f1(x571,f1(x572,x573)),f1(x571,f1(x573,x572)))), % 232.50/232.68 inference(scs_inference,[],[17,56,45,51,12,13])). % 232.50/232.68 cnf(64,plain, % 232.50/232.68 (P2(x641,f1(x642,f1(x643,x644)))+~P2(x641,f2(x645,f2(x643,x646)))), % 232.50/232.68 inference(scs_inference,[],[50,53])). % 232.50/232.68 cnf(69,plain, % 232.50/232.68 (~E(a3,f2(f1(a3,a6),a3))), % 232.50/232.68 inference(scs_inference,[],[19,18,3,2])). % 232.50/232.68 cnf(70,plain, % 232.50/232.68 (~E(a3,f2(a3,f1(a3,a6)))), % 232.50/232.68 inference(scs_inference,[],[69,18,3])). % 232.50/232.68 cnf(95,plain, % 232.50/232.68 (E(f1(x951,f1(x952,x953)),f1(x951,f1(x953,x952)))), % 232.50/232.68 inference(scs_inference,[],[17,2,5])). % 232.50/232.68 cnf(96,plain, % 232.50/232.68 (E(f1(f2(x961,x962),x963),f1(f2(x962,x961),x963))), % 232.50/232.68 inference(scs_inference,[],[18,2,4])). % 232.50/232.68 cnf(99,plain, % 232.50/232.68 (E(f1(f2(x991,x992),x993),f1(f2(x992,x991),x993))), % 232.50/232.68 inference(rename_variables,[],[96])). % 232.50/232.68 cnf(100,plain, % 232.50/232.68 (P1(f1(x1001,f2(x1002,x1003)),f1(f2(x1003,x1002),x1001))), % 232.50/232.68 inference(scs_inference,[],[96,99,57,35,12,13])). % 232.50/232.68 cnf(102,plain, % 232.50/232.68 (E(f5(f2(x1021,x1022),x1023),f5(f2(x1022,x1021),x1023))), % 232.50/232.68 inference(scs_inference,[],[18,2,6])). % 232.50/232.68 cnf(103,plain, % 232.50/232.68 (P1(f1(f2(x1031,x1032),f2(x1033,x1034)),f1(f2(x1034,x1033),f2(x1032,x1031)))), % 232.50/232.68 inference(scs_inference,[],[96,100,12])). % 232.50/232.68 cnf(105,plain, % 232.50/232.68 (E(f1(f2(x1051,x1052),x1053),f1(f2(x1052,x1051),x1053))), % 232.50/232.68 inference(rename_variables,[],[96])). % 232.50/232.68 cnf(106,plain, % 232.50/232.68 (P1(f1(f1(x1061,x1062),f2(x1063,x1064)),f1(f2(x1064,x1063),f1(x1062,x1061)))), % 232.50/232.68 inference(scs_inference,[],[96,105,100,42,12,13])). % 232.50/232.68 cnf(113,plain, % 232.50/232.68 (E(f5(x1131,f2(x1132,x1133)),f5(x1131,f2(x1133,x1132)))), % 232.50/232.68 inference(scs_inference,[],[18,2,7])). % 232.50/232.68 cnf(117,plain, % 232.50/232.68 (E(f2(f2(x1171,x1172),x1173),f2(f2(x1172,x1171),x1173))), % 232.50/232.68 inference(scs_inference,[],[18,2,8])). % 232.50/232.68 cnf(119,plain, % 232.50/232.68 (P1(f2(f2(x1191,x1192),x1193),f2(x1193,f2(x1192,x1191)))), % 232.50/232.68 inference(scs_inference,[],[37,117,12])). % 232.50/232.68 cnf(120,plain, % 232.50/232.68 (P1(f2(x1201,x1202),f2(x1202,x1201))), % 232.50/232.68 inference(rename_variables,[],[37])). % 232.50/232.68 cnf(121,plain, % 232.50/232.68 (P1(f2(x1211,f2(x1212,x1213)),f2(f2(x1213,x1212),x1211))), % 232.50/232.68 inference(scs_inference,[],[37,120,117,12,13])). % 232.50/232.68 cnf(141,plain, % 232.50/232.68 (E(f1(f2(x1411,x1412),x1413),f1(f2(x1412,x1411),x1413))), % 232.50/232.68 inference(rename_variables,[],[96])). % 232.50/232.68 cnf(144,plain, % 232.50/232.68 (E(f1(f2(x1441,x1442),f1(x1443,x1444)),f1(f1(x1444,x1443),f2(x1442,x1441)))), % 232.50/232.68 inference(scs_inference,[],[96,141,106,51,16,12,13,22])). % 232.50/232.68 cnf(146,plain, % 232.50/232.68 (E(f1(f2(x1461,x1462),f1(x1463,x1464)),f1(f1(x1464,x1463),f2(x1461,x1462)))), % 232.50/232.68 inference(scs_inference,[],[96,141,106,51,16,12,13,22,3])). % 232.50/232.68 cnf(148,plain, % 232.50/232.68 (E(f1(f1(x1481,x1482),f2(x1483,x1484)),f1(f2(x1484,x1483),f1(x1482,x1481)))), % 232.50/232.68 inference(scs_inference,[],[96,141,106,51,16,12,13,22,3,2])). % 232.50/232.68 cnf(150,plain, % 232.50/232.68 (E(f1(f1(x1501,x1502),f2(x1503,x1504)),f1(f2(x1503,x1504),f1(x1502,x1501)))), % 232.50/232.68 inference(scs_inference,[],[146,2])). % 232.50/232.68 cnf(152,plain, % 232.50/232.68 (E(f1(f2(x1521,x1522),f1(x1523,x1524)),f1(f1(x1524,x1523),f2(x1521,x1522)))), % 232.50/232.68 inference(rename_variables,[],[146])). % 232.50/232.68 cnf(156,plain, % 232.50/232.68 (P1(f1(x1561,f2(x1562,x1563)),f1(f2(x1563,x1562),x1561))), % 232.50/232.68 inference(rename_variables,[],[100])). % 232.50/232.68 cnf(157,plain, % 232.50/232.68 (E(f1(f2(x1571,x1572),f1(x1573,x1574)),f1(f1(x1573,x1574),f2(x1572,x1571)))), % 232.50/232.68 inference(scs_inference,[],[146,152,148,40,100,156,2,3,12,13,22])). % 232.50/232.68 cnf(160,plain, % 232.50/232.68 (E(f4(x1601,f1(f2(x1602,x1603),f1(x1604,x1605))),f4(x1601,f1(f1(x1605,x1604),f2(x1602,x1603))))), % 232.50/232.68 inference(scs_inference,[],[150,2,11])). % 232.50/232.68 cnf(161,plain, % 232.50/232.68 (E(f1(f1(x1611,x1612),f2(x1613,x1614)),f1(f2(x1614,x1613),f1(x1611,x1612)))), % 232.50/232.68 inference(scs_inference,[],[157,2])). % 232.50/232.68 cnf(162,plain, % 232.50/232.68 (E(f1(f1(x1621,x1622),f2(x1623,x1624)),f1(f1(x1622,x1621),f2(x1624,x1623)))), % 232.50/232.68 inference(scs_inference,[],[157,150,2,3])). % 232.50/232.68 cnf(166,plain, % 232.50/232.68 (E(f1(f1(f2(x1661,x1662),f1(x1663,x1664)),x1665),f1(f1(f1(x1663,x1664),f2(x1662,x1661)),x1665))), % 232.50/232.68 inference(scs_inference,[],[161,2,4])). % 232.50/232.68 cnf(173,plain, % 232.50/232.68 (E(f2(x1731,f1(f1(x1732,x1733),f2(x1734,x1735))),f2(x1731,f1(f2(x1735,x1734),f1(x1733,x1732))))), % 232.50/232.68 inference(scs_inference,[],[144,2,9])). % 232.50/232.68 cnf(180,plain, % 232.50/232.68 (E(f1(x1801,f1(f2(x1802,x1803),f1(x1804,x1805))),f1(x1801,f1(f1(x1804,x1805),f2(x1803,x1802))))), % 232.50/232.68 inference(scs_inference,[],[161,2,5])). % 232.50/232.68 cnf(183,plain, % 232.50/232.68 (P1(f2(f2(x1831,x1832),x1833),f2(f2(x1832,x1831),x1833))), % 232.50/232.68 inference(scs_inference,[],[117,16,12])). % 232.50/232.68 cnf(186,plain, % 232.50/232.68 (E(f5(x1861,f1(f1(x1862,x1863),f2(x1864,x1865))),f5(x1861,f1(f1(x1863,x1862),f2(x1865,x1864))))), % 232.50/232.68 inference(scs_inference,[],[162,2,7])). % 232.50/232.68 cnf(187,plain, % 232.50/232.68 (E(f4(x1871,f1(f1(x1872,x1873),f2(x1874,x1875))),f4(x1871,f1(f2(x1875,x1874),f1(x1873,x1872))))), % 232.50/232.68 inference(scs_inference,[],[144,2,11])). % 232.50/232.68 cnf(188,plain, % 232.50/232.68 (E(f1(f2(x1881,x1882),f1(x1883,x1884)),f1(f2(x1882,x1881),f1(x1884,x1883)))), % 232.50/232.68 inference(scs_inference,[],[146,161,3])). % 232.50/232.68 cnf(192,plain, % 232.50/232.68 (E(f1(f1(f2(x1921,x1922),f1(x1923,x1924)),x1925),f1(f1(f1(x1924,x1923),f2(x1922,x1921)),x1925))), % 232.50/232.68 inference(scs_inference,[],[148,2,4])). % 232.50/232.68 cnf(193,plain, % 232.50/232.68 (E(f1(x1931,f1(f2(x1932,x1933),f1(x1934,x1935))),f1(x1931,f1(f1(x1935,x1934),f2(x1932,x1933))))), % 232.50/232.68 inference(scs_inference,[],[150,2,5])). % 232.50/232.68 cnf(195,plain, % 232.50/232.68 (E(f5(x1951,f1(f1(x1952,x1953),f2(x1954,x1955))),f5(x1951,f1(f2(x1955,x1954),f1(x1953,x1952))))), % 232.50/232.68 inference(scs_inference,[],[144,2,7])). % 232.50/232.68 cnf(196,plain, % 232.50/232.68 (E(f2(f1(f1(x1961,x1962),f2(x1963,x1964)),x1965),f2(f1(f2(x1963,x1964),f1(x1962,x1961)),x1965))), % 232.50/232.68 inference(scs_inference,[],[146,2,8])). % 232.50/232.68 cnf(197,plain, % 232.50/232.68 (E(f2(x1971,f1(f2(x1972,x1973),f1(x1974,x1975))),f2(x1971,f1(f1(x1975,x1974),f2(x1973,x1972))))), % 232.50/232.68 inference(scs_inference,[],[148,2,9])). % 232.50/232.68 cnf(202,plain, % 232.50/232.68 (E(f5(f1(f2(x2021,x2022),f1(x2023,x2024)),x2025),f5(f1(f1(x2023,x2024),f2(x2022,x2021)),x2025))), % 232.50/232.68 inference(scs_inference,[],[161,2,6])). % 232.50/232.68 cnf(208,plain, % 232.50/232.68 (E(f1(f1(f1(x2081,x2082),f2(x2083,x2084)),x2085),f1(f1(f2(x2084,x2083),f1(x2082,x2081)),x2085))), % 232.50/232.68 inference(scs_inference,[],[144,2,4])). % 232.50/232.68 cnf(210,plain, % 232.50/232.68 (E(f5(f1(f1(x2101,x2102),f2(x2103,x2104)),x2105),f5(f1(f2(x2103,x2104),f1(x2102,x2101)),x2105))), % 232.50/232.68 inference(scs_inference,[],[146,2,6])). % 232.50/232.68 cnf(212,plain, % 232.50/232.68 (E(f2(f1(x2121,x2122),x2123),f2(f1(x2122,x2121),x2123))), % 232.50/232.68 inference(scs_inference,[],[17,2,8])). % 232.50/232.68 cnf(214,plain, % 232.50/232.68 (E(f2(f1(x2141,x2142),x2143),f2(f1(x2142,x2141),x2143))), % 232.50/232.68 inference(rename_variables,[],[212])). % 232.50/232.68 cnf(215,plain, % 232.50/232.68 (P1(f2(f2(x2151,x2152),f1(x2153,x2154)),f2(f1(x2154,x2153),f2(x2152,x2151)))), % 232.50/232.68 inference(scs_inference,[],[212,214,69,119,3,13])). % 232.50/232.68 cnf(221,plain, % 232.50/232.68 (E(f2(x2211,f1(x2212,x2213)),f2(x2211,f1(x2213,x2212)))), % 232.50/232.68 inference(scs_inference,[],[17,2,9])). % 232.50/232.68 cnf(223,plain, % 232.50/232.68 (E(f2(x2231,f1(x2232,x2233)),f2(x2231,f1(x2233,x2232)))), % 232.50/232.68 inference(rename_variables,[],[221])). % 232.50/232.68 cnf(224,plain, % 232.50/232.68 (P1(f2(f2(x2241,x2242),f1(x2243,x2244)),f2(f2(x2242,x2241),f1(x2244,x2243)))), % 232.50/232.68 inference(scs_inference,[],[183,221,223,70,3,12])). % 232.50/232.68 cnf(227,plain, % 232.50/232.68 (P1(f2(x2271,f1(x2272,x2273)),f2(f1(x2273,x2272),x2271))), % 232.50/232.68 inference(scs_inference,[],[212,183,221,223,37,70,3,12,13])). % 232.50/232.68 cnf(229,plain, % 232.50/232.68 (E(f4(f1(x2291,x2292),x2293),f4(f1(x2292,x2291),x2293))), % 232.50/232.68 inference(scs_inference,[],[17,2,10])). % 232.50/232.68 cnf(236,plain, % 232.50/232.68 (P1(f2(f1(x2361,x2362),f1(x2363,x2364)),f2(f1(x2364,x2363),f1(x2362,x2361)))), % 232.50/232.68 inference(scs_inference,[],[17,212,215,227,103,121,22,13,12])). % 232.50/232.68 cnf(240,plain, % 232.50/232.68 (E(f4(x2401,f1(x2402,x2403)),f4(x2401,f1(x2403,x2402)))), % 232.50/232.68 inference(scs_inference,[],[17,2,11])). % 232.50/232.68 cnf(246,plain, % 232.50/232.68 (E(f5(f1(x2461,x2462),x2463),f5(f1(x2462,x2461),x2463))), % 232.50/232.68 inference(scs_inference,[],[17,2,6])). % 232.50/232.68 cnf(250,plain, % 232.50/232.68 (E(f5(x2501,f1(x2502,x2503)),f5(x2501,f1(x2503,x2502)))), % 232.50/232.68 inference(scs_inference,[],[17,2,7])). % 232.50/232.68 cnf(251,plain, % 232.50/232.68 (E(f1(x2511,f2(x2512,x2513)),f1(x2511,f2(x2513,x2512)))), % 232.50/232.68 inference(scs_inference,[],[18,2,5])). % 232.50/232.68 cnf(258,plain, % 232.50/232.68 (E(f2(x2581,f2(x2582,x2583)),f2(x2581,f2(x2583,x2582)))), % 232.50/232.68 inference(scs_inference,[],[18,2,9])). % 232.50/232.68 cnf(260,plain, % 232.50/232.68 (E(f2(x2601,x2602),f2(x2602,x2601))), % 232.50/232.68 inference(rename_variables,[],[18])). % 232.50/232.68 cnf(261,plain, % 232.50/232.68 (P1(f2(f1(x2611,x2612),f2(x2613,x2614)),f2(f2(x2614,x2613),f1(x2612,x2611)))), % 232.50/232.68 inference(scs_inference,[],[18,260,224,236,13,12])). % 232.50/232.68 cnf(263,plain, % 232.50/232.68 (E(f4(f2(x2631,x2632),x2633),f4(f2(x2632,x2631),x2633))), % 232.50/232.68 inference(scs_inference,[],[18,2,10])). % 232.50/232.68 cnf(264,plain, % 232.50/232.68 (E(f2(f2(x2641,x2642),f1(x2643,x2644)),f2(f1(x2644,x2643),f2(x2642,x2641)))), % 232.50/232.68 inference(scs_inference,[],[261,215,22])). % 232.50/232.68 cnf(267,plain, % 232.50/232.68 (E(f2(f1(x2671,x2672),f2(x2673,x2674)),f2(f1(x2672,x2671),f2(x2674,x2673)))), % 232.50/232.68 inference(scs_inference,[],[18,261,215,22,3])). % 232.50/232.68 cnf(268,plain, % 232.50/232.68 (E(f2(x2681,x2682),f2(x2682,x2681))), % 232.50/232.68 inference(rename_variables,[],[18])). % 232.50/232.68 cnf(270,plain, % 232.50/232.68 (E(f2(x2701,x2702),f2(x2702,x2701))), % 232.50/232.68 inference(rename_variables,[],[18])). % 232.50/232.68 cnf(274,plain, % 232.50/232.68 (E(f2(f1(x2741,x2742),f2(x2743,x2744)),f2(f2(x2744,x2743),f1(x2742,x2741)))), % 232.50/232.68 inference(scs_inference,[],[18,268,270,261,119,215,22,3,13,12,2])). % 232.50/232.68 cnf(276,plain, % 232.50/232.68 (E(f2(f2(x2761,x2762),f1(x2763,x2764)),f2(f2(x2762,x2761),f1(x2764,x2763)))), % 232.50/232.68 inference(scs_inference,[],[18,274,3])). % 232.50/232.68 cnf(292,plain, % 232.50/232.68 (E(f5(f2(f1(x2921,x2922),f2(x2923,x2924)),x2925),f5(f2(f2(x2924,x2923),f1(x2922,x2921)),x2925))), % 232.50/232.68 inference(scs_inference,[],[264,2,6])). % 232.50/232.68 cnf(317,plain, % 232.50/232.68 (E(f2(f2(x3171,x3172),f1(x3173,x3174)),f2(f1(x3174,x3173),f2(x3171,x3172)))), % 232.50/232.68 inference(scs_inference,[],[117,264,3])). % 232.50/232.68 cnf(320,plain, % 232.50/232.68 (E(f2(f1(x3201,x3202),f2(x3203,x3204)),f2(f2(x3203,x3204),f1(x3202,x3201)))), % 232.50/232.68 inference(scs_inference,[],[117,264,3,2])). % 232.50/232.68 cnf(322,plain, % 232.50/232.68 (E(f1(f2(f1(x3221,x3222),f2(x3223,x3224)),x3225),f1(f2(f2(x3223,x3224),f1(x3222,x3221)),x3225))), % 232.50/232.68 inference(scs_inference,[],[317,2,4])). % 232.50/232.68 cnf(323,plain, % 232.50/232.68 (E(f2(f1(x3231,x3232),f2(x3233,x3234)),f2(f2(x3234,x3233),f1(x3231,x3232)))), % 232.50/232.68 inference(scs_inference,[],[320,267,3])). % 232.50/232.68 cnf(325,plain, % 232.50/232.68 (E(f2(f2(x3251,x3252),f1(x3253,x3254)),f2(f1(x3253,x3254),f2(x3252,x3251)))), % 232.50/232.68 inference(scs_inference,[],[320,267,3,2])). % 232.50/232.68 cnf(326,plain, % 232.50/232.68 (E(f5(x3261,f2(f2(x3262,x3263),f1(x3264,x3265))),f5(x3261,f2(f1(x3264,x3265),f2(x3263,x3262))))), % 232.50/232.68 inference(scs_inference,[],[323,2,7])). % 232.50/232.68 cnf(327,plain, % 232.50/232.68 (E(f4(f2(f1(x3271,x3272),f2(x3273,x3274)),x3275),f4(f2(f2(x3274,x3273),f1(x3271,x3272)),x3275))), % 232.50/232.68 inference(scs_inference,[],[325,2,10])). % 232.50/232.68 cnf(328,plain, % 232.50/232.68 (E(f4(x3281,f2(f2(x3282,x3283),f1(x3284,x3285))),f4(x3281,f2(f1(x3285,x3284),f2(x3283,x3282))))), % 232.50/232.68 inference(scs_inference,[],[274,2,11])). % 232.50/232.68 cnf(330,plain, % 232.50/232.68 (E(f1(x3301,f2(f1(x3302,x3303),f2(x3304,x3305))),f1(x3301,f2(f2(x3304,x3305),f1(x3303,x3302))))), % 232.50/232.68 inference(scs_inference,[],[317,2,5])). % 232.50/232.68 cnf(340,plain, % 232.50/232.68 (E(f5(f2(f1(x3401,x3402),f2(x3403,x3404)),x3405),f5(f2(f2(x3404,x3403),f1(x3401,x3402)),x3405))), % 232.50/232.68 inference(scs_inference,[],[325,2,6])). % 232.50/232.68 cnf(346,plain, % 232.50/232.68 (E(f1(f2(f2(x3461,x3462),f1(x3463,x3464)),x3465),f1(f2(f1(x3464,x3463),f2(x3462,x3461)),x3465))), % 232.50/232.68 inference(scs_inference,[],[274,2,4])). % 232.50/232.68 cnf(398,plain, % 232.50/232.68 (E(f1(f2(f1(x3981,x3982),f2(x3983,x3984)),x3985),f1(f2(f2(x3984,x3983),f1(x3981,x3982)),x3985))), % 232.50/232.68 inference(scs_inference,[],[325,2,4])). % 232.50/232.68 cnf(415,plain, % 232.50/232.68 (E(f1(f2(f1(x4151,x4152),f2(x4153,x4154)),x4155),f1(f2(f2(x4154,x4153),f1(x4152,x4151)),x4155))), % 232.50/232.68 inference(scs_inference,[],[264,2,4])). % 232.50/232.68 cnf(427,plain, % 232.50/232.68 (E(f5(f1(f2(x4271,x4272),f1(x4273,x4274)),x4275),f5(f1(f1(x4274,x4273),f2(x4272,x4271)),x4275))), % 232.50/232.68 inference(scs_inference,[],[148,2,6])). % 232.50/232.68 cnf(428,plain, % 232.50/232.68 (E(f2(f1(f2(x4281,x4282),f1(x4283,x4284)),x4285),f2(f1(f1(x4284,x4283),f2(x4281,x4282)),x4285))), % 232.50/232.68 inference(scs_inference,[],[150,2,8])). % 232.50/232.68 cnf(542,plain, % 232.50/232.68 (~P2(x5421,f1(f2(x5422,x5423),f1(x5424,x5425)))+P2(x5421,f1(f2(x5423,x5422),f1(x5425,x5424)))), % 232.50/232.68 inference(scs_inference,[],[188,2,15])). % 232.50/232.68 cnf(543,plain, % 232.50/232.68 (~P2(x5431,f1(f2(x5432,x5433),f1(x5434,x5435)))+P2(x5431,f1(x5436,f1(f2(x5433,x5432),f1(x5435,x5434))))), % 232.50/232.68 inference(scs_inference,[],[542,25])). % 232.50/232.68 cnf(545,plain, % 232.50/232.68 (~P2(f4(f1(x5451,x5452),x5453),x5454)+P2(f4(f1(x5452,x5451),x5453),x5454)), % 232.50/232.68 inference(scs_inference,[],[229,2,14])). % 232.50/232.68 cnf(546,plain, % 232.50/232.68 (~P2(f4(f1(x5461,x5462),x5463),x5464)+P2(f4(f1(x5462,x5461),x5463),f1(x5465,x5464))), % 232.50/232.68 inference(scs_inference,[],[545,25])). % 232.50/232.68 cnf(547,plain, % 232.50/232.68 (P2(f4(f1(x5471,x5472),x5473),f1(x5474,f1(x5472,x5471)))+P1(f1(x5472,x5471),x5473)), % 232.50/232.68 inference(scs_inference,[],[546,23])). % 232.50/232.68 cnf(556,plain, % 232.50/232.68 (~P2(f4(f2(x5561,x5562),x5563),x5564)+P2(f4(f2(x5562,x5561),x5563),x5564)), % 232.50/232.68 inference(scs_inference,[],[263,2,14])). % 232.50/232.68 cnf(557,plain, % 232.50/232.68 (~P2(f4(f2(x5571,x5572),x5573),x5574)+P2(f4(f2(x5572,x5571),x5573),f1(x5575,x5574))), % 232.50/232.68 inference(scs_inference,[],[556,25])). % 232.50/232.68 cnf(590,plain, % 232.50/232.68 (~E(f2(f1(a6,a3),a3),a3)), % 232.50/232.68 inference(scs_inference,[],[69,212,2,3])). % 232.50/232.68 cnf(618,plain, % 232.50/232.68 (~P2(x6181,f1(f1(x6182,x6183),f2(x6184,x6185)))+P2(x6181,f1(f2(x6185,x6184),f1(x6183,x6182)))), % 232.50/232.68 inference(scs_inference,[],[144,2,15])). % 232.50/232.68 cnf(619,plain, % 232.50/232.68 (~P2(x6191,f1(f1(x6192,x6193),f2(x6194,x6195)))+P2(x6191,f1(x6196,f1(f2(x6195,x6194),f1(x6193,x6192))))), % 232.50/232.68 inference(scs_inference,[],[618,25])). % 232.50/232.68 cnf(638,plain, % 232.50/232.68 (P1(f1(f4(f1(x6381,x6382),x6383),x6384),f1(f4(f1(x6382,x6381),x6383),x6384))), % 232.50/232.68 inference(scs_inference,[],[229,21,4])). % 232.50/232.68 cnf(641,plain, % 232.50/232.68 (P1(f1(f2(f1(x6411,x6412),f2(x6413,x6414)),x6415),f1(f2(f1(x6412,x6411),f2(x6414,x6413)),x6415))), % 232.50/232.68 inference(scs_inference,[],[267,21,4])). % 232.50/232.68 cnf(644,plain, % 232.50/232.68 (P1(f1(f2(f2(x6441,x6442),f1(x6443,x6444)),x6445),f1(f2(f1(x6443,x6444),f2(x6442,x6441)),x6445))), % 232.50/232.68 inference(scs_inference,[],[325,21,4])). % 232.50/232.68 cnf(645,plain, % 232.50/232.68 (P1(f1(x6451,f2(f2(x6452,x6453),f1(x6454,x6455))),f1(x6451,f2(f2(x6453,x6452),f1(x6455,x6454))))), % 232.50/232.68 inference(scs_inference,[],[276,21,5])). % 232.50/232.68 cnf(646,plain, % 232.50/232.68 (P1(f5(f2(f1(x6461,x6462),f2(x6463,x6464)),x6465),f5(f2(f2(x6463,x6464),f1(x6462,x6461)),x6465))), % 232.50/232.68 inference(scs_inference,[],[320,21,6])). % 232.50/232.68 cnf(647,plain, % 232.50/232.68 (P1(f5(x6471,f2(f1(x6472,x6473),f2(x6474,x6475))),f5(x6471,f2(f2(x6475,x6474),f1(x6472,x6473))))), % 232.50/232.68 inference(scs_inference,[],[323,21,7])). % 232.50/232.68 cnf(648,plain, % 232.50/232.68 (~P2(x6481,f1(f2(x6482,x6483),x6484))+P2(x6481,f1(f2(x6483,x6482),x6484))), % 232.50/232.68 inference(scs_inference,[],[96,21,24])). % 232.54/232.68 cnf(649,plain, % 232.54/232.68 (~P2(x6491,f1(f2(x6492,x6493),x6494))+P2(x6491,f1(x6495,f1(f2(x6493,x6492),x6494)))), % 232.54/232.68 inference(scs_inference,[],[648,25])). % 232.54/232.68 cnf(652,plain, % 232.54/232.68 (~P2(x6521,f1(f2(x6522,x6523),f1(x6524,x6525)))+P2(x6521,f1(f1(x6525,x6524),f2(x6523,x6522)))), % 232.54/232.68 inference(scs_inference,[],[144,21,24])). % 232.54/232.68 cnf(653,plain, % 232.54/232.68 (~P2(x6531,f1(f2(x6532,x6533),f1(x6534,x6535)))+P2(x6531,f1(x6536,f1(f1(x6535,x6534),f2(x6533,x6532))))), % 232.54/232.68 inference(scs_inference,[],[652,25])). % 232.54/232.68 cnf(654,plain, % 232.54/232.68 (~P2(x6541,f1(f2(x6542,x6543),f1(x6544,x6545)))+P2(x6541,f1(f1(x6545,x6544),f2(x6542,x6543)))), % 232.54/232.68 inference(scs_inference,[],[146,21,24])). % 232.54/232.68 cnf(655,plain, % 232.54/232.68 (~P2(x6551,f1(f2(x6552,x6553),f1(x6554,x6555)))+P2(x6551,f1(x6556,f1(f1(x6555,x6554),f2(x6552,x6553))))), % 232.54/232.68 inference(scs_inference,[],[654,25])). % 232.54/232.68 cnf(658,plain, % 232.54/232.68 (~P2(x6581,f1(f1(x6582,x6583),f2(x6584,x6585)))+P2(x6581,f1(f2(x6584,x6585),f1(x6583,x6582)))), % 232.54/232.68 inference(scs_inference,[],[150,21,24])). % 232.54/232.68 cnf(663,plain, % 232.54/232.68 (~P2(x6631,f1(f1(x6632,x6633),f2(x6634,x6635)))+P2(x6631,f1(f1(x6633,x6632),f2(x6635,x6634)))), % 232.54/232.68 inference(scs_inference,[],[162,21,24])). % 232.54/232.68 cnf(664,plain, % 232.54/232.68 (~P2(x6641,f1(f1(x6642,x6643),f2(x6644,x6645)))+P2(x6641,f1(x6646,f1(f1(x6643,x6642),f2(x6645,x6644))))), % 232.54/232.68 inference(scs_inference,[],[663,25])). % 232.54/232.68 cnf(665,plain, % 232.54/232.68 (P1(f1(x6651,f1(f2(x6652,x6653),f1(x6654,x6655))),f1(x6651,f1(f2(x6653,x6652),f1(x6655,x6654))))), % 232.54/232.68 inference(scs_inference,[],[188,21,5])). % 232.54/232.68 cnf(666,plain, % 232.54/232.68 (~P2(x6661,f1(x6662,f1(x6663,x6664)))+P2(x6661,f1(x6662,f1(x6664,x6663)))), % 232.54/232.68 inference(scs_inference,[],[95,21,24])). % 232.54/232.68 cnf(667,plain, % 232.54/232.68 (~P2(x6671,f1(x6672,f1(x6673,x6674)))+P2(x6671,f1(x6675,f1(x6672,f1(x6674,x6673))))), % 232.54/232.68 inference(scs_inference,[],[666,25])). % 232.54/232.68 cnf(668,plain, % 232.54/232.68 (P1(f1(x6681,f4(f1(x6682,x6683),x6684)),f1(x6681,f4(f1(x6683,x6682),x6684)))), % 232.54/232.68 inference(scs_inference,[],[229,21,5])). % 232.54/232.68 cnf(671,plain, % 232.54/232.68 (P1(f1(f5(x6711,f2(x6712,x6713)),x6714),f1(f5(x6711,f2(x6713,x6712)),x6714))), % 232.54/232.68 inference(scs_inference,[],[113,21,4])). % 232.54/232.68 cnf(674,plain, % 232.54/232.68 (P1(f1(f5(f1(x6741,x6742),x6743),x6744),f1(f5(f1(x6742,x6741),x6743),x6744))), % 232.54/232.68 inference(scs_inference,[],[246,21,4])). % 232.54/232.68 cnf(677,plain, % 232.54/232.68 (P1(f1(f1(f2(x6771,x6772),f1(x6773,x6774)),x6775),f1(f1(f1(x6774,x6773),f2(x6772,x6771)),x6775))), % 232.54/232.68 inference(scs_inference,[],[144,21,4])). % 232.54/232.68 cnf(678,plain, % 232.54/232.68 (P1(f1(x6781,f1(f2(x6782,x6783),f1(x6784,x6785))),f1(x6781,f1(f1(x6785,x6784),f2(x6782,x6783))))), % 232.54/232.68 inference(scs_inference,[],[146,21,5])). % 232.54/232.68 cnf(681,plain, % 232.54/232.68 (P1(f2(f2(f2(x6811,x6812),f1(x6813,x6814)),x6815),f2(f2(f1(x6814,x6813),f2(x6812,x6811)),x6815))), % 232.54/232.68 inference(scs_inference,[],[264,21,8])). % 232.54/232.68 cnf(682,plain, % 232.54/232.68 (~P2(x6821,f1(f2(x6822,x6823),f1(x6824,x6825)))+P2(x6821,f1(f1(x6824,x6825),f2(x6823,x6822)))), % 232.54/232.68 inference(scs_inference,[],[157,21,24])). % 232.54/232.68 cnf(686,plain, % 232.54/232.68 (P1(f1(f2(f1(x6861,x6862),f2(x6863,x6864)),x6865),f1(f2(f2(x6864,x6863),f1(x6862,x6861)),x6865))), % 232.54/232.68 inference(scs_inference,[],[274,21,4])). % 232.54/232.68 cnf(687,plain, % 232.54/232.68 (P1(f5(f1(f2(x6871,x6872),f1(x6873,x6874)),x6875),f5(f1(f2(x6872,x6871),f1(x6874,x6873)),x6875))), % 232.54/232.68 inference(scs_inference,[],[188,21,6])). % 232.54/232.68 cnf(688,plain, % 232.54/232.68 (~P2(x6881,f2(f1(x6882,x6883),x6884))+P2(x6881,f2(f1(x6883,x6882),x6884))), % 232.54/232.68 inference(scs_inference,[],[212,21,24])). % 232.54/232.68 cnf(689,plain, % 232.54/232.68 (~P2(x6891,f2(f1(x6892,x6893),x6894))+P2(x6891,f1(x6895,f2(f1(x6893,x6892),x6894)))), % 232.54/232.68 inference(scs_inference,[],[688,25])). % 232.54/232.68 cnf(691,plain, % 232.54/232.68 (~P2(x6911,f2(x6912,f1(x6913,x6914)))+P2(x6911,f2(x6912,f1(x6914,x6913)))), % 232.54/232.68 inference(scs_inference,[],[221,21,24])). % 232.54/232.68 cnf(692,plain, % 232.54/232.68 (~P2(x6921,f2(x6922,f1(x6923,x6924)))+P2(x6921,f1(x6925,f2(x6922,f1(x6924,x6923))))), % 232.54/232.68 inference(scs_inference,[],[691,25])). % 232.54/232.68 cnf(693,plain, % 232.54/232.68 (P1(f1(f2(f2(x6931,x6932),f1(x6933,x6934)),x6935),f1(f2(f1(x6934,x6933),f2(x6931,x6932)),x6935))), % 232.54/232.68 inference(scs_inference,[],[317,21,4])). % 232.54/232.68 cnf(700,plain, % 232.54/232.68 (P1(f1(f2(x7001,f2(x7002,x7003)),x7004),f1(f2(x7001,f2(x7003,x7002)),x7004))), % 232.54/232.68 inference(scs_inference,[],[258,21,4])). % 232.54/232.68 cnf(713,plain, % 232.54/232.68 (P1(f1(f1(f1(x7131,x7132),f2(x7133,x7134)),x7135),f1(f1(f1(x7132,x7131),f2(x7134,x7133)),x7135))), % 232.54/232.68 inference(scs_inference,[],[162,21,4])). % 232.54/232.68 cnf(715,plain, % 232.54/232.68 (P1(f5(x7151,f2(f1(x7152,x7153),f2(x7154,x7155))),f5(x7151,f2(f2(x7154,x7155),f1(x7153,x7152))))), % 232.54/232.68 inference(scs_inference,[],[320,21,7])). % 232.54/232.68 cnf(719,plain, % 232.54/232.68 (~P2(x7191,f1(x7192,f2(x7193,x7194)))+P2(x7191,f1(x7192,f2(x7194,x7193)))), % 232.54/232.68 inference(scs_inference,[],[251,21,24])). % 232.54/232.68 cnf(720,plain, % 232.54/232.68 (~P2(x7201,f1(x7202,f2(x7203,x7204)))+P2(x7201,f1(x7205,f1(x7202,f2(x7204,x7203))))), % 232.54/232.68 inference(scs_inference,[],[719,25])). % 232.54/232.68 cnf(723,plain, % 232.54/232.68 (P1(f1(x7231,f5(x7232,f2(x7233,x7234))),f1(x7231,f5(x7232,f2(x7234,x7233))))), % 232.54/232.68 inference(scs_inference,[],[113,21,5])). % 232.54/232.68 cnf(726,plain, % 232.54/232.68 (P1(f2(x7261,f1(f1(x7262,x7263),f2(x7264,x7265))),f2(x7261,f1(f2(x7265,x7264),f1(x7263,x7262))))), % 232.54/232.68 inference(scs_inference,[],[148,21,9])). % 232.54/232.68 cnf(732,plain, % 232.54/232.68 (~P2(x7321,f1(x7322,x7323))+P2(x7321,f1(x7323,x7322))), % 232.54/232.68 inference(scs_inference,[],[17,21,24])). % 232.54/232.68 cnf(733,plain, % 232.54/232.68 (~P2(x7331,f1(x7332,x7333))+P2(x7331,f1(x7334,f1(x7333,x7332)))), % 232.54/232.68 inference(scs_inference,[],[732,25])). % 232.54/232.68 cnf(746,plain, % 232.54/232.68 (P1(f5(f2(f2(x7461,x7462),f1(x7463,x7464)),x7465),f5(f2(f1(x7464,x7463),f2(x7461,x7462)),x7465))), % 232.54/232.68 inference(scs_inference,[],[317,21,6])). % 232.54/232.68 cnf(747,plain, % 232.54/232.68 (P1(f2(f2(f1(x7471,x7472),f2(x7473,x7474)),x7475),f2(f2(f2(x7473,x7474),f1(x7472,x7471)),x7475))), % 232.54/232.68 inference(scs_inference,[],[320,21,8])). % 232.54/232.68 cnf(750,plain, % 232.54/232.68 (P1(f4(x7501,f2(f2(x7502,x7503),f1(x7504,x7505))),f4(x7501,f2(f1(x7504,x7505),f2(x7503,x7502))))), % 232.54/232.68 inference(scs_inference,[],[325,21,11])). % 232.54/232.68 cnf(752,plain, % 232.54/232.68 (P1(f1(f2(f2(x7521,x7522),x7523),x7524),f1(f2(f2(x7522,x7521),x7523),x7524))), % 232.54/232.68 inference(scs_inference,[],[117,21,4])). % 232.54/232.68 cnf(772,plain, % 232.54/232.68 (P1(f1(x7721,f2(f1(x7722,x7723),x7724)),f1(x7721,f2(f1(x7723,x7722),x7724)))), % 232.54/232.68 inference(scs_inference,[],[212,21,5])). % 232.54/232.68 cnf(776,plain, % 232.54/232.68 (P1(f1(f2(x7761,f1(x7762,x7763)),x7764),f1(f2(x7761,f1(x7763,x7762)),x7764))), % 232.54/232.68 inference(scs_inference,[],[221,21,4])). % 232.54/232.68 cnf(777,plain, % 232.54/232.68 (P1(f1(x7771,f2(f1(x7772,x7773),f2(x7774,x7775))),f1(x7771,f2(f1(x7773,x7772),f2(x7775,x7774))))), % 232.54/232.68 inference(scs_inference,[],[267,21,5])). % 232.54/232.68 cnf(786,plain, % 232.54/232.68 (P1(f1(x7861,f5(x7862,f1(x7863,x7864))),f1(x7861,f5(x7862,f1(x7864,x7863))))), % 232.54/232.68 inference(scs_inference,[],[250,21,5])). % 232.54/232.68 cnf(827,plain, % 232.54/232.68 (~P2(x8271,f1(f1(x8272,x8273),x8274))+P2(x8271,f1(f1(x8273,x8272),x8274))), % 232.54/232.68 inference(scs_inference,[],[39,21,24])). % 232.54/232.68 cnf(828,plain, % 232.54/232.68 (~P2(x8281,f1(f1(x8282,x8283),x8284))+P2(x8281,f1(x8285,f1(f1(x8283,x8282),x8284)))), % 232.54/232.68 inference(scs_inference,[],[827,25])). % 232.54/232.68 cnf(838,plain, % 232.54/232.68 (P1(f1(f1(f2(x8381,x8382),f1(x8383,x8384)),x8385),f1(f1(f1(x8383,x8384),f2(x8382,x8381)),x8385))), % 232.54/232.68 inference(scs_inference,[],[157,21,4])). % 232.54/232.68 cnf(839,plain, % 232.54/232.68 (P1(f1(x8391,f5(f2(x8392,x8393),x8394)),f1(x8391,f5(f2(x8393,x8392),x8394)))), % 232.54/232.68 inference(scs_inference,[],[102,21,5])). % 232.54/232.68 cnf(862,plain, % 232.54/232.68 (P1(x8621,x8622)+P2(f4(x8621,x8622),f1(x8623,x8621))), % 232.54/232.68 inference(scs_inference,[],[23,25])). % 232.54/232.68 cnf(863,plain, % 232.54/232.68 (P1(x8631,x8632)+P2(f4(x8631,x8632),f1(f1(x8633,x8631),x8634))), % 232.54/232.68 inference(scs_inference,[],[862,26])). % 232.54/232.68 cnf(864,plain, % 232.54/232.68 (P1(x8641,f1(f1(x8642,x8641),x8643))), % 232.54/232.68 inference(scs_inference,[],[863,29])). % 232.54/232.68 cnf(870,plain, % 232.54/232.68 (P1(x8701,f1(f2(x8702,x8703),f1(x8701,x8704)))), % 232.54/232.68 inference(scs_inference,[],[148,864,13])). % 232.54/232.68 cnf(883,plain, % 232.54/232.68 (P1(x8831,f1(f1(x8831,x8832),f2(x8833,x8834)))), % 232.54/232.68 inference(scs_inference,[],[157,870,13])). % 232.54/232.68 cnf(916,plain, % 232.54/232.68 (P1(x9161,x9162)+P2(f4(x9161,x9162),f1(x9161,x9163))), % 232.54/232.68 inference(scs_inference,[],[23,26])). % 232.54/232.68 cnf(917,plain, % 232.54/232.68 (P1(x9171,x9172)+P2(f4(x9171,x9172),f1(x9173,f1(x9171,x9174)))), % 232.54/232.68 inference(scs_inference,[],[916,25])). % 232.54/232.68 cnf(918,plain, % 232.54/232.68 (P1(x9181,f1(x9182,f1(x9181,x9183)))), % 232.54/232.68 inference(scs_inference,[],[917,29])). % 232.54/232.68 cnf(933,plain, % 232.54/232.68 (P1(f1(x9331,x9332),f1(f1(f1(x9332,x9331),x9333),f2(x9334,x9335)))), % 232.54/232.68 inference(scs_inference,[],[17,883,12])). % 232.54/232.68 cnf(940,plain, % 232.54/232.68 (E(f1(x9401,f1(x9402,x9403)),x9403)+~P1(f1(x9401,f1(x9402,x9403)),x9403)), % 232.54/232.68 inference(scs_inference,[],[17,864,883,12,13,22,2])). % 232.54/232.68 cnf(943,plain, % 232.54/232.68 (P1(x9431,f1(f1(x9431,x9432),x9433))), % 232.54/232.68 inference(scs_inference,[],[17,918,13])). % 232.54/232.68 cnf(998,plain, % 232.54/232.68 (P2(f4(f1(x9981,x9982),x9983),f1(x9982,x9981))+P1(f1(x9982,x9981),x9983)), % 232.54/232.68 inference(scs_inference,[],[23,545])). % 232.54/232.68 cnf(1021,plain, % 232.54/232.68 (~P2(x10211,x10212)+P2(x10211,x10213)+P2(f4(x10212,x10213),x10212)), % 232.54/232.68 inference(scs_inference,[],[23,24])). % 232.54/232.68 cnf(1022,plain, % 232.54/232.68 (~P2(x10221,x10222)+P2(x10221,x10223)+P2(f4(x10222,x10223),f1(f1(x10224,x10222),x10225))), % 232.54/232.68 inference(scs_inference,[],[864,1021,24])). % 232.54/232.68 cnf(1062,plain, % 232.54/232.68 (P1(x10621,x10622)+~P2(f4(x10621,x10622),x10623)+P2(f4(x10621,x10622),f2(x10623,x10621))), % 232.54/232.68 inference(scs_inference,[],[23,31])). % 232.54/232.68 cnf(1063,plain, % 232.54/232.68 (P1(x10631,x10632)+~P2(f4(x10631,x10632),x10633)+P2(f4(x10631,x10632),f1(x10634,f2(x10633,x10631)))), % 232.54/232.68 inference(scs_inference,[],[1062,25])). % 232.54/232.68 cnf(1087,plain, % 232.54/232.68 (P2(f4(x10871,x10872),f2(x10871,x10871))+P1(x10871,x10872)), % 232.54/232.68 inference(scs_inference,[],[23,1062])). % 232.54/232.68 cnf(1092,plain, % 232.54/232.68 (P2(f4(x10921,x10922),f1(x10923,f2(x10921,x10921)))+P1(x10921,x10922)), % 232.54/232.68 inference(scs_inference,[],[23,1063])). % 232.54/232.68 cnf(1114,plain, % 232.54/232.68 (~P2(x11141,x11142)+P2(x11141,f1(f1(x11143,x11142),x11144))), % 232.54/232.68 inference(scs_inference,[],[25,26])). % 232.54/232.68 cnf(1115,plain, % 232.54/232.68 (P2(x11151,f1(f1(x11152,x11153),x11154))+~P2(x11151,f2(x11155,x11153))), % 232.54/232.68 inference(scs_inference,[],[1114,27])). % 232.54/232.68 cnf(1117,plain, % 232.54/232.68 (P2(x11171,f1(x11172,x11173))+~P2(x11171,f2(x11174,x11173))), % 232.54/232.68 inference(scs_inference,[],[25,27])). % 232.54/232.68 cnf(1118,plain, % 232.54/232.68 (P1(x11181,f1(x11182,x11183))+~P2(f4(x11181,f1(x11182,x11183)),f2(x11184,x11183))), % 232.54/232.68 inference(scs_inference,[],[1117,29])). % 232.54/232.68 cnf(1119,plain, % 232.54/232.68 (P1(f2(x11191,x11192),f1(x11193,x11192))), % 232.54/232.68 inference(scs_inference,[],[1118,23])). % 232.54/232.68 cnf(1317,plain, % 232.54/232.68 (P1(f2(x13171,x13172),f1(x13172,x13173))), % 232.54/232.68 inference(scs_inference,[],[17,1119,13])). % 232.54/232.68 cnf(1389,plain, % 232.54/232.68 (P1(f2(x13891,x13892),f1(x13891,x13893))), % 232.54/232.68 inference(scs_inference,[],[18,1317,12])). % 232.54/232.68 cnf(1570,plain, % 232.54/232.68 (~P2(f4(x15701,f1(x15702,x15703)),x15703)+P1(x15701,f1(x15702,x15703))), % 232.54/232.68 inference(scs_inference,[],[25,29])). % 232.54/232.68 cnf(1571,plain, % 232.54/232.68 (P1(x15711,f1(x15712,x15711))), % 232.54/232.68 inference(scs_inference,[],[1570,23])). % 232.54/232.68 cnf(1650,plain, % 232.54/232.68 (P2(x16501,f1(x16502,x16503))+~P2(x16501,f2(x16503,x16504))), % 232.54/232.68 inference(scs_inference,[],[25,28])). % 232.54/232.68 cnf(1651,plain, % 232.54/232.68 (~P2(x16511,f2(x16512,x16513))+P2(x16511,f1(f1(x16514,x16512),x16515))), % 232.54/232.68 inference(scs_inference,[],[1650,26])). % 232.54/232.68 cnf(1661,plain, % 232.54/232.68 (P1(x16611,f1(x16612,x16611))), % 232.54/232.68 inference(rename_variables,[],[1571])). % 232.54/232.68 cnf(1662,plain, % 232.54/232.68 (P1(x16621,f1(x16621,x16622))), % 232.54/232.68 inference(scs_inference,[],[17,1571,1661,12,13])). % 232.54/232.68 cnf(1670,plain, % 232.54/232.68 (P1(f1(x16701,x16702),f1(f1(x16702,x16701),x16703))), % 232.54/232.68 inference(scs_inference,[],[17,1662,12])). % 232.54/232.68 cnf(1769,plain, % 232.54/232.68 (~P2(f4(f2(x17691,x17692),x17693),x17694)+P2(f4(f2(x17692,x17691),x17693),f1(x17695,f1(x17696,x17694)))), % 232.54/232.68 inference(scs_inference,[],[25,557])). % 232.54/232.68 cnf(1821,plain, % 232.54/232.68 (~P2(x18211,f2(x18212,x18213))+P2(x18211,f2(f2(x18213,x18212),f2(x18213,x18212)))), % 232.54/232.68 inference(scs_inference,[],[18,15,31])). % 232.54/232.68 cnf(1823,plain, % 232.54/232.68 (~P2(x18231,f2(x18232,x18233))+P2(x18231,f1(x18234,f2(x18233,x18232)))), % 232.54/232.68 inference(scs_inference,[],[18,15,31,25])). % 232.54/232.68 cnf(1825,plain, % 232.54/232.68 (~P2(x18251,f2(x18252,x18253))+P2(x18251,f1(f2(x18253,x18252),x18254))), % 232.54/232.68 inference(scs_inference,[],[18,15,31,25,26])). % 232.54/232.68 cnf(1827,plain, % 232.54/232.68 (~P2(x18271,f2(f2(x18272,x18273),x18274))+P2(x18271,x18272)), % 232.54/232.68 inference(scs_inference,[],[18,15,31,25,26,53])). % 232.54/232.68 cnf(1880,plain, % 232.54/232.68 (~P2(x18801,f2(f2(x18802,x18803),x18804))+P2(x18801,f1(x18805,x18802))), % 232.54/232.68 inference(scs_inference,[],[1827,25])). % 232.54/232.68 cnf(1888,plain, % 232.54/232.68 (~P2(x18881,f1(x18882,x18883))+P2(x18881,f1(f1(x18883,x18882),x18884))), % 232.54/232.68 inference(scs_inference,[],[1670,24])). % 232.54/232.69 cnf(1898,plain, % 232.54/232.69 (~P2(x18981,x18982)+P2(x18981,f1(f1(x18982,x18983),x18984))), % 232.54/232.69 inference(scs_inference,[],[943,24])). % 232.54/232.69 cnf(1907,plain, % 232.54/232.69 (~P2(x19071,f1(x19072,x19073))+P2(x19071,f1(x19074,f1(x19075,f1(x19073,x19072))))), % 232.54/232.69 inference(scs_inference,[],[1888,733])). % 232.54/232.69 cnf(1909,plain, % 232.54/232.69 (~P2(x19091,f2(x19092,x19093))+P2(x19091,f1(x19092,x19094))), % 232.54/232.69 inference(scs_inference,[],[1389,24])). % 232.54/232.69 cnf(1927,plain, % 232.54/232.69 (~P2(x19271,f2(x19272,x19273))+P2(x19271,f1(x19274,f1(x19273,x19275)))), % 232.54/232.69 inference(scs_inference,[],[1821,64])). % 232.54/232.69 cnf(1929,plain, % 232.54/232.69 (~P2(x19291,f2(x19292,x19293))+P2(x19291,f1(x19293,x19294))), % 232.54/232.69 inference(scs_inference,[],[1317,24])). % 232.54/232.69 cnf(1950,plain, % 232.54/232.69 (~P2(x19501,x19502)+P2(x19501,f2(x19502,x19502))), % 232.54/232.69 inference(scs_inference,[],[16,24,31])). % 232.54/232.69 cnf(1952,plain, % 232.54/232.69 (~P2(x19521,x19522)+P2(x19521,f1(x19523,f2(x19522,x19522)))), % 232.54/232.69 inference(scs_inference,[],[16,24,31,1823])). % 232.54/232.69 cnf(1954,plain, % 232.54/232.69 (~P2(x19541,x19542)+P2(x19541,f1(f2(x19542,x19542),x19543))), % 232.54/232.69 inference(scs_inference,[],[16,24,31,1823,1825])). % 232.54/232.69 cnf(2048,plain, % 232.54/232.69 (~P2(x20481,f1(f1(x20482,x20483),f2(x20484,x20485)))+P2(x20481,f1(x20486,f1(f2(x20484,x20485),f1(x20483,x20482))))), % 232.54/232.69 inference(scs_inference,[],[25,658])). % 232.54/232.69 cnf(2050,plain, % 232.54/232.69 (~P2(x20501,f1(f2(x20502,x20503),f1(x20504,x20505)))+P2(x20501,f1(x20506,f1(f1(x20504,x20505),f2(x20503,x20502))))), % 232.54/232.69 inference(scs_inference,[],[25,682])). % 232.54/232.69 cnf(2063,plain, % 232.54/232.69 (~P2(x20631,f2(x20632,x20633))+P2(x20631,f1(x20634,f1(f1(x20635,x20633),x20636)))), % 232.54/232.69 inference(scs_inference,[],[25,1115])). % 232.54/232.69 cnf(2065,plain, % 232.54/232.69 (~P2(x20651,f2(x20652,x20653))+P2(x20651,f1(x20654,f1(f1(x20655,x20652),x20656)))), % 232.54/232.69 inference(scs_inference,[],[25,1651])). % 232.54/232.69 cnf(2072,plain, % 232.54/232.69 (P2(x20721,f2(f1(x20722,x20723),f1(x20722,x20723)))+~P2(x20721,x20723)), % 232.54/232.69 inference(scs_inference,[],[25,1950])). % 232.54/232.69 cnf(2076,plain, % 232.54/232.69 (P2(x20761,f1(x20762,f2(f1(x20763,x20764),f1(x20763,x20764))))+~P2(x20761,x20764)), % 232.54/232.69 inference(scs_inference,[],[25,1952])). % 232.54/232.69 cnf(2078,plain, % 232.54/232.69 (P2(x20781,f1(f2(f1(x20782,x20783),f1(x20782,x20783)),x20784))+~P2(x20781,x20783)), % 232.54/232.69 inference(scs_inference,[],[25,1954])). % 232.54/232.69 cnf(2085,plain, % 232.54/232.69 (~P2(x20851,x20852)+~P2(x20851,x20853)+P2(x20851,f2(x20853,f1(x20854,x20852)))), % 232.54/232.69 inference(scs_inference,[],[25,31])). % 232.54/232.69 cnf(2086,plain, % 232.54/232.69 (~P2(x20861,x20862)+~P2(x20861,x20863)+P2(x20861,f1(f2(x20863,f1(x20864,x20862)),x20865))), % 232.54/232.69 inference(scs_inference,[],[2085,26])). % 232.54/232.69 cnf(2088,plain, % 232.54/232.69 (~P2(x20881,x20882)+~P2(x20881,x20883)+P2(x20881,f2(f1(x20884,x20882),x20883))), % 232.54/232.69 inference(scs_inference,[],[25,31])). % 232.54/232.69 cnf(2135,plain, % 232.54/232.69 (~P2(x21351,x21352)+~P2(x21351,x21353)+P2(x21351,f2(f1(x21354,x21352),f1(x21355,x21353)))), % 232.54/232.69 inference(scs_inference,[],[25,2085])). % 232.54/232.69 cnf(2136,plain, % 232.54/232.69 (~P2(x21361,x21362)+~P2(x21361,x21363)+P2(x21361,f1(f2(f1(x21364,x21362),f1(x21365,x21363)),x21366))), % 232.54/232.69 inference(scs_inference,[],[2135,26])). % 232.54/232.69 cnf(2140,plain, % 232.54/232.69 (~P2(x21401,f2(x21402,x21403))+P2(x21401,f1(x21404,f1(x21402,x21405)))), % 232.54/232.69 inference(scs_inference,[],[25,1909])). % 232.54/232.69 cnf(2164,plain, % 232.54/232.69 (~P2(x21641,f2(x21642,x21643))+P2(x21641,f1(x21644,f1(x21645,f1(x21643,x21646))))), % 232.54/232.69 inference(scs_inference,[],[25,1927])). % 232.54/232.69 cnf(2169,plain, % 232.54/232.69 (~P2(x21691,x21692)+P2(x21691,f1(f1(x21693,f1(x21694,x21692)),x21695))), % 232.54/232.69 inference(scs_inference,[],[864,25,24])). % 232.54/232.69 cnf(2182,plain, % 232.54/232.69 (E(f4(f2(x21821,x21822),f1(f2(x21823,x21824),f1(x21825,x21826))),f4(f2(x21822,x21821),f1(f1(x21826,x21825),f2(x21823,x21824))))), % 232.54/232.69 inference(scs_inference,[],[263,160,2,3])). % 232.54/232.69 cnf(2186,plain, % 232.54/232.69 (E(f1(x21861,x21862),f1(x21862,x21861))), % 232.54/232.69 inference(rename_variables,[],[17])). % 232.54/232.69 cnf(2187,plain, % 232.54/232.69 (P1(f1(x21871,x21872),f1(f1(x21873,f1(x21872,x21871)),x21874))), % 232.54/232.69 inference(scs_inference,[],[17,2186,263,864,933,160,2,3,13,12])). % 232.54/232.69 cnf(2193,plain, % 232.54/232.69 (E(f1(x21931,f1(f2(x21932,x21933),f1(x21934,x21935))),f1(f1(f1(x21934,x21935),f2(x21933,x21932)),x21931))), % 232.54/232.69 inference(scs_inference,[],[17,166,2182,2,3])). % 232.54/232.69 cnf(2208,plain, % 232.54/232.69 (E(f2(f1(f1(x22081,x22082),f2(x22083,x22084)),x22085),f2(x22085,f1(f2(x22084,x22083),f1(x22082,x22081))))), % 232.54/232.69 inference(scs_inference,[],[17,18,2187,173,2193,2,13,3])). % 232.54/232.69 cnf(2217,plain, % 232.54/232.69 (E(f1(f1(f2(x22171,x22172),f1(x22173,x22174)),x22175),f1(x22175,f1(f1(x22173,x22174),f2(x22172,x22171))))), % 232.54/232.69 inference(scs_inference,[],[17,180,2208,2,3])). % 232.54/232.69 cnf(2233,plain, % 232.54/232.69 (E(f4(f2(x22331,x22332),f1(f1(x22333,x22334),f2(x22335,x22336))),f4(f2(x22332,x22331),f1(f2(x22336,x22335),f1(x22334,x22333))))), % 232.54/232.69 inference(scs_inference,[],[17,263,638,187,2217,2,13,3])). % 232.54/232.69 cnf(2244,plain, % 232.54/232.69 (E(f1(x22441,x22442),f1(x22442,x22441))), % 232.54/232.69 inference(rename_variables,[],[17])). % 232.54/232.69 cnf(2245,plain, % 232.54/232.69 (E(f1(x22451,f1(f2(x22452,x22453),f1(x22454,x22455))),f1(f1(f1(x22455,x22454),f2(x22453,x22452)),x22451))), % 232.54/232.69 inference(scs_inference,[],[17,2244,641,192,2233,2,13,3])). % 232.54/232.69 cnf(2252,plain, % 232.54/232.69 (E(f1(f1(f1(x22521,x22522),f2(x22523,x22524)),x22525),f1(x22525,f1(f2(x22524,x22523),f1(x22522,x22521))))), % 232.54/232.69 inference(scs_inference,[],[2245,2])). % 232.54/232.69 cnf(2255,plain, % 232.54/232.69 (E(f1(x22551,x22552),f1(x22552,x22551))), % 232.54/232.69 inference(rename_variables,[],[17])). % 232.54/232.69 cnf(2256,plain, % 232.54/232.69 (E(f1(f1(f2(x22561,x22562),f1(x22563,x22564)),x22565),f1(x22565,f1(f1(x22564,x22563),f2(x22561,x22562))))), % 232.54/232.69 inference(scs_inference,[],[17,2255,644,193,2245,2,13,3])). % 232.54/232.69 cnf(2258,plain, % 232.54/232.69 (E(f1(x22581,x22582),f1(x22582,x22581))), % 232.54/232.69 inference(rename_variables,[],[17])). % 232.54/232.69 cnf(2262,plain, % 232.54/232.69 (E(f1(f2(f2(x22621,x22621),f1(x22622,x22623)),x22624),f1(x22624,f2(f1(x22622,x22623),f2(x22621,x22621))))), % 232.54/232.69 inference(scs_inference,[],[17,2255,2258,100,641,644,193,2245,2,13,3,12,22])). % 232.54/232.69 cnf(2269,plain, % 232.54/232.69 (E(f1(x22691,x22692),f1(x22692,x22691))), % 232.54/232.69 inference(rename_variables,[],[17])). % 232.54/232.69 cnf(2276,plain, % 232.54/232.69 (E(f1(f2(x22761,x22761),f2(f2(x22762,x22762),f1(x22763,x22764))),f1(f2(f1(x22763,x22764),f2(x22762,x22762)),f2(x22761,x22761)))), % 232.54/232.69 inference(scs_inference,[],[17,2269,246,103,644,645,2262,195,2,13,3,12,22])). % 232.54/232.69 cnf(2284,plain, % 232.54/232.69 (E(f2(x22841,f1(f1(x22842,x22843),f2(x22844,x22845))),f2(f1(f2(x22844,x22845),f1(x22843,x22842)),x22841))), % 232.54/232.69 inference(scs_inference,[],[18,113,646,2276,196,2,13,3])). % 232.54/232.69 cnf(2290,plain, % 232.54/232.69 (E(f1(x22901,f1(f1(x22902,x22903),f2(x22904,x22905))),f1(f1(f2(x22904,x22905),f1(x22903,x22902)),x22901))), % 232.54/232.69 inference(scs_inference,[],[2256,2])). % 232.54/232.69 cnf(2294,plain, % 232.54/232.69 (E(f2(f1(f2(x22941,x22942),f1(x22943,x22944)),x22945),f2(x22945,f1(f1(x22944,x22943),f2(x22942,x22941))))), % 232.54/232.69 inference(scs_inference,[],[18,113,647,197,2256,2,13,3])). % 232.54/232.69 cnf(2316,plain, % 232.54/232.69 (E(f5(f1(f2(x23161,x23162),f1(x23163,x23164)),f2(x23165,x23166)),f5(f1(f1(x23163,x23164),f2(x23162,x23161)),f2(x23166,x23165)))), % 232.54/232.69 inference(scs_inference,[],[17,113,671,202,2284,2,13,3])). % 232.54/232.69 cnf(2326,plain, % 232.54/232.69 (E(f1(x23261,x23262),f1(x23262,x23261))), % 232.54/232.69 inference(rename_variables,[],[17])). % 232.54/232.69 cnf(2327,plain, % 232.54/232.69 (E(f1(x23271,f1(f1(x23272,x23273),f2(x23274,x23275))),f1(f1(f2(x23275,x23274),f1(x23273,x23272)),x23271))), % 232.54/232.69 inference(scs_inference,[],[17,2326,674,2316,208,2,13,3])). % 232.54/232.69 cnf(2338,plain, % 232.54/232.69 (E(f5(f1(f1(x23381,x23382),f2(x23383,x23384)),f2(x23385,x23386)),f5(f1(f2(x23383,x23384),f1(x23382,x23381)),f2(x23386,x23385)))), % 232.54/232.69 inference(scs_inference,[],[17,113,677,210,2294,2,13,3])). % 232.54/232.69 cnf(2346,plain, % 232.54/232.69 (P1(f1(x23461,f1(f2(x23462,x23463),f1(x23464,x23465))),f1(x23461,f1(f1(x23465,x23464),f2(x23462,x23463))))), % 232.54/232.69 inference(rename_variables,[],[678])). % 232.54/232.69 cnf(2347,plain, % 232.54/232.69 (E(f1(x23471,x23472),f1(x23472,x23471))), % 232.54/232.69 inference(rename_variables,[],[17])). % 232.54/232.69 cnf(2354,plain, % 232.54/232.69 (E(f1(x23541,f1(f2(x23542,x23543),f1(x23544,x23544))),f1(f1(f1(x23544,x23544),f2(x23542,x23543)),x23541))), % 232.54/232.69 inference(scs_inference,[],[17,2347,113,42,678,2346,2338,292,2,13,3,12,22])). % 232.54/232.69 cnf(2369,plain, % 232.54/232.69 (P1(f2(f2(f2(x23691,x23692),f1(x23693,x23694)),x23695),f2(f2(f1(x23694,x23693),f2(x23692,x23691)),x23695))), % 232.54/232.69 inference(rename_variables,[],[681])). % 232.54/232.69 cnf(2370,plain, % 232.54/232.69 (E(f2(x23701,x23702),f2(x23702,x23701))), % 232.54/232.69 inference(rename_variables,[],[18])). % 232.54/232.69 cnf(2374,plain, % 232.54/232.69 (P1(f2(x23741,f2(f2(x23742,x23743),f1(x23744,x23745))),f2(f2(f1(x23745,x23744),f2(x23743,x23742)),x23741))), % 232.54/232.69 inference(scs_inference,[],[17,18,2370,681,2369,2354,322,2,13,3,12])). % 232.54/232.69 cnf(2377,plain, % 232.54/232.69 (E(f2(f2(f2(x23771,x23771),f1(x23772,x23772)),x23773),f2(x23773,f2(f1(x23772,x23772),f2(x23771,x23771))))), % 232.54/232.69 inference(scs_inference,[],[17,18,2370,121,681,2369,2354,322,2,13,3,12,22])). % 232.54/232.69 cnf(2382,plain, % 232.54/232.69 (P1(f1(f2(f1(x23821,x23822),f2(x23823,x23824)),x23825),f1(x23825,f2(f2(x23824,x23823),f1(x23822,x23821))))), % 232.54/232.69 inference(scs_inference,[],[17,686,2377,2,13])). % 232.54/232.69 cnf(2383,plain, % 232.54/232.69 (P1(f1(f2(f1(x23831,x23832),f2(x23833,x23834)),x23835),f1(f2(f2(x23834,x23833),f1(x23832,x23831)),x23835))), % 232.54/232.69 inference(rename_variables,[],[686])). % 232.54/232.69 cnf(2384,plain, % 232.54/232.69 (E(f1(x23841,x23842),f1(x23842,x23841))), % 232.54/232.69 inference(rename_variables,[],[17])). % 232.54/232.69 cnf(2391,plain, % 232.54/232.69 (E(f2(x23911,f2(f2(x23912,x23912),f1(x23913,x23913))),f2(f2(f1(x23913,x23913),f2(x23912,x23912)),x23911))), % 232.54/232.69 inference(scs_inference,[],[17,2384,113,119,686,2383,2374,2377,326,2,13,3,12,22])). % 232.54/232.69 cnf(2403,plain, % 232.54/232.69 (P1(f1(x24031,f2(f2(x24032,x24033),f1(x24034,x24035))),f1(f2(f1(x24035,x24034),f2(x24032,x24033)),x24031))), % 232.54/232.69 inference(scs_inference,[],[17,113,263,687,693,2391,327,2,13,3,12])). % 232.54/232.69 cnf(2406,plain, % 232.54/232.69 (E(f1(f2(f1(x24061,x24061),f2(x24062,x24062)),x24063),f1(x24063,f2(f2(x24062,x24062),f1(x24061,x24061))))), % 232.54/232.69 inference(scs_inference,[],[17,113,263,100,687,693,2382,2391,327,2,13,3,12,22])). % 232.54/232.69 cnf(2414,plain, % 232.54/232.69 (E(f1(x24141,x24142),f1(x24142,x24141))), % 232.54/232.69 inference(rename_variables,[],[17])). % 232.54/232.69 cnf(2421,plain, % 232.54/232.69 (E(f1(f2(x24211,x24211),f2(f2(x24212,x24213),f1(x24214,x24214))),f1(f2(f1(x24214,x24214),f2(x24212,x24213)),f2(x24211,x24211)))), % 232.54/232.69 inference(scs_inference,[],[17,2414,263,103,693,700,2403,2406,328,2,13,3,12,22])). % 232.54/232.69 cnf(2427,plain, % 232.54/232.69 (P1(f1(f2(x24271,f2(x24272,x24273)),x24274),f1(x24274,f2(x24271,f2(x24273,x24272))))), % 232.54/232.69 inference(scs_inference,[],[17,700,2421,2,13])). % 232.54/232.69 cnf(2429,plain, % 232.54/232.69 (E(f1(x24291,x24292),f1(x24292,x24291))), % 232.54/232.69 inference(rename_variables,[],[17])). % 232.54/232.69 cnf(2430,plain, % 232.54/232.69 (E(f1(f2(f1(x24301,x24302),f2(x24303,x24304)),x24305),f1(x24305,f2(f2(x24303,x24304),f1(x24302,x24301))))), % 232.54/232.69 inference(scs_inference,[],[17,2429,700,2421,330,2,13,3])). % 232.54/232.69 cnf(2462,plain, % 232.54/232.69 (E(f1(f1(f2(x24621,x24622),f1(x24623,x24624)),x24625),f1(x24625,f1(f1(x24624,x24623),f2(x24622,x24621))))), % 232.54/232.69 inference(scs_inference,[],[2327,2])). % 232.54/232.69 cnf(2484,plain, % 232.54/232.69 (E(f1(x24841,f2(f2(x24842,x24843),f1(x24844,x24845))),f1(f2(f1(x24845,x24844),f2(x24842,x24843)),x24841))), % 232.54/232.69 inference(scs_inference,[],[2430,2])). % 232.54/232.69 cnf(2488,plain, % 232.54/232.69 (E(f5(f2(f1(x24881,x24882),f2(x24883,x24884)),f2(x24885,x24886)),f5(f2(f2(x24884,x24883),f1(x24881,x24882)),f2(x24886,x24885)))), % 232.54/232.69 inference(scs_inference,[],[17,113,713,340,2430,2,13,3])). % 232.54/232.69 cnf(2498,plain, % 232.54/232.69 (E(f1(x24981,f2(f2(x24982,x24983),f1(x24984,x24985))),f1(f2(f1(x24985,x24984),f2(x24983,x24982)),x24981))), % 232.54/232.69 inference(scs_inference,[],[17,113,715,2488,346,2,13,3])). % 232.54/232.69 cnf(2584,plain, % 232.54/232.69 (E(f1(x25841,f2(f1(x25842,x25843),f2(x25844,x25845))),f1(f2(f2(x25845,x25844),f1(x25842,x25843)),x25841))), % 232.54/232.69 inference(scs_inference,[],[17,18,726,398,2498,2,13,3])). % 232.54/232.69 cnf(2658,plain, % 232.54/232.69 (E(f1(x26581,f2(f1(x26582,x26583),f2(x26584,x26585))),f1(f2(f2(x26585,x26584),f1(x26583,x26582)),x26581))), % 232.54/232.69 inference(scs_inference,[],[17,113,746,415,13,3])). % 232.54/232.69 cnf(2664,plain, % 232.54/232.69 (E(f2(x26641,f2(f1(x26642,x26642),f2(x26643,x26644))),f2(f2(f2(x26643,x26644),f1(x26642,x26642)),x26641))), % 232.54/232.69 inference(scs_inference,[],[17,18,113,119,746,747,415,13,3,12,22])). % 232.54/232.69 cnf(2673,plain, % 232.54/232.69 (E(f5(f1(f2(x26731,x26732),f1(x26733,x26734)),f2(x26735,x26736)),f5(f1(f1(x26734,x26733),f2(x26732,x26731)),f2(x26736,x26735)))), % 232.54/232.69 inference(scs_inference,[],[18,113,747,2664,427,2,13,3])). % 232.54/232.69 cnf(2683,plain, % 232.54/232.69 (E(f2(x26831,f1(f2(x26832,x26833),f1(x26834,x26835))),f2(f1(f1(x26835,x26834),f2(x26832,x26833)),x26831))), % 232.54/232.69 inference(scs_inference,[],[18,263,750,2673,428,2,13,3])). % 232.54/232.69 cnf(2691,plain, % 232.54/232.69 (P1(f1(f2(f2(x26911,x26912),x26913),x26914),f1(x26914,f2(f2(x26912,x26911),x26913)))), % 232.54/232.69 inference(scs_inference,[],[17,752,2683,2,13])). % 232.54/232.69 cnf(2732,plain, % 232.54/232.69 (~P2(x27321,f2(x27322,x27323))+P2(x27321,f1(x27324,f1(x27325,f2(x27323,x27322))))), % 232.54/232.69 inference(scs_inference,[],[25,720])). % 232.54/232.69 cnf(2813,plain, % 232.54/232.69 (P1(f1(f2(x28131,f1(x28132,x28133)),x28134),f1(x28134,f2(x28131,f1(x28133,x28132))))), % 232.54/232.69 inference(scs_inference,[],[17,776,13])). % 232.54/232.69 cnf(2853,plain, % 232.54/232.69 (P1(f1(x28531,f5(x28532,f1(x28533,x28534))),f1(f5(x28532,f1(x28534,x28533)),x28531))), % 232.54/232.69 inference(scs_inference,[],[17,786,13])). % 232.54/232.69 cnf(2989,plain, % 232.54/232.69 (P1(f1(f1(f2(x29891,x29892),f1(x29893,x29894)),x29895),f1(x29895,f1(f1(x29893,x29894),f2(x29892,x29891))))), % 232.54/232.69 inference(scs_inference,[],[17,838,13])). % 232.54/232.69 cnf(2991,plain, % 232.54/232.69 (E(f1(x29911,x29912),f1(x29912,x29911))), % 232.54/232.69 inference(rename_variables,[],[17])). % 232.54/232.69 cnf(2992,plain, % 232.54/232.69 (P1(f1(f5(f2(x29921,x29922),x29923),x29924),f1(x29924,f5(f2(x29922,x29921),x29923)))), % 232.54/232.69 inference(scs_inference,[],[17,2991,838,839,13,12])). % 232.54/232.69 cnf(3204,plain, % 232.54/232.69 (E(f1(f1(x32041,x32042),x32043),f1(f1(x32042,x32041),x32043))), % 232.54/232.69 inference(rename_variables,[],[39])). % 232.54/232.69 cnf(3205,plain, % 232.54/232.69 (P1(f1(f1(x32051,x32052),x32053),f1(f1(x32054,f1(x32053,f1(x32052,x32051))),x32055))), % 232.54/232.69 inference(scs_inference,[],[39,3204,2187,678,13,12])). % 232.54/232.69 cnf(3251,plain, % 232.54/232.69 (E(f1(f1(x32511,x32512),x32513),f1(f1(x32512,x32511),x32513))), % 232.54/232.69 inference(rename_variables,[],[39])). % 232.54/232.69 cnf(3252,plain, % 232.54/232.69 (P1(f1(f1(x32521,x32522),f2(f2(x32523,x32524),f1(x32525,x32526))),f1(f2(f1(x32526,x32525),f2(x32523,x32524)),f1(x32522,x32521)))), % 232.54/232.69 inference(scs_inference,[],[39,3251,786,2403,13,12])). % 232.54/232.69 cnf(3262,plain, % 232.54/232.69 (P1(f1(f2(f1(x32621,x32622),f2(x32623,x32624)),f1(x32625,x32626)),f1(f1(x32626,x32625),f2(f2(x32624,x32623),f1(x32622,x32621))))), % 232.54/232.69 inference(scs_inference,[],[39,2382,13])). % 232.54/232.69 cnf(3264,plain, % 232.54/232.69 (E(f1(f1(x32641,x32642),x32643),f1(f1(x32642,x32641),x32643))), % 232.54/232.69 inference(rename_variables,[],[39])). % 232.54/232.69 cnf(3265,plain, % 232.54/232.69 (P1(f1(f1(x32651,x32652),f5(x32653,f1(x32654,x32655))),f1(f5(x32653,f1(x32655,x32654)),f1(x32652,x32651)))), % 232.54/232.69 inference(scs_inference,[],[39,3264,2382,2853,13,12])). % 232.54/232.69 cnf(3285,plain, % 232.54/232.69 (P1(f1(f2(x32851,f2(x32852,x32853)),f1(x32854,x32855)),f1(f1(x32855,x32854),f2(x32851,f2(x32853,x32852))))), % 232.54/232.69 inference(scs_inference,[],[39,2427,13])). % 232.54/232.69 cnf(3296,plain, % 232.54/232.69 (P1(f1(f2(f2(x32961,x32962),x32963),f1(x32964,x32965)),f1(f1(x32965,x32964),f2(f2(x32962,x32961),x32963)))), % 232.54/232.69 inference(scs_inference,[],[39,2691,13])). % 232.54/232.69 cnf(3308,plain, % 232.54/232.69 (P1(f1(f2(x33081,f1(x33082,x33083)),f1(x33084,x33085)),f1(f1(x33085,x33084),f2(x33081,f1(x33083,x33082))))), % 232.54/232.69 inference(scs_inference,[],[39,2813,13])). % 232.54/232.69 cnf(3320,plain, % 232.54/232.69 (P1(f1(f1(f2(x33201,x33202),f1(x33203,x33204)),f1(x33205,x33206)),f1(f1(x33206,x33205),f1(f1(x33203,x33204),f2(x33202,x33201))))), % 232.54/232.69 inference(scs_inference,[],[39,2989,13])). % 232.54/232.69 cnf(3335,plain, % 232.54/232.69 (E(f1(f1(x33351,x33352),x33353),f1(f1(x33352,x33351),x33353))), % 232.54/232.69 inference(rename_variables,[],[39])). % 232.54/232.69 cnf(3341,plain, % 232.54/232.69 (E(f1(f5(f2(x33411,x33411),x33412),f1(x33413,x33414)),f1(f1(x33414,x33413),f5(f2(x33411,x33411),x33412)))), % 232.54/232.69 inference(scs_inference,[],[39,3335,17,42,2992,3262,2252,13,12,3,22])). % 232.54/232.69 cnf(3348,plain, % 232.54/232.69 (E(f1(x33481,x33482),f1(x33482,x33481))), % 232.54/232.69 inference(rename_variables,[],[17])). % 232.54/232.69 cnf(3351,plain, % 232.54/232.69 (E(f1(f1(x33511,x33512),f1(f1(x33513,x33514),f2(x33515,x33516))),f1(f1(f2(x33515,x33516),f1(x33514,x33513)),f1(x33512,x33511)))), % 232.54/232.69 inference(scs_inference,[],[39,17,3348,3252,3285,3341,2290,2,13,12,3])). % 232.54/232.69 cnf(3358,plain, % 232.54/232.69 (E(f1(f1(x33581,x33582),x33583),f1(f1(x33582,x33581),x33583))), % 232.54/232.69 inference(rename_variables,[],[39])). % 232.54/232.69 cnf(3361,plain, % 232.54/232.69 (E(f1(f1(f1(x33611,x33612),f2(x33613,x33614)),x33615),f1(x33615,f1(f1(x33612,x33611),f2(x33614,x33613))))), % 232.54/232.69 inference(scs_inference,[],[39,3358,17,3296,3351,665,2462,2,13,12,3])). % 232.54/232.69 cnf(3368,plain, % 232.54/232.69 (E(f1(f1(x33681,x33682),x33683),f1(f1(x33682,x33681),x33683))), % 232.54/232.69 inference(rename_variables,[],[39])). % 232.54/232.69 cnf(3371,plain, % 232.54/232.69 (E(f1(f1(x33711,x33712),f2(f2(x33713,x33714),f1(x33715,x33716))),f1(f2(f1(x33716,x33715),f2(x33713,x33714)),f1(x33712,x33711)))), % 232.54/232.69 inference(scs_inference,[],[39,3368,17,3308,3361,668,2484,2,13,12,3])). % 232.54/232.69 cnf(3378,plain, % 232.54/232.69 (E(f1(f1(x33781,x33782),x33783),f1(f1(x33782,x33781),x33783))), % 232.54/232.69 inference(rename_variables,[],[39])). % 232.54/232.69 cnf(3380,plain, % 232.54/232.69 (E(f1(f1(x33801,x33802),x33803),f1(f1(x33802,x33801),x33803))), % 232.54/232.69 inference(rename_variables,[],[39])). % 232.54/232.69 cnf(3381,plain, % 232.54/232.69 (E(f1(f1(x33811,x33812),f2(f1(x33813,x33814),f2(x33815,x33816))),f1(f2(f2(x33816,x33815),f1(x33813,x33814)),f1(x33812,x33811)))), % 232.54/232.69 inference(scs_inference,[],[39,3378,3380,3320,3371,723,2584,2,13,12,3])). % 232.54/232.69 cnf(3384,plain, % 232.54/232.69 (E(f1(f1(f1(x33841,x33842),f2(x33843,x33843)),f1(x33844,x33845)),f1(f1(x33845,x33844),f1(f1(x33841,x33842),f2(x33843,x33843))))), % 232.54/232.69 inference(scs_inference,[],[39,3378,3380,42,3320,3371,723,2584,2,13,12,3,22])). % 232.54/232.69 cnf(3413,plain, % 232.54/232.69 (E(f1(f1(x34131,x34132),x34133),f1(f1(x34132,x34131),x34133))), % 232.54/232.69 inference(rename_variables,[],[39])). % 232.54/232.69 cnf(3416,plain, % 232.54/232.69 (E(f1(f1(x34161,x34162),x34163),f1(f1(x34162,x34161),x34163))), % 232.54/232.69 inference(rename_variables,[],[39])). % 232.54/232.69 cnf(3417,plain, % 232.54/232.69 (E(f1(f1(x34171,x34172),f2(f1(x34173,x34174),f2(x34175,x34176))),f1(f2(f2(x34176,x34175),f1(x34174,x34173)),f1(x34172,x34171)))), % 232.54/232.69 inference(scs_inference,[],[39,3413,3416,3384,772,777,2658,2,13,12,3])). % 232.54/232.69 cnf(4990,plain, % 232.54/232.69 (E(f1(f2(f2(x49901,x49902),f1(x49903,x49904)),f1(x49905,x49906)),f1(f2(f1(x49904,x49903),f2(x49901,x49902)),f1(x49906,x49905)))), % 232.54/232.69 inference(scs_inference,[],[17,212,96,95,240,221,51,3371,3265,4,5,6,7,8,9,10,11,22,3])). % 232.54/232.69 cnf(5092,plain, % 232.54/232.69 (E(f1(f2(f1(x50921,x50922),f2(x50923,x50924)),f1(x50925,x50926)),f1(f2(f2(x50924,x50923),f1(x50921,x50922)),f1(x50926,x50925)))), % 232.54/232.69 inference(scs_inference,[],[17,251,95,117,221,102,250,3381,4990,4,7,9,11,5,8,6,10,2,3])). % 232.54/232.69 cnf(5219,plain, % 232.54/232.69 (E(f1(f2(f1(x52191,x52192),f2(x52193,x52194)),f1(x52195,x52196)),f1(f2(f2(x52194,x52193),f1(x52192,x52191)),f1(x52196,x52195)))), % 232.54/232.69 inference(scs_inference,[],[17,95,221,240,102,250,258,3417,5092,9,8,4,11,7,6,10,5,2,3])). % 232.54/232.69 cnf(5220,plain, % 232.54/232.69 (E(f1(x52201,x52202),f1(x52202,x52201))), % 232.54/232.69 inference(rename_variables,[],[17])). % 232.54/232.69 cnf(5223,plain, % 232.54/232.69 (E(f1(x52231,x52232),f1(x52232,x52231))), % 232.54/232.69 inference(rename_variables,[],[17])). % 232.54/232.69 cnf(5234,plain, % 232.54/232.69 (P2(f5(f2(f1(a6,a3),a3),a3),f2(f1(a6,a3),a3))), % 232.54/232.69 inference(scs_inference,[],[17,5220,5223,95,221,240,102,250,258,590,3205,3320,3417,5092,9,8,4,11,7,6,10,5,2,3,12,13,30,2136,31,2088,33])). % 232.54/232.69 cnf(5362,plain, % 232.54/232.69 (E(f5(x53621,f1(f1(x53622,x53623),f2(x53624,x53625))),f5(x53621,f1(f1(x53623,x53622),f2(x53625,x53624))))), % 232.54/232.69 inference(rename_variables,[],[186])). % 232.54/232.69 cnf(5387,plain, % 232.54/232.69 ($false), % 232.54/232.69 inference(scs_inference,[],[186,5362,17,864,102,590,3285,202,5234,5219,1927,2072,2063,649,2732,667,1898,720,664,692,1825,2076,2048,1909,2050,733,1651,543,1929,50,2140,2164,1907,619,653,655,689,2169,2078,1114,828,2065,25,26,6,4,10,9,11,8,5,7,2,33,1022,2086,2136,2088,31,15,14,3,12,13,1880,1769,940,1087,1092,998,557,546,547,23,27]), % 232.54/232.69 ['proof']). % 232.54/232.69 % SZS output end Proof % 232.54/232.69 % Total time :231.720000s %------------------------------------------------------------------------------