%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SEU124+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 : n020.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:09 EDT 2024 % Result : Theorem 117.06s 117.21s % Output : CNFRefutation 117.23s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SEU124+1 : TPTP v8.2.0. Released v3.3.0. % 0.00/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n020.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 12:20:54 EDT 2024 % 0.12/0.33 % CPUTime : % 0.18/0.55 start to proof:theBenchmark % 117.06/117.19 %------------------------------------------- % 117.06/117.19 % File :CSE---1.7 % 117.06/117.19 % Problem :theBenchmark % 117.06/117.19 % Transform :cnf % 117.06/117.19 % Format :tptp:raw % 117.06/117.19 % Command :java -jar mcs_scs.jar %d %s % 117.06/117.19 % 117.06/117.19 % Result :Theorem 116.500000s % 117.06/117.19 % Output :CNFRefutation 116.500000s % 117.06/117.19 %------------------------------------------- % 117.06/117.21 %------------------------------------------------------------------------------ % 117.06/117.21 % File : SEU124+1 : TPTP v8.2.0. Released v3.3.0. % 117.06/117.21 % Domain : Set theory % 117.06/117.21 % Problem : MPTP bushy problem t7_xboole_1 % 117.06/117.21 % Version : [Urb07] axioms : Especial. % 117.06/117.21 % English : % 117.06/117.21 % 117.06/117.21 % Refs : [Ban01] Bancerek et al. (2001), On the Characterizations of Co % 117.06/117.21 % : [Urb07] Urban (2006), Email to G. Sutcliffe % 117.06/117.21 % Source : [Urb07] % 117.06/117.21 % Names : bushy-t7_xboole_1 [Urb07] % 117.06/117.21 % 117.06/117.21 % Status : Theorem % 117.06/117.21 % Rating : 0.17 v7.5.0, 0.19 v7.4.0, 0.07 v7.3.0, 0.10 v7.2.0, 0.07 v7.1.0, 0.04 v7.0.0, 0.07 v6.4.0, 0.12 v6.2.0, 0.24 v6.1.0, 0.27 v6.0.0, 0.22 v5.5.0, 0.15 v5.4.0, 0.21 v5.3.0, 0.30 v5.2.0, 0.10 v5.0.0, 0.17 v4.1.0, 0.22 v4.0.0, 0.25 v3.7.0, 0.20 v3.5.0, 0.21 v3.3.0 % 117.06/117.21 % Syntax : Number of formulae : 18 ( 10 unt; 0 def) % 117.06/117.21 % Number of atoms : 30 ( 6 equ) % 117.06/117.21 % Maximal formula atoms : 4 ( 1 avg) % 117.06/117.21 % Number of connectives : 21 ( 9 ~; 1 |; 3 &) % 117.06/117.21 % ( 3 <=>; 5 =>; 0 <=; 0 <~>) % 117.06/117.21 % Maximal formula depth : 8 ( 4 avg) % 117.06/117.21 % Maximal term depth : 2 ( 1 avg) % 117.06/117.21 % Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty) % 117.06/117.21 % Number of functors : 2 ( 2 usr; 1 con; 0-2 aty) % 117.06/117.21 % Number of variables : 29 ( 27 !; 2 ?) % 117.06/117.21 % SPC : FOF_THM_RFO_SEQ % 117.06/117.21 % 117.06/117.21 % Comments : Translated by MPTP 0.2 from the original problem in the Mizar % 117.06/117.21 % library, www.mizar.org % 117.06/117.21 %------------------------------------------------------------------------------ % 117.06/117.21 fof(antisymmetry_r2_hidden,axiom, % 117.06/117.21 ! [A,B] : % 117.06/117.21 ( in(A,B) % 117.06/117.21 => ~ in(B,A) ) ). % 117.06/117.21 % 117.06/117.21 fof(commutativity_k2_xboole_0,axiom, % 117.06/117.21 ! [A,B] : set_union2(A,B) = set_union2(B,A) ). % 117.06/117.21 % 117.06/117.21 fof(d2_xboole_0,axiom, % 117.06/117.21 ! [A,B,C] : % 117.06/117.21 ( C = set_union2(A,B) % 117.06/117.21 <=> ! [D] : % 117.06/117.21 ( in(D,C) % 117.06/117.21 <=> ( in(D,A) % 117.06/117.21 | in(D,B) ) ) ) ). % 117.06/117.21 % 117.06/117.21 fof(d3_tarski,axiom, % 117.06/117.21 ! [A,B] : % 117.06/117.21 ( subset(A,B) % 117.06/117.21 <=> ! [C] : % 117.06/117.21 ( in(C,A) % 117.06/117.21 => in(C,B) ) ) ). % 117.06/117.21 % 117.06/117.21 fof(dt_k1_xboole_0,axiom, % 117.06/117.21 $true ). % 117.06/117.21 % 117.06/117.21 fof(dt_k2_xboole_0,axiom, % 117.06/117.21 $true ). % 117.06/117.21 % 117.06/117.21 fof(fc1_xboole_0,axiom, % 117.06/117.21 empty(empty_set) ). % 117.06/117.21 % 117.06/117.21 fof(fc2_xboole_0,axiom, % 117.06/117.21 ! [A,B] : % 117.06/117.21 ( ~ empty(A) % 117.06/117.21 => ~ empty(set_union2(A,B)) ) ). % 117.06/117.21 % 117.06/117.21 fof(fc3_xboole_0,axiom, % 117.06/117.21 ! [A,B] : % 117.06/117.21 ( ~ empty(A) % 117.06/117.21 => ~ empty(set_union2(B,A)) ) ). % 117.06/117.21 % 117.06/117.21 fof(idempotence_k2_xboole_0,axiom, % 117.06/117.21 ! [A,B] : set_union2(A,A) = A ). % 117.06/117.21 % 117.06/117.21 fof(rc1_xboole_0,axiom, % 117.06/117.21 ? [A] : empty(A) ). % 117.06/117.21 % 117.06/117.21 fof(rc2_xboole_0,axiom, % 117.06/117.21 ? [A] : ~ empty(A) ). % 117.06/117.21 % 117.06/117.21 fof(reflexivity_r1_tarski,axiom, % 117.06/117.21 ! [A,B] : subset(A,A) ). % 117.06/117.21 % 117.06/117.21 fof(t1_boole,axiom, % 117.06/117.21 ! [A] : set_union2(A,empty_set) = A ). % 117.06/117.21 % 117.06/117.21 fof(t6_boole,axiom, % 117.06/117.21 ! [A] : % 117.06/117.21 ( empty(A) % 117.06/117.21 => A = empty_set ) ). % 117.06/117.21 % 117.06/117.21 fof(t7_boole,axiom, % 117.06/117.21 ! [A,B] : % 117.06/117.21 ~ ( in(A,B) % 117.06/117.21 & empty(B) ) ). % 117.06/117.21 % 117.06/117.21 fof(t7_xboole_1,conjecture, % 117.06/117.21 ! [A,B] : subset(A,set_union2(A,B)) ). % 117.06/117.21 % 117.06/117.21 fof(t8_boole,axiom, % 117.06/117.21 ! [A,B] : % 117.06/117.21 ~ ( empty(A) % 117.06/117.21 & A != B % 117.06/117.21 & empty(B) ) ). % 117.06/117.21 % 117.06/117.21 %------------------------------------------------------------------------------ % 117.06/117.21 %------------------------------------------- % 117.06/117.21 % Proof found % 117.06/117.21 % SZS status Theorem for theBenchmark % 117.06/117.21 % SZS output start Proof % 117.06/117.22 %ClaNum:38(EqnAxiom:15) % 117.06/117.22 %VarNum:106(SingletonVarNum:44) % 117.06/117.22 %MaxLitNum:4 % 117.06/117.22 %MaxfuncDepth:1 % 117.06/117.22 %SharedTerms:10 % 117.06/117.22 %goalClause: 23 % 117.06/117.22 %singleGoalClaCount:1 % 117.06/117.22 [16]P1(a1) % 117.06/117.22 [17]P1(a2) % 117.06/117.22 [22]~P1(a6) % 117.06/117.22 [23]~P2(a7,f5(a7,a8)) % 117.06/117.22 [19]P2(x191,x191) % 117.06/117.22 [18]E(f5(x181,a1),x181) % 117.06/117.22 [20]E(f5(x201,x201),x201) % 117.06/117.22 [21]E(f5(x211,x212),f5(x212,x211)) % 117.06/117.22 [24]~P1(x241)+E(x241,a1) % 117.06/117.22 [26]~P1(x261)+~P3(x262,x261) % 117.06/117.22 [27]~P3(x272,x271)+~P3(x271,x272) % 117.06/117.23 [28]P1(x281)+~P1(f5(x282,x281)) % 117.06/117.23 [29]P1(x291)+~P1(f5(x291,x292)) % 117.06/117.23 [30]P2(x301,x302)+P3(f3(x301,x302),x301) % 117.06/117.23 [35]P2(x351,x352)+~P3(f3(x351,x352),x352) % 117.06/117.23 [25]~P1(x252)+~P1(x251)+E(x251,x252) % 117.06/117.23 [31]~P2(x313,x312)+P3(x311,x312)+~P3(x311,x313) % 117.06/117.23 [37]~P3(f4(x372,x373,x371),x371)+~P3(f4(x372,x373,x371),x373)+E(x371,f5(x372,x373)) % 117.06/117.23 [38]~P3(f4(x382,x383,x381),x381)+~P3(f4(x382,x383,x381),x382)+E(x381,f5(x382,x383)) % 117.06/117.23 [32]~P3(x321,x324)+P3(x321,x322)+~E(x322,f5(x323,x324)) % 117.06/117.23 [33]~P3(x331,x333)+P3(x331,x332)+~E(x332,f5(x333,x334)) % 117.06/117.23 [36]P3(f4(x362,x363,x361),x361)+P3(f4(x362,x363,x361),x363)+P3(f4(x362,x363,x361),x362)+E(x361,f5(x362,x363)) % 117.06/117.23 [34]~P3(x341,x344)+P3(x341,x342)+P3(x341,x343)+~E(x344,f5(x343,x342)) % 117.06/117.23 %EqnAxiom % 117.06/117.23 [1]E(x11,x11) % 117.06/117.23 [2]E(x22,x21)+~E(x21,x22) % 117.06/117.23 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 117.06/117.23 [4]~E(x41,x42)+E(f5(x41,x43),f5(x42,x43)) % 117.06/117.23 [5]~E(x51,x52)+E(f5(x53,x51),f5(x53,x52)) % 117.06/117.23 [6]~E(x61,x62)+E(f4(x61,x63,x64),f4(x62,x63,x64)) % 117.06/117.23 [7]~E(x71,x72)+E(f4(x73,x71,x74),f4(x73,x72,x74)) % 117.06/117.23 [8]~E(x81,x82)+E(f4(x83,x84,x81),f4(x83,x84,x82)) % 117.06/117.23 [9]~E(x91,x92)+E(f3(x91,x93),f3(x92,x93)) % 117.06/117.23 [10]~E(x101,x102)+E(f3(x103,x101),f3(x103,x102)) % 117.06/117.23 [11]~P1(x111)+P1(x112)+~E(x111,x112) % 117.06/117.23 [12]P3(x122,x123)+~E(x121,x122)+~P3(x121,x123) % 117.06/117.23 [13]P3(x133,x132)+~E(x131,x132)+~P3(x133,x131) % 117.06/117.23 [14]P2(x142,x143)+~E(x141,x142)+~P2(x141,x143) % 117.06/117.23 [15]P2(x153,x152)+~E(x151,x152)+~P2(x153,x151) % 117.06/117.23 % 117.06/117.23 %------------------------------------------- % 117.06/117.25 cnf(39,plain, % 117.06/117.25 (~P3(x391,x392)+P3(x391,f5(x393,x392))), % 117.06/117.25 inference(equality_inference,[],[32])). % 117.06/117.25 cnf(40,plain, % 117.06/117.25 (~P3(x401,x402)+P3(x401,f5(x402,x403))), % 117.06/117.25 inference(equality_inference,[],[33])). % 117.06/117.25 cnf(41,plain, % 117.06/117.25 (~P3(x411,f5(x412,x413))+P3(x411,x413)+P3(x411,x412)), % 117.06/117.25 inference(equality_inference,[],[34])). % 117.06/117.25 cnf(42,plain, % 117.06/117.25 (~P3(x421,a1)), % 117.06/117.25 inference(scs_inference,[],[16,26])). % 117.06/117.25 cnf(44,plain, % 117.06/117.25 (E(x441,f5(x441,x441))), % 117.06/117.25 inference(scs_inference,[],[20,16,26,2])). % 117.06/117.25 cnf(46,plain, % 117.06/117.25 (P2(x461,x461)), % 117.06/117.25 inference(rename_variables,[],[19])). % 117.06/117.25 cnf(47,plain, % 117.06/117.25 (~E(a7,f5(a7,a8))), % 117.06/117.25 inference(scs_inference,[],[23,19,46,20,16,26,2,14,15])). % 117.06/117.25 cnf(49,plain, % 117.06/117.25 (~P3(f4(a7,a8,a7),a7)), % 117.06/117.25 inference(scs_inference,[],[23,19,46,20,16,26,2,14,15,38])). % 117.06/117.25 cnf(51,plain, % 117.06/117.25 (~P3(x511,f5(a1,a1))), % 117.06/117.25 inference(scs_inference,[],[23,19,46,20,16,26,2,14,15,38,41])). % 117.06/117.25 cnf(54,plain, % 117.06/117.25 (E(f5(x541,x541),x541)), % 117.06/117.25 inference(rename_variables,[],[20])). % 117.06/117.25 cnf(56,plain, % 117.06/117.25 (E(f5(x561,x561),x561)), % 117.06/117.25 inference(rename_variables,[],[20])). % 117.06/117.25 cnf(57,plain, % 117.06/117.25 (~P3(x571,f5(f5(a1,a1),f5(a1,a1)))), % 117.06/117.25 inference(scs_inference,[],[23,19,46,20,54,56,16,22,26,2,14,15,38,41,3,11,34])). % 117.06/117.25 cnf(58,plain, % 117.06/117.25 (E(f5(x581,x581),x581)), % 117.06/117.25 inference(rename_variables,[],[20])). % 117.06/117.25 cnf(60,plain, % 117.06/117.25 (P3(f4(a7,a8,a7),a8)), % 117.06/117.25 inference(scs_inference,[],[23,19,46,20,54,56,16,22,26,2,14,15,38,41,3,11,34,36])). % 117.06/117.25 cnf(62,plain, % 117.06/117.25 (P2(a1,x621)), % 117.06/117.25 inference(scs_inference,[],[23,19,46,20,54,56,16,22,26,2,14,15,38,41,3,11,34,36,30])). % 117.06/117.25 cnf(66,plain, % 117.06/117.25 (P3(f4(a7,a8,a7),f5(x661,a8))), % 117.06/117.25 inference(scs_inference,[],[23,19,46,20,54,56,16,22,26,2,14,15,38,41,3,11,34,36,30,27,39])). % 117.06/117.25 cnf(68,plain, % 117.06/117.25 (P3(f4(a7,a8,a7),f5(a8,x681))), % 117.06/117.25 inference(scs_inference,[],[23,19,46,20,54,56,16,22,26,2,14,15,38,41,3,11,34,36,30,27,39,40])). % 117.06/117.25 cnf(70,plain, % 117.06/117.25 (~E(a8,a7)), % 117.06/117.25 inference(scs_inference,[],[23,19,46,20,54,56,16,22,26,2,14,15,38,41,3,11,34,36,30,27,39,40,5])). % 117.06/117.25 cnf(74,plain, % 117.06/117.25 (E(f5(x741,x741),x741)), % 117.06/117.25 inference(rename_variables,[],[20])). % 117.06/117.25 cnf(76,plain, % 117.06/117.25 (P3(f4(a7,a8,a7),f5(f5(a8,x761),f5(a8,x761)))), % 117.06/117.25 inference(scs_inference,[],[23,19,46,20,54,56,58,74,16,22,26,2,14,15,38,41,3,11,34,36,30,27,39,40,5,25,32,33])). % 117.06/117.25 cnf(84,plain, % 117.06/117.25 (P3(f4(a7,a8,a7),f5(f5(a8,x841),x842))), % 117.06/117.25 inference(scs_inference,[],[68,40])). % 117.06/117.25 cnf(86,plain, % 117.06/117.25 (P3(f4(a7,a8,a7),f5(x861,f5(a8,x862)))), % 117.06/117.25 inference(scs_inference,[],[68,40,39])). % 117.06/117.25 cnf(88,plain, % 117.06/117.25 (~P3(x881,a2)), % 117.06/117.25 inference(scs_inference,[],[68,17,40,39,26])). % 117.06/117.25 cnf(92,plain, % 117.06/117.25 (P2(f5(a1,a1),x921)), % 117.06/117.25 inference(scs_inference,[],[76,68,51,17,40,39,26,27,30])). % 117.06/117.25 cnf(93,plain, % 117.06/117.25 (~P3(x931,f5(a1,a1))), % 117.06/117.25 inference(rename_variables,[],[51])). % 117.06/117.25 cnf(95,plain, % 117.06/117.25 (E(x951,f5(x951,a1))), % 117.06/117.25 inference(scs_inference,[],[76,68,51,18,17,40,39,26,27,30,2])). % 117.06/117.25 cnf(96,plain, % 117.06/117.25 (~P3(f4(a7,a8,a7),f5(a7,a7))), % 117.06/117.25 inference(scs_inference,[],[76,68,49,51,18,17,40,39,26,27,30,2,41])). % 117.06/117.25 cnf(99,plain, % 117.06/117.25 (E(x991,f5(x991,x991))), % 117.06/117.25 inference(rename_variables,[],[44])). % 117.06/117.25 cnf(100,plain, % 117.06/117.25 (~E(a1,a7)), % 117.06/117.25 inference(scs_inference,[],[23,62,44,76,68,49,51,18,17,40,39,26,27,30,2,41,12,14])). % 117.06/117.25 cnf(102,plain, % 117.06/117.25 (~E(a7,f5(a8,a7))), % 117.06/117.25 inference(scs_inference,[],[23,62,47,44,76,68,49,51,21,18,17,40,39,26,27,30,2,41,12,14,3])). % 117.06/117.25 cnf(104,plain, % 117.06/117.25 (P1(f5(a1,a1))), % 117.06/117.25 inference(scs_inference,[],[23,62,47,44,99,76,68,49,51,21,18,16,17,40,39,26,27,30,2,41,12,14,3,11])). % 117.06/117.25 cnf(108,plain, % 117.06/117.25 (P3(f4(f5(a1,a1),f5(a1,a1),f5(a8,x1081)),f5(a8,x1081))), % 117.06/117.25 inference(scs_inference,[],[23,62,47,44,99,57,76,68,49,51,93,21,18,16,17,40,39,26,27,30,2,41,12,14,3,11,13,36])). % 117.06/117.25 cnf(111,plain, % 117.06/117.25 (~E(a8,f5(a1,a1))), % 117.06/117.25 inference(scs_inference,[],[23,62,47,44,99,57,76,68,49,51,93,21,18,16,17,40,39,26,27,30,2,41,12,14,3,11,13,36,4])). % 117.06/117.25 cnf(114,plain, % 117.06/117.25 (~P3(f4(a8,a7,a7),a7)), % 117.06/117.25 inference(scs_inference,[],[23,62,47,44,99,57,76,68,49,51,93,70,21,18,16,17,40,39,26,27,30,2,41,12,14,3,11,13,36,4,25,37])). % 117.06/117.25 cnf(116,plain, % 117.06/117.25 (P3(f4(a7,a8,a7),f5(f5(x1161,a8),x1162))), % 117.06/117.25 inference(scs_inference,[],[66,40])). % 117.06/117.25 cnf(118,plain, % 117.06/117.25 (P3(f4(a7,a8,a7),f5(x1181,f5(x1182,a8)))), % 117.06/117.25 inference(scs_inference,[],[66,40,39])). % 117.06/117.25 cnf(122,plain, % 117.06/117.25 (P2(a2,x1221)), % 117.06/117.25 inference(scs_inference,[],[84,66,88,40,39,27,30])). % 117.06/117.25 cnf(129,plain, % 117.06/117.25 (P3(f5(f4(a7,a8,a7),a1),a8)), % 117.06/117.25 inference(scs_inference,[],[100,60,84,95,96,66,88,16,40,39,27,30,25,41,12])). % 117.06/117.25 cnf(136,plain, % 117.06/117.25 (P3(f4(a1,a1,a8),a8)), % 117.06/117.25 inference(scs_inference,[],[23,92,47,100,18,60,84,95,96,66,42,88,111,16,40,39,27,30,25,41,12,14,3,13,36])). % 117.06/117.25 cnf(143,plain, % 117.06/117.25 (P3(f5(f4(a7,a8,a7),a1),f5(x1431,a8))), % 117.06/117.25 inference(scs_inference,[],[129,39])). % 117.06/117.25 cnf(147,plain, % 117.06/117.25 (P3(f5(f4(a7,a8,a7),a1),f5(a8,x1471))), % 117.06/117.25 inference(scs_inference,[],[116,129,39,27,40])). % 117.06/117.25 cnf(149,plain, % 117.06/117.25 (~P3(f4(a8,a7,a7),f5(a7,a7))), % 117.06/117.25 inference(scs_inference,[],[114,116,129,39,27,40,41])). % 117.06/117.25 cnf(151,plain, % 117.06/117.25 (~P1(a8)), % 117.06/117.25 inference(scs_inference,[],[114,116,129,111,104,39,27,40,41,25])). % 117.06/117.25 cnf(153,plain, % 117.06/117.25 (P3(f5(f4(a1,a1,a8),f4(a1,a1,a8)),a8)), % 117.06/117.25 inference(scs_inference,[],[44,114,116,129,136,111,104,39,27,40,41,25,12])). % 117.06/117.25 cnf(155,plain, % 117.06/117.25 (~E(a2,a7)), % 117.06/117.25 inference(scs_inference,[],[23,122,44,114,116,129,136,111,104,39,27,40,41,25,12,14])). % 117.06/117.25 cnf(159,plain, % 117.06/117.25 (~E(a8,f5(f5(a1,a1),f5(a1,a1)))), % 117.06/117.25 inference(scs_inference,[],[23,122,47,20,44,114,116,129,136,57,111,104,39,27,40,41,25,12,14,3,13])). % 117.06/117.25 cnf(161,plain, % 117.06/117.25 (P3(f4(a8,a7,a7),a8)), % 117.06/117.25 inference(scs_inference,[],[23,122,47,20,44,102,114,116,129,136,57,111,104,39,27,40,41,25,12,14,3,13,36])). % 117.06/117.25 cnf(166,plain, % 117.06/117.25 (P3(f4(a8,a7,a7),f5(a8,x1661))), % 117.06/117.25 inference(scs_inference,[],[161,40])). % 117.06/117.25 cnf(170,plain, % 117.06/117.25 (P3(f4(a8,a7,a7),f5(x1701,a8))), % 117.06/117.25 inference(scs_inference,[],[118,161,40,27,39])). % 117.06/117.25 cnf(177,plain, % 117.06/117.25 (~E(f5(x1771,f5(x1772,a8)),f5(a1,a1))), % 117.06/117.25 inference(scs_inference,[],[21,51,42,118,143,161,40,27,39,41,12,13])). % 117.06/117.25 cnf(178,plain, % 117.06/117.25 (~P3(x1781,f5(a1,a1))), % 117.06/117.25 inference(rename_variables,[],[51])). % 117.06/117.25 cnf(179,plain, % 117.06/117.25 (P3(f4(f5(a1,a1),f5(a1,a1),a8),a8)), % 117.06/117.25 inference(scs_inference,[],[21,51,178,42,118,143,161,159,40,27,39,41,12,13,36])). % 117.06/117.25 cnf(187,plain, % 117.06/117.25 (P3(f4(a8,a7,a7),f5(x1871,f5(a8,x1872)))), % 117.06/117.25 inference(scs_inference,[],[166,39])). % 117.06/117.25 cnf(191,plain, % 117.06/117.25 (P3(f4(a8,a7,a7),f5(f5(a8,x1911),x1912))), % 117.06/117.25 inference(scs_inference,[],[86,166,39,27,40])). % 117.06/117.25 cnf(193,plain, % 117.06/117.25 (~P3(x1931,f5(a2,a2))), % 117.06/117.25 inference(scs_inference,[],[88,86,166,39,27,40,41])). % 117.06/117.25 cnf(197,plain, % 117.06/117.25 (P3(f5(f4(a8,a7,a7),a1),f5(a8,x1971))), % 117.06/117.25 inference(scs_inference,[],[95,88,177,86,166,104,39,27,40,41,25,12])). % 117.06/117.25 cnf(199,plain, % 117.06/117.25 (~E(f5(x1991,f5(a8,x1992)),a2)), % 117.06/117.25 inference(scs_inference,[],[95,88,177,86,166,104,39,27,40,41,25,12,13])). % 117.06/117.25 cnf(211,plain, % 117.06/117.25 (P3(f4(a8,a7,a7),f5(f5(x2111,a8),x2112))), % 117.06/117.25 inference(scs_inference,[],[187,170,193,30,27,40])). % 117.06/117.25 cnf(213,plain, % 117.06/117.25 (P3(f4(a8,a7,a7),f5(x2131,f5(x2132,a8)))), % 117.06/117.26 inference(scs_inference,[],[187,170,193,30,27,40,39])). % 117.06/117.26 cnf(218,plain, % 117.06/117.26 (~E(f5(a2,a2),a7)), % 117.06/117.26 inference(scs_inference,[],[23,42,51,187,170,193,30,27,40,39,41,14])). % 117.06/117.26 cnf(221,plain, % 117.06/117.26 (P3(f5(f4(a8,a7,a7),f4(a8,a7,a7)),f5(x2211,a8))), % 117.06/117.26 inference(scs_inference,[],[23,44,42,51,187,170,193,199,17,30,27,40,39,41,14,25,12])). % 117.06/117.26 cnf(239,plain, % 117.06/117.26 (P3(f5(f4(a1,a1,a8),a1),a8)), % 117.06/117.26 inference(scs_inference,[],[95,51,88,191,179,136,40,27,39,41,12])). % 117.06/117.26 cnf(241,plain, % 117.06/117.26 (~E(f5(f5(a8,x2411),x2412),f5(a1,a1))), % 117.06/117.26 inference(scs_inference,[],[95,51,88,191,179,136,40,27,39,41,12,13])). % 117.06/117.26 cnf(255,plain, % 117.06/117.26 (P3(f5(f4(a1,a1,a8),f4(a1,a1,a8)),f5(a8,x2551))), % 117.06/117.26 inference(scs_inference,[],[211,153,27,40])). % 117.06/117.26 cnf(257,plain, % 117.06/117.26 (P3(f5(f4(a1,a1,a8),f4(a1,a1,a8)),f5(x2571,a8))), % 117.06/117.26 inference(scs_inference,[],[211,153,27,40,39])). % 117.06/117.26 cnf(261,plain, % 117.06/117.26 (~P3(x2611,f5(a1,a2))), % 117.06/117.26 inference(scs_inference,[],[42,88,241,211,153,104,27,40,39,25,41])). % 117.06/117.26 cnf(264,plain, % 117.06/117.26 (P3(f5(a1,f4(a7,a8,a7)),f5(a8,x2641))), % 117.06/117.26 inference(scs_inference,[],[21,42,88,241,211,147,153,104,27,40,39,25,41,12])). % 117.06/117.26 cnf(279,plain, % 117.06/117.26 (P3(f5(f4(a1,a1,a8),a1),f5(x2791,a8))), % 117.06/117.26 inference(scs_inference,[],[261,239,30,39])). % 117.06/117.26 cnf(289,plain, % 117.06/117.26 (P3(f4(a1,a1,a8),f5(a8,x2891))), % 117.06/117.26 inference(scs_inference,[],[23,20,51,193,213,255,261,239,30,39,40,27,14,41,12])). % 117.06/117.26 cnf(293,plain, % 117.06/117.26 (P3(f4(a1,a1,f5(a8,x2931)),f5(a8,x2931))), % 117.06/117.26 inference(scs_inference,[],[23,20,51,42,193,213,108,255,261,239,30,39,40,27,14,41,12,13,36])). % 117.06/117.26 cnf(297,plain, % 117.06/117.26 (P3(f4(a1,a1,a8),f5(f5(a8,x2971),x2972))), % 117.06/117.26 inference(scs_inference,[],[289,40])). % 117.06/117.26 cnf(306,plain, % 117.06/117.26 (P3(f4(a1,a1,a8),f5(x3061,a8))), % 117.06/117.26 inference(scs_inference,[],[20,42,193,221,289,257,40,39,27,41,12])). % 117.06/117.26 cnf(309,plain, % 117.06/117.26 (~P3(x3091,a1)), % 117.06/117.26 inference(rename_variables,[],[42])). % 117.06/117.26 cnf(310,plain, % 117.06/117.26 (P3(f5(f4(a8,a7,a7),f4(a8,a7,a7)),a8)), % 117.06/117.26 inference(scs_inference,[],[20,21,42,309,193,221,289,257,213,40,39,27,41,12,13,34])). % 117.06/117.26 cnf(321,plain, % 117.06/117.26 (~P3(f4(a8,a7,a7),f5(f5(a7,a7),f5(a7,a7)))), % 117.06/117.26 inference(scs_inference,[],[297,149,306,39,27,40,41])). % 117.06/117.26 cnf(323,plain, % 117.06/117.26 (P3(f5(f4(a7,a8,a7),f4(a7,a8,a7)),a8)), % 117.06/117.26 inference(scs_inference,[],[44,297,149,306,60,39,27,40,41,12])). % 117.06/117.26 cnf(363,plain, % 117.06/117.26 (P3(f5(a1,f4(a7,a8,a7)),a8)), % 117.06/117.26 inference(scs_inference,[],[21,51,264,27,34])). % 117.06/117.26 cnf(377,plain, % 117.06/117.26 (P3(f4(a7,a7,f5(a2,a2)),a7)), % 117.06/117.26 inference(scs_inference,[],[218,20,21,42,193,293,27,3,34,36])). % 117.06/117.26 cnf(397,plain, % 117.06/117.26 (~P3(x3971,f5(a1,a1))), % 117.06/117.26 inference(rename_variables,[],[51])). % 117.06/117.26 cnf(398,plain, % 117.06/117.26 (P3(f5(f4(a8,a7,a7),a1),a8)), % 117.06/117.26 inference(scs_inference,[],[21,51,397,197,149,377,39,40,27,12,13,34])). % 117.06/117.26 cnf(403,plain, % 117.06/117.26 (P3(f4(a1,a1,a7),a7)), % 117.06/117.26 inference(scs_inference,[],[21,51,397,42,197,149,377,39,40,27,12,13,34,36])). % 117.06/117.26 cnf(408,plain, % 117.06/117.26 (P3(f4(a1,a1,a7),f5(a7,x4081))), % 117.06/117.26 inference(scs_inference,[],[403,40])). % 117.06/117.26 cnf(417,plain, % 117.06/117.26 (~E(f4(a1,a1,a7),f4(a7,a8,a7))), % 117.06/117.26 inference(scs_inference,[],[88,261,49,279,398,403,40,39,27,41,12])). % 117.06/117.26 cnf(418,plain, % 117.06/117.26 (~E(f5(x4181,a8),a2)), % 117.06/117.26 inference(scs_inference,[],[88,261,49,279,398,403,40,39,27,41,12,13])). % 117.06/117.26 cnf(422,plain, % 117.06/117.26 (P3(f4(a1,a1,a7),f5(x4221,f5(a7,x4222)))), % 117.06/117.26 inference(scs_inference,[],[408,39])). % 117.06/117.26 cnf(424,plain, % 117.06/117.26 (P3(f4(a1,a1,a7),f5(f5(a7,x4241),x4242))), % 117.06/117.26 inference(scs_inference,[],[408,39,40])). % 117.06/117.26 cnf(436,plain, % 117.06/117.26 (P3(f4(a1,a1,a7),f5(x4361,a7))), % 117.06/117.26 inference(scs_inference,[],[403,39])). % 117.06/117.26 cnf(443,plain, % 117.06/117.26 (~E(a8,a2)), % 117.06/117.26 inference(scs_inference,[],[88,193,323,310,403,39,27,41,13])). % 117.06/117.26 cnf(449,plain, % 117.06/117.26 (P3(f4(a1,a1,a7),f5(x4491,f5(x4492,a7)))), % 117.06/117.26 inference(scs_inference,[],[436,39])). % 117.06/117.26 cnf(451,plain, % 117.06/117.26 (~P3(a8,f4(a1,a1,a8))), % 117.06/117.26 inference(scs_inference,[],[136,436,39,27])). % 117.06/117.26 cnf(457,plain, % 117.06/117.26 (P3(f4(a1,a2,a8),a8)), % 117.06/117.26 inference(scs_inference,[],[261,88,42,136,436,39,27,41,13,36])). % 117.06/117.26 cnf(461,plain, % 117.06/117.26 (P3(f4(a1,a2,a8),f5(a8,x4611))), % 117.06/117.26 inference(scs_inference,[],[261,88,42,136,436,39,27,41,13,36,40])). % 117.06/117.26 cnf(463,plain, % 117.06/117.26 (P3(f5(f4(a1,a2,a8),f4(a1,a2,a8)),a8)), % 117.06/117.26 inference(scs_inference,[],[44,261,88,42,136,436,39,27,41,13,36,40,12])). % 117.06/117.26 cnf(474,plain, % 117.06/117.26 (P3(f5(f4(a1,a2,a8),f4(a1,a2,a8)),f5(a8,x4741))), % 117.06/117.26 inference(scs_inference,[],[44,261,88,161,461,40,39,27,41,12])). % 117.06/117.26 cnf(476,plain, % 117.06/117.26 (~E(f5(x4761,a8),f5(a1,a2))), % 117.06/117.26 inference(scs_inference,[],[44,261,88,161,306,461,40,39,27,41,12,13])). % 117.06/117.26 cnf(489,plain, % 117.06/117.26 (~E(f5(a8,x4891),f5(a1,a2))), % 117.06/117.26 inference(scs_inference,[],[261,51,289,463,39,27,41,13])). % 117.06/117.26 cnf(495,plain, % 117.06/117.26 (P3(f4(a1,a2,a8),f5(x4951,a8))), % 117.06/117.26 inference(scs_inference,[],[457,39])). % 117.06/117.26 cnf(504,plain, % 117.06/117.26 (~E(f5(a7,x5041),a2)), % 117.06/117.26 inference(scs_inference,[],[261,193,66,422,457,39,27,41,13,5])). % 117.06/117.26 cnf(513,plain, % 117.06/117.26 (~P1(f5(a7,x5131))), % 117.06/117.26 inference(scs_inference,[],[166,495,504,17,39,27,25])). % 117.06/117.26 cnf(515,plain, % 117.06/117.26 (~P3(x5151,f5(a2,a1))), % 117.06/117.26 inference(scs_inference,[],[88,42,166,495,504,17,39,27,25,41])). % 117.06/117.26 cnf(518,plain, % 117.06/117.26 (~E(f5(f5(a7,x5181),x5182),a2)), % 117.06/117.26 inference(scs_inference,[],[88,42,166,424,495,504,17,39,27,25,41,13])). % 117.06/117.26 cnf(526,plain, % 117.06/117.26 (~P1(f5(f5(a7,x5261),x5262))), % 117.06/117.26 inference(scs_inference,[],[23,170,515,518,17,30,27,14,25])). % 117.06/117.26 cnf(549,plain, % 117.06/117.26 (~P3(f3(f5(a7,a7),f5(a7,a8)),f5(a7,a8))), % 117.06/117.26 inference(scs_inference,[],[23,20,35,14])). % 117.06/117.26 cnf(577,plain, % 117.06/117.26 (P3(f4(a1,a2,a7),a7)), % 117.06/117.26 inference(scs_inference,[],[549,306,261,88,42,377,27,12,13,36])). % 117.06/117.26 cnf(581,plain, % 117.06/117.26 (P3(f4(a1,a2,a7),f5(a7,x5811))), % 117.06/117.26 inference(scs_inference,[],[549,306,261,88,42,377,27,12,13,36,40])). % 117.06/117.26 cnf(583,plain, % 117.06/117.26 (P3(f4(a1,a2,a7),f5(x5831,a7))), % 117.06/117.26 inference(scs_inference,[],[549,306,261,88,42,377,27,12,13,36,40,39])). % 117.06/117.26 cnf(597,plain, % 117.06/117.26 (~E(f5(x5971,f5(x5972,a7)),f5(a1,a1))), % 117.06/117.26 inference(scs_inference,[],[549,51,408,403,449,583,40,39,27,41,12,13])). % 117.06/117.26 cnf(602,plain, % 117.06/117.26 (P3(f4(a1,a2,a7),f5(f5(a7,x6021),x6022))), % 117.06/117.26 inference(scs_inference,[],[581,40])). % 117.06/117.26 cnf(616,plain, % 117.06/117.26 (P3(f4(a2,a2,a8),a8)), % 117.06/117.26 inference(scs_inference,[],[549,193,88,60,457,495,597,581,104,40,39,27,25,41,12,13,36])). % 117.06/117.26 cnf(619,plain, % 117.06/117.26 (P3(f4(a2,a2,a8),f5(a8,x6191))), % 117.06/117.26 inference(scs_inference,[],[616,40])). % 117.06/117.26 cnf(623,plain, % 117.06/117.26 (~P3(f5(x6231,a7),f4(a1,a1,a7))), % 117.06/117.26 inference(scs_inference,[],[436,616,40,39,27])). % 117.06/117.26 cnf(627,plain, % 117.06/117.26 (~E(f4(a1,a2,a7),f4(a8,a7,a7))), % 117.06/117.26 inference(scs_inference,[],[436,321,602,616,40,39,27,41,12])). % 117.06/117.26 cnf(642,plain, % 117.06/117.26 (~E(f4(a1,a2,a7),f4(a7,a8,a7))), % 117.06/117.26 inference(scs_inference,[],[239,49,577,619,40,39,27,12])). % 117.06/117.26 cnf(680,plain, % 117.06/117.26 (~P3(a8,f5(a1,f4(a7,a8,a7)))), % 117.06/117.26 inference(scs_inference,[],[363,27])). % 117.06/117.26 cnf(691,plain, % 117.06/117.26 (P3(f4(a2,a2,a7),f5(x6911,a7))), % 117.06/117.26 inference(scs_inference,[],[549,193,88,403,363,581,27,12,13,36,40,39])). % 117.06/117.26 cnf(705,plain, % 117.06/117.26 (P3(f4(a1,a2,f5(x7051,a7)),f5(x7051,a7))), % 117.06/117.26 inference(scs_inference,[],[261,42,88,96,436,179,691,40,39,27,12,13,36])). % 117.06/117.26 cnf(740,plain, % 117.06/117.26 (P3(f4(a2,a2,f5(x7401,a7)),f5(x7401,a7))), % 117.06/117.26 inference(scs_inference,[],[193,149,88,436,398,705,27,12,13,36])). % 117.06/117.26 cnf(751,plain, % 117.06/117.26 (~E(f5(a8,x7511),a7)), % 117.06/117.26 inference(scs_inference,[],[114,96,166,495,740,27,41,12,13])). % 117.06/117.26 cnf(925,plain, % 117.06/117.26 (~E(f5(a8,x9251),f5(a7,a7))), % 117.06/117.26 inference(scs_inference,[],[68,96,108,27,13])). % 117.06/117.26 cnf(1021,plain, % 117.06/117.26 (P1(f5(a2,a2))), % 117.06/117.26 inference(scs_inference,[],[17,44,11])). % 117.06/117.26 cnf(1024,plain, % 117.06/117.26 (P1(f5(a2,a1))), % 117.06/117.26 inference(scs_inference,[],[17,95,11])). % 117.06/117.26 cnf(1175,plain, % 117.06/117.26 (~P3(f4(a7,a8,a7),f5(a7,a1))), % 117.06/117.26 inference(scs_inference,[],[49,42,41])). % 117.06/117.26 cnf(1181,plain, % 117.06/117.26 (~P3(f4(a7,a8,a7),f5(a7,a2))), % 117.06/117.26 inference(scs_inference,[],[49,88,41])). % 117.06/117.26 cnf(1292,plain, % 117.06/117.26 (~E(a8,f5(a7,a1))), % 117.06/117.26 inference(scs_inference,[],[70,18,3])). % 117.06/117.26 cnf(1399,plain, % 117.06/117.26 (P3(f4(a7,a7,a1),a7)), % 117.06/117.26 inference(scs_inference,[],[100,20,42,3,36])). % 117.06/117.26 cnf(1404,plain, % 117.06/117.26 (P3(f4(a7,a7,a1),f5(x14041,a7))), % 117.06/117.26 inference(scs_inference,[],[100,20,42,3,36,40,39])). % 117.06/117.26 cnf(1410,plain, % 117.06/117.26 (~E(f4(a7,a7,a1),f4(a7,a8,a7))), % 117.06/117.26 inference(scs_inference,[],[100,20,49,42,3,36,40,39,27,41,12])). % 117.06/117.26 cnf(1424,plain, % 117.06/117.26 (~E(f4(a7,a7,a1),f4(a8,a7,a7))), % 117.06/117.26 inference(scs_inference,[],[100,18,149,1404,40,39,27,3,41,12])). % 117.06/117.26 cnf(1426,plain, % 117.06/117.26 (P3(f4(a7,a1,a1),a7)), % 117.06/117.26 inference(scs_inference,[],[100,18,149,42,1404,40,39,27,3,41,12,36])). % 117.06/117.26 cnf(1450,plain, % 117.06/117.26 (P3(f4(a7,a1,a1),f5(x14501,a7))), % 117.06/117.26 inference(scs_inference,[],[1426,40,39])). % 117.06/117.26 cnf(1476,plain, % 117.06/117.26 (~P3(a7,f4(a7,a1,a1))), % 117.06/117.26 inference(scs_inference,[],[1426,1450,40,39,27])). % 117.06/117.26 cnf(1480,plain, % 117.06/117.26 (~E(f4(a7,a1,a1),f4(a8,a7,a7))), % 117.06/117.26 inference(scs_inference,[],[149,1426,1450,40,39,27,41,12])). % 117.06/117.26 cnf(1510,plain, % 117.06/117.26 (~E(a7,f5(f5(a8,a7),f5(a8,a7)))), % 117.06/117.26 inference(scs_inference,[],[102,20,3])). % 117.06/117.26 cnf(1514,plain, % 117.06/117.26 (~P3(f4(f5(a8,a7),f5(a8,a7),a7),f5(a7,a7))+~P3(f4(f5(a8,a7),f5(a8,a7),a7),f5(a8,a7))), % 117.06/117.26 inference(scs_inference,[],[102,20,3,37,41])). % 117.06/117.26 cnf(1537,plain, % 117.06/117.26 (P3(f4(f5(a8,a7),f5(a8,a7),a7),f5(x15371,a7))+P3(f4(f5(a8,a7),f5(a8,a7),a7),f5(a8,a7))), % 117.06/117.26 inference(scs_inference,[],[1510,36,40,39])). % 117.06/117.26 cnf(1541,plain, % 117.06/117.26 (P3(f4(f5(a8,a7),f5(a8,a7),a7),f5(a8,a7))), % 117.06/117.26 inference(factoring_inference,[],[1537])). % 117.06/117.26 cnf(1543,plain, % 117.06/117.26 (~P3(f4(f5(a8,a7),f5(a8,a7),a7),f5(a7,a7))), % 117.06/117.26 inference(scs_inference,[],[1541,1514])). % 117.06/117.26 cnf(1562,plain, % 117.06/117.26 (P1(f5(f5(a1,a1),f5(a1,a1)))), % 117.06/117.26 inference(scs_inference,[],[104,44,11])). % 117.06/117.26 cnf(1605,plain, % 117.06/117.26 (~P3(f4(a8,a7,a7),f5(a7,a1))), % 117.06/117.26 inference(scs_inference,[],[114,42,41])). % 117.06/117.26 cnf(1803,plain, % 117.06/117.26 (P3(f4(a7,a7,a2),a7)), % 117.06/117.26 inference(scs_inference,[],[155,20,88,3,36])). % 117.06/117.26 cnf(1806,plain, % 117.06/117.26 (P3(f4(a7,a7,a2),f5(a7,x18061))), % 117.06/117.26 inference(scs_inference,[],[155,20,88,3,36,40])). % 117.06/117.26 cnf(1808,plain, % 117.06/117.26 (P3(f4(a7,a7,a2),f5(x18081,a7))), % 117.06/117.26 inference(scs_inference,[],[155,20,88,3,36,40,39])). % 117.06/117.26 cnf(1830,plain, % 117.06/117.26 (P3(f4(a7,a1,a2),a7)), % 117.06/117.26 inference(scs_inference,[],[155,549,18,88,42,1808,1806,40,39,27,3,41,12,36])). % 117.06/117.26 cnf(1840,plain, % 117.06/117.26 (P3(f4(a7,a1,a2),f5(a7,x18401))), % 117.06/117.26 inference(scs_inference,[],[1830,40])). % 117.06/117.26 cnf(1842,plain, % 117.06/117.26 (P3(f4(a7,a1,a2),f5(x18421,a7))), % 117.06/117.26 inference(scs_inference,[],[1830,40,39])). % 117.06/117.26 cnf(1858,plain, % 117.06/117.26 (~E(f4(a7,a1,a2),f4(a7,a8,a7))), % 117.06/117.26 inference(scs_inference,[],[49,1806,1830,40,39,27,41,12])). % 117.06/117.26 cnf(1865,plain, % 117.06/117.27 (~P3(a7,f4(a7,a1,a2))), % 117.06/117.27 inference(scs_inference,[],[1830,1840,40,39,27])). % 117.06/117.27 cnf(1884,plain, % 117.06/117.27 (~E(f4(a7,a1,a2),f4(a8,a7,a7))), % 117.06/117.27 inference(scs_inference,[],[1842,321,40,39,27,41,12])). % 117.06/117.27 cnf(1975,plain, % 117.06/117.27 (~P3(x19751,f5(f5(a2,a2),f5(a2,a2)))), % 117.06/117.27 inference(scs_inference,[],[193,41])). % 117.06/117.27 cnf(1995,plain, % 117.06/117.27 (~P3(x19951,f5(f5(a2,a2),f5(a2,a1)))), % 117.06/117.27 inference(scs_inference,[],[193,515,41])). % 117.06/117.27 cnf(2162,plain, % 117.06/117.27 (~P1(f5(x21621,a6))), % 117.06/117.27 inference(scs_inference,[],[22,28])). % 117.06/117.27 cnf(2164,plain, % 117.06/117.27 (~P1(f5(a6,x21641))), % 117.06/117.27 inference(scs_inference,[],[22,28,29])). % 117.06/117.27 cnf(2168,plain, % 117.06/117.27 (~E(a2,f5(x21681,a8))), % 117.06/117.27 inference(scs_inference,[],[418,1021,22,28,29,24,2])). % 117.06/117.27 cnf(2169,plain, % 117.06/117.27 (~E(f5(a2,a1),f5(x21691,a7))), % 117.06/117.27 inference(scs_inference,[],[1803,418,1021,22,515,28,29,24,2,32])). % 117.06/117.27 cnf(2170,plain, % 117.06/117.27 (~P3(x21701,f5(a2,a1))), % 117.06/117.27 inference(rename_variables,[],[515])). % 117.06/117.27 cnf(2172,plain, % 117.06/117.27 (~E(f5(a2,a1),f5(a7,x21721))), % 117.06/117.27 inference(scs_inference,[],[1803,418,1021,22,515,2170,28,29,24,2,32,33])). % 117.06/117.27 cnf(2175,plain, % 117.06/117.27 (~P2(f5(a7,a1),f5(a7,a8))), % 117.06/117.27 inference(scs_inference,[],[1803,418,1021,22,23,515,2170,18,28,29,24,2,32,33,14])). % 117.06/117.27 cnf(2177,plain, % 117.06/117.27 (~E(f5(a8,a1),f5(a7,a1))), % 117.06/117.27 inference(scs_inference,[],[1803,418,1021,22,1292,95,23,515,2170,18,28,29,24,2,32,33,14,3])). % 117.06/117.27 cnf(2179,plain, % 117.06/117.27 (~P2(a7,f5(a8,a7))), % 117.06/117.27 inference(scs_inference,[],[1803,418,1021,22,1292,95,23,515,2170,18,21,28,29,24,2,32,33,14,3,15])). % 117.06/117.27 cnf(2180,plain, % 117.06/117.27 (E(f5(x21801,x21802),f5(x21802,x21801))), % 117.06/117.27 inference(rename_variables,[],[21])). % 117.06/117.27 cnf(2182,plain, % 117.06/117.27 (~P3(f4(a8,a7,a7),f5(a1,a7))), % 117.06/117.27 inference(scs_inference,[],[16,151,1803,418,1021,22,1605,1292,95,23,515,2170,18,21,2180,28,29,24,2,32,33,14,3,15,11,13])). % 117.06/117.27 cnf(2184,plain, % 117.06/117.27 (E(f5(a2,a1),a1)), % 117.06/117.27 inference(scs_inference,[],[1024,24])). % 117.06/117.27 cnf(2187,plain, % 117.06/117.27 (~E(f5(a2,a1),f5(x21871,a8))), % 117.06/117.27 inference(scs_inference,[],[2177,1024,457,515,24,2,32])). % 117.06/117.27 cnf(2188,plain, % 117.06/117.27 (~P3(x21881,f5(a2,a1))), % 117.06/117.27 inference(rename_variables,[],[515])). % 117.06/117.27 cnf(2190,plain, % 117.06/117.27 (~E(f5(a2,a1),f5(a8,x21901))), % 117.06/117.27 inference(scs_inference,[],[2177,1024,457,515,2188,24,2,32,33])). % 117.06/117.27 cnf(2193,plain, % 117.06/117.27 (~P2(f5(a1,a7),f5(a7,a8))), % 117.06/117.27 inference(scs_inference,[],[2175,2177,1024,457,515,2188,21,24,2,32,33,14])). % 117.06/117.27 cnf(2197,plain, % 117.06/117.27 (E(a2,a1)), % 117.06/117.27 inference(scs_inference,[],[17,24])). % 117.06/117.27 cnf(2199,plain, % 117.06/117.27 (E(f5(a2,x21991),f5(a1,x21991))), % 117.06/117.27 inference(scs_inference,[],[17,24,4])). % 117.06/117.27 cnf(2200,plain, % 117.06/117.27 (E(f5(x22001,a2),f5(x22001,a1))), % 117.06/117.27 inference(scs_inference,[],[17,24,4,5])). % 117.06/117.27 cnf(2203,plain, % 117.06/117.27 (~P3(x22031,f5(a2,a2))), % 117.06/117.27 inference(rename_variables,[],[193])). % 117.06/117.27 cnf(2208,plain, % 117.06/117.27 (~P2(f5(a7,a1),f5(a8,a7))), % 117.06/117.27 inference(scs_inference,[],[2169,2179,1399,17,18,193,2203,24,4,5,2,32,33,14])). % 117.06/117.27 cnf(2211,plain, % 117.06/117.27 (E(f3(a2,x22111),f3(a1,x22111))), % 117.06/117.27 inference(scs_inference,[],[2169,2179,2184,1399,17,18,193,2203,24,4,5,2,32,33,14,3,9])). % 117.06/117.27 cnf(2212,plain, % 117.06/117.27 (E(f3(x22121,a2),f3(x22121,a1))), % 117.06/117.27 inference(scs_inference,[],[2169,2179,2184,1399,17,18,193,2203,24,4,5,2,32,33,14,3,9,10])). % 117.06/117.27 cnf(2213,plain, % 117.06/117.27 (E(f4(a2,x22131,x22132),f4(a1,x22131,x22132))), % 117.06/117.27 inference(scs_inference,[],[2169,2179,2184,1399,17,18,193,2203,24,4,5,2,32,33,14,3,9,10,6])). % 117.06/117.27 cnf(2214,plain, % 117.06/117.27 (E(f4(x22141,a2,x22142),f4(x22141,a1,x22142))), % 117.06/117.27 inference(scs_inference,[],[2169,2179,2184,1399,17,18,193,2203,24,4,5,2,32,33,14,3,9,10,6,7])). % 117.06/117.27 cnf(2215,plain, % 117.06/117.27 (E(f4(x22151,x22152,a2),f4(x22151,x22152,a1))), % 117.06/117.27 inference(scs_inference,[],[2169,2179,2184,1399,17,18,193,2203,24,4,5,2,32,33,14,3,9,10,6,7,8])). % 117.06/117.27 cnf(2218,plain, % 117.06/117.27 (~E(f5(a7,a1),f5(x22181,a8))), % 117.06/117.27 inference(scs_inference,[],[2172,1175,60,2,32])). % 117.06/117.27 cnf(2220,plain, % 117.06/117.27 (~E(f5(a7,a1),f5(a8,x22201))), % 117.06/117.27 inference(scs_inference,[],[2172,1175,60,2,32,33])). % 117.06/117.27 cnf(2222,plain, % 117.06/117.27 (P2(f4(a1,x22221,x22222),f4(a2,x22221,x22222))), % 117.06/117.27 inference(scs_inference,[],[2172,2213,1175,19,60,2,32,33,14])). % 117.06/117.27 cnf(2224,plain, % 117.06/117.27 (~E(a1,f5(x22241,a8))), % 117.06/117.27 inference(scs_inference,[],[2197,2172,2213,2168,1175,19,60,2,32,33,14,3])). % 117.06/117.27 cnf(2225,plain, % 117.06/117.27 (~P3(f4(a8,a7,a7),f5(a2,a7))), % 117.06/117.27 inference(scs_inference,[],[2197,2182,2172,2213,2199,2168,1175,19,60,2,32,33,14,3,13])). % 117.06/117.27 cnf(2229,plain, % 117.06/117.27 (~P3(x22291,f5(a1,a2))), % 117.06/117.27 inference(rename_variables,[],[261])). % 117.06/117.27 cnf(2236,plain, % 117.06/117.27 (~E(a1,f5(a8,x22361))), % 117.06/117.27 inference(scs_inference,[],[2208,2187,2190,2200,2184,1803,261,2229,2,32,33,14,3])). % 117.06/117.27 cnf(2239,plain, % 117.06/117.27 (P2(f4(a1,x22391,a2),f4(a2,x22391,a1))), % 117.06/117.27 inference(scs_inference,[],[2208,2187,2190,2215,2222,2200,1865,2184,2214,1803,261,2229,2,32,33,14,3,13,15])). % 117.06/117.27 cnf(2243,plain, % 117.06/117.27 (~P3(x22431,f4(a1,x22432,a2))+P3(x22431,f4(a2,x22432,a1))), % 117.06/117.27 inference(scs_inference,[],[16,2208,2187,2190,2215,2222,513,2200,1865,2184,2214,1803,261,2229,2,32,33,14,3,13,15,11,31])). % 117.06/117.27 cnf(2249,plain, % 117.06/117.27 (~E(f5(a7,a2),f5(x22491,a8))), % 117.06/117.27 inference(scs_inference,[],[2220,1181,60,2,32])). % 117.06/117.27 cnf(2251,plain, % 117.06/117.27 (~E(f5(a7,a2),f5(a8,x22511))), % 117.06/117.27 inference(scs_inference,[],[2220,1181,60,2,32,33])). % 117.06/117.27 cnf(2253,plain, % 117.06/117.27 (P2(f3(a1,x22531),f3(a2,x22531))), % 117.06/117.27 inference(scs_inference,[],[2220,2211,1181,19,60,2,32,33,14])). % 117.06/117.27 cnf(2255,plain, % 117.06/117.27 (E(f3(a2,a2),f3(a1,a1))), % 117.06/117.27 inference(scs_inference,[],[2220,2211,2212,1181,19,60,2,32,33,14,3])). % 117.06/117.27 cnf(2265,plain, % 117.06/117.27 (~P3(x22651,a2)), % 117.06/117.27 inference(rename_variables,[],[88])). % 117.06/117.27 cnf(2270,plain, % 117.06/117.27 (~P2(f5(a2,a7),f5(a7,a8))), % 117.06/117.27 inference(scs_inference,[],[2193,2249,2199,1399,88,2265,2,32,33,14])). % 117.06/117.27 cnf(2277,plain, % 117.06/117.27 (~E(f5(a8,x22771),f5(a7,a2))), % 117.06/117.27 inference(scs_inference,[],[2251,2])). % 117.06/117.27 cnf(2278,plain, % 117.06/117.27 (~E(f5(a2,a7),f5(x22781,a8))), % 117.06/117.27 inference(scs_inference,[],[2251,2225,161,2,32])). % 117.06/117.27 cnf(2280,plain, % 117.06/117.27 (~E(f5(a2,a7),f5(a8,x22801))), % 117.06/117.27 inference(scs_inference,[],[2251,2225,161,2,32,33])). % 117.06/117.27 cnf(2282,plain, % 117.06/117.27 (P2(f3(a1,a1),f3(a2,a2))), % 117.06/117.27 inference(scs_inference,[],[2251,2255,2225,19,161,2,32,33,14])). % 117.06/117.27 cnf(2298,plain, % 117.06/117.27 (~E(f5(a1,a7),f5(x22981,a8))), % 117.06/117.27 inference(scs_inference,[],[2278,2175,2199,577,2200,51,2,33,14,3])). % 117.06/117.27 cnf(2300,plain, % 117.06/117.27 (P2(f4(a1,x23001,a2),f4(a1,x23001,a1))), % 117.06/117.27 inference(scs_inference,[],[2278,2239,2175,2213,2199,577,2200,51,2,33,14,3,15])). % 117.06/117.27 cnf(2302,plain, % 117.06/117.27 (~E(a1,f5(x23021,a6))), % 117.06/117.27 inference(scs_inference,[],[16,2278,2162,2239,2175,2213,2199,577,2200,51,2,33,14,3,15,11])). % 117.06/117.27 cnf(2310,plain, % 117.06/117.27 (~E(f5(a1,a7),f5(a8,x23101))), % 117.06/117.27 inference(scs_inference,[],[2280,2182,161,2,33])). % 117.06/117.27 cnf(2312,plain, % 117.06/117.27 (P2(f4(a1,a1,a2),f4(a1,a2,a1))), % 117.06/117.27 inference(scs_inference,[],[2280,2300,2182,2214,161,2,33,14])). % 117.06/117.27 cnf(2317,plain, % 117.06/117.27 (~E(a1,f5(a6,x23171))), % 117.06/117.27 inference(scs_inference,[],[16,2218,2280,2164,2300,2182,2214,18,161,2,33,14,3,11])). % 117.06/117.27 cnf(2318,plain, % 117.06/117.27 (~P3(f5(x23181,a7),f4(a2,a1,a7))), % 117.06/117.27 inference(scs_inference,[],[16,2218,2280,2164,2300,623,2182,2213,2214,18,161,2,33,14,3,11,13])). % 117.06/117.27 cnf(2323,plain, % 117.06/117.27 (E(f5(x23231,x23232),f5(x23232,x23231))), % 117.06/117.27 inference(rename_variables,[],[21])). % 117.06/117.27 cnf(2328,plain, % 117.06/117.27 (~E(a1,a6)), % 117.06/117.27 inference(scs_inference,[],[16,2270,2318,2298,2224,22,95,21,2323,2,12,15,3,11])). % 117.06/117.27 cnf(2329,plain, % 117.06/117.27 (~P3(x23291,f3(x23292,a2))+P3(x23291,f3(x23292,a1))), % 117.06/117.27 inference(scs_inference,[],[16,2270,2318,2298,2224,2212,22,95,21,2323,2,12,15,3,11,13])). % 117.06/117.27 cnf(2330,plain, % 117.06/117.27 (P2(f4(a1,a1,a1),f4(a1,a2,a1))), % 117.06/117.27 inference(scs_inference,[],[16,2270,2318,2298,2312,2224,2212,2215,22,95,21,2323,2,12,15,3,11,13,14])). % 117.06/117.27 cnf(2334,plain, % 117.06/117.27 (~P3(f3(x23341,a1),f3(x23341,a2))), % 117.06/117.27 inference(scs_inference,[],[16,2270,2318,2298,2312,2224,2212,2215,22,95,21,2323,2,12,15,3,11,13,14,27])). % 117.06/117.27 cnf(2337,plain, % 117.06/117.27 (~P3(f3(a2,a1),f3(a1,a2))), % 117.06/117.27 inference(scs_inference,[],[2328,2253,2334,2,31])). % 117.06/117.27 cnf(2338,plain, % 117.06/117.27 (~P3(f3(x23381,a1),f3(x23381,a2))), % 117.06/117.27 inference(rename_variables,[],[2334])). % 117.06/117.27 cnf(2339,plain, % 117.06/117.27 (P2(f3(a1,x23391),f3(a2,x23391))), % 117.06/117.27 inference(rename_variables,[],[2253])). % 117.06/117.27 cnf(2343,plain, % 117.06/117.27 (P2(f3(a1,a2),f3(a1,a1))), % 117.06/117.27 inference(scs_inference,[],[2328,2253,2339,2334,2255,2212,2,31,12,15])). % 117.06/117.27 cnf(2345,plain, % 117.06/117.27 (~E(f5(a1,a1),a6)), % 117.06/117.27 inference(scs_inference,[],[2328,2253,2339,2334,2255,2212,95,2,31,12,15,3])). % 117.06/117.27 cnf(2347,plain, % 117.06/117.27 (~P3(f3(a1,a1),f3(a2,a2))), % 117.06/117.27 inference(scs_inference,[],[2328,2253,2339,2334,2338,2211,2255,2212,95,2,31,12,15,3,13])). % 117.06/117.27 cnf(2352,plain, % 117.06/117.27 (~P3(f3(a1,a1),f3(a1,a1))), % 117.06/117.27 inference(scs_inference,[],[2347,2310,2282,2,31])). % 117.06/117.27 cnf(2358,plain, % 117.06/117.27 (~E(a6,f5(a1,a1))), % 117.06/117.27 inference(scs_inference,[],[2345,2])). % 117.06/117.27 cnf(2360,plain, % 117.06/117.27 (E(f3(a2,x23601),f3(a1,x23601))), % 117.06/117.27 inference(rename_variables,[],[2211])). % 117.06/117.27 cnf(2361,plain, % 117.06/117.27 (~P3(f3(a1,a1),f3(a2,a1))), % 117.06/117.27 inference(scs_inference,[],[2352,2345,2211,2360,2,12,13])). % 117.06/117.27 cnf(2366,plain, % 117.06/117.27 (~P3(a8,f4(a2,a1,a8))), % 117.06/117.27 inference(scs_inference,[],[2361,2302,451,2212,2213,2,12,13])). % 117.06/117.27 cnf(2368,plain, % 117.06/117.27 (~P3(f3(a1,a2),f3(a2,a2))), % 117.06/117.27 inference(scs_inference,[],[2361,2302,451,2212,2213,2,12,13,2329])). % 117.06/117.27 cnf(2371,plain, % 117.06/117.27 (P2(f4(a1,x23711,a1),f4(a2,x23711,a2))), % 117.06/117.27 inference(scs_inference,[],[2361,2330,2302,2222,451,2215,2212,2213,2,12,13,2329,31,14])). % 117.06/117.27 cnf(2376,plain, % 117.06/117.27 (~P3(f4(a1,a2,a1),f4(a1,a1,a1))), % 117.06/117.27 inference(scs_inference,[],[2361,2330,2302,2222,451,2215,2212,2213,2,12,13,2329,31,14,27])). % 117.06/117.27 cnf(2378,plain, % 117.06/117.27 (~P3(f4(a1,a2,a2),f4(a1,a1,a1))), % 117.06/117.27 inference(scs_inference,[],[2376,2317,2215,2,12])). % 117.06/117.27 cnf(2379,plain, % 117.06/117.27 (E(f4(x23791,x23792,a2),f4(x23791,x23792,a1))), % 117.06/117.27 inference(rename_variables,[],[2215])). % 117.06/117.27 cnf(2380,plain, % 117.06/117.27 (P2(f4(a1,x23801,a1),f4(a1,x23801,a2))), % 117.06/117.27 inference(scs_inference,[],[2376,2371,2317,2215,2213,2,12,15])). % 117.06/117.27 cnf(2382,plain, % 117.06/117.27 (~P3(f4(a1,a2,a1),f4(a1,a1,a2))), % 117.06/117.27 inference(scs_inference,[],[2376,2371,2317,2215,2379,2213,2,12,15,13])). % 117.06/117.27 cnf(2384,plain, % 117.06/117.27 (~E(a2,a8)), % 117.06/117.27 inference(scs_inference,[],[443,2])). % 117.06/117.27 cnf(2386,plain, % 117.06/117.27 (~P3(f4(a1,a2,a1),f4(a1,a2,a2))), % 117.06/117.27 inference(scs_inference,[],[2382,443,2361,2255,2214,2,12,13])). % 117.06/117.27 cnf(2388,plain, % 117.06/117.27 (~P3(f4(a1,a2,a1),f4(a1,a2,a1))), % 117.06/117.27 inference(scs_inference,[],[2382,2380,443,2361,2255,2214,2,12,13,31])). % 117.06/117.27 cnf(2391,plain, % 117.06/117.27 (~E(f5(a6,a1),f5(a1,a1))), % 117.06/117.27 inference(scs_inference,[],[2382,2380,2358,443,2361,2255,2214,95,2,12,13,31,3])). % 117.06/117.27 cnf(2393,plain, % 117.06/117.27 (~E(a2,f5(x23931,a6))), % 117.06/117.27 inference(scs_inference,[],[17,2382,2380,2358,443,2162,2361,2255,2214,95,2,12,13,31,3,11])). % 117.06/117.27 cnf(2398,plain, % 117.06/117.27 (~P3(f4(a2,a2,a2),f4(a1,a1,a1))), % 117.06/117.27 inference(scs_inference,[],[2368,2378,2391,2253,2213,2,31,12])). % 117.06/117.27 cnf(2400,plain, % 117.06/117.27 (~E(f5(a2,a1),a8)), % 117.06/117.27 inference(scs_inference,[],[2384,2368,2378,2391,2253,2213,95,2,31,12,3])). % 117.06/117.27 cnf(2405,plain, % 117.06/117.27 (~P3(f4(a1,a2,a2),f4(a1,a2,a2))), % 117.06/117.27 inference(scs_inference,[],[2386,2400,2215,2,12])). % 117.06/117.27 cnf(2411,plain, % 117.06/117.27 (P2(f4(a1,a1,a2),f4(a2,a2,a1))), % 117.06/117.27 inference(scs_inference,[],[2386,2400,2236,2239,2215,2214,2213,95,2,12,3,13,14])). % 117.06/117.27 cnf(2416,plain, % 117.06/117.27 (E(f4(a2,x24161,x24162),f4(a1,x24161,x24162))), % 117.06/117.27 inference(rename_variables,[],[2213])). % 117.06/117.27 cnf(2417,plain, % 117.06/117.27 (~P3(f4(a1,a2,a2),f4(a2,a2,a2))), % 117.06/117.27 inference(scs_inference,[],[2405,2393,2213,2416,2,12,13])). % 117.06/117.27 cnf(2420,plain, % 117.06/117.27 (~P3(f4(a1,a2,a2),f4(a1,a2,a1))), % 117.06/117.27 inference(scs_inference,[],[2417,751,2371,2,31])). % 117.06/117.27 cnf(2427,plain, % 117.06/117.27 (~E(a2,f5(a6,x24271))), % 117.06/117.27 inference(scs_inference,[],[17,2417,2398,751,2164,2371,2215,2213,2,31,12,13,11])). % 117.06/117.27 cnf(2429,plain, % 117.06/117.27 (~P3(f4(a2,a2,a2),f4(a1,a2,a1))), % 117.06/117.27 inference(scs_inference,[],[2420,2427,2213,2,12])). % 117.06/117.27 cnf(2434,plain, % 117.06/117.27 (~E(f4(a8,a7,a7),f4(a7,a1,a2))), % 117.06/117.27 inference(scs_inference,[],[1884,2])). % 117.06/117.27 cnf(2435,plain, % 117.06/117.27 (~E(a8,f5(a7,a2))), % 117.06/117.27 inference(scs_inference,[],[18,2277,1884,2,3])). % 117.06/117.27 cnf(2438,plain, % 117.06/117.27 (P2(f4(a1,a1,a1),f4(a2,a2,a1))), % 117.06/117.27 inference(scs_inference,[],[18,2277,2411,1884,2215,2,3,14])). % 117.06/117.27 cnf(2441,plain, % 117.06/117.28 (~P3(f5(a8,a1),f4(a2,a1,a8))), % 117.06/117.28 inference(scs_inference,[],[18,2366,2435,2,12])). % 117.06/117.28 cnf(2446,plain, % 117.06/117.28 (~P3(x24461,f4(a1,a1,a1))+P3(x24461,f4(a2,a2,a1))), % 117.06/117.28 inference(scs_inference,[],[2441,2438,1858,2200,2,12,31])). % 117.06/117.28 cnf(2448,plain, % 117.06/117.28 (~E(f5(a2,a1),f5(x24481,a6))), % 117.06/117.28 inference(scs_inference,[],[2441,2438,1858,1024,2162,2200,2,12,31,11])). % 117.06/117.28 cnf(2454,plain, % 117.06/117.28 (~P3(f4(a2,a2,a2),f4(a2,a2,a1))), % 117.06/117.28 inference(scs_inference,[],[2448,2429,2213,2,13])). % 117.06/117.28 cnf(2474,plain, % 117.06/117.28 (~E(f5(a2,a1),f5(a6,x24741))), % 117.06/117.28 inference(scs_inference,[],[489,2164,1024,2,11])). % 117.06/117.28 cnf(2478,plain, % 117.06/117.28 (~P2(f5(a1,a7),f5(a8,a7))), % 117.06/117.28 inference(scs_inference,[],[2474,2193,21,2,15])). % 117.06/117.28 cnf(2484,plain, % 117.06/117.28 (P2(f3(x24841,a1),f3(x24841,a2))), % 117.06/117.28 inference(scs_inference,[],[19,2474,1476,2193,2366,2212,2214,21,20,2,15,12,13,14])). % 117.06/117.28 cnf(2487,plain, % 117.06/117.28 (P2(f5(a2,x24871),f5(a1,x24871))), % 117.06/117.28 inference(scs_inference,[],[19,1480,2199,2,15])). % 117.06/117.28 cnf(2495,plain, % 117.06/117.28 (~E(f5(a2,a2),f5(x24951,a6))), % 117.06/117.28 inference(scs_inference,[],[1424,2162,1021,2,11])). % 117.06/117.28 cnf(2498,plain, % 117.06/117.28 (~P2(f5(a7,a7),f5(a8,a7))), % 117.06/117.28 inference(scs_inference,[],[2495,2179,20,2,14])). % 117.06/117.28 cnf(2506,plain, % 117.06/117.28 (P2(x25061,x25061)), % 117.06/117.28 inference(rename_variables,[],[19])). % 117.06/117.28 cnf(2507,plain, % 117.06/117.28 (P2(f4(x25071,x25072,a1),f4(x25071,x25072,a2))), % 117.06/117.28 inference(scs_inference,[],[19,2506,1410,2200,2215,2,15,14])). % 117.06/117.28 cnf(2512,plain, % 117.06/117.28 (P2(f4(x25121,a1,x25122),f4(x25121,a2,x25122))), % 117.06/117.28 inference(scs_inference,[],[19,476,2214,2,14])). % 117.06/117.28 cnf(2516,plain, % 117.06/117.28 (E(f4(a2,a2,a1),f4(a1,a1,a1))), % 117.06/117.28 inference(scs_inference,[],[19,2454,476,2214,2213,2,14,31,3])). % 117.06/117.28 cnf(2520,plain, % 117.06/117.28 (~E(f5(a1,a1),f5(x25201,a6))), % 117.06/117.28 inference(scs_inference,[],[2190,2302,95,2,3])). % 117.06/117.28 cnf(2522,plain, % 117.06/117.28 (~E(f5(a2,a1),a6)), % 117.06/117.28 inference(scs_inference,[],[2190,2302,1024,22,95,2,3,11])). % 117.06/117.28 cnf(2524,plain, % 117.06/117.28 (P2(f4(a2,a2,a1),f4(a1,a1,a1))), % 117.06/117.28 inference(scs_inference,[],[19,2516,2520,2,15])). % 117.06/117.28 cnf(2526,plain, % 117.06/117.28 (~P3(f4(a1,a2,a1),f4(a2,a2,a1))), % 117.06/117.28 inference(scs_inference,[],[19,2516,2520,2376,2,15,13])). % 117.06/117.28 cnf(2527,plain, % 117.06/117.28 (~P3(f4(a1,a2,a2),f4(a2,a2,a1))), % 117.06/117.28 inference(scs_inference,[],[19,2516,2520,2376,2215,2,15,13,12])). % 117.06/117.28 cnf(2532,plain, % 117.06/117.28 (~P3(f4(a2,a2,a1),f4(a1,a1,a1))), % 117.06/117.28 inference(scs_inference,[],[2526,2522,2213,2,12,2446])). % 117.06/117.28 cnf(2534,plain, % 117.06/117.28 (~P3(f4(a2,a2,a1),f4(a1,a2,a2))), % 117.06/117.28 inference(scs_inference,[],[2526,2522,2213,2,12,2446,2243])). % 117.06/117.28 cnf(2542,plain, % 117.06/117.28 (~E(f5(a1,a1),f5(a6,x25421))), % 117.06/117.28 inference(scs_inference,[],[2534,2532,2507,2317,627,2215,95,2,13,31,3])). % 117.06/117.28 cnf(2545,plain, % 117.06/117.28 (P2(f4(a2,a1,a1),f4(a1,a1,a1))), % 117.06/117.28 inference(scs_inference,[],[2524,2542,2214,2,14])). % 117.06/117.28 cnf(2550,plain, % 117.06/117.28 (~E(f5(a2,a2),f5(a6,x25501))), % 117.06/117.28 inference(scs_inference,[],[2527,2524,2542,2512,2164,1021,2214,2,14,31,11])). % 117.06/117.28 cnf(2552,plain, % 117.06/117.28 (~P3(f4(a2,a2,a1),f4(a2,a1,a1))), % 117.06/117.28 inference(scs_inference,[],[2545,2550,2532,2,31])). % 117.06/117.28 cnf(2554,plain, % 117.06/117.28 (P2(f3(a2,a1),f3(a1,a2))), % 117.06/117.28 inference(scs_inference,[],[2545,2550,2484,2532,2211,2,31,15])). % 117.06/117.28 cnf(2558,plain, % 117.06/117.28 (~P3(f3(a2,a1),f3(a2,a1))), % 117.06/117.28 inference(scs_inference,[],[2554,2337,642,2,31])). % 117.06/117.28 cnf(2583,plain, % 117.06/117.28 (P2(f4(a1,a1,a1),f4(a2,a2,a2))), % 117.06/117.28 inference(scs_inference,[],[2507,925,2516,2,14])). % 117.06/117.28 cnf(2586,plain, % 117.06/117.28 (P2(f4(a1,a1,a1),f4(a1,a2,a2))), % 117.06/117.28 inference(scs_inference,[],[2583,417,2213,2,15])). % 117.06/117.28 cnf(2610,plain, % 117.06/117.28 (E(f5(a2,a2),f5(a1,a1))), % 117.06/117.28 inference(scs_inference,[],[42,193,36])). % 117.06/117.28 cnf(2630,plain, % 117.06/117.28 (E(a2,f5(a1,a1))), % 117.06/117.28 inference(scs_inference,[],[42,88,36])). % 117.06/117.28 cnf(2680,plain, % 117.06/117.28 (E(f4(f5(a2,a2),x26801,x26802),f4(a1,x26801,x26802))), % 117.06/117.28 inference(scs_inference,[],[1021,24,6])). % 117.06/117.28 cnf(2696,plain, % 117.06/117.28 (~P3(f3(a2,a1),f5(f5(a2,f3(a2,a1)),a1))), % 117.06/117.28 inference(scs_inference,[],[17,2558,18,26,34])). % 117.06/117.28 cnf(2735,plain, % 117.06/117.28 (E(f5(x27351,f5(a1,a1)),f5(x27351,a2))), % 117.06/117.28 inference(scs_inference,[],[2630,2,5])). % 117.06/117.28 cnf(2748,plain, % 117.06/117.28 (E(f4(a1,x27481,x27482),f4(a2,x27481,x27482))), % 117.06/117.28 inference(scs_inference,[],[2197,2,6])). % 117.06/117.28 cnf(2749,plain, % 117.06/117.28 (P2(f4(a2,a1,a1),f4(a1,a2,a2))), % 117.06/117.28 inference(scs_inference,[],[2586,2748,14])). % 117.06/117.28 cnf(2750,plain, % 117.06/117.28 (E(f4(a1,x27501,x27502),f4(a2,x27501,x27502))), % 117.06/117.28 inference(rename_variables,[],[2748])). % 117.06/117.28 cnf(2751,plain, % 117.06/117.28 (~P3(f4(a1,a2,a1),f4(a2,a1,a1))), % 117.06/117.28 inference(scs_inference,[],[2586,2748,2750,2552,14,12])). % 117.06/117.28 cnf(2757,plain, % 117.06/117.28 (~P3(f4(a1,a2,a1),f4(a2,a1,a2))), % 117.06/117.28 inference(scs_inference,[],[2749,2751,2748,2215,15,13])). % 117.06/117.28 cnf(2772,plain, % 117.06/117.28 (E(a1,a2)), % 117.23/117.28 inference(scs_inference,[],[2197,2])). % 117.23/117.28 cnf(2773,plain, % 117.23/117.28 (E(f5(a1,x27731),f5(a2,x27731))), % 117.23/117.28 inference(scs_inference,[],[2197,2,4])). % 117.23/117.28 cnf(2775,plain, % 117.23/117.28 (E(f3(a1,x27751),f3(a2,x27751))), % 117.23/117.28 inference(scs_inference,[],[2197,2,4,5,9])). % 117.23/117.28 cnf(2776,plain, % 117.23/117.28 (E(f4(x27761,a1,x27762),f4(x27761,a2,x27762))), % 117.23/117.28 inference(scs_inference,[],[2197,2,4,5,9,7])). % 117.23/117.28 cnf(2778,plain, % 117.23/117.28 (E(f3(x27781,a1),f3(x27781,a2))), % 117.23/117.28 inference(scs_inference,[],[2197,2,4,5,9,7,8,10])). % 117.23/117.28 cnf(2779,plain, % 117.23/117.28 (~P3(f4(a1,a1,a1),f4(a2,a1,a2))), % 117.23/117.28 inference(scs_inference,[],[2757,2197,2,4,5,9,7,8,10,12])). % 117.23/117.28 cnf(2780,plain, % 117.23/117.28 (P2(f3(a1,a2),f3(a2,a1))), % 117.23/117.28 inference(scs_inference,[],[2343,2757,2197,2,4,5,9,7,8,10,12,15])). % 117.23/117.28 cnf(2783,plain, % 117.23/117.28 (E(f3(a1,x27831),f3(a2,x27831))), % 117.23/117.28 inference(rename_variables,[],[2775])). % 117.23/117.28 cnf(2787,plain, % 117.23/117.28 (~P3(f4(a1,a1,a1),f4(a1,a2,a1))), % 117.23/117.28 inference(scs_inference,[],[2779,2780,2776,2775,2388,2222,14,31,12])). % 117.23/117.28 cnf(2789,plain, % 117.23/117.28 (E(f3(a1,a1),f3(a2,a2))), % 117.23/117.28 inference(scs_inference,[],[2779,2780,2776,2775,2783,2778,2388,2222,14,31,12,3])). % 117.23/117.28 cnf(2918,plain, % 117.23/117.28 (P3(f3(a7,f5(a8,a7)),f5(x29181,a7))), % 117.23/117.28 inference(scs_inference,[],[2179,30,39])). % 117.23/117.28 cnf(2922,plain, % 117.23/117.28 (~P2(f5(a1,a7),f5(a2,a1))), % 117.23/117.28 inference(scs_inference,[],[2478,515,30,31])). % 117.23/117.28 cnf(2925,plain, % 117.23/117.28 (~P2(f5(a1,a7),f5(a1,a1))), % 117.23/117.28 inference(scs_inference,[],[2922,2773,2199,14,15])). % 117.23/117.28 cnf(2928,plain, % 117.23/117.28 (~P2(f5(a2,a7),f5(a1,a1))), % 117.23/117.28 inference(scs_inference,[],[2925,2199,14])). % 117.23/117.28 cnf(2930,plain, % 117.23/117.28 (~P2(f5(a1,a7),f5(a2,a2))), % 117.23/117.28 inference(scs_inference,[],[2925,2610,2199,14,15])). % 117.23/117.28 cnf(2932,plain, % 117.23/117.28 (~P2(f5(a2,a7),f5(a2,a2))), % 117.23/117.28 inference(scs_inference,[],[2930,2199,14])). % 117.23/117.28 cnf(2934,plain, % 117.23/117.28 (~P2(f5(a2,a7),a2)), % 117.23/117.28 inference(scs_inference,[],[2930,2928,2630,2199,14,15])). % 117.23/117.28 cnf(2950,plain, % 117.23/117.28 (P3(f3(f5(a2,a7),f5(a2,a2)),f5(a2,a7))), % 117.23/117.28 inference(scs_inference,[],[2789,2932,526,2498,549,35,28,6,29,5,7,10,8,9,39,30])). % 117.23/117.28 cnf(2962,plain, % 117.23/117.28 (E(f4(f5(a2,a2),x29621,x29622),f4(a1,x29621,x29622))), % 117.23/117.28 inference(rename_variables,[],[2680])). % 117.23/117.28 cnf(2969,plain, % 117.23/117.28 (E(f4(f5(a2,a2),x29691,x29692),f4(a1,x29691,x29692))), % 117.23/117.28 inference(rename_variables,[],[2680])). % 117.23/117.28 cnf(2972,plain, % 117.23/117.28 (~P3(x29721,f5(f5(a2,a2),f5(a2,a2)))), % 117.23/117.28 inference(rename_variables,[],[1975])). % 117.23/117.28 cnf(2984,plain, % 117.23/117.28 (~P3(x29841,f5(f5(a2,a2),f5(a2,a2)))), % 117.23/117.28 inference(rename_variables,[],[1975])). % 117.23/117.28 cnf(2986,plain, % 117.23/117.28 (~E(f5(a8,x29861),f5(f5(f5(a2,a2),f5(a2,a2)),f5(f5(a2,a2),f5(a2,a2))))), % 117.23/117.28 inference(scs_inference,[],[474,2772,2434,2787,2789,2932,2487,2934,1543,2680,2962,2969,2918,680,1975,2972,2984,1995,526,2696,1562,2512,1541,2498,549,44,35,28,6,29,5,7,10,8,9,39,30,40,27,24,2,4,11,13,32,31,14,33,41,12,15,3,36,34])). % 117.23/117.28 cnf(3005,plain, % 117.23/117.28 ($false), % 117.23/117.28 inference(scs_inference,[],[424,57,2179,2918,2735,2950,2986,4,2,27,40,30,39,35]), % 117.23/117.28 ['proof']). % 117.23/117.28 % SZS output end Proof % 117.23/117.28 % Total time :116.500000s %------------------------------------------------------------------------------