%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SEU295+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 : n022.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 0.57s 0.65s % Output : CNFRefutation 0.57s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SEU295+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.33 % Computer : n022.cluster.edu % 0.11/0.33 % Model : x86_64 x86_64 % 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.33 % Memory : 8042.1875MB % 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.33 % CPULimit : 300 % 0.11/0.33 % WCLimit : 300 % 0.11/0.33 % DateTime : Fri Jun 21 16:52:09 EDT 2024 % 0.11/0.33 % CPUTime : % 0.49/0.59 start to proof:theBenchmark % 0.57/0.64 %------------------------------------------- % 0.57/0.64 % File :CSE---1.7 % 0.57/0.64 % Problem :theBenchmark % 0.57/0.64 % Transform :cnf % 0.57/0.64 % Format :tptp:raw % 0.57/0.64 % Command :java -jar mcs_scs.jar %d %s % 0.57/0.64 % 0.57/0.64 % Result :Theorem 0.000000s % 0.57/0.64 % Output :CNFRefutation 0.000000s % 0.57/0.64 %------------------------------------------- % 0.57/0.64 %------------------------------------------------------------------------------ % 0.57/0.64 % File : SEU295+1 : TPTP v8.2.0. Released v3.3.0. % 0.57/0.64 % Domain : Set theory % 0.57/0.64 % Problem : MPTP bushy problem t15_finset_1 % 0.57/0.64 % Version : [Urb07] axioms : Especial. % 0.57/0.64 % English : % 0.57/0.64 % 0.57/0.64 % Refs : [Ban01] Bancerek et al. (2001), On the Characterizations of Co % 0.57/0.64 % : [Urb07] Urban (2006), Email to G. Sutcliffe % 0.57/0.64 % Source : [Urb07] % 0.57/0.64 % Names : bushy-t15_finset_1 [Urb07] % 0.57/0.64 % 0.57/0.64 % Status : Theorem % 0.57/0.64 % Rating : 0.03 v8.1.0, 0.00 v6.4.0, 0.04 v6.2.0, 0.08 v6.1.0, 0.07 v6.0.0, 0.04 v5.4.0, 0.07 v5.3.0, 0.11 v5.2.0, 0.00 v4.0.0, 0.04 v3.7.0, 0.05 v3.3.0 % 0.57/0.64 % Syntax : Number of formulae : 57 ( 14 unt; 0 def) % 0.57/0.64 % Number of atoms : 154 ( 5 equ) % 0.57/0.64 % Maximal formula atoms : 10 ( 2 avg) % 0.57/0.64 % Number of connectives : 112 ( 15 ~; 1 |; 71 &) % 0.57/0.64 % ( 1 <=>; 24 =>; 0 <=; 0 <~>) % 0.57/0.64 % Maximal formula depth : 12 ( 4 avg) % 0.57/0.64 % Maximal term depth : 2 ( 1 avg) % 0.57/0.64 % Number of predicates : 15 ( 13 usr; 1 prp; 0-2 aty) % 0.57/0.64 % Number of functors : 3 ( 3 usr; 1 con; 0-2 aty) % 0.57/0.64 % Number of variables : 75 ( 56 !; 19 ?) % 0.57/0.64 % SPC : FOF_THM_RFO_SEQ % 0.57/0.64 % 0.57/0.64 % Comments : Translated by MPTP 0.2 from the original problem in the Mizar % 0.57/0.64 % library, www.mizar.org % 0.57/0.64 %------------------------------------------------------------------------------ % 0.57/0.64 fof(antisymmetry_r2_hidden,axiom, % 0.57/0.64 ! [A,B] : % 0.57/0.64 ( in(A,B) % 0.57/0.64 => ~ in(B,A) ) ). % 0.57/0.64 % 0.57/0.64 fof(cc1_arytm_3,axiom, % 0.57/0.64 ! [A] : % 0.57/0.64 ( ordinal(A) % 0.57/0.64 => ! [B] : % 0.57/0.64 ( element(B,A) % 0.57/0.64 => ( epsilon_transitive(B) % 0.57/0.64 & epsilon_connected(B) % 0.57/0.64 & ordinal(B) ) ) ) ). % 0.57/0.64 % 0.57/0.64 fof(cc1_finset_1,axiom, % 0.57/0.64 ! [A] : % 0.57/0.64 ( empty(A) % 0.57/0.64 => finite(A) ) ). % 0.57/0.64 % 0.57/0.64 fof(cc1_funct_1,axiom, % 0.57/0.64 ! [A] : % 0.57/0.64 ( empty(A) % 0.57/0.64 => function(A) ) ). % 0.57/0.64 % 0.57/0.64 fof(cc1_ordinal1,axiom, % 0.57/0.64 ! [A] : % 0.57/0.64 ( ordinal(A) % 0.57/0.64 => ( epsilon_transitive(A) % 0.57/0.64 & epsilon_connected(A) ) ) ). % 0.57/0.64 % 0.57/0.64 fof(cc1_relat_1,axiom, % 0.57/0.64 ! [A] : % 0.57/0.64 ( empty(A) % 0.57/0.64 => relation(A) ) ). % 0.57/0.64 % 0.57/0.64 fof(cc2_arytm_3,axiom, % 0.57/0.64 ! [A] : % 0.57/0.64 ( ( empty(A) % 0.57/0.64 & ordinal(A) ) % 0.57/0.64 => ( epsilon_transitive(A) % 0.57/0.64 & epsilon_connected(A) % 0.57/0.64 & ordinal(A) % 0.57/0.64 & natural(A) ) ) ). % 0.57/0.64 % 0.57/0.64 fof(cc2_finset_1,axiom, % 0.57/0.64 ! [A] : % 0.57/0.64 ( finite(A) % 0.57/0.64 => ! [B] : % 0.57/0.64 ( element(B,powerset(A)) % 0.57/0.64 => finite(B) ) ) ). % 0.57/0.64 % 0.57/0.64 fof(cc2_funct_1,axiom, % 0.57/0.64 ! [A] : % 0.57/0.64 ( ( relation(A) % 0.57/0.64 & empty(A) % 0.57/0.64 & function(A) ) % 0.57/0.65 => ( relation(A) % 0.57/0.65 & function(A) % 0.57/0.65 & one_to_one(A) ) ) ). % 0.57/0.65 % 0.57/0.65 fof(cc2_ordinal1,axiom, % 0.57/0.65 ! [A] : % 0.57/0.65 ( ( epsilon_transitive(A) % 0.57/0.65 & epsilon_connected(A) ) % 0.57/0.65 => ordinal(A) ) ). % 0.57/0.65 % 0.57/0.65 fof(cc3_ordinal1,axiom, % 0.57/0.65 ! [A] : % 0.57/0.65 ( empty(A) % 0.57/0.65 => ( epsilon_transitive(A) % 0.57/0.65 & epsilon_connected(A) % 0.57/0.65 & ordinal(A) ) ) ). % 0.57/0.65 % 0.57/0.65 fof(commutativity_k3_xboole_0,axiom, % 0.57/0.65 ! [A,B] : set_intersection2(A,B) = set_intersection2(B,A) ). % 0.57/0.65 % 0.57/0.65 fof(dt_k1_xboole_0,axiom, % 0.57/0.65 $true ). % 0.57/0.65 % 0.57/0.65 fof(dt_k1_zfmisc_1,axiom, % 0.57/0.65 $true ). % 0.57/0.65 % 0.57/0.65 fof(dt_k3_xboole_0,axiom, % 0.57/0.65 $true ). % 0.57/0.65 % 0.57/0.65 fof(dt_m1_subset_1,axiom, % 0.57/0.65 $true ). % 0.57/0.65 % 0.57/0.65 fof(existence_m1_subset_1,axiom, % 0.57/0.65 ! [A] : % 0.57/0.65 ? [B] : element(B,A) ). % 0.57/0.65 % 0.57/0.65 fof(fc10_finset_1,axiom, % 0.57/0.65 ! [A,B] : % 0.57/0.65 ( finite(B) % 0.57/0.65 => finite(set_intersection2(A,B)) ) ). % 0.57/0.65 % 0.57/0.65 fof(fc11_finset_1,axiom, % 0.57/0.65 ! [A,B] : % 0.57/0.65 ( finite(A) % 0.57/0.65 => finite(set_intersection2(A,B)) ) ). % 0.57/0.65 % 0.57/0.65 fof(fc12_relat_1,axiom, % 0.57/0.65 ( empty(empty_set) % 0.57/0.65 & relation(empty_set) % 0.57/0.65 & relation_empty_yielding(empty_set) ) ). % 0.57/0.65 % 0.57/0.65 fof(fc1_relat_1,axiom, % 0.57/0.65 ! [A,B] : % 0.57/0.65 ( ( relation(A) % 0.57/0.65 & relation(B) ) % 0.57/0.65 => relation(set_intersection2(A,B)) ) ). % 0.57/0.65 % 0.57/0.65 fof(fc1_subset_1,axiom, % 0.57/0.65 ! [A] : ~ empty(powerset(A)) ). % 0.57/0.65 % 0.57/0.65 fof(fc1_xboole_0,axiom, % 0.57/0.65 empty(empty_set) ). % 0.57/0.65 % 0.57/0.65 fof(fc2_ordinal1,axiom, % 0.57/0.65 ( relation(empty_set) % 0.57/0.65 & relation_empty_yielding(empty_set) % 0.57/0.65 & function(empty_set) % 0.57/0.65 & one_to_one(empty_set) % 0.57/0.65 & empty(empty_set) % 0.57/0.65 & epsilon_transitive(empty_set) % 0.57/0.65 & epsilon_connected(empty_set) % 0.57/0.65 & ordinal(empty_set) ) ). % 0.57/0.65 % 0.57/0.65 fof(fc4_relat_1,axiom, % 0.57/0.65 ( empty(empty_set) % 0.57/0.65 & relation(empty_set) ) ). % 0.57/0.65 % 0.57/0.65 fof(idempotence_k3_xboole_0,axiom, % 0.57/0.65 ! [A,B] : set_intersection2(A,A) = A ). % 0.57/0.65 % 0.57/0.65 fof(rc1_arytm_3,axiom, % 0.57/0.65 ? [A] : % 0.57/0.65 ( ~ empty(A) % 0.57/0.65 & epsilon_transitive(A) % 0.57/0.65 & epsilon_connected(A) % 0.57/0.65 & ordinal(A) % 0.57/0.65 & natural(A) ) ). % 0.57/0.65 % 0.57/0.65 fof(rc1_finset_1,axiom, % 0.57/0.65 ? [A] : % 0.57/0.65 ( ~ empty(A) % 0.57/0.65 & finite(A) ) ). % 0.57/0.65 % 0.57/0.65 fof(rc1_funct_1,axiom, % 0.57/0.65 ? [A] : % 0.57/0.65 ( relation(A) % 0.57/0.65 & function(A) ) ). % 0.57/0.65 % 0.57/0.65 fof(rc1_ordinal1,axiom, % 0.57/0.65 ? [A] : % 0.57/0.65 ( epsilon_transitive(A) % 0.57/0.65 & epsilon_connected(A) % 0.57/0.65 & ordinal(A) ) ). % 0.57/0.65 % 0.57/0.65 fof(rc1_relat_1,axiom, % 0.57/0.65 ? [A] : % 0.57/0.65 ( empty(A) % 0.57/0.65 & relation(A) ) ). % 0.57/0.65 % 0.57/0.65 fof(rc1_subset_1,axiom, % 0.57/0.65 ! [A] : % 0.57/0.65 ( ~ empty(A) % 0.57/0.65 => ? [B] : % 0.57/0.65 ( element(B,powerset(A)) % 0.57/0.65 & ~ empty(B) ) ) ). % 0.57/0.65 % 0.57/0.65 fof(rc1_xboole_0,axiom, % 0.57/0.65 ? [A] : empty(A) ). % 0.57/0.65 % 0.57/0.65 fof(rc2_finset_1,axiom, % 0.57/0.65 ! [A] : % 0.57/0.65 ? [B] : % 0.57/0.65 ( element(B,powerset(A)) % 0.57/0.65 & empty(B) % 0.57/0.65 & relation(B) % 0.57/0.65 & function(B) % 0.57/0.65 & one_to_one(B) % 0.57/0.65 & epsilon_transitive(B) % 0.57/0.65 & epsilon_connected(B) % 0.57/0.65 & ordinal(B) % 0.57/0.65 & natural(B) % 0.57/0.65 & finite(B) ) ). % 0.57/0.65 % 0.57/0.65 fof(rc2_funct_1,axiom, % 0.57/0.65 ? [A] : % 0.57/0.65 ( relation(A) % 0.57/0.65 & empty(A) % 0.57/0.65 & function(A) ) ). % 0.57/0.65 % 0.57/0.65 fof(rc2_ordinal1,axiom, % 0.57/0.65 ? [A] : % 0.57/0.65 ( relation(A) % 0.57/0.65 & function(A) % 0.57/0.65 & one_to_one(A) % 0.57/0.65 & empty(A) % 0.57/0.65 & epsilon_transitive(A) % 0.57/0.65 & epsilon_connected(A) % 0.57/0.65 & ordinal(A) ) ). % 0.57/0.65 % 0.57/0.65 fof(rc2_relat_1,axiom, % 0.57/0.65 ? [A] : % 0.57/0.65 ( ~ empty(A) % 0.57/0.65 & relation(A) ) ). % 0.57/0.65 % 0.57/0.65 fof(rc2_subset_1,axiom, % 0.57/0.65 ! [A] : % 0.57/0.65 ? [B] : % 0.57/0.65 ( element(B,powerset(A)) % 0.57/0.65 & empty(B) ) ). % 0.57/0.65 % 0.57/0.65 fof(rc2_xboole_0,axiom, % 0.57/0.65 ? [A] : ~ empty(A) ). % 0.57/0.65 % 0.57/0.65 fof(rc3_finset_1,axiom, % 0.57/0.65 ! [A] : % 0.57/0.65 ( ~ empty(A) % 0.57/0.65 => ? [B] : % 0.57/0.65 ( element(B,powerset(A)) % 0.57/0.65 & ~ empty(B) % 0.57/0.65 & finite(B) ) ) ). % 0.57/0.65 % 0.57/0.65 fof(rc3_funct_1,axiom, % 0.57/0.65 ? [A] : % 0.57/0.65 ( relation(A) % 0.57/0.65 & function(A) % 0.57/0.65 & one_to_one(A) ) ). % 0.57/0.65 % 0.57/0.65 fof(rc3_ordinal1,axiom, % 0.57/0.65 ? [A] : % 0.57/0.65 ( ~ empty(A) % 0.57/0.65 & epsilon_transitive(A) % 0.57/0.65 & epsilon_connected(A) % 0.57/0.65 & ordinal(A) ) ). % 0.57/0.65 % 0.57/0.65 fof(rc3_relat_1,axiom, % 0.57/0.65 ? [A] : % 0.57/0.65 ( relation(A) % 0.57/0.65 & relation_empty_yielding(A) ) ). % 0.57/0.65 % 0.57/0.65 fof(rc4_funct_1,axiom, % 0.57/0.65 ? [A] : % 0.57/0.65 ( relation(A) % 0.57/0.65 & relation_empty_yielding(A) % 0.57/0.65 & function(A) ) ). % 0.57/0.65 % 0.57/0.65 fof(reflexivity_r1_tarski,axiom, % 0.57/0.65 ! [A,B] : subset(A,A) ). % 0.57/0.65 % 0.57/0.65 fof(t13_finset_1,axiom, % 0.57/0.65 ! [A,B] : % 0.57/0.65 ( ( subset(A,B) % 0.57/0.65 & finite(B) ) % 0.57/0.65 => finite(A) ) ). % 0.57/0.65 % 0.57/0.65 fof(t15_finset_1,conjecture, % 0.57/0.65 ! [A,B] : % 0.57/0.65 ( finite(A) % 0.57/0.65 => finite(set_intersection2(A,B)) ) ). % 0.57/0.65 % 0.57/0.65 fof(t17_xboole_1,axiom, % 0.57/0.65 ! [A,B] : subset(set_intersection2(A,B),A) ). % 0.57/0.65 % 0.57/0.65 fof(t1_subset,axiom, % 0.57/0.65 ! [A,B] : % 0.57/0.65 ( in(A,B) % 0.57/0.65 => element(A,B) ) ). % 0.57/0.65 % 0.57/0.65 fof(t2_boole,axiom, % 0.57/0.65 ! [A] : set_intersection2(A,empty_set) = empty_set ). % 0.57/0.65 % 0.57/0.65 fof(t2_subset,axiom, % 0.57/0.65 ! [A,B] : % 0.57/0.65 ( element(A,B) % 0.57/0.65 => ( empty(B) % 0.57/0.65 | in(A,B) ) ) ). % 0.57/0.65 % 0.57/0.65 fof(t3_subset,axiom, % 0.57/0.65 ! [A,B] : % 0.57/0.65 ( element(A,powerset(B)) % 0.57/0.65 <=> subset(A,B) ) ). % 0.57/0.65 % 0.57/0.65 fof(t4_subset,axiom, % 0.57/0.65 ! [A,B,C] : % 0.57/0.65 ( ( in(A,B) % 0.57/0.65 & element(B,powerset(C)) ) % 0.57/0.65 => element(A,C) ) ). % 0.57/0.65 % 0.57/0.65 fof(t5_subset,axiom, % 0.57/0.65 ! [A,B,C] : % 0.57/0.65 ~ ( in(A,B) % 0.57/0.65 & element(B,powerset(C)) % 0.57/0.65 & empty(C) ) ). % 0.57/0.65 % 0.57/0.65 fof(t6_boole,axiom, % 0.57/0.65 ! [A] : % 0.57/0.65 ( empty(A) % 0.57/0.65 => A = empty_set ) ). % 0.57/0.65 % 0.57/0.65 fof(t7_boole,axiom, % 0.57/0.65 ! [A,B] : % 0.57/0.65 ~ ( in(A,B) % 0.57/0.65 & empty(B) ) ). % 0.57/0.65 % 0.57/0.65 fof(t8_boole,axiom, % 0.57/0.65 ! [A,B] : % 0.57/0.65 ~ ( empty(A) % 0.57/0.65 & A != B % 0.57/0.65 & empty(B) ) ). % 0.57/0.65 % 0.57/0.65 %------------------------------------------------------------------------------ % 0.57/0.65 %------------------------------------------- % 0.57/0.65 % Proof found % 0.57/0.65 % SZS status Theorem for theBenchmark % 0.57/0.65 % SZS output start Proof % 0.57/0.66 %ClaNum:138(EqnAxiom:27) % 0.57/0.66 %VarNum:139(SingletonVarNum:74) % 0.57/0.66 %MaxLitNum:4 % 0.57/0.66 %MaxfuncDepth:1 % 0.57/0.66 %SharedTerms:68 % 0.57/0.66 %goalClause: 52 102 % 0.57/0.66 %singleGoalClaCount:2 % 0.57/0.66 [28]P1(a1) % 0.57/0.66 [29]P1(a2) % 0.57/0.66 [30]P1(a16) % 0.57/0.66 [31]P1(a3) % 0.57/0.66 [32]P1(a5) % 0.57/0.66 [33]P2(a1) % 0.57/0.66 [34]P2(a2) % 0.57/0.66 [35]P2(a16) % 0.57/0.66 [36]P2(a3) % 0.57/0.66 [37]P2(a5) % 0.57/0.66 [38]P3(a1) % 0.57/0.66 [39]P3(a2) % 0.57/0.66 [40]P3(a16) % 0.57/0.66 [41]P3(a3) % 0.57/0.66 [42]P3(a5) % 0.57/0.66 [46]P4(a1) % 0.57/0.66 [47]P4(a19) % 0.57/0.66 [48]P4(a20) % 0.57/0.66 [49]P4(a4) % 0.57/0.66 [50]P4(a3) % 0.57/0.66 [51]P6(a17) % 0.57/0.66 [52]P6(a11) % 0.57/0.66 [53]P7(a1) % 0.57/0.66 [54]P7(a18) % 0.57/0.66 [55]P7(a4) % 0.57/0.66 [56]P7(a3) % 0.57/0.66 [57]P7(a6) % 0.57/0.66 [58]P7(a12) % 0.57/0.66 [61]P11(a1) % 0.57/0.66 [62]P11(a18) % 0.57/0.66 [63]P11(a19) % 0.57/0.66 [64]P11(a4) % 0.57/0.66 [65]P11(a3) % 0.57/0.66 [66]P11(a7) % 0.57/0.66 [67]P11(a6) % 0.57/0.66 [68]P11(a13) % 0.57/0.66 [69]P11(a12) % 0.57/0.66 [70]P8(a2) % 0.57/0.66 [71]P10(a1) % 0.57/0.66 [72]P10(a3) % 0.57/0.66 [73]P10(a6) % 0.57/0.66 [75]P12(a1) % 0.57/0.66 [76]P12(a13) % 0.57/0.66 [77]P12(a12) % 0.57/0.66 [96]~P4(a2) % 0.57/0.66 [97]~P4(a17) % 0.57/0.66 [98]~P4(a7) % 0.57/0.66 [99]~P4(a9) % 0.57/0.66 [100]~P4(a5) % 0.57/0.66 [102]~P6(f23(a11,a15)) % 0.57/0.66 [89]P13(x891,x891) % 0.57/0.66 [78]P1(f22(x781)) % 0.57/0.66 [79]P2(f22(x791)) % 0.57/0.66 [80]P3(f22(x801)) % 0.57/0.66 [81]P4(f22(x811)) % 0.57/0.66 [82]P4(f8(x821)) % 0.57/0.66 [83]P6(f22(x831)) % 0.57/0.66 [84]P7(f22(x841)) % 0.57/0.66 [85]P11(f22(x851)) % 0.57/0.66 [86]P8(f22(x861)) % 0.57/0.66 [87]P10(f22(x871)) % 0.57/0.66 [88]E(f23(x881,a1),a1) % 0.57/0.66 [90]E(f23(x901,x901),x901) % 0.57/0.66 [91]P5(f14(x911),x911) % 0.57/0.66 [92]P5(f22(x921),f24(x921)) % 0.57/0.66 [93]P5(f8(x931),f24(x931)) % 0.57/0.66 [101]~P4(f24(x1011)) % 0.57/0.66 [94]E(f23(x941,x942),f23(x942,x941)) % 0.57/0.66 [95]P13(f23(x951,x952),x951) % 0.57/0.66 [103]~P4(x1031)+E(x1031,a1) % 0.57/0.66 [104]~P4(x1041)+P1(x1041) % 0.57/0.66 [105]~P1(x1051)+P2(x1051) % 0.57/0.66 [106]~P4(x1061)+P2(x1061) % 0.57/0.66 [107]~P1(x1071)+P3(x1071) % 0.57/0.66 [108]~P4(x1081)+P3(x1081) % 0.57/0.66 [109]~P4(x1091)+P6(x1091) % 0.57/0.66 [110]~P4(x1101)+P7(x1101) % 0.57/0.66 [111]~P4(x1111)+P11(x1111) % 0.57/0.66 [112]P4(x1121)+P6(f10(x1121)) % 0.57/0.66 [118]P4(x1181)+~P4(f21(x1181)) % 0.57/0.66 [119]P4(x1191)+~P4(f10(x1191)) % 0.57/0.66 [122]P4(x1221)+P5(f21(x1221),f24(x1221)) % 0.57/0.66 [123]P4(x1231)+P5(f10(x1231),f24(x1231)) % 0.57/0.66 [121]~P4(x1211)+~P9(x1212,x1211) % 0.57/0.66 [128]~P9(x1281,x1282)+P5(x1281,x1282) % 0.57/0.66 [135]~P9(x1352,x1351)+~P9(x1351,x1352) % 0.57/0.66 [129]~P6(x1292)+P6(f23(x1291,x1292)) % 0.57/0.66 [130]~P6(x1301)+P6(f23(x1301,x1302)) % 0.57/0.66 [132]~P13(x1321,x1322)+P5(x1321,f24(x1322)) % 0.57/0.66 [136]P13(x1361,x1362)+~P5(x1361,f24(x1362)) % 0.57/0.66 [114]~P2(x1141)+~P3(x1141)+P1(x1141) % 0.57/0.66 [117]~P1(x1171)+~P4(x1171)+P8(x1171) % 0.57/0.66 [113]~P4(x1132)+~P4(x1131)+E(x1131,x1132) % 0.57/0.66 [124]~P5(x1241,x1242)+P1(x1241)+~P1(x1242) % 0.57/0.66 [125]~P5(x1251,x1252)+P2(x1251)+~P1(x1252) % 0.57/0.66 [126]~P5(x1261,x1262)+P3(x1261)+~P1(x1262) % 0.57/0.66 [127]~P13(x1271,x1272)+P6(x1271)+~P6(x1272) % 0.57/0.66 [131]~P5(x1312,x1311)+P4(x1311)+P9(x1312,x1311) % 0.57/0.66 [133]P6(x1331)+~P6(x1332)+~P5(x1331,f24(x1332)) % 0.57/0.66 [134]~P11(x1342)+~P11(x1341)+P11(f23(x1341,x1342)) % 0.57/0.66 [137]~P4(x1371)+~P9(x1372,x1373)+~P5(x1373,f24(x1371)) % 0.57/0.66 [138]P5(x1381,x1382)+~P9(x1381,x1383)+~P5(x1383,f24(x1382)) % 0.57/0.66 [120]~P4(x1201)+~P7(x1201)+~P11(x1201)+P10(x1201) % 0.57/0.66 %EqnAxiom % 0.57/0.66 [1]E(x11,x11) % 0.57/0.66 [2]E(x22,x21)+~E(x21,x22) % 0.57/0.66 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.57/0.66 [4]~E(x41,x42)+E(f22(x41),f22(x42)) % 0.57/0.66 [5]~E(x51,x52)+E(f24(x51),f24(x52)) % 0.57/0.66 [6]~E(x61,x62)+E(f10(x61),f10(x62)) % 0.57/0.66 [7]~E(x71,x72)+E(f21(x71),f21(x72)) % 0.57/0.66 [8]~E(x81,x82)+E(f8(x81),f8(x82)) % 0.57/0.66 [9]~E(x91,x92)+E(f23(x91,x93),f23(x92,x93)) % 0.57/0.66 [10]~E(x101,x102)+E(f23(x103,x101),f23(x103,x102)) % 0.57/0.66 [11]~E(x111,x112)+E(f14(x111),f14(x112)) % 0.57/0.66 [12]~P1(x121)+P1(x122)+~E(x121,x122) % 0.57/0.66 [13]P5(x132,x133)+~E(x131,x132)+~P5(x131,x133) % 0.57/0.66 [14]P5(x143,x142)+~E(x141,x142)+~P5(x143,x141) % 0.57/0.66 [15]P9(x152,x153)+~E(x151,x152)+~P9(x151,x153) % 0.57/0.66 [16]P9(x163,x162)+~E(x161,x162)+~P9(x163,x161) % 0.57/0.66 [17]P13(x172,x173)+~E(x171,x172)+~P13(x171,x173) % 0.57/0.66 [18]P13(x183,x182)+~E(x181,x182)+~P13(x183,x181) % 0.57/0.66 [19]~P6(x191)+P6(x192)+~E(x191,x192) % 0.57/0.66 [20]~P2(x201)+P2(x202)+~E(x201,x202) % 0.57/0.66 [21]~P11(x211)+P11(x212)+~E(x211,x212) % 0.57/0.66 [22]~P8(x221)+P8(x222)+~E(x221,x222) % 0.57/0.66 [23]~P4(x231)+P4(x232)+~E(x231,x232) % 0.57/0.66 [24]~P10(x241)+P10(x242)+~E(x241,x242) % 0.57/0.66 [25]~P3(x251)+P3(x252)+~E(x251,x252) % 0.57/0.66 [26]~P12(x261)+P12(x262)+~E(x261,x262) % 0.57/0.66 [27]~P7(x271)+P7(x272)+~E(x271,x272) % 0.57/0.66 % 0.57/0.66 %------------------------------------------- % 0.57/0.66 cnf(139,plain, % 0.57/0.66 ($false), % 0.57/0.66 inference(scs_inference,[],[52,102,130]), % 0.57/0.66 ['proof']). % 0.57/0.66 % SZS output end Proof % 0.57/0.66 % Total time :0.000000s %------------------------------------------------------------------------------