%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SEU128+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 : n018.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:11 EDT 2024 % Result : Theorem 116.67s 116.74s % Output : CNFRefutation 116.75s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SEU128+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 : n018.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 15:24:39 EDT 2024 % 0.12/0.33 % CPUTime : % 0.51/0.57 start to proof:theBenchmark % 116.67/116.72 %------------------------------------------- % 116.67/116.72 % File :CSE---1.7 % 116.67/116.72 % Problem :theBenchmark % 116.67/116.72 % Transform :cnf % 116.67/116.72 % Format :tptp:raw % 116.67/116.72 % Command :java -jar mcs_scs.jar %d %s % 116.67/116.72 % 116.67/116.72 % Result :Theorem 116.110000s % 116.67/116.72 % Output :CNFRefutation 116.110000s % 116.67/116.72 %------------------------------------------- % 116.67/116.73 %------------------------------------------------------------------------------ % 116.67/116.73 % File : SEU128+1 : TPTP v8.2.0. Released v3.3.0. % 116.67/116.73 % Domain : Set theory % 116.67/116.73 % Problem : MPTP bushy problem t19_xboole_1 % 116.67/116.73 % Version : [Urb07] axioms : Especial. % 116.67/116.73 % English : % 116.67/116.73 % 116.67/116.73 % Refs : [Ban01] Bancerek et al. (2001), On the Characterizations of Co % 116.67/116.73 % : [Urb07] Urban (2006), Email to G. Sutcliffe % 116.67/116.73 % Source : [Urb07] % 116.67/116.73 % Names : bushy-t19_xboole_1 [Urb07] % 116.67/116.73 % 116.67/116.73 % Status : Theorem % 116.67/116.73 % Rating : 0.22 v8.2.0, 0.25 v8.1.0, 0.22 v7.5.0, 0.25 v7.4.0, 0.13 v7.3.0, 0.14 v7.2.0, 0.10 v7.1.0, 0.09 v7.0.0, 0.07 v6.4.0, 0.12 v6.2.0, 0.28 v6.1.0, 0.30 v6.0.0, 0.22 v5.5.0, 0.30 v5.4.0, 0.39 v5.3.0, 0.37 v5.2.0, 0.10 v5.0.0, 0.17 v4.0.1, 0.22 v4.0.0, 0.29 v3.7.0, 0.25 v3.5.0, 0.21 v3.4.0, 0.26 v3.3.0 % 116.67/116.73 % Syntax : Number of formulae : 16 ( 9 unt; 0 def) % 116.67/116.73 % Number of atoms : 28 ( 6 equ) % 116.67/116.73 % Maximal formula atoms : 4 ( 1 avg) % 116.67/116.73 % Number of connectives : 17 ( 5 ~; 0 |; 5 &) % 116.67/116.74 % ( 3 <=>; 4 =>; 0 <=; 0 <~>) % 116.67/116.74 % Maximal formula depth : 8 ( 4 avg) % 116.67/116.74 % Maximal term depth : 2 ( 1 avg) % 116.67/116.74 % Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty) % 116.67/116.74 % Number of functors : 2 ( 2 usr; 1 con; 0-2 aty) % 116.67/116.74 % Number of variables : 26 ( 24 !; 2 ?) % 116.67/116.74 % SPC : FOF_THM_RFO_SEQ % 116.67/116.74 % 116.67/116.74 % Comments : Translated by MPTP 0.2 from the original problem in the Mizar % 116.67/116.74 % library, www.mizar.org % 116.67/116.74 %------------------------------------------------------------------------------ % 116.67/116.74 fof(antisymmetry_r2_hidden,axiom, % 116.67/116.74 ! [A,B] : % 116.67/116.74 ( in(A,B) % 116.67/116.74 => ~ in(B,A) ) ). % 116.67/116.74 % 116.67/116.74 fof(commutativity_k3_xboole_0,axiom, % 116.67/116.74 ! [A,B] : set_intersection2(A,B) = set_intersection2(B,A) ). % 116.67/116.74 % 116.67/116.74 fof(d3_tarski,axiom, % 116.67/116.74 ! [A,B] : % 116.67/116.74 ( subset(A,B) % 116.67/116.74 <=> ! [C] : % 116.67/116.74 ( in(C,A) % 116.67/116.74 => in(C,B) ) ) ). % 116.67/116.74 % 116.67/116.74 fof(d3_xboole_0,axiom, % 116.67/116.74 ! [A,B,C] : % 116.67/116.74 ( C = set_intersection2(A,B) % 116.67/116.74 <=> ! [D] : % 116.67/116.74 ( in(D,C) % 116.67/116.74 <=> ( in(D,A) % 116.67/116.74 & in(D,B) ) ) ) ). % 116.67/116.74 % 116.67/116.74 fof(dt_k1_xboole_0,axiom, % 116.67/116.74 $true ). % 116.67/116.74 % 116.67/116.74 fof(dt_k3_xboole_0,axiom, % 116.67/116.74 $true ). % 116.67/116.74 % 116.67/116.74 fof(fc1_xboole_0,axiom, % 116.67/116.74 empty(empty_set) ). % 116.67/116.74 % 116.67/116.74 fof(idempotence_k3_xboole_0,axiom, % 116.67/116.74 ! [A,B] : set_intersection2(A,A) = A ). % 116.67/116.74 % 116.67/116.74 fof(rc1_xboole_0,axiom, % 116.67/116.74 ? [A] : empty(A) ). % 116.67/116.74 % 116.67/116.74 fof(rc2_xboole_0,axiom, % 116.67/116.74 ? [A] : ~ empty(A) ). % 116.67/116.74 % 116.67/116.74 fof(reflexivity_r1_tarski,axiom, % 116.67/116.74 ! [A,B] : subset(A,A) ). % 116.67/116.74 % 116.67/116.74 fof(t19_xboole_1,conjecture, % 116.67/116.74 ! [A,B,C] : % 116.67/116.74 ( ( subset(A,B) % 116.67/116.74 & subset(A,C) ) % 116.67/116.74 => subset(A,set_intersection2(B,C)) ) ). % 116.67/116.74 % 116.67/116.74 fof(t2_boole,axiom, % 116.67/116.74 ! [A] : set_intersection2(A,empty_set) = empty_set ). % 116.67/116.74 % 116.67/116.74 fof(t6_boole,axiom, % 116.67/116.74 ! [A] : % 116.67/116.74 ( empty(A) % 116.67/116.74 => A = empty_set ) ). % 116.67/116.74 % 116.67/116.74 fof(t7_boole,axiom, % 116.67/116.74 ! [A,B] : % 116.67/116.74 ~ ( in(A,B) % 116.67/116.74 & empty(B) ) ). % 116.67/116.74 % 116.67/116.74 fof(t8_boole,axiom, % 116.67/116.74 ! [A,B] : % 116.67/116.74 ~ ( empty(A) % 116.67/116.74 & A != B % 116.67/116.74 & empty(B) ) ). % 116.67/116.74 % 116.67/116.74 %------------------------------------------------------------------------------ % 116.67/116.74 %------------------------------------------- % 116.67/116.74 % Proof found % 116.67/116.74 % SZS status Theorem for theBenchmark % 116.67/116.74 % SZS output start Proof % 116.75/116.75 %ClaNum:38(EqnAxiom:15) % 116.75/116.75 %VarNum:99(SingletonVarNum:40) % 116.75/116.75 %MaxLitNum:4 % 116.75/116.75 %MaxfuncDepth:1 % 116.75/116.75 %SharedTerms:13 % 116.75/116.75 %goalClause: 18 19 25 % 116.75/116.75 %singleGoalClaCount:3 % 116.75/116.75 [16]P1(a1) % 116.75/116.75 [17]P1(a2) % 116.75/116.75 [18]P2(a5,a7) % 116.75/116.75 [19]P2(a5,a8) % 116.75/116.75 [24]~P1(a6) % 116.75/116.75 [25]~P2(a5,f9(a7,a8)) % 116.75/116.75 [21]P2(x211,x211) % 116.75/116.75 [20]E(f9(x201,a1),a1) % 116.75/116.75 [22]E(f9(x221,x221),x221) % 116.75/116.75 [23]E(f9(x231,x232),f9(x232,x231)) % 116.75/116.75 [26]~P1(x261)+E(x261,a1) % 116.75/116.75 [28]~P1(x281)+~P3(x282,x281) % 116.75/116.75 [29]~P3(x292,x291)+~P3(x291,x292) % 116.75/116.75 [30]P2(x301,x302)+P3(f3(x301,x302),x301) % 116.75/116.75 [34]P2(x341,x342)+~P3(f3(x341,x342),x342) % 116.75/116.75 [27]~P1(x272)+~P1(x271)+E(x271,x272) % 116.75/116.75 [31]~P2(x313,x312)+P3(x311,x312)+~P3(x311,x313) % 116.75/116.75 [36]P3(f4(x362,x363,x361),x361)+P3(f4(x362,x363,x361),x363)+E(x361,f9(x362,x363)) % 116.75/116.75 [37]P3(f4(x372,x373,x371),x371)+P3(f4(x372,x373,x371),x372)+E(x371,f9(x372,x373)) % 116.75/116.75 [32]~P3(x321,x323)+P3(x321,x322)+~E(x323,f9(x324,x322)) % 116.75/116.75 [33]~P3(x331,x333)+P3(x331,x332)+~E(x333,f9(x332,x334)) % 116.75/116.75 [38]~P3(f4(x382,x383,x381),x381)+~P3(f4(x382,x383,x381),x383)+~P3(f4(x382,x383,x381),x382)+E(x381,f9(x382,x383)) % 116.75/116.75 [35]~P3(x351,x354)+~P3(x351,x353)+P3(x351,x352)+~E(x352,f9(x353,x354)) % 116.75/116.75 %EqnAxiom % 116.75/116.75 [1]E(x11,x11) % 116.75/116.75 [2]E(x22,x21)+~E(x21,x22) % 116.75/116.75 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 116.75/116.75 [4]~E(x41,x42)+E(f9(x41,x43),f9(x42,x43)) % 116.75/116.75 [5]~E(x51,x52)+E(f9(x53,x51),f9(x53,x52)) % 116.75/116.75 [6]~E(x61,x62)+E(f4(x61,x63,x64),f4(x62,x63,x64)) % 116.75/116.75 [7]~E(x71,x72)+E(f4(x73,x71,x74),f4(x73,x72,x74)) % 116.75/116.75 [8]~E(x81,x82)+E(f4(x83,x84,x81),f4(x83,x84,x82)) % 116.75/116.75 [9]~E(x91,x92)+E(f3(x91,x93),f3(x92,x93)) % 116.75/116.75 [10]~E(x101,x102)+E(f3(x103,x101),f3(x103,x102)) % 116.75/116.75 [11]~P1(x111)+P1(x112)+~E(x111,x112) % 116.75/116.75 [12]P3(x122,x123)+~E(x121,x122)+~P3(x121,x123) % 116.75/116.75 [13]P3(x133,x132)+~E(x131,x132)+~P3(x133,x131) % 116.75/116.75 [14]P2(x142,x143)+~E(x141,x142)+~P2(x141,x143) % 116.75/116.75 [15]P2(x153,x152)+~E(x151,x152)+~P2(x153,x151) % 116.75/116.75 % 116.75/116.75 %------------------------------------------- % 116.75/116.76 cnf(39,plain, % 116.75/116.76 (~P3(x391,f9(x392,x393))+P3(x391,x393)), % 116.75/116.76 inference(equality_inference,[],[32])). % 116.75/116.76 cnf(40,plain, % 116.75/116.76 (~P3(x401,f9(x402,x403))+P3(x401,x402)), % 116.75/116.76 inference(equality_inference,[],[33])). % 116.75/116.76 cnf(41,plain, % 116.75/116.76 (~P3(x411,x412)+~P3(x411,x413)+P3(x411,f9(x413,x412))), % 116.75/116.76 inference(equality_inference,[],[35])). % 116.75/116.76 cnf(42,plain, % 116.75/116.76 (~P3(x421,a1)), % 116.75/116.76 inference(scs_inference,[],[16,28])). % 116.75/116.76 cnf(44,plain, % 116.75/116.76 (~P3(x441,f9(x442,a1))), % 116.75/116.76 inference(scs_inference,[],[16,28,39])). % 116.75/116.76 cnf(46,plain, % 116.75/116.76 (~P3(x461,f9(a1,x462))), % 116.75/116.76 inference(scs_inference,[],[16,28,39,40])). % 116.75/116.76 cnf(48,plain, % 116.75/116.76 (E(x481,f9(x481,x481))), % 116.75/116.76 inference(scs_inference,[],[22,16,28,39,40,2])). % 116.75/116.76 cnf(49,plain, % 116.75/116.76 (P2(f9(a5,a5),a7)), % 116.75/116.76 inference(scs_inference,[],[18,22,16,28,39,40,2,14])). % 116.75/116.76 cnf(50,plain, % 116.75/116.76 (~E(a7,f9(a7,a8))), % 116.75/116.76 inference(scs_inference,[],[18,25,22,16,28,39,40,2,14,15])). % 116.75/116.76 cnf(51,plain, % 116.75/116.76 (P3(f4(a7,a8,a7),a7)), % 116.75/116.76 inference(scs_inference,[],[18,25,22,16,28,39,40,2,14,15,37])). % 116.75/116.76 cnf(53,plain, % 116.75/116.76 (~E(a7,f9(a8,a7))), % 116.75/116.76 inference(scs_inference,[],[18,25,22,23,16,28,39,40,2,14,15,37,3])). % 116.75/116.76 cnf(54,plain, % 116.75/116.76 (E(f9(x541,x542),f9(x542,x541))), % 116.75/116.77 inference(rename_variables,[],[23])). % 116.75/116.77 cnf(56,plain, % 116.75/116.77 (P3(f4(a7,a8,a7),f9(a7,a7))), % 116.75/116.77 inference(scs_inference,[],[18,25,22,23,54,16,28,39,40,2,14,15,37,3,13,35])). % 116.75/116.77 cnf(59,plain, % 116.75/116.77 (~P3(f4(a7,a8,a7),a8)), % 116.75/116.77 inference(scs_inference,[],[18,25,22,23,54,16,28,39,40,2,14,15,37,3,13,35,38])). % 116.75/116.77 cnf(61,plain, % 116.75/116.77 (~P1(a7)), % 116.75/116.77 inference(scs_inference,[],[18,25,22,23,54,16,28,39,40,2,14,15,37,3,13,35,38,26])). % 116.75/116.77 cnf(63,plain, % 116.75/116.77 (~P3(a7,f4(a7,a8,a7))), % 116.75/116.77 inference(scs_inference,[],[18,25,22,23,54,16,28,39,40,2,14,15,37,3,13,35,38,26,29])). % 116.75/116.77 cnf(71,plain, % 116.75/116.77 (~P3(x711,f9(x712,f9(x713,a1)))), % 116.75/116.77 inference(scs_inference,[],[44,39])). % 116.75/116.77 cnf(73,plain, % 116.75/116.77 (~P3(x731,f9(f9(x732,a1),x733))), % 116.75/116.77 inference(scs_inference,[],[44,39,40])). % 116.75/116.77 cnf(77,plain, % 116.75/116.77 (~P3(x771,a2)), % 116.75/116.77 inference(scs_inference,[],[44,56,17,39,40,29,28])). % 116.75/116.77 cnf(79,plain, % 116.75/116.77 (E(a1,f9(x791,a1))), % 116.75/116.77 inference(scs_inference,[],[44,56,20,17,39,40,29,28,2])). % 116.75/116.77 cnf(80,plain, % 116.75/116.77 (P2(f9(x801,a1),x802)), % 116.75/116.77 inference(scs_inference,[],[44,56,20,17,39,40,29,28,2,30])). % 116.75/116.77 cnf(81,plain, % 116.75/116.77 (~P3(x811,f9(x812,a1))), % 116.75/116.77 inference(rename_variables,[],[44])). % 116.75/116.77 cnf(83,plain, % 116.75/116.77 (P3(f4(a8,a7,a7),a7)), % 116.75/116.77 inference(scs_inference,[],[44,56,53,20,17,39,40,29,28,2,30,36])). % 116.75/116.77 cnf(85,plain, % 116.75/116.77 (E(f9(x851,a1),f9(a1,a1))), % 116.75/116.77 inference(scs_inference,[],[48,44,56,53,20,17,39,40,29,28,2,30,36,3])). % 116.75/116.77 cnf(86,plain, % 116.75/116.77 (E(x861,f9(x861,x861))), % 116.75/116.77 inference(rename_variables,[],[48])). % 116.75/116.77 cnf(87,plain, % 116.75/116.77 (P2(f9(a5,a5),a8)), % 116.75/116.77 inference(scs_inference,[],[19,48,86,44,56,53,20,17,39,40,29,28,2,30,36,3,14])). % 116.75/116.77 cnf(88,plain, % 116.75/116.77 (E(x881,f9(x881,x881))), % 116.75/116.77 inference(rename_variables,[],[48])). % 116.75/116.77 cnf(89,plain, % 116.75/116.77 (~E(a8,f9(a7,a8))), % 116.75/116.77 inference(scs_inference,[],[19,25,48,86,44,56,53,20,17,39,40,29,28,2,30,36,3,14,15])). % 116.75/116.77 cnf(90,plain, % 116.75/116.77 (P3(f9(f4(a7,a8,a7),f4(a7,a8,a7)),a7)), % 116.75/116.77 inference(scs_inference,[],[19,25,48,86,88,51,44,56,53,20,17,39,40,29,28,2,30,36,3,14,15,12])). % 116.75/116.77 cnf(91,plain, % 116.75/116.77 (E(x911,f9(x911,x911))), % 116.75/116.77 inference(rename_variables,[],[48])). % 116.75/116.77 cnf(92,plain, % 116.75/116.77 (~E(a7,f9(x921,a1))), % 116.75/116.77 inference(scs_inference,[],[19,25,48,86,88,51,44,81,56,53,20,17,39,40,29,28,2,30,36,3,14,15,12,13])). % 116.75/116.77 cnf(96,plain, % 116.75/116.77 (~P3(f4(a8,a7,a7),a8)), % 116.75/116.77 inference(scs_inference,[],[19,25,48,86,88,91,51,44,81,56,53,20,16,17,39,40,29,28,2,30,36,3,14,15,12,13,11,38])). % 116.75/116.77 cnf(98,plain, % 116.75/116.77 (P3(f4(a7,a8,a7),f9(f9(a7,a7),f9(a7,a7)))), % 116.75/116.77 inference(scs_inference,[],[19,25,48,86,88,91,51,44,81,56,53,20,16,22,17,39,40,29,28,2,30,36,3,14,15,12,13,11,38,35])). % 116.75/116.77 cnf(105,plain, % 116.75/116.77 (~P3(x1051,f9(f9(a1,x1052),x1053))), % 116.75/116.77 inference(scs_inference,[],[46,40])). % 116.75/116.77 cnf(109,plain, % 116.75/116.77 (~P3(x1091,f9(x1092,f9(a1,x1093)))), % 116.75/116.77 inference(scs_inference,[],[98,46,40,29,39])). % 116.75/116.77 cnf(111,plain, % 116.75/116.77 (P2(f9(a1,x1111),x1112)), % 116.75/116.77 inference(scs_inference,[],[98,46,40,29,39,30])). % 116.75/116.77 cnf(115,plain, % 116.75/116.77 (~E(a7,f9(f9(a7,a8),f9(a7,a8)))), % 116.75/116.77 inference(scs_inference,[],[50,98,46,85,22,40,29,39,30,2,3])). % 116.75/116.77 cnf(117,plain, % 116.75/116.77 (P3(f4(a7,a8,a8),a8)), % 116.75/116.77 inference(scs_inference,[],[50,89,98,46,85,22,40,29,39,30,2,3,36])). % 116.75/116.77 cnf(120,plain, % 116.75/116.77 (P2(x1201,x1201)), % 116.75/116.77 inference(rename_variables,[],[21])). % 116.75/116.77 cnf(121,plain, % 116.75/116.77 (P3(f9(f4(a8,a7,a7),f4(a8,a7,a7)),a7)), % 116.75/116.77 inference(scs_inference,[],[25,50,21,89,98,46,83,85,48,22,40,29,39,30,2,3,36,14,12])). % 116.75/116.77 cnf(123,plain, % 116.75/116.77 (~E(a5,f9(a7,a8))), % 116.75/116.77 inference(scs_inference,[],[25,50,21,120,89,98,46,83,85,48,22,40,29,39,30,2,3,36,14,12,15])). % 116.75/116.77 cnf(125,plain, % 116.75/116.77 (P1(f9(x1251,a1))), % 116.75/116.77 inference(scs_inference,[],[25,50,21,120,89,98,46,83,85,79,48,16,22,40,29,39,30,2,3,36,14,12,15,11])). % 116.75/116.77 cnf(126,plain, % 116.75/116.77 (~E(a7,f9(x1261,f9(x1262,a1)))), % 116.75/116.77 inference(scs_inference,[],[25,50,21,120,89,98,71,46,83,85,79,48,16,22,40,29,39,30,2,3,36,14,12,15,11,13])). % 116.75/116.77 cnf(128,plain, % 116.75/116.77 (~P3(f4(a7,a8,a8),a7)), % 116.75/116.77 inference(scs_inference,[],[25,50,21,120,89,98,71,46,83,85,79,48,16,22,40,29,39,30,2,3,36,14,12,15,11,13,38])). % 116.75/116.77 cnf(135,plain, % 116.75/116.77 (~P3(f4(a7,a8,a7),f9(x1351,a8))), % 116.75/116.77 inference(scs_inference,[],[117,59,29,39])). % 116.75/116.77 cnf(137,plain, % 116.75/116.77 (~P3(f4(a7,a8,a7),f9(a8,x1371))), % 116.75/116.77 inference(scs_inference,[],[117,59,29,39,40])). % 116.75/116.77 cnf(139,plain, % 116.75/116.77 (P2(a1,x1391)), % 116.75/116.77 inference(scs_inference,[],[117,59,42,29,39,40,30])). % 116.75/116.77 cnf(140,plain, % 116.75/116.77 (~P3(x1401,a1)), % 116.75/116.77 inference(rename_variables,[],[42])). % 116.75/116.77 cnf(142,plain, % 116.75/116.77 (P3(f4(x1421,a1,a7),a7)), % 116.75/116.77 inference(scs_inference,[],[117,59,42,140,92,29,39,40,30,36])). % 116.75/116.77 cnf(150,plain, % 116.75/116.77 (P2(f9(a5,a5),f9(a7,a7))), % 116.75/116.77 inference(scs_inference,[],[25,80,49,117,59,42,140,92,48,125,29,39,40,30,36,14,27,12,15])). % 116.75/116.77 cnf(152,plain, % 116.75/116.77 (P1(f9(a1,x1521))), % 116.75/116.77 inference(scs_inference,[],[25,80,49,23,117,59,42,140,92,48,125,29,39,40,30,36,14,27,12,15,11])). % 116.75/116.77 cnf(153,plain, % 116.75/116.77 (E(f9(x1531,x1532),f9(x1532,x1531))), % 116.75/116.77 inference(rename_variables,[],[23])). % 116.75/116.77 cnf(154,plain, % 116.75/116.77 (~E(a8,f9(f9(x1541,a1),x1542))), % 116.75/116.77 inference(scs_inference,[],[25,80,49,23,73,117,59,42,140,92,48,125,29,39,40,30,36,14,27,12,15,11,13])). % 116.75/116.77 cnf(156,plain, % 116.75/116.77 (P3(f4(a7,a8,a8),f9(a8,a8))), % 116.75/116.77 inference(scs_inference,[],[25,80,49,23,153,73,117,59,42,140,92,48,125,29,39,40,30,36,14,27,12,15,11,13,35])). % 116.75/116.77 cnf(159,plain, % 116.75/116.77 (~E(a8,a7)), % 116.75/116.77 inference(scs_inference,[],[25,80,49,23,153,73,117,59,42,140,92,48,125,29,39,40,30,36,14,27,12,15,11,13,35,8])). % 116.75/116.77 cnf(164,plain, % 116.75/116.77 (~P3(f4(a7,a8,a8),f9(x1641,a7))), % 116.75/116.77 inference(scs_inference,[],[128,39])). % 116.75/116.77 cnf(166,plain, % 116.75/116.77 (~P3(f4(a7,a8,a8),f9(a7,x1661))), % 116.75/116.77 inference(scs_inference,[],[128,39,40])). % 116.75/116.77 cnf(168,plain, % 116.75/116.77 (P2(a2,x1681)), % 116.75/116.77 inference(scs_inference,[],[128,77,39,40,30])). % 116.75/116.77 cnf(171,plain, % 116.75/116.77 (~P3(f9(a8,a8),f4(a7,a8,a8))), % 116.75/116.77 inference(scs_inference,[],[128,156,77,39,40,30,29])). % 116.75/116.77 cnf(173,plain, % 116.75/116.77 (P3(f4(x1731,f9(x1732,a1),a7),a7)), % 116.75/116.77 inference(scs_inference,[],[44,128,156,77,126,39,40,30,29,36])). % 116.75/116.77 cnf(175,plain, % 116.75/116.77 (~P3(x1751,f9(x1752,a1))), % 116.75/116.77 inference(rename_variables,[],[44])). % 116.75/116.77 cnf(177,plain, % 116.75/116.77 (P2(a5,f9(a7,a7))), % 116.75/116.77 inference(scs_inference,[],[150,22,44,128,156,77,126,39,40,30,29,36,14])). % 116.75/116.77 cnf(179,plain, % 116.75/116.77 (~P1(a8)), % 116.75/116.77 inference(scs_inference,[],[150,22,44,128,156,77,126,154,125,39,40,30,29,36,14,27])). % 116.75/116.77 cnf(180,plain, % 116.75/116.77 (~E(a8,f9(f9(x1801,a1),x1802))), % 116.75/116.77 inference(rename_variables,[],[154])). % 116.75/116.77 cnf(184,plain, % 116.75/116.77 (P3(f4(f9(x1841,a1),x1842,a8),a8)), % 116.75/116.77 inference(scs_inference,[],[150,22,44,175,128,156,77,90,126,154,180,125,39,40,30,29,36,14,27,12,37])). % 116.75/116.77 cnf(186,plain, % 116.75/116.77 (~P3(x1861,f9(x1862,a1))), % 116.75/116.77 inference(rename_variables,[],[44])). % 116.75/116.77 cnf(188,plain, % 116.75/116.77 (P2(f9(a5,a5),f9(a8,a8))), % 116.75/116.77 inference(scs_inference,[],[150,87,22,44,175,128,156,77,90,126,154,180,48,125,39,40,30,29,36,14,27,12,37,15])). % 116.75/116.77 cnf(190,plain, % 116.75/116.77 (~E(f9(a8,a8),f9(x1901,a1))), % 116.75/116.77 inference(scs_inference,[],[150,87,22,44,175,186,128,156,77,90,126,154,180,48,125,39,40,30,29,36,14,27,12,37,15,13])). % 116.75/116.77 cnf(192,plain, % 116.75/116.77 (P3(f4(a7,a8,a8),f9(f9(a8,a8),f9(a8,a8)))), % 116.75/116.77 inference(scs_inference,[],[150,87,22,23,44,175,186,128,156,77,90,126,154,180,48,125,39,40,30,29,36,14,27,12,37,15,13,35])). % 116.75/116.77 cnf(205,plain, % 116.75/116.77 (P3(f4(x2051,a1,f9(a8,a8)),f9(a8,a8))), % 116.75/116.77 inference(scs_inference,[],[135,192,190,42,40,29,39,36])). % 116.75/116.77 cnf(216,plain, % 116.75/116.77 (~E(a7,f9(f9(a1,x2161),x2162))), % 116.75/116.77 inference(scs_inference,[],[25,111,177,105,135,192,190,121,42,128,152,40,29,39,36,14,12,27,15,13])). % 116.75/116.77 cnf(218,plain, % 116.75/116.77 (~E(a7,a8)), % 116.75/116.77 inference(scs_inference,[],[25,111,177,105,135,192,190,121,42,128,152,40,29,39,36,14,12,27,15,13,5])). % 116.75/116.77 cnf(221,plain, % 116.75/116.77 (P3(f4(a7,a8,a5),a7)), % 116.75/116.77 inference(scs_inference,[],[18,25,111,177,123,105,135,192,190,121,42,128,152,40,29,39,36,14,12,27,15,13,5,37,31])). % 116.75/116.77 cnf(224,plain, % 116.75/116.77 (~P3(a7,f4(a7,a8,a5))), % 116.75/116.77 inference(scs_inference,[],[221,29])). % 116.75/116.77 cnf(230,plain, % 116.75/116.77 (P3(f4(x2301,a1,f9(a8,a8)),a8)), % 116.75/116.77 inference(scs_inference,[],[221,23,137,205,29,39,40,33])). % 116.75/116.77 cnf(233,plain, % 116.75/116.77 (P2(a5,f9(a8,a8))), % 116.75/116.77 inference(scs_inference,[],[221,188,22,23,137,205,29,39,40,33,14])). % 116.75/116.77 cnf(234,plain, % 116.75/116.77 (E(f9(x2341,x2341),x2341)), % 116.75/116.77 inference(rename_variables,[],[22])). % 116.75/116.77 cnf(235,plain, % 116.75/116.77 (P3(f4(f9(a1,a1),x2351,a7),a7)), % 116.75/116.77 inference(scs_inference,[],[221,188,22,23,44,137,205,216,29,39,40,33,14,37])). % 116.75/116.77 cnf(237,plain, % 116.75/116.77 (~P3(x2371,f9(x2372,a1))), % 116.75/116.77 inference(rename_variables,[],[44])). % 116.75/116.77 cnf(241,plain, % 116.75/116.77 (~E(a8,f9(x2411,a1))), % 116.75/116.77 inference(scs_inference,[],[25,221,188,22,23,44,237,137,205,216,184,128,29,39,40,33,14,37,12,15,13])). % 116.75/116.77 cnf(243,plain, % 116.75/116.77 (P3(f4(a7,a8,a5),f9(f9(a7,a7),f9(a7,a7)))), % 116.75/116.77 inference(scs_inference,[],[25,221,188,22,234,23,44,237,137,205,216,184,128,29,39,40,33,14,37,12,15,13,35])). % 116.75/116.77 cnf(246,plain, % 116.75/116.77 (~E(a5,a8)), % 116.75/116.77 inference(scs_inference,[],[25,221,188,22,234,23,44,237,137,205,216,184,128,29,39,40,33,14,37,12,15,13,35,8])). % 116.75/116.77 cnf(258,plain, % 116.75/116.77 (P3(f4(a7,a8,a5),f9(a7,a7))), % 116.75/116.77 inference(scs_inference,[],[23,164,243,39,40,29,33])). % 116.75/116.77 cnf(261,plain, % 116.75/116.77 (P3(f4(x2611,a1,a8),a8)), % 116.75/116.77 inference(scs_inference,[],[23,164,42,243,241,39,40,29,33,36])). % 116.75/116.77 cnf(267,plain, % 116.75/116.77 (~E(a7,f9(x2671,f9(a1,x2672)))), % 116.75/116.77 inference(scs_inference,[],[25,139,221,23,109,164,42,243,235,241,128,39,40,29,33,36,14,12,13])). % 116.75/116.77 cnf(276,plain, % 116.75/116.77 (~P3(f9(a7,a7),f4(a7,a8,a5))), % 116.75/116.77 inference(scs_inference,[],[166,258,40,29])). % 116.75/116.77 cnf(280,plain, % 116.75/116.77 (P3(f4(f9(x2801,a1),f9(a1,x2802),a7),a7)), % 116.75/116.77 inference(scs_inference,[],[44,166,258,267,40,29,39,37])). % 116.75/116.77 cnf(282,plain, % 116.75/116.77 (~P3(x2821,f9(x2822,a1))), % 116.75/116.77 inference(rename_variables,[],[44])). % 116.75/116.77 cnf(287,plain, % 116.75/116.77 (~E(f9(a7,a7),f9(x2871,a1))), % 116.75/116.77 inference(scs_inference,[],[25,168,44,282,166,258,267,173,128,40,29,39,37,14,12,13])). % 116.75/116.77 cnf(296,plain, % 116.75/116.77 (~P3(x2961,f9(x2962,a2))), % 116.75/116.77 inference(scs_inference,[],[77,230,29,39])). % 116.75/116.77 cnf(298,plain, % 116.75/116.77 (~P3(x2981,f9(a2,x2982))), % 116.75/116.77 inference(scs_inference,[],[77,230,29,39,40])). % 116.75/116.77 cnf(302,plain, % 116.75/116.77 (P3(f4(x3021,a1,f9(a7,a7)),f9(a7,a7))), % 116.75/116.77 inference(scs_inference,[],[79,190,77,42,287,230,29,39,40,3,36])). % 116.75/116.77 cnf(306,plain, % 116.75/116.77 (~E(a8,f9(x3061,f9(x3062,a1)))), % 116.75/116.77 inference(scs_inference,[],[79,190,71,77,42,96,287,230,29,39,40,3,36,12,13])). % 116.75/116.77 cnf(325,plain, % 116.75/116.77 (P3(f4(x3251,a1,f9(a7,a7)),a7)), % 116.75/116.77 inference(scs_inference,[],[23,276,302,298,30,39,40,29,33])). % 116.75/116.77 cnf(328,plain, % 116.75/116.77 (P3(f4(x3281,f9(x3282,a1),a8),a8)), % 116.75/116.77 inference(scs_inference,[],[23,44,276,302,298,306,30,39,40,29,33,36])). % 116.75/116.77 cnf(330,plain, % 116.75/116.77 (~P3(x3301,f9(x3302,a1))), % 116.75/116.77 inference(rename_variables,[],[44])). % 116.75/116.77 cnf(339,plain, % 116.75/116.77 (~P1(f9(f9(a8,a8),f9(a8,a8)))), % 116.75/116.77 inference(scs_inference,[],[25,23,44,330,164,276,302,298,306,192,115,125,30,39,40,29,33,36,14,12,13,37,27])). % 116.75/116.77 cnf(354,plain, % 116.75/116.77 (~E(a7,f9(f9(x3541,a1),x3542))), % 116.75/116.77 inference(scs_inference,[],[221,73,296,325,328,96,39,40,29,12,13])). % 116.75/116.77 cnf(371,plain, % 116.75/116.77 (~E(a8,f9(f9(a1,x3711),x3712))), % 116.75/116.77 inference(scs_inference,[],[105,224,280,261,128,40,29,39,12,13])). % 116.75/116.77 cnf(376,plain, % 116.75/116.77 (~P3(a7,f4(x3761,a1,a7))), % 116.75/116.77 inference(scs_inference,[],[142,29])). % 116.75/116.77 cnf(378,plain, % 116.75/116.77 (~P3(x3781,f9(x3782,f9(a2,x3783)))), % 116.75/116.77 inference(scs_inference,[],[298,142,29,39])). % 116.75/116.77 cnf(382,plain, % 116.75/116.77 (P3(f4(f9(x3821,a1),x3822,a7),a7)), % 116.75/116.77 inference(scs_inference,[],[44,298,354,142,29,39,40,37])). % 116.75/116.77 cnf(384,plain, % 116.75/116.77 (~P3(x3841,f9(x3842,a1))), % 116.75/116.77 inference(rename_variables,[],[44])). % 116.75/116.77 cnf(387,plain, % 116.75/116.77 (~E(f9(f9(a7,a7),f9(a7,a7)),f9(x3871,a1))), % 116.75/116.77 inference(scs_inference,[],[44,384,298,354,142,98,128,29,39,40,37,12,13])). % 116.75/116.77 cnf(407,plain, % 116.75/116.77 (~E(f9(a7,a7),f9(x4071,f9(a1,x4072)))), % 116.75/116.77 inference(scs_inference,[],[109,387,171,382,56,128,125,39,40,29,27,12,13])). % 116.75/116.77 cnf(409,plain, % 116.75/116.77 (~E(a7,f9(a1,x4091))), % 116.75/116.77 inference(scs_inference,[],[109,387,171,382,56,128,125,39,40,29,27,12,13,5])). % 116.75/116.77 cnf(438,plain, % 116.75/116.77 (P3(f4(a1,x4381,a7),a7)), % 116.75/116.77 inference(scs_inference,[],[42,90,63,409,29,39,40,37])). % 116.75/116.77 cnf(464,plain, % 116.75/116.77 (~P3(a8,f4(x4641,a1,a8))), % 116.75/116.77 inference(scs_inference,[],[261,376,40,29])). % 116.75/116.77 cnf(483,plain, % 116.75/116.77 (~E(f9(a7,a7),f9(f9(a1,x4831),x4832))), % 116.75/116.77 inference(scs_inference,[],[105,83,258,464,128,29,39,40,12,13])). % 116.75/116.77 cnf(499,plain, % 116.75/116.77 (~P3(f4(a8,a7,a7),f9(a8,x4991))), % 116.75/116.77 inference(scs_inference,[],[96,40])). % 116.75/116.77 cnf(503,plain, % 116.75/116.77 (~P3(f4(a8,a7,a7),f9(x5031,a8))), % 116.75/116.77 inference(scs_inference,[],[328,96,40,29,39])). % 116.75/116.77 cnf(519,plain, % 116.75/116.77 (~P3(f4(a8,a7,a7),f9(x5191,f9(x5192,a8)))), % 116.75/116.77 inference(scs_inference,[],[503,39])). % 116.75/116.77 cnf(523,plain, % 116.75/116.77 (~P3(a7,f4(a1,x5231,a7))), % 116.75/116.77 inference(scs_inference,[],[438,503,39,40,29])). % 116.75/116.77 cnf(560,plain, % 116.75/116.77 (~P3(f3(f9(a5,a5),f9(a7,a8)),f9(a7,a8))), % 116.75/116.77 inference(scs_inference,[],[25,22,34,14])). % 116.75/116.77 cnf(685,plain, % 116.75/116.77 (~E(f9(a7,a7),f9(f9(a1,x6851),x6852))), % 116.75/116.77 inference(rename_variables,[],[483])). % 116.75/116.77 cnf(686,plain, % 116.75/116.77 (~P3(x6861,f9(x6862,a2))), % 116.75/116.77 inference(rename_variables,[],[296])). % 116.75/116.77 cnf(688,plain, % 116.75/116.77 (P3(f4(f9(a1,a2),x6881,f9(a7,a7)),f9(a7,a7))), % 116.75/116.77 inference(scs_inference,[],[483,685,296,686,36,37])). % 116.75/116.77 cnf(690,plain, % 116.75/116.77 (~P3(x6901,f9(x6902,a2))), % 116.75/116.77 inference(rename_variables,[],[296])). % 116.75/116.77 cnf(692,plain, % 116.75/116.77 (~E(a7,f9(x6921,a2))), % 116.75/116.77 inference(scs_inference,[],[221,483,685,296,686,690,36,37,13])). % 116.75/116.77 cnf(703,plain, % 116.75/116.77 (P3(f4(x7031,a2,a7),a7)), % 116.75/116.77 inference(scs_inference,[],[77,688,692,29,36])). % 116.75/116.77 cnf(743,plain, % 116.75/116.77 (P3(f4(a8,a7,a5),a7)), % 116.75/116.77 inference(scs_inference,[],[18,123,23,48,44,3,36,13,12,29,31])). % 116.75/116.77 cnf(1329,plain, % 116.75/116.77 (~E(a7,a2)), % 116.75/116.77 inference(scs_inference,[],[692,48,3])). % 116.75/116.77 cnf(1821,plain, % 116.75/116.77 (~P1(f9(a6,a6))), % 116.75/116.77 inference(scs_inference,[],[24,22,11])). % 116.75/116.77 cnf(2197,plain, % 116.75/116.77 (~E(a7,f9(f9(a1,x21971),x21972))), % 116.75/116.77 inference(rename_variables,[],[216])). % 116.75/116.77 cnf(2198,plain, % 116.75/116.77 (~P3(x21981,f9(a1,x21982))), % 116.75/116.77 inference(rename_variables,[],[46])). % 116.75/116.77 cnf(2200,plain, % 116.75/116.77 (P3(f4(f9(a1,x22001),x22002,a7),a7)), % 116.75/116.77 inference(scs_inference,[],[46,2198,216,2197,36,37])). % 116.75/116.77 cnf(2215,plain, % 116.75/116.77 (~E(a8,f9(f9(a1,x22151),x22152))), % 116.75/116.77 inference(rename_variables,[],[371])). % 116.75/116.77 cnf(2216,plain, % 116.75/116.77 (~P3(x22161,f9(a1,x22162))), % 116.75/116.77 inference(rename_variables,[],[46])). % 116.75/116.77 cnf(2218,plain, % 116.75/116.77 (P3(f4(f9(a1,x22181),x22182,a8),a8)), % 116.75/116.77 inference(scs_inference,[],[46,2216,371,2215,2200,29,36,37])). % 116.75/116.77 cnf(2231,plain, % 116.75/116.77 (~E(f9(a7,a7),f9(x22311,f9(a1,x22312)))), % 116.75/116.77 inference(rename_variables,[],[407])). % 116.75/116.77 cnf(2232,plain, % 116.75/116.77 (~P3(x22321,f9(a1,x22322))), % 116.75/116.77 inference(rename_variables,[],[46])). % 116.75/116.77 cnf(2234,plain, % 116.75/116.77 (P3(f4(x22341,f9(a1,x22342),f9(a7,a7)),f9(a7,a7))), % 116.75/116.77 inference(scs_inference,[],[46,2232,407,2231,2218,29,37,36])). % 116.75/116.77 cnf(2246,plain, % 116.75/116.77 (P3(f4(x22461,f9(a1,x22462),a7),a7)), % 116.75/116.77 inference(scs_inference,[],[46,267,2234,29,36])). % 116.75/116.77 cnf(2248,plain, % 116.75/116.77 (~P3(x22481,f9(a1,x22482))), % 116.75/116.77 inference(rename_variables,[],[46])). % 116.75/116.77 cnf(2252,plain, % 116.75/116.77 (~P3(x22521,f9(a1,x22522))), % 116.75/116.77 inference(rename_variables,[],[46])). % 116.75/116.77 cnf(2255,plain, % 116.75/116.77 (~E(a8,f9(a1,x22551))), % 116.75/116.77 inference(scs_inference,[],[46,2248,2252,230,117,267,96,483,2234,29,36,37,12,13])). % 116.75/116.77 cnf(2291,plain, % 116.75/116.77 (P3(f4(a1,x22911,a8),a8)), % 116.75/116.77 inference(scs_inference,[],[42,2246,2255,29,37])). % 116.75/116.77 cnf(2306,plain, % 116.75/116.77 (~P3(a8,f4(a1,x23061,a8))), % 116.75/116.77 inference(scs_inference,[],[2291,29])). % 116.75/116.77 cnf(2421,plain, % 116.75/116.77 (E(f9(a1,x24211),a1)), % 116.75/116.77 inference(scs_inference,[],[152,26])). % 116.75/116.77 cnf(2423,plain, % 116.75/116.77 (~E(a2,a7)), % 116.75/116.77 inference(scs_inference,[],[1329,152,26,2])). % 116.75/116.77 cnf(2425,plain, % 116.75/116.77 (~P3(x24251,a2)), % 116.75/116.77 inference(rename_variables,[],[77])). % 116.75/116.77 cnf(2427,plain, % 116.75/116.77 (~E(a8,f9(x24271,a2))), % 116.75/116.77 inference(scs_inference,[],[1329,152,2291,77,2425,26,2,33,32])). % 116.75/116.77 cnf(2428,plain, % 116.75/116.77 (~P3(x24281,a2)), % 116.75/116.77 inference(rename_variables,[],[77])). % 116.75/116.77 cnf(2430,plain, % 116.75/116.77 (~E(f9(a1,x24301),a7)), % 116.75/116.77 inference(scs_inference,[],[61,1329,152,2291,77,2425,26,2,33,32,11])). % 116.75/116.77 cnf(2431,plain, % 116.75/116.77 (~P3(f4(a7,a8,a8),a5)), % 116.75/116.77 inference(scs_inference,[],[18,61,1329,152,2291,77,2425,128,26,2,33,32,11,31])). % 116.75/116.77 cnf(2435,plain, % 116.75/116.77 (~P2(f9(a5,a5),f9(a7,a8))), % 116.75/116.77 inference(scs_inference,[],[18,61,1329,152,2291,77,2425,25,128,22,26,2,33,32,11,31,41,14])). % 116.75/116.77 cnf(2436,plain, % 116.75/116.77 (E(f9(x24361,x24361),x24361)), % 116.75/116.77 inference(rename_variables,[],[22])). % 116.75/116.77 cnf(2437,plain, % 116.75/116.77 (~P2(a5,f9(a8,a7))), % 116.75/116.77 inference(scs_inference,[],[18,61,1329,152,2291,77,2425,23,25,128,22,26,2,33,32,11,31,41,14,15])). % 116.75/116.77 cnf(2439,plain, % 116.75/116.77 (~P3(f4(a7,a8,a8),f9(a5,a5))), % 116.75/116.77 inference(scs_inference,[],[18,61,1329,152,2291,77,2425,23,25,128,22,2436,26,2,33,32,11,31,41,14,15,13])). % 116.75/116.77 cnf(2440,plain, % 116.75/116.77 (E(f9(x24401,x24401),x24401)), % 116.75/116.77 inference(rename_variables,[],[22])). % 116.75/116.77 cnf(2441,plain, % 116.75/116.77 (~P3(f9(a8,a8),f4(a1,x24411,a8))), % 116.75/116.78 inference(scs_inference,[],[18,61,1329,2306,152,2291,77,2425,23,25,128,22,2436,2440,26,2,33,32,11,31,41,14,15,13,12])). % 116.75/116.78 cnf(2443,plain, % 116.75/116.78 (~E(f9(a2,x24431),f9(a8,a8))), % 116.75/116.78 inference(scs_inference,[],[18,61,1329,2306,152,2291,298,77,2425,23,25,128,22,2436,2440,26,2,33,32,11,31,41,14,15,13,12,35])). % 116.75/116.78 cnf(2444,plain, % 116.75/116.78 (~P3(x24441,f9(a2,x24442))), % 116.75/116.78 inference(rename_variables,[],[298])). % 116.75/116.78 cnf(2446,plain, % 116.75/116.78 (E(f9(a2,x24461),f9(x24462,a2))), % 116.75/116.78 inference(scs_inference,[],[18,61,1329,2306,152,2291,298,2444,77,2425,2428,23,25,128,22,2436,2440,26,2,33,32,11,31,41,14,15,13,12,35,36])). % 116.75/116.78 cnf(2447,plain, % 116.75/116.78 (~P3(x24471,a2)), % 116.75/116.78 inference(rename_variables,[],[77])). % 116.75/116.78 cnf(2448,plain, % 116.75/116.78 (~P3(x24481,f9(a2,x24482))), % 116.75/116.78 inference(rename_variables,[],[298])). % 116.75/116.78 cnf(2454,plain, % 116.75/116.78 (~E(f9(a7,a7),a8)), % 116.75/116.78 inference(scs_inference,[],[18,61,1329,2306,218,152,2291,298,2444,2448,77,2425,2428,2447,48,23,25,128,22,2436,2440,26,2,33,32,11,31,41,14,15,13,12,35,36,37,3])). % 116.75/116.78 cnf(2456,plain, % 116.75/116.78 (E(a2,a1)), % 116.75/116.78 inference(scs_inference,[],[17,26])). % 116.75/116.78 cnf(2458,plain, % 116.75/116.78 (E(f4(x24581,x24582,a2),f4(x24581,x24582,a1))), % 116.75/116.78 inference(scs_inference,[],[17,26,8])). % 116.75/116.78 cnf(2462,plain, % 116.75/116.78 (P2(f4(x24621,x24622,a1),f4(x24621,x24622,a2))), % 116.75/116.78 inference(scs_inference,[],[2443,17,21,703,26,8,2,41,14])). % 116.75/116.78 cnf(2464,plain, % 116.75/116.78 (~P2(f9(a5,a5),f9(a8,a7))), % 116.75/116.78 inference(scs_inference,[],[2443,2435,17,21,703,23,26,8,2,41,14,15])). % 116.75/116.78 cnf(2466,plain, % 116.75/116.78 (~E(f9(x24661,a2),f9(a8,a8))), % 116.75/116.78 inference(scs_inference,[],[2443,2435,2446,17,21,703,23,26,8,2,41,14,15,3])). % 116.75/116.78 cnf(2468,plain, % 116.75/116.78 (~E(f9(a8,x24681),f9(a7,a7))), % 116.75/116.78 inference(scs_inference,[],[2443,2435,2446,17,21,703,499,83,23,26,8,2,41,14,15,3,35])). % 116.75/116.78 cnf(2470,plain, % 116.75/116.78 (E(f3(a2,x24701),f3(a1,x24701))), % 116.75/116.78 inference(scs_inference,[],[2443,2435,2446,17,21,703,499,83,23,26,8,2,41,14,15,3,35,9])). % 116.75/116.78 cnf(2471,plain, % 116.75/116.78 (E(f3(x24711,a2),f3(x24711,a1))), % 116.75/116.78 inference(scs_inference,[],[2443,2435,2446,17,21,703,499,83,23,26,8,2,41,14,15,3,35,9,10])). % 116.75/116.78 cnf(2472,plain, % 116.75/116.78 (E(f4(a2,x24721,x24722),f4(a1,x24721,x24722))), % 116.75/116.78 inference(scs_inference,[],[2443,2435,2446,17,21,703,499,83,23,26,8,2,41,14,15,3,35,9,10,6])). % 116.75/116.78 cnf(2473,plain, % 116.75/116.78 (E(f4(x24731,a2,x24732),f4(x24731,a1,x24732))), % 116.75/116.78 inference(scs_inference,[],[2443,2435,2446,17,21,703,499,83,23,26,8,2,41,14,15,3,35,9,10,6,7])). % 116.75/116.78 cnf(2474,plain, % 116.75/116.78 (E(f9(a2,x24741),f9(a1,x24741))), % 116.75/116.78 inference(scs_inference,[],[2443,2435,2446,17,21,703,499,83,23,26,8,2,41,14,15,3,35,9,10,6,7,4])). % 116.75/116.78 cnf(2478,plain, % 116.75/116.78 (~P3(x24781,f4(x24782,x24783,a2))+P3(x24781,f4(x24782,x24783,a1))), % 116.75/116.78 inference(scs_inference,[],[2443,2435,2446,17,21,703,499,83,23,26,8,2,41,14,15,3,35,9,10,6,7,4,5,29,13])). % 116.75/116.78 cnf(2485,plain, % 116.75/116.78 (~E(a1,a7)), % 116.75/116.78 inference(scs_inference,[],[2423,2456,2466,438,2,41,3])). % 116.75/116.78 cnf(2486,plain, % 116.75/116.78 (~P3(f9(a8,a8),f4(a2,x24861,a8))), % 116.75/116.78 inference(scs_inference,[],[2423,2456,2466,2472,2441,438,2,41,3,13])). % 116.75/116.78 cnf(2488,plain, % 116.75/116.78 (E(f4(a2,x24881,x24882),f4(a1,x24881,x24882))), % 116.75/116.78 inference(rename_variables,[],[2472])). % 116.75/116.78 cnf(2489,plain, % 116.75/116.78 (~E(f9(a2,x24891),f9(a7,a7))), % 116.75/116.78 inference(scs_inference,[],[2423,2456,2466,2472,2441,438,298,2,41,3,13,35])). % 116.75/116.78 cnf(2492,plain, % 116.75/116.78 (~P3(f9(a7,a7),f4(a1,x24921,a7))), % 116.75/116.78 inference(scs_inference,[],[2423,2456,2466,2472,2441,438,298,2,41,3,13,35,29])). % 116.75/116.78 cnf(2494,plain, % 116.75/116.78 (P2(f4(a1,x24941,a1),f4(a2,x24941,a2))), % 116.75/116.78 inference(scs_inference,[],[2423,2456,2466,2462,2472,2488,2441,438,298,2,41,3,13,35,29,14])). % 116.75/116.78 cnf(2495,plain, % 116.75/116.78 (E(f4(a2,x24951,x24952),f4(a1,x24951,x24952))), % 116.75/116.78 inference(rename_variables,[],[2472])). % 116.75/116.78 cnf(2496,plain, % 116.75/116.78 (P2(f4(x24961,x24962,a1),f4(x24961,x24962,a2))), % 116.75/116.78 inference(rename_variables,[],[2462])). % 116.75/116.78 cnf(2497,plain, % 116.75/116.78 (P2(f4(a2,x24971,a1),f4(a1,x24971,a2))), % 116.75/116.78 inference(scs_inference,[],[2423,2456,2466,2462,2496,2472,2488,2495,2441,438,298,2,41,3,13,35,29,14,15])). % 116.75/116.78 cnf(2501,plain, % 116.75/116.78 (P3(f4(x25011,a1,a7),f9(a7,a7))), % 116.75/116.78 inference(scs_inference,[],[2468,142,2,41])). % 116.75/116.78 cnf(2503,plain, % 116.75/116.78 (E(f4(x25031,a2,a2),f4(x25031,a1,a1))), % 116.75/116.78 inference(scs_inference,[],[2468,2458,2473,142,2,41,3])). % 116.75/116.78 cnf(2506,plain, % 116.75/116.78 (~E(f9(x25061,a2),f9(a7,a7))), % 116.75/116.78 inference(scs_inference,[],[2468,2458,2473,142,296,2,41,3,35])). % 116.75/116.78 cnf(2511,plain, % 116.75/116.78 (~P3(x25111,f3(a2,x25112))+P3(x25111,f3(a1,x25112))), % 116.75/116.78 inference(scs_inference,[],[2468,2458,2473,2470,142,296,2,41,3,35,29,13])). % 116.75/116.78 cnf(2512,plain, % 116.75/116.78 (~P3(x25121,f3(a2,x25122))+~P1(f3(a1,x25122))), % 116.75/116.78 inference(scs_inference,[],[2468,2458,2473,2470,142,296,2,41,3,35,29,13,28])). % 116.75/116.78 cnf(2517,plain, % 116.75/116.78 (~E(f9(a1,x25171),f9(a7,a7))), % 116.75/116.78 inference(scs_inference,[],[2489,2474,261,2,41,3])). % 116.75/116.78 cnf(2522,plain, % 116.75/116.78 (~E(f9(x25221,a8),f9(a7,a7))), % 116.75/116.78 inference(scs_inference,[],[2489,2474,2473,464,503,261,83,2,41,3,13,35])). % 116.75/116.78 cnf(2526,plain, % 116.75/116.78 (~E(f9(a8,a8),f9(x25261,a5))), % 116.75/116.78 inference(scs_inference,[],[2489,2431,2474,2473,464,503,261,156,83,2,41,3,13,35,29,32])). % 116.75/116.78 cnf(2528,plain, % 116.75/116.78 (~E(f9(a8,a8),f9(a5,x25281))), % 116.75/116.78 inference(scs_inference,[],[2489,2431,2474,2473,464,503,261,156,83,2,41,3,13,35,29,32,33])). % 116.75/116.78 cnf(2530,plain, % 116.75/116.78 (~P3(x25301,f4(a1,x25302,a1))+P3(x25301,f4(a2,x25302,a2))), % 116.75/116.78 inference(scs_inference,[],[2489,2494,2431,2474,2473,464,503,261,156,83,2,41,3,13,35,29,32,33,31])). % 116.75/116.78 cnf(2532,plain, % 116.75/116.78 (E(f9(a2,x25321),f9(a1,x25322))), % 116.75/116.78 inference(scs_inference,[],[2489,2494,2431,2474,2473,464,503,261,156,298,83,42,2,41,3,13,35,29,32,33,31,37])). % 116.75/116.78 cnf(2533,plain, % 116.75/116.78 (~P3(x25331,a1)), % 116.75/116.78 inference(rename_variables,[],[42])). % 116.75/116.78 cnf(2534,plain, % 116.75/116.78 (~P3(x25341,f9(a2,x25342))), % 116.75/116.78 inference(rename_variables,[],[298])). % 116.75/116.78 cnf(2542,plain, % 116.75/116.78 (~P3(x25421,f4(a1,x25422,a1))+~P1(f4(a2,x25422,a2))), % 116.75/116.78 inference(scs_inference,[],[2489,2494,2486,2431,2474,2473,464,503,261,156,298,2534,83,48,42,2533,2,41,3,13,35,29,32,33,31,37,36,12,28])). % 116.75/116.78 cnf(2546,plain, % 116.75/116.78 (~P3(x25461,a2)), % 116.75/116.78 inference(rename_variables,[],[77])). % 116.75/116.78 cnf(2550,plain, % 116.75/116.78 (E(a2,f9(a2,x25501))), % 116.75/116.78 inference(scs_inference,[],[2506,703,77,2546,743,2,33,41,37])). % 116.75/116.78 cnf(2552,plain, % 116.75/116.78 (~P3(x25521,a2)), % 116.75/116.78 inference(rename_variables,[],[77])). % 116.75/116.78 cnf(2554,plain, % 116.75/116.78 (E(a2,f9(x25541,a2))), % 116.75/116.78 inference(scs_inference,[],[2506,703,77,2546,2552,743,2,33,41,37,36])). % 116.75/116.78 cnf(2571,plain, % 116.75/116.78 (P3(f4(a8,a7,a7),f9(a7,a7))), % 116.75/116.78 inference(scs_inference,[],[2522,2431,117,83,2,33,41])). % 116.75/116.78 cnf(2573,plain, % 116.75/116.78 (E(f9(x25731,a2),f9(a2,x25732))), % 116.75/116.78 inference(scs_inference,[],[2522,2431,296,117,77,83,2,33,41,37])). % 116.75/116.78 cnf(2574,plain, % 116.75/116.78 (~P3(x25741,a2)), % 116.75/116.78 inference(rename_variables,[],[77])). % 116.75/116.78 cnf(2575,plain, % 116.75/116.78 (~P3(x25751,f9(x25752,a2))), % 116.75/116.78 inference(rename_variables,[],[296])). % 116.75/116.78 cnf(2577,plain, % 116.75/116.78 (E(f9(x25771,a2),f9(x25772,a2))), % 116.75/116.78 inference(scs_inference,[],[2522,2431,296,2575,117,77,2574,83,2,33,41,37,36])). % 116.75/116.78 cnf(2590,plain, % 116.75/116.78 (P2(f4(x25901,a1,a1),f4(x25901,a2,a2))), % 116.75/116.78 inference(scs_inference,[],[2522,2503,2492,2439,246,2472,2431,21,296,2575,117,77,2574,83,48,2,33,41,37,36,3,13,35,29,14])). % 116.75/116.78 cnf(2592,plain, % 116.75/116.78 (P2(f4(a2,a2,a1),f4(a1,a1,a1))), % 116.75/116.78 inference(scs_inference,[],[2522,2497,2503,2492,2439,246,2472,2431,21,296,2575,117,77,2574,83,48,2,33,41,37,36,3,13,35,29,14,15])). % 116.75/116.78 cnf(2595,plain, % 116.75/116.78 (~E(f9(x25951,a5),f9(a8,a8))), % 116.75/116.78 inference(scs_inference,[],[2526,2])). % 116.75/116.78 cnf(2596,plain, % 116.75/116.78 (E(f3(a2,a2),f3(a1,a1))), % 116.75/116.78 inference(scs_inference,[],[2526,2471,2470,2,3])). % 116.75/116.78 cnf(2597,plain, % 116.75/116.78 (E(f3(x25971,a2),f3(x25971,a1))), % 116.75/116.78 inference(rename_variables,[],[2471])). % 116.75/116.78 cnf(2605,plain, % 116.75/116.78 (~P3(f3(a2,a1),f3(a2,a2))), % 116.75/116.78 inference(scs_inference,[],[2526,2471,2597,2470,2,3,13,2512,2511,29])). % 116.75/116.78 cnf(2610,plain, % 116.75/116.78 (~P3(f3(a2,a2),f3(a2,a2))), % 116.75/116.78 inference(scs_inference,[],[2605,2528,2595,2532,2471,2,3,12])). % 116.75/116.78 cnf(2615,plain, % 116.75/116.78 (~E(f9(a8,a8),f9(x26151,a7))), % 116.75/116.78 inference(scs_inference,[],[2605,2528,2595,2532,2471,2472,523,156,128,2,3,12,13,32])). % 116.75/116.78 cnf(2617,plain, % 116.75/116.78 (~P3(x26171,f4(a2,a2,a1))+P3(x26171,f4(a1,a1,a1))), % 116.75/116.78 inference(scs_inference,[],[2605,2528,2595,2592,2532,2471,2472,523,156,128,2,3,12,13,32,31])). % 116.75/116.78 cnf(2621,plain, % 116.75/116.78 (~P3(x26211,f4(a2,a2,a1))+P3(x26211,f4(a2,a1,a2))), % 116.75/116.78 inference(scs_inference,[],[2605,2528,2595,2592,2532,2471,2472,523,156,128,2,3,12,13,32,31,2542,2530])). % 116.75/116.78 cnf(2625,plain, % 116.75/116.78 (~P3(f4(a1,a1,a1),f4(a2,a2,a1))), % 116.75/116.78 inference(scs_inference,[],[2605,2528,2595,2592,2532,2471,2472,523,156,128,2,3,12,13,32,31,2542,2530,29])). % 116.75/116.78 cnf(2629,plain, % 116.75/116.78 (~P3(f4(a1,a1,a2),f4(a2,a2,a1))), % 116.75/116.78 inference(scs_inference,[],[2625,2517,2615,2421,2458,2,3,12])). % 116.75/116.78 cnf(2630,plain, % 116.75/116.78 (E(f4(x26301,x26302,a2),f4(x26301,x26302,a1))), % 116.75/116.78 inference(rename_variables,[],[2458])). % 116.75/116.78 cnf(2631,plain, % 116.75/116.78 (~P3(f4(a1,a1,a1),f4(a2,a2,a2))), % 116.75/116.78 inference(scs_inference,[],[2625,2517,2615,2421,2458,2630,2,3,12,13])). % 116.75/116.78 cnf(2633,plain, % 116.75/116.78 (~P3(f4(a1,a1,a2),f4(a2,a2,a2))), % 116.75/116.78 inference(scs_inference,[],[2625,2517,2615,2421,2458,2630,2,3,12,13,2478])). % 116.75/116.78 cnf(2634,plain, % 116.75/116.78 (~P3(f4(a1,a1,a1),f4(a1,a2,a1))), % 116.75/116.78 inference(scs_inference,[],[2625,2517,2615,2421,2458,2630,2,3,12,13,2478,2530])). % 116.75/116.78 cnf(2636,plain, % 116.75/116.78 (~P3(f4(a1,a1,a1),f4(a2,a1,a1))), % 116.75/116.78 inference(scs_inference,[],[2625,2517,2615,2590,2421,2458,2630,2,3,12,13,2478,2530,31])). % 116.75/116.78 cnf(2641,plain, % 116.75/116.78 (~E(f9(a2,x26411),a7)), % 116.75/116.78 inference(scs_inference,[],[2454,2430,2573,2,3])). % 116.75/116.78 cnf(2644,plain, % 116.75/116.78 (~P3(f4(a7,a8,a7),a5)), % 116.75/116.78 inference(scs_inference,[],[19,2454,2430,2573,59,2,3,31])). % 116.75/116.78 cnf(2646,plain, % 116.75/116.78 (~P3(f4(a1,a1,a1),f4(a2,a1,a2))), % 116.75/116.78 inference(scs_inference,[],[19,2636,2454,2430,2573,2458,59,2,3,31,13])). % 116.75/116.78 cnf(2648,plain, % 116.75/116.78 (~P3(f4(a1,a2,a2),f4(a2,a2,a2))), % 116.75/116.78 inference(scs_inference,[],[19,2631,2636,2454,2430,2573,2458,2503,59,2,3,31,13,12])). % 116.75/116.78 cnf(2650,plain, % 116.75/116.78 (P2(f3(a1,a1),f3(a2,a2))), % 116.75/116.78 inference(scs_inference,[],[19,2631,2636,2454,2596,2430,2573,2458,2503,21,59,2,3,31,13,12,14])). % 116.75/116.78 cnf(2652,plain, % 116.75/116.78 (~E(f9(a8,a8),f9(a7,x26521))), % 116.75/116.78 inference(scs_inference,[],[19,2631,2636,2454,2596,2430,2573,2458,2503,21,156,59,128,2,3,31,13,12,14,33])). % 116.75/116.78 cnf(2654,plain, % 116.75/116.78 (~P3(f4(a1,a1,a2),f4(a1,a2,a1))), % 116.75/116.78 inference(scs_inference,[],[19,2633,2631,2636,2454,2596,2430,2573,2458,2503,21,156,59,128,2,3,31,13,12,14,33,2530])). % 116.75/116.78 cnf(2657,plain, % 116.75/116.78 (E(f4(a2,a2,a2),f4(a1,a1,a1))), % 116.75/116.78 inference(scs_inference,[],[2652,2503,2472,2,3])). % 116.75/116.78 cnf(2661,plain, % 116.75/116.78 (E(f3(a2,x26611),f3(a1,x26611))), % 116.75/116.78 inference(rename_variables,[],[2470])). % 116.75/116.78 cnf(2662,plain, % 116.75/116.78 (~E(f9(a7,a7),f9(x26621,a5))), % 116.75/116.78 inference(scs_inference,[],[2650,2644,2652,2470,2503,2472,56,2,3,15,32])). % 116.75/116.78 cnf(2664,plain, % 116.75/116.78 (~E(f9(a7,a7),f9(a5,x26641))), % 116.75/116.78 inference(scs_inference,[],[2650,2644,2652,2470,2503,2472,56,2,3,15,32,33])). % 116.75/116.78 cnf(2670,plain, % 116.75/116.78 (~P3(f4(a1,a2,a2),f4(a1,a2,a1))), % 116.75/116.78 inference(scs_inference,[],[2650,2654,2644,2652,2610,2470,2661,2473,2503,2472,56,2,3,15,32,33,31,13,12])). % 116.75/116.78 cnf(2672,plain, % 116.75/116.78 (~E(a5,f9(a8,a8))), % 116.75/116.78 inference(scs_inference,[],[2650,2654,2644,2652,2610,2470,2661,2473,2503,2431,2472,56,117,2,3,15,32,33,31,13,12,35])). % 116.75/116.78 cnf(2679,plain, % 116.75/116.78 (~E(a7,f9(x26791,a5))), % 116.75/116.78 inference(scs_inference,[],[2662,2641,2577,2644,51,2,3,32])). % 116.75/116.78 cnf(2681,plain, % 116.75/116.78 (~E(a7,f9(a5,x26811))), % 116.75/116.78 inference(scs_inference,[],[2662,2641,2577,2644,51,2,3,32,33])). % 116.75/116.78 cnf(2683,plain, % 116.75/116.78 (~P3(f4(a8,a7,a7),a5)), % 116.75/116.78 inference(scs_inference,[],[19,2662,2641,2577,2644,51,96,2,3,32,33,31])). % 116.75/116.78 cnf(2685,plain, % 116.75/116.78 (~P3(f4(a1,a2,a2),f4(a1,a2,a2))), % 116.75/116.78 inference(scs_inference,[],[19,2670,2662,2641,2577,2644,2458,51,96,2,3,32,33,31,13])). % 116.75/116.78 cnf(2688,plain, % 116.75/116.78 (~E(a5,f9(a7,a7))), % 116.75/116.78 inference(scs_inference,[],[19,2657,2670,2646,2662,2641,2577,2644,2458,51,96,2,3,32,33,31,13,12,35])). % 116.75/116.78 cnf(2690,plain, % 116.75/116.78 (~P3(f4(a2,a2,a2),f4(a2,a2,a1))), % 116.75/116.78 inference(scs_inference,[],[19,2657,2670,2646,2662,2641,2577,2644,2458,51,96,2,3,32,33,31,13,12,35,2621])). % 116.75/116.78 cnf(2694,plain, % 116.75/116.78 (~P3(f4(a2,a2,a2),f4(a2,a2,a2))), % 116.75/116.78 inference(scs_inference,[],[2485,2690,2664,2458,79,2,3,13])). % 116.75/116.78 cnf(2698,plain, % 116.75/116.78 (~P3(f4(a1,a1,a1),f4(a1,a2,a2))), % 116.75/116.78 inference(scs_inference,[],[2485,2685,2690,2664,2634,2458,2472,79,2,3,13,12,2478])). % 116.75/116.78 cnf(2700,plain, % 116.75/116.78 (~E(f9(a8,a8),a7)), % 116.75/116.78 inference(scs_inference,[],[2688,159,48,2,3])). % 116.75/116.78 cnf(2704,plain, % 116.75/116.78 (~P3(f4(a1,a2,a1),f4(a1,a2,a2))), % 116.75/116.78 inference(scs_inference,[],[2698,2683,2688,159,2473,48,22,2,3,13,12])). % 116.75/116.78 cnf(2708,plain, % 116.75/116.78 (P2(f4(a1,a1,a1),f4(a2,a2,a2))), % 116.75/116.78 inference(scs_inference,[],[2694,2698,2683,2688,159,2657,2473,21,48,22,2,3,13,12,2530,14])). % 116.75/116.78 cnf(2710,plain, % 116.75/116.78 (~E(a2,a8)), % 116.75/116.78 inference(scs_inference,[],[179,2694,2698,2683,2688,159,2657,17,2473,21,48,22,2,3,13,12,2530,14,11])). % 116.75/116.78 cnf(2711,plain, % 116.75/116.78 (~E(a8,a2)), % 116.75/116.78 inference(scs_inference,[],[2710,2])). % 116.75/116.78 cnf(2713,plain, % 116.75/116.78 (~P3(f4(a1,a2,a2),f4(a1,a1,a1))), % 116.75/116.78 inference(scs_inference,[],[2710,2708,2648,2550,2,3,31])). % 116.75/116.78 cnf(2717,plain, % 116.75/116.78 (P2(f4(a1,a1,a1),f4(a2,a1,a1))), % 116.75/116.78 inference(scs_inference,[],[2710,2708,2648,2629,2550,2503,2473,2,3,31,12,15])). % 116.75/116.78 cnf(2720,plain, % 116.75/116.78 (~E(f9(a8,a8),a2)), % 116.75/116.78 inference(scs_inference,[],[2711,2672,48,2,3])). % 116.75/116.78 cnf(2722,plain, % 116.75/116.78 (~P3(f4(a1,a1,a1),f4(a1,a1,a1))), % 116.75/116.78 inference(scs_inference,[],[2711,2717,2672,2636,48,2,3,31])). % 116.75/116.78 cnf(2724,plain, % 116.75/116.78 (~P3(f4(a2,a2,a2),f4(a1,a1,a1))), % 116.75/116.78 inference(scs_inference,[],[2711,2713,2717,2672,2636,2472,48,2,3,31,12])). % 116.75/116.78 cnf(2730,plain, % 116.75/116.78 (~P3(f4(a1,a1,a1),f4(a1,a1,a2))), % 116.75/116.78 inference(scs_inference,[],[2724,2722,2700,2657,2636,2458,2,13,12,2478])). % 116.75/116.78 cnf(2734,plain, % 116.75/116.78 (~P3(f4(a1,a2,a1),f4(a2,a2,a2))), % 116.75/116.78 inference(scs_inference,[],[2720,2704,87,2472,59,2,31,13])). % 116.75/116.78 cnf(2736,plain, % 116.75/116.78 (~P3(f4(a1,a2,a2),f4(a1,a1,a2))), % 116.75/116.78 inference(scs_inference,[],[2730,2720,2704,87,2503,2472,59,2,31,13,12])). % 116.75/116.78 cnf(2740,plain, % 116.75/116.78 (P2(f3(x27401,a1),f3(x27401,a2))), % 116.75/116.78 inference(scs_inference,[],[2730,2720,2704,87,2471,2503,21,2472,59,2,31,13,12,2530,14])). % 116.75/116.78 cnf(2742,plain, % 116.75/116.78 (~E(f9(a1,x27421),f9(a6,a6))), % 116.75/116.78 inference(scs_inference,[],[2730,1821,2720,2704,87,2471,152,2503,21,2472,59,2,31,13,12,2530,14,11])). % 116.75/116.78 cnf(2744,plain, % 116.75/116.78 (~P3(f3(a2,a1),f3(a2,a1))), % 116.75/116.78 inference(scs_inference,[],[2742,2740,2605,2,31])). % 116.75/116.78 cnf(2747,plain, % 116.75/116.78 (~P3(f4(a1,a2,a2),f4(a2,a1,a2))), % 116.75/116.78 inference(scs_inference,[],[2736,2742,2740,2605,2472,2,31,13])). % 116.75/116.78 cnf(2755,plain, % 116.75/116.78 (~P3(f4(a1,a1,a2),f4(a1,a2,a2))), % 116.75/116.78 inference(scs_inference,[],[2747,2427,2462,2654,2458,2,31,13])). % 116.75/116.78 cnf(2761,plain, % 116.75/116.78 (~P3(f4(a2,a1,a2),f4(a1,a2,a2))), % 116.75/116.78 inference(scs_inference,[],[2679,2755,2472,2,12])). % 116.75/116.78 cnf(2762,plain, % 116.75/116.78 (E(f4(a2,x27621,x27622),f4(a1,x27621,x27622))), % 116.75/116.78 inference(rename_variables,[],[2472])). % 116.75/116.78 cnf(2763,plain, % 116.75/116.78 (P2(f4(a2,a1,a1),f4(a1,a1,a1))), % 116.75/116.78 inference(scs_inference,[],[2679,2755,2592,2473,2472,2,12,14])). % 116.75/116.78 cnf(2765,plain, % 116.75/116.78 (~E(a2,a6)), % 116.75/116.78 inference(scs_inference,[],[2679,2755,24,2592,17,2473,2472,2,12,14,11])). % 116.75/116.78 cnf(2766,plain, % 116.75/116.78 (~P3(f4(a2,a1,a2),f4(a2,a2,a2))), % 116.75/116.78 inference(scs_inference,[],[2679,2755,24,2592,17,2473,2472,2762,2,12,14,11,13])). % 116.75/116.78 cnf(2768,plain, % 116.75/116.78 (~P3(f4(a2,a1,a2),f4(a1,a2,a1))), % 116.75/116.78 inference(scs_inference,[],[2766,2530])). % 116.75/116.78 cnf(2770,plain, % 116.75/116.78 (~E(a6,a2)), % 116.75/116.78 inference(scs_inference,[],[2765,2766,2530,2])). % 116.75/116.78 cnf(2771,plain, % 116.75/116.78 (~E(f9(x27711,a2),a6)), % 116.75/116.78 inference(scs_inference,[],[2765,2766,2554,2530,2,3])). % 116.75/116.78 cnf(2773,plain, % 116.75/116.78 (~P3(f4(a2,a1,a2),f4(a2,a2,a1))), % 116.75/116.78 inference(scs_inference,[],[2768,2681,2472,2,13])). % 116.75/116.78 cnf(2775,plain, % 116.75/116.78 (~E(f9(a6,a6),a2)), % 116.75/116.78 inference(scs_inference,[],[2770,2768,2681,2472,48,2,13,3])). % 116.75/116.78 cnf(2777,plain, % 116.75/116.78 (~P3(f4(a2,a1,a2),f4(a1,a1,a1))), % 116.75/116.78 inference(scs_inference,[],[2770,2768,2681,2761,2590,2472,48,2,13,3,31])). % 116.75/116.78 cnf(2782,plain, % 116.75/116.78 (~E(a2,f9(a6,a6))), % 116.75/116.78 inference(scs_inference,[],[2775,2])). % 116.75/116.78 cnf(2783,plain, % 116.75/116.78 (~P3(f4(a2,a1,a2),f4(a2,a1,a1))), % 116.75/116.78 inference(scs_inference,[],[2777,2763,2775,2,31])). % 116.75/116.78 cnf(2786,plain, % 116.75/116.78 (~P3(f4(a1,a2,a1),f4(a1,a1,a1))), % 116.75/116.78 inference(scs_inference,[],[2771,2734,2708,2,31])). % 116.75/116.78 cnf(2792,plain, % 116.75/116.78 (~E(f9(a2,x27921),f9(a6,a6))), % 116.75/116.78 inference(scs_inference,[],[2783,2782,2771,2734,2550,2708,2458,2,31,2617,13,3])). % 116.75/116.78 cnf(2795,plain, % 116.75/116.78 (~P3(f4(a2,a2,a1),f4(a1,a1,a1))), % 116.75/116.78 inference(scs_inference,[],[2786,2792,2472,2,12])). % 116.75/116.78 cnf(2912,plain, % 116.75/116.78 (~P3(x29121,a1)), % 116.75/116.78 inference(rename_variables,[],[42])). % 116.75/116.78 cnf(2914,plain, % 116.75/116.78 (E(a1,f9(x29141,a2))), % 116.75/116.78 inference(scs_inference,[],[42,2912,77,37,36])). % 116.75/116.78 cnf(2919,plain, % 116.75/116.78 (E(f9(x29191,a2),f9(a1,x29192))), % 116.75/116.78 inference(scs_inference,[],[42,296,37])). % 116.75/116.78 cnf(2928,plain, % 116.75/116.78 (E(a2,f9(a1,x29281))), % 116.75/116.78 inference(scs_inference,[],[42,77,37])). % 116.75/116.78 cnf(2942,plain, % 116.75/116.78 (E(f9(a1,x29421),f9(a1,x29422))), % 116.75/116.78 inference(scs_inference,[],[42,46,37])). % 116.75/116.78 cnf(2958,plain, % 116.75/116.78 (E(f9(a1,x29581),f9(a2,x29582))), % 116.75/116.78 inference(scs_inference,[],[46,77,37])). % 116.75/116.78 cnf(2985,plain, % 116.75/116.78 (E(f9(f9(a1,x29851),x29852),f9(a1,x29852))), % 116.75/116.78 inference(scs_inference,[],[152,26,4])). % 116.75/116.78 cnf(2987,plain, % 116.75/116.78 (E(a1,a2)), % 116.75/116.78 inference(scs_inference,[],[17,26,2])). % 116.75/116.78 cnf(2991,plain, % 116.75/116.78 (E(f3(x29911,a1),f3(x29911,a2))), % 116.75/116.78 inference(scs_inference,[],[2987,6,9,7,10])). % 116.75/116.78 cnf(2992,plain, % 116.75/116.78 (E(f4(x29921,x29922,a1),f4(x29921,x29922,a2))), % 116.75/116.78 inference(scs_inference,[],[2987,6,9,7,10,8])). % 116.75/116.78 cnf(3099,plain, % 116.75/116.78 (E(f4(x30991,f9(x30992,a2),x30993),f4(x30991,a1,x30993))), % 116.75/116.78 inference(scs_inference,[],[2914,2,7])). % 116.75/116.78 cnf(3102,plain, % 116.75/116.78 (E(f4(x31021,x31022,f9(a1,x31023)),f4(x31021,x31022,a2))), % 116.75/116.78 inference(scs_inference,[],[2928,2,8])). % 116.75/116.78 cnf(3108,plain, % 116.75/116.78 (E(f3(a2,a1),f3(a1,a2))), % 116.75/116.78 inference(scs_inference,[],[2991,2470,3])). % 116.75/116.78 cnf(3113,plain, % 116.75/116.78 (E(f9(f3(a1,a2),x31131),f9(f3(a2,a1),x31131))), % 116.75/116.78 inference(scs_inference,[],[3108,2,4])). % 116.75/116.78 cnf(3183,plain, % 116.75/116.78 (~P3(f9(f9(a7,a7),f9(a7,a7)),f4(a8,a7,a7))), % 116.75/116.78 inference(scs_inference,[],[2571,29,41])). % 116.75/116.78 cnf(3223,plain, % 116.75/116.78 (~E(f3(a5,f9(a8,a7)),f4(a8,a7,a7))), % 116.75/116.78 inference(scs_inference,[],[2437,2683,30,12])). % 116.75/116.78 cnf(3224,plain, % 116.75/116.78 (P3(f3(a5,f9(a8,a7)),f9(a5,a5))), % 116.75/116.78 inference(scs_inference,[],[2437,48,30,13])). % 116.75/116.78 cnf(3226,plain, % 116.75/116.78 (P2(f4(a1,x32261,a2),f4(a2,x32261,a2))), % 116.75/116.78 inference(scs_inference,[],[2494,2992,14])). % 116.75/116.78 cnf(3230,plain, % 116.75/116.78 (P3(f3(f9(a5,a5),f9(a7,a8)),f9(f9(a5,a5),f9(a5,a5)))), % 116.75/116.78 inference(scs_inference,[],[2435,30,41])). % 116.75/116.78 cnf(3233,plain, % 116.75/116.78 (P3(f3(a5,f9(a8,a7)),f9(a8,a8))), % 116.75/116.78 inference(scs_inference,[],[2437,233,30,31])). % 116.75/116.78 cnf(3237,plain, % 116.75/116.78 (~P2(a5,a2)), % 116.75/116.78 inference(scs_inference,[],[2437,77,30,31])). % 116.75/116.78 cnf(3244,plain, % 116.75/116.78 (~P2(a5,a1)), % 116.75/116.78 inference(scs_inference,[],[3237,2987,22,30,41,14,15])). % 116.75/116.78 cnf(3258,plain, % 116.75/116.78 (~P2(a5,f9(x32581,a1))), % 116.75/116.78 inference(scs_inference,[],[3244,20,22,30,41,14,15])). % 116.75/116.78 cnf(3262,plain, % 116.75/116.78 (~P2(f9(a5,a5),f9(x32621,a1))), % 116.75/116.78 inference(scs_inference,[],[3258,22,14])). % 116.75/116.78 cnf(3267,plain, % 116.75/116.78 (~P2(f9(a5,a5),f9(x32671,a2))), % 116.75/116.78 inference(scs_inference,[],[3262,2919,15])). % 116.75/116.78 cnf(3272,plain, % 116.75/116.78 (~P2(f9(a5,a5),f9(x32721,a2))), % 116.75/116.78 inference(rename_variables,[],[3267])). % 116.75/116.78 cnf(3274,plain, % 116.75/116.78 (~P2(a5,f9(x32741,a2))), % 116.75/116.78 inference(scs_inference,[],[3267,3272,2942,48,15,14])). % 116.75/116.78 cnf(3277,plain, % 116.75/116.78 (~P2(a5,f9(a1,x32771))), % 116.75/116.78 inference(scs_inference,[],[3274,2958,15])). % 116.75/116.78 cnf(3301,plain, % 116.75/116.78 (P3(f3(a5,a2),f9(a7,a7))), % 116.75/116.78 inference(scs_inference,[],[3237,177,30,31])). % 116.75/116.78 cnf(3431,plain, % 116.75/116.78 (P3(f3(a5,f9(a8,a7)),a5)), % 116.75/116.78 inference(scs_inference,[],[3224,2464,34,39])). % 116.75/116.78 cnf(3438,plain, % 116.75/116.78 (E(f9(x34381,f4(x34382,f9(x34383,a2),x34384)),f9(x34381,f4(x34382,a1,x34384)))), % 116.75/116.78 inference(scs_inference,[],[3224,3099,2464,34,39,6,7,9,4,10,5])). % 116.75/116.78 cnf(3446,plain, % 116.75/116.78 (P3(f3(a5,f9(a8,a7)),a8)), % 116.75/116.78 inference(scs_inference,[],[3224,3233,3099,3230,3277,2464,34,39,6,7,9,4,10,5,29,8,30,28,40])). % 116.75/116.78 cnf(3451,plain, % 116.75/116.78 (~P3(x34511,f9(x34512,f9(a2,x34513)))), % 116.75/116.78 inference(rename_variables,[],[378])). % 116.75/116.78 cnf(3457,plain, % 116.75/116.78 (E(f4(x34571,f9(x34572,a2),x34573),f4(x34571,a1,x34573))), % 116.75/116.78 inference(rename_variables,[],[3099])). % 116.75/116.78 cnf(3459,plain, % 116.75/116.78 (E(f4(x34591,f9(x34592,a2),x34593),f4(x34591,a1,x34593))), % 116.75/116.78 inference(rename_variables,[],[3099])). % 116.75/116.78 cnf(3462,plain, % 116.75/116.78 (~P3(x34621,f9(x34622,f9(a2,x34623)))), % 116.75/116.78 inference(rename_variables,[],[378])). % 116.75/116.78 cnf(3464,plain, % 116.75/116.78 (~E(f9(a7,a7),f9(f9(x34641,f9(a2,x34642)),x34643))), % 116.75/116.78 inference(scs_inference,[],[2501,3223,3224,3233,3099,3457,3102,3230,2773,378,3451,3462,3277,2464,34,39,6,7,9,4,10,5,29,8,30,28,40,2,37,41,3,12,36,33])). % 116.75/116.78 cnf(3467,plain, % 116.75/116.78 (~E(f9(a7,a7),f9(x34671,f9(x34672,f9(x34673,a8))))), % 116.75/116.78 inference(scs_inference,[],[2501,3223,3224,3233,3099,3457,3102,3230,519,2773,378,3451,3462,3277,2571,2464,34,39,6,7,9,4,10,5,29,8,30,28,40,2,37,41,3,12,36,33,32])). % 116.75/116.78 cnf(3482,plain, % 116.75/116.78 (~P3(f4(a2,f9(x34821,a2),a2),f4(a1,a2,a1))), % 116.75/116.78 inference(scs_inference,[],[2501,3226,3183,3223,3224,3233,3099,3457,3459,3102,2985,339,3230,519,2773,378,3451,3462,3277,2571,2464,17,22,34,39,6,7,9,4,10,5,29,8,30,28,40,2,37,41,3,12,36,33,32,13,11,14,15,35,2478,31,2530])). % 116.75/116.78 cnf(3485,plain, % 116.75/116.78 (~P3(f3(a5,f9(a8,a7)),f9(a8,a7))), % 116.75/116.78 inference(scs_inference,[],[2437,34])). % 116.75/116.78 cnf(3664,plain, % 116.75/116.78 ($false), % 116.75/116.78 inference(scs_inference,[],[18,22,42,48,44,2458,560,152,21,2503,164,2708,2795,2958,73,3301,3485,2443,2744,3233,3230,3431,3446,3482,3113,3438,3464,3467,2,40,30,2478,5,29,4,39,15,14,11,13,32,33,12,36,3,41,31]), % 116.75/116.78 ['proof']). % 116.75/116.78 % SZS output end Proof % 116.75/116.78 % Total time :116.110000s %------------------------------------------------------------------------------