%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SEU174+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 : n027.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:33 EDT 2024 % Result : Theorem 58.65s 58.70s % Output : CNFRefutation 58.65s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SEU174+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.11/0.32 % Computer : n027.cluster.edu % 0.11/0.32 % Model : x86_64 x86_64 % 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.32 % Memory : 8042.1875MB % 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.32 % CPULimit : 300 % 0.11/0.32 % WCLimit : 300 % 0.11/0.32 % DateTime : Fri Jun 21 12:15:24 EDT 2024 % 0.11/0.33 % CPUTime : % 0.19/0.56 start to proof:theBenchmark % 58.65/58.68 %------------------------------------------- % 58.65/58.68 % File :CSE---1.7 % 58.65/58.68 % Problem :theBenchmark % 58.65/58.68 % Transform :cnf % 58.65/58.68 % Format :tptp:raw % 58.65/58.68 % Command :java -jar mcs_scs.jar %d %s % 58.65/58.68 % 58.65/58.68 % Result :Theorem 58.090000s % 58.65/58.68 % Output :CNFRefutation 58.090000s % 58.65/58.68 %------------------------------------------- % 58.65/58.69 %------------------------------------------------------------------------------ % 58.65/58.69 % File : SEU174+1 : TPTP v8.2.0. Released v3.3.0. % 58.65/58.69 % Domain : Set theory % 58.65/58.69 % Problem : MPTP bushy problem t46_setfam_1 % 58.65/58.69 % Version : [Urb07] axioms : Especial. % 58.65/58.69 % English : % 58.65/58.69 % 58.65/58.69 % Refs : [Ban01] Bancerek et al. (2001), On the Characterizations of Co % 58.65/58.69 % : [Urb07] Urban (2006), Email to G. Sutcliffe % 58.65/58.69 % Source : [Urb07] % 58.65/58.69 % Names : bushy-t46_setfam_1 [Urb07] % 58.65/58.69 % 58.65/58.69 % Status : Theorem % 58.65/58.69 % Rating : 0.25 v8.2.0, 0.22 v7.5.0, 0.25 v7.4.0, 0.17 v7.2.0, 0.14 v7.1.0, 0.17 v7.0.0, 0.13 v6.4.0, 0.19 v6.3.0, 0.21 v6.2.0, 0.24 v6.1.0, 0.33 v6.0.0, 0.26 v5.5.0, 0.33 v5.4.0, 0.36 v5.3.0, 0.37 v5.2.0, 0.15 v5.1.0, 0.14 v5.0.0, 0.21 v4.1.0, 0.22 v4.0.1, 0.26 v4.0.0, 0.29 v3.7.0, 0.20 v3.5.0, 0.21 v3.4.0, 0.32 v3.3.0 % 58.65/58.69 % Syntax : Number of formulae : 27 ( 9 unt; 0 def) % 58.65/58.69 % Number of atoms : 56 ( 7 equ) % 58.65/58.69 % Maximal formula atoms : 6 ( 2 avg) % 58.65/58.69 % Number of connectives : 40 ( 11 ~; 1 |; 9 &) % 58.65/58.69 % ( 4 <=>; 15 =>; 0 <=; 0 <~>) % 58.65/58.69 % Maximal formula depth : 10 ( 4 avg) % 58.65/58.69 % Maximal term depth : 3 ( 1 avg) % 58.65/58.69 % Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty) % 58.65/58.69 % Number of functors : 4 ( 4 usr; 1 con; 0-2 aty) % 58.65/58.69 % Number of variables : 47 ( 42 !; 5 ?) % 58.65/58.69 % SPC : FOF_THM_RFO_SEQ % 58.65/58.69 % 58.65/58.69 % Comments : Translated by MPTP 0.2 from the original problem in the Mizar % 58.65/58.69 % library, www.mizar.org % 58.65/58.69 %------------------------------------------------------------------------------ % 58.65/58.69 fof(antisymmetry_r2_hidden,axiom, % 58.65/58.69 ! [A,B] : % 58.65/58.69 ( in(A,B) % 58.65/58.69 => ~ in(B,A) ) ). % 58.65/58.69 % 58.65/58.69 fof(d3_tarski,axiom, % 58.65/58.69 ! [A,B] : % 58.65/58.69 ( subset(A,B) % 58.65/58.69 <=> ! [C] : % 58.65/58.69 ( in(C,A) % 58.65/58.69 => in(C,B) ) ) ). % 58.65/58.69 % 58.65/58.69 fof(d8_setfam_1,axiom, % 58.65/58.69 ! [A,B] : % 58.65/58.69 ( element(B,powerset(powerset(A))) % 58.65/58.69 => ! [C] : % 58.65/58.69 ( element(C,powerset(powerset(A))) % 58.65/58.69 => ( C = complements_of_subsets(A,B) % 58.65/58.69 <=> ! [D] : % 58.65/58.69 ( element(D,powerset(A)) % 58.65/58.69 => ( in(D,C) % 58.65/58.69 <=> in(subset_complement(A,D),B) ) ) ) ) ) ). % 58.65/58.69 % 58.65/58.69 fof(dt_k1_xboole_0,axiom, % 58.65/58.69 $true ). % 58.65/58.69 % 58.65/58.69 fof(dt_k1_zfmisc_1,axiom, % 58.65/58.69 $true ). % 58.65/58.70 % 58.65/58.70 fof(dt_k3_subset_1,axiom, % 58.65/58.70 ! [A,B] : % 58.65/58.70 ( element(B,powerset(A)) % 58.65/58.70 => element(subset_complement(A,B),powerset(A)) ) ). % 58.65/58.70 % 58.65/58.70 fof(dt_k7_setfam_1,axiom, % 58.65/58.70 ! [A,B] : % 58.65/58.70 ( element(B,powerset(powerset(A))) % 58.65/58.70 => element(complements_of_subsets(A,B),powerset(powerset(A))) ) ). % 58.65/58.70 % 58.65/58.70 fof(dt_m1_subset_1,axiom, % 58.65/58.70 $true ). % 58.65/58.70 % 58.65/58.70 fof(existence_m1_subset_1,axiom, % 58.65/58.70 ! [A] : % 58.65/58.70 ? [B] : element(B,A) ). % 58.65/58.70 % 58.65/58.70 fof(fc1_subset_1,axiom, % 58.65/58.70 ! [A] : ~ empty(powerset(A)) ). % 58.65/58.70 % 58.65/58.70 fof(fc1_xboole_0,axiom, % 58.65/58.70 empty(empty_set) ). % 58.65/58.70 % 58.65/58.70 fof(involutiveness_k3_subset_1,axiom, % 58.65/58.70 ! [A,B] : % 58.65/58.70 ( element(B,powerset(A)) % 58.65/58.70 => subset_complement(A,subset_complement(A,B)) = B ) ). % 58.65/58.70 % 58.65/58.70 fof(involutiveness_k7_setfam_1,axiom, % 58.65/58.70 ! [A,B] : % 58.65/58.70 ( element(B,powerset(powerset(A))) % 58.65/58.70 => complements_of_subsets(A,complements_of_subsets(A,B)) = B ) ). % 58.65/58.70 % 58.65/58.70 fof(rc1_subset_1,axiom, % 58.65/58.70 ! [A] : % 58.65/58.70 ( ~ empty(A) % 58.65/58.70 => ? [B] : % 58.65/58.70 ( element(B,powerset(A)) % 58.65/58.70 & ~ empty(B) ) ) ). % 58.65/58.70 % 58.65/58.70 fof(rc1_xboole_0,axiom, % 58.65/58.70 ? [A] : empty(A) ). % 58.65/58.70 % 58.65/58.70 fof(rc2_subset_1,axiom, % 58.65/58.70 ! [A] : % 58.65/58.70 ? [B] : % 58.65/58.70 ( element(B,powerset(A)) % 58.65/58.70 & empty(B) ) ). % 58.65/58.70 % 58.65/58.70 fof(rc2_xboole_0,axiom, % 58.65/58.70 ? [A] : ~ empty(A) ). % 58.65/58.70 % 58.65/58.70 fof(reflexivity_r1_tarski,axiom, % 58.65/58.70 ! [A,B] : subset(A,A) ). % 58.65/58.70 % 58.65/58.70 fof(t1_subset,axiom, % 58.65/58.70 ! [A,B] : % 58.65/58.70 ( in(A,B) % 58.65/58.70 => element(A,B) ) ). % 58.65/58.70 % 58.65/58.70 fof(t2_subset,axiom, % 58.65/58.70 ! [A,B] : % 58.65/58.70 ( element(A,B) % 58.65/58.70 => ( empty(B) % 58.65/58.70 | in(A,B) ) ) ). % 58.65/58.70 % 58.65/58.70 fof(t3_subset,axiom, % 58.65/58.70 ! [A,B] : % 58.65/58.70 ( element(A,powerset(B)) % 58.65/58.70 <=> subset(A,B) ) ). % 58.65/58.70 % 58.65/58.70 fof(t46_setfam_1,conjecture, % 58.65/58.70 ! [A,B] : % 58.65/58.70 ( element(B,powerset(powerset(A))) % 58.65/58.70 => ~ ( B != empty_set % 58.65/58.70 & complements_of_subsets(A,B) = empty_set ) ) ). % 58.65/58.70 % 58.65/58.70 fof(t4_subset,axiom, % 58.65/58.70 ! [A,B,C] : % 58.65/58.70 ( ( in(A,B) % 58.65/58.70 & element(B,powerset(C)) ) % 58.65/58.70 => element(A,C) ) ). % 58.65/58.70 % 58.65/58.70 fof(t5_subset,axiom, % 58.65/58.70 ! [A,B,C] : % 58.65/58.70 ~ ( in(A,B) % 58.65/58.70 & element(B,powerset(C)) % 58.65/58.70 & empty(C) ) ). % 58.65/58.70 % 58.65/58.70 fof(t6_boole,axiom, % 58.65/58.70 ! [A] : % 58.65/58.70 ( empty(A) % 58.65/58.70 => A = empty_set ) ). % 58.65/58.70 % 58.65/58.70 fof(t7_boole,axiom, % 58.65/58.70 ! [A,B] : % 58.65/58.70 ~ ( in(A,B) % 58.65/58.70 & empty(B) ) ). % 58.65/58.70 % 58.65/58.70 fof(t8_boole,axiom, % 58.65/58.70 ! [A,B] : % 58.65/58.70 ~ ( empty(A) % 58.65/58.70 & A != B % 58.65/58.70 & empty(B) ) ). % 58.65/58.70 % 58.65/58.70 %------------------------------------------------------------------------------ % 58.65/58.70 %------------------------------------------- % 58.65/58.70 % Proof found % 58.65/58.70 % SZS status Theorem for theBenchmark % 58.65/58.70 % SZS output start Proof % 58.65/58.70 %ClaNum:58(EqnAxiom:23) % 58.65/58.70 %VarNum:163(SingletonVarNum:60) % 58.65/58.70 %MaxLitNum:6 % 58.65/58.70 %MaxfuncDepth:2 % 58.65/58.70 %SharedTerms:14 % 58.65/58.70 %goalClause: 27 30 32 % 58.65/58.70 %singleGoalClaCount:3 % 58.65/58.70 [24]P1(a1) % 58.65/58.70 [25]P1(a3) % 58.65/58.70 [32]~E(a1,a11) % 58.65/58.70 [33]~P1(a10) % 58.65/58.70 [27]E(f2(a9,a11),a1) % 58.65/58.70 [30]P2(a11,f12(f12(a9))) % 58.65/58.70 [28]P3(x281,x281) % 58.65/58.70 [26]P1(f8(x261)) % 58.65/58.70 [29]P2(f4(x291),x291) % 58.65/58.70 [31]P2(f8(x311),f12(x311)) % 58.65/58.70 [34]~P1(f12(x341)) % 58.65/58.70 [35]~P1(x351)+E(x351,a1) % 58.65/58.70 [37]P1(x371)+~P1(f7(x371)) % 58.65/58.70 [39]P1(x391)+P2(f7(x391),f12(x391)) % 58.65/58.70 [38]~P1(x381)+~P4(x382,x381) % 58.65/58.70 [40]~P4(x401,x402)+P2(x401,x402) % 58.65/58.70 [43]~P4(x432,x431)+~P4(x431,x432) % 58.65/58.70 [42]~P3(x421,x422)+P2(x421,f12(x422)) % 58.65/58.70 [44]P3(x441,x442)+~P2(x441,f12(x442)) % 58.65/58.70 [45]P3(x451,x452)+P4(f5(x451,x452),x451) % 58.65/58.70 [50]P3(x501,x502)+~P4(f5(x501,x502),x502) % 58.65/58.70 [51]~P2(x512,f12(x511))+P2(f13(x511,x512),f12(x511)) % 58.65/58.70 [49]~P2(x492,f12(x491))+E(f13(x491,f13(x491,x492)),x492) % 58.65/58.70 [52]~P2(x522,f12(f12(x521)))+E(f2(x521,f2(x521,x522)),x522) % 58.65/58.70 [53]~P2(x532,f12(f12(x531)))+P2(f2(x531,x532),f12(f12(x531))) % 58.65/58.70 [36]~P1(x362)+~P1(x361)+E(x361,x362) % 58.65/58.70 [41]~P2(x412,x411)+P1(x411)+P4(x412,x411) % 58.65/58.70 [46]~P3(x463,x462)+P4(x461,x462)+~P4(x461,x463) % 58.65/58.70 [47]~P1(x471)+~P4(x472,x473)+~P2(x473,f12(x471)) % 58.65/58.70 [48]P2(x481,x482)+~P4(x481,x483)+~P2(x483,f12(x482)) % 58.65/58.70 [56]P2(f6(x562,x563,x561),f12(x562))+E(x561,f2(x562,x563))+~P2(x561,f12(f12(x562)))+~P2(x563,f12(f12(x562))) % 58.65/58.70 [57]P4(f6(x572,x573,x571),x571)+E(x571,f2(x572,x573))+P4(f13(x572,f6(x572,x573,x571)),x573)+~P2(x571,f12(f12(x572)))+~P2(x573,f12(f12(x572))) % 58.65/58.70 [58]~P4(f6(x582,x583,x581),x581)+E(x581,f2(x582,x583))+~P2(x581,f12(f12(x582)))+~P2(x583,f12(f12(x582)))+~P4(f13(x582,f6(x582,x583,x581)),x583) % 58.65/58.70 [54]~P4(x542,x544)+~P2(x542,f12(x541))+P4(f13(x541,x542),x543)+~E(x544,f2(x541,x543))+~P2(x543,f12(f12(x541)))+~P2(x544,f12(f12(x541))) % 58.65/58.70 [55]P4(x551,x552)+~P2(x551,f12(x553))+~P4(f13(x553,x551),x554)+~E(x552,f2(x553,x554))+~P2(x552,f12(f12(x553)))+~P2(x554,f12(f12(x553))) % 58.65/58.70 %EqnAxiom % 58.65/58.70 [1]E(x11,x11) % 58.65/58.70 [2]E(x22,x21)+~E(x21,x22) % 58.65/58.70 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 58.65/58.70 [4]~E(x41,x42)+E(f8(x41),f8(x42)) % 58.65/58.70 [5]~E(x51,x52)+E(f2(x51,x53),f2(x52,x53)) % 58.65/58.70 [6]~E(x61,x62)+E(f2(x63,x61),f2(x63,x62)) % 58.65/58.70 [7]~E(x71,x72)+E(f4(x71),f4(x72)) % 58.65/58.70 [8]~E(x81,x82)+E(f12(x81),f12(x82)) % 58.65/58.70 [9]~E(x91,x92)+E(f13(x91,x93),f13(x92,x93)) % 58.65/58.70 [10]~E(x101,x102)+E(f13(x103,x101),f13(x103,x102)) % 58.65/58.70 [11]~E(x111,x112)+E(f5(x111,x113),f5(x112,x113)) % 58.65/58.70 [12]~E(x121,x122)+E(f5(x123,x121),f5(x123,x122)) % 58.65/58.70 [13]~E(x131,x132)+E(f6(x131,x133,x134),f6(x132,x133,x134)) % 58.65/58.70 [14]~E(x141,x142)+E(f6(x143,x141,x144),f6(x143,x142,x144)) % 58.65/58.70 [15]~E(x151,x152)+E(f6(x153,x154,x151),f6(x153,x154,x152)) % 58.65/58.70 [16]~E(x161,x162)+E(f7(x161),f7(x162)) % 58.65/58.70 [17]~P1(x171)+P1(x172)+~E(x171,x172) % 58.65/58.70 [18]P4(x182,x183)+~E(x181,x182)+~P4(x181,x183) % 58.65/58.70 [19]P4(x193,x192)+~E(x191,x192)+~P4(x193,x191) % 58.65/58.70 [20]P2(x202,x203)+~E(x201,x202)+~P2(x201,x203) % 58.65/58.70 [21]P2(x213,x212)+~E(x211,x212)+~P2(x213,x211) % 58.65/58.70 [22]P3(x222,x223)+~E(x221,x222)+~P3(x221,x223) % 58.65/58.70 [23]P3(x233,x232)+~E(x231,x232)+~P3(x233,x231) % 58.65/58.70 % 58.65/58.70 %------------------------------------------- % 58.65/58.72 cnf(61,plain, % 58.65/58.72 (E(a1,f2(a9,a11))), % 58.65/58.72 inference(scs_inference,[],[27,2])). % 58.65/58.72 cnf(62,plain, % 58.65/58.72 (~P4(x621,a1)), % 58.65/58.72 inference(scs_inference,[],[27,24,2,38])). % 58.65/58.72 cnf(68,plain, % 58.65/58.72 (P1(f2(a9,a11))), % 58.65/58.72 inference(scs_inference,[],[27,30,24,2,38,44,45,17])). % 58.65/58.72 cnf(70,plain, % 58.65/58.72 (P2(f4(x701),x701)), % 58.65/58.72 inference(rename_variables,[],[29])). % 58.65/58.72 cnf(71,plain, % 58.65/58.72 (P3(f2(a9,a11),x711)), % 58.65/58.72 inference(scs_inference,[],[27,30,29,24,2,38,44,45,17,21,22])). % 58.65/58.72 cnf(72,plain, % 58.65/58.72 (~P1(a11)), % 58.65/58.72 inference(scs_inference,[],[27,32,30,29,24,2,38,44,45,17,21,22,36])). % 58.65/58.72 cnf(74,plain, % 58.65/58.72 (P4(f4(a10),a10)), % 58.65/58.72 inference(scs_inference,[],[27,32,30,29,70,24,33,2,38,44,45,17,21,22,36,41])). % 58.65/58.72 cnf(75,plain, % 58.65/58.72 (P2(f4(x751),x751)), % 58.65/58.72 inference(rename_variables,[],[29])). % 58.65/58.72 cnf(77,plain, % 58.65/58.72 (~P4(x771,f4(f12(a1)))), % 58.65/58.72 inference(scs_inference,[],[27,32,30,29,70,75,24,33,2,38,44,45,17,21,22,36,41,47])). % 58.65/58.72 cnf(89,plain, % 58.65/58.72 (~P4(x891,f2(a9,a11))), % 58.65/58.72 inference(scs_inference,[],[68,38])). % 58.65/58.72 cnf(91,plain, % 58.65/58.72 (P3(f4(f12(a1)),x911)), % 58.65/58.72 inference(scs_inference,[],[68,77,38,45])). % 58.65/58.72 cnf(92,plain, % 58.65/58.72 (~P4(x921,f4(f12(a1)))), % 58.65/58.72 inference(rename_variables,[],[77])). % 58.65/58.72 cnf(96,plain, % 58.65/58.72 (P4(f4(a11),a11)), % 58.65/58.72 inference(scs_inference,[],[68,77,31,72,29,38,45,44,41])). % 58.65/58.72 cnf(101,plain, % 58.65/58.72 (~P4(x1011,f8(f2(a9,a11)))), % 58.65/58.72 inference(scs_inference,[],[68,77,92,31,72,29,38,45,44,41,19,47])). % 58.65/58.72 cnf(105,plain, % 58.65/58.72 (~P4(a11,f4(a11))), % 58.65/58.72 inference(scs_inference,[],[27,68,77,92,31,72,29,38,45,44,41,19,47,23,43])). % 58.65/58.72 cnf(107,plain, % 58.65/58.72 (P2(f4(a11),f12(a9))), % 58.65/58.72 inference(scs_inference,[],[27,30,68,77,92,31,72,29,38,45,44,41,19,47,23,43,48])). % 58.65/58.72 cnf(116,plain, % 58.65/58.72 (~P4(x1161,f8(f2(a9,a11)))), % 58.65/58.72 inference(rename_variables,[],[101])). % 58.65/58.72 cnf(118,plain, % 58.65/58.72 (~P4(x1181,a3)), % 58.65/58.72 inference(scs_inference,[],[101,25,45,38])). % 58.65/58.72 cnf(122,plain, % 58.65/58.72 (P4(a11,f12(f12(a9)))), % 58.65/58.72 inference(scs_inference,[],[30,101,107,25,34,45,38,44,41])). % 58.65/58.72 cnf(127,plain, % 58.65/58.72 (~P4(f12(f12(a9)),a11)), % 58.65/58.72 inference(scs_inference,[],[30,74,101,116,107,25,34,45,38,44,41,19,43])). % 58.65/58.72 cnf(136,plain, % 58.65/58.72 (~P4(x1361,f8(x1362))), % 58.65/58.72 inference(scs_inference,[],[26,38])). % 58.65/58.72 cnf(138,plain, % 58.65/58.72 (P3(a3,x1381)), % 58.65/58.72 inference(scs_inference,[],[118,26,38,45])). % 58.65/58.72 cnf(142,plain, % 58.65/58.72 (P2(f4(x1421),x1421)), % 58.65/58.72 inference(rename_variables,[],[29])). % 58.65/58.72 cnf(144,plain, % 58.65/58.72 (~P2(f12(f12(a9)),a11)), % 58.65/58.72 inference(scs_inference,[],[29,118,127,26,72,38,45,44,41])). % 58.65/58.72 cnf(151,plain, % 58.65/58.72 (~E(a10,a1)), % 58.65/58.72 inference(scs_inference,[],[61,74,29,142,89,118,127,26,72,38,45,44,41,48,19,3])). % 58.65/58.72 cnf(164,plain, % 58.65/58.72 (P3(f8(x1641),x1642)), % 58.65/58.72 inference(scs_inference,[],[136,45])). % 58.65/58.72 cnf(194,plain, % 58.65/58.72 (E(a11,f2(a9,a11))+P4(f6(a9,a11,a11),a11)+P4(f13(a9,f6(a9,a11,a11)),a11)), % 58.65/58.72 inference(scs_inference,[],[30,107,96,138,136,77,19,57])). % 58.65/58.72 cnf(197,plain, % 58.65/58.72 (~E(a11,f2(a9,a11))), % 58.65/58.72 inference(scs_inference,[],[96,89,19])). % 58.65/58.72 cnf(199,plain, % 58.65/58.72 (P2(f6(a9,a11,a11),f12(a9))), % 58.65/58.72 inference(scs_inference,[],[30,96,89,19,56])). % 58.65/58.72 cnf(201,plain, % 58.65/58.72 (P3(f6(a9,a11,a11),a9)), % 58.65/58.72 inference(scs_inference,[],[30,96,89,19,56,44])). % 58.65/58.72 cnf(208,plain, % 58.65/58.72 (P4(f6(a9,a11,a11),a11)+P4(f13(a9,f6(a9,a11,a11)),a11)), % 58.65/58.72 inference(scs_inference,[],[197,194])). % 58.65/58.72 cnf(226,plain, % 58.65/58.72 (P2(x2261,f12(x2262))+~E(f8(x2262),x2261)), % 58.65/58.72 inference(scs_inference,[],[31,122,62,19,20])). % 58.65/58.72 cnf(236,plain, % 58.65/58.72 (P3(x2361,x2362)+~E(f8(x2363),x2361)), % 58.65/58.72 inference(scs_inference,[],[122,164,136,201,19,23,22])). % 58.65/58.72 cnf(262,plain, % 58.65/58.72 (~P1(f7(a10))), % 58.65/58.72 inference(scs_inference,[],[151,35,37])). % 58.65/58.72 cnf(263,plain, % 58.65/58.72 (P4(f4(f7(a10)),f7(a10))), % 58.65/58.72 inference(scs_inference,[],[29,262,41])). % 58.65/58.72 cnf(295,plain, % 58.65/58.72 (~E(f8(f12(a9)),f2(a9,a11))+~P4(f13(a9,f4(a11)),a11)), % 58.65/58.72 inference(scs_inference,[],[30,107,31,122,118,136,19,55])). % 58.65/58.72 cnf(744,plain, % 58.65/58.72 (P2(f7(a10),f12(a10))), % 58.65/58.72 inference(scs_inference,[],[74,39,38])). % 58.65/58.72 cnf(745,plain, % 58.65/58.72 (P3(f7(a10),a10)), % 58.65/58.72 inference(scs_inference,[],[744,44])). % 58.65/58.72 cnf(874,plain, % 58.65/58.72 (P4(f4(f7(a10)),a10)), % 58.65/58.72 inference(scs_inference,[],[263,745,46])). % 58.65/58.72 cnf(1087,plain, % 58.65/58.72 (E(f8(f2(a9,a11)),f8(a1))), % 58.65/58.72 inference(scs_inference,[],[61,4,2])). % 58.65/58.72 cnf(1088,plain, % 58.65/58.72 (P2(f8(a1),f12(f2(a9,a11)))), % 58.65/58.72 inference(scs_inference,[],[1087,226])). % 58.65/58.72 cnf(1089,plain, % 58.65/58.72 (E(f8(a1),f8(f2(a9,a11)))), % 58.65/58.72 inference(scs_inference,[],[1087,226,2])). % 58.65/58.72 cnf(3009,plain, % 58.65/58.72 (~P4(x30091,f4(f12(a3)))), % 58.65/58.72 inference(scs_inference,[],[25,29,47])). % 58.65/58.72 cnf(3012,plain, % 58.65/58.72 (P3(f4(f12(a3)),x30121)), % 58.65/58.72 inference(scs_inference,[],[25,29,47,45])). % 58.65/58.72 cnf(4913,plain, % 58.65/58.72 (P4(f4(f12(x49131)),f12(x49131))), % 58.65/58.72 inference(scs_inference,[],[29,34,41])). % 58.65/58.72 cnf(4920,plain, % 58.65/58.72 (P4(x49201,f12(x49202))+~E(f4(f12(x49202)),x49201)), % 58.65/58.72 inference(scs_inference,[],[29,34,89,41,43,19,18])). % 58.65/58.72 cnf(6006,plain, % 58.65/58.72 (P4(f8(x60061),f12(x60061))), % 58.65/58.72 inference(scs_inference,[],[31,34,41])). % 58.65/58.72 cnf(6009,plain, % 58.65/58.72 (P4(f8(f2(a9,a11)),f12(a1))), % 58.65/58.72 inference(scs_inference,[],[31,1089,34,41,18])). % 58.65/58.72 cnf(6647,plain, % 58.65/58.72 (~P4(f13(a9,f4(a11)),a11)), % 58.65/58.72 inference(scs_inference,[],[68,26,295,36])). % 58.65/58.72 cnf(6824,plain, % 58.65/58.72 (~P2(f13(a9,f4(a11)),a11)), % 58.65/58.72 inference(scs_inference,[],[6647,72,41])). % 58.65/58.72 cnf(8981,plain, % 58.65/58.72 (~E(f8(f12(a9)),f2(a9,a11))+~P4(f13(a9,f6(a9,a11,a11)),a11)), % 58.65/58.72 inference(scs_inference,[],[30,199,31,136,55])). % 58.65/58.72 cnf(9060,plain, % 58.65/58.72 (~P4(f13(a9,f6(a9,a11,a11)),a11)), % 58.65/58.72 inference(scs_inference,[],[68,26,8981,36])). % 58.65/58.72 cnf(9061,plain, % 58.65/58.72 (P4(f6(a9,a11,a11),a11)), % 58.65/58.72 inference(scs_inference,[],[9060,208])). % 58.65/58.72 cnf(9069,plain, % 58.65/58.72 (~P4(a11,f6(a9,a11,a11))), % 58.65/58.72 inference(scs_inference,[],[9061,43])). % 58.65/58.72 cnf(10326,plain, % 58.65/58.72 (~P2(f13(a9,f6(a9,a11,a11)),a11)), % 58.65/58.72 inference(scs_inference,[],[9060,72,41])). % 58.65/58.72 cnf(13875,plain, % 58.65/58.72 (E(f2(f2(a9,a11),x138751),f2(a1,x138751))), % 58.65/58.72 inference(scs_inference,[],[68,35,5])). % 58.65/58.72 cnf(13876,plain, % 58.65/58.72 (E(f2(a1,x138761),f2(f2(a9,a11),x138761))), % 58.65/58.72 inference(scs_inference,[],[13875,2])). % 58.65/58.72 cnf(14579,plain, % 58.65/58.72 (E(f2(x145791,f2(a9,a11)),f2(x145791,a1))), % 58.65/58.72 inference(scs_inference,[],[68,35,6])). % 58.65/58.72 cnf(14580,plain, % 58.65/58.72 (E(f2(x145801,a1),f2(x145801,f2(a9,a11)))), % 58.65/58.73 inference(scs_inference,[],[14579,2])). % 58.65/58.73 cnf(14581,plain, % 58.65/58.73 (E(f2(a1,f2(a9,a11)),f2(f2(a9,a11),a1))), % 58.65/58.73 inference(scs_inference,[],[13876,14579,2,3])). % 58.65/58.73 cnf(14591,plain, % 58.65/58.73 (E(f2(f2(a9,a11),a1),f2(a1,f2(a9,a11)))), % 58.65/58.73 inference(scs_inference,[],[14581,2])). % 58.65/58.73 cnf(14594,plain, % 58.65/58.73 (E(f2(x145941,a1),f2(x145941,f2(a9,a11)))), % 58.65/58.73 inference(rename_variables,[],[14580])). % 58.65/58.73 cnf(14595,plain, % 58.65/58.73 (~P1(f2(x145951,a1))+P1(f2(x145951,f2(a9,a11)))), % 58.65/58.73 inference(scs_inference,[],[13876,14580,14594,14581,2,3,17])). % 58.65/58.73 cnf(14706,plain, % 58.65/58.73 (P1(f2(x147061,f2(a9,a11)))+P2(f7(f2(x147061,a1)),f12(f2(x147061,a1)))), % 58.65/58.73 inference(scs_inference,[],[14595,39])). % 58.65/58.73 cnf(15373,plain, % 58.65/58.73 (P3(f2(f2(a9,a11),a1),f2(a1,f2(a9,a11)))), % 58.65/58.73 inference(scs_inference,[],[14591,28,23])). % 58.65/58.73 cnf(15384,plain, % 58.65/58.73 (E(f2(x153841,a1),f2(x153841,f2(a9,a11)))), % 58.65/58.73 inference(rename_variables,[],[14580])). % 58.65/58.73 cnf(15385,plain, % 58.65/58.73 (P2(f4(f2(x153851,a1)),f2(x153851,f2(a9,a11)))), % 58.65/58.73 inference(scs_inference,[],[14580,15384,15373,29,22,21])). % 58.65/58.73 cnf(15389,plain, % 58.65/58.73 (P2(x153891,f2(x153892,f2(a9,a11)))+~E(f4(f2(x153892,a1)),x153891)), % 58.65/58.73 inference(scs_inference,[],[14580,15384,13876,15373,29,22,21,23,20])). % 58.65/58.73 cnf(16264,plain, % 58.65/58.73 (P1(f2(x162641,f2(a9,a11)))+P3(f7(f2(x162641,a1)),f2(x162641,a1))), % 58.65/58.73 inference(scs_inference,[],[14706,44])). % 58.65/58.73 cnf(17385,plain, % 58.65/58.73 (P3(x173851,x173851)), % 58.65/58.73 inference(rename_variables,[],[28])). % 58.65/58.73 cnf(17388,plain, % 58.65/58.73 (E(f2(a1,x173881),f2(f2(a9,a11),x173881))), % 58.65/58.73 inference(rename_variables,[],[13876])). % 58.65/58.73 cnf(17389,plain, % 58.65/58.73 (P3(f2(a1,x173891),f2(f2(a9,a11),x173891))), % 58.65/58.73 inference(scs_inference,[],[13876,17388,15385,28,17385,22,21,23])). % 58.65/58.73 cnf(17816,plain, % 58.65/58.73 (~P3(a10,f2(a9,a11))), % 58.65/58.73 inference(scs_inference,[],[74,89,46])). % 58.65/58.73 cnf(17866,plain, % 58.65/58.73 (~P3(f12(x178661),f2(a9,a11))), % 58.65/58.73 inference(scs_inference,[],[4913,89,46])). % 58.65/58.73 cnf(17878,plain, % 58.65/58.73 (~P3(a11,f4(f12(a1)))), % 58.65/58.73 inference(scs_inference,[],[96,77,46])). % 58.65/58.73 cnf(17883,plain, % 58.65/58.73 (~E(f8(x178831),a11)), % 58.65/58.73 inference(scs_inference,[],[3012,96,77,17866,46,22,236])). % 58.65/58.73 cnf(17891,plain, % 58.65/58.73 (~P3(a11,f2(a9,a11))), % 58.65/58.73 inference(scs_inference,[],[96,89,46])). % 58.65/58.73 cnf(17894,plain, % 58.65/58.73 (~E(f2(a9,a11),a11)), % 58.65/58.73 inference(scs_inference,[],[71,96,89,17878,46,22])). % 58.65/58.73 cnf(17903,plain, % 58.65/58.73 (~E(f4(f12(a3)),a11)), % 58.65/58.73 inference(scs_inference,[],[3012,17891,22])). % 58.65/58.73 cnf(17940,plain, % 58.65/58.73 (~E(f4(f12(a1)),a11)), % 58.65/58.73 inference(scs_inference,[],[91,17891,22])). % 58.65/58.73 cnf(17949,plain, % 58.65/58.73 (~E(a3,a11)), % 58.65/58.73 inference(scs_inference,[],[138,17878,22])). % 58.65/58.73 cnf(18090,plain, % 58.65/58.73 (~P4(f13(a9,f4(a11)),x180901)+~E(x180901,a11)), % 58.65/58.73 inference(scs_inference,[],[118,6009,6647,46,19])). % 58.65/58.73 cnf(18122,plain, % 58.65/58.73 (~P4(f13(a9,f6(a9,a11,a11)),x181221)+~E(x181221,a11)), % 58.65/58.73 inference(scs_inference,[],[118,874,9060,46,19])). % 58.65/58.73 cnf(18131,plain, % 58.65/58.73 (~P4(f12(f12(a9)),x181311)+~E(x181311,a11)), % 58.65/58.73 inference(scs_inference,[],[118,96,127,46,19])). % 58.65/58.73 cnf(18178,plain, % 58.65/58.73 (~P4(x181781,f4(a11))+~E(x181781,a11)), % 58.65/58.73 inference(scs_inference,[],[105,18])). % 58.65/58.73 cnf(18183,plain, % 58.65/58.73 (~P4(x181831,f6(a9,a11,a11))+~E(x181831,a11)), % 58.65/58.73 inference(scs_inference,[],[9069,18])). % 58.65/58.73 cnf(18315,plain, % 58.65/58.73 (~P3(f12(a1),a1)), % 58.65/58.73 inference(scs_inference,[],[6009,62,46])). % 58.65/58.73 cnf(18324,plain, % 58.65/58.73 (~P3(f12(f12(a9)),f4(a11))), % 58.65/58.73 inference(scs_inference,[],[105,122,46])). % 58.65/58.73 cnf(18663,plain, % 58.65/58.73 (E(f2(a9,f2(a9,a11)),a11)), % 58.65/58.73 inference(scs_inference,[],[30,51,52])). % 58.65/58.73 cnf(18667,plain, % 58.65/58.73 (~P1(f2(a9,f2(a9,a11)))), % 58.65/58.73 inference(scs_inference,[],[30,72,51,52,44,17])). % 58.65/58.73 cnf(18668,plain, % 58.65/58.73 (~E(a1,f2(a9,f2(a9,a11)))), % 58.65/58.73 inference(scs_inference,[],[30,32,72,51,52,44,17,3])). % 58.65/58.73 cnf(18686,plain, % 58.65/58.73 (P2(f13(f2(a9,a11),f8(a1)),f12(f2(a9,a11)))), % 58.65/58.73 inference(scs_inference,[],[1088,18663,18090,18178,51])). % 58.65/58.73 cnf(18688,plain, % 58.65/58.73 (~P4(f13(a9,f6(a9,a11,a11)),f2(a9,f2(a9,a11)))), % 58.65/58.73 inference(scs_inference,[],[1088,18663,18090,18178,51,18122])). % 58.65/58.73 cnf(18691,plain, % 58.65/58.73 (~P4(f12(f12(a9)),f2(a9,f2(a9,a11)))), % 58.65/58.73 inference(scs_inference,[],[1088,18663,18090,18178,51,18122,44,18131])). % 58.65/58.73 cnf(18696,plain, % 58.65/58.73 (~P1(f2(a9,a1))), % 58.65/58.73 inference(scs_inference,[],[14580,1088,18667,18668,18663,18090,18178,51,18122,44,18131,18183,2,41,17])). % 58.65/58.73 cnf(18697,plain, % 58.65/58.73 (E(f2(x186971,a1),f2(x186971,f2(a9,a11)))), % 58.65/58.73 inference(rename_variables,[],[14580])). % 58.65/58.73 cnf(18698,plain, % 58.65/58.73 (~P4(x186981,f13(f2(a9,a11),f8(a1)))), % 58.65/58.73 inference(scs_inference,[],[14580,1088,68,18667,18668,18663,18090,18178,51,18122,44,18131,18183,2,41,17,47])). % 58.65/58.73 cnf(18700,plain, % 58.65/58.73 (~E(f4(f12(a3)),f2(a9,f2(a9,a11)))), % 58.65/58.73 inference(scs_inference,[],[14580,1088,17903,68,18667,18668,18663,18090,18178,51,18122,44,18131,18183,2,41,17,47,3])). % 58.65/58.73 cnf(18701,plain, % 58.65/58.73 (~E(f4(f2(a9,a1)),f13(a9,f4(a11)))), % 58.65/58.73 inference(scs_inference,[],[14580,1088,15385,17903,68,18667,18668,18663,18090,18178,51,18122,44,18131,18183,2,41,17,47,3,20])). % 58.65/58.73 cnf(18704,plain, % 58.65/58.73 (~E(f13(f2(a9,a11),f8(a1)),a11)), % 58.65/58.73 inference(scs_inference,[],[14580,27,1088,15385,17903,68,18667,18668,17891,18663,18090,18178,51,18122,44,18131,18183,2,41,17,47,3,20,23,22])). % 58.65/58.73 cnf(18705,plain, % 58.65/58.73 (~P4(f13(a9,f4(a11)),f2(a9,a1))), % 58.65/58.73 inference(scs_inference,[],[14580,18697,27,1088,15385,17903,68,18667,18668,17891,18663,18090,18178,51,18122,44,18131,18183,2,41,17,47,3,20,23,22,19])). % 58.65/58.73 cnf(18706,plain, % 58.65/58.73 (E(f2(x187061,a1),f2(x187061,f2(a9,a11)))), % 58.65/58.73 inference(rename_variables,[],[14580])). % 58.65/58.73 cnf(18709,plain, % 58.65/58.73 (P3(f13(f2(a9,a11),f8(a1)),x187091)), % 58.65/58.73 inference(scs_inference,[],[14580,18697,18706,27,1088,15385,17903,68,18667,18668,17891,18663,18090,18178,51,18122,44,18131,18183,2,41,17,47,3,20,23,22,19,18,45])). % 58.65/58.73 cnf(18730,plain, % 58.65/58.73 (~E(f4(f12(a1)),f2(a9,f2(a9,a11)))), % 58.65/58.73 inference(scs_inference,[],[17940,6009,18705,18701,18696,107,18698,18663,51,44,2,46,41,3])). % 58.65/58.73 cnf(18731,plain, % 58.65/58.73 (~E(f12(a9),a11)), % 58.65/58.73 inference(scs_inference,[],[17940,6009,18705,18701,18696,107,6824,18698,18663,51,44,2,46,41,3,21])). % 58.65/58.73 cnf(18732,plain, % 58.65/58.73 (~P4(f13(a9,f6(a9,a11,a11)),f2(a9,a1))), % 58.65/58.73 inference(scs_inference,[],[14580,17940,6009,18688,18705,18701,18696,107,6824,18698,18663,51,44,2,46,41,3,21,19])). % 58.65/58.73 cnf(18748,plain, % 58.65/58.73 (~E(a3,f2(a9,f2(a9,a11)))), % 58.65/58.73 inference(scs_inference,[],[17949,18696,18700,18732,199,18663,51,44,2,41,3])). % 58.65/58.73 cnf(18749,plain, % 58.65/58.73 (~P4(f12(f12(a9)),f2(a9,a1))), % 58.65/58.73 inference(scs_inference,[],[14580,17949,18696,18700,18732,18691,199,18663,51,44,2,41,3,19])). % 58.65/58.73 cnf(18759,plain, % 58.65/58.73 (~E(f2(a9,a11),f2(a9,f2(a9,a11)))), % 58.65/58.73 inference(scs_inference,[],[17894,18704,744,18663,51,2,3])). % 58.65/58.73 cnf(18760,plain, % 58.65/58.73 (~E(f12(a1),f13(f2(a9,a11),f8(a1)))), % 58.65/58.73 inference(scs_inference,[],[6009,17894,18704,744,18663,18698,51,2,3,19])). % 58.65/58.73 cnf(18769,plain, % 58.65/58.73 (P2(f13(x187691,f8(x187691)),f12(x187691))), % 58.65/58.73 inference(scs_inference,[],[31,51])). % 58.65/58.73 cnf(18774,plain, % 58.65/58.73 (~E(f8(x187741),f2(a9,f2(a9,a11)))), % 58.65/58.73 inference(scs_inference,[],[17883,18730,31,144,18663,51,2,48,3])). % 58.65/58.73 cnf(18782,plain, % 58.65/58.73 (P3(f13(x187821,f8(x187821)),x187821)), % 58.65/58.73 inference(scs_inference,[],[18769,44])). % 58.65/58.73 cnf(18785,plain, % 58.65/58.73 (~E(f13(f2(a9,a11),f8(a1)),f2(a9,f2(a9,a11)))), % 58.65/58.73 inference(scs_inference,[],[18704,18759,18663,18769,44,2,3])). % 58.65/58.73 cnf(18793,plain, % 58.65/58.73 (~E(f2(a9,a11),f2(a9,a1))), % 58.65/58.73 inference(scs_inference,[],[14580,18759,18774,2,3])). % 58.65/58.73 cnf(18802,plain, % 58.65/58.73 (~E(a1,f2(a9,a1))), % 58.65/58.73 inference(scs_inference,[],[14580,18668,18748,2,3])). % 58.65/58.73 cnf(18817,plain, % 58.65/58.73 (~P2(f13(a9,f6(a9,a11,a11)),f2(a9,f2(a9,a11)))), % 58.65/58.73 inference(scs_inference,[],[18667,18688,18793,2,41])). % 58.65/58.73 cnf(18829,plain, % 58.65/58.73 (~P2(f12(f12(a9)),f2(a9,f2(a9,a11)))), % 58.65/58.73 inference(scs_inference,[],[18667,18691,18785,2,41])). % 58.65/58.73 cnf(18850,plain, % 58.65/58.73 (~E(f13(f2(a9,a11),f8(a1)),f12(a1))), % 58.65/58.73 inference(scs_inference,[],[18760,2])). % 58.65/58.73 cnf(18859,plain, % 58.65/58.73 (~E(f13(f2(a9,a11),f8(a1)),f2(a9,a1))), % 58.65/58.73 inference(scs_inference,[],[14580,18785,18802,2,3])). % 58.65/58.73 cnf(18867,plain, % 58.65/58.73 (~E(f8(x188671),f2(a9,a1))), % 58.65/58.73 inference(scs_inference,[],[14580,18774,18859,2,3])). % 58.65/58.73 cnf(18880,plain, % 58.65/58.73 (~E(a3,f2(a9,a1))), % 58.65/58.73 inference(scs_inference,[],[14580,18748,18867,2,3])). % 58.65/58.73 cnf(18888,plain, % 58.65/58.73 (~E(f12(a9),f2(a9,f2(a9,a11)))), % 58.65/58.73 inference(scs_inference,[],[18880,18731,18663,2,3])). % 58.65/58.73 cnf(18896,plain, % 58.65/58.73 (~E(f12(a9),f2(a9,a1))), % 58.65/58.73 inference(scs_inference,[],[14580,18888,2,3])). % 58.65/58.73 cnf(18912,plain, % 58.65/58.73 (P2(x189121,f12(f2(a9,a11)))+~E(f13(f2(a9,a11),f8(a1)),x189121)), % 58.65/58.73 inference(scs_inference,[],[18896,18686,2,20])). % 58.65/58.73 cnf(18933,plain, % 58.65/58.73 (P2(x189331,f12(x189332))+~E(f13(x189332,f8(x189332)),x189331)), % 58.65/58.73 inference(scs_inference,[],[18769,20])). % 58.65/58.73 cnf(19124,plain, % 58.65/58.73 (~E(x191241,f12(a1))+~E(f13(f2(a9,a11),f8(a1)),x191241)), % 58.65/58.73 inference(scs_inference,[],[18850,3])). % 58.65/58.73 cnf(19281,plain, % 58.65/58.73 (~P3(f12(f12(a9)),a1)), % 58.65/58.73 inference(scs_inference,[],[122,62,46])). % 58.65/58.73 cnf(20042,plain, % 58.65/58.73 (P2(f13(f2(a9,a11),f8(a1)),f12(x200421))), % 58.65/58.73 inference(scs_inference,[],[18709,262,37,42])). % 58.65/58.73 cnf(20048,plain, % 58.65/58.73 (P2(f2(a9,a11),f12(f12(a9)))), % 58.65/58.73 inference(scs_inference,[],[27,18709,262,30,37,42,39,11,12,53])). % 58.65/58.73 cnf(20055,plain, % 58.65/58.73 (E(a3,a1)), % 58.65/58.73 inference(scs_inference,[],[27,18709,18829,25,262,18667,30,37,42,39,11,12,53,15389,16264,14706,35])). % 58.65/58.73 cnf(20066,plain, % 58.65/58.73 (E(f13(x200661,a3),f13(x200661,a1))), % 58.65/58.73 inference(scs_inference,[],[27,19281,18709,18829,25,262,18667,18663,30,9061,37,42,39,11,12,53,15389,16264,14706,35,8,2,40,13,14,44,15,10])). % 58.65/58.73 cnf(20072,plain, % 58.65/58.73 (P4(f5(f12(a1),a1),f12(a1))), % 58.65/58.73 inference(scs_inference,[],[27,19281,18709,18829,18315,18324,25,262,18667,18663,30,9061,37,42,39,11,12,53,15389,16264,14706,35,8,2,40,13,14,44,15,10,16,9,50,7,45])). % 58.65/58.73 cnf(20086,plain, % 58.65/58.73 (E(f2(x200861,a1),f2(x200861,f2(a9,a11)))), % 58.65/58.73 inference(rename_variables,[],[14580])). % 58.65/58.73 cnf(20087,plain, % 58.65/58.73 (E(f2(a9,a1),a11)), % 58.65/58.73 inference(scs_inference,[],[27,18782,19281,18709,18829,18817,18315,18324,10326,6006,25,15385,262,18667,18663,122,14580,20086,18769,96,30,9061,37,42,39,11,12,53,15389,16264,14706,35,8,2,40,13,14,44,15,10,16,9,50,7,45,47,19,18,22,48,20,21,3])). % 58.65/58.73 cnf(20089,plain, % 58.65/58.73 (~P3(a10,a1)), % 58.65/58.73 inference(scs_inference,[],[27,18782,19281,18709,18829,18817,18315,18324,10326,6006,17816,25,15385,262,18667,61,18663,122,14580,20086,18769,96,30,9061,37,42,39,11,12,53,15389,16264,14706,35,8,2,40,13,14,44,15,10,16,9,50,7,45,47,19,18,22,48,20,21,3,23])). % 58.65/58.73 cnf(20090,plain, % 58.65/58.73 (P1(f4(f12(a3)))), % 58.65/58.73 inference(scs_inference,[],[27,18782,19281,18709,18829,18817,18315,18324,10326,6006,17816,25,15385,262,3009,18667,61,18663,122,14580,20086,18769,96,29,30,9061,37,42,39,11,12,53,15389,16264,14706,35,8,2,40,13,14,44,15,10,16,9,50,7,45,47,19,18,22,48,20,21,3,23,41])). % 58.65/58.73 cnf(20094,plain, % 58.65/58.73 (E(f8(a3),f8(a1))), % 58.65/58.73 inference(scs_inference,[],[27,18782,19281,18709,18829,18817,18315,18324,10326,6006,17816,25,15385,262,3009,18667,61,18663,122,14580,20086,18769,96,29,30,9061,37,42,39,11,12,53,15389,16264,14706,35,8,2,40,13,14,44,15,10,16,9,50,7,45,47,19,18,22,48,20,21,3,23,41,4])). % 58.65/58.73 cnf(20099,plain, % 58.65/58.73 (E(f2(x200991,a3),f2(x200991,a1))), % 58.65/58.73 inference(scs_inference,[],[27,18782,19281,18709,18829,18817,18315,18324,10326,6006,17816,25,15385,262,3009,18667,61,18663,122,14580,20086,18769,96,29,30,9061,37,42,39,11,12,53,15389,16264,14706,35,8,2,40,13,14,44,15,10,16,9,50,7,45,47,19,18,22,48,20,21,3,23,41,4,5,18933,19124,18912,6])). % 58.65/58.73 cnf(20142,plain, % 58.65/58.73 (E(f2(x201421,a3),f2(x201421,a1))), % 58.65/58.73 inference(rename_variables,[],[20099])). % 58.65/58.73 cnf(20157,plain, % 58.65/58.73 ($false), % 58.65/58.73 inference(scs_inference,[],[27,20055,20089,20066,20099,20142,20087,20094,20042,20072,20048,20090,17389,18867,6006,164,18749,28,34,72,61,31,29,136,62,37,42,39,12,35,11,5,6,4,40,8,44,2,14,13,15,10,16,45,4920,9,7,19,20,18,21,22,23,41,3,57]), % 58.65/58.73 ['proof']). % 58.65/58.74 % SZS output end Proof % 58.80/58.74 % Total time :58.090000s %------------------------------------------------------------------------------