%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SEU145+1 : TPTP v8.2.0. Released v3.3.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n017.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 15:01:18 EDT 2024 % Result : Theorem 116.75s 116.78s % Output : CNFRefutation 116.84s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SEU145+1 : TPTP v8.2.0. Released v3.3.0. % 0.03/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n017.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Fri Jun 21 13:00:09 EDT 2024 % 0.12/0.33 % CPUTime : % 0.52/0.58 start to proof:theBenchmark % 116.66/116.76 %------------------------------------------- % 116.66/116.76 % File :CSE---1.7 % 116.66/116.76 % Problem :theBenchmark % 116.66/116.76 % Transform :cnf % 116.66/116.76 % Format :tptp:raw % 116.66/116.76 % Command :java -jar mcs_scs.jar %d %s % 116.66/116.76 % 116.66/116.76 % Result :Theorem 116.120000s % 116.66/116.76 % Output :CNFRefutation 116.120000s % 116.66/116.76 %------------------------------------------- % 116.75/116.78 %------------------------------------------------------------------------------ % 116.75/116.78 % File : SEU145+1 : TPTP v8.2.0. Released v3.3.0. % 116.75/116.78 % Domain : Set theory % 116.75/116.78 % Problem : MPTP bushy problem l3_zfmisc_1 % 116.75/116.78 % Version : [Urb07] axioms : Especial. % 116.75/116.78 % English : % 116.75/116.78 % 116.75/116.78 % Refs : [Ban01] Bancerek et al. (2001), On the Characterizations of Co % 116.75/116.78 % : [Urb07] Urban (2006), Email to G. Sutcliffe % 116.75/116.78 % Source : [Urb07] % 116.75/116.78 % Names : bushy-l3_zfmisc_1 [Urb07] % 116.75/116.78 % 116.75/116.78 % Status : Theorem % 116.75/116.78 % Rating : 0.31 v8.1.0, 0.28 v7.5.0, 0.34 v7.4.0, 0.27 v7.3.0, 0.21 v7.2.0, 0.17 v7.1.0, 0.22 v7.0.0, 0.23 v6.4.0, 0.27 v6.3.0, 0.29 v6.2.0, 0.36 v6.1.0, 0.47 v6.0.0, 0.39 v5.5.0, 0.44 v5.4.0, 0.50 v5.3.0, 0.56 v5.2.0, 0.35 v5.1.0, 0.38 v5.0.0, 0.46 v4.1.0, 0.43 v4.0.0, 0.46 v3.7.0, 0.40 v3.5.0, 0.42 v3.4.0, 0.53 v3.3.0 % 116.75/116.78 % Syntax : Number of formulae : 8 ( 3 unt; 0 def) % 116.75/116.78 % Number of atoms : 18 ( 3 equ) % 116.75/116.78 % Maximal formula atoms : 4 ( 2 avg) % 116.75/116.78 % Number of connectives : 12 ( 2 ~; 1 |; 1 &) % 116.75/116.78 % ( 5 <=>; 3 =>; 0 <=; 0 <~>) % 116.75/116.78 % Maximal formula depth : 9 ( 5 avg) % 116.75/116.78 % Maximal term depth : 3 ( 1 avg) % 116.75/116.78 % Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty) % 116.75/116.78 % Number of functors : 2 ( 2 usr; 0 con; 1-2 aty) % 116.75/116.78 % Number of variables : 17 ( 17 !; 0 ?) % 116.75/116.78 % SPC : FOF_THM_RFO_SEQ % 116.75/116.78 % 116.75/116.78 % Comments : Translated by MPTP 0.2 from the original problem in the Mizar % 116.75/116.78 % library, www.mizar.org % 116.75/116.78 %------------------------------------------------------------------------------ % 116.75/116.78 fof(antisymmetry_r2_hidden,axiom, % 116.75/116.78 ! [A,B] : % 116.75/116.78 ( in(A,B) % 116.75/116.78 => ~ in(B,A) ) ). % 116.75/116.78 % 116.75/116.78 fof(d1_tarski,axiom, % 116.75/116.78 ! [A,B] : % 116.75/116.78 ( B = singleton(A) % 116.75/116.78 <=> ! [C] : % 116.75/116.78 ( in(C,B) % 116.75/116.78 <=> C = A ) ) ). % 116.75/116.78 % 116.75/116.78 fof(d3_tarski,axiom, % 116.75/116.78 ! [A,B] : % 116.75/116.78 ( subset(A,B) % 116.75/116.78 <=> ! [C] : % 116.75/116.78 ( in(C,A) % 116.75/116.78 => in(C,B) ) ) ). % 116.75/116.78 % 116.75/116.78 fof(d4_xboole_0,axiom, % 116.75/116.78 ! [A,B,C] : % 116.75/116.78 ( C = set_difference(A,B) % 116.75/116.78 <=> ! [D] : % 116.75/116.78 ( in(D,C) % 116.75/116.78 <=> ( in(D,A) % 116.75/116.78 & ~ in(D,B) ) ) ) ). % 116.75/116.78 % 116.75/116.78 fof(dt_k1_tarski,axiom, % 116.75/116.78 $true ). % 116.75/116.78 % 116.75/116.78 fof(dt_k4_xboole_0,axiom, % 116.75/116.78 $true ). % 116.75/116.78 % 116.75/116.78 fof(l3_zfmisc_1,conjecture, % 116.75/116.78 ! [A,B,C] : % 116.75/116.78 ( subset(A,B) % 116.75/116.78 => ( in(C,A) % 116.75/116.78 | subset(A,set_difference(B,singleton(C))) ) ) ). % 116.75/116.78 % 116.75/116.78 fof(reflexivity_r1_tarski,axiom, % 116.75/116.78 ! [A,B] : subset(A,A) ). % 116.75/116.78 % 116.75/116.78 %------------------------------------------------------------------------------ % 116.75/116.78 %------------------------------------------- % 116.75/116.78 % Proof found % 116.75/116.78 % SZS status Theorem for theBenchmark % 116.75/116.78 % SZS output start Proof % 116.75/116.79 %ClaNum:35(EqnAxiom:17) % 116.75/116.79 %VarNum:110(SingletonVarNum:41) % 116.75/116.79 %MaxLitNum:4 % 116.75/116.79 %MaxfuncDepth:2 % 116.75/116.79 %SharedTerms:8 % 116.75/116.79 %goalClause: 18 20 21 % 116.75/116.79 %singleGoalClaCount:3 % 116.75/116.79 [18]P1(a1,a5) % 116.75/116.79 [20]~P2(a6,a1) % 116.75/116.79 [21]~P1(a1,f8(a5,f7(a6))) % 116.75/116.79 [19]P1(x191,x191) % 116.75/116.79 [24]~P2(x242,x241)+~P2(x241,x242) % 116.75/116.79 [25]P1(x251,x252)+P2(f2(x251,x252),x251) % 116.75/116.79 [31]P1(x311,x312)+~P2(f2(x311,x312),x312) % 116.75/116.79 [27]E(f3(x272,x271),x272)+P2(f3(x272,x271),x271)+E(x271,f7(x272)) % 116.75/116.79 [32]~E(f3(x322,x321),x322)+~P2(f3(x322,x321),x321)+E(x321,f7(x322)) % 116.75/116.79 [26]~P1(x263,x262)+P2(x261,x262)+~P2(x261,x263) % 116.75/116.79 [22]P2(x221,x222)+~E(x221,x223)+~E(x222,f7(x223)) % 116.75/116.79 [23]~P2(x231,x233)+E(x231,x232)+~E(x233,f7(x232)) % 116.75/116.79 [33]P2(f4(x332,x333,x331),x331)+P2(f4(x332,x333,x331),x332)+E(x331,f8(x332,x333)) % 116.75/116.79 [34]P2(f4(x342,x343,x341),x341)+~P2(f4(x342,x343,x341),x343)+E(x341,f8(x342,x343)) % 116.75/116.79 [28]~P2(x281,x283)+P2(x281,x282)+~E(x283,f8(x282,x284)) % 116.75/116.79 [29]~P2(x294,x293)+~P2(x294,x291)+~E(x291,f8(x292,x293)) % 116.75/116.79 [35]P2(f4(x352,x353,x351),x353)+~P2(f4(x352,x353,x351),x351)+~P2(f4(x352,x353,x351),x352)+E(x351,f8(x352,x353)) % 116.75/116.79 [30]~P2(x301,x304)+P2(x301,x302)+P2(x301,x303)+~E(x302,f8(x304,x303)) % 116.75/116.79 %EqnAxiom % 116.75/116.79 [1]E(x11,x11) % 116.75/116.79 [2]E(x22,x21)+~E(x21,x22) % 116.75/116.79 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 116.75/116.79 [4]~E(x41,x42)+E(f7(x41),f7(x42)) % 116.75/116.79 [5]~E(x51,x52)+E(f8(x51,x53),f8(x52,x53)) % 116.75/116.79 [6]~E(x61,x62)+E(f8(x63,x61),f8(x63,x62)) % 116.75/116.79 [7]~E(x71,x72)+E(f4(x71,x73,x74),f4(x72,x73,x74)) % 116.75/116.79 [8]~E(x81,x82)+E(f4(x83,x81,x84),f4(x83,x82,x84)) % 116.75/116.79 [9]~E(x91,x92)+E(f4(x93,x94,x91),f4(x93,x94,x92)) % 116.75/116.79 [10]~E(x101,x102)+E(f3(x101,x103),f3(x102,x103)) % 116.75/116.79 [11]~E(x111,x112)+E(f3(x113,x111),f3(x113,x112)) % 116.75/116.79 [12]~E(x121,x122)+E(f2(x121,x123),f2(x122,x123)) % 116.75/116.79 [13]~E(x131,x132)+E(f2(x133,x131),f2(x133,x132)) % 116.75/116.79 [14]P1(x142,x143)+~E(x141,x142)+~P1(x141,x143) % 116.75/116.79 [15]P1(x153,x152)+~E(x151,x152)+~P1(x153,x151) % 116.75/116.79 [16]P2(x162,x163)+~E(x161,x162)+~P2(x161,x163) % 116.75/116.79 [17]P2(x173,x172)+~E(x171,x172)+~P2(x173,x171) % 116.75/116.79 % 116.75/116.79 %------------------------------------------- % 116.78/116.81 cnf(36,plain, % 116.78/116.81 (~P2(x361,f7(x362))+E(x361,x362)), % 116.78/116.81 inference(equality_inference,[],[23])). % 116.78/116.81 cnf(37,plain, % 116.78/116.81 (~P2(x371,f8(x372,x373))+P2(x371,x372)), % 116.78/116.81 inference(equality_inference,[],[28])). % 116.78/116.81 cnf(38,plain, % 116.78/116.81 (~P2(x381,x382)+~P2(x381,f8(x383,x382))), % 116.78/116.81 inference(equality_inference,[],[29])). % 116.78/116.81 cnf(39,plain, % 116.78/116.81 (~P2(x391,x392)+P2(x391,f8(x392,x393))+P2(x391,x393)), % 116.78/116.81 inference(equality_inference,[],[30])). % 116.78/116.81 cnf(40,plain, % 116.78/116.81 (~P2(a6,f8(a1,x401))), % 116.78/116.81 inference(scs_inference,[],[20,37])). % 116.78/116.81 cnf(42,plain, % 116.78/116.81 (~E(f8(a5,f7(a6)),a1)), % 116.78/116.81 inference(scs_inference,[],[20,21,19,37,14])). % 116.78/116.81 cnf(44,plain, % 116.78/116.81 (~E(a5,f8(a5,f7(a6)))), % 116.78/116.81 inference(scs_inference,[],[18,20,21,19,37,14,15])). % 116.78/116.81 cnf(45,plain, % 116.78/116.81 (~P2(f8(a5,f7(a6)),f7(a1))), % 116.78/116.81 inference(scs_inference,[],[18,20,21,19,37,14,15,36])). % 116.78/116.81 cnf(47,plain, % 116.78/116.81 (~P2(a6,x471)+P2(a6,f8(x471,f8(a1,x472)))), % 116.78/116.81 inference(scs_inference,[],[18,20,21,19,37,14,15,36,39])). % 116.78/116.81 cnf(49,plain, % 116.78/116.81 (P2(f4(a5,f7(a6),a5),a5)), % 116.78/116.81 inference(scs_inference,[],[18,20,21,19,37,14,15,36,39,33])). % 116.78/116.81 cnf(61,plain, % 116.78/116.81 (~P2(a5,f4(a5,f7(a6),a5))), % 116.78/116.81 inference(scs_inference,[],[49,45,37,24])). % 116.78/116.81 cnf(63,plain, % 116.78/116.81 (~P2(f4(a5,f7(a6),a5),f8(x631,a5))), % 116.78/116.81 inference(scs_inference,[],[49,45,37,24,38])). % 116.78/116.81 cnf(65,plain, % 116.78/116.81 (P2(f4(a5,f7(a6),a5),f8(a5,f8(x651,a5)))), % 116.78/116.81 inference(scs_inference,[],[49,45,37,24,38,39])). % 116.78/116.81 cnf(67,plain, % 116.78/116.81 (~E(a5,f8(x671,a5))), % 116.78/116.81 inference(scs_inference,[],[49,45,37,24,38,39,17])). % 116.78/116.81 cnf(68,plain, % 116.78/116.81 (~E(a1,f8(a5,f7(a6)))), % 116.78/116.81 inference(scs_inference,[],[21,49,45,19,37,24,38,39,17,15])). % 116.78/116.81 cnf(70,plain, % 116.78/116.81 (P2(f4(a5,f7(a6),a5),f7(a6))), % 116.78/116.81 inference(scs_inference,[],[21,49,45,44,19,37,24,38,39,17,15,35])). % 116.78/116.81 cnf(72,plain, % 116.78/116.81 (~P2(a5,f7(f8(x721,a5)))), % 116.78/116.81 inference(scs_inference,[],[21,49,45,44,19,37,24,38,39,17,15,35,36])). % 116.78/116.81 cnf(80,plain, % 116.78/116.81 (~P2(f7(a6),f4(a5,f7(a6),a5))), % 116.78/116.81 inference(scs_inference,[],[40,70,37,24])). % 116.78/116.81 cnf(82,plain, % 116.78/116.81 (~P2(f4(a5,f7(a6),a5),f8(x821,f7(a6)))), % 116.78/116.81 inference(scs_inference,[],[40,70,37,24,38])). % 116.78/116.81 cnf(84,plain, % 116.78/116.81 (P2(f4(a5,f7(a6),a5),f8(f7(a6),f8(x841,a5)))), % 116.78/116.81 inference(scs_inference,[],[40,63,70,37,24,38,39])). % 116.78/116.81 cnf(86,plain, % 116.78/116.81 (~E(f7(a6),f8(x861,a5))), % 116.78/116.81 inference(scs_inference,[],[40,63,70,37,24,38,39,17])). % 116.78/116.81 cnf(87,plain, % 116.78/116.81 (~P2(f7(a6),f7(f8(x871,a5)))), % 116.78/116.81 inference(scs_inference,[],[40,63,70,37,24,38,39,17,36])). % 116.78/116.81 cnf(95,plain, % 116.78/116.81 (~P2(f4(a5,f7(a6),a5),f8(f8(x951,a5),x952))), % 116.78/116.81 inference(scs_inference,[],[63,37])). % 116.78/116.81 cnf(99,plain, % 116.78/116.81 (~E(f8(f7(a6),f8(x991,a5)),f8(x992,f7(a6)))), % 116.78/116.81 inference(scs_inference,[],[82,84,63,37,24,17])). % 116.78/116.81 cnf(100,plain, % 116.78/116.81 (~E(f8(x1001,a5),f7(a6))), % 116.78/116.81 inference(scs_inference,[],[82,84,63,37,24,17,6])). % 116.78/116.81 cnf(113,plain, % 116.78/116.81 (~E(f7(a6),f8(f8(x1131,a5),x1132))), % 116.78/116.81 inference(scs_inference,[],[70,95,65,24,17])). % 116.78/116.81 cnf(120,plain, % 116.78/116.81 (~E(f8(a5,f8(x1201,a5)),f8(x1202,a5))), % 116.78/116.81 inference(scs_inference,[],[63,65,17])). % 116.78/116.81 cnf(121,plain, % 116.78/116.81 (~E(f8(x1211,a5),a5)), % 116.78/116.81 inference(scs_inference,[],[63,65,17,6])). % 116.78/116.81 cnf(126,plain, % 116.78/116.81 (P2(f4(f7(a6),a5,f7(a6)),a5)+~P2(f4(f7(a6),a5,f7(a6)),a5)), % 116.78/116.81 inference(scs_inference,[],[63,86,65,17,6,36,34,35])). % 116.78/116.81 cnf(129,plain, % 116.78/116.81 (~P2(f7(a6),f4(f7(a6),a5,f7(a6)))+~P2(f4(f7(a6),a5,f7(a6)),a5)), % 116.78/116.81 inference(scs_inference,[],[63,86,65,17,6,36,34,35,24])). % 116.78/116.81 cnf(137,plain, % 116.78/116.81 (~E(f8(f7(a6),f8(x1371,a5)),f8(x1372,a5))), % 116.78/116.81 inference(scs_inference,[],[63,84,120,36,17])). % 116.78/116.81 cnf(138,plain, % 116.78/116.81 (P2(f4(f8(x1381,a5),x1382,f7(a6)),f7(a6))+~P2(f4(f8(x1381,a5),x1382,f7(a6)),x1382)), % 116.78/116.81 inference(scs_inference,[],[63,84,120,113,36,17,34])). % 116.78/116.81 cnf(150,plain, % 116.78/116.81 (P2(f4(a5,a5,a5),a5)), % 116.78/116.81 inference(scs_inference,[],[67,137,36,33,35])). % 116.78/116.81 cnf(157,plain, % 116.78/116.81 (~P2(f4(a5,a5,a5),f8(x1571,a5))), % 116.78/116.81 inference(scs_inference,[],[150,24,38])). % 116.78/116.81 cnf(159,plain, % 116.78/116.81 (~P2(f8(x1591,a5),f7(a5))), % 116.78/116.81 inference(scs_inference,[],[150,121,24,38,36])). % 116.78/116.81 cnf(161,plain, % 116.78/116.81 (P2(f4(a5,a5,a5),f8(a5,f8(x1611,a5)))), % 116.78/116.81 inference(scs_inference,[],[150,121,24,38,36,39])). % 116.78/116.81 cnf(165,plain, % 116.78/116.81 (P2(f4(x1651,a5,f7(a6)),f7(a6))+P2(f4(x1651,a5,f7(a6)),x1651)), % 116.78/116.81 inference(scs_inference,[],[86,150,121,24,38,36,39,37,33])). % 116.78/116.81 cnf(172,plain, % 116.78/116.81 (~P2(f8(a5,f8(x1721,a5)),f4(a5,a5,a5))), % 116.78/116.81 inference(scs_inference,[],[157,161,37,24])). % 116.78/116.81 cnf(179,plain, % 116.78/116.81 (P2(f4(a5,f7(a6),a1),a5)), % 116.78/116.81 inference(scs_inference,[],[18,20,68,157,161,37,24,33,16,38,26])). % 116.78/116.81 cnf(185,plain, % 116.78/116.81 (~P2(a5,f4(a5,f7(a6),a1))), % 116.78/116.81 inference(scs_inference,[],[179,172,37,24])). % 116.78/116.81 cnf(187,plain, % 116.78/116.81 (~P2(f4(a5,f7(a6),a1),f8(x1871,a5))), % 116.78/116.81 inference(scs_inference,[],[179,172,37,24,38])). % 116.78/116.81 cnf(189,plain, % 116.78/116.81 (P2(f4(a5,f7(a6),a1),f8(a5,f8(x1891,a5)))), % 116.78/116.81 inference(scs_inference,[],[179,172,37,24,38,39])). % 116.78/116.81 cnf(191,plain, % 116.78/116.81 (P2(f4(f8(x1911,a5),x1912,f7(a6)),f7(a6))+P2(f4(f8(x1911,a5),x1912,f7(a6)),f8(x1911,a5))), % 116.78/116.81 inference(scs_inference,[],[179,113,172,37,24,38,39,33])). % 116.78/116.81 cnf(195,plain, % 116.78/116.81 (~P2(f4(a5,f7(a6),a1),f8(f8(x1951,a5),x1952))), % 116.78/116.81 inference(scs_inference,[],[187,37])). % 116.78/116.81 cnf(207,plain, % 116.78/116.81 (~E(a5,f8(f8(x2071,a5),x2072))), % 116.78/116.81 inference(scs_inference,[],[179,195,159,37,17])). % 116.78/116.81 cnf(245,plain, % 116.78/116.82 (E(f7(f4(a5,f7(a6),a5)),f7(a6))), % 116.78/116.82 inference(scs_inference,[],[70,4,36])). % 116.78/116.82 cnf(270,plain, % 116.78/116.82 (~E(f8(a5,f8(x2701,a5)),a1)+~E(f4(a5,f7(a6),a5),a6)), % 116.78/116.82 inference(scs_inference,[],[20,65,16,17])). % 116.78/116.82 cnf(280,plain, % 116.78/116.82 (~E(f8(f7(a6),f8(x2801,a5)),a1)+~E(f4(a5,f7(a6),a5),a6)), % 116.78/116.82 inference(scs_inference,[],[20,84,16,17])). % 116.78/116.82 cnf(472,plain, % 116.78/116.82 (~P2(a6,x4721)+~E(a1,f8(x4721,a1))), % 116.78/116.82 inference(scs_inference,[],[40,47,30])). % 116.78/116.82 cnf(488,plain, % 116.78/116.82 (~P2(a6,f8(x4881,x4882))+~E(a1,f8(x4881,a1))), % 116.78/116.82 inference(scs_inference,[],[472,37])). % 116.78/116.82 cnf(615,plain, % 116.78/116.82 (E(f4(f4(a5,f7(a6),a5),x6151,x6152),f4(a6,x6151,x6152))), % 116.78/116.82 inference(scs_inference,[],[70,7,36])). % 116.78/116.82 cnf(631,plain, % 116.78/116.82 (E(f4(x6311,f4(a5,f7(a6),a5),x6312),f4(x6311,a6,x6312))), % 116.78/116.82 inference(scs_inference,[],[70,8,36])). % 116.78/116.82 cnf(647,plain, % 116.78/116.82 (E(f4(x6471,x6472,f4(a5,f7(a6),a5)),f4(x6471,x6472,a6))), % 116.78/116.82 inference(scs_inference,[],[70,9,36])). % 116.78/116.82 cnf(1113,plain, % 116.78/116.82 (~E(f8(a5,f8(x11131,a5)),a1)), % 116.78/116.82 inference(scs_inference,[],[70,270,36])). % 116.78/116.82 cnf(1114,plain, % 116.78/116.82 (~P2(f8(a5,f8(x11141,a5)),f7(a1))), % 116.78/116.82 inference(scs_inference,[],[1113,36])). % 116.78/116.82 cnf(1329,plain, % 116.78/116.82 (E(f4(f7(a6),a5,f7(a6)),a6)), % 116.78/116.82 inference(scs_inference,[],[165,36])). % 116.78/116.82 cnf(1330,plain, % 116.78/116.82 (E(a6,f4(f7(a6),a5,f7(a6)))), % 116.78/116.82 inference(scs_inference,[],[1329,2])). % 116.78/116.82 cnf(1347,plain, % 116.78/116.82 (~E(f8(f7(a6),f8(x13471,a5)),a1)), % 116.78/116.82 inference(scs_inference,[],[70,280,36])). % 116.78/116.82 cnf(1421,plain, % 116.78/116.82 (P2(f4(a5,a5,a5),f8(f8(a5,f8(x14211,a5)),f8(x14212,a5)))), % 116.78/116.82 inference(scs_inference,[],[161,157,39])). % 116.78/116.82 cnf(1423,plain, % 116.78/116.82 (~P2(f8(f8(a5,f8(x14231,a5)),f8(x14232,a5)),f4(a5,a5,a5))), % 116.78/116.82 inference(scs_inference,[],[161,157,39,24])). % 116.78/116.82 cnf(1430,plain, % 116.78/116.82 (~E(f8(f8(a5,f8(x14301,a5)),f8(x14302,a5)),f8(x14303,a5))), % 116.78/116.82 inference(scs_inference,[],[157,1421,17])). % 116.78/116.82 cnf(2589,plain, % 116.78/116.82 (P2(f4(f8(x25891,a5),f8(x25891,a5),f7(a6)),f7(a6))), % 116.78/116.82 inference(scs_inference,[],[138,191])). % 116.78/116.82 cnf(2590,plain, % 116.78/116.82 (~P2(f7(a6),f4(f8(x25901,a5),f8(x25901,a5),f7(a6)))), % 116.78/116.82 inference(scs_inference,[],[2589,24])). % 116.78/116.82 cnf(2592,plain, % 116.78/116.82 (~P2(f4(f8(x25921,a5),f8(x25921,a5),f7(a6)),f8(x25922,f7(a6)))), % 116.78/116.82 inference(scs_inference,[],[2589,24,38])). % 116.78/116.82 cnf(2595,plain, % 116.78/116.82 (P2(f4(x25951,f7(a6),f7(a6)),f7(a6))+P2(f4(x25951,f7(a6),f7(a6)),x25951)), % 116.78/116.82 inference(scs_inference,[],[2589,24,38,17,33])). % 116.78/116.82 cnf(2597,plain, % 116.78/116.82 (P2(f4(f7(a6),f7(a6),f7(a6)),f7(a6))), % 116.78/116.82 inference(scs_inference,[],[2589,24,38,17,33,35])). % 116.78/116.82 cnf(2600,plain, % 116.78/116.82 (~P2(f7(a6),f4(f7(a6),f7(a6),f7(a6)))), % 116.78/116.82 inference(scs_inference,[],[2597,24])). % 116.78/116.82 cnf(2605,plain, % 116.78/116.82 (~E(f4(f7(a6),f7(a6),f7(a6)),f4(f7(a6),a5,f7(a6)))+P2(f4(f7(a6),a5,f7(a6)),a5)), % 116.78/116.82 inference(scs_inference,[],[86,2597,24,38,16,35])). % 116.78/116.82 cnf(2638,plain, % 116.78/116.82 (E(f4(f7(a6),f7(a6),f7(a6)),a6)), % 116.78/116.82 inference(scs_inference,[],[2595,36])). % 116.78/116.82 cnf(2639,plain, % 116.78/116.82 (E(a6,f4(f7(a6),f7(a6),f7(a6)))), % 116.78/116.82 inference(scs_inference,[],[2638,2])). % 116.78/116.82 cnf(2640,plain, % 116.78/116.82 (E(f4(f7(a6),a5,f7(a6)),f4(f7(a6),f7(a6),f7(a6)))), % 116.78/116.82 inference(scs_inference,[],[1329,2638,2,3])). % 116.78/116.82 cnf(2641,plain, % 116.78/116.82 (P2(a6,f7(a6))), % 116.78/116.82 inference(scs_inference,[],[2597,1329,2638,2,3,16])). % 116.78/116.82 cnf(2642,plain, % 116.78/116.82 (~P2(f7(a6),a6)), % 116.78/116.82 inference(scs_inference,[],[2597,1329,2638,2,3,16,24])). % 116.78/116.82 cnf(2644,plain, % 116.78/116.82 (~P2(f7(a6),f8(a6,x26441))), % 116.78/116.82 inference(scs_inference,[],[2597,1329,2638,2,3,16,24,37])). % 116.78/116.82 cnf(2646,plain, % 116.78/116.82 (~P2(a6,f8(x26461,f7(a6)))), % 116.78/116.82 inference(scs_inference,[],[2597,1329,2638,2,3,16,24,37,38])). % 116.78/116.82 cnf(2648,plain, % 116.78/116.82 (P2(a6,f8(f7(a6),a1))), % 116.78/116.82 inference(scs_inference,[],[20,2597,1329,2638,2,3,16,24,37,38,39])). % 116.78/116.82 cnf(2651,plain, % 116.78/116.82 (~P2(f7(a6),f7(a1))), % 116.78/116.82 inference(scs_inference,[],[20,2597,1329,2638,2,3,16,24,37,38,39,17,36])). % 116.78/116.82 cnf(2654,plain, % 116.78/116.82 (E(f4(f7(a6),f7(a6),f7(a6)),f4(f7(a6),a5,f7(a6)))), % 116.78/116.82 inference(scs_inference,[],[2640,2])). % 116.78/116.82 cnf(2655,plain, % 116.78/116.82 (~P2(f8(f7(a6),a1),a6)), % 116.78/116.82 inference(scs_inference,[],[2640,2648,2,24])). % 116.78/116.82 cnf(2657,plain, % 116.78/116.82 (~P2(f7(a6),f8(f8(a6,x26571),x26572))), % 116.78/116.82 inference(scs_inference,[],[2640,2644,2648,2,24,37])). % 116.78/116.82 cnf(2659,plain, % 116.78/116.82 (P2(a6,f8(f8(f7(a6),a1),f8(a1,x26591)))), % 116.78/116.82 inference(scs_inference,[],[40,2640,2644,2648,2,24,37,39])). % 116.78/116.82 cnf(2662,plain, % 116.78/116.82 (P2(f4(f7(a6),a5,f7(a6)),f8(f7(a6),a1))), % 116.78/116.82 inference(scs_inference,[],[20,40,1330,2640,2644,2648,2,24,37,39,17,16])). % 116.78/116.82 cnf(2663,plain, % 116.78/116.82 (~P2(f8(f7(a6),a1),f7(a1))), % 116.78/116.82 inference(scs_inference,[],[20,40,1330,2640,2644,2648,2,24,37,39,17,16,36])). % 116.78/116.82 cnf(2666,plain, % 116.78/116.82 (P2(f4(f7(a6),a5,f7(a6)),a5)), % 116.78/116.82 inference(scs_inference,[],[2654,2605])). % 116.78/116.82 cnf(2667,plain, % 116.78/116.82 (~P2(f8(f7(a6),a1),f4(f7(a6),a5,f7(a6)))), % 116.78/116.82 inference(scs_inference,[],[2662,24])). % 116.78/116.82 cnf(2669,plain, % 116.78/116.82 (~P2(f7(a6),f8(f7(a1),x26691))), % 116.78/116.82 inference(scs_inference,[],[2651,2662,24,37])). % 116.78/116.82 cnf(2671,plain, % 116.78/116.82 (P2(a6,f8(f7(a6),f8(a1,x26711)))), % 116.78/116.82 inference(scs_inference,[],[40,2651,2662,2641,24,37,39])). % 116.78/116.82 cnf(2674,plain, % 116.78/116.82 (P2(f4(f7(a6),a5,f7(a6)),f7(a6))), % 116.78/116.82 inference(scs_inference,[],[20,40,2597,2654,2651,2662,2641,2659,24,37,39,17,16])). % 116.78/116.82 cnf(2677,plain, % 116.78/116.82 (~P2(f4(f7(a6),a5,f7(a6)),f8(x26771,f7(a6)))), % 116.78/116.82 inference(scs_inference,[],[20,40,2597,2654,2651,2662,2641,2659,24,37,39,17,16,36,38])). % 116.78/116.82 cnf(2680,plain, % 116.78/116.82 (P2(f4(f7(a6),a5,f7(a6)),a5)), % 116.78/116.82 inference(scs_inference,[],[2666,126])). % 116.78/116.82 cnf(2681,plain, % 116.78/116.82 (~P2(f7(a6),f4(f7(a6),a5,f7(a6)))), % 116.78/116.82 inference(scs_inference,[],[2666,129])). % 116.78/116.82 cnf(2686,plain, % 116.78/116.82 (~P2(f4(f7(a6),a5,f7(a6)),f8(x26861,a5))), % 116.78/116.82 inference(scs_inference,[],[2666,2663,24,37,38])). % 116.78/116.82 cnf(2688,plain, % 116.78/116.82 (P2(a6,f8(f8(f7(a6),f8(a1,x26881)),f8(a1,x26882)))), % 116.78/116.82 inference(scs_inference,[],[40,2666,2663,2671,24,37,38,39])). % 116.78/116.82 cnf(2690,plain, % 116.78/116.82 (~E(a5,f8(x26901,f7(a6)))), % 116.78/116.82 inference(scs_inference,[],[40,2666,2677,2663,2671,24,37,38,39,17])). % 116.78/116.82 cnf(2691,plain, % 116.78/116.82 (P2(a6,a5)), % 116.78/116.82 inference(scs_inference,[],[40,1329,2666,2677,2663,2671,24,37,38,39,17,16])). % 116.78/116.82 cnf(2695,plain, % 116.78/116.82 (~P2(f8(f8(f7(a6),f8(a1,x26951)),f8(a1,x26952)),a6)), % 116.78/116.82 inference(scs_inference,[],[2688,24])). % 116.78/116.82 cnf(2697,plain, % 116.78/116.82 (~P2(f4(f7(a6),a5,f7(a6)),f8(f8(x26971,a5),x26972))), % 116.78/116.82 inference(scs_inference,[],[2686,2688,24,37])). % 116.78/116.82 cnf(2699,plain, % 116.78/116.82 (~P2(a6,f8(x26991,a5))), % 116.78/116.82 inference(scs_inference,[],[2686,2688,2691,24,37,38])). % 116.78/116.82 cnf(2701,plain, % 116.78/116.82 (P2(f4(f7(a6),a5,f7(a6)),f8(a5,f8(x27011,a5)))), % 116.78/116.82 inference(scs_inference,[],[2666,2686,2688,2691,24,37,38,39])). % 116.78/116.82 cnf(2703,plain, % 116.78/116.82 (~E(f8(a5,f8(x27031,a5)),f8(x27032,f7(a6)))), % 116.78/116.82 inference(scs_inference,[],[82,65,2666,2686,2688,2691,24,37,38,39,17])). % 116.78/116.82 cnf(2704,plain, % 116.78/116.82 (P2(f4(f7(a6),a5,f7(a6)),f8(f7(a6),f8(a1,x27041)))), % 116.78/116.82 inference(scs_inference,[],[82,65,1330,2666,2686,2688,2691,2671,24,37,38,39,17,16])). % 116.78/116.82 cnf(2711,plain, % 116.78/116.82 (P2(a6,f8(f7(a6),f8(x27111,a5)))), % 116.78/116.82 inference(scs_inference,[],[2704,2695,2699,2641,24,37,39])). % 116.78/116.82 cnf(2714,plain, % 116.78/116.82 (P2(a6,f8(a5,f8(x27141,a5)))), % 116.78/116.82 inference(scs_inference,[],[1329,2697,2704,2701,2695,2699,2641,24,37,39,17,16])). % 116.78/116.82 cnf(2717,plain, % 116.78/116.82 (~P2(a5,a6)), % 116.78/116.82 inference(scs_inference,[],[2691,24])). % 116.78/116.82 cnf(2721,plain, % 116.78/116.82 (P2(a6,f8(f8(f7(a6),f8(x27211,a5)),f8(a1,x27212)))), % 116.78/116.82 inference(scs_inference,[],[40,2711,2655,2691,24,37,39])). % 116.78/116.82 cnf(2735,plain, % 116.78/116.82 (~P2(f8(f8(f7(a6),f8(x27351,a5)),f8(a1,x27352)),a6)), % 116.78/116.82 inference(scs_inference,[],[2721,24])). % 116.78/116.82 cnf(2747,plain, % 116.78/116.82 (P2(a6,f8(f8(a5,f8(x27471,a5)),f8(a1,x27472)))), % 116.78/116.82 inference(scs_inference,[],[40,2735,2714,2701,24,37,39])). % 116.78/116.82 cnf(2750,plain, % 116.78/116.82 (~E(a1,f7(a6))), % 116.78/116.82 inference(scs_inference,[],[40,2735,2714,2662,2677,2701,24,37,39,17,6])). % 116.78/116.82 cnf(2763,plain, % 116.78/116.82 (~P2(a5,f8(a6,x27631))), % 116.78/116.82 inference(scs_inference,[],[2671,2717,24,37])). % 116.78/116.82 cnf(2772,plain, % 116.78/116.82 (~P2(f8(f8(a5,f8(x27721,a5)),f8(a1,x27722)),a6)), % 116.78/116.82 inference(scs_inference,[],[2747,24])). % 116.78/116.82 cnf(2774,plain, % 116.78/116.82 (~P2(a6,f8(f8(x27741,a5),x27742))), % 116.78/116.82 inference(scs_inference,[],[2699,2747,24,37])). % 116.78/116.82 cnf(2776,plain, % 116.78/116.82 (~E(f8(f7(a6),f8(a1,x27761)),f8(x27762,a5))), % 116.78/116.82 inference(scs_inference,[],[2704,2699,2686,2747,24,37,17])). % 116.78/116.82 cnf(2777,plain, % 116.78/116.82 (~E(f8(a1,x27771),a5)), % 116.78/116.82 inference(scs_inference,[],[2704,2699,2686,2747,24,37,17,6])). % 116.78/116.82 cnf(2778,plain, % 116.78/116.82 (~P2(f8(a1,x27781),f7(a5))), % 116.78/116.82 inference(scs_inference,[],[2704,2699,2686,2747,24,37,17,6,36])). % 116.78/116.82 cnf(2786,plain, % 116.78/116.82 (~P2(f8(f8(f7(a6),a1),f8(a1,x27861)),a6)), % 116.78/116.82 inference(scs_inference,[],[2659,24])). % 116.78/116.82 cnf(2790,plain, % 116.78/116.82 (~P2(f8(a1,x27901),f8(f7(a5),x27902))), % 116.78/116.82 inference(scs_inference,[],[2776,2778,2659,24,36,37])). % 116.78/116.82 cnf(2792,plain, % 116.78/116.82 (~E(f8(f7(a6),a1),f8(x27921,a5))), % 116.78/116.82 inference(scs_inference,[],[2662,2686,2776,2778,2659,24,36,37,17])). % 116.78/116.82 cnf(2793,plain, % 116.78/116.82 (~E(a1,a5)), % 116.78/116.82 inference(scs_inference,[],[2662,2686,2776,2778,2659,24,36,37,17,6])). % 116.78/116.82 cnf(2803,plain, % 116.78/116.82 (~E(f8(f7(a6),f8(a1,x28031)),a1)), % 116.78/116.82 inference(scs_inference,[],[20,2671,2772,2792,36,37,17])). % 116.78/116.82 cnf(2810,plain, % 116.78/116.82 (~E(f8(f8(f7(a6),f8(a1,x28101)),f8(a1,x28102)),a1)), % 116.78/116.82 inference(scs_inference,[],[20,2786,2793,2688,36,37,17])). % 116.78/116.82 cnf(2820,plain, % 116.78/116.82 (~P2(f8(f8(f7(a6),f8(a1,x28201)),f8(a1,x28202)),f7(a1))), % 116.78/116.82 inference(scs_inference,[],[2810,36])). % 116.78/116.82 cnf(3654,plain, % 116.78/116.82 (P2(a6,f8(a5,f8(a1,x36541)))), % 116.78/116.82 inference(scs_inference,[],[2641,2691,472,47])). % 116.78/116.82 cnf(3656,plain, % 116.78/116.82 (~P2(f4(f7(a6),a5,f7(a6)),f8(a1,x36561))), % 116.78/116.82 inference(scs_inference,[],[2641,2704,2691,472,47,38])). % 116.78/116.82 cnf(3658,plain, % 116.78/116.82 (E(f4(f8(x36581,a5),f8(x36581,a5),f7(a6)),a6)), % 116.78/116.82 inference(scs_inference,[],[2641,2704,2691,2589,472,47,38,36])). % 116.78/116.82 cnf(3663,plain, % 116.78/116.82 (~E(f8(x36631,f7(a6)),f7(a6))), % 116.78/116.82 inference(scs_inference,[],[1430,2592,2641,2704,2691,2589,472,47,38,36,24,2,22])). % 116.78/116.82 cnf(3666,plain, % 116.78/116.82 (E(f4(f8(x36661,a5),f8(x36661,a5),f7(a6)),f4(f7(a6),f7(a6),f7(a6)))), % 116.78/116.82 inference(scs_inference,[],[1430,2592,2639,2641,2704,2691,2589,472,47,38,36,24,2,22,3])). % 116.78/116.82 cnf(3667,plain, % 116.78/116.82 (~P2(f4(f7(a6),f7(a6),f7(a6)),f8(f8(x36671,a5),x36672))), % 116.78/116.82 inference(scs_inference,[],[1430,2774,2592,2639,2638,2641,2704,2691,2589,472,47,38,36,24,2,22,3,16])). % 116.78/116.82 cnf(3684,plain, % 116.78/116.82 (E(f4(a5,f7(a6),a5),a6)), % 116.78/116.82 inference(scs_inference,[],[70,36])). % 116.78/116.82 cnf(3687,plain, % 116.78/116.82 (~E(f7(a6),f8(f8(a1,x36871),x36872))), % 116.78/116.82 inference(scs_inference,[],[3656,2777,2674,70,36,2,28])). % 116.78/116.82 cnf(3689,plain, % 116.78/116.82 (~E(f8(a1,x36891),f7(a6))), % 116.78/116.82 inference(scs_inference,[],[3656,2777,2674,1329,70,36,2,28,22])). % 116.78/116.82 cnf(3691,plain, % 116.78/116.82 (~E(f8(a1,x36911),f8(f7(a6),f8(a1,x36911)))), % 116.78/116.82 inference(scs_inference,[],[3656,2777,2674,1329,70,36,2,28,22,30])). % 116.78/116.82 cnf(3693,plain, % 116.78/116.82 (E(a6,x36931)+~E(f8(a5,f8(a1,x36932)),f7(x36931))), % 116.78/116.82 inference(scs_inference,[],[3656,3654,2777,2674,1329,70,36,2,28,22,30,23])). % 116.78/116.82 cnf(3695,plain, % 116.78/116.82 (~P2(a5,f4(f8(x36951,a5),f8(x36951,a5),f7(a6)))), % 116.78/116.82 inference(scs_inference,[],[3656,3658,3654,2777,2674,2717,1329,70,36,2,28,22,30,23,17])). % 116.78/116.82 cnf(3711,plain, % 116.78/116.82 (~E(f7(a6),f8(a1,x37111))), % 116.78/116.82 inference(scs_inference,[],[3689,2])). % 116.78/116.82 cnf(3712,plain, % 116.78/116.82 (~E(a5,f8(f8(a1,x37121),x37122))), % 116.78/116.82 inference(scs_inference,[],[3689,2680,3656,2,28])). % 116.78/116.82 cnf(3715,plain, % 116.78/116.82 (~E(f8(a1,x37151),f8(a5,f8(a1,x37151)))), % 116.78/116.82 inference(scs_inference,[],[3689,3684,2680,3656,40,2,28,16,30])). % 116.78/116.82 cnf(3717,plain, % 116.78/116.82 (P2(f4(f8(x37171,a5),f8(x37171,a5),f7(a6)),x37172)+~E(x37172,f7(a6))), % 116.78/116.82 inference(scs_inference,[],[3689,3684,2680,3658,3656,40,2,28,16,30,22])). % 116.78/116.82 cnf(3724,plain, % 116.78/116.82 (P2(f4(f7(a6),f7(a6),f7(a6)),x37241)+~E(f7(a6),f8(x37241,x37242))), % 116.78/116.82 inference(scs_inference,[],[3691,2674,2686,2597,2,30,28])). % 116.78/116.82 cnf(3728,plain, % 116.78/116.82 (~E(f8(a5,f8(a1,x37281)),f8(a1,x37282))), % 116.78/116.82 inference(scs_inference,[],[3715,3654,20,2,28])). % 116.78/116.82 cnf(3730,plain, % 116.78/116.82 (~P2(f4(a5,f7(a6),a5),a1)), % 116.78/116.82 inference(scs_inference,[],[3715,3684,3654,20,2,28,16])). % 116.78/116.82 cnf(3731,plain, % 116.78/116.82 (P2(f4(f7(a6),f7(a6),f7(a6)),x37311)+~E(x37311,f7(a6))), % 116.78/116.82 inference(scs_inference,[],[3715,3684,3654,2638,20,2,28,16,22])). % 116.78/116.82 cnf(3733,plain, % 116.78/116.82 (E(f4(f7(a6),f7(a6),f7(a6)),x37331)+~E(f7(x37331),f7(a6))), % 116.78/116.82 inference(scs_inference,[],[3715,3684,3654,2638,20,2,28,16,22,36])). % 116.78/116.82 cnf(3737,plain, % 116.78/116.82 (~E(f7(x37371),f7(a6))+~E(f7(x37371),f8(x37372,f7(x37371)))), % 116.84/116.82 inference(scs_inference,[],[3715,3684,3654,2638,20,2,28,16,22,36,24,29])). % 116.84/116.82 cnf(3739,plain, % 116.84/116.82 (P2(f4(f7(a6),f7(a6),f7(a6)),x37391)+P2(f4(f7(a6),f7(a6),f7(a6)),f8(f7(a6),x37391))+~E(f7(x37392),f7(a6))), % 116.84/116.82 inference(scs_inference,[],[3715,3684,3654,2638,2597,20,2,28,16,22,36,24,29,39])). % 116.84/116.82 cnf(3743,plain, % 116.84/116.82 (P2(f4(f7(a6),f7(a6),f7(a6)),x37431)+P2(f4(f7(a6),f7(a6),f7(a6)),f8(f7(a6),x37431))), % 116.84/116.82 inference(equality_inference,[],[3739])). % 116.84/116.82 cnf(3750,plain, % 116.84/116.82 (P2(f4(f8(x37501,a5),f8(x37501,a5),f7(a6)),x37502)+~E(f7(a6),f8(x37502,x37503))), % 116.84/116.82 inference(scs_inference,[],[3728,3695,3656,2686,2589,2,39,22,28])). % 116.84/116.82 cnf(3752,plain, % 116.84/116.82 (~E(f8(f8(a1,x37521),x37522),f7(a6))), % 116.84/116.82 inference(scs_inference,[],[3687,2])). % 116.84/116.82 cnf(3753,plain, % 116.84/116.82 (~E(f8(a5,f8(x37531,a5)),f8(a1,x37532))), % 116.84/116.82 inference(scs_inference,[],[3687,2714,20,2,28])). % 116.84/116.82 cnf(3755,plain, % 116.84/116.82 (P1(f4(f8(x37551,a5),f8(x37551,a5),f7(a6)),a6)), % 116.84/116.82 inference(scs_inference,[],[3687,2714,3658,19,20,2,28,15])). % 116.84/116.82 cnf(3756,plain, % 116.84/116.82 (P1(x37561,x37561)), % 116.84/116.82 inference(rename_variables,[],[19])). % 116.84/116.82 cnf(3759,plain, % 116.84/116.82 (~P2(f7(a6),x37591)+~E(x37591,f7(f8(a1,x37592)))), % 116.84/116.82 inference(scs_inference,[],[3711,3687,2714,3658,19,3756,20,2,28,15,14,23])). % 116.84/116.82 cnf(3764,plain, % 116.84/116.82 (~P2(f7(a6),f7(f8(a1,x37641)))), % 116.84/116.82 inference(equality_inference,[],[3759])). % 116.84/116.82 cnf(3767,plain, % 116.84/116.82 (E(a6,x37671)+~E(f8(f7(a6),f8(x37672,a5)),f7(x37671))), % 116.84/116.82 inference(scs_inference,[],[3753,2699,3654,2711,2,17,23])). % 116.84/116.82 cnf(3790,plain, % 116.84/116.82 (~E(f8(f8(a1,x37901),x37902),a5)), % 116.84/116.82 inference(scs_inference,[],[3712,2])). % 116.84/116.82 cnf(3797,plain, % 116.84/116.82 (~E(f8(x37971,f7(a6)),a5)), % 116.84/116.82 inference(scs_inference,[],[2690,2])). % 116.84/116.82 cnf(3805,plain, % 116.84/116.82 (~P2(x38051,a1)+P2(x38051,a5)), % 116.84/116.82 inference(scs_inference,[],[18,2803,2,26])). % 116.84/116.82 cnf(3816,plain, % 116.84/116.82 (P1(f4(f7(a6),f7(a6),f7(a6)),a6)), % 116.84/116.82 inference(scs_inference,[],[2792,2638,19,2,15])). % 116.84/116.82 cnf(3825,plain, % 116.84/116.82 (~P2(a5,f4(f7(a6),f7(a6),f7(a6)))), % 116.84/116.82 inference(scs_inference,[],[3816,2776,2717,2,26])). % 116.84/116.82 cnf(3843,plain, % 116.84/116.82 (~E(a5,x38431)+~E(f4(f7(a6),f7(a6),f7(a6)),f7(x38431))), % 116.84/116.82 inference(scs_inference,[],[3825,1347,2,22])). % 116.84/116.82 cnf(3847,plain, % 116.84/116.82 (E(a6,x38471)+~E(f7(a6),f7(x38471))), % 116.84/116.82 inference(scs_inference,[],[1113,2641,2,23])). % 116.84/116.82 cnf(3865,plain, % 116.84/116.82 (~P2(f8(f8(a1,x38651),x38652),x38653)+~E(x38653,f7(a5))), % 116.84/116.82 inference(scs_inference,[],[3790,137,2,23])). % 116.84/116.82 cnf(3870,plain, % 116.84/116.82 (~P2(f8(f8(a1,x38701),x38702),f7(a5))), % 116.84/116.82 inference(equality_inference,[],[3865])). % 116.84/116.82 cnf(3872,plain, % 116.84/116.82 (~E(f8(f8(a1,x38721),x38722),x38723)+~E(f7(a5),f7(x38723))), % 116.84/116.82 inference(scs_inference,[],[3870,120,2,22])). % 116.84/116.82 cnf(3875,plain, % 116.84/116.82 (~E(f8(f8(x38751,a5),x38752),f7(a6))), % 116.84/116.82 inference(scs_inference,[],[113,2])). % 116.84/116.82 cnf(3882,plain, % 116.84/116.82 (~E(f8(f8(x38821,a5),x38822),a5)), % 116.84/116.82 inference(scs_inference,[],[207,2])). % 116.84/116.82 cnf(3883,plain, % 116.84/116.82 (E(a6,x38831)+~E(f8(a5,f8(x38832,a5)),f7(x38831))), % 116.84/116.82 inference(scs_inference,[],[2714,207,2,23])). % 116.84/116.82 cnf(3956,plain, % 116.84/116.82 (~P2(f8(f8(x39561,a5),x39562),x39563)+~E(x39563,f7(a5))), % 116.84/116.82 inference(scs_inference,[],[3882,23])). % 116.84/116.82 cnf(3961,plain, % 116.84/116.82 (~P2(f8(f8(x39611,a5),x39612),f7(a5))), % 116.84/116.82 inference(equality_inference,[],[3956])). % 116.84/116.82 cnf(3962,plain, % 116.84/116.82 (E(a6,x39621)+~E(f8(f7(a6),a1),f7(x39621))), % 116.84/116.82 inference(scs_inference,[],[2648,23])). % 116.84/116.82 cnf(3978,plain, % 116.84/116.82 (~E(f8(f8(x39781,a5),x39782),x39783)+~E(f7(a5),f7(x39783))), % 116.84/116.82 inference(scs_inference,[],[3961,22])). % 116.84/116.82 cnf(3981,plain, % 116.84/116.82 (~P2(f8(x39811,f7(a6)),x39812)+~E(x39812,f7(a5))), % 116.84/116.82 inference(scs_inference,[],[3797,23])). % 116.84/116.82 cnf(3986,plain, % 116.84/116.82 (~P2(f8(x39861,f7(a6)),f7(a5))), % 116.84/116.82 inference(equality_inference,[],[3981])). % 116.84/116.82 cnf(3993,plain, % 116.84/116.82 (E(a6,x39931)+~E(a5,f7(x39931))), % 116.84/116.82 inference(scs_inference,[],[2691,23])). % 116.84/116.82 cnf(4023,plain, % 116.84/116.82 (E(a6,x40231)+~E(f8(f7(a6),f8(a1,x40232)),f7(x40231))), % 116.84/116.82 inference(scs_inference,[],[2671,23])). % 116.84/116.82 cnf(4080,plain, % 116.84/116.82 (~E(f7(f8(x40801,a5)),f7(f3(a5,x40802)))+E(x40802,f7(a5))+P2(f3(a5,x40802),x40802)), % 116.84/116.83 inference(scs_inference,[],[72,22,2,27])). % 116.84/116.83 cnf(4084,plain, % 116.84/116.83 (~E(f8(f7(a6),f8(x40841,a5)),f8(a1,x40842))), % 116.84/116.83 inference(scs_inference,[],[20,42,2711,2638,16,23,28])). % 116.84/116.83 cnf(4092,plain, % 116.84/116.83 (~P2(x40921,f4(f7(a6),a5,f7(a6)))+~E(x40921,f7(a6))), % 116.84/116.83 inference(scs_inference,[],[2681,16])). % 116.84/116.83 cnf(4102,plain, % 116.84/116.83 (~P2(f4(f8(x41021,a5),f8(x41021,a5),f7(a6)),a1)), % 116.84/116.83 inference(scs_inference,[],[20,3658,16])). % 116.84/116.83 cnf(4109,plain, % 116.84/116.83 (~P2(x41091,a1)+~E(x41091,f4(f8(x41092,a5),f8(x41092,a5),f7(a6)))), % 116.84/116.83 inference(scs_inference,[],[4102,16])). % 116.84/116.83 cnf(4115,plain, % 116.84/116.83 (~P2(f8(f8(a1,x41151),x41152),x41153)+~E(x41153,f8(f7(a5),x41154))), % 116.84/116.83 inference(scs_inference,[],[3870,4084,23,28])). % 116.84/116.83 cnf(4118,plain, % 116.84/116.83 (~P2(f8(f8(a1,x41181),x41182),f8(f7(a5),x41183))), % 116.84/116.83 inference(equality_inference,[],[4115])). % 116.84/116.83 cnf(4226,plain, % 116.84/116.83 (~P2(x42261,f8(f7(a1),x42262))+~E(x42261,f7(a6))), % 116.84/116.83 inference(scs_inference,[],[2669,16])). % 116.84/116.83 cnf(4236,plain, % 116.84/116.83 (~P2(f8(a1,x42361),x42362)+~E(x42362,f7(f7(a6)))), % 116.84/116.83 inference(scs_inference,[],[3689,23])). % 116.84/116.83 cnf(4239,plain, % 116.84/116.83 (~P2(f8(a1,x42391),f7(f7(a6)))), % 116.84/116.83 inference(equality_inference,[],[4236])). % 116.84/116.83 cnf(4259,plain, % 116.84/116.83 (~E(f8(a1,x42591),x42592)+~E(f7(f7(a6)),f7(x42592))), % 116.84/116.83 inference(scs_inference,[],[4239,22])). % 116.84/116.83 cnf(4262,plain, % 116.84/116.83 (E(f4(a5,f7(a6),a5),x42621)+~E(f7(a6),f7(x42621))), % 116.84/116.83 inference(scs_inference,[],[70,23])). % 116.84/116.83 cnf(4371,plain, % 116.84/116.83 (~P2(f8(x43711,a5),x43712)+~E(x43712,f7(a5))), % 116.84/116.83 inference(scs_inference,[],[121,23])). % 116.84/116.83 cnf(4384,plain, % 116.84/116.83 (~P2(f8(a1,x43841),x43842)+~E(x43842,f7(a5))), % 116.84/116.83 inference(scs_inference,[],[2777,23])). % 116.84/116.83 cnf(4397,plain, % 116.84/116.83 (~E(a5,x43971)+~E(f4(a5,f7(a6),a1),f7(x43971))), % 116.84/116.83 inference(scs_inference,[],[185,1114,30,22])). % 116.84/116.83 cnf(4429,plain, % 116.84/116.83 (~P2(x44291,f4(f7(a6),f7(a6),f7(a6)))+~E(x44291,f7(a6))), % 116.84/116.83 inference(scs_inference,[],[42,2600,3,16])). % 116.84/116.83 cnf(4585,plain, % 116.84/116.83 (~E(a5,x45851)+~E(f4(a5,f7(a6),a5),f7(x45851))), % 116.84/116.83 inference(scs_inference,[],[61,22])). % 116.84/116.83 cnf(4589,plain, % 116.84/116.83 (~P2(x45891,a1)+~E(x45891,f4(a5,f7(a6),a5))), % 116.84/116.83 inference(scs_inference,[],[3730,2642,30,16])). % 116.84/116.83 cnf(4645,plain, % 116.84/116.83 (P2(f4(f7(a6),f7(a6),f7(a6)),a5)), % 116.84/116.83 inference(scs_inference,[],[2651,2699,2638,2597,16,22,39])). % 116.84/116.83 cnf(4710,plain, % 116.84/116.83 (~E(a5,f7(f7(a5)))), % 116.84/116.83 inference(scs_inference,[],[4645,23,4371,4384,3843])). % 116.84/116.83 cnf(4714,plain, % 116.84/116.83 (~E(f7(f7(a5)),a5)), % 116.84/116.83 inference(scs_inference,[],[4710,2])). % 116.84/116.83 cnf(4733,plain, % 116.84/116.83 (~P2(f7(f7(a5)),x47331)+~E(x47331,f7(a5))), % 116.84/116.83 inference(scs_inference,[],[4714,23])). % 116.84/116.83 cnf(4738,plain, % 116.84/116.83 (~P2(f7(f7(a5)),f7(a5))), % 116.84/116.83 inference(equality_inference,[],[4733])). % 116.84/116.83 cnf(4799,plain, % 116.84/116.83 (~P2(x47991,f4(f8(x47992,a5),f8(x47992,a5),f7(a6)))+~E(x47991,f7(a6))), % 116.84/116.83 inference(scs_inference,[],[2590,4738,28,16])). % 116.84/116.83 cnf(4811,plain, % 116.84/116.83 (~P2(x48111,a6)+~E(x48111,f7(a6))), % 116.84/116.83 inference(scs_inference,[],[2642,16])). % 116.84/116.83 cnf(4890,plain, % 116.84/116.83 (~P2(f4(f8(x48901,a5),f8(x48901,a5),f7(a6)),f8(x48902,a5))), % 116.84/116.83 inference(scs_inference,[],[2699,3658,16])). % 116.84/116.83 cnf(4918,plain, % 116.84/116.83 (~E(x49181,f7(a6))+~E(f8(f8(a1,x49182),x49183),x49181)), % 116.84/116.83 inference(scs_inference,[],[4890,3752,16,3])). % 116.84/116.83 cnf(4957,plain, % 116.84/116.83 (~E(x49571,f7(a6))+~E(f8(f8(x49572,a5),x49573),x49571)), % 116.84/116.83 inference(scs_inference,[],[3875,3])). % 116.84/116.83 cnf(4958,plain, % 116.84/116.83 (~E(x49581,f8(f8(x49582,a5),x49583))+~E(x49581,f7(a6))), % 116.84/116.83 inference(scs_inference,[],[3875,3,2])). % 116.84/116.83 cnf(4981,plain, % 116.84/116.83 (~E(f8(a1,x49811),x49812)+~E(f7(a5),f7(x49812))), % 116.84/116.83 inference(scs_inference,[],[2778,22])). % 116.84/116.83 cnf(5049,plain, % 116.84/116.83 (~P2(x50491,f4(a5,f7(a6),a5))+~E(x50491,f7(a6))), % 116.84/116.83 inference(scs_inference,[],[80,16])). % 116.84/116.83 cnf(5088,plain, % 116.84/116.83 (~P2(x50881,f8(f8(a6,x50882),x50883))+~E(x50881,f7(a6))), % 116.84/116.83 inference(scs_inference,[],[2657,16])). % 116.84/116.83 cnf(5141,plain, % 116.84/116.83 (~E(x51411,f7(a6))+~E(f8(a1,x51412),x51411)), % 116.84/116.83 inference(scs_inference,[],[3689,3])). % 116.84/116.83 cnf(5142,plain, % 116.84/116.83 (~P2(x51421,f7(f8(x51422,a5)))+~E(x51421,f7(a6))), % 116.84/116.83 inference(scs_inference,[],[87,16])). % 116.84/116.83 cnf(5156,plain, % 116.84/116.83 (~P2(x51561,f8(a6,x51562))+~E(x51561,f7(a6))), % 116.84/116.83 inference(scs_inference,[],[2644,16])). % 116.84/116.83 cnf(5159,plain, % 116.84/116.83 (~E(f7(a6),x51591)+~E(a6,f7(x51591))), % 116.84/116.83 inference(scs_inference,[],[2642,22])). % 116.84/116.83 cnf(5175,plain, % 116.84/116.83 (~E(x51751,f7(a6))+~E(f8(x51752,a5),x51751)), % 116.84/116.83 inference(scs_inference,[],[100,3])). % 116.84/116.83 cnf(5176,plain, % 116.84/116.83 (~E(a6,f7(f7(f4(f7(a6),f7(a6),f7(a6)))))), % 116.84/116.83 inference(scs_inference,[],[2639,5159,4])). % 116.84/116.83 cnf(5201,plain, % 116.84/116.83 (~P2(x52011,f7(f8(a1,x52012)))+~E(x52011,f7(a6))), % 116.84/116.83 inference(scs_inference,[],[3764,16])). % 116.84/116.83 cnf(5228,plain, % 116.84/116.83 (~E(f8(x52281,f7(a6)),x52282)+~E(f7(a5),f7(x52282))), % 116.84/116.83 inference(scs_inference,[],[3986,22])). % 116.84/116.83 cnf(5263,plain, % 116.84/116.83 (~E(x52631,f7(a6))+~E(f8(x52632,f7(a6)),x52631)), % 116.84/116.83 inference(scs_inference,[],[3663,3])). % 116.84/116.83 cnf(5286,plain, % 116.84/116.83 (~E(f8(a1,x52861),x52862)+~E(f8(f7(a5),x52863),f7(x52862))), % 116.84/116.83 inference(scs_inference,[],[2790,22])). % 116.84/116.83 cnf(5315,plain, % 116.84/116.83 (~P2(x53151,f7(a1))+~E(x53151,f7(a6))), % 116.84/116.83 inference(scs_inference,[],[2651,16])). % 116.84/116.83 cnf(5390,plain, % 116.84/116.83 (~E(a5,x53901)+~E(f8(a6,x53902),f7(x53901))), % 116.84/116.83 inference(scs_inference,[],[2763,22])). % 116.84/116.83 cnf(5438,plain, % 116.84/116.83 (~E(x54381,f7(a6))+~E(a1,x54381)), % 116.84/116.83 inference(scs_inference,[],[2750,3])). % 116.84/116.83 cnf(5450,plain, % 116.84/116.83 (~E(f8(x54501,a5),x54502)+~E(f7(a5),f7(x54502))), % 116.84/116.83 inference(scs_inference,[],[159,22])). % 116.84/116.83 cnf(5527,plain, % 116.84/116.83 (~E(x55271,f8(a1,x55272))+~E(x55271,f7(a6))), % 116.84/116.83 inference(scs_inference,[],[5141,2])). % 116.84/116.83 cnf(5570,plain, % 116.84/116.83 (~P2(f8(a6,x55701),f7(f7(x55702)))+~E(a5,x55702)), % 116.84/116.83 inference(scs_inference,[],[5390,36])). % 116.84/116.83 cnf(5571,plain, % 116.84/116.83 (~P2(f8(a6,x55711),f7(f7(a5)))), % 116.84/116.83 inference(equality_inference,[],[5570])). % 116.84/116.83 cnf(5572,plain, % 116.84/116.83 (~E(f8(a6,x55721),x55722)+~E(f7(f7(a5)),f7(x55722))), % 116.84/116.83 inference(scs_inference,[],[5571,22])). % 116.84/116.83 cnf(5894,plain, % 116.84/116.83 (~E(f7(x58941),f7(f7(a6)))+~E(f8(a1,x58942),x58941)), % 116.84/116.83 inference(scs_inference,[],[4259,2])). % 116.84/116.83 cnf(5897,plain, % 116.84/116.83 (~P2(f4(a5,f7(a6),a1),f7(f7(x58971)))+~E(a5,x58971)), % 116.84/116.83 inference(scs_inference,[],[4397,36])). % 116.84/116.83 cnf(5898,plain, % 116.84/116.83 (~P2(f4(a5,f7(a6),a1),f7(f7(a5)))), % 116.84/116.83 inference(equality_inference,[],[5897])). % 116.84/116.83 cnf(5910,plain, % 116.84/116.83 (~E(f7(a6),f7(f7(x59101)))+~E(a5,x59101)), % 116.84/116.83 inference(scs_inference,[],[4585,4262])). % 116.84/116.83 cnf(5911,plain, % 116.84/116.83 (~E(f7(f7(x59111)),f7(a6))+~E(a5,x59111)), % 116.84/116.83 inference(scs_inference,[],[5910,2])). % 116.84/116.83 cnf(5912,plain, % 116.84/116.83 (~E(f7(x59121),a6)+~E(a5,x59121)), % 116.84/116.83 inference(scs_inference,[],[5911,4])). % 116.84/116.83 cnf(5913,plain, % 116.84/116.83 (~E(x59131,a5)+~E(f7(x59131),a6)), % 116.84/116.83 inference(scs_inference,[],[5912,2])). % 116.84/116.83 cnf(5914,plain, % 116.84/116.83 (~P2(f7(x59141),f7(a6))+~E(x59141,a5)), % 116.84/116.83 inference(scs_inference,[],[5913,36])). % 116.84/116.83 cnf(5915,plain, % 116.84/116.83 (~P2(f7(a5),f7(a6))), % 116.84/116.83 inference(equality_inference,[],[5914])). % 116.84/116.83 cnf(5916,plain, % 116.84/116.83 (~E(a6,f7(a5))), % 116.84/116.83 inference(scs_inference,[],[5915,2641,16])). % 116.84/116.83 cnf(5919,plain, % 116.84/116.83 (~E(f7(a5),a6)), % 116.84/116.83 inference(scs_inference,[],[5915,2641,16,3847,2])). % 116.84/116.83 cnf(5920,plain, % 116.84/116.83 (~E(f7(a5),x59201)+~E(f7(a6),f7(x59201))), % 116.84/116.83 inference(scs_inference,[],[5915,2641,16,3847,2,22])). % 116.84/116.83 cnf(5927,plain, % 116.84/116.83 (~E(f7(a5),f4(f7(a6),a5,f7(a6)))), % 116.84/116.83 inference(scs_inference,[],[1330,5920,4])). % 116.84/116.83 cnf(5929,plain, % 116.84/116.83 (~E(f4(f7(a6),f7(a6),f7(a6)),f7(a5))), % 116.84/116.83 inference(scs_inference,[],[5916,5927,2639,2,3])). % 116.84/116.83 cnf(5930,plain, % 116.84/116.83 (~E(f7(f7(a5)),f7(a6))), % 116.84/116.83 inference(scs_inference,[],[5916,5927,2639,2,3,3733])). % 116.84/116.83 cnf(5936,plain, % 116.84/116.83 (~E(f7(a5),f4(f7(a6),f7(a6),f7(a6)))), % 116.84/116.83 inference(scs_inference,[],[5929,2])). % 116.84/116.83 cnf(5937,plain, % 116.84/116.83 (~E(f7(a5),f4(a5,f7(a6),a5))), % 116.84/116.83 inference(scs_inference,[],[5929,5919,3684,2,3])). % 116.84/116.83 cnf(5940,plain, % 116.84/116.83 (~E(x59401,f7(a6))+~E(f7(f7(a5)),x59401)), % 116.84/116.83 inference(scs_inference,[],[5930,5937,2,3])). % 116.84/116.83 cnf(5941,plain, % 116.84/116.83 (~E(f7(a5),x59411)+~E(f7(x59411),f7(a6))), % 116.84/116.83 inference(scs_inference,[],[5940,4])). % 116.84/116.83 cnf(5948,plain, % 116.84/116.83 (~E(f7(a5),f4(f8(x59481,a5),f8(x59481,a5),f7(a6)))), % 116.84/116.83 inference(scs_inference,[],[3658,5941,4])). % 116.84/116.83 cnf(5949,plain, % 116.84/116.83 (~E(f4(f8(x59491,a5),f8(x59491,a5),f7(a6)),f7(a5))), % 116.84/116.83 inference(scs_inference,[],[5948,2])). % 116.84/116.83 cnf(5970,plain, % 116.84/116.83 (~E(x59701,f8(f8(a1,x59702),x59703))+~E(x59701,f7(a6))), % 116.84/116.83 inference(scs_inference,[],[4918,2])). % 116.84/116.83 cnf(6007,plain, % 116.84/116.83 (~E(f7(a5),x60071)+~E(f8(a6,x60072),x60071)), % 116.84/116.83 inference(scs_inference,[],[5572,4])). % 116.84/116.83 cnf(6008,plain, % 116.84/116.83 (~E(f7(a5),f8(f4(f7(a6),f7(a6),f7(a6)),x60081))), % 116.84/116.83 inference(scs_inference,[],[2639,6007,5])). % 116.84/116.83 cnf(6034,plain, % 116.84/116.83 (~E(f7(f8(a1,a6)),f7(f7(a6)))), % 116.84/116.83 inference(scs_inference,[],[3684,5894,6])). % 116.84/116.83 cnf(6095,plain, % 116.84/116.83 (P2(f2(a1,f8(a5,f7(a6))),a1)), % 116.84/116.83 inference(scs_inference,[],[3667,245,2721,21,5438,5315,5175,5527,4226,5201,4429,4799,3743,488,25])). % 116.84/116.83 cnf(6100,plain, % 116.84/116.83 (E(f4(f7(a6),f7(a6),f7(a6)),f4(a5,f7(a6),a5))), % 116.84/116.83 inference(scs_inference,[],[3667,3666,245,2721,21,5438,5315,5175,5527,4226,5201,4429,4799,3743,488,25,12,472,3733])). % 116.84/116.83 cnf(6102,plain, % 116.84/116.83 (~P2(f2(a1,f8(a5,f7(a6))),f8(a5,f7(a6)))), % 116.84/116.83 inference(scs_inference,[],[3667,3666,245,2721,21,5438,5315,5175,5527,4226,5201,4429,4799,3743,488,25,12,472,3733,31])). % 116.84/116.83 cnf(6109,plain, % 116.84/116.83 (P2(a6,f8(f8(f8(f7(a6),f8(x61091,a5)),f8(a1,x61092)),f8(a1,x61093)))), % 116.84/116.83 inference(scs_inference,[],[3667,3666,245,5176,2721,21,5438,5315,5175,5527,4226,5201,4429,4799,3743,488,25,12,472,3733,31,9,3993,24,47])). % 116.84/116.83 cnf(6115,plain, % 116.84/116.83 (E(f8(f4(f8(x61151,a5),f8(x61151,a5),f7(a6)),x61152),f8(f4(f7(a6),f7(a6),f7(a6)),x61152))), % 116.84/116.83 inference(scs_inference,[],[3667,3666,245,5176,2721,21,5438,5315,5175,5527,4226,5201,4429,4799,3743,488,25,12,472,3733,31,9,3993,24,47,13,3847,4,5])). % 116.84/116.83 cnf(6116,plain, % 116.84/116.83 (E(f8(x61161,f4(f8(x61162,a5),f8(x61162,a5),f7(a6))),f8(x61161,f4(f7(a6),f7(a6),f7(a6))))), % 116.84/116.83 inference(scs_inference,[],[3667,3666,245,5176,2721,21,5438,5315,5175,5527,4226,5201,4429,4799,3743,488,25,12,472,3733,31,9,3993,24,47,13,3847,4,5,6])). % 116.84/116.83 cnf(6123,plain, % 116.84/116.83 (P1(x61231,x61231)), % 116.84/116.83 inference(rename_variables,[],[19])). % 116.84/116.83 cnf(6127,plain, % 116.84/116.83 (E(f4(f8(x61271,a5),f8(x61271,a5),f7(a6)),f4(f7(a6),f7(a6),f7(a6)))), % 116.84/116.83 inference(rename_variables,[],[3666])). % 116.84/116.83 cnf(6148,plain, % 116.84/116.83 (~P2(f7(f4(a5,f7(a6),a5)),f8(a6,x61481))), % 116.84/116.83 inference(scs_inference,[],[2703,1423,3667,3666,6127,245,615,631,5176,2667,5936,2735,2654,1421,2592,2721,3755,4645,19,6123,21,5438,5315,5175,5527,4226,5201,4429,4799,3743,488,25,12,472,3733,31,9,3993,24,47,13,3847,4,5,6,8,10,11,7,2,15,29,22,28,26,17,23,3,16,14,39,30,4811,5141,5156])). % 116.84/116.83 cnf(6163,plain, % 116.84/116.83 (~E(f2(a1,f8(a5,f7(a6))),f4(f8(x61631,a5),f8(x61631,a5),f7(a6)))), % 116.84/116.83 inference(scs_inference,[],[2703,1423,3667,3666,6127,245,615,631,5176,2667,5936,2735,2654,1421,2592,2721,3755,4645,19,6123,21,5438,5315,5175,5527,4226,5201,4429,4799,3743,488,25,12,472,3733,31,9,3993,24,47,13,3847,4,5,6,8,10,11,7,2,15,29,22,28,26,17,23,3,16,14,39,30,4811,5141,5156,5940,5142,5263,5450,4918,4957,4958,5088,5970,3737,5049,4092,4109])). % 116.84/116.83 cnf(6182,plain, % 116.84/116.83 (P2(f2(a1,f8(a5,f7(a6))),a5)), % 116.84/116.83 inference(scs_inference,[],[2703,1423,3667,3666,6127,245,615,631,5176,2667,5936,2735,2654,1421,2592,2721,3755,4645,19,6123,21,5438,5315,5175,5527,4226,5201,4429,4799,3743,488,25,12,472,3733,31,9,3993,24,47,13,3847,4,5,6,8,10,11,7,2,15,29,22,28,26,17,23,3,16,14,39,30,4811,5141,5156,5940,5142,5263,5450,4918,4957,4958,5088,5970,3737,5049,4092,4109,3717,3750,3731,3724,4023,3883,3767,3962,3693,3805])). % 116.84/116.83 cnf(6188,plain, % 116.84/116.83 (~E(f2(a1,f8(a5,f7(a6))),f4(a5,f7(a6),a5))), % 116.84/116.83 inference(scs_inference,[],[2703,1423,3667,3666,6127,245,615,631,5176,2667,5949,5936,2735,2654,1421,2592,2721,3755,4645,19,6123,21,5438,5315,5175,5527,4226,5201,4429,4799,3743,488,25,12,472,3733,31,9,3993,24,47,13,3847,4,5,6,8,10,11,7,2,15,29,22,28,26,17,23,3,16,14,39,30,4811,5141,5156,5940,5142,5263,5450,4918,4957,4958,5088,5970,3737,5049,4092,4109,3717,3750,3731,3724,4023,3883,3767,3962,3693,3805,36,4080,4589])). % 116.84/116.83 cnf(6199,plain, % 116.84/116.83 (E(f8(x61991,f4(f8(x61992,a5),f8(x61992,a5),f7(a6))),f8(x61991,f4(f7(a6),f7(a6),f7(a6))))), % 116.84/116.83 inference(rename_variables,[],[6116])). % 116.84/116.83 cnf(6202,plain, % 116.84/116.83 (E(f8(f4(f8(x62021,a5),f8(x62021,a5),f7(a6)),x62022),f8(f4(f7(a6),f7(a6),f7(a6)),x62022))), % 116.84/116.83 inference(rename_variables,[],[6115])). % 116.84/116.83 cnf(6205,plain, % 116.84/116.83 (E(f8(x62051,f4(f8(x62052,a5),f8(x62052,a5),f7(a6))),f8(x62051,f4(f7(a6),f7(a6),f7(a6))))), % 116.84/116.83 inference(rename_variables,[],[6116])). % 116.84/116.83 cnf(6208,plain, % 116.84/116.83 (E(f8(x62081,f4(f8(x62082,a5),f8(x62082,a5),f7(a6))),f8(x62081,f4(f7(a6),f7(a6),f7(a6))))), % 116.84/116.83 inference(rename_variables,[],[6116])). % 116.84/116.83 cnf(6211,plain, % 116.84/116.83 (E(f8(x62111,f4(f8(x62112,a5),f8(x62112,a5),f7(a6))),f8(x62111,f4(f7(a6),f7(a6),f7(a6))))), % 116.84/116.83 inference(rename_variables,[],[6116])). % 116.84/116.83 cnf(6219,plain, % 116.84/116.83 (P2(a6,f8(f8(f8(f8(f7(a6),f8(x62191,a5)),f8(a1,x62192)),f8(a1,x62193)),f8(a1,x62194)))), % 116.84/116.83 inference(scs_inference,[],[6100,6109,6115,6116,6199,6205,6208,2688,4981,5228,5572,5894,5286,488,472,12,9,47])). % 116.84/116.83 cnf(6221,plain, % 116.84/116.83 (~P2(f8(f8(f8(f7(a6),f8(x62211,a5)),f8(a1,x62212)),f8(a1,x62213)),a6)), % 116.84/116.83 inference(scs_inference,[],[6100,6109,6115,6116,6199,6205,6208,2688,4981,5228,5572,5894,5286,488,472,12,9,47,24])). % 116.84/116.83 cnf(6226,plain, % 116.84/116.83 (E(f8(x62261,f4(f7(a6),f7(a6),f7(a6))),f8(x62261,f4(a5,f7(a6),a5)))), % 116.84/116.83 inference(scs_inference,[],[6100,6109,6115,6116,6199,6205,6208,2688,4981,5228,5572,5894,5286,488,472,12,9,47,24,13,4,5,6])). % 116.84/116.83 cnf(6232,plain, % 116.84/116.83 (~E(f8(f8(f8(f7(a6),f8(x62321,a5)),f8(a1,x62322)),f8(a1,x62323)),f8(x62324,f8(f8(f8(f7(a6),f8(x62321,a5)),f8(a1,x62322)),f8(a1,x62323))))), % 116.84/116.83 inference(scs_inference,[],[6100,6034,6109,6115,6116,6199,6205,6208,2688,4981,5228,5572,5894,5286,488,472,12,9,47,24,13,4,5,6,8,10,11,7,2,29])). % 116.84/116.83 cnf(6236,plain, % 116.84/116.83 (E(f8(x62361,f4(f8(x62362,a5),f8(x62362,a5),f7(a6))),f8(x62361,f4(f7(a6),f7(a6),f7(a6))))), % 116.84/116.83 inference(rename_variables,[],[6116])). % 116.84/116.83 cnf(6238,plain, % 116.84/116.83 (~E(f8(f8(f8(f7(a6),f8(x62381,a5)),f8(a1,x62382)),f8(a1,x62383)),f8(f8(x62384,a5),x62385))), % 116.84/116.83 inference(scs_inference,[],[6100,4118,6034,6109,6115,6116,6199,6205,6208,6211,2688,2699,4981,5228,5572,5894,5286,488,472,12,9,47,24,13,4,5,6,8,10,11,7,2,29,22,28])). % 116.84/116.83 cnf(6240,plain, % 116.84/116.83 (~E(f8(a5,f8(x62401,a5)),f7(f7(a5)))), % 116.84/116.83 inference(scs_inference,[],[6100,4118,5898,6034,6109,6115,6116,6199,6205,6208,6211,2688,189,2699,4981,5228,5572,5894,5286,488,472,12,9,47,24,13,4,5,6,8,10,11,7,2,29,22,28,17])). % 116.84/116.83 cnf(6246,plain, % 116.84/116.83 (P2(f2(a1,f8(a5,f7(a6))),f7(a6))), % 116.84/116.83 inference(scs_inference,[],[6100,4118,5898,6034,6148,6109,6008,6182,6188,6102,6115,6202,6116,6199,6205,6208,6211,2688,189,2699,4981,5228,5572,5894,5286,488,472,12,9,47,24,13,4,5,6,8,10,11,7,2,29,22,28,17,23,3,16,39])). % 116.84/116.83 cnf(6251,plain, % 116.84/116.83 (E(f8(x62511,f4(f8(x62512,a5),f8(x62512,a5),f7(a6))),f8(x62511,f4(f7(a6),f7(a6),f7(a6))))), % 116.84/116.83 inference(rename_variables,[],[6116])). % 116.84/116.83 cnf(6254,plain, % 116.84/116.83 (E(f8(x62541,f4(f8(x62542,a5),f8(x62542,a5),f7(a6))),f8(x62541,f4(f7(a6),f7(a6),f7(a6))))), % 116.84/116.83 inference(rename_variables,[],[6116])). % 116.84/116.83 cnf(6257,plain, % 116.84/116.83 (E(f8(x62571,f4(f8(x62572,a5),f8(x62572,a5),f7(a6))),f8(x62571,f4(f7(a6),f7(a6),f7(a6))))), % 116.84/116.83 inference(rename_variables,[],[6116])). % 116.84/116.83 cnf(6262,plain, % 116.84/116.83 (E(f2(a1,f8(a5,f7(a6))),a6)), % 116.84/116.83 inference(scs_inference,[],[6100,4118,5898,6034,6148,6109,6008,6182,6188,6102,6115,6202,6116,6199,6205,6208,6211,6236,6251,6254,6257,2688,189,2699,4981,5228,5572,5894,5286,488,472,12,9,47,24,13,4,5,6,8,10,11,7,2,29,22,28,17,23,3,16,39,30,6007,4259,3872,3978,36])). % 116.84/116.83 cnf(6300,plain, % 116.84/116.83 (~E(f7(a6),f7(f4(f8(x63001,a5),f8(x63001,a5),f7(a6))))), % 116.84/116.83 inference(scs_inference,[],[2820,6240,647,6246,6221,6095,6262,6163,6219,6226,2747,3816,488,472,12,9,47,24,13,4,5,6,8,10,11,7,2,29,22,26,28,17,23])). % 116.84/116.83 cnf(6316,plain, % 116.84/116.83 (E(a6,f4(f8(x63161,a5),f8(x63161,a5),f7(a6)))), % 116.84/116.83 inference(scs_inference,[],[3658,2])). % 116.84/116.83 cnf(6356,plain, % 116.84/116.83 ($false), % 116.84/116.83 inference(scs_inference,[],[99,245,3654,2646,6316,6238,6232,6300,2,38,36,6,37,5,4]), % 116.84/116.83 ['proof']). % 116.84/116.83 % SZS output end Proof % 116.84/116.83 % Total time :116.120000s %------------------------------------------------------------------------------