%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SET956+1 : TPTP v8.2.0. Released v3.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:23:05 EDT 2024 % Result : Theorem 116.80s 116.92s % Output : CNFRefutation 116.89s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.13 % Problem : SET956+1 : TPTP v8.2.0. Released v3.2.0. % 0.03/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.13/0.34 % Computer : n028.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Sun Jun 23 16:39:23 EDT 2024 % 0.13/0.34 % CPUTime : % 0.54/0.61 start to proof:theBenchmark % 116.80/116.91 %------------------------------------------- % 116.80/116.91 % File :CSE---1.7 % 116.80/116.91 % Problem :theBenchmark % 116.80/116.91 % Transform :cnf % 116.80/116.91 % Format :tptp:raw % 116.80/116.91 % Command :java -jar mcs_scs.jar %d %s % 116.80/116.91 % 116.80/116.91 % Result :Theorem 116.170000s % 116.80/116.91 % Output :CNFRefutation 116.170000s % 116.80/116.91 %------------------------------------------- % 116.80/116.92 %------------------------------------------------------------------------------ % 116.80/116.92 % File : SET956+1 : TPTP v8.2.0. Released v3.2.0. % 116.80/116.92 % Domain : Set theory % 116.80/116.92 % Problem : Basic properties of sets, theorem 109 % 116.80/116.92 % Version : [Urb06] axioms : Especial. % 116.80/116.92 % English : ( subset(A,cartesian_product2(B,C)) & % 116.80/116.92 % ( in(ordered_pair(E,F),A) => in(ordered_pair(E,F),D) ) ) % 116.80/116.92 % => subset(A,D) % 116.80/116.92 % 116.80/116.92 % Refs : [Byl90] Bylinski (1990), Some Basic Properties of Sets % 116.80/116.92 % : [Urb06] Urban (2006), Email to G. Sutcliffe % 116.80/116.92 % Source : [Urb06] % 116.80/116.92 % Names : zfmisc_1__t109_zfmisc_1 [Urb06] % 116.80/116.92 % 116.80/116.92 % Status : Theorem % 116.80/116.92 % Rating : 0.19 v8.2.0, 0.22 v8.1.0, 0.28 v7.4.0, 0.20 v7.3.0, 0.24 v7.2.0, 0.21 v7.1.0, 0.22 v7.0.0, 0.23 v6.4.0, 0.35 v6.3.0, 0.21 v6.2.0, 0.20 v6.1.0, 0.23 v6.0.0, 0.09 v5.5.0, 0.22 v5.4.0, 0.21 v5.3.0, 0.37 v5.2.0, 0.20 v5.1.0, 0.19 v5.0.0, 0.21 v4.1.0, 0.26 v4.0.0, 0.25 v3.7.0, 0.20 v3.5.0, 0.21 v3.4.0, 0.26 v3.3.0, 0.21 v3.2.0 % 116.80/116.92 % Syntax : Number of formulae : 10 ( 6 unt; 0 def) % 116.80/116.92 % Number of atoms : 20 ( 3 equ) % 116.80/116.92 % Maximal formula atoms : 5 ( 2 avg) % 116.80/116.92 % Number of connectives : 15 ( 5 ~; 0 |; 5 &) % 116.80/116.92 % ( 1 <=>; 4 =>; 0 <=; 0 <~>) % 116.80/116.92 % Maximal formula depth : 13 ( 5 avg) % 116.80/116.92 % Maximal term depth : 3 ( 1 avg) % 116.80/116.92 % Number of predicates : 4 ( 3 usr; 0 prp; 1-2 aty) % 116.80/116.92 % Number of functors : 4 ( 4 usr; 0 con; 1-2 aty) % 116.80/116.92 % Number of variables : 27 ( 25 !; 2 ?) % 116.80/116.92 % SPC : FOF_THM_RFO_SEQ % 116.80/116.92 % 116.80/116.92 % Comments : Translated by MPTP 0.2 from the original problem in the Mizar % 116.80/116.92 % library, www.mizar.org % 116.80/116.92 %------------------------------------------------------------------------------ % 116.80/116.92 fof(antisymmetry_r2_hidden,axiom, % 116.80/116.92 ! [A,B] : % 116.80/116.92 ( in(A,B) % 116.80/116.92 => ~ in(B,A) ) ). % 116.80/116.92 % 116.80/116.92 fof(commutativity_k2_tarski,axiom, % 116.80/116.92 ! [A,B] : unordered_pair(A,B) = unordered_pair(B,A) ). % 116.80/116.92 % 116.80/116.92 fof(d3_tarski,axiom, % 116.80/116.92 ! [A,B] : % 116.80/116.92 ( subset(A,B) % 116.80/116.92 <=> ! [C] : % 116.80/116.92 ( in(C,A) % 116.80/116.92 => in(C,B) ) ) ). % 116.80/116.92 % 116.80/116.92 fof(d5_tarski,axiom, % 116.80/116.92 ! [A,B] : ordered_pair(A,B) = unordered_pair(unordered_pair(A,B),singleton(A)) ). % 116.80/116.92 % 116.80/116.92 fof(fc1_zfmisc_1,axiom, % 116.80/116.92 ! [A,B] : ~ empty(ordered_pair(A,B)) ). % 116.80/116.92 % 116.80/116.92 fof(rc1_xboole_0,axiom, % 116.80/116.92 ? [A] : empty(A) ). % 116.80/116.92 % 116.80/116.92 fof(rc2_xboole_0,axiom, % 116.80/116.92 ? [A] : ~ empty(A) ). % 116.80/116.92 % 116.80/116.92 fof(reflexivity_r1_tarski,axiom, % 116.80/116.92 ! [A,B] : subset(A,A) ). % 116.80/116.92 % 116.80/116.92 fof(t103_zfmisc_1,axiom, % 116.80/116.92 ! [A,B,C,D] : % 116.80/116.92 ~ ( subset(A,cartesian_product2(B,C)) % 116.80/116.92 & in(D,A) % 116.80/116.92 & ! [E,F] : % 116.80/116.92 ~ ( in(E,B) % 116.80/116.92 & in(F,C) % 116.80/116.92 & D = ordered_pair(E,F) ) ) ). % 116.80/116.92 % 116.80/116.92 fof(t109_zfmisc_1,conjecture, % 116.80/116.92 ! [A,B,C,D] : % 116.80/116.92 ( ( subset(A,cartesian_product2(B,C)) % 116.80/116.92 & ! [E,F] : % 116.80/116.92 ( in(ordered_pair(E,F),A) % 116.80/116.92 => in(ordered_pair(E,F),D) ) ) % 116.80/116.92 => subset(A,D) ) ). % 116.80/116.92 % 116.80/116.92 %------------------------------------------------------------------------------ % 116.80/116.92 %------------------------------------------- % 116.80/116.92 % Proof found % 116.80/116.92 % SZS status Theorem for theBenchmark % 116.80/116.92 % SZS output start Proof % 116.89/116.93 %ClaNum:38(EqnAxiom:23) % 116.89/116.93 %VarNum:73(SingletonVarNum:28) % 116.89/116.93 %MaxLitNum:3 % 116.89/116.93 %MaxfuncDepth:3 % 116.89/116.93 %SharedTerms:11 % 116.89/116.93 %goalClause: 27 29 35 % 116.89/116.93 %singleGoalClaCount:2 % 116.89/116.93 [24]P1(a1) % 116.89/116.93 [28]~P1(a6) % 116.89/116.93 [29]~P2(a5,a11) % 116.89/116.93 [27]P2(a5,f2(a9,a10)) % 116.89/116.93 [25]P2(x251,x251) % 116.89/116.93 [26]E(f4(x261,x262),f4(x262,x261)) % 116.89/116.93 [30]~P1(f4(f4(x301,x302),f12(x301))) % 116.89/116.93 [31]~P3(x312,x311)+~P3(x311,x312) % 116.89/116.93 [32]P2(x321,x322)+P3(f3(x321,x322),x321) % 116.89/116.93 [34]P2(x341,x342)+~P3(f3(x341,x342),x342) % 116.89/116.93 [35]P3(f4(f4(x351,x352),f12(x351)),a11)+~P3(f4(f4(x351,x352),f12(x351)),a5) % 116.89/116.93 [33]~P2(x333,x332)+P3(x331,x332)+~P3(x331,x333) % 116.89/116.93 [36]~P3(x364,x361)+~P2(x361,f2(x362,x363))+P3(f7(x361,x362,x363,x364),x362) % 116.89/116.93 [37]~P3(x374,x371)+~P2(x371,f2(x372,x373))+P3(f8(x371,x372,x373,x374),x373) % 116.89/116.93 [38]~P3(x384,x381)+~P2(x381,f2(x382,x383))+E(f4(f4(f7(x381,x382,x383,x384),f8(x381,x382,x383,x384)),f12(f7(x381,x382,x383,x384))),x384) % 116.89/116.93 %EqnAxiom % 116.89/116.93 [1]E(x11,x11) % 116.89/116.93 [2]E(x22,x21)+~E(x21,x22) % 116.89/116.93 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 116.89/116.93 [4]~E(x41,x42)+E(f4(x41,x43),f4(x42,x43)) % 116.89/116.93 [5]~E(x51,x52)+E(f4(x53,x51),f4(x53,x52)) % 116.89/116.93 [6]~E(x61,x62)+E(f2(x61,x63),f2(x62,x63)) % 116.89/116.93 [7]~E(x71,x72)+E(f2(x73,x71),f2(x73,x72)) % 116.89/116.93 [8]~E(x81,x82)+E(f7(x81,x83,x84,x85),f7(x82,x83,x84,x85)) % 116.89/116.93 [9]~E(x91,x92)+E(f7(x93,x91,x94,x95),f7(x93,x92,x94,x95)) % 116.89/116.93 [10]~E(x101,x102)+E(f7(x103,x104,x101,x105),f7(x103,x104,x102,x105)) % 116.89/116.93 [11]~E(x111,x112)+E(f7(x113,x114,x115,x111),f7(x113,x114,x115,x112)) % 116.89/116.93 [12]~E(x121,x122)+E(f12(x121),f12(x122)) % 116.89/116.93 [13]~E(x131,x132)+E(f8(x131,x133,x134,x135),f8(x132,x133,x134,x135)) % 116.89/116.93 [14]~E(x141,x142)+E(f8(x143,x141,x144,x145),f8(x143,x142,x144,x145)) % 116.89/116.93 [15]~E(x151,x152)+E(f8(x153,x154,x151,x155),f8(x153,x154,x152,x155)) % 116.89/116.93 [16]~E(x161,x162)+E(f8(x163,x164,x165,x161),f8(x163,x164,x165,x162)) % 116.89/116.93 [17]~E(x171,x172)+E(f3(x171,x173),f3(x172,x173)) % 116.89/116.93 [18]~E(x181,x182)+E(f3(x183,x181),f3(x183,x182)) % 116.89/116.93 [19]~P1(x191)+P1(x192)+~E(x191,x192) % 116.89/116.93 [20]P2(x202,x203)+~E(x201,x202)+~P2(x201,x203) % 116.89/116.93 [21]P2(x213,x212)+~E(x211,x212)+~P2(x213,x211) % 116.89/116.93 [22]P3(x222,x223)+~E(x221,x222)+~P3(x221,x223) % 116.89/116.93 [23]P3(x233,x232)+~E(x231,x232)+~P3(x233,x231) % 116.89/116.93 % 116.89/116.93 %------------------------------------------- % 116.89/116.95 cnf(42,plain, % 116.89/116.95 (~P1(f4(f12(x421),f4(x421,x422)))), % 116.89/116.95 inference(scs_inference,[],[27,29,25,26,30,20,21,19])). % 116.89/116.95 cnf(48,plain, % 116.89/116.95 (E(f4(f4(x481,x482),x483),f4(f4(x482,x481),x483))), % 116.89/116.95 inference(scs_inference,[],[26,2,4])). % 116.89/116.95 cnf(49,plain, % 116.89/116.95 (~P1(f4(f4(x491,x492),f12(x492)))), % 116.89/116.95 inference(scs_inference,[],[48,30,19])). % 116.89/116.95 cnf(51,plain, % 116.89/116.95 (~P3(a5,f3(a5,a11))), % 116.89/116.95 inference(scs_inference,[],[29,31,32])). % 116.89/116.95 cnf(53,plain, % 116.89/116.95 (~E(x531,a5)+~P3(f3(x531,a11),a11)), % 116.89/116.95 inference(scs_inference,[],[29,34,20])). % 116.89/116.95 cnf(54,plain, % 116.89/116.95 (~P3(f3(a5,a11),a11)), % 116.89/116.95 inference(equality_inference,[],[53])). % 116.89/116.95 cnf(72,plain, % 116.89/116.95 (P3(f3(a5,a11),f2(a9,a10))), % 116.89/116.95 inference(scs_inference,[],[27,29,33,32])). % 116.89/116.95 cnf(75,plain, % 116.89/116.95 (P3(x751,f2(a9,a10))+~E(f3(a5,a11),x751)), % 116.89/116.95 inference(scs_inference,[],[72,31,22])). % 116.89/116.95 cnf(83,plain, % 116.89/116.95 (P3(f7(a5,a9,a10,f3(a5,a11)),a9)), % 116.89/116.95 inference(scs_inference,[],[27,29,36,32])). % 116.89/116.95 cnf(91,plain, % 116.89/116.95 (P3(x911,a9)+~E(f7(a5,a9,a10,f3(a5,a11)),x911)), % 116.89/116.95 inference(scs_inference,[],[83,22])). % 116.89/116.95 cnf(103,plain, % 116.89/116.95 (P3(f8(a5,a9,a10,f3(a5,a11)),a10)), % 116.89/116.95 inference(scs_inference,[],[27,29,37,32])). % 116.89/116.95 cnf(106,plain, % 116.89/116.95 (P3(x1061,a10)+~E(f8(a5,a9,a10,f3(a5,a11)),x1061)), % 116.89/116.95 inference(scs_inference,[],[103,31,22])). % 116.89/116.95 cnf(143,plain, % 116.89/116.95 (E(f7(x1431,x1432,x1433,f4(f4(x1434,x1435),x1436)),f7(x1431,x1432,x1433,f4(f4(x1435,x1434),x1436)))), % 116.89/116.95 inference(scs_inference,[],[48,2,11])). % 116.89/116.95 cnf(146,plain, % 116.89/116.95 (E(f8(x1461,f4(x1462,x1463),x1464,x1465),f8(x1461,f4(x1463,x1462),x1464,x1465))), % 116.89/116.95 inference(scs_inference,[],[26,2,14])). % 116.89/116.95 cnf(153,plain, % 116.89/116.95 (P2(f4(f4(x1531,x1532),x1533),f4(f4(x1532,x1531),x1533))), % 116.89/116.95 inference(scs_inference,[],[48,25,2,20])). % 116.89/116.95 cnf(156,plain, % 116.89/116.95 (P2(f8(x1561,f4(x1562,x1563),x1564,x1565),f8(x1561,f4(x1563,x1562),x1564,x1565))), % 116.89/116.95 inference(scs_inference,[],[25,146,20])). % 116.89/116.95 cnf(174,plain, % 116.89/116.95 (E(f8(x1741,x1742,f4(x1743,x1744),x1745),f8(x1741,x1742,f4(x1744,x1743),x1745))), % 116.89/116.95 inference(scs_inference,[],[26,2,15])). % 116.89/116.95 cnf(175,plain, % 116.89/116.95 (P2(f4(f4(x1751,x1752),x1753),f4(x1753,f4(x1752,x1751)))), % 116.89/116.95 inference(scs_inference,[],[26,153,21])). % 116.89/116.95 cnf(185,plain, % 116.89/116.95 (E(f4(x1851,x1852),f4(x1852,x1851))), % 116.89/116.95 inference(rename_variables,[],[26])). % 116.89/116.95 cnf(186,plain, % 116.89/116.95 (P2(f4(x1861,f4(x1862,x1863)),f4(f4(x1863,x1862),x1861))), % 116.89/116.95 inference(scs_inference,[],[26,185,175,20,21])). % 116.89/116.95 cnf(197,plain, % 116.89/116.95 (E(f3(f8(x1971,f4(x1972,x1973),x1974,x1975),x1976),f3(f8(x1971,f4(x1973,x1972),x1974,x1975),x1976))), % 116.89/116.95 inference(scs_inference,[],[146,2,17])). % 116.89/116.95 cnf(198,plain, % 116.89/116.95 (E(f3(x1981,f8(x1982,f4(x1983,x1984),x1985,x1986)),f3(x1981,f8(x1982,f4(x1984,x1983),x1985,x1986)))), % 116.89/116.95 inference(scs_inference,[],[146,2,18])). % 116.89/116.95 cnf(215,plain, % 116.89/116.95 (P2(f8(x2151,f4(x2152,x2153),f4(x2154,x2155),x2156),f8(x2151,f4(x2153,x2152),f4(x2155,x2154),x2156))), % 116.89/116.95 inference(scs_inference,[],[174,156,21])). % 116.89/116.95 cnf(252,plain, % 116.89/116.95 (E(x2521,f4(f4(f7(a5,a9,a10,x2521),f8(a5,a9,a10,x2521)),f12(f7(a5,a9,a10,x2521))))+~P3(x2521,a5)), % 116.89/116.95 inference(scs_inference,[],[27,2,38])). % 116.89/116.95 cnf(253,plain, % 116.89/116.95 (~P3(a1,a5)), % 116.89/116.95 inference(scs_inference,[],[24,30,252,19])). % 116.89/116.95 cnf(262,plain, % 116.89/116.95 (~P2(f2(a9,a10),a11)), % 116.89/116.95 inference(scs_inference,[],[72,54,33])). % 116.89/116.95 cnf(298,plain, % 116.89/116.95 (E(f4(x2981,f4(x2982,x2983)),f4(x2981,f4(x2983,x2982)))), % 116.89/116.95 inference(scs_inference,[],[26,2,5])). % 116.89/116.95 cnf(325,plain, % 116.89/116.95 (E(f4(f4(x3251,f4(x3252,x3253)),x3254),f4(f4(x3251,f4(x3253,x3252)),x3254))), % 116.89/116.95 inference(scs_inference,[],[298,2,4])). % 116.89/116.95 cnf(328,plain, % 116.89/116.95 (E(f3(a5,a11),f4(f4(f7(f2(a9,a10),a9,a10,f3(a5,a11)),f8(f2(a9,a10),a9,a10,f3(a5,a11))),f12(f7(f2(a9,a10),a9,a10,f3(a5,a11)))))), % 116.89/116.95 inference(scs_inference,[],[25,72,2,38])). % 116.89/116.95 cnf(329,plain, % 116.89/116.95 (E(f2(f4(x3291,x3292),x3293),f2(f4(x3292,x3291),x3293))), % 116.89/116.95 inference(scs_inference,[],[26,2,6])). % 116.89/116.95 cnf(347,plain, % 116.89/116.95 (E(f4(f8(x3471,x3472,f4(x3473,x3474),x3475),x3476),f4(f8(x3471,x3472,f4(x3474,x3473),x3475),x3476))), % 116.89/116.95 inference(scs_inference,[],[174,2,4])). % 116.89/116.95 cnf(356,plain, % 116.89/116.95 (P2(f2(f4(x3561,x3562),x3563),f2(f4(x3562,x3561),x3563))), % 116.89/116.95 inference(scs_inference,[],[329,25,20])). % 116.89/116.95 cnf(359,plain, % 116.89/116.95 (E(x3591,f4(f4(f7(f2(f4(x3592,x3593),x3594),f4(x3593,x3592),x3594,x3591),f8(f2(f4(x3592,x3593),x3594),f4(x3593,x3592),x3594,x3591)),f12(f7(f2(f4(x3592,x3593),x3594),f4(x3593,x3592),x3594,x3591))))+~P3(x3591,f2(f4(x3592,x3593),x3594))), % 116.89/116.95 inference(scs_inference,[],[356,2,38])). % 116.89/116.95 cnf(378,plain, % 116.89/116.95 (~P3(f2(a9,a10),f3(f2(a9,a10),a11))), % 116.89/116.95 inference(scs_inference,[],[262,31,32])). % 116.89/116.95 cnf(437,plain, % 116.89/116.95 (P3(f3(f2(a9,a10),a11),f2(a9,a10))), % 116.89/116.95 inference(scs_inference,[],[72,54,32,33])). % 116.89/116.95 cnf(438,plain, % 116.89/116.95 (P3(x4381,f2(a9,a10))+~E(f3(f2(a9,a10),a11),x4381)), % 116.89/116.95 inference(scs_inference,[],[437,22])). % 116.89/116.95 cnf(445,plain, % 116.89/116.95 (P3(f3(f2(a9,a10),a11),x4451)+~E(f2(a9,a10),x4451)), % 116.89/116.95 inference(scs_inference,[],[437,23])). % 116.89/116.95 cnf(446,plain, % 116.89/116.95 (~E(f3(f2(a9,a10),a11),f2(a9,a10))+~E(f2(a9,a10),f3(f2(a9,a10),a11))), % 116.89/116.95 inference(scs_inference,[],[437,378,23,22])). % 116.89/116.95 cnf(452,plain, % 116.89/116.95 (~E(f3(f2(a9,a10),a11),f2(a9,a10))), % 116.89/116.95 inference(scs_inference,[],[446,2])). % 116.89/116.95 cnf(461,plain, % 116.89/116.95 (E(f3(a5,a11),f4(f4(f7(a5,a9,a10,f3(a5,a11)),f8(a5,a9,a10,f3(a5,a11))),f12(f7(a5,a9,a10,f3(a5,a11)))))), % 116.89/116.95 inference(scs_inference,[],[29,32,252])). % 116.89/116.95 cnf(543,plain, % 116.89/116.95 (~E(x5431,a11)+~P3(f3(f2(a9,a10),x5431),x5431)), % 116.89/116.95 inference(scs_inference,[],[262,34,21])). % 116.89/116.95 cnf(544,plain, % 116.89/116.95 (~P3(f3(f2(a9,a10),a11),a11)), % 116.89/116.95 inference(equality_inference,[],[543])). % 116.89/116.95 cnf(825,plain, % 116.89/116.95 (~P3(f4(f4(x8251,x8252),x8253),x8254)+P3(f4(f4(x8252,x8251),x8253),x8254)), % 116.89/116.95 inference(scs_inference,[],[26,4,22])). % 116.89/116.95 cnf(826,plain, % 116.89/116.95 (~P3(x8261,f4(f4(x8262,x8263),x8264))+~P3(f4(f4(x8263,x8262),x8264),x8261)), % 116.89/116.95 inference(scs_inference,[],[825,31])). % 116.89/116.95 cnf(827,plain, % 116.89/116.95 (~P3(f2(a9,a10),f4(f4(x8271,x8272),x8273))+~E(f3(a5,a11),f4(f4(x8272,x8271),x8273))), % 116.89/116.95 inference(scs_inference,[],[826,75])). % 116.89/116.95 cnf(828,plain, % 116.89/116.95 (~E(f4(f4(x8281,x8282),x8283),f3(a5,a11))+~P3(f2(a9,a10),f4(f4(x8282,x8281),x8283))), % 116.89/116.95 inference(scs_inference,[],[827,2])). % 116.89/116.95 cnf(829,plain, % 116.89/116.95 (~E(f4(f4(x8291,x8292),x8293),f3(a5,a11))+~P3(f2(a9,a10),f4(f4(x8291,x8292),x8293))), % 116.89/116.95 inference(scs_inference,[],[48,828,3])). % 116.89/116.95 cnf(830,plain, % 116.89/116.95 (~E(f3(a5,a11),f4(f4(x8301,x8302),x8303))+~P3(f2(a9,a10),f4(f4(x8301,x8302),x8303))), % 116.89/116.95 inference(scs_inference,[],[829,2])). % 116.89/116.95 cnf(831,plain, % 116.89/116.95 (~P3(f2(a9,a10),f4(f4(f7(a5,a9,a10,f3(a5,a11)),f8(a5,a9,a10,f3(a5,a11))),f12(f7(a5,a9,a10,f3(a5,a11)))))+~P3(f3(a5,a11),a5)), % 116.89/116.95 inference(scs_inference,[],[830,252])). % 116.89/116.95 cnf(868,plain, % 116.89/116.95 (P2(f4(x8681,f8(x8682,f4(x8683,x8684),x8685,x8686)),f4(x8681,f8(x8682,f4(x8684,x8683),x8685,x8686)))), % 116.89/116.95 inference(scs_inference,[],[146,25,5,20])). % 116.89/116.95 cnf(995,plain, % 116.89/116.95 (P2(f3(f8(x9951,f4(x9952,x9953),x9954,x9955),x9956),f3(f8(x9951,f4(x9953,x9952),x9954,x9955),x9956))), % 116.89/116.95 inference(scs_inference,[],[146,25,17,20])). % 116.89/116.95 cnf(1002,plain, % 116.89/116.95 (~P3(x10021,f3(f8(x10022,f4(x10023,x10024),x10025,x10026),x10027))+P3(x10021,f3(f8(x10022,f4(x10024,x10023),x10025,x10026),x10027))), % 116.89/116.95 inference(scs_inference,[],[146,17,23])). % 116.89/116.95 cnf(1025,plain, % 116.89/116.95 (~E(x10251,f3(a5,a11))+P3(x10251,f2(a9,a10))), % 116.89/116.95 inference(scs_inference,[],[75,2])). % 116.89/116.95 cnf(1027,plain, % 116.89/116.95 (~E(f3(a5,a11),x10271)+P3(f7(f2(a9,a10),a9,a10,x10271),a9)), % 116.89/116.95 inference(scs_inference,[],[25,75,36])). % 116.89/116.95 cnf(1045,plain, % 116.89/116.95 (~E(f3(a5,a11),x10451)+P3(f8(f2(a9,a10),a9,a10,x10451),a10)), % 116.89/116.95 inference(scs_inference,[],[25,75,37])). % 116.89/116.95 cnf(1065,plain, % 116.89/116.95 (~E(f3(a5,a11),x10651)+E(f4(f4(f7(f2(a9,a10),a9,a10,x10651),f8(f2(a9,a10),a9,a10,x10651)),f12(f7(f2(a9,a10),a9,a10,x10651))),x10651)), % 116.89/116.95 inference(scs_inference,[],[25,75,38])). % 116.89/116.95 cnf(1066,plain, % 116.89/116.95 (E(f4(f4(f7(f2(a9,a10),a9,a10,f3(a5,a11)),f8(f2(a9,a10),a9,a10,f3(a5,a11))),f12(f7(f2(a9,a10),a9,a10,f3(a5,a11)))),f3(a5,a11))), % 116.89/116.95 inference(equality_inference,[],[1065])). % 116.89/116.95 cnf(1067,plain, % 116.89/116.95 (P3(f4(f4(f7(a5,a9,a10,f3(a5,a11)),f8(a5,a9,a10,f3(a5,a11))),f12(f7(a5,a9,a10,f3(a5,a11)))),f2(a9,a10))+~P3(f3(a5,a11),a5)), % 116.89/116.95 inference(scs_inference,[],[75,252])). % 116.89/116.95 cnf(1260,plain, % 116.89/116.95 (~E(x12601,f3(a5,a11))+P3(f7(f2(a9,a10),a9,a10,x12601),a9)), % 116.89/116.95 inference(scs_inference,[],[25,1025,36])). % 116.89/116.95 cnf(1264,plain, % 116.89/116.95 (~E(x12641,f3(a5,a11))+P3(f8(f2(a9,a10),a9,a10,x12641),a10)), % 116.89/116.95 inference(scs_inference,[],[25,1025,37])). % 116.89/116.95 cnf(1268,plain, % 116.89/116.95 (~P3(f2(a9,a10),x12681)+~E(x12681,f3(a5,a11))), % 116.89/116.95 inference(scs_inference,[],[1025,31])). % 116.89/116.95 cnf(1275,plain, % 116.89/116.95 (~E(f4(x12751,x12752),f3(a5,a11))+P3(f4(x12752,x12751),f2(a9,a10))), % 116.89/116.95 inference(scs_inference,[],[26,1025,3])). % 116.89/116.95 cnf(1383,plain, % 116.89/116.95 (~E(f2(a9,a10),f3(a5,a11))+~E(f3(a5,a11),f2(a9,a10))), % 116.89/116.95 inference(scs_inference,[],[1268,75])). % 116.89/116.95 cnf(1384,plain, % 116.89/116.95 (~E(f3(a5,a11),f2(a9,a10))), % 116.89/116.95 inference(scs_inference,[],[1383,2])). % 116.89/116.95 cnf(1419,plain, % 116.89/116.95 (~E(f2(a9,a10),f3(a5,a11))), % 116.89/116.95 inference(scs_inference,[],[1268,1025])). % 116.89/116.95 cnf(1421,plain, % 116.89/116.95 (~E(f4(x14211,x14212),f3(a5,a11))+~P3(f2(a9,a10),f4(x14212,x14211))), % 116.89/116.95 inference(scs_inference,[],[26,1268,3])). % 116.89/116.95 cnf(1643,plain, % 116.89/116.95 (~E(f3(a5,a11),x16431)+P3(f7(a5,a9,a10,x16431),a9)), % 116.89/116.95 inference(scs_inference,[],[91,11])). % 116.89/116.95 cnf(1829,plain, % 116.89/116.95 (~E(f3(a5,a11),x18291)+P3(f8(a5,a9,a10,x18291),a10)), % 116.89/116.95 inference(scs_inference,[],[106,16])). % 116.89/116.95 cnf(2231,plain, % 116.89/116.95 (~E(f3(f2(a9,a10),a11),x22311)+E(f4(f4(f7(f2(a9,a10),a9,a10,x22311),f8(f2(a9,a10),a9,a10,x22311)),f12(f7(f2(a9,a10),a9,a10,x22311))),x22311)), % 116.89/116.95 inference(scs_inference,[],[25,438,38])). % 116.89/116.95 cnf(2370,plain, % 116.89/116.95 (P3(f3(f2(a9,a10),a11),f3(f8(x23701,f4(x23702,x23703),x23704,x23705),x23706))+~E(f2(a9,a10),f3(f8(x23701,f4(x23703,x23702),x23704,x23705),x23706))), % 116.89/116.95 inference(scs_inference,[],[445,1002])). % 116.89/116.95 cnf(2371,plain, % 116.89/116.95 (~E(f3(f8(x23711,f4(x23712,x23713),x23714,x23715),x23716),a11)+~E(f2(a9,a10),f3(f8(x23711,f4(x23713,x23712),x23714,x23715),x23716))), % 116.89/116.95 inference(scs_inference,[],[544,2370,23])). % 116.89/116.95 cnf(2372,plain, % 116.89/116.96 (~E(f3(f8(x23721,f4(x23722,x23723),x23724,x23725),x23726),f2(a9,a10))+~E(f3(f8(x23721,f4(x23723,x23722),x23724,x23725),x23726),a11)), % 116.89/116.96 inference(scs_inference,[],[2371,2])). % 116.89/116.96 cnf(2373,plain, % 116.89/116.96 (~E(x23731,f2(a9,a10))+~E(f3(f8(x23732,f4(x23733,x23734),x23735,x23736),x23737),x23731)+~E(f3(f8(x23732,f4(x23734,x23733),x23735,x23736),x23737),a11)), % 116.89/116.96 inference(scs_inference,[],[2372,3])). % 116.89/116.96 cnf(2536,plain, % 116.89/116.96 (P3(f3(a5,a11),a5)), % 116.89/116.96 inference(scs_inference,[],[29,32])). % 116.89/116.96 cnf(2548,plain, % 116.89/116.96 (E(f7(x25481,x25482,x25483,f4(x25484,f4(x25485,x25486))),f7(x25481,x25482,x25483,f4(x25484,f4(x25486,x25485))))), % 116.89/116.96 inference(scs_inference,[],[29,298,26,329,32,12,4,5,6,7,17,18,8,9,10,11])). % 116.89/116.96 cnf(2554,plain, % 116.89/116.96 (~E(a1,a6)), % 116.89/116.96 inference(scs_inference,[],[28,452,24,29,298,26,329,32,12,4,5,6,7,17,18,8,9,10,11,13,14,15,16,2,19])). % 116.89/116.96 cnf(2564,plain, % 116.89/116.96 (~P3(f2(a9,a10),f4(f4(f7(a5,a9,a10,f3(a5,a11)),f8(a5,a9,a10,f3(a5,a11))),f12(f7(a5,a9,a10,f3(a5,a11)))))), % 116.89/116.96 inference(scs_inference,[],[2536,831])). % 116.89/116.96 cnf(2565,plain, % 116.89/116.96 (P3(f4(f4(f7(a5,a9,a10,f3(a5,a11)),f8(a5,a9,a10,f3(a5,a11))),f12(f7(a5,a9,a10,f3(a5,a11)))),f2(a9,a10))), % 116.89/116.96 inference(scs_inference,[],[2536,1067])). % 116.89/116.96 cnf(2572,plain, % 116.89/116.96 (E(f7(x25721,x25722,x25723,f4(x25724,x25725)),f7(x25721,x25722,x25723,f4(x25725,x25724)))), % 116.89/116.96 inference(scs_inference,[],[26,11])). % 116.89/116.96 cnf(2573,plain, % 116.89/116.96 (E(f7(x25731,f4(x25732,x25733),x25734,x25735),f7(x25731,f4(x25733,x25732),x25734,x25735))), % 116.89/116.96 inference(scs_inference,[],[26,11,9])). % 116.89/116.96 cnf(2574,plain, % 116.89/116.96 (E(f8(x25741,x25742,x25743,f4(x25744,x25745)),f8(x25741,x25742,x25743,f4(x25745,x25744)))), % 116.89/116.96 inference(scs_inference,[],[26,11,9,16])). % 116.89/116.96 cnf(2575,plain, % 116.89/116.96 (E(f2(x25751,f4(x25752,x25753)),f2(x25751,f4(x25753,x25752)))), % 116.89/116.96 inference(scs_inference,[],[26,11,9,16,7])). % 116.89/116.96 cnf(2576,plain, % 116.89/116.96 (E(f3(x25761,f4(x25762,x25763)),f3(x25761,f4(x25763,x25762)))), % 116.89/116.96 inference(scs_inference,[],[26,11,9,16,7,18])). % 116.89/116.96 cnf(2577,plain, % 116.89/116.96 (E(f8(f4(x25771,x25772),x25773,x25774,x25775),f8(f4(x25772,x25771),x25773,x25774,x25775))), % 116.89/116.96 inference(scs_inference,[],[26,11,9,16,7,18,13])). % 116.89/116.96 cnf(2579,plain, % 116.89/116.96 (E(f7(x25791,x25792,f4(x25793,x25794),x25795),f7(x25791,x25792,f4(x25794,x25793),x25795))), % 116.89/116.96 inference(scs_inference,[],[2554,26,11,9,16,7,18,13,2,10])). % 116.89/116.96 cnf(2580,plain, % 116.89/116.96 (E(f7(f4(x25801,x25802),x25803,x25804,x25805),f7(f4(x25802,x25801),x25803,x25804,x25805))), % 116.89/116.96 inference(scs_inference,[],[2554,26,11,9,16,7,18,13,2,10,8])). % 116.89/116.96 cnf(2581,plain, % 116.89/116.96 (~E(a1,f4(f12(x25811),f4(x25811,x25812)))), % 116.89/116.96 inference(scs_inference,[],[2554,42,24,26,11,9,16,7,18,13,2,10,8,19])). % 116.89/116.96 cnf(2584,plain, % 116.89/116.96 (~E(f4(f12(x25841),f4(x25841,x25842)),a1)), % 116.89/116.96 inference(scs_inference,[],[2581,2])). % 116.89/116.96 cnf(2585,plain, % 116.89/116.96 (~E(f4(f12(x25851),f4(x25852,x25851)),a1)), % 116.89/116.96 inference(scs_inference,[],[2581,298,2,3])). % 116.89/116.96 cnf(2595,plain, % 116.89/116.96 (~E(f4(f4(x25951,x25952),f12(x25951)),a1)), % 116.89/116.96 inference(scs_inference,[],[2584,26,3])). % 116.89/116.96 cnf(2598,plain, % 116.89/116.96 (~E(a1,f4(f4(x25981,x25982),f12(x25981)))), % 116.89/116.96 inference(scs_inference,[],[2584,49,24,26,3,19,2])). % 116.89/116.96 cnf(2601,plain, % 116.89/116.96 (~E(f3(a5,a11),a1)), % 116.89/116.96 inference(scs_inference,[],[2584,2576,2536,253,49,24,26,3,19,2,2373,22])). % 116.89/116.96 cnf(2605,plain, % 116.89/116.96 (~E(f4(f4(x26051,x26052),f12(x26052)),a1)), % 116.89/116.96 inference(scs_inference,[],[2601,2585,26,2,3])). % 116.89/116.96 cnf(2619,plain, % 116.89/116.96 (P2(f7(x26191,x26192,x26193,f4(x26194,x26195)),f7(x26191,x26192,x26193,f4(x26195,x26194)))), % 116.89/116.96 inference(scs_inference,[],[2572,25,21])). % 116.89/116.96 cnf(2635,plain, % 116.89/116.96 (P2(f7(x26351,f4(x26352,x26353),x26354,f4(x26355,x26356)),f7(x26351,f4(x26353,x26352),x26354,f4(x26356,x26355)))), % 116.89/116.96 inference(scs_inference,[],[2573,2619,20])). % 116.89/116.96 cnf(2667,plain, % 116.89/116.96 (P2(f7(x26671,f4(x26672,x26673),f4(x26674,x26675),f4(x26676,x26677)),f7(x26671,f4(x26673,x26672),f4(x26675,x26674),f4(x26677,x26676)))), % 116.89/116.96 inference(scs_inference,[],[2579,2635,21])). % 116.89/116.96 cnf(2695,plain, % 116.89/116.96 (P2(f7(x26951,f4(x26952,x26953),f4(x26954,x26955),f4(x26956,x26957)),f7(x26951,f4(x26953,x26952),f4(x26955,x26954),f4(x26957,x26956)))), % 116.89/116.96 inference(rename_variables,[],[2667])). % 116.89/116.96 cnf(2696,plain, % 116.89/116.96 (P2(f7(x26961,f4(x26962,x26963),f4(x26964,x26965),f4(x26966,x26967)),f7(x26961,f4(x26963,x26962),f4(x26965,x26964),f4(x26966,x26967)))), % 116.89/116.96 inference(scs_inference,[],[2580,2667,2695,2572,21,20])). % 116.89/116.96 cnf(2723,plain, % 116.89/116.96 (~P3(f8(x27231,x27232,x27233,f4(x27234,x27235)),x27236)+P3(f8(x27231,x27232,x27233,f4(x27235,x27234)),x27236)), % 116.89/116.96 inference(scs_inference,[],[2574,22])). % 116.89/116.96 cnf(2732,plain, % 116.89/116.96 (P2(f7(x27321,f4(x27322,x27323),f4(x27324,x27325),f4(x27326,x27327)),f7(x27321,f4(x27323,x27322),f4(x27324,x27325),f4(x27326,x27327)))), % 116.89/116.96 inference(scs_inference,[],[2696,2579,21])). % 116.89/116.96 cnf(2775,plain, % 116.89/116.96 (P2(f8(x27751,f4(x27752,x27753),f4(x27754,x27755),f4(x27756,x27757)),f8(x27751,f4(x27753,x27752),f4(x27755,x27754),f4(x27757,x27756)))), % 116.89/116.96 inference(scs_inference,[],[215,2574,21])). % 116.89/116.96 cnf(2790,plain, % 116.89/116.96 (P2(f8(f4(x27901,x27902),f4(x27903,x27904),f4(x27905,x27906),f4(x27907,x27908)),f8(f4(x27902,x27901),f4(x27904,x27903),f4(x27906,x27905),f4(x27908,x27907)))), % 116.89/116.96 inference(scs_inference,[],[2775,2577,20])). % 116.89/116.96 cnf(2800,plain, % 116.89/116.96 (~P3(x28001,f7(x28002,x28003,x28004,f4(x28005,x28006)))+P3(x28001,f7(x28002,x28003,x28004,f4(x28006,x28005)))), % 116.89/116.96 inference(scs_inference,[],[2572,23])). % 116.89/116.96 cnf(2823,plain, % 116.89/116.96 (P2(f7(f4(x28231,x28232),f4(x28233,x28234),f4(x28235,x28236),f4(x28237,x28238)),f7(f4(x28232,x28231),f4(x28234,x28233),f4(x28235,x28236),f4(x28237,x28238)))), % 116.89/116.96 inference(scs_inference,[],[2732,2580,21])). % 116.89/116.96 cnf(2845,plain, % 116.89/116.96 (~P3(a5,x28451)+~E(x28451,f3(a5,a11))), % 116.89/116.96 inference(scs_inference,[],[2790,51,2574,20,23])). % 116.89/116.96 cnf(2846,plain, % 116.89/116.96 (~E(f3(a5,a11),x28461)+~P3(a5,x28461)), % 116.89/116.96 inference(scs_inference,[],[2790,51,2574,20,23,2])). % 116.89/116.96 cnf(2894,plain, % 116.89/116.96 (P2(f7(f4(x28941,x28942),f4(x28943,x28944),f4(x28945,x28946),f4(x28947,x28948)),f7(f4(x28942,x28941),f4(x28943,x28944),f4(x28945,x28946),f4(x28947,x28948)))), % 116.89/116.96 inference(scs_inference,[],[2823,2573,20])). % 116.89/116.96 cnf(2896,plain, % 116.89/116.96 (~P3(f7(x28961,x28962,x28963,f4(x28964,x28965)),x28966)+P3(f7(x28961,x28962,x28963,f4(x28965,x28964)),x28966)), % 116.89/116.96 inference(scs_inference,[],[2823,2573,2572,20,22])). % 116.89/116.96 cnf(2922,plain, % 116.89/116.96 (~P3(x29221,a11)+~E(x29221,f3(a5,a11))), % 116.89/116.96 inference(scs_inference,[],[54,22])). % 116.89/116.96 cnf(2923,plain, % 116.89/116.96 (~E(f3(a5,a11),x29231)+~P3(x29231,a11)), % 116.89/116.96 inference(scs_inference,[],[54,22,2])). % 116.89/116.96 cnf(2945,plain, % 116.89/116.96 (P2(f7(f4(x29451,x29452),f4(x29453,x29454),f4(x29455,x29456),f4(x29457,x29458)),f7(f4(x29452,x29451),f4(x29453,x29454),f4(x29455,x29456),f4(x29458,x29457)))), % 116.89/116.96 inference(scs_inference,[],[2894,2572,20])). % 116.89/116.96 cnf(2997,plain, % 116.89/116.96 (P2(f2(f4(x29971,x29972),f4(x29973,x29974)),f2(f4(x29972,x29971),f4(x29974,x29973)))), % 116.89/116.96 inference(scs_inference,[],[356,2575,20])). % 116.89/116.96 cnf(3058,plain, % 116.89/116.96 (~P3(x30581,f8(x30582,x30583,x30584,f4(x30585,x30586)))+P3(x30581,f8(x30582,x30583,x30584,f4(x30586,x30585)))), % 116.89/116.96 inference(scs_inference,[],[2945,2573,2574,20,23])). % 116.89/116.96 cnf(3082,plain, % 116.89/116.96 (~P3(f4(x30821,f4(x30822,x30823)),x30824)+P3(f4(x30821,f4(x30823,x30822)),x30824)), % 116.89/116.96 inference(scs_inference,[],[2997,298,329,20,22])). % 116.89/116.96 cnf(3172,plain, % 116.89/116.96 (~P3(f4(x31721,x31722),x31723)+P3(f4(x31722,x31721),x31723)), % 116.89/116.96 inference(scs_inference,[],[25,2577,26,21,22])). % 116.89/116.96 cnf(3176,plain, % 116.89/116.96 (~P3(f4(x31761,x31762),f2(x31763,x31764))+P3(f7(f2(x31763,x31764),x31763,x31764,f4(x31762,x31761)),x31763)), % 116.89/116.96 inference(scs_inference,[],[25,3172,36])). % 116.89/116.96 cnf(3204,plain, % 116.89/116.96 (~P3(x32041,f4(x32042,x32043))+P3(x32041,f4(x32043,x32042))), % 116.89/116.96 inference(scs_inference,[],[25,2580,26,20,23])). % 116.89/116.96 cnf(3386,plain, % 116.89/116.96 (~P3(x33861,f4(f4(x33862,x33863),x33864))+P3(x33861,f4(f4(x33863,x33862),x33864))), % 116.89/116.96 inference(scs_inference,[],[48,23])). % 116.89/116.96 cnf(3403,plain, % 116.89/116.96 (~P3(x34031,f4(x34032,f4(x34033,x34034)))+P3(x34031,f4(f4(x34034,x34033),x34032))), % 116.89/116.96 inference(scs_inference,[],[186,33])). % 116.89/116.96 cnf(3541,plain, % 116.89/116.96 (~E(x35411,f2(a9,a10))+~E(f3(a5,a11),x35411)), % 116.89/116.96 inference(scs_inference,[],[1384,3])). % 116.89/116.96 cnf(3543,plain, % 116.89/116.96 (~E(f4(f4(f7(a5,a9,a10,f3(a5,a11)),f8(a5,a9,a10,f3(a5,a11))),f12(f7(a5,a9,a10,f3(a5,a11)))),f2(a9,a10))), % 116.89/116.96 inference(scs_inference,[],[2536,3541,252])). % 116.89/116.96 cnf(3563,plain, % 116.89/116.96 (~E(x35631,f3(a5,a11))+~E(f2(a9,a10),x35631)), % 116.89/116.96 inference(scs_inference,[],[1419,3])). % 116.89/116.96 cnf(3758,plain, % 116.89/116.96 (~P3(x37581,f7(f2(x37581,x37582),x37581,x37582,f4(x37583,x37584)))+~P3(f4(x37584,x37583),f2(x37581,x37582))), % 116.89/116.96 inference(scs_inference,[],[3176,31])). % 116.89/116.96 cnf(3781,plain, % 116.89/116.96 (~P3(a9,f7(f2(a9,a10),a9,a10,f4(x37811,x37812)))+~E(f3(a5,a11),f4(x37812,x37811))), % 116.89/116.96 inference(scs_inference,[],[3758,75])). % 116.89/116.96 cnf(3791,plain, % 116.89/116.96 (~P3(a9,f7(f2(a9,a10),a9,a10,f4(f12(f7(a5,a9,a10,f3(a5,a11))),f4(f7(a5,a9,a10,f3(a5,a11)),f8(a5,a9,a10,f3(a5,a11))))))), % 116.89/116.96 inference(scs_inference,[],[2536,3781,252])). % 116.89/116.96 cnf(3977,plain, % 116.89/116.96 (P3(f8(f2(a9,a10),a9,a10,f4(f4(f7(a5,a9,a10,f3(a5,a11)),f8(a5,a9,a10,f3(a5,a11))),f12(f7(a5,a9,a10,f3(a5,a11))))),a10)), % 116.89/116.96 inference(scs_inference,[],[1066,461,2564,328,75,3541,3563,3386,3403,1643,1829,1275,1421,1027,1045])). % 116.89/116.96 cnf(3981,plain, % 116.89/116.96 (P3(f8(f2(a9,a10),a9,a10,f4(f4(f7(f2(a9,a10),a9,a10,f3(a5,a11)),f8(f2(a9,a10),a9,a10,f3(a5,a11))),f12(f7(f2(a9,a10),a9,a10,f3(a5,a11))))),a10)), % 116.89/116.96 inference(scs_inference,[],[1066,461,2564,328,75,3541,3563,3386,3403,1643,1829,1275,1421,1027,1045,1260,1264])). % 116.89/116.96 cnf(3988,plain, % 116.89/116.96 (P3(f4(f4(f8(a5,a9,a10,f3(a5,a11)),f7(a5,a9,a10,f3(a5,a11))),f12(f7(a5,a9,a10,f3(a5,a11)))),f2(a9,a10))), % 116.89/116.96 inference(scs_inference,[],[1066,2565,461,2564,328,75,3541,3563,3386,3403,1643,1829,1275,1421,1027,1045,1260,1264,827,3781,3204,825])). % 116.89/116.96 cnf(3990,plain, % 116.89/116.96 (~P3(a5,f4(f4(f7(a5,a9,a10,f3(a5,a11)),f8(a5,a9,a10,f3(a5,a11))),f12(f7(a5,a9,a10,f3(a5,a11)))))), % 116.89/116.96 inference(scs_inference,[],[1066,2565,461,2564,328,75,3541,3563,3386,3403,1643,1829,1275,1421,1027,1045,1260,1264,827,3781,3204,825,2896,2846])). % 116.89/116.96 cnf(4016,plain, % 116.89/116.96 (E(f4(f4(x40161,f4(x40162,x40163)),x40164),f4(f4(x40161,f4(x40163,x40162)),x40164))), % 116.89/116.96 inference(rename_variables,[],[325])). % 116.89/116.96 cnf(4018,plain, % 116.89/116.96 (P3(f7(a5,a9,a10,f4(f12(f7(a5,a9,a10,f3(a5,a11))),f4(f8(a5,a9,a10,f3(a5,a11)),f7(a5,a9,a10,f3(a5,a11))))),a9)), % 116.89/116.96 inference(scs_inference,[],[197,198,325,347,868,995,2548,1066,3543,2565,461,2564,328,2536,27,75,3541,3563,3386,3403,1643,1829,1275,1421,1027,1045,1260,1264,827,3781,3204,825,2896,2846,4,12,14,17,5,15,6,2845,16,9,7,13,11,18,10,2,8,31,38,20,21,22])). % 116.89/116.96 cnf(4026,plain, % 116.89/116.96 (~P3(a9,f7(a5,a9,a10,f4(f4(f8(a5,a9,a10,f3(a5,a11)),f7(a5,a9,a10,f3(a5,a11))),f12(f7(a5,a9,a10,f3(a5,a11))))))), % 116.89/116.96 inference(scs_inference,[],[197,198,325,4016,347,868,995,2548,143,1066,3543,2565,461,2564,328,3791,2605,2619,2536,27,75,3541,3563,3386,3403,1643,1829,1275,1421,1027,1045,1260,1264,827,3781,3204,825,2896,2846,4,12,14,17,5,15,6,2845,16,9,7,13,11,18,10,2,8,31,38,20,21,22,33,3,23])). % 116.89/116.96 cnf(4036,plain, % 116.89/116.96 (P3(f4(f12(f7(f2(a9,a10),a9,a10,f3(a5,a11))),f4(f8(f2(a9,a10),a9,a10,f3(a5,a11)),f7(f2(a9,a10),a9,a10,f3(a5,a11)))),f2(a9,a10))), % 116.89/116.96 inference(scs_inference,[],[197,198,325,4016,347,868,995,2548,143,1066,3543,2565,461,2564,328,3791,2605,2619,2595,2536,27,75,3541,3563,3386,3403,1643,1829,1275,1421,1027,1045,1260,1264,827,3781,3204,825,2896,2846,4,12,14,17,5,15,6,2845,16,9,7,13,11,18,10,2,8,31,38,20,21,22,33,3,23,3176,3758,2231,3172,3082])). % 116.89/116.96 cnf(4039,plain, % 116.89/116.96 (~P3(f4(f4(f7(a5,a9,a10,f3(a5,a11)),f8(a5,a9,a10,f3(a5,a11))),f12(f7(a5,a9,a10,f3(a5,a11)))),a11)), % 116.89/116.96 inference(scs_inference,[],[197,198,325,4016,347,868,995,2548,143,1066,3543,2565,461,2564,328,3791,2605,2619,2595,2536,27,75,3541,3563,3386,3403,1643,1829,1275,1421,1027,1045,1260,1264,827,3781,3204,825,2896,2846,4,12,14,17,5,15,6,2845,16,9,7,13,11,18,10,2,8,31,38,20,21,22,33,3,23,3176,3758,2231,3172,3082,2922,2723,2923])). % 116.89/116.96 cnf(4074,plain, % 116.89/116.96 ($false), % 116.89/116.96 inference(scs_inference,[],[48,2536,1066,461,3988,4036,3977,3981,4018,3990,4039,4026,2598,31,2800,2723,2896,825,3058,3204,3172,3176,3386,3403,3758,359,35,3,22]), % 116.89/116.96 ['proof']). % 116.89/116.96 % SZS output end Proof % 116.89/116.96 % Total time :116.170000s %------------------------------------------------------------------------------