%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SEU294+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 : n023.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:02:18 EDT 2024 % Result : Theorem 58.98s 59.11s % Output : CNFRefutation 59.09s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.11 % Problem : SEU294+1 : TPTP v8.2.0. Released v3.3.0. % 0.03/0.11 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.11/0.32 % Computer : n023.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 16:32:09 EDT 2024 % 0.11/0.32 % CPUTime : % 0.52/0.57 start to proof:theBenchmark % 58.98/59.09 %------------------------------------------- % 58.98/59.09 % File :CSE---1.7 % 58.98/59.09 % Problem :theBenchmark % 58.98/59.09 % Transform :cnf % 58.98/59.09 % Format :tptp:raw % 58.98/59.09 % Command :java -jar mcs_scs.jar %d %s % 58.98/59.09 % 58.98/59.09 % Result :Theorem 58.450000s % 58.98/59.09 % Output :CNFRefutation 58.450000s % 58.98/59.09 %------------------------------------------- % 58.98/59.10 %------------------------------------------------------------------------------ % 58.98/59.10 % File : SEU294+1 : TPTP v8.2.0. Released v3.3.0. % 58.98/59.10 % Domain : Set theory % 58.98/59.10 % Problem : MPTP bushy problem t13_finset_1 % 58.98/59.10 % Version : [Urb07] axioms : Especial. % 58.98/59.10 % English : % 58.98/59.10 % 58.98/59.10 % Refs : [Ban01] Bancerek et al. (2001), On the Characterizations of Co % 58.98/59.10 % : [Urb07] Urban (2006), Email to G. Sutcliffe % 58.98/59.10 % Source : [Urb07] % 58.98/59.10 % Names : bushy-t13_finset_1 [Urb07] % 58.98/59.10 % 58.98/59.10 % Status : Theorem % 58.98/59.10 % Rating : 0.03 v8.1.0, 0.00 v6.4.0, 0.04 v6.3.0, 0.08 v6.2.0, 0.04 v6.1.0, 0.10 v6.0.0, 0.09 v5.5.0, 0.07 v5.4.0, 0.11 v5.3.0, 0.15 v5.2.0, 0.00 v4.0.0, 0.04 v3.7.0, 0.05 v3.4.0, 0.11 v3.3.0 % 58.98/59.10 % Syntax : Number of formulae : 48 ( 9 unt; 0 def) % 58.98/59.10 % Number of atoms : 140 ( 2 equ) % 58.98/59.10 % Maximal formula atoms : 10 ( 2 avg) % 58.98/59.10 % Number of connectives : 107 ( 15 ~; 1 |; 70 &) % 58.98/59.10 % ( 1 <=>; 20 =>; 0 <=; 0 <~>) % 58.98/59.10 % Maximal formula depth : 12 ( 4 avg) % 58.98/59.10 % Maximal term depth : 2 ( 1 avg) % 58.98/59.10 % Number of predicates : 15 ( 13 usr; 1 prp; 0-2 aty) % 58.98/59.10 % Number of functors : 2 ( 2 usr; 1 con; 0-1 aty) % 58.98/59.10 % Number of variables : 60 ( 41 !; 19 ?) % 58.98/59.10 % SPC : FOF_THM_RFO_SEQ % 58.98/59.10 % 58.98/59.10 % Comments : Translated by MPTP 0.2 from the original problem in the Mizar % 58.98/59.10 % library, www.mizar.org % 58.98/59.10 %------------------------------------------------------------------------------ % 58.98/59.10 fof(antisymmetry_r2_hidden,axiom, % 58.98/59.10 ! [A,B] : % 58.98/59.10 ( in(A,B) % 58.98/59.10 => ~ in(B,A) ) ). % 58.98/59.10 % 58.98/59.10 fof(cc1_arytm_3,axiom, % 58.98/59.10 ! [A] : % 58.98/59.10 ( ordinal(A) % 58.98/59.10 => ! [B] : % 58.98/59.10 ( element(B,A) % 58.98/59.10 => ( epsilon_transitive(B) % 58.98/59.10 & epsilon_connected(B) % 58.98/59.10 & ordinal(B) ) ) ) ). % 58.98/59.10 % 58.98/59.10 fof(cc1_finset_1,axiom, % 58.98/59.10 ! [A] : % 58.98/59.10 ( empty(A) % 58.98/59.10 => finite(A) ) ). % 58.98/59.10 % 58.98/59.10 fof(cc1_funct_1,axiom, % 58.98/59.10 ! [A] : % 58.98/59.10 ( empty(A) % 58.98/59.10 => function(A) ) ). % 58.98/59.10 % 58.98/59.10 fof(cc1_ordinal1,axiom, % 58.98/59.10 ! [A] : % 58.98/59.10 ( ordinal(A) % 58.98/59.10 => ( epsilon_transitive(A) % 58.98/59.10 & epsilon_connected(A) ) ) ). % 58.98/59.10 % 58.98/59.10 fof(cc1_relat_1,axiom, % 58.98/59.10 ! [A] : % 58.98/59.10 ( empty(A) % 58.98/59.10 => relation(A) ) ). % 58.98/59.10 % 58.98/59.10 fof(cc2_arytm_3,axiom, % 58.98/59.10 ! [A] : % 58.98/59.10 ( ( empty(A) % 58.98/59.10 & ordinal(A) ) % 58.98/59.10 => ( epsilon_transitive(A) % 58.98/59.10 & epsilon_connected(A) % 58.98/59.10 & ordinal(A) % 58.98/59.10 & natural(A) ) ) ). % 58.98/59.10 % 58.98/59.10 fof(cc2_finset_1,axiom, % 58.98/59.10 ! [A] : % 58.98/59.10 ( finite(A) % 58.98/59.10 => ! [B] : % 58.98/59.10 ( element(B,powerset(A)) % 58.98/59.10 => finite(B) ) ) ). % 58.98/59.10 % 58.98/59.10 fof(cc2_funct_1,axiom, % 58.98/59.10 ! [A] : % 58.98/59.10 ( ( relation(A) % 58.98/59.10 & empty(A) % 58.98/59.10 & function(A) ) % 58.98/59.10 => ( relation(A) % 58.98/59.10 & function(A) % 58.98/59.10 & one_to_one(A) ) ) ). % 58.98/59.10 % 58.98/59.10 fof(cc2_ordinal1,axiom, % 58.98/59.10 ! [A] : % 58.98/59.10 ( ( epsilon_transitive(A) % 58.98/59.10 & epsilon_connected(A) ) % 58.98/59.10 => ordinal(A) ) ). % 58.98/59.10 % 58.98/59.10 fof(cc3_ordinal1,axiom, % 58.98/59.10 ! [A] : % 58.98/59.10 ( empty(A) % 58.98/59.10 => ( epsilon_transitive(A) % 58.98/59.10 & epsilon_connected(A) % 58.98/59.10 & ordinal(A) ) ) ). % 58.98/59.10 % 58.98/59.10 fof(dt_k1_xboole_0,axiom, % 58.98/59.10 $true ). % 58.98/59.10 % 58.98/59.10 fof(dt_k1_zfmisc_1,axiom, % 58.98/59.10 $true ). % 58.98/59.10 % 58.98/59.10 fof(dt_m1_subset_1,axiom, % 58.98/59.10 $true ). % 58.98/59.10 % 58.98/59.10 fof(existence_m1_subset_1,axiom, % 58.98/59.10 ! [A] : % 58.98/59.10 ? [B] : element(B,A) ). % 58.98/59.10 % 58.98/59.10 fof(fc12_relat_1,axiom, % 58.98/59.10 ( empty(empty_set) % 58.98/59.10 & relation(empty_set) % 58.98/59.10 & relation_empty_yielding(empty_set) ) ). % 58.98/59.10 % 58.98/59.10 fof(fc1_subset_1,axiom, % 58.98/59.10 ! [A] : ~ empty(powerset(A)) ). % 58.98/59.10 % 58.98/59.10 fof(fc1_xboole_0,axiom, % 58.98/59.10 empty(empty_set) ). % 58.98/59.10 % 58.98/59.10 fof(fc2_ordinal1,axiom, % 58.98/59.10 ( relation(empty_set) % 58.98/59.10 & relation_empty_yielding(empty_set) % 58.98/59.10 & function(empty_set) % 58.98/59.10 & one_to_one(empty_set) % 58.98/59.10 & empty(empty_set) % 58.98/59.10 & epsilon_transitive(empty_set) % 58.98/59.10 & epsilon_connected(empty_set) % 58.98/59.10 & ordinal(empty_set) ) ). % 58.98/59.10 % 58.98/59.10 fof(fc4_relat_1,axiom, % 58.98/59.10 ( empty(empty_set) % 58.98/59.10 & relation(empty_set) ) ). % 58.98/59.10 % 58.98/59.10 fof(rc1_arytm_3,axiom, % 58.98/59.10 ? [A] : % 58.98/59.10 ( ~ empty(A) % 58.98/59.10 & epsilon_transitive(A) % 58.98/59.10 & epsilon_connected(A) % 58.98/59.10 & ordinal(A) % 58.98/59.10 & natural(A) ) ). % 58.98/59.10 % 58.98/59.10 fof(rc1_finset_1,axiom, % 58.98/59.10 ? [A] : % 58.98/59.11 ( ~ empty(A) % 58.98/59.11 & finite(A) ) ). % 58.98/59.11 % 58.98/59.11 fof(rc1_funct_1,axiom, % 58.98/59.11 ? [A] : % 58.98/59.11 ( relation(A) % 58.98/59.11 & function(A) ) ). % 58.98/59.11 % 58.98/59.11 fof(rc1_ordinal1,axiom, % 58.98/59.11 ? [A] : % 58.98/59.11 ( epsilon_transitive(A) % 58.98/59.11 & epsilon_connected(A) % 58.98/59.11 & ordinal(A) ) ). % 58.98/59.11 % 58.98/59.11 fof(rc1_relat_1,axiom, % 58.98/59.11 ? [A] : % 58.98/59.11 ( empty(A) % 58.98/59.11 & relation(A) ) ). % 58.98/59.11 % 58.98/59.11 fof(rc1_subset_1,axiom, % 58.98/59.11 ! [A] : % 58.98/59.11 ( ~ empty(A) % 58.98/59.11 => ? [B] : % 58.98/59.11 ( element(B,powerset(A)) % 58.98/59.11 & ~ empty(B) ) ) ). % 58.98/59.11 % 58.98/59.11 fof(rc1_xboole_0,axiom, % 58.98/59.11 ? [A] : empty(A) ). % 58.98/59.11 % 58.98/59.11 fof(rc2_finset_1,axiom, % 58.98/59.11 ! [A] : % 58.98/59.11 ? [B] : % 58.98/59.11 ( element(B,powerset(A)) % 58.98/59.11 & empty(B) % 58.98/59.11 & relation(B) % 58.98/59.11 & function(B) % 58.98/59.11 & one_to_one(B) % 58.98/59.11 & epsilon_transitive(B) % 58.98/59.11 & epsilon_connected(B) % 58.98/59.11 & ordinal(B) % 58.98/59.11 & natural(B) % 58.98/59.11 & finite(B) ) ). % 58.98/59.11 % 58.98/59.11 fof(rc2_funct_1,axiom, % 58.98/59.11 ? [A] : % 58.98/59.11 ( relation(A) % 58.98/59.11 & empty(A) % 58.98/59.11 & function(A) ) ). % 58.98/59.11 % 58.98/59.11 fof(rc2_ordinal1,axiom, % 58.98/59.11 ? [A] : % 58.98/59.11 ( relation(A) % 58.98/59.11 & function(A) % 58.98/59.11 & one_to_one(A) % 58.98/59.11 & empty(A) % 58.98/59.11 & epsilon_transitive(A) % 58.98/59.11 & epsilon_connected(A) % 58.98/59.11 & ordinal(A) ) ). % 58.98/59.11 % 58.98/59.11 fof(rc2_relat_1,axiom, % 58.98/59.11 ? [A] : % 58.98/59.11 ( ~ empty(A) % 58.98/59.11 & relation(A) ) ). % 58.98/59.11 % 58.98/59.11 fof(rc2_subset_1,axiom, % 58.98/59.11 ! [A] : % 58.98/59.11 ? [B] : % 58.98/59.11 ( element(B,powerset(A)) % 58.98/59.11 & empty(B) ) ). % 58.98/59.11 % 58.98/59.11 fof(rc2_xboole_0,axiom, % 58.98/59.11 ? [A] : ~ empty(A) ). % 58.98/59.11 % 58.98/59.11 fof(rc3_finset_1,axiom, % 58.98/59.11 ! [A] : % 58.98/59.11 ( ~ empty(A) % 58.98/59.11 => ? [B] : % 58.98/59.11 ( element(B,powerset(A)) % 58.98/59.11 & ~ empty(B) % 58.98/59.11 & finite(B) ) ) ). % 58.98/59.11 % 58.98/59.11 fof(rc3_funct_1,axiom, % 58.98/59.11 ? [A] : % 58.98/59.11 ( relation(A) % 58.98/59.11 & function(A) % 58.98/59.11 & one_to_one(A) ) ). % 58.98/59.11 % 58.98/59.11 fof(rc3_ordinal1,axiom, % 58.98/59.11 ? [A] : % 58.98/59.11 ( ~ empty(A) % 58.98/59.11 & epsilon_transitive(A) % 58.98/59.11 & epsilon_connected(A) % 58.98/59.11 & ordinal(A) ) ). % 58.98/59.11 % 58.98/59.11 fof(rc3_relat_1,axiom, % 58.98/59.11 ? [A] : % 58.98/59.11 ( relation(A) % 58.98/59.11 & relation_empty_yielding(A) ) ). % 58.98/59.11 % 58.98/59.11 fof(rc4_funct_1,axiom, % 58.98/59.11 ? [A] : % 58.98/59.11 ( relation(A) % 58.98/59.11 & relation_empty_yielding(A) % 58.98/59.11 & function(A) ) ). % 58.98/59.11 % 58.98/59.11 fof(reflexivity_r1_tarski,axiom, % 58.98/59.11 ! [A,B] : subset(A,A) ). % 58.98/59.11 % 58.98/59.11 fof(t13_finset_1,conjecture, % 58.98/59.11 ! [A,B] : % 58.98/59.11 ( ( subset(A,B) % 58.98/59.11 & finite(B) ) % 58.98/59.11 => finite(A) ) ). % 58.98/59.11 % 58.98/59.11 fof(t1_subset,axiom, % 58.98/59.11 ! [A,B] : % 58.98/59.11 ( in(A,B) % 58.98/59.11 => element(A,B) ) ). % 58.98/59.11 % 58.98/59.11 fof(t2_subset,axiom, % 58.98/59.11 ! [A,B] : % 58.98/59.11 ( element(A,B) % 58.98/59.11 => ( empty(B) % 58.98/59.11 | in(A,B) ) ) ). % 58.98/59.11 % 58.98/59.11 fof(t3_subset,axiom, % 58.98/59.11 ! [A,B] : % 58.98/59.11 ( element(A,powerset(B)) % 58.98/59.11 <=> subset(A,B) ) ). % 58.98/59.11 % 58.98/59.11 fof(t4_subset,axiom, % 58.98/59.11 ! [A,B,C] : % 58.98/59.11 ( ( in(A,B) % 58.98/59.11 & element(B,powerset(C)) ) % 58.98/59.11 => element(A,C) ) ). % 58.98/59.11 % 58.98/59.11 fof(t5_subset,axiom, % 58.98/59.11 ! [A,B,C] : % 58.98/59.11 ~ ( in(A,B) % 58.98/59.11 & element(B,powerset(C)) % 58.98/59.11 & empty(C) ) ). % 58.98/59.11 % 58.98/59.11 fof(t6_boole,axiom, % 58.98/59.11 ! [A] : % 58.98/59.11 ( empty(A) % 58.98/59.11 => A = empty_set ) ). % 58.98/59.11 % 58.98/59.11 fof(t7_boole,axiom, % 58.98/59.11 ! [A,B] : % 58.98/59.11 ~ ( in(A,B) % 58.98/59.11 & empty(B) ) ). % 58.98/59.11 % 58.98/59.11 fof(t8_boole,axiom, % 58.98/59.11 ! [A,B] : % 58.98/59.11 ~ ( empty(A) % 58.98/59.11 & A != B % 58.98/59.11 & empty(B) ) ). % 58.98/59.11 % 58.98/59.11 %------------------------------------------------------------------------------ % 58.98/59.11 %------------------------------------------- % 58.98/59.11 % Proof found % 58.98/59.11 % SZS status Theorem for theBenchmark % 58.98/59.11 % SZS output start Proof % 58.98/59.11 %ClaNum:129(EqnAxiom:25) % 58.98/59.11 %VarNum:114(SingletonVarNum:60) % 58.98/59.11 %MaxLitNum:4 % 58.98/59.11 %MaxfuncDepth:1 % 58.98/59.11 %SharedTerms:68 % 58.98/59.11 %goalClause: 50 86 96 % 58.98/59.11 %singleGoalClaCount:3 % 58.98/59.11 [26]P1(a1) % 58.98/59.11 [27]P1(a2) % 58.98/59.11 [28]P1(a16) % 58.98/59.11 [29]P1(a3) % 58.98/59.11 [30]P1(a5) % 58.98/59.11 [31]P2(a1) % 58.98/59.11 [32]P2(a2) % 58.98/59.11 [33]P2(a16) % 58.98/59.11 [34]P2(a3) % 58.98/59.11 [35]P2(a5) % 58.98/59.11 [36]P3(a1) % 58.98/59.11 [37]P3(a2) % 58.98/59.11 [38]P3(a16) % 58.98/59.11 [39]P3(a3) % 58.98/59.11 [40]P3(a5) % 58.98/59.11 [44]P4(a1) % 58.98/59.11 [45]P4(a19) % 58.98/59.11 [46]P4(a20) % 58.98/59.11 [47]P4(a4) % 58.98/59.11 [48]P4(a3) % 58.98/59.11 [49]P6(a17) % 58.98/59.11 [50]P6(a11) % 58.98/59.11 [51]P7(a1) % 58.98/59.11 [52]P7(a18) % 58.98/59.11 [53]P7(a4) % 58.98/59.11 [54]P7(a3) % 58.98/59.11 [55]P7(a6) % 58.98/59.11 [56]P7(a12) % 58.98/59.11 [59]P11(a1) % 58.98/59.11 [60]P11(a18) % 58.98/59.11 [61]P11(a19) % 58.98/59.11 [62]P11(a4) % 58.98/59.11 [63]P11(a3) % 58.98/59.11 [64]P11(a7) % 58.98/59.11 [65]P11(a6) % 58.98/59.11 [66]P11(a13) % 58.98/59.11 [67]P11(a12) % 58.98/59.11 [68]P8(a2) % 58.98/59.11 [69]P10(a1) % 58.98/59.11 [70]P10(a3) % 58.98/59.11 [71]P10(a6) % 58.98/59.11 [73]P12(a1) % 58.98/59.11 [74]P12(a13) % 58.98/59.11 [75]P12(a12) % 58.98/59.11 [86]P13(a14,a11) % 58.98/59.11 [91]~P4(a2) % 58.98/59.11 [92]~P4(a17) % 58.98/59.11 [93]~P4(a7) % 58.98/59.11 [94]~P4(a9) % 58.98/59.11 [95]~P4(a5) % 58.98/59.11 [96]~P6(a14) % 58.98/59.11 [87]P13(x871,x871) % 58.98/59.11 [76]P1(f22(x761)) % 58.98/59.11 [77]P2(f22(x771)) % 58.98/59.11 [78]P3(f22(x781)) % 58.98/59.11 [79]P4(f22(x791)) % 58.98/59.11 [80]P4(f8(x801)) % 58.98/59.11 [81]P6(f22(x811)) % 58.98/59.11 [82]P7(f22(x821)) % 58.98/59.11 [83]P11(f22(x831)) % 58.98/59.11 [84]P8(f22(x841)) % 58.98/59.11 [85]P10(f22(x851)) % 58.98/59.11 [88]P5(f15(x881),x881) % 58.98/59.11 [89]P5(f22(x891),f23(x891)) % 58.98/59.11 [90]P5(f8(x901),f23(x901)) % 58.98/59.11 [97]~P4(f23(x971)) % 58.98/59.11 [98]~P4(x981)+E(x981,a1) % 58.98/59.11 [99]~P4(x991)+P1(x991) % 58.98/59.11 [100]~P1(x1001)+P2(x1001) % 58.98/59.11 [101]~P4(x1011)+P2(x1011) % 58.98/59.11 [102]~P1(x1021)+P3(x1021) % 58.98/59.11 [103]~P4(x1031)+P3(x1031) % 58.98/59.11 [104]~P4(x1041)+P6(x1041) % 58.98/59.11 [105]~P4(x1051)+P7(x1051) % 58.98/59.11 [106]~P4(x1061)+P11(x1061) % 58.98/59.11 [107]P4(x1071)+P6(f10(x1071)) % 58.98/59.11 [113]P4(x1131)+~P4(f21(x1131)) % 58.98/59.11 [114]P4(x1141)+~P4(f10(x1141)) % 58.98/59.11 [117]P4(x1171)+P5(f21(x1171),f23(x1171)) % 58.98/59.11 [118]P4(x1181)+P5(f10(x1181),f23(x1181)) % 58.98/59.11 [116]~P4(x1161)+~P9(x1162,x1161) % 58.98/59.11 [122]~P9(x1221,x1222)+P5(x1221,x1222) % 58.98/59.11 [126]~P9(x1262,x1261)+~P9(x1261,x1262) % 58.98/59.11 [124]~P13(x1241,x1242)+P5(x1241,f23(x1242)) % 58.98/59.11 [127]P13(x1271,x1272)+~P5(x1271,f23(x1272)) % 58.98/59.11 [109]~P2(x1091)+~P3(x1091)+P1(x1091) % 58.98/59.11 [112]~P1(x1121)+~P4(x1121)+P8(x1121) % 58.98/59.11 [108]~P4(x1082)+~P4(x1081)+E(x1081,x1082) % 58.98/59.11 [119]~P5(x1191,x1192)+P1(x1191)+~P1(x1192) % 58.98/59.11 [120]~P5(x1201,x1202)+P2(x1201)+~P1(x1202) % 58.98/59.11 [121]~P5(x1211,x1212)+P3(x1211)+~P1(x1212) % 58.98/59.11 [123]~P5(x1232,x1231)+P4(x1231)+P9(x1232,x1231) % 58.98/59.11 [125]P6(x1251)+~P6(x1252)+~P5(x1251,f23(x1252)) % 58.98/59.11 [128]~P4(x1281)+~P9(x1282,x1283)+~P5(x1283,f23(x1281)) % 58.98/59.11 [129]P5(x1291,x1292)+~P9(x1291,x1293)+~P5(x1293,f23(x1292)) % 58.98/59.11 [115]~P4(x1151)+~P7(x1151)+~P11(x1151)+P10(x1151) % 58.98/59.11 %EqnAxiom % 58.98/59.11 [1]E(x11,x11) % 58.98/59.11 [2]E(x22,x21)+~E(x21,x22) % 58.98/59.11 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 58.98/59.11 [4]~E(x41,x42)+E(f22(x41),f22(x42)) % 58.98/59.11 [5]~E(x51,x52)+E(f23(x51),f23(x52)) % 58.98/59.11 [6]~E(x61,x62)+E(f10(x61),f10(x62)) % 58.98/59.11 [7]~E(x71,x72)+E(f21(x71),f21(x72)) % 58.98/59.11 [8]~E(x81,x82)+E(f8(x81),f8(x82)) % 58.98/59.11 [9]~E(x91,x92)+E(f15(x91),f15(x92)) % 58.98/59.11 [10]~P1(x101)+P1(x102)+~E(x101,x102) % 58.98/59.11 [11]P5(x112,x113)+~E(x111,x112)+~P5(x111,x113) % 58.98/59.11 [12]P5(x123,x122)+~E(x121,x122)+~P5(x123,x121) % 58.98/59.11 [13]P9(x132,x133)+~E(x131,x132)+~P9(x131,x133) % 58.98/59.11 [14]P9(x143,x142)+~E(x141,x142)+~P9(x143,x141) % 58.98/59.11 [15]~P4(x151)+P4(x152)+~E(x151,x152) % 58.98/59.11 [16]~P10(x161)+P10(x162)+~E(x161,x162) % 58.98/59.11 [17]~P2(x171)+P2(x172)+~E(x171,x172) % 58.98/59.11 [18]~P3(x181)+P3(x182)+~E(x181,x182) % 58.98/59.11 [19]P13(x192,x193)+~E(x191,x192)+~P13(x191,x193) % 58.98/59.11 [20]P13(x203,x202)+~E(x201,x202)+~P13(x203,x201) % 58.98/59.11 [21]~P8(x211)+P8(x212)+~E(x211,x212) % 58.98/59.11 [22]~P6(x221)+P6(x222)+~E(x221,x222) % 58.98/59.11 [23]~P11(x231)+P11(x232)+~E(x231,x232) % 58.98/59.11 [24]~P7(x241)+P7(x242)+~E(x241,x242) % 58.98/59.11 [25]~P12(x251)+P12(x252)+~E(x251,x252) % 58.98/59.11 % 58.98/59.11 %------------------------------------------- % 58.98/59.11 cnf(130,plain, % 58.98/59.11 (~P4(a14)), % 58.98/59.12 inference(scs_inference,[],[96,104])). % 58.98/59.12 cnf(132,plain, % 58.98/59.12 (P13(f15(f23(x1321)),x1321)), % 58.98/59.12 inference(scs_inference,[],[96,88,104,127])). % 58.98/59.12 cnf(133,plain, % 58.98/59.12 (P5(f15(x1331),x1331)), % 58.98/59.12 inference(rename_variables,[],[88])). % 58.98/59.12 cnf(138,plain, % 58.98/59.12 (P5(f15(x1381),x1381)), % 58.98/59.12 inference(rename_variables,[],[88])). % 58.98/59.12 cnf(140,plain, % 58.98/59.12 (P9(f15(a2),a2)), % 58.98/59.12 inference(scs_inference,[],[50,96,88,133,138,44,91,104,127,116,125,123])). % 58.98/59.12 cnf(141,plain, % 58.98/59.12 (P5(f15(x1411),x1411)), % 58.98/59.12 inference(rename_variables,[],[88])). % 58.98/59.12 cnf(143,plain, % 58.98/59.12 (~P9(x1431,f15(f23(a1)))), % 58.98/59.12 inference(scs_inference,[],[50,96,88,133,138,141,44,91,104,127,116,125,123,128])). % 58.98/59.12 cnf(144,plain, % 58.98/59.12 (P5(f15(x1441),x1441)), % 58.98/59.12 inference(rename_variables,[],[88])). % 58.98/59.12 cnf(146,plain, % 58.98/59.12 (P8(a1)), % 58.98/59.12 inference(scs_inference,[],[50,96,88,133,138,141,44,91,26,104,127,116,125,123,128,112])). % 58.98/59.12 cnf(148,plain, % 58.98/59.12 (~E(a2,a1)), % 58.98/59.12 inference(scs_inference,[],[50,96,88,133,138,141,44,91,26,104,127,116,125,123,128,112,14])). % 58.98/59.12 cnf(154,plain, % 58.98/59.12 (P13(a14,x1541)+~E(a11,x1541)), % 58.98/59.12 inference(scs_inference,[],[50,86,96,88,133,138,141,44,47,91,26,53,62,104,127,116,125,123,128,112,14,115,126,19,20])). % 58.98/59.12 cnf(156,plain, % 58.98/59.12 (P5(f15(x1561),x1561)), % 58.98/59.12 inference(rename_variables,[],[88])). % 58.98/59.12 cnf(159,plain, % 58.98/59.12 (P5(f15(x1591),x1592)+~E(x1591,x1592)), % 58.98/59.12 inference(scs_inference,[],[50,86,96,88,133,138,141,144,156,44,47,91,26,53,62,104,127,116,125,123,128,112,14,115,126,19,20,129,11,12])). % 58.98/59.12 cnf(166,plain, % 58.98/59.12 (~P9(x1661,a19)), % 58.98/59.12 inference(scs_inference,[],[45,116])). % 58.98/59.12 cnf(168,plain, % 58.98/59.12 (P13(f22(x1681),x1681)), % 58.98/59.12 inference(scs_inference,[],[89,45,116,127])). % 58.98/59.12 cnf(178,plain, % 58.98/59.12 (~P9(x1781,f22(a19))), % 58.98/59.12 inference(scs_inference,[],[50,130,89,90,45,48,88,29,116,127,125,112,123,128])). % 58.98/59.12 cnf(179,plain, % 58.98/59.12 (P5(f22(x1791),f23(x1791))), % 58.98/59.12 inference(rename_variables,[],[89])). % 58.98/59.12 cnf(185,plain, % 58.98/59.12 (P13(x1851,x1852)+~E(x1852,x1851)), % 58.98/59.12 inference(scs_inference,[],[50,130,87,143,140,89,90,45,48,88,29,116,127,125,112,123,128,14,126,19])). % 58.98/59.12 cnf(190,plain, % 58.98/59.12 (P13(x1901,x1902)+~E(x1901,x1902)), % 58.98/59.12 inference(scs_inference,[],[50,130,87,143,140,89,179,90,45,48,88,29,116,127,125,112,123,128,14,126,19,12,129,13,20])). % 58.98/59.12 cnf(199,plain, % 58.98/59.12 (P13(f8(x1991),x1991)), % 58.98/59.12 inference(scs_inference,[],[46,90,116,127])). % 58.98/59.12 cnf(204,plain, % 58.98/59.12 (~P9(x2041,f8(a20))), % 58.98/59.12 inference(scs_inference,[],[46,90,88,92,116,127,123,128])). % 58.98/59.12 cnf(205,plain, % 58.98/59.12 (P5(f8(x2051),f23(x2051))), % 58.98/59.12 inference(rename_variables,[],[90])). % 58.98/59.12 cnf(218,plain, % 58.98/59.12 (P13(f22(x2181),x2182)+~E(x2181,x2182)), % 58.98/59.12 inference(scs_inference,[],[140,168,178,46,90,205,88,92,116,127,123,128,14,126,112,129,19,12,13,20])). % 58.98/59.12 cnf(225,plain, % 58.98/59.12 (P9(f15(a7),a7)), % 58.98/59.12 inference(scs_inference,[],[79,88,93,116,123])). % 58.98/59.12 cnf(228,plain, % 58.98/59.12 (~P9(x2281,f8(f22(x2282)))), % 58.98/59.12 inference(scs_inference,[],[79,88,90,93,116,123,128])). % 58.98/59.12 cnf(229,plain, % 58.98/59.12 (P5(f8(x2291),f23(x2291))), % 58.98/59.12 inference(rename_variables,[],[90])). % 58.98/59.12 cnf(240,plain, % 58.98/59.12 (P13(f8(x2401),x2402)+~E(x2401,x2402)), % 58.98/59.12 inference(scs_inference,[],[140,199,204,79,80,88,90,229,93,116,123,128,14,126,112,19,11,13,20])). % 58.98/59.12 cnf(250,plain, % 58.98/59.12 (P5(f15(x2501),x2501)), % 59.09/59.12 inference(rename_variables,[],[88])). % 59.09/59.12 cnf(263,plain, % 59.09/59.12 (P13(f15(f23(x2631)),x2632)+~E(x2631,x2632)), % 59.09/59.12 inference(scs_inference,[],[140,132,228,47,88,250,94,116,123,128,14,126,112,19,13,20])). % 59.09/59.12 cnf(271,plain, % 59.09/59.12 (~P9(x2711,f8(a3))), % 59.09/59.12 inference(scs_inference,[],[90,48,116,128])). % 59.09/59.12 cnf(292,plain, % 59.09/59.12 (P9(x2921,f23(x2922))+~E(f22(x2922),x2921)), % 59.09/59.12 inference(scs_inference,[],[89,140,80,271,97,116,123,14,13])). % 59.09/59.12 cnf(346,plain, % 59.09/59.12 (~P9(x3461,f15(f23(a19)))), % 59.09/59.12 inference(scs_inference,[],[88,45,128])). % 59.09/59.12 cnf(387,plain, % 59.09/59.12 (E(a1,a19)), % 59.09/59.12 inference(scs_inference,[],[45,2,98])). % 59.09/59.12 cnf(394,plain, % 59.09/59.12 (E(a19,a1)), % 59.09/59.12 inference(scs_inference,[],[387,185,190,218,240,263,159,2])). % 59.09/59.12 cnf(405,plain, % 59.09/59.12 (~P6(a1)+P6(a19)), % 59.09/59.12 inference(scs_inference,[],[26,225,387,346,148,146,51,36,31,69,73,185,190,218,240,263,159,2,3,10,16,17,18,21,24,25,14,22])). % 59.09/59.12 cnf(411,plain, % 59.09/59.12 (P6(a19)), % 59.09/59.12 inference(scs_inference,[],[44,405,104])). % 59.09/59.12 cnf(413,plain, % 59.09/59.12 (P13(f22(a19),a1)), % 59.09/59.12 inference(scs_inference,[],[394,218])). % 59.09/59.12 cnf(416,plain, % 59.09/59.12 (P5(f15(a19),a1)), % 59.09/59.12 inference(scs_inference,[],[394,218,240,263,159])). % 59.09/59.12 cnf(417,plain, % 59.09/59.12 (P6(a1)), % 59.09/59.12 inference(scs_inference,[],[411,394,218,240,263,159,22])). % 59.09/59.12 cnf(462,plain, % 59.09/59.12 (P1(f15(a2))), % 59.09/59.12 inference(scs_inference,[],[140,27,122,119])). % 59.09/59.12 cnf(468,plain, % 59.09/59.12 (P5(a1,f23(a19))), % 59.09/59.12 inference(scs_inference,[],[394,124,185])). % 59.09/59.12 cnf(469,plain, % 59.09/59.12 (P9(a1,f23(a19))), % 59.09/59.12 inference(scs_inference,[],[468,97,123])). % 59.09/59.12 cnf(543,plain, % 59.09/59.12 (P2(a4)), % 59.09/59.12 inference(scs_inference,[],[47,99,100])). % 59.09/59.12 cnf(555,plain, % 59.09/59.12 (P3(a4)), % 59.09/59.12 inference(scs_inference,[],[47,99,102])). % 59.09/59.12 cnf(556,plain, % 59.09/59.12 (P1(a4)), % 59.09/59.12 inference(scs_inference,[],[543,555,109])). % 59.09/59.12 cnf(1242,plain, % 59.09/59.12 (E(a1,a4)), % 59.09/59.12 inference(scs_inference,[],[47,98,2])). % 59.09/59.12 cnf(1244,plain, % 59.09/59.12 (E(a4,a1)), % 59.09/59.12 inference(scs_inference,[],[1242,185,2])). % 59.09/59.12 cnf(1261,plain, % 59.09/59.12 (P13(f22(a4),a19)), % 59.09/59.12 inference(scs_inference,[],[387,1244,218,240,263,159,20])). % 59.09/59.12 cnf(1770,plain, % 59.09/59.12 (P5(f15(a19),a4)), % 59.09/59.12 inference(scs_inference,[],[1242,413,416,469,13,20,12])). % 59.09/59.12 cnf(2279,plain, % 59.09/59.12 (~P4(a11)+P13(a14,a1)), % 59.09/59.12 inference(scs_inference,[],[98,154])). % 59.09/59.12 cnf(2288,plain, % 59.09/59.12 (P9(a1,f23(x22881))), % 59.09/59.12 inference(scs_inference,[],[79,98,292])). % 59.09/59.12 cnf(2289,plain, % 59.09/59.12 (P9(a19,f23(x22891))), % 59.09/59.12 inference(scs_inference,[],[387,2288,13])). % 59.09/59.12 cnf(2321,plain, % 59.09/59.12 (E(a4,a19)), % 59.09/59.12 inference(scs_inference,[],[47,387,98,3])). % 59.09/59.12 cnf(2322,plain, % 59.09/59.12 (E(a19,a4)), % 59.09/59.12 inference(scs_inference,[],[2321,2])). % 59.09/59.12 cnf(2515,plain, % 59.09/59.12 (P5(a14,f23(a1))+~P4(a11)), % 59.09/59.12 inference(scs_inference,[],[2279,124])). % 59.09/59.12 cnf(2516,plain, % 59.09/59.12 (~P4(a11)), % 59.09/59.12 inference(scs_inference,[],[417,96,2515,125])). % 59.09/59.12 cnf(2517,plain, % 59.09/59.12 (P9(f15(a11),a11)), % 59.09/59.12 inference(scs_inference,[],[88,2516,123])). % 59.09/59.12 cnf(2573,plain, % 59.09/59.12 (~E(a11,a19)), % 59.09/59.12 inference(scs_inference,[],[2517,166,14])). % 59.09/59.12 cnf(2644,plain, % 59.09/59.12 (~P5(a14,f23(a11))), % 59.09/59.12 inference(scs_inference,[],[50,2573,2289,2322,1261,2516,1770,556,462,79,45,48,46,96,100,107,113,114,124,117,118,4,5,6,7,8,9,98,105,104,106,2,119,120,121,3,128,125])). % 59.09/59.12 cnf(2914,plain, % 59.09/59.12 ($false), % 59.09/59.12 inference(scs_inference,[],[2644,86,124]), % 59.09/59.12 ['proof']). % 59.09/59.12 % SZS output end Proof % 59.09/59.12 % Total time :58.450000s %------------------------------------------------------------------------------