%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SEU186+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:37 EDT 2024 % Result : Theorem 67.20s 67.26s % Output : CNFRefutation 67.36s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.12 % Problem : SEU186+1 : TPTP v8.2.0. Released v3.3.0. % 0.10/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 14:15:09 EDT 2024 % 0.12/0.34 % CPUTime : % 0.19/0.58 start to proof:theBenchmark % 67.20/67.24 %------------------------------------------- % 67.20/67.24 % File :CSE---1.7 % 67.20/67.24 % Problem :theBenchmark % 67.20/67.24 % Transform :cnf % 67.20/67.24 % Format :tptp:raw % 67.20/67.24 % Command :java -jar mcs_scs.jar %d %s % 67.20/67.24 % 67.20/67.24 % Result :Theorem 66.630000s % 67.20/67.24 % Output :CNFRefutation 66.630000s % 67.20/67.24 %------------------------------------------- % 67.20/67.25 %------------------------------------------------------------------------------ % 67.20/67.25 % File : SEU186+1 : TPTP v8.2.0. Released v3.3.0. % 67.20/67.25 % Domain : Set theory % 67.20/67.25 % Problem : MPTP bushy problem t56_relat_1 % 67.20/67.25 % Version : [Urb07] axioms : Especial. % 67.20/67.25 % English : % 67.20/67.25 % 67.20/67.25 % Refs : [Ban01] Bancerek et al. (2001), On the Characterizations of Co % 67.20/67.25 % : [Urb07] Urban (2006), Email to G. Sutcliffe % 67.20/67.25 % Source : [Urb07] % 67.20/67.25 % Names : bushy-t56_relat_1 [Urb07] % 67.20/67.25 % 67.20/67.25 % Status : Theorem % 67.20/67.25 % Rating : 0.17 v8.1.0, 0.19 v7.5.0, 0.22 v7.4.0, 0.13 v7.3.0, 0.14 v7.2.0, 0.10 v7.1.0, 0.13 v7.0.0, 0.10 v6.4.0, 0.15 v6.3.0, 0.21 v6.2.0, 0.24 v6.1.0, 0.27 v6.0.0, 0.17 v5.5.0, 0.19 v5.4.0, 0.25 v5.3.0, 0.30 v5.2.0, 0.15 v5.1.0, 0.19 v5.0.0, 0.21 v4.1.0, 0.17 v4.0.1, 0.22 v4.0.0, 0.25 v3.7.0, 0.20 v3.5.0, 0.21 v3.3.0 % 67.20/67.25 % Syntax : Number of formulae : 26 ( 14 unt; 0 def) % 67.20/67.25 % Number of atoms : 42 ( 6 equ) % 67.20/67.25 % Maximal formula atoms : 3 ( 1 avg) % 67.20/67.25 % Number of connectives : 28 ( 12 ~; 1 |; 7 &) % 67.20/67.25 % ( 1 <=>; 7 =>; 0 <=; 0 <~>) % 67.20/67.25 % Maximal formula depth : 9 ( 3 avg) % 67.20/67.25 % Maximal term depth : 3 ( 1 avg) % 67.20/67.25 % Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty) % 67.20/67.25 % Number of functors : 4 ( 4 usr; 1 con; 0-2 aty) % 67.20/67.25 % Number of variables : 34 ( 29 !; 5 ?) % 67.20/67.25 % SPC : FOF_THM_RFO_SEQ % 67.20/67.25 % 67.20/67.25 % Comments : Translated by MPTP 0.2 from the original problem in the Mizar % 67.20/67.25 % library, www.mizar.org % 67.20/67.25 %------------------------------------------------------------------------------ % 67.20/67.25 fof(antisymmetry_r2_hidden,axiom, % 67.20/67.25 ! [A,B] : % 67.20/67.25 ( in(A,B) % 67.20/67.25 => ~ in(B,A) ) ). % 67.20/67.25 % 67.20/67.25 fof(cc1_relat_1,axiom, % 67.20/67.25 ! [A] : % 67.20/67.25 ( empty(A) % 67.20/67.25 => relation(A) ) ). % 67.20/67.25 % 67.20/67.25 fof(commutativity_k2_tarski,axiom, % 67.20/67.25 ! [A,B] : unordered_pair(A,B) = unordered_pair(B,A) ). % 67.20/67.25 % 67.20/67.25 fof(d1_relat_1,axiom, % 67.20/67.25 ! [A] : % 67.20/67.25 ( relation(A) % 67.20/67.25 <=> ! [B] : % 67.20/67.25 ~ ( in(B,A) % 67.20/67.25 & ! [C,D] : B != ordered_pair(C,D) ) ) ). % 67.20/67.25 % 67.20/67.25 fof(d5_tarski,axiom, % 67.20/67.25 ! [A,B] : ordered_pair(A,B) = unordered_pair(unordered_pair(A,B),singleton(A)) ). % 67.20/67.25 % 67.20/67.25 fof(dt_k1_tarski,axiom, % 67.20/67.25 $true ). % 67.20/67.25 % 67.20/67.25 fof(dt_k1_xboole_0,axiom, % 67.20/67.25 $true ). % 67.20/67.25 % 67.20/67.25 fof(dt_k2_tarski,axiom, % 67.20/67.25 $true ). % 67.20/67.25 % 67.20/67.25 fof(dt_k4_tarski,axiom, % 67.20/67.25 $true ). % 67.20/67.26 % 67.20/67.26 fof(dt_m1_subset_1,axiom, % 67.20/67.26 $true ). % 67.20/67.26 % 67.20/67.26 fof(existence_m1_subset_1,axiom, % 67.20/67.26 ! [A] : % 67.20/67.26 ? [B] : element(B,A) ). % 67.20/67.26 % 67.20/67.26 fof(fc1_xboole_0,axiom, % 67.20/67.26 empty(empty_set) ). % 67.20/67.26 % 67.20/67.26 fof(fc1_zfmisc_1,axiom, % 67.20/67.26 ! [A,B] : ~ empty(ordered_pair(A,B)) ). % 67.20/67.26 % 67.20/67.26 fof(fc2_subset_1,axiom, % 67.20/67.26 ! [A] : ~ empty(singleton(A)) ). % 67.20/67.26 % 67.20/67.26 fof(fc3_subset_1,axiom, % 67.20/67.26 ! [A,B] : ~ empty(unordered_pair(A,B)) ). % 67.20/67.26 % 67.20/67.26 fof(fc4_relat_1,axiom, % 67.20/67.26 ( empty(empty_set) % 67.20/67.26 & relation(empty_set) ) ). % 67.20/67.26 % 67.20/67.26 fof(rc1_relat_1,axiom, % 67.20/67.26 ? [A] : % 67.20/67.26 ( empty(A) % 67.20/67.26 & relation(A) ) ). % 67.20/67.26 % 67.20/67.26 fof(rc1_xboole_0,axiom, % 67.20/67.26 ? [A] : empty(A) ). % 67.20/67.26 % 67.20/67.26 fof(rc2_relat_1,axiom, % 67.20/67.26 ? [A] : % 67.20/67.26 ( ~ empty(A) % 67.20/67.26 & relation(A) ) ). % 67.20/67.26 % 67.20/67.26 fof(rc2_xboole_0,axiom, % 67.20/67.26 ? [A] : ~ empty(A) ). % 67.20/67.26 % 67.20/67.26 fof(t1_subset,axiom, % 67.20/67.26 ! [A,B] : % 67.20/67.26 ( in(A,B) % 67.20/67.26 => element(A,B) ) ). % 67.20/67.26 % 67.20/67.26 fof(t2_subset,axiom, % 67.20/67.26 ! [A,B] : % 67.20/67.26 ( element(A,B) % 67.20/67.26 => ( empty(B) % 67.20/67.26 | in(A,B) ) ) ). % 67.20/67.26 % 67.20/67.26 fof(t56_relat_1,conjecture, % 67.20/67.26 ! [A] : % 67.20/67.26 ( relation(A) % 67.20/67.26 => ( ! [B,C] : ~ in(ordered_pair(B,C),A) % 67.20/67.26 => A = empty_set ) ) ). % 67.20/67.26 % 67.20/67.26 fof(t6_boole,axiom, % 67.20/67.26 ! [A] : % 67.20/67.26 ( empty(A) % 67.20/67.26 => A = empty_set ) ). % 67.20/67.26 % 67.20/67.26 fof(t7_boole,axiom, % 67.20/67.26 ! [A,B] : % 67.20/67.26 ~ ( in(A,B) % 67.20/67.26 & empty(B) ) ). % 67.20/67.26 % 67.20/67.26 fof(t8_boole,axiom, % 67.20/67.26 ! [A,B] : % 67.20/67.26 ~ ( empty(A) % 67.20/67.26 & A != B % 67.20/67.26 & empty(B) ) ). % 67.20/67.26 % 67.20/67.26 %------------------------------------------------------------------------------ % 67.20/67.26 %------------------------------------------- % 67.20/67.26 % Proof found % 67.20/67.26 % SZS status Theorem for theBenchmark % 67.20/67.26 % SZS output start Proof % 67.20/67.26 %ClaNum:45(EqnAxiom:18) % 67.20/67.26 %VarNum:54(SingletonVarNum:26) % 67.20/67.26 %MaxLitNum:3 % 67.20/67.26 %MaxfuncDepth:3 % 67.20/67.26 %SharedTerms:16 % 67.20/67.26 %goalClause: 26 29 35 % 67.20/67.26 %singleGoalClaCount:3 % 67.20/67.26 [20]P1(a1) % 67.20/67.26 [21]P1(a2) % 67.20/67.26 [22]P1(a7) % 67.20/67.26 [23]P3(a1) % 67.20/67.26 [24]P3(a2) % 67.20/67.26 [25]P3(a8) % 67.20/67.26 [26]P3(a9) % 67.20/67.26 [29]~E(a9,a1) % 67.20/67.26 [30]~P1(a8) % 67.20/67.26 [31]~P1(a10) % 67.20/67.26 [27]P2(f3(x271),x271) % 67.20/67.26 [32]~P1(f12(x321)) % 67.20/67.26 [28]E(f11(x281,x282),f11(x282,x281)) % 67.20/67.26 [33]~P1(f11(x331,x332)) % 67.20/67.26 [35]~P4(f11(f11(x351,x352),f12(x351)),a9) % 67.20/67.26 [36]~P1(x361)+E(x361,a1) % 67.20/67.26 [37]~P1(x371)+P3(x371) % 67.20/67.26 [39]P3(x391)+P4(f4(x391),x391) % 67.20/67.26 [40]~P1(x401)+~P4(x402,x401) % 67.20/67.26 [41]~P4(x411,x412)+P2(x411,x412) % 67.20/67.26 [43]~P4(x432,x431)+~P4(x431,x432) % 67.20/67.26 [44]P3(x441)+~E(f4(x441),f11(f11(x442,x443),f12(x442))) % 67.20/67.26 [38]~P1(x382)+~P1(x381)+E(x381,x382) % 67.20/67.26 [42]~P2(x422,x421)+P1(x421)+P4(x422,x421) % 67.20/67.26 [45]~P3(x451)+~P4(x452,x451)+E(f11(f11(f5(x451,x452),f6(x451,x452)),f12(f5(x451,x452))),x452) % 67.20/67.26 %EqnAxiom % 67.20/67.26 [1]E(x11,x11) % 67.20/67.26 [2]E(x22,x21)+~E(x21,x22) % 67.20/67.26 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 67.20/67.26 [4]~E(x41,x42)+E(f3(x41),f3(x42)) % 67.20/67.26 [5]~E(x51,x52)+E(f11(x51,x53),f11(x52,x53)) % 67.20/67.26 [6]~E(x61,x62)+E(f11(x63,x61),f11(x63,x62)) % 67.20/67.26 [7]~E(x71,x72)+E(f12(x71),f12(x72)) % 67.20/67.26 [8]~E(x81,x82)+E(f4(x81),f4(x82)) % 67.20/67.26 [9]~E(x91,x92)+E(f5(x91,x93),f5(x92,x93)) % 67.20/67.26 [10]~E(x101,x102)+E(f5(x103,x101),f5(x103,x102)) % 67.20/67.26 [11]~E(x111,x112)+E(f6(x111,x113),f6(x112,x113)) % 67.20/67.26 [12]~E(x121,x122)+E(f6(x123,x121),f6(x123,x122)) % 67.20/67.26 [13]~P1(x131)+P1(x132)+~E(x131,x132) % 67.20/67.26 [14]P4(x142,x143)+~E(x141,x142)+~P4(x141,x143) % 67.20/67.26 [15]P4(x153,x152)+~E(x151,x152)+~P4(x153,x151) % 67.20/67.26 [16]~P3(x161)+P3(x162)+~E(x161,x162) % 67.20/67.26 [17]P2(x172,x173)+~E(x171,x172)+~P2(x171,x173) % 67.20/67.26 [18]P2(x183,x182)+~E(x181,x182)+~P2(x183,x181) % 67.20/67.26 % 67.20/67.26 %------------------------------------------- % 67.20/67.27 cnf(46,plain, % 67.20/67.27 (~P1(a9)), % 67.20/67.27 inference(scs_inference,[],[29,36])). % 67.20/67.27 cnf(48,plain, % 67.20/67.27 (~P4(x481,a1)), % 67.20/67.27 inference(scs_inference,[],[29,20,36,40])). % 67.20/67.27 cnf(50,plain, % 67.20/67.27 (P4(f3(a8),a8)), % 67.20/67.27 inference(scs_inference,[],[29,27,20,30,36,40,42])). % 67.20/67.27 cnf(51,plain, % 67.20/67.27 (P2(f3(x511),x511)), % 67.20/67.27 inference(rename_variables,[],[27])). % 67.20/67.27 cnf(54,plain, % 67.20/67.27 (P2(f3(f11(x541,x542)),f11(x542,x541))), % 67.20/67.27 inference(scs_inference,[],[29,27,51,28,20,30,36,40,42,15,18])). % 67.20/67.27 cnf(55,plain, % 67.20/67.27 (P2(f3(x551),x551)), % 67.20/67.27 inference(rename_variables,[],[27])). % 67.20/67.27 cnf(58,plain, % 67.20/67.27 (P4(x581,a8)+~E(f3(a8),x581)), % 67.20/67.27 inference(scs_inference,[],[29,27,51,28,20,30,36,40,42,15,18,43,14])). % 67.20/67.27 cnf(60,plain, % 67.20/67.27 (P2(x601,x602)+~E(f3(x602),x601)), % 67.20/67.27 inference(scs_inference,[],[29,27,51,55,28,20,30,36,40,42,15,18,43,14,16,17])). % 67.20/67.27 cnf(63,plain, % 67.20/67.27 (~P4(x631,a2)), % 67.20/67.27 inference(scs_inference,[],[21,40])). % 67.20/67.27 cnf(65,plain, % 67.20/67.27 (~P2(f11(f11(x651,x652),f12(x651)),a9)), % 67.20/67.27 inference(scs_inference,[],[35,46,21,40,42])). % 67.20/67.27 cnf(67,plain, % 67.20/67.27 (~E(f3(a9),f11(f11(x671,x672),f12(x671)))), % 67.20/67.27 inference(scs_inference,[],[35,46,21,27,40,42,17])). % 67.20/67.27 cnf(71,plain, % 67.20/67.27 (~P4(x711,a7)), % 67.20/67.27 inference(scs_inference,[],[22,40])). % 67.20/67.27 cnf(86,plain, % 67.20/67.27 (P4(f3(f12(x861)),f12(x861))), % 67.20/67.27 inference(scs_inference,[],[32,27,42])). % 67.20/67.27 cnf(91,plain, % 67.20/67.27 (~P4(f12(x911),f3(f12(x911)))), % 67.20/67.27 inference(scs_inference,[],[50,63,32,27,42,15,43])). % 67.20/67.27 cnf(93,plain, % 67.20/67.27 (P4(x931,f12(x932))+~E(f3(f12(x932)),x931)), % 67.20/67.27 inference(scs_inference,[],[50,63,32,27,42,15,43,14])). % 67.20/67.27 cnf(95,plain, % 67.20/67.27 (P4(f3(f11(x951,x952)),f11(x952,x951))), % 67.20/67.27 inference(scs_inference,[],[54,33,42])). % 67.20/67.27 cnf(102,plain, % 67.20/67.27 (P4(x1021,f11(x1022,x1023))+~E(f3(f11(x1023,x1022)),x1021)), % 67.20/67.27 inference(scs_inference,[],[50,54,71,33,42,15,43,14])). % 67.20/67.27 cnf(108,plain, % 67.20/67.27 (~P4(a1,a9)), % 67.20/67.27 inference(scs_inference,[],[26,95,48,15,45])). % 67.20/67.27 cnf(112,plain, % 67.20/67.28 (E(f3(f11(x1121,x1122)),f3(f11(x1122,x1121)))), % 67.20/67.28 inference(scs_inference,[],[28,2,4])). % 67.20/67.28 cnf(113,plain, % 67.20/67.28 (P4(f3(f11(x1131,x1132)),f11(x1131,x1132))), % 67.20/67.28 inference(scs_inference,[],[112,102])). % 67.20/67.28 cnf(126,plain, % 67.20/67.28 (~P4(f11(f12(x1261),f11(x1261,x1262)),a9)), % 67.20/67.28 inference(scs_inference,[],[65,28,41,14])). % 67.20/67.28 cnf(184,plain, % 67.20/67.28 (~E(f11(x1841,x1842),a2)), % 67.20/67.28 inference(scs_inference,[],[63,95,15])). % 67.20/67.28 cnf(186,plain, % 67.20/67.28 (~P4(a2,a9)), % 67.20/67.28 inference(scs_inference,[],[63,26,95,15,45])). % 67.20/67.28 cnf(198,plain, % 67.20/67.28 (~E(f11(x1981,x1982),a7)), % 67.20/67.28 inference(scs_inference,[],[71,95,15])). % 67.20/67.28 cnf(200,plain, % 67.20/67.28 (~P4(a7,a9)), % 67.20/67.28 inference(scs_inference,[],[71,26,95,15,45])). % 67.20/67.28 cnf(216,plain, % 67.20/67.28 (~P2(a1,a9)), % 67.20/67.28 inference(scs_inference,[],[108,46,42])). % 67.20/67.28 cnf(224,plain, % 67.20/67.28 (~P2(f11(f12(x2241),f11(x2241,x2242)),a9)), % 67.20/67.28 inference(scs_inference,[],[126,46,42])). % 67.20/67.28 cnf(238,plain, % 67.20/67.28 (~P2(a2,a9)), % 67.20/67.28 inference(scs_inference,[],[186,46,42])). % 67.20/67.28 cnf(245,plain, % 67.20/67.28 (~P2(a7,a9)), % 67.20/67.28 inference(scs_inference,[],[200,46,42])). % 67.20/67.28 cnf(251,plain, % 67.20/67.28 (~P1(f3(a9))), % 67.20/67.28 inference(scs_inference,[],[216,27,17,36])). % 67.20/67.28 cnf(268,plain, % 67.20/67.28 (~E(f3(a9),a2)), % 67.20/67.28 inference(scs_inference,[],[238,27,17])). % 67.20/67.28 cnf(272,plain, % 67.20/67.28 (~E(f3(a9),a7)), % 67.20/67.28 inference(scs_inference,[],[245,27,17])). % 67.20/67.28 cnf(290,plain, % 67.20/67.28 (~E(f3(a8),a2)), % 67.20/67.28 inference(scs_inference,[],[25,184,45,58])). % 67.20/67.28 cnf(295,plain, % 67.20/67.28 (~E(f3(a8),a7)), % 67.20/67.28 inference(scs_inference,[],[25,198,45,58])). % 67.20/67.28 cnf(330,plain, % 67.20/67.28 (E(a1,a2)), % 67.20/67.28 inference(scs_inference,[],[21,36,2])). % 67.20/67.28 cnf(331,plain, % 67.20/67.28 (E(a2,a1)), % 67.20/67.28 inference(scs_inference,[],[330,2])). % 67.20/67.28 cnf(332,plain, % 67.20/67.28 (~E(a9,a2)), % 67.20/67.28 inference(scs_inference,[],[29,330,2,3])). % 67.20/67.28 cnf(526,plain, % 67.20/67.28 (E(a1,a7)), % 67.20/67.28 inference(scs_inference,[],[22,36,2])). % 67.20/67.28 cnf(556,plain, % 67.20/67.28 (E(f11(a2,x5561),f11(a1,x5561))), % 67.20/67.28 inference(scs_inference,[],[21,36,5])). % 67.20/67.28 cnf(557,plain, % 67.20/67.28 (E(f11(a1,x5571),f11(a2,x5571))), % 67.20/67.28 inference(scs_inference,[],[556,2])). % 67.20/67.28 cnf(558,plain, % 67.20/67.28 (E(f11(x5581,a2),f11(a1,x5581))), % 67.20/67.28 inference(scs_inference,[],[28,556,2,3])). % 67.20/67.28 cnf(568,plain, % 67.20/67.28 (E(f11(a1,x5681),f11(x5681,a2))), % 67.20/67.28 inference(scs_inference,[],[558,2])). % 67.20/67.28 cnf(569,plain, % 67.20/67.28 (P2(f3(f11(x5691,a1)),f11(a2,x5691))), % 67.20/67.28 inference(scs_inference,[],[557,558,54,2,18])). % 67.20/67.28 cnf(581,plain, % 67.20/67.28 (E(f11(a1,a1),f11(a2,a2))), % 67.20/67.28 inference(scs_inference,[],[568,557,3])). % 67.20/67.28 cnf(583,plain, % 67.20/67.28 (E(f11(a1,x5831),f11(x5831,a2))), % 67.20/67.28 inference(rename_variables,[],[568])). % 67.20/67.28 cnf(584,plain, % 67.20/67.28 (P2(f3(f11(x5841,a1)),f11(x5841,a2))), % 67.20/67.28 inference(scs_inference,[],[568,583,557,54,3,18])). % 67.20/67.28 cnf(586,plain, % 67.20/67.28 (P2(f3(f11(a1,x5861)),f11(x5861,a2))), % 67.20/67.28 inference(scs_inference,[],[112,568,583,557,54,3,18,17])). % 67.20/67.28 cnf(588,plain, % 67.20/67.28 (E(f11(a2,a2),f11(a1,a1))), % 67.20/67.28 inference(scs_inference,[],[112,568,583,557,54,3,18,17,2])). % 67.20/67.28 cnf(603,plain, % 67.20/67.28 (P2(f3(f11(a2,x6031)),f11(a1,x6031))), % 67.20/67.28 inference(scs_inference,[],[558,54,18])). % 67.20/67.28 cnf(605,plain, % 67.20/67.28 (P2(f3(f11(x6051,a2)),f11(a1,x6051))), % 67.20/67.28 inference(scs_inference,[],[112,558,54,18,17])). % 67.20/67.28 cnf(675,plain, % 67.20/67.28 (P4(f3(f11(x6751,a1)),f11(a2,x6751))), % 67.20/67.28 inference(scs_inference,[],[569,33,42])). % 67.20/67.28 cnf(678,plain, % 67.20/67.28 (P4(f3(f11(a1,x6781)),f11(a2,x6781))), % 67.20/67.28 inference(scs_inference,[],[569,112,33,42,14])). % 67.20/67.28 cnf(680,plain, % 67.20/67.28 (~P4(f11(a2,x6801),f3(f11(x6801,a1)))), % 67.20/67.28 inference(scs_inference,[],[569,112,33,42,14,43])). % 67.20/67.28 cnf(683,plain, % 67.20/67.28 (~P4(f11(a2,x6831),f3(f11(a1,x6831)))), % 67.20/67.28 inference(scs_inference,[],[678,43])). % 67.20/67.28 cnf(689,plain, % 67.20/67.28 (P4(f3(f11(x6891,a1)),f11(x6891,a2))), % 67.20/67.28 inference(scs_inference,[],[584,33,42])). % 67.20/67.28 cnf(692,plain, % 67.20/67.28 (P4(f3(f11(a1,x6921)),f11(x6921,a2))), % 67.20/67.28 inference(scs_inference,[],[584,112,33,42,14])). % 67.20/67.28 cnf(694,plain, % 67.20/67.28 (~P4(f11(x6941,a2),f3(f11(x6941,a1)))), % 67.20/67.28 inference(scs_inference,[],[584,112,33,42,14,43])). % 67.20/67.28 cnf(697,plain, % 67.20/67.28 (~P4(f11(x6971,a2),f3(f11(a1,x6971)))), % 67.20/67.28 inference(scs_inference,[],[692,43])). % 67.20/67.28 cnf(713,plain, % 67.20/67.28 (P4(f3(f11(x7131,a2)),f11(a1,x7131))), % 67.20/67.28 inference(scs_inference,[],[603,112,33,42,14])). % 67.20/67.28 cnf(715,plain, % 67.20/67.28 (~P4(f11(a1,x7151),f3(f11(a2,x7151)))), % 67.20/67.28 inference(scs_inference,[],[603,112,33,42,14,43])). % 67.20/67.28 cnf(718,plain, % 67.20/67.28 (~P4(f11(a1,x7181),f3(f11(x7181,a2)))), % 67.20/67.28 inference(scs_inference,[],[713,43])). % 67.20/67.28 cnf(768,plain, % 67.20/67.28 (E(f11(x7681,a1),f11(a2,x7681))), % 67.20/67.28 inference(scs_inference,[],[28,557,3])). % 67.20/67.28 cnf(770,plain, % 67.20/67.28 (E(f11(x7701,x7702),f11(x7702,x7701))), % 67.20/67.28 inference(rename_variables,[],[28])). % 67.20/67.28 cnf(771,plain, % 67.20/67.28 (P2(f3(f11(x7711,a2)),f11(x7711,a1))), % 67.20/67.28 inference(scs_inference,[],[28,770,557,605,3,18])). % 67.20/67.28 cnf(774,plain, % 67.20/67.28 (P2(f3(f11(a2,x7741)),f11(x7741,a1))), % 67.20/67.28 inference(scs_inference,[],[28,770,112,557,605,3,18,17])). % 67.20/67.28 cnf(776,plain, % 67.20/67.28 (E(f11(a2,x7761),f11(x7761,a1))), % 67.20/67.28 inference(scs_inference,[],[28,770,112,557,605,3,18,17,2])). % 67.20/67.28 cnf(778,plain, % 67.20/67.28 (E(f11(x7781,a1),f11(x7781,a2))), % 67.20/67.28 inference(scs_inference,[],[28,568,3])). % 67.20/67.28 cnf(988,plain, % 67.20/67.28 (P4(f3(f11(x9881,a2)),f11(x9881,a1))), % 67.20/67.28 inference(scs_inference,[],[771,33,42])). % 67.20/67.28 cnf(993,plain, % 67.20/67.28 (~P4(f11(x9931,a1),f3(f11(x9931,a2)))), % 67.20/67.28 inference(scs_inference,[],[771,112,33,42,14,43])). % 67.20/67.28 cnf(1552,plain, % 67.20/67.28 (E(f11(a7,x15521),f11(a1,x15521))), % 67.20/67.28 inference(scs_inference,[],[22,36,5])). % 67.20/67.28 cnf(1553,plain, % 67.20/67.28 (E(f11(a1,x15531),f11(a7,x15531))), % 67.20/67.28 inference(scs_inference,[],[1552,2])). % 67.20/67.28 cnf(1554,plain, % 67.20/67.28 (E(f11(a1,a7),f11(a1,a2))), % 67.20/67.28 inference(scs_inference,[],[568,1552,2,3])). % 67.20/67.28 cnf(1566,plain, % 67.20/67.28 (E(f11(a1,a2),f11(a1,a7))), % 67.20/67.28 inference(scs_inference,[],[1554,2])). % 67.20/67.28 cnf(1567,plain, % 67.20/67.28 (E(f11(x15671,a2),f11(a7,x15671))), % 67.20/67.28 inference(scs_inference,[],[558,1553,1554,2,3])). % 67.20/67.28 cnf(1585,plain, % 67.20/67.28 (E(f11(a7,x15851),f11(x15851,a2))), % 67.20/67.28 inference(scs_inference,[],[1567,2])). % 67.20/67.28 cnf(1586,plain, % 67.20/67.28 (E(f11(a2,a2),f11(a1,a7))), % 67.20/67.28 inference(scs_inference,[],[558,1566,1567,2,3])). % 67.20/67.28 cnf(1596,plain, % 67.20/67.28 (E(f11(a1,a7),f11(a2,a2))), % 67.20/67.28 inference(scs_inference,[],[1586,2])). % 67.20/67.28 cnf(1597,plain, % 67.20/67.28 (E(f11(a1,a1),f11(a1,a7))), % 67.20/67.28 inference(scs_inference,[],[581,1586,2,3])). % 67.20/67.28 cnf(1617,plain, % 67.20/67.28 (E(f11(a1,a7),f11(a1,a1))), % 67.20/67.28 inference(scs_inference,[],[1597,2])). % 67.20/67.28 cnf(1618,plain, % 67.20/67.28 (E(f11(a2,a2),f11(a7,a1))), % 67.20/67.28 inference(scs_inference,[],[558,1597,1567,2,3])). % 67.20/67.28 cnf(1629,plain, % 67.20/67.28 (E(f11(a7,a1),f11(a2,a2))), % 67.20/67.28 inference(scs_inference,[],[1618,2])). % 67.20/67.28 cnf(1630,plain, % 67.20/67.28 (E(f11(a7,a2),f11(a1,a1))), % 67.20/67.28 inference(scs_inference,[],[558,1618,1617,2,3])). % 67.20/67.28 cnf(1640,plain, % 67.20/67.28 (E(f11(a1,a1),f11(a7,a2))), % 67.20/67.28 inference(scs_inference,[],[1630,2])). % 67.20/67.28 cnf(1641,plain, % 67.20/67.28 (E(f11(a2,a7),f11(a2,a2))), % 67.20/67.28 inference(scs_inference,[],[776,1629,1630,2,3])). % 67.20/67.28 cnf(1659,plain, % 67.20/67.28 (E(f11(a1,a1),f11(a2,a7))), % 67.20/67.28 inference(scs_inference,[],[581,1641,2,3])). % 67.20/67.28 cnf(1673,plain, % 67.20/67.28 (E(f11(a2,a7),f11(a1,a1))), % 67.20/67.28 inference(scs_inference,[],[1659,2])). % 67.20/67.28 cnf(1717,plain, % 67.20/67.28 (E(f11(a1,a7),f11(a2,a1))), % 67.20/67.28 inference(scs_inference,[],[768,1586,3,2])). % 67.20/67.28 cnf(1736,plain, % 67.20/67.28 (E(f11(x17361,a1),f11(a7,x17361))), % 67.20/67.28 inference(scs_inference,[],[778,1567,3])). % 67.20/67.28 cnf(1738,plain, % 67.20/67.28 (E(f11(a7,x17381),f11(x17381,a1))), % 67.20/67.28 inference(scs_inference,[],[778,1567,3,2])). % 67.20/67.28 cnf(1779,plain, % 67.20/67.28 (P2(f3(f11(x17791,a7)),f11(a1,x17791))), % 67.20/67.28 inference(scs_inference,[],[1552,54,18])). % 67.20/67.28 cnf(1781,plain, % 67.20/67.28 (E(f11(a7,x17811),f11(a2,x17811))), % 67.20/67.28 inference(scs_inference,[],[1552,557,54,18,3])). % 67.20/67.28 cnf(1785,plain, % 67.20/67.28 (E(f11(a2,x17851),f11(a7,x17851))), % 67.20/67.28 inference(scs_inference,[],[1552,112,557,54,18,3,17,2])). % 67.20/67.28 cnf(1805,plain, % 67.20/67.28 (E(f11(a7,x18051),f11(a1,x18051))), % 67.20/67.28 inference(rename_variables,[],[1552])). % 67.20/67.28 cnf(1806,plain, % 67.20/67.28 (E(f11(a7,a7),f11(a1,a2))), % 67.20/67.28 inference(scs_inference,[],[1552,1805,1554,586,18,3])). % 67.20/67.28 cnf(1810,plain, % 67.20/67.28 (E(f11(a1,a2),f11(a7,a7))), % 67.20/67.28 inference(scs_inference,[],[1552,1805,112,1554,586,18,3,17,2])). % 67.20/67.28 cnf(1821,plain, % 67.20/67.28 (E(f11(a7,x18211),f11(a1,x18211))), % 67.20/67.28 inference(rename_variables,[],[1552])). % 67.20/67.28 cnf(1822,plain, % 67.20/67.28 (E(f11(a7,a7),f11(a2,a2))), % 67.20/67.28 inference(scs_inference,[],[1552,1821,1596,774,18,3])). % 67.20/67.28 cnf(1824,plain, % 67.20/67.28 (P2(f3(f11(a7,a2)),f11(a1,a1))), % 67.20/67.28 inference(scs_inference,[],[1552,1821,112,1596,774,18,3,17])). % 67.20/67.28 cnf(1826,plain, % 67.20/67.28 (E(f11(a2,a2),f11(a7,a7))), % 67.20/67.28 inference(scs_inference,[],[1552,1821,112,1596,774,18,3,17,2])). % 67.20/67.28 cnf(1828,plain, % 67.20/67.28 (E(f11(a7,a7),f11(a1,a1))), % 67.20/67.28 inference(scs_inference,[],[1552,581,1617,1824,18,3])). % 67.20/67.28 cnf(1832,plain, % 67.20/67.28 (E(f11(a1,a1),f11(a7,a7))), % 67.20/67.28 inference(scs_inference,[],[1552,112,581,1617,1824,18,3,17,2])). % 67.20/67.28 cnf(1834,plain, % 67.20/67.28 (E(f11(a7,a7),f11(a2,a1))), % 67.20/67.28 inference(scs_inference,[],[1552,1717,3])). % 67.20/67.28 cnf(1836,plain, % 67.20/67.28 (E(f11(a2,a1),f11(a7,a7))), % 67.20/67.28 inference(scs_inference,[],[1552,1717,3,2])). % 67.20/67.28 cnf(1838,plain, % 67.20/67.28 (P2(f3(f11(x18381,a1)),f11(a7,x18381))), % 67.20/67.28 inference(scs_inference,[],[1553,54,18])). % 67.20/67.28 cnf(1840,plain, % 67.20/67.28 (P2(f3(f11(a1,x18401)),f11(a7,x18401))), % 67.20/67.28 inference(scs_inference,[],[1553,112,54,18,17])). % 67.20/67.28 cnf(1847,plain, % 67.20/67.28 (P2(f3(f11(a2,x18471)),f11(a7,x18471))), % 67.20/67.28 inference(scs_inference,[],[1553,603,18])). % 67.20/67.28 cnf(1849,plain, % 67.20/67.28 (P2(f3(f11(x18491,a2)),f11(a7,x18491))), % 67.20/67.28 inference(scs_inference,[],[1553,112,603,18,17])). % 67.20/67.28 cnf(1911,plain, % 67.20/67.28 (P2(f3(f11(x19111,a7)),f11(x19111,a2))), % 67.20/67.28 inference(scs_inference,[],[1585,54,18])). % 67.20/67.28 cnf(1959,plain, % 67.20/67.28 (P2(f3(f11(x19591,a7)),f11(x19591,a1))), % 67.20/67.28 inference(scs_inference,[],[1738,54,18])). % 67.20/67.28 cnf(1966,plain, % 67.20/67.28 (P4(f3(f11(x19661,a7)),f11(a1,x19661))), % 67.20/67.28 inference(scs_inference,[],[1779,33,42])). % 67.20/67.28 cnf(1969,plain, % 67.20/67.28 (P4(f3(f11(a7,x19691)),f11(a1,x19691))), % 67.20/67.28 inference(scs_inference,[],[1779,112,33,42,14])). % 67.20/67.28 cnf(1971,plain, % 67.20/67.28 (~P4(f11(a1,x19711),f3(f11(x19711,a7)))), % 67.20/67.28 inference(scs_inference,[],[1779,112,33,42,14,43])). % 67.20/67.28 cnf(1974,plain, % 67.20/67.28 (~P4(f11(a1,x19741),f3(f11(a7,x19741)))), % 67.20/67.28 inference(scs_inference,[],[1969,43])). % 67.20/67.28 cnf(1979,plain, % 67.20/67.28 (P2(f3(f11(x19791,a7)),f11(a2,x19791))), % 67.20/67.28 inference(scs_inference,[],[1781,54,18])). % 67.20/67.28 cnf(1981,plain, % 67.20/67.28 (P2(f3(f11(a7,x19811)),f11(a2,x19811))), % 67.20/67.28 inference(scs_inference,[],[1781,112,54,18,17])). % 67.20/67.28 cnf(2011,plain, % 67.20/67.28 (P4(f3(f11(x20111,a1)),f11(a7,x20111))), % 67.20/67.28 inference(scs_inference,[],[1838,33,42])). % 67.20/67.28 cnf(2014,plain, % 67.20/67.28 (P4(f3(f11(a1,x20141)),f11(a7,x20141))), % 67.20/67.28 inference(scs_inference,[],[1838,112,33,42,14])). % 67.20/67.28 cnf(2016,plain, % 67.20/67.28 (~P4(f11(a7,x20161),f3(f11(x20161,a1)))), % 67.20/67.28 inference(scs_inference,[],[1838,112,33,42,14,43])). % 67.20/67.28 cnf(2019,plain, % 67.20/67.28 (~P4(f11(a7,x20191),f3(f11(a1,x20191)))), % 67.20/67.28 inference(scs_inference,[],[2014,43])). % 67.20/67.28 cnf(2032,plain, % 67.20/67.28 (P4(f3(f11(a2,x20321)),f11(a7,x20321))), % 67.20/67.28 inference(scs_inference,[],[1847,33,42])). % 67.20/67.28 cnf(2116,plain, % 67.20/67.28 (P4(f3(a9),a9)), % 67.20/67.28 inference(scs_inference,[],[46,27,42])). % 67.20/67.28 cnf(2119,plain, % 67.20/67.28 (~P4(a9,f3(a9))), % 67.20/67.28 inference(scs_inference,[],[46,27,42,43])). % 67.20/67.28 cnf(2188,plain, % 67.20/67.28 (P4(f3(f11(x21881,a7)),f11(x21881,a2))), % 67.20/67.28 inference(scs_inference,[],[1911,33,42])). % 67.20/67.28 cnf(2193,plain, % 67.20/67.28 (~P4(f11(x21931,a2),f3(f11(x21931,a7)))), % 67.20/67.28 inference(scs_inference,[],[1911,112,33,42,14,43])). % 67.20/67.28 cnf(2217,plain, % 67.20/67.28 (P4(f3(f11(x22171,a7)),f11(x22171,a1))), % 67.20/67.28 inference(scs_inference,[],[1959,33,42])). % 67.20/67.28 cnf(2220,plain, % 67.20/67.28 (P4(f3(f11(a7,x22201)),f11(x22201,a1))), % 67.20/67.28 inference(scs_inference,[],[1959,112,33,42,14])). % 67.20/67.28 cnf(2225,plain, % 67.20/67.28 (~P4(f11(x22251,a1),f3(f11(a7,x22251)))), % 67.20/67.28 inference(scs_inference,[],[2220,43])). % 67.20/67.28 cnf(2234,plain, % 67.20/67.28 (P4(f3(f11(x22341,a7)),f11(a2,x22341))), % 67.20/67.28 inference(scs_inference,[],[1979,33,42])). % 67.20/67.28 cnf(2331,plain, % 67.20/67.28 (E(f11(x23311,a7),f11(x23311,a2))), % 67.20/67.28 inference(scs_inference,[],[28,1585,3])). % 67.20/67.28 cnf(2333,plain, % 67.20/67.28 (E(f11(x23331,x23332),f11(x23332,x23331))), % 67.20/67.28 inference(rename_variables,[],[28])). % 67.20/67.28 cnf(2334,plain, % 67.20/67.28 (P2(f3(f11(a1,x23341)),f11(x23341,a7))), % 67.20/67.28 inference(scs_inference,[],[28,2333,1585,1840,3,18])). % 67.20/67.28 cnf(2339,plain, % 67.20/67.28 (E(f11(x23391,a2),f11(x23391,a7))), % 67.20/67.28 inference(scs_inference,[],[28,2333,112,1585,1840,3,18,17,2])). % 67.20/67.28 cnf(2376,plain, % 67.20/67.28 (E(f11(x23761,a7),f11(x23761,a1))), % 67.20/67.28 inference(scs_inference,[],[28,1738,3])). % 67.20/67.28 cnf(2378,plain, % 67.20/67.28 (E(f11(x23781,x23782),f11(x23782,x23781))), % 67.20/67.28 inference(rename_variables,[],[28])). % 67.20/67.28 cnf(2384,plain, % 67.20/67.28 (E(f11(x23841,a1),f11(x23841,a7))), % 67.20/67.28 inference(scs_inference,[],[28,2378,112,1738,1849,3,18,17,2])). % 67.20/67.28 cnf(2403,plain, % 67.20/67.28 (E(f11(x24031,a7),f11(a2,x24031))), % 67.20/67.28 inference(scs_inference,[],[28,1781,3])). % 67.20/67.28 cnf(2406,plain, % 67.20/67.28 (E(f11(a2,x24061),f11(x24061,a7))), % 67.20/67.28 inference(scs_inference,[],[28,1781,3,2])). % 67.20/67.28 cnf(2429,plain, % 67.20/67.28 (E(f11(a1,x24291),f11(x24291,a7))), % 67.20/67.28 inference(scs_inference,[],[28,2384,3])). % 67.20/67.29 cnf(2432,plain, % 67.20/67.29 (E(f11(x24321,a7),f11(a1,x24321))), % 67.20/67.29 inference(scs_inference,[],[28,2384,3,2])). % 67.20/67.29 cnf(2819,plain, % 67.20/67.29 (P4(f3(f11(a1,x28191)),f11(x28191,a7))), % 67.20/67.29 inference(scs_inference,[],[2334,33,42])). % 67.20/67.29 cnf(2822,plain, % 67.20/67.29 (P4(f3(f11(x28221,a1)),f11(x28221,a7))), % 67.20/67.29 inference(scs_inference,[],[2334,112,33,42,14])). % 67.20/67.29 cnf(2824,plain, % 67.20/67.29 (~P4(f11(x28241,a7),f3(f11(a1,x28241)))), % 67.20/67.29 inference(scs_inference,[],[2334,112,33,42,14,43])). % 67.20/67.29 cnf(2827,plain, % 67.20/67.29 (~P4(f11(x28271,a7),f3(f11(x28271,a1)))), % 67.20/67.29 inference(scs_inference,[],[2822,43])). % 67.20/67.29 cnf(2842,plain, % 67.20/67.29 (E(f3(f11(x28421,a7)),f3(f11(a2,x28421)))), % 67.20/67.29 inference(scs_inference,[],[2403,4])). % 67.20/67.29 cnf(2845,plain, % 67.20/67.29 (E(f11(f11(x28451,a7),x28452),f11(f11(a2,x28451),x28452))), % 67.20/67.29 inference(scs_inference,[],[2403,4,7,8,5])). % 67.20/67.29 cnf(2846,plain, % 67.20/67.29 (E(f11(x28461,f11(x28462,a7)),f11(x28461,f11(a2,x28462)))), % 67.20/67.29 inference(scs_inference,[],[2403,4,7,8,5,6])). % 67.20/67.29 cnf(2847,plain, % 67.20/67.29 (E(f5(f11(x28471,a7),x28472),f5(f11(a2,x28471),x28472))), % 67.20/67.29 inference(scs_inference,[],[2403,4,7,8,5,6,9])). % 67.20/67.29 cnf(2848,plain, % 67.20/67.29 (E(f5(x28481,f11(x28482,a7)),f5(x28481,f11(a2,x28482)))), % 67.20/67.29 inference(scs_inference,[],[2403,4,7,8,5,6,9,10])). % 67.20/67.29 cnf(2849,plain, % 67.20/67.29 (E(f6(f11(x28491,a7),x28492),f6(f11(a2,x28491),x28492))), % 67.20/67.29 inference(scs_inference,[],[2403,4,7,8,5,6,9,10,11])). % 67.20/67.29 cnf(2850,plain, % 67.20/67.29 (E(f6(x28501,f11(x28502,a7)),f6(x28501,f11(a2,x28502)))), % 67.20/67.29 inference(scs_inference,[],[2403,4,7,8,5,6,9,10,11,12])). % 67.20/67.29 cnf(2853,plain, % 67.20/67.29 (E(f3(f11(x28531,a7)),f3(f11(x28531,a2)))), % 67.20/67.29 inference(scs_inference,[],[332,2403,31,21,112,4,7,8,5,6,9,10,11,12,2,13,3])). % 67.20/67.29 cnf(2857,plain, % 67.20/67.29 (P4(f3(f12(f11(x28571,a7))),f12(f11(a2,x28571)))), % 67.20/67.29 inference(scs_inference,[],[2119,332,2403,31,86,251,21,112,4,7,8,5,6,9,10,11,12,2,13,3,42,15])). % 67.20/67.29 cnf(2859,plain, % 67.20/67.29 (~P4(f12(f11(x28591,a7)),f3(f12(f11(a2,x28591))))), % 67.20/67.29 inference(scs_inference,[],[2119,332,2403,91,31,86,251,21,112,4,7,8,5,6,9,10,11,12,2,13,3,42,15,14])). % 67.20/67.29 cnf(2861,plain, % 67.20/67.29 (~P2(f11(f11(x28611,a7),f12(a2)),a9)), % 67.20/67.29 inference(scs_inference,[],[2119,332,2403,91,31,65,86,251,21,112,4,7,8,5,6,9,10,11,12,2,13,3,42,15,14,17])). % 67.20/67.29 cnf(2865,plain, % 67.20/67.29 (~E(f3(a9),f11(f11(x28651,a7),f12(a2)))), % 67.20/67.29 inference(scs_inference,[],[2119,332,2403,91,31,65,86,251,21,112,4,7,8,5,6,9,10,11,12,2,13,3,42,15,14,17,41,60])). % 67.20/67.29 cnf(2866,plain, % 67.20/67.29 (~P4(f12(f11(a2,x28661)),f3(f12(f11(x28661,a7))))), % 67.20/67.29 inference(scs_inference,[],[2119,332,2403,91,31,65,86,251,21,112,4,7,8,5,6,9,10,11,12,2,13,3,42,15,14,17,41,60,43])). % 67.20/67.29 cnf(2877,plain, % 67.20/67.29 (E(f5(f11(x28771,a7),x28772),f5(f11(x28771,a1),x28772))), % 67.20/67.29 inference(scs_inference,[],[2376,7,8,9])). % 67.20/67.29 cnf(2878,plain, % 67.20/67.29 (E(f5(x28781,f11(x28782,a7)),f5(x28781,f11(x28782,a1)))), % 67.20/67.29 inference(scs_inference,[],[2376,7,8,9,10])). % 67.20/67.29 cnf(2879,plain, % 67.20/67.29 (E(f11(f11(x28791,a7),x28792),f11(f11(x28791,a1),x28792))), % 67.20/67.29 inference(scs_inference,[],[2376,7,8,9,10,5])). % 67.20/67.29 cnf(2882,plain, % 67.20/67.29 (E(f3(f11(x28821,a7)),f3(f11(x28821,a1)))), % 67.20/67.29 inference(scs_inference,[],[2376,7,8,9,10,5,12,11,4])). % 67.20/67.29 cnf(2883,plain, % 67.20/67.29 (E(f11(x28831,f11(x28832,a7)),f11(x28831,f11(x28832,a1)))), % 67.20/67.29 inference(scs_inference,[],[2376,7,8,9,10,5,12,11,4,6])). % 67.20/67.29 cnf(2889,plain, % 67.20/67.29 (P4(f3(f11(a1,f11(x28891,a7))),f11(f11(a2,x28891),a7))), % 67.20/67.29 inference(scs_inference,[],[2865,2845,2847,2848,2819,2376,32,22,7,8,9,10,5,12,11,4,6,2,13,3,15])). % 67.20/67.29 cnf(2890,plain, % 67.20/67.29 (E(f11(f11(x28901,a7),x28902),f11(f11(a2,x28901),x28902))), % 67.20/67.29 inference(rename_variables,[],[2845])). % 67.20/67.29 cnf(2895,plain, % 67.20/67.29 (~P2(f11(f12(a2),f11(x28951,a7)),a9)), % 67.20/67.29 inference(scs_inference,[],[694,2865,2845,2890,2846,2847,2848,2819,224,2376,32,22,7,8,9,10,5,12,11,4,6,2,13,3,15,14,17])). % 67.20/67.29 cnf(2898,plain, % 67.20/67.29 (P2(f3(f11(a1,f11(x28981,a7))),f11(f11(a2,x28981),a7))), % 67.20/67.29 inference(scs_inference,[],[694,2865,2845,2890,2846,2847,2848,2819,224,2376,32,22,7,8,9,10,5,12,11,4,6,2,13,3,15,14,17,41])). % 67.20/67.29 cnf(2900,plain, % 67.20/67.29 (~E(f3(a9),f11(f12(a2),f11(x29001,a7)))), % 67.20/67.29 inference(scs_inference,[],[694,2865,2845,2890,2846,2847,2848,2819,224,2376,32,22,7,8,9,10,5,12,11,4,6,2,13,3,15,14,17,41,60])). % 67.20/67.29 cnf(2916,plain, % 67.20/67.29 (E(f11(f11(x29161,a7),x29162),f11(f11(x29161,a2),x29162))), % 67.20/67.29 inference(scs_inference,[],[2331,8,9,12,7,10,11,5])). % 67.20/67.29 cnf(2917,plain, % 67.20/67.29 (E(f11(x29171,f11(x29172,a7)),f11(x29171,f11(x29172,a2)))), % 67.20/67.29 inference(scs_inference,[],[2331,8,9,12,7,10,11,5,6])). % 67.20/67.29 cnf(2918,plain, % 67.20/67.29 (E(f3(f11(x29181,a2)),f3(f11(x29181,a7)))), % 67.20/67.29 inference(scs_inference,[],[2331,2339,8,9,12,7,10,11,5,6,4])). % 67.20/67.29 cnf(2919,plain, % 67.20/67.29 (~E(f11(f12(a2),f11(x29191,a7)),f3(a9))), % 67.20/67.29 inference(scs_inference,[],[2900,2331,2339,8,9,12,7,10,11,5,6,4,2])). % 67.20/67.29 cnf(2925,plain, % 67.20/67.29 (E(f11(f11(x29251,a7),x29252),f11(f11(x29251,a1),x29252))), % 67.20/67.29 inference(rename_variables,[],[2879])). % 67.20/67.29 cnf(2930,plain, % 67.20/67.29 (P2(f3(f11(f11(x29301,a7),a1)),f11(f11(a2,x29301),a7))), % 67.20/67.29 inference(scs_inference,[],[697,2900,2849,2850,2879,2925,2889,2898,2331,2339,31,22,112,8,9,12,7,10,11,5,6,4,2,13,3,15,14,17])). % 67.20/67.29 cnf(2934,plain, % 67.20/67.29 (~P4(f11(f11(a2,a1),a7),f3(f11(a1,f11(a7,a7))))), % 67.20/67.29 inference(scs_inference,[],[697,2900,2849,2850,2879,2925,2889,2898,2331,2339,31,22,112,8,9,12,7,10,11,5,6,4,2,13,3,15,14,17,41,43])). % 67.20/67.29 cnf(2943,plain, % 67.20/67.29 (E(f5(f11(a7,a7),x29431),f5(f11(a2,a1),x29431))), % 67.20/67.29 inference(scs_inference,[],[1834,9])). % 67.20/67.29 cnf(2944,plain, % 67.20/67.29 (E(f6(x29441,f11(a7,a7)),f6(x29441,f11(a2,a1)))), % 67.20/67.29 inference(scs_inference,[],[1834,9,12])). % 67.20/67.29 cnf(2946,plain, % 67.20/67.29 (E(f6(f11(a7,a7),x29461),f6(f11(a2,a1),x29461))), % 67.20/67.29 inference(scs_inference,[],[1834,9,12,8,11])). % 67.20/67.29 cnf(2947,plain, % 67.20/67.29 (E(f12(f11(a7,a7)),f12(f11(a2,a1)))), % 67.20/67.29 inference(scs_inference,[],[1834,9,12,8,11,7])). % 67.20/67.29 cnf(2948,plain, % 67.20/67.29 (E(f11(f11(a7,a7),x29481),f11(f11(a2,a1),x29481))), % 67.20/67.29 inference(scs_inference,[],[1834,9,12,8,11,7,5])). % 67.20/67.29 cnf(2949,plain, % 67.20/67.29 (E(f5(x29491,f11(a7,a7)),f5(x29491,f11(a2,a1)))), % 67.20/67.29 inference(scs_inference,[],[1834,9,12,8,11,7,5,10])). % 67.20/67.29 cnf(2950,plain, % 67.20/67.29 (E(f11(x29501,f11(a7,a7)),f11(x29501,f11(a2,a1)))), % 67.20/67.29 inference(scs_inference,[],[1834,9,12,8,11,7,5,10,6])). % 67.20/67.29 cnf(2958,plain, % 67.20/67.29 (E(f11(x29581,f11(x29582,a7)),f11(x29581,f11(x29582,a1)))), % 67.20/67.29 inference(rename_variables,[],[2883])). % 67.20/67.29 cnf(2963,plain, % 67.20/67.29 (P2(f3(f11(f11(x29631,a7),a7)),f11(a1,f11(x29631,a1)))), % 67.20/67.29 inference(scs_inference,[],[680,2877,2878,2883,2958,290,1966,1834,32,21,9,12,8,11,7,5,10,6,4,2,13,3,15,14,41])). % 67.20/67.29 cnf(2974,plain, % 67.20/67.29 (E(f6(x29741,f11(a2,a1)),f6(x29741,f11(a7,a7)))), % 67.20/67.29 inference(scs_inference,[],[1836,12])). % 67.20/67.29 cnf(2976,plain, % 67.20/67.29 (E(f5(f11(a2,a1),x29761),f5(f11(a7,a7),x29761))), % 67.20/67.29 inference(scs_inference,[],[1836,12,8,9])). % 67.20/67.29 cnf(2977,plain, % 67.20/67.29 (E(f6(f11(a2,a1),x29771),f6(f11(a7,a7),x29771))), % 67.20/67.29 inference(scs_inference,[],[1836,12,8,9,11])). % 67.20/67.29 cnf(2978,plain, % 67.20/67.29 (E(f11(f11(a2,a1),x29781),f11(f11(a7,a7),x29781))), % 67.20/67.29 inference(scs_inference,[],[1836,12,8,9,11,5])). % 67.20/67.29 cnf(2979,plain, % 67.20/67.29 (E(f12(f11(a2,a1)),f12(f11(a7,a7)))), % 67.20/67.29 inference(scs_inference,[],[1836,12,8,9,11,5,7])). % 67.20/67.29 cnf(2980,plain, % 67.20/67.29 (E(f5(x29801,f11(a2,a1)),f5(x29801,f11(a7,a7)))), % 67.20/67.29 inference(scs_inference,[],[1836,12,8,9,11,5,7,10])). % 67.20/67.29 cnf(2982,plain, % 67.20/67.29 (E(f11(x29821,f11(a2,a1)),f11(x29821,f11(a7,a7)))), % 67.20/67.29 inference(scs_inference,[],[1836,12,8,9,11,5,7,10,4,6])). % 67.20/67.29 cnf(2984,plain, % 67.20/67.29 (E(f5(f11(a7,a7),f11(a7,a7)),f5(f11(a2,a1),f11(a2,a1)))), % 67.20/67.29 inference(scs_inference,[],[2943,2949,295,1836,12,8,9,11,5,7,10,4,6,2,3])). % 67.20/67.29 cnf(2989,plain, % 67.20/67.29 (~P4(f12(f11(a7,a7)),f3(f12(f11(a1,a7))))), % 67.20/67.29 inference(scs_inference,[],[2943,2947,2949,2866,295,1836,86,12,8,9,11,5,7,10,4,6,2,3,15,14])). % 67.20/67.29 cnf(3003,plain, % 67.20/67.29 (E(f5(f11(a7,a7),x30031),f5(f11(a1,a1),x30031))), % 67.20/67.29 inference(scs_inference,[],[1828,8,9])). % 67.20/67.29 cnf(3004,plain, % 67.20/67.29 (E(f6(x30041,f11(a7,a7)),f6(x30041,f11(a1,a1)))), % 67.20/67.29 inference(scs_inference,[],[1828,8,9,12])). % 67.20/67.29 cnf(3005,plain, % 67.20/67.29 (E(f6(f11(a7,a7),x30051),f6(f11(a1,a1),x30051))), % 67.20/67.29 inference(scs_inference,[],[1828,8,9,12,11])). % 67.20/67.29 cnf(3006,plain, % 67.20/67.29 (E(f12(f11(a7,a7)),f12(f11(a1,a1)))), % 67.20/67.29 inference(scs_inference,[],[1828,8,9,12,11,7])). % 67.20/67.29 cnf(3007,plain, % 67.20/67.29 (E(f5(x30071,f11(a7,a7)),f5(x30071,f11(a1,a1)))), % 67.20/67.29 inference(scs_inference,[],[1828,8,9,12,11,7,10])). % 67.20/67.29 cnf(3008,plain, % 67.20/67.29 (E(f11(f11(a7,a7),x30081),f11(f11(a1,a1),x30081))), % 67.20/67.29 inference(scs_inference,[],[1828,8,9,12,11,7,10,5])). % 67.20/67.29 cnf(3009,plain, % 67.20/67.29 (E(f11(x30091,f11(a7,a7)),f11(x30091,f11(a1,a1)))), % 67.20/67.29 inference(scs_inference,[],[1828,8,9,12,11,7,10,5,6])). % 67.20/67.29 cnf(3011,plain, % 67.20/67.29 (~E(a2,f3(a9))), % 67.20/67.29 inference(scs_inference,[],[268,1828,8,9,12,11,7,10,5,6,4,2])). % 67.20/67.29 cnf(3012,plain, % 67.20/67.29 (~E(a2,a8)), % 67.20/67.29 inference(scs_inference,[],[268,1828,30,21,8,9,12,11,7,10,5,6,4,2,13])). % 67.20/67.29 cnf(3013,plain, % 67.20/67.29 (E(f6(f11(a7,a7),f11(a7,a7)),f6(f11(a2,a1),f11(a2,a1)))), % 67.20/67.29 inference(scs_inference,[],[2944,2946,268,1828,30,21,8,9,12,11,7,10,5,6,4,2,13,3])). % 67.20/67.29 cnf(3017,plain, % 67.20/67.29 (E(f11(f11(a7,a7),x30171),f11(f11(a2,a1),x30171))), % 67.20/67.29 inference(rename_variables,[],[2948])). % 67.20/67.29 cnf(3022,plain, % 67.20/67.29 (P2(f3(f11(a2,f11(x30221,a7))),f11(a1,f11(x30221,a1)))), % 67.20/67.29 inference(scs_inference,[],[993,2944,2946,2948,3017,2842,2963,268,2188,1828,30,21,8,9,12,11,7,10,5,6,4,2,13,3,15,14,17])). % 67.20/67.29 cnf(3026,plain, % 67.20/67.29 (~P4(f11(f11(a2,a1),a2),f3(f11(f11(a7,a7),a7)))), % 67.20/67.29 inference(scs_inference,[],[993,2944,2946,2948,3017,2842,2963,268,2188,1828,30,21,8,9,12,11,7,10,5,6,4,2,13,3,15,14,17,41,43])). % 67.20/67.29 cnf(3032,plain, % 67.20/67.29 (E(f5(f11(a1,a1),x30321),f5(f11(a7,a7),x30321))), % 67.20/67.29 inference(scs_inference,[],[1832,9])). % 67.20/67.29 cnf(3033,plain, % 67.20/67.29 (E(f6(x30331,f11(a1,a1)),f6(x30331,f11(a7,a7)))), % 67.20/67.29 inference(scs_inference,[],[1832,9,12])). % 67.20/67.29 cnf(3035,plain, % 67.20/67.29 (E(f5(x30351,f11(a1,a1)),f5(x30351,f11(a7,a7)))), % 67.20/67.29 inference(scs_inference,[],[1832,9,12,8,10])). % 67.20/67.29 cnf(3036,plain, % 67.20/67.29 (E(f6(f11(a1,a1),x30361),f6(f11(a7,a7),x30361))), % 67.20/67.29 inference(scs_inference,[],[1832,9,12,8,10,11])). % 67.20/67.29 cnf(3037,plain, % 67.20/67.29 (E(f12(f11(a1,a1)),f12(f11(a7,a7)))), % 67.20/67.29 inference(scs_inference,[],[1832,9,12,8,10,11,7])). % 67.20/67.29 cnf(3038,plain, % 67.20/67.29 (E(f11(f11(a1,a1),x30381),f11(f11(a7,a7),x30381))), % 67.20/67.29 inference(scs_inference,[],[1832,9,12,8,10,11,7,5])). % 67.20/67.29 cnf(3040,plain, % 67.20/67.29 (E(f11(x30401,f11(a1,a1)),f11(x30401,f11(a7,a7)))), % 67.20/67.29 inference(scs_inference,[],[1832,9,12,8,10,11,7,5,4,6])). % 67.20/67.29 cnf(3043,plain, % 67.20/67.29 (E(f11(x30431,f11(a7,a7)),f11(x30431,f11(a2,a1)))), % 67.20/67.29 inference(rename_variables,[],[2950])). % 67.20/67.29 cnf(3046,plain, % 67.20/67.29 (E(f11(x30461,f11(a7,a7)),f11(x30461,f11(a2,a1)))), % 67.20/67.29 inference(rename_variables,[],[2950])). % 67.20/67.29 cnf(3049,plain, % 67.20/67.29 (E(f11(x30491,f11(a7,a7)),f11(x30491,f11(a2,a1)))), % 67.20/67.29 inference(rename_variables,[],[2950])). % 67.20/67.29 cnf(3051,plain, % 67.20/67.29 (P2(f3(f11(a7,f11(a7,a7))),f11(a2,f11(a2,a1)))), % 67.20/67.29 inference(scs_inference,[],[2919,683,2950,3043,3046,3049,272,1981,2011,1832,9,12,8,10,11,7,5,4,6,2,3,15,14,18])). % 67.20/67.29 cnf(3059,plain, % 67.20/67.29 (~E(f3(a9),f11(f11(a2,a1),f12(a7)))), % 67.20/67.29 inference(scs_inference,[],[2919,683,2950,3043,3046,3049,2978,272,1981,2011,1832,65,9,12,8,10,11,7,5,4,6,2,3,15,14,18,17,41,60])). % 67.20/67.29 cnf(3060,plain, % 67.20/67.29 (~P4(f11(a7,f11(a2,a1)),f3(f11(f11(a7,a7),a1)))), % 67.20/67.29 inference(scs_inference,[],[2919,683,2950,3043,3046,3049,2978,272,1981,2011,1832,65,9,12,8,10,11,7,5,4,6,2,3,15,14,18,17,41,60,43])). % 67.20/67.29 cnf(3067,plain, % 67.20/67.29 (E(f6(x30671,f11(a7,a7)),f6(x30671,f11(a2,a2)))), % 67.20/67.29 inference(scs_inference,[],[1822,12])). % 67.20/67.29 cnf(3069,plain, % 67.20/67.29 (E(f5(f11(a7,a7),x30691),f5(f11(a2,a2),x30691))), % 67.20/67.29 inference(scs_inference,[],[1822,12,8,9])). % 67.20/67.29 cnf(3070,plain, % 67.20/67.29 (E(f5(x30701,f11(a7,a7)),f5(x30701,f11(a2,a2)))), % 67.20/67.29 inference(scs_inference,[],[1822,12,8,9,10])). % 67.20/67.29 cnf(3071,plain, % 67.20/67.29 (E(f12(f11(a7,a7)),f12(f11(a2,a2)))), % 67.20/67.29 inference(scs_inference,[],[1822,12,8,9,10,7])). % 67.20/67.29 cnf(3072,plain, % 67.20/67.29 (E(f11(f11(a7,a7),x30721),f11(f11(a2,a2),x30721))), % 67.20/67.29 inference(scs_inference,[],[1822,12,8,9,10,7,5])). % 67.20/67.29 cnf(3073,plain, % 67.20/67.29 (E(f6(f11(a7,a7),x30731),f6(f11(a2,a2),x30731))), % 67.20/67.29 inference(scs_inference,[],[1822,12,8,9,10,7,5,11])). % 67.20/67.29 cnf(3074,plain, % 67.20/67.29 (E(f11(x30741,f11(a7,a7)),f11(x30741,f11(a2,a2)))), % 67.20/67.29 inference(scs_inference,[],[1822,12,8,9,10,7,5,11,6])). % 67.20/67.29 cnf(3077,plain, % 67.20/67.29 (E(f6(f11(a2,a1),f11(a2,a1)),f6(f11(a7,a7),f11(a7,a7)))), % 67.20/67.29 inference(scs_inference,[],[3059,2974,2977,1822,12,8,9,10,7,5,11,6,4,2,3])). % 67.20/67.29 cnf(3083,plain, % 67.20/67.29 (P4(f3(f12(f11(a7,a7))),f12(f11(a1,a1)))), % 67.20/67.29 inference(scs_inference,[],[3059,2974,2977,3006,3051,1822,86,33,12,8,9,10,7,5,11,6,4,2,3,42,15])). % 67.20/67.29 cnf(3088,plain, % 67.20/67.29 (~P2(f11(f11(a7,a7),f12(a1)),a9)), % 67.20/67.29 inference(scs_inference,[],[715,3059,2974,2977,2982,3006,3008,3051,1822,65,86,33,12,8,9,10,7,5,11,6,4,2,3,42,15,14,17])). % 67.20/67.29 cnf(3093,plain, % 67.20/67.29 (~E(f3(a9),f11(f11(a7,a7),f12(a1)))), % 67.20/67.29 inference(scs_inference,[],[715,3059,2974,2977,2982,3006,3008,3051,1822,65,86,33,12,8,9,10,7,5,11,6,4,2,3,42,15,14,17,41,60])). % 67.20/67.29 cnf(3094,plain, % 67.20/67.29 (~P4(f11(a2,f11(a2,a1)),f3(f11(a7,f11(a7,a7))))), % 67.20/67.29 inference(scs_inference,[],[715,3059,2974,2977,2982,3006,3008,3051,1822,65,86,33,12,8,9,10,7,5,11,6,4,2,3,42,15,14,17,41,60,43])). % 67.20/67.29 cnf(3127,plain, % 67.20/67.29 (E(f6(x31271,f11(a7,a7)),f6(x31271,f11(a1,a2)))), % 67.20/67.29 inference(scs_inference,[],[1806,12])). % 67.20/67.29 cnf(3128,plain, % 67.20/67.29 (E(f5(f11(a7,a7),x31281),f5(f11(a1,a2),x31281))), % 67.20/67.29 inference(scs_inference,[],[1806,12,9])). % 67.20/67.29 cnf(3130,plain, % 67.20/67.29 (E(f5(x31301,f11(a7,a7)),f5(x31301,f11(a1,a2)))), % 67.20/67.29 inference(scs_inference,[],[1806,12,9,8,10])). % 67.20/67.29 cnf(3131,plain, % 67.20/67.29 (E(f12(f11(a7,a7)),f12(f11(a1,a2)))), % 67.20/67.29 inference(scs_inference,[],[1806,12,9,8,10,7])). % 67.20/67.29 cnf(3132,plain, % 67.20/67.29 (E(f11(f11(a7,a7),x31321),f11(f11(a1,a2),x31321))), % 67.20/67.29 inference(scs_inference,[],[1806,12,9,8,10,7,5])). % 67.20/67.29 cnf(3133,plain, % 67.20/67.29 (E(f11(x31331,f11(a7,a7)),f11(x31331,f11(a1,a2)))), % 67.20/67.29 inference(scs_inference,[],[1806,12,9,8,10,7,5,6])). % 67.20/67.29 cnf(3134,plain, % 67.20/67.29 (E(f6(f11(a7,a7),x31341),f6(f11(a1,a2),x31341))), % 67.20/67.29 inference(scs_inference,[],[1806,12,9,8,10,7,5,6,11])). % 67.20/67.29 cnf(3139,plain, % 67.20/67.29 (E(f5(f11(a2,a1),f11(a2,a1)),f5(f11(a7,a7),f11(a7,a7)))), % 67.20/67.29 inference(scs_inference,[],[3093,2976,2980,3083,1806,12,9,8,10,7,5,6,11,4,43,2,3])). % 67.20/67.29 cnf(3142,plain, % 67.20/67.29 (P4(f3(f11(a2,f11(a7,a7))),f11(a7,f11(a1,a1)))), % 67.20/67.29 inference(scs_inference,[],[3093,2976,2980,3009,3083,2032,1806,12,9,8,10,7,5,6,11,4,43,2,3,15])). % 67.20/67.29 cnf(3143,plain, % 67.20/67.29 (E(f11(x31431,f11(a7,a7)),f11(x31431,f11(a1,a1)))), % 67.20/67.29 inference(rename_variables,[],[3009])). % 67.20/67.29 cnf(3151,plain, % 67.20/67.29 (P2(f3(f11(a2,f11(a7,a7))),f11(a7,f11(a1,a1)))), % 67.20/67.29 inference(scs_inference,[],[718,3093,2976,2980,3009,3143,3038,3083,2861,2032,1806,12,9,8,10,7,5,6,11,4,43,2,3,15,14,17,41])). % 67.20/67.29 cnf(3153,plain, % 67.20/67.29 (~E(f3(a9),f11(f11(a1,a1),f12(a2)))), % 67.20/67.29 inference(scs_inference,[],[718,3093,2976,2980,3009,3143,3038,3083,2861,2032,1806,12,9,8,10,7,5,6,11,4,43,2,3,15,14,17,41,60])). % 67.20/67.29 cnf(3160,plain, % 67.20/67.29 (E(f5(x31601,f11(a1,a2)),f5(x31601,f11(a7,a7)))), % 67.20/67.29 inference(scs_inference,[],[1810,10])). % 67.20/67.29 cnf(3161,plain, % 67.20/67.29 (E(f6(x31611,f11(a1,a2)),f6(x31611,f11(a7,a7)))), % 67.20/67.29 inference(scs_inference,[],[1810,10,12])). % 67.20/67.29 cnf(3163,plain, % 67.20/67.29 (E(f5(f11(a1,a2),x31631),f5(f11(a7,a7),x31631))), % 67.20/67.29 inference(scs_inference,[],[1810,10,12,8,9])). % 67.20/67.29 cnf(3165,plain, % 67.20/67.29 (E(f6(f11(a1,a2),x31651),f6(f11(a7,a7),x31651))), % 67.20/67.29 inference(scs_inference,[],[1810,10,12,8,9,7,11])). % 67.20/67.29 cnf(3166,plain, % 67.20/67.29 (E(f11(f11(a1,a2),x31661),f11(f11(a7,a7),x31661))), % 67.20/67.29 inference(scs_inference,[],[1810,10,12,8,9,7,11,5])). % 67.20/67.29 cnf(3167,plain, % 67.20/67.29 (E(f11(x31671,f11(a1,a2)),f11(x31671,f11(a7,a7)))), % 67.20/67.29 inference(scs_inference,[],[1810,10,12,8,9,7,11,5,6])). % 67.20/67.29 cnf(3169,plain, % 67.20/67.29 (~P4(f11(a7,f11(a1,a1)),f3(f11(a2,f11(a7,a7))))), % 67.20/67.29 inference(scs_inference,[],[3142,1810,10,12,8,9,7,11,5,6,4,43])). % 67.20/67.29 cnf(3172,plain, % 67.20/67.29 (E(f5(f11(a7,a7),f11(a7,a7)),f5(f11(a1,a1),f11(a1,a1)))), % 67.20/67.29 inference(scs_inference,[],[3153,3003,3007,3142,1810,10,12,8,9,7,11,5,6,4,43,2,3])). % 67.20/67.29 cnf(3175,plain, % 67.20/67.29 (P4(f3(f11(f11(x31751,a7),a1)),f11(f11(a2,x31751),a7))), % 67.20/67.29 inference(scs_inference,[],[3153,3003,3007,3142,2930,1810,33,10,12,8,9,7,11,5,6,4,43,2,3,42])). % 67.20/67.29 cnf(3178,plain, % 67.20/67.29 (P4(f3(f12(f11(a7,a7))),f12(f11(a2,a2)))), % 67.20/67.29 inference(scs_inference,[],[3153,3003,3007,3071,3142,2930,1810,86,33,10,12,8,9,7,11,5,6,4,43,2,3,42,15])). % 67.20/67.29 cnf(3183,plain, % 67.20/67.29 (~P2(f11(f12(a2),f11(a1,a1)),a9)), % 67.20/67.29 inference(scs_inference,[],[3153,2984,3003,3007,3037,3040,3071,3142,2930,2989,2895,1810,86,27,33,10,12,8,9,7,11,5,6,4,43,2,3,42,15,14,18,17])). % 67.20/67.29 cnf(3188,plain, % 67.20/67.29 (~E(f3(a9),f11(f12(a2),f11(a1,a1)))), % 67.20/67.29 inference(scs_inference,[],[3153,2984,3003,3007,3037,3040,3071,3142,2930,2989,2895,1810,86,27,33,10,12,8,9,7,11,5,6,4,43,2,3,42,15,14,18,17,41,60])). % 67.20/67.29 cnf(3198,plain, % 67.20/67.29 (E(f6(x31981,f11(x31982,a1)),f6(x31981,f11(a7,x31982)))), % 67.20/67.29 inference(scs_inference,[],[3178,1736,43,9,10,8,12])). % 67.20/67.29 cnf(3200,plain, % 67.20/67.29 (E(f11(x32001,f11(x32002,a1)),f11(x32001,f11(a7,x32002)))), % 67.20/67.29 inference(scs_inference,[],[3178,1736,43,9,10,8,12,7,6])). % 67.20/67.29 cnf(3202,plain, % 67.20/67.29 (E(f11(f11(x32021,a1),x32022),f11(f11(a7,x32021),x32022))), % 67.20/67.29 inference(scs_inference,[],[3178,1736,43,9,10,8,12,7,6,11,5])). % 67.20/67.29 cnf(3203,plain, % 67.20/67.29 (E(f3(f11(x32031,a1)),f3(f11(a7,x32031)))), % 67.20/67.29 inference(scs_inference,[],[3178,1736,43,9,10,8,12,7,6,11,5,4])). % 67.20/67.29 cnf(3205,plain, % 67.20/67.29 (P4(f3(f11(f11(a7,a7),a7)),f11(f11(a2,a2),a1))), % 67.20/67.29 inference(scs_inference,[],[3188,3072,3178,2217,1736,43,9,10,8,12,7,6,11,5,4,2,15])). % 67.20/67.29 cnf(3208,plain, % 67.20/67.29 (E(f6(f11(a7,a7),f11(a7,a7)),f6(f11(a1,a1),f11(a1,a1)))), % 67.20/67.29 inference(scs_inference,[],[3188,3004,3005,3072,3178,2217,1736,43,9,10,8,12,7,6,11,5,4,2,15,3])). % 67.20/67.29 cnf(3218,plain, % 67.20/67.29 (~E(f3(a9),f11(f11(a1,a2),f12(a2)))), % 67.20/67.29 inference(scs_inference,[],[3188,2979,3004,3005,3072,3166,3178,2859,2217,1736,2861,43,9,10,8,12,7,6,11,5,4,2,15,3,17,14,41,60])). % 67.20/67.29 cnf(3224,plain, % 67.20/67.29 (~P4(f11(f11(a2,a2),a1),f3(f11(f11(a7,a7),a7)))), % 67.20/67.29 inference(scs_inference,[],[3205,43])). % 67.20/67.29 cnf(3232,plain, % 67.20/67.29 (E(f11(x32321,f11(a1,x32322)),f11(x32321,f11(x32322,a7)))), % 67.20/67.29 inference(scs_inference,[],[3205,2429,43,8,9,10,12,7,11,6])). % 67.20/67.29 cnf(3233,plain, % 67.20/67.29 (E(f11(f11(a1,x32331),x32332),f11(f11(x32331,a7),x32332))), % 67.20/67.29 inference(scs_inference,[],[3205,2429,43,8,9,10,12,7,11,6,5])). % 67.20/67.29 cnf(3234,plain, % 67.20/67.29 (E(f3(f11(a1,x32341)),f3(f11(x32341,a7)))), % 67.20/67.29 inference(scs_inference,[],[3205,2429,43,8,9,10,12,7,11,6,5,4])). % 67.20/67.29 cnf(3236,plain, % 67.20/67.29 (P4(f3(f11(f11(a7,a7),a7)),f11(a2,f11(a2,a2)))), % 67.20/67.29 inference(scs_inference,[],[3218,3074,3205,2234,2429,43,8,9,10,12,7,11,6,5,4,2,15])). % 67.20/67.29 cnf(3237,plain, % 67.20/67.29 (E(f11(x32371,f11(a7,a7)),f11(x32371,f11(a2,a2)))), % 67.20/67.29 inference(rename_variables,[],[3074])). % 67.20/67.29 cnf(3239,plain, % 67.20/67.29 (E(f5(f11(a1,a1),f11(a1,a1)),f5(f11(a7,a7),f11(a7,a7)))), % 67.20/67.29 inference(scs_inference,[],[3218,3032,3035,3074,3205,2234,2429,43,8,9,10,12,7,11,6,5,4,2,15,3])). % 67.20/67.29 cnf(3242,plain, % 67.20/67.29 (~P2(f11(f12(a1),f11(a7,a7)),a9)), % 67.20/67.29 inference(scs_inference,[],[3218,3032,3035,3074,3133,3205,2234,2429,224,43,8,9,10,12,7,11,6,5,4,2,15,3,17])). % 67.20/67.29 cnf(3251,plain, % 67.20/67.29 (~E(f3(a9),f11(f12(a1),f11(a7,a7)))), % 67.20/67.29 inference(scs_inference,[],[1971,3218,3032,3035,3074,3237,3133,3205,2234,2429,224,30,22,43,8,9,10,12,7,11,6,5,4,2,15,3,17,14,13,41,60])). % 67.20/67.29 cnf(3269,plain, % 67.20/67.29 (E(f3(f11(x32691,a7)),f3(f11(a1,x32691)))), % 67.20/67.29 inference(scs_inference,[],[3236,2432,43,10,12,8,9,7,6,11,4])). % 67.20/67.29 cnf(3272,plain, % 67.20/67.29 (P4(f3(f12(f11(a7,a7))),f12(f11(a1,a2)))), % 67.20/67.29 inference(scs_inference,[],[3251,3131,3236,2432,86,43,10,12,8,9,7,6,11,4,5,2,15])). % 67.20/67.29 cnf(3274,plain, % 67.20/67.29 (E(f6(f11(a7,a7),f11(a1,a1)),f6(f11(a2,a1),f11(a2,a1)))), % 67.36/67.29 inference(scs_inference,[],[3251,3013,3033,3131,3236,2432,86,43,10,12,8,9,7,6,11,4,5,2,15,3])). % 67.36/67.29 cnf(3276,plain, % 67.36/67.29 (~P2(f11(f11(a7,a1),f12(a1)),a9)), % 67.36/67.29 inference(scs_inference,[],[3251,3088,3013,3033,3131,3202,3236,2432,86,43,10,12,8,9,7,6,11,4,5,2,15,3,17])). % 67.36/67.29 cnf(3278,plain, % 67.36/67.29 (P4(f3(f11(a2,f11(x32781,a7))),f11(a1,f11(x32781,a1)))), % 67.36/67.29 inference(scs_inference,[],[3251,3088,3013,3033,3131,3202,3236,3022,2432,86,33,43,10,12,8,9,7,6,11,4,5,2,15,3,17,42])). % 67.36/67.29 cnf(3287,plain, % 67.36/67.29 (~E(f3(a9),f11(f11(a7,a1),f12(a1)))), % 67.36/67.29 inference(scs_inference,[],[3251,3088,3013,3033,3131,3202,3236,3022,2432,91,86,27,33,43,10,12,8,9,7,6,11,4,5,2,15,3,17,42,14,18,41,60])). % 67.36/67.29 cnf(3301,plain, % 67.36/67.29 (E(f11(x33011,f11(a2,x33012)),f11(x33011,f11(x33012,a7)))), % 67.36/67.29 inference(scs_inference,[],[3272,2406,43,8,10,9,12,11,7,6])). % 67.36/67.29 cnf(3302,plain, % 67.36/67.29 (E(f11(f11(a2,x33021),x33022),f11(f11(x33021,a7),x33022))), % 67.36/67.29 inference(scs_inference,[],[3272,2406,43,8,10,9,12,11,7,6,5])). % 67.36/67.29 cnf(3303,plain, % 67.36/67.29 (E(f3(f11(a2,x33031)),f3(f11(x33031,a7)))), % 67.36/67.29 inference(scs_inference,[],[3272,2406,43,8,10,9,12,11,7,6,5,4])). % 67.36/67.29 cnf(3305,plain, % 67.36/67.29 (P4(f3(f11(f11(a7,a7),a2)),f11(f11(a1,a2),a1))), % 67.36/67.29 inference(scs_inference,[],[3287,3132,3272,988,2406,43,8,10,9,12,11,7,6,5,4,2,15])). % 67.36/67.29 cnf(3306,plain, % 67.36/67.29 (E(f11(f11(a7,a7),x33061),f11(f11(a1,a2),x33061))), % 67.36/67.29 inference(rename_variables,[],[3132])). % 67.36/67.29 cnf(3311,plain, % 67.36/67.29 (~P2(f11(f12(a1),f11(a7,a1)),a9)), % 67.36/67.29 inference(scs_inference,[],[3287,3242,3036,3067,3132,3200,3272,988,2406,43,8,10,9,12,11,7,6,5,4,2,15,3,17])). % 67.36/67.29 cnf(3318,plain, % 67.36/67.29 (~E(f3(a9),f11(f12(a1),f11(a7,a1)))), % 67.36/67.29 inference(scs_inference,[],[35,3287,3242,3036,3067,3132,3306,3200,3272,988,2406,43,8,10,9,12,11,7,6,5,4,2,15,3,17,14,41,60])). % 67.36/67.29 cnf(3331,plain, % 67.36/67.29 (E(f11(x33311,f11(x33312,a2)),f11(x33311,f11(x33312,a7)))), % 67.36/67.29 inference(scs_inference,[],[3305,2339,43,9,12,8,10,11,6])). % 67.36/67.29 cnf(3334,plain, % 67.36/67.29 (E(f11(f11(x33341,a2),x33342),f11(f11(x33341,a7),x33342))), % 67.36/67.29 inference(scs_inference,[],[3305,2339,1640,43,9,12,8,10,11,6,7,4,5])). % 67.36/67.29 cnf(3336,plain, % 67.36/67.29 (P4(f3(f11(f11(a1,a2),a1)),f11(a2,f11(a7,a7)))), % 67.36/67.29 inference(scs_inference,[],[3318,3167,3305,675,2339,1640,43,9,12,8,10,11,6,7,4,5,2,15])). % 67.36/67.29 cnf(3337,plain, % 67.36/67.29 (E(f11(x33371,f11(a1,a2)),f11(x33371,f11(a7,a7)))), % 67.36/67.29 inference(rename_variables,[],[3167])). % 67.36/67.29 cnf(3339,plain, % 67.36/67.29 (E(f5(f11(a7,a7),f11(a7,a7)),f5(f11(a2,a2),f11(a2,a2)))), % 67.36/67.29 inference(scs_inference,[],[3318,3069,3070,3167,3305,675,2339,1640,43,9,12,8,10,11,6,7,4,5,2,15,3])). % 67.36/67.29 cnf(3344,plain, % 67.36/67.29 (E(f11(x33441,f11(a1,a2)),f11(x33441,f11(a7,a7)))), % 67.36/67.29 inference(rename_variables,[],[3167])). % 67.36/67.29 cnf(3350,plain, % 67.36/67.29 (~E(f3(a9),f11(f12(a2),f11(a1,a2)))), % 67.36/67.29 inference(scs_inference,[],[1974,3318,3069,3070,3167,3337,3344,3305,675,2895,2339,1640,43,9,12,8,10,11,6,7,4,5,2,15,3,17,14,41,60])). % 67.36/67.29 cnf(3357,plain, % 67.36/67.29 (~P4(f11(a2,f11(a7,a7)),f3(f11(f11(a1,a2),a1)))), % 67.36/67.29 inference(scs_inference,[],[3336,43])). % 67.36/67.29 cnf(3359,plain, % 67.36/67.29 (E(f6(x33591,f11(a2,a7)),f6(x33591,f11(a1,a1)))), % 67.36/67.29 inference(scs_inference,[],[3336,1673,43,12])). % 67.36/67.29 cnf(3360,plain, % 67.36/67.29 (E(f5(f11(a2,a7),x33601),f5(f11(a1,a1),x33601))), % 67.36/67.29 inference(scs_inference,[],[3336,1673,43,12,9])). % 67.36/67.29 cnf(3361,plain, % 67.36/67.29 (E(f5(x33611,f11(a2,a7)),f5(x33611,f11(a1,a1)))), % 67.36/67.29 inference(scs_inference,[],[3336,1673,43,12,9,10])). % 67.36/67.29 cnf(3364,plain, % 67.36/67.29 (E(f6(f11(a2,a7),x33641),f6(f11(a1,a1),x33641))), % 67.36/67.29 inference(scs_inference,[],[3336,1673,43,12,9,10,8,7,11])). % 67.36/67.29 cnf(3365,plain, % 67.36/67.29 (E(f11(x33651,f11(a2,a7)),f11(x33651,f11(a1,a1)))), % 67.36/67.29 inference(scs_inference,[],[3336,1673,43,12,9,10,8,7,11,6])). % 67.36/67.29 cnf(3367,plain, % 67.36/67.29 (E(f11(f11(a2,a7),x33671),f11(f11(a1,a1),x33671))), % 67.36/67.29 inference(scs_inference,[],[3336,1673,43,12,9,10,8,7,11,6,4,5])). % 67.36/67.29 cnf(3369,plain, % 67.36/67.29 (P4(f3(f11(f11(a7,a7),a1)),f11(f11(a2,a2),a7))), % 67.36/67.29 inference(scs_inference,[],[3350,2916,3336,3175,1673,43,12,9,10,8,7,11,6,4,5,2,15])). % 67.36/67.29 cnf(3373,plain, % 67.36/67.29 (E(f6(f11(a7,a7),x33731),f6(f11(a2,a2),x33731))), % 67.36/67.29 inference(rename_variables,[],[3073])). % 67.36/67.29 cnf(3377,plain, % 67.36/67.29 (P2(f3(f6(f11(a7,a7),x33771)),f6(f11(a2,a2),x33771))), % 67.36/67.29 inference(scs_inference,[],[3350,3073,3373,3127,2916,3301,3336,3175,3242,1673,27,43,12,9,10,8,7,11,6,4,5,2,15,3,17,18])). % 67.36/67.29 cnf(3384,plain, % 67.36/67.29 (~E(f3(a9),f11(f12(a1),f11(a2,a7)))), % 67.36/67.29 inference(scs_inference,[],[2016,3350,3073,3373,3127,2916,2917,3301,3336,3175,3242,1673,27,43,12,9,10,8,7,11,6,4,5,2,15,3,17,18,14,41,60])). % 67.36/67.29 cnf(3391,plain, % 67.36/67.29 (~P4(f11(f11(a2,a2),a7),f3(f11(f11(a7,a7),a1)))), % 67.36/67.29 inference(scs_inference,[],[3369,43])). % 67.36/67.29 cnf(3393,plain, % 67.36/67.29 (E(f5(f11(a7,a1),x33931),f5(f11(a2,a2),x33931))), % 67.36/67.29 inference(scs_inference,[],[3369,1629,43,9])). % 67.36/67.29 cnf(3394,plain, % 67.36/67.29 (E(f6(x33941,f11(a7,a1)),f6(x33941,f11(a2,a2)))), % 67.36/67.29 inference(scs_inference,[],[3369,1629,43,9,12])). % 67.36/67.29 cnf(3396,plain, % 67.36/67.29 (E(f5(x33961,f11(a7,a1)),f5(x33961,f11(a2,a2)))), % 67.36/67.29 inference(scs_inference,[],[3369,1629,43,9,12,8,10])). % 67.36/67.29 cnf(3397,plain, % 67.36/67.29 (E(f11(x33971,f11(a7,a1)),f11(x33971,f11(a2,a2)))), % 67.36/67.29 inference(scs_inference,[],[3369,1629,43,9,12,8,10,6])). % 67.36/67.29 cnf(3398,plain, % 67.36/67.29 (E(f12(f11(a7,a1)),f12(f11(a2,a2)))), % 67.36/67.29 inference(scs_inference,[],[3369,1629,43,9,12,8,10,6,7])). % 67.36/67.29 cnf(3399,plain, % 67.36/67.29 (E(f6(f11(a7,a1),x33991),f6(f11(a2,a2),x33991))), % 67.36/67.29 inference(scs_inference,[],[3369,1629,43,9,12,8,10,6,7,11])). % 67.36/67.29 cnf(3401,plain, % 67.36/67.29 (E(f11(f11(a7,a1),x34011),f11(f11(a2,a2),x34011))), % 67.36/67.29 inference(scs_inference,[],[3369,1629,43,9,12,8,10,6,7,11,4,5])). % 67.36/67.29 cnf(3405,plain, % 67.36/67.29 (E(f6(f11(a2,a1),f11(a2,a1)),f6(f11(a1,a2),f11(a7,a7)))), % 67.36/67.29 inference(scs_inference,[],[3384,3077,3134,3269,3369,2934,1629,43,9,12,8,10,6,7,11,4,5,2,15,3])). % 67.36/67.29 cnf(3407,plain, % 67.36/67.29 (~P2(f11(f11(a1,x34071),f12(a2)),a9)), % 67.36/67.29 inference(scs_inference,[],[3384,3077,3134,3233,3269,3369,2934,1629,2861,43,9,12,8,10,6,7,11,4,5,2,15,3,17])). % 67.36/67.29 cnf(3413,plain, % 67.36/67.29 (~E(f3(a9),f11(f11(a1,x34131),f12(a2)))), % 67.36/67.29 inference(scs_inference,[],[2019,3384,3077,3134,3365,3233,3269,3369,2934,1629,2861,43,9,12,8,10,6,7,11,4,5,2,15,3,17,14,60])). % 67.36/67.29 cnf(3422,plain, % 67.36/67.29 (E(f6(x34221,f11(a7,a2)),f6(x34221,f11(a1,a1)))), % 67.36/67.29 inference(scs_inference,[],[3278,1630,43,12])). % 67.36/67.29 cnf(3423,plain, % 67.36/67.29 (E(f5(f11(a7,a2),x34231),f5(f11(a1,a1),x34231))), % 67.36/67.29 inference(scs_inference,[],[3278,1630,43,12,9])). % 67.36/67.29 cnf(3424,plain, % 67.36/67.29 (E(f5(x34241,f11(a7,a2)),f5(x34241,f11(a1,a1)))), % 67.36/67.29 inference(scs_inference,[],[3278,1630,43,12,9,10])). % 67.36/67.29 cnf(3427,plain, % 67.36/67.29 (E(f11(x34271,f11(a7,a2)),f11(x34271,f11(a1,a1)))), % 67.36/67.29 inference(scs_inference,[],[3278,1630,43,12,9,10,8,11,6])). % 67.36/67.29 cnf(3428,plain, % 67.36/67.29 (E(f11(f11(a7,a2),x34281),f11(f11(a1,a1),x34281))), % 67.36/67.29 inference(scs_inference,[],[3278,1630,43,12,9,10,8,11,6,5])). % 67.36/67.29 cnf(3430,plain, % 67.36/67.29 (E(f12(f11(a7,a2)),f12(f11(a1,a1)))), % 67.36/67.29 inference(scs_inference,[],[3278,1630,43,12,9,10,8,11,6,5,4,7])). % 67.36/67.29 cnf(3432,plain, % 67.36/67.29 (P4(f3(f11(f11(a2,a7),a1)),f11(f11(a1,a1),a2))), % 67.36/67.29 inference(scs_inference,[],[3413,3367,3278,689,1630,43,12,9,10,8,11,6,5,4,7,2,15])). % 67.36/67.29 cnf(3433,plain, % 67.36/67.29 (E(f11(f11(a2,a7),x34331),f11(f11(a1,a1),x34331))), % 67.36/67.29 inference(rename_variables,[],[3367])). % 67.36/67.29 cnf(3441,plain, % 67.36/67.29 (~E(a2,f11(x34411,x34412))), % 67.36/67.29 inference(scs_inference,[],[3413,3128,3130,3367,3397,3278,689,1630,224,21,33,43,12,9,10,8,11,6,5,4,7,2,15,3,17,13])). % 67.36/67.29 cnf(3442,plain, % 67.36/67.29 (~P4(f11(f11(a2,a7),f12(a1)),a9)), % 67.36/67.29 inference(scs_inference,[],[35,3413,3128,3130,3367,3433,3397,3278,689,1630,224,21,33,43,12,9,10,8,11,6,5,4,7,2,15,3,17,13,14])). % 67.36/67.29 cnf(3447,plain, % 67.36/67.29 (~E(f3(a9),f11(f12(a2),f11(a7,a1)))), % 67.36/67.29 inference(scs_inference,[],[35,3413,3128,3130,3367,3433,3397,3278,689,1630,224,21,33,43,12,9,10,8,11,6,5,4,7,2,15,3,17,13,14,41,60])). % 67.36/67.29 cnf(3454,plain, % 67.36/67.29 (~P4(f11(f11(a1,a1),a2),f3(f11(f11(a2,a7),a1)))), % 67.36/67.29 inference(scs_inference,[],[3432,43])). % 67.36/67.29 cnf(3460,plain, % 67.36/67.29 (E(f11(f11(a2,a2),x34601),f11(f11(a7,a7),x34601))), % 67.36/67.29 inference(scs_inference,[],[3432,1826,43,9,12,8,10,5])). % 67.36/67.29 cnf(3462,plain, % 67.36/67.29 (E(f12(f11(a2,a2)),f12(f11(a7,a7)))), % 67.36/67.29 inference(scs_inference,[],[3432,1826,43,9,12,8,10,5,4,7])). % 67.36/67.29 cnf(3464,plain, % 67.36/67.29 (E(f11(x34641,f11(a2,a2)),f11(x34641,f11(a7,a7)))), % 67.36/67.29 inference(scs_inference,[],[3432,1826,43,9,12,8,10,5,4,7,11,6])). % 67.36/67.29 cnf(3471,plain, % 67.36/67.29 (~P2(f11(f11(a2,a7),f12(a1)),a9)), % 67.36/67.29 inference(scs_inference,[],[3447,3183,3442,3139,3172,3427,3234,3432,3026,1826,46,43,9,12,8,10,5,4,7,11,6,2,15,3,17,42])). % 67.36/67.29 cnf(3473,plain, % 67.36/67.29 (~P4(f11(f11(a7,a1),f12(a2)),a9)), % 67.36/67.29 inference(scs_inference,[],[35,3447,3183,3442,3139,3172,3401,3427,3234,3432,3026,1826,46,43,9,12,8,10,5,4,7,11,6,2,15,3,17,42,14])). % 67.36/67.29 cnf(3476,plain, % 67.36/67.29 (~E(f3(a9),f11(f12(a2),f11(a7,a2)))), % 67.36/67.29 inference(scs_inference,[],[35,3447,3183,3442,3139,3172,3401,3427,3234,3432,3026,1826,46,43,9,12,8,10,5,4,7,11,6,2,15,3,17,42,14,60])). % 67.36/67.29 cnf(3490,plain, % 67.36/67.29 (E(f11(x34901,f11(a2,x34902)),f11(x34901,f11(a7,x34902)))), % 67.36/67.29 inference(scs_inference,[],[3175,1785,43,12,9,10,8,7,11,6])). % 67.36/67.29 cnf(3491,plain, % 67.36/67.29 (E(f11(f11(a2,x34911),x34912),f11(f11(a7,x34911),x34912))), % 67.36/67.29 inference(scs_inference,[],[3175,1785,43,12,9,10,8,7,11,6,5])). % 67.36/67.29 cnf(3493,plain, % 67.36/67.29 (~E(f3(a9),f11(f11(a2,a7),f12(a1)))), % 67.36/67.29 inference(scs_inference,[],[3471,3175,1785,43,12,9,10,8,7,11,6,5,4,60])). % 67.36/67.29 cnf(3495,plain, % 67.36/67.29 (P4(f3(f12(f11(a7,a1))),f12(f11(a2,a2)))), % 67.36/67.29 inference(scs_inference,[],[3476,3471,3398,3175,1785,86,43,12,9,10,8,7,11,6,5,4,60,2,15])). % 67.36/67.29 cnf(3500,plain, % 67.36/67.29 (~P2(f11(f11(a7,a2),f12(a2)),a9)), % 67.36/67.29 inference(scs_inference,[],[3476,3471,3407,3160,3163,3398,3428,3175,1785,86,43,12,9,10,8,7,11,6,5,4,60,2,15,3,17])). % 67.36/67.29 cnf(3521,plain, % 67.36/67.29 (E(f11(f11(a7,x35211),x35212),f11(f11(x35211,a1),x35212))), % 67.36/67.29 inference(scs_inference,[],[3495,1738,43,12,10,8,9,7,11,5])). % 67.36/67.29 cnf(3522,plain, % 67.36/67.29 (E(f11(x35221,f11(a7,x35222)),f11(x35221,f11(x35222,a1)))), % 67.36/67.29 inference(scs_inference,[],[3495,1738,43,12,10,8,9,7,11,5,6])). % 67.36/67.29 cnf(3523,plain, % 67.36/67.29 (E(f3(f11(a7,x35231)),f3(f11(x35231,a1)))), % 67.36/67.29 inference(scs_inference,[],[3495,1738,43,12,10,8,9,7,11,5,6,4])). % 67.36/67.29 cnf(3524,plain, % 67.36/67.29 (~E(f3(a9),f11(f11(a7,a2),f12(a2)))), % 67.36/67.29 inference(scs_inference,[],[3500,3495,1738,43,12,10,8,9,7,11,5,6,4,60])). % 67.36/67.29 cnf(3529,plain, % 67.36/67.29 (E(f6(x35291,f11(a1,a2)),f6(x35291,f11(a7,a7)))), % 67.36/67.29 inference(rename_variables,[],[3161])). % 67.36/67.29 cnf(3531,plain, % 67.36/67.29 (~P2(f11(f11(a2,a1),f12(a1)),a9)), % 67.36/67.29 inference(scs_inference,[],[3493,3276,3500,3161,3165,3491,2882,3495,3060,1738,43,12,10,8,9,7,11,5,6,4,60,2,15,3,17])). % 67.36/67.29 cnf(3536,plain, % 67.36/67.29 (~P4(f11(f11(a2,a2),f12(a7)),a9)), % 67.36/67.29 inference(scs_inference,[],[35,3493,3276,3500,3161,3529,3165,3460,3491,2882,3377,3495,3060,1738,43,12,10,8,9,7,11,5,6,4,60,2,15,3,17,18,14])). % 67.36/67.29 cnf(3552,plain, % 67.36/67.29 (E(f11(f11(x35521,a1),x35522),f11(f11(x35521,a7),x35522))), % 67.36/67.29 inference(scs_inference,[],[3524,2384,2,8,9,10,12,11,7,6,5])). % 67.36/67.29 cnf(3553,plain, % 67.36/67.29 (E(f3(f11(x35531,a1)),f3(f11(x35531,a7)))), % 67.36/67.29 inference(scs_inference,[],[3524,2384,2,8,9,10,12,11,7,6,5,4])). % 67.36/67.29 cnf(3554,plain, % 67.36/67.29 (~E(f3(a9),f11(f11(a2,a1),f12(a1)))), % 67.36/67.29 inference(scs_inference,[],[3524,3531,2384,2,8,9,10,12,11,7,6,5,4,60])). % 67.36/67.29 cnf(3559,plain, % 67.36/67.29 (~P2(f11(f12(a1),f11(a2,a2)),a9)), % 67.36/67.29 inference(scs_inference,[],[3524,3531,3208,3430,3464,3198,3242,2384,86,2,8,9,10,12,11,7,6,5,4,60,15,3,17])). % 67.36/67.29 cnf(3561,plain, % 67.36/67.29 (~P2(f11(f11(a7,a1),f12(a2)),a9)), % 67.36/67.29 inference(scs_inference,[],[3524,3473,3531,3208,3430,3464,3198,3242,2384,86,46,2,8,9,10,12,11,7,6,5,4,60,15,3,17,42])). % 67.36/67.29 cnf(3579,plain, % 67.36/67.29 (E(f11(f11(a1,a1),x35791),f11(f11(a7,a2),x35791))), % 67.36/67.29 inference(scs_inference,[],[3554,1640,2,10,12,9,8,7,11,5])). % 67.36/67.29 cnf(3582,plain, % 67.36/67.29 (~E(f3(a9),f11(f12(a1),f11(a2,a2)))), % 67.36/67.29 inference(scs_inference,[],[3554,3559,1640,1659,2,10,12,9,8,7,11,5,6,4,60])). % 67.36/67.29 cnf(3586,plain, % 67.36/67.29 (~P2(f11(f12(a1),f11(a2,a1)),a9)), % 67.36/67.29 inference(scs_inference,[],[3554,3311,3559,3239,3339,3490,3203,3094,1640,1659,2,10,12,9,8,7,11,5,6,4,60,15,3,17])). % 67.36/67.29 cnf(3607,plain, % 67.36/67.29 (E(f12(f11(a1,a7)),f12(f11(a2,a2)))), % 67.36/67.29 inference(scs_inference,[],[3582,1596,2,9,8,12,10,11,7])). % 67.36/67.29 cnf(3609,plain, % 67.36/67.29 (E(f11(f11(a1,a7),x36091),f11(f11(a2,a2),x36091))), % 67.36/67.29 inference(scs_inference,[],[3582,1596,2,9,8,12,10,11,7,6,5])). % 67.36/67.29 cnf(3611,plain, % 67.36/67.29 (~E(f3(a9),f11(f11(a7,a1),f12(a2)))), % 67.36/67.29 inference(scs_inference,[],[3582,3561,1596,2,9,8,12,10,11,7,6,5,4,60])). % 67.36/67.29 cnf(3615,plain, % 67.36/67.29 (~P2(f11(f11(a7,a2),f12(a1)),a9)), % 67.36/67.29 inference(scs_inference,[],[3582,3561,3274,3405,3462,3334,2857,3088,1596,2,9,8,12,10,11,7,6,5,4,60,15,3,17])). % 67.36/67.29 cnf(3617,plain, % 67.36/67.29 (~P2(f11(f11(a2,a2),f12(a7)),a9)), % 67.36/67.29 inference(scs_inference,[],[3582,3536,3561,3274,3405,3462,3334,2857,3088,1596,46,2,9,8,12,10,11,7,6,5,4,60,15,3,17,42])). % 67.36/67.29 cnf(3633,plain, % 67.36/67.29 (E(f12(f11(a2,a2)),f12(f11(a7,a1)))), % 67.36/67.29 inference(scs_inference,[],[3611,1618,2,12,8,9,10,11,7])). % 67.36/67.29 cnf(3634,plain, % 67.36/67.29 (E(f11(x36341,f11(a2,a2)),f11(x36341,f11(a7,a1)))), % 67.36/67.29 inference(scs_inference,[],[3611,1618,2,12,8,9,10,11,7,6])). % 67.36/67.29 cnf(3637,plain, % 67.36/67.29 (~E(f3(a9),f11(f12(a1),f11(a2,a1)))), % 67.36/67.29 inference(scs_inference,[],[3611,3586,1618,2,12,8,9,10,11,7,6,5,4,60])). % 67.36/67.29 cnf(3643,plain, % 67.36/67.29 (~P2(f11(f12(a1),f11(a7,a2)),a9)), % 67.36/67.29 inference(scs_inference,[],[3611,3586,3359,3364,3522,3523,3357,1618,2,12,8,9,10,11,7,6,5,4,60,15,3,17])). % 67.36/67.29 cnf(3663,plain, % 67.36/67.29 (E(f11(f11(a7,x36631),x36632),f11(f11(a2,x36631),x36632))), % 67.36/67.29 inference(scs_inference,[],[3637,1781,2,9,8,10,12,6,11,7,5])). % 67.36/67.29 cnf(3664,plain, % 67.36/67.29 (E(f3(f11(a7,x36641)),f3(f11(a2,x36641)))), % 67.36/67.29 inference(scs_inference,[],[3637,1781,2,9,8,10,12,6,11,7,5,4])). % 67.36/67.29 cnf(3665,plain, % 67.36/67.29 (~E(f3(a9),f11(f11(a7,a2),f12(a1)))), % 67.36/67.29 inference(scs_inference,[],[3637,3615,1781,2,9,8,10,12,6,11,7,5,4,60])). % 67.36/67.29 cnf(3667,plain, % 67.36/67.29 (E(f11(f11(a1,a1),x36671),f11(f11(a7,a2),x36671))), % 67.36/67.29 inference(rename_variables,[],[3579])). % 67.36/67.29 cnf(3672,plain, % 67.36/67.29 (~P2(f11(f11(a1,a7),f12(a7)),a9)), % 67.36/67.29 inference(scs_inference,[],[3637,3615,3617,3360,3361,3579,3609,113,1781,2,9,8,10,12,6,11,7,5,4,60,15,3,17])). % 67.36/67.29 cnf(3677,plain, % 67.36/67.29 (P2(f3(f11(f11(a1,a1),x36771)),f11(f11(a7,a2),x36771))), % 67.36/67.29 inference(scs_inference,[],[2193,3637,3615,3617,3360,3361,3579,3667,3609,113,1781,2,9,8,10,12,6,11,7,5,4,60,15,3,17,14,41])). % 67.36/67.29 cnf(3679,plain, % 67.36/67.29 (~P4(f11(f11(a7,a2),x36791),f3(f11(f11(a1,a1),x36791)))), % 67.36/67.29 inference(scs_inference,[],[2193,3637,3615,3617,3360,3361,3579,3667,3609,113,1781,2,9,8,10,12,6,11,7,5,4,60,15,3,17,14,41,43])). % 67.36/67.29 cnf(3698,plain, % 67.36/67.29 (~E(f3(a9),f11(f12(a1),f11(a7,a2)))), % 67.36/67.29 inference(scs_inference,[],[3665,3643,1659,1586,2,10,8,9,12,7,11,6,5,4,60])). % 67.36/67.29 cnf(3705,plain, % 67.36/67.29 (~P2(f11(f11(a2,a2),f12(a1)),a9)), % 67.36/67.29 inference(scs_inference,[],[3665,3643,3393,3396,3302,2853,3679,3471,1659,1586,2,10,8,9,12,7,11,6,5,4,60,15,3,17])). % 67.36/67.29 cnf(3718,plain, % 67.36/67.29 (E(f5(x37181,a1),f5(x37181,a7))), % 67.36/67.29 inference(scs_inference,[],[3698,526,2,10])). % 67.36/67.30 cnf(3719,plain, % 67.36/67.30 (E(f6(x37191,a1),f6(x37191,a7))), % 67.36/67.30 inference(scs_inference,[],[3698,526,2,10,12])). % 67.36/67.30 cnf(3720,plain, % 67.36/67.30 (E(f4(a1),f4(a7))), % 67.36/67.30 inference(scs_inference,[],[3698,526,2,10,12,8])). % 67.36/67.30 cnf(3721,plain, % 67.36/67.30 (E(f5(a1,x37211),f5(a7,x37211))), % 67.36/67.30 inference(scs_inference,[],[3698,526,2,10,12,8,9])). % 67.36/67.30 cnf(3722,plain, % 67.36/67.30 (E(f12(a1),f12(a7))), % 67.36/67.30 inference(scs_inference,[],[3698,526,2,10,12,8,9,7])). % 67.36/67.30 cnf(3723,plain, % 67.36/67.30 (E(f6(a1,x37231),f6(a7,x37231))), % 67.36/67.30 inference(scs_inference,[],[3698,526,2,10,12,8,9,7,11])). % 67.36/67.30 cnf(3725,plain, % 67.36/67.30 (E(f11(f11(a2,x37251),x37252),f11(f11(a1,x37251),x37252))), % 67.36/67.30 inference(scs_inference,[],[3698,526,556,2,10,12,8,9,7,11,6,5])). % 67.36/67.30 cnf(3727,plain, % 67.36/67.30 (~E(f3(a9),f11(f11(a1,a7),f12(a7)))), % 67.36/67.30 inference(scs_inference,[],[3698,3672,526,556,2,10,12,8,9,7,11,6,5,4,60])). % 67.36/67.30 cnf(3728,plain, % 67.36/67.30 (P4(f3(f12(f11(a1,a7))),f12(f11(a2,a2)))), % 67.36/67.30 inference(scs_inference,[],[3698,3672,3607,526,556,86,2,10,12,8,9,7,11,6,5,4,60,15])). % 67.36/67.30 cnf(3731,plain, % 67.36/67.30 (~P2(f11(f11(a1,a1),f12(a7)),a9)), % 67.36/67.30 inference(scs_inference,[],[3012,3698,3672,3607,3552,526,556,86,331,2,10,12,8,9,7,11,6,5,4,60,15,3,17])). % 67.36/67.30 cnf(3755,plain, % 67.36/67.30 (~E(f3(a9),f11(f11(a2,a2),f12(a1)))), % 67.36/67.30 inference(scs_inference,[],[3718,3727,3705,2,10,9,12,7,11,8,6,5,4,60])). % 67.36/67.30 cnf(3758,plain, % 67.36/67.30 (E(f5(a1,a1),f5(a7,a7))), % 67.36/67.30 inference(scs_inference,[],[3718,3721,3727,3705,3391,2882,2,10,9,12,7,11,8,6,5,4,60,15,3])). % 67.36/67.30 cnf(3761,plain, % 67.36/67.30 (~P2(f11(f11(a2,a7),f12(a7)),a9)), % 67.36/67.30 inference(scs_inference,[],[3718,3721,3727,3705,3725,3391,2882,3672,2,10,9,12,7,11,8,6,5,4,60,15,3,17])). % 67.36/67.30 cnf(3781,plain, % 67.36/67.30 (~E(f3(a9),f11(f11(a1,a1),f12(a7)))), % 67.36/67.30 inference(scs_inference,[],[3719,3755,3731,2,10,7,9,11,12,8,6,5,4,60])). % 67.36/67.30 cnf(3786,plain, % 67.36/67.30 (P2(f3(f11(f11(a7,a7),a7)),f11(a7,f11(a1,a1)))), % 67.36/67.30 inference(scs_inference,[],[20,3719,3011,3722,3755,3731,3303,3151,32,86,331,2,10,7,9,11,12,8,6,5,4,60,15,3,13,17])). % 67.36/67.30 cnf(3810,plain, % 67.36/67.30 (~E(f3(a9),f11(f11(a2,a7),f12(a7)))), % 67.36/67.30 inference(scs_inference,[],[3723,3781,3761,2,10,8,12,7,11,9,4,6,5,60])). % 67.36/67.30 cnf(3819,plain, % 67.36/67.30 (~P2(f11(f12(a7),f11(a2,a2)),a9)), % 67.36/67.30 inference(scs_inference,[],[3723,3781,3761,3394,3634,3664,3786,3169,224,33,2,10,8,12,7,11,9,4,6,5,60,15,3,42,17])). % 67.36/67.30 cnf(3845,plain, % 67.36/67.30 (~E(f3(a9),f11(f12(a7),f11(a2,a2)))), % 67.36/67.30 inference(scs_inference,[],[3720,3810,3819,2,10,8,9,11,7,12,5,4,6,60])). % 67.36/67.30 cnf(3848,plain, % 67.36/67.30 (P2(f3(f11(f11(a1,a1),a7)),f11(f11(a7,a2),a1))), % 67.36/67.30 inference(scs_inference,[],[3441,3720,3810,3819,3633,3553,3677,3728,331,2,10,8,9,11,7,12,5,4,6,60,15,3,17])). % 67.36/67.30 cnf(3887,plain, % 67.36/67.30 (~P2(f11(f12(a2),f11(a1,x38871)),a9)), % 67.36/67.30 inference(scs_inference,[],[3758,2225,3845,3399,3422,3232,3521,3848,3454,3617,3523,2895,33,60,2,10,12,8,7,11,9,6,5,4,14,15,3,42,17])). % 67.36/67.30 cnf(3899,plain, % 67.36/67.30 (~E(f3(a9),f11(f12(a2),f11(a1,x38991)))), % 67.36/67.30 inference(scs_inference,[],[3887,60])). % 67.36/67.30 cnf(3944,plain, % 67.36/67.30 (E(f5(f11(a7,a2),x39441),f5(f11(a1,a1),x39441))), % 67.36/67.30 inference(rename_variables,[],[3423])). % 67.36/67.30 cnf(3952,plain, % 67.36/67.30 (~E(f3(a9),f11(f12(a2),f11(x39521,a2)))), % 67.36/67.30 inference(scs_inference,[],[2824,3899,3423,3944,3424,3331,3663,3224,2918,3722,2895,27,2,10,8,12,7,11,9,5,6,4,14,15,3,17,18,93,60])). % 67.36/67.30 cnf(3969,plain, % 67.36/67.30 (E(f11(f11(a2,a2),x39691),f11(f11(a1,a1),x39691))), % 67.36/67.30 inference(scs_inference,[],[3952,588,2,10,8,11,12,9,7,5])). % 67.36/67.30 cnf(4005,plain, % 67.36/67.30 ($false), % 67.36/67.30 inference(scs_inference,[],[2827,3969,67,2116,1586,1585,26,2,10,8,7,12,11,9,6,5,4,14,45]), % 67.36/67.30 ['proof']). % 67.36/67.30 % SZS output end Proof % 67.36/67.30 % Total time :66.630000s %------------------------------------------------------------------------------