%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SEU321+1 : TPTP v8.2.0. Released v3.3.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n032.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:27 EDT 2024 % Result : Theorem 0.68s 0.84s % Output : CNFRefutation 0.68s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.02/0.09 % Problem : SEU321+1 : TPTP v8.2.0. Released v3.3.0. % 0.02/0.09 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.08/0.28 % Computer : n032.cluster.edu % 0.08/0.28 % Model : x86_64 x86_64 % 0.08/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.28 % Memory : 8042.1875MB % 0.08/0.28 % OS : Linux 3.10.0-693.el7.x86_64 % 0.08/0.28 % CPULimit : 300 % 0.08/0.28 % WCLimit : 300 % 0.08/0.28 % DateTime : Fri Jun 21 16:52:23 EDT 2024 % 0.08/0.28 % CPUTime : % 0.13/0.45 start to proof:theBenchmark % 0.68/0.83 %------------------------------------------- % 0.68/0.83 % File :CSE---1.7 % 0.68/0.83 % Problem :theBenchmark % 0.68/0.83 % Transform :cnf % 0.68/0.83 % Format :tptp:raw % 0.68/0.83 % Command :java -jar mcs_scs.jar %d %s % 0.68/0.83 % 0.68/0.83 % Result :Theorem 0.340000s % 0.68/0.83 % Output :CNFRefutation 0.340000s % 0.68/0.83 %------------------------------------------- % 0.68/0.83 %------------------------------------------------------------------------------ % 0.68/0.83 % File : SEU321+1 : TPTP v8.2.0. Released v3.3.0. % 0.68/0.83 % Domain : Set theory % 0.68/0.83 % Problem : MPTP bushy problem l40_tops_1 % 0.68/0.83 % Version : [Urb07] axioms : Especial. % 0.68/0.83 % English : % 0.68/0.83 % 0.68/0.83 % Refs : [Ban01] Bancerek et al. (2001), On the Characterizations of Co % 0.68/0.83 % : [Urb07] Urban (2006), Email to G. Sutcliffe % 0.68/0.83 % Source : [Urb07] % 0.68/0.83 % Names : bushy-l40_tops_1 [Urb07] % 0.68/0.83 % 0.68/0.83 % Status : Theorem % 0.68/0.83 % Rating : 0.22 v8.2.0, 0.19 v8.1.0, 0.11 v7.5.0, 0.12 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.17 v6.2.0, 0.20 v6.1.0, 0.30 v6.0.0, 0.13 v5.5.0, 0.22 v5.4.0, 0.29 v5.3.0, 0.33 v5.2.0, 0.20 v5.1.0, 0.19 v5.0.0, 0.21 v4.1.0, 0.26 v4.0.0, 0.29 v3.7.0, 0.25 v3.5.0, 0.26 v3.3.0 % 0.68/0.83 % Syntax : Number of formulae : 42 ( 8 unt; 0 def) % 0.68/0.83 % Number of atoms : 133 ( 4 equ) % 0.68/0.83 % Maximal formula atoms : 7 ( 3 avg) % 0.68/0.83 % Number of connectives : 107 ( 16 ~; 1 |; 46 &) % 0.68/0.83 % ( 2 <=>; 42 =>; 0 <=; 0 <~>) % 0.68/0.83 % Maximal formula depth : 9 ( 5 avg) % 0.68/0.83 % Maximal term depth : 3 ( 1 avg) % 0.68/0.83 % Number of predicates : 18 ( 16 usr; 1 prp; 0-2 aty) % 0.68/0.83 % Number of functors : 4 ( 4 usr; 1 con; 0-2 aty) % 0.68/0.83 % Number of variables : 67 ( 62 !; 5 ?) % 0.68/0.83 % SPC : FOF_THM_RFO_SEQ % 0.68/0.83 % 0.68/0.83 % Comments : Translated by MPTP 0.2 from the original problem in the Mizar % 0.68/0.83 % library, www.mizar.org % 0.68/0.83 %------------------------------------------------------------------------------ % 0.68/0.83 fof(reflexivity_r1_tarski,axiom, % 0.68/0.83 ! [A,B] : subset(A,A) ). % 0.68/0.83 % 0.68/0.83 fof(rc5_struct_0,axiom, % 0.68/0.83 ! [A] : % 0.68/0.83 ( ( ~ empty_carrier(A) % 0.68/0.83 & one_sorted_str(A) ) % 0.68/0.83 => ? [B] : % 0.68/0.83 ( element(B,powerset(the_carrier(A))) % 0.68/0.83 & ~ empty(B) ) ) ). % 0.68/0.83 % 0.68/0.83 fof(cc1_membered,axiom, % 0.68/0.84 ! [A] : % 0.68/0.84 ( v5_membered(A) % 0.68/0.84 => v4_membered(A) ) ). % 0.68/0.84 % 0.68/0.84 fof(cc2_membered,axiom, % 0.68/0.84 ! [A] : % 0.68/0.84 ( v4_membered(A) % 0.68/0.84 => v3_membered(A) ) ). % 0.68/0.84 % 0.68/0.84 fof(cc3_membered,axiom, % 0.68/0.84 ! [A] : % 0.68/0.84 ( v3_membered(A) % 0.68/0.84 => v2_membered(A) ) ). % 0.68/0.84 % 0.68/0.84 fof(cc4_membered,axiom, % 0.68/0.84 ! [A] : % 0.68/0.84 ( v2_membered(A) % 0.68/0.84 => v1_membered(A) ) ). % 0.68/0.84 % 0.68/0.84 fof(rc1_membered,axiom, % 0.68/0.84 ? [A] : % 0.68/0.84 ( ~ empty(A) % 0.68/0.84 & v1_membered(A) % 0.68/0.84 & v2_membered(A) % 0.68/0.84 & v3_membered(A) % 0.68/0.84 & v4_membered(A) % 0.68/0.84 & v5_membered(A) ) ). % 0.68/0.84 % 0.68/0.84 fof(cc10_membered,axiom, % 0.68/0.84 ! [A] : % 0.68/0.84 ( v1_membered(A) % 0.68/0.84 => ! [B] : % 0.68/0.84 ( element(B,A) % 0.68/0.84 => v1_xcmplx_0(B) ) ) ). % 0.68/0.84 % 0.68/0.84 fof(cc11_membered,axiom, % 0.68/0.84 ! [A] : % 0.68/0.84 ( v2_membered(A) % 0.68/0.84 => ! [B] : % 0.68/0.84 ( element(B,A) % 0.68/0.84 => ( v1_xcmplx_0(B) % 0.68/0.84 & v1_xreal_0(B) ) ) ) ). % 0.68/0.84 % 0.68/0.84 fof(cc12_membered,axiom, % 0.68/0.84 ! [A] : % 0.68/0.84 ( v3_membered(A) % 0.68/0.84 => ! [B] : % 0.68/0.84 ( element(B,A) % 0.68/0.84 => ( v1_xcmplx_0(B) % 0.68/0.84 & v1_xreal_0(B) % 0.68/0.84 & v1_rat_1(B) ) ) ) ). % 0.68/0.84 % 0.68/0.84 fof(cc13_membered,axiom, % 0.68/0.84 ! [A] : % 0.68/0.84 ( v4_membered(A) % 0.68/0.84 => ! [B] : % 0.68/0.84 ( element(B,A) % 0.68/0.84 => ( v1_xcmplx_0(B) % 0.68/0.84 & v1_xreal_0(B) % 0.68/0.84 & v1_int_1(B) % 0.68/0.84 & v1_rat_1(B) ) ) ) ). % 0.68/0.84 % 0.68/0.84 fof(cc14_membered,axiom, % 0.68/0.84 ! [A] : % 0.68/0.84 ( v5_membered(A) % 0.68/0.84 => ! [B] : % 0.68/0.84 ( element(B,A) % 0.68/0.84 => ( v1_xcmplx_0(B) % 0.68/0.84 & natural(B) % 0.68/0.84 & v1_xreal_0(B) % 0.68/0.84 & v1_int_1(B) % 0.68/0.84 & v1_rat_1(B) ) ) ) ). % 0.68/0.84 % 0.68/0.84 fof(cc15_membered,axiom, % 0.68/0.84 ! [A] : % 0.68/0.84 ( empty(A) % 0.68/0.84 => ( v1_membered(A) % 0.68/0.84 & v2_membered(A) % 0.68/0.84 & v3_membered(A) % 0.68/0.84 & v4_membered(A) % 0.68/0.84 & v5_membered(A) ) ) ). % 0.68/0.84 % 0.68/0.84 fof(cc16_membered,axiom, % 0.68/0.84 ! [A] : % 0.68/0.84 ( v1_membered(A) % 0.68/0.84 => ! [B] : % 0.68/0.84 ( element(B,powerset(A)) % 0.68/0.84 => v1_membered(B) ) ) ). % 0.68/0.84 % 0.68/0.84 fof(cc17_membered,axiom, % 0.68/0.84 ! [A] : % 0.68/0.84 ( v2_membered(A) % 0.68/0.84 => ! [B] : % 0.68/0.84 ( element(B,powerset(A)) % 0.68/0.84 => ( v1_membered(B) % 0.68/0.84 & v2_membered(B) ) ) ) ). % 0.68/0.84 % 0.68/0.84 fof(cc18_membered,axiom, % 0.68/0.84 ! [A] : % 0.68/0.84 ( v3_membered(A) % 0.68/0.84 => ! [B] : % 0.68/0.84 ( element(B,powerset(A)) % 0.68/0.84 => ( v1_membered(B) % 0.68/0.84 & v2_membered(B) % 0.68/0.84 & v3_membered(B) ) ) ) ). % 0.68/0.84 % 0.68/0.84 fof(cc19_membered,axiom, % 0.68/0.84 ! [A] : % 0.68/0.84 ( v4_membered(A) % 0.68/0.84 => ! [B] : % 0.68/0.84 ( element(B,powerset(A)) % 0.68/0.84 => ( v1_membered(B) % 0.68/0.84 & v2_membered(B) % 0.68/0.84 & v3_membered(B) % 0.68/0.84 & v4_membered(B) ) ) ) ). % 0.68/0.84 % 0.68/0.84 fof(cc20_membered,axiom, % 0.68/0.84 ! [A] : % 0.68/0.84 ( v5_membered(A) % 0.68/0.84 => ! [B] : % 0.68/0.84 ( element(B,powerset(A)) % 0.68/0.84 => ( v1_membered(B) % 0.68/0.84 & v2_membered(B) % 0.68/0.84 & v3_membered(B) % 0.68/0.84 & v4_membered(B) % 0.68/0.84 & v5_membered(B) ) ) ) ). % 0.68/0.84 % 0.68/0.84 fof(t2_subset,axiom, % 0.68/0.84 ! [A,B] : % 0.68/0.84 ( element(A,B) % 0.68/0.84 => ( empty(B) % 0.68/0.84 | in(A,B) ) ) ). % 0.68/0.84 % 0.68/0.84 fof(t5_subset,axiom, % 0.68/0.84 ! [A,B,C] : % 0.68/0.84 ~ ( in(A,B) % 0.68/0.84 & element(B,powerset(C)) % 0.68/0.84 & empty(C) ) ). % 0.68/0.84 % 0.68/0.84 fof(t8_boole,axiom, % 0.68/0.84 ! [A,B] : % 0.68/0.84 ~ ( empty(A) % 0.68/0.84 & A != B % 0.68/0.84 & empty(B) ) ). % 0.68/0.84 % 0.68/0.84 fof(involutiveness_k3_subset_1,axiom, % 0.68/0.84 ! [A,B] : % 0.68/0.84 ( element(B,powerset(A)) % 0.68/0.84 => subset_complement(A,subset_complement(A,B)) = B ) ). % 0.68/0.84 % 0.68/0.84 fof(antisymmetry_r2_hidden,axiom, % 0.68/0.84 ! [A,B] : % 0.68/0.84 ( in(A,B) % 0.68/0.84 => ~ in(B,A) ) ). % 0.68/0.84 % 0.68/0.84 fof(existence_l1_struct_0,axiom, % 0.68/0.84 ? [A] : one_sorted_str(A) ). % 0.68/0.84 % 0.68/0.84 fof(existence_m1_subset_1,axiom, % 0.68/0.84 ! [A] : % 0.68/0.84 ? [B] : element(B,A) ). % 0.68/0.84 % 0.68/0.84 fof(dt_k1_xboole_0,axiom, % 0.68/0.84 $true ). % 0.68/0.84 % 0.68/0.84 fof(dt_k1_zfmisc_1,axiom, % 0.68/0.84 $true ). % 0.68/0.84 % 0.68/0.84 fof(dt_k3_subset_1,axiom, % 0.68/0.84 ! [A,B] : % 0.68/0.84 ( element(B,powerset(A)) % 0.68/0.84 => element(subset_complement(A,B),powerset(A)) ) ). % 0.68/0.84 % 0.68/0.84 fof(dt_l1_struct_0,axiom, % 0.68/0.84 $true ). % 0.68/0.84 % 0.68/0.84 fof(dt_m1_subset_1,axiom, % 0.68/0.84 $true ). % 0.68/0.84 % 0.68/0.84 fof(dt_u1_struct_0,axiom, % 0.68/0.84 $true ). % 0.68/0.84 % 0.68/0.84 fof(rc3_struct_0,axiom, % 0.68/0.84 ? [A] : % 0.68/0.84 ( one_sorted_str(A) % 0.68/0.84 & ~ empty_carrier(A) ) ). % 0.68/0.84 % 0.68/0.84 fof(fc1_struct_0,axiom, % 0.68/0.84 ! [A] : % 0.68/0.84 ( ( ~ empty_carrier(A) % 0.68/0.84 & one_sorted_str(A) ) % 0.68/0.84 => ~ empty(the_carrier(A)) ) ). % 0.68/0.84 % 0.68/0.84 fof(fc6_membered,axiom, % 0.68/0.84 ( empty(empty_set) % 0.68/0.84 & v1_membered(empty_set) % 0.68/0.84 & v2_membered(empty_set) % 0.68/0.84 & v3_membered(empty_set) % 0.68/0.84 & v4_membered(empty_set) % 0.68/0.84 & v5_membered(empty_set) ) ). % 0.68/0.84 % 0.68/0.84 fof(t1_subset,axiom, % 0.68/0.84 ! [A,B] : % 0.68/0.84 ( in(A,B) % 0.68/0.84 => element(A,B) ) ). % 0.68/0.84 % 0.68/0.84 fof(t3_subset,axiom, % 0.68/0.84 ! [A,B] : % 0.68/0.84 ( element(A,powerset(B)) % 0.68/0.84 <=> subset(A,B) ) ). % 0.68/0.84 % 0.68/0.84 fof(t4_subset,axiom, % 0.68/0.84 ! [A,B,C] : % 0.68/0.84 ( ( in(A,B) % 0.68/0.84 & element(B,powerset(C)) ) % 0.68/0.84 => element(A,C) ) ). % 0.68/0.84 % 0.68/0.84 fof(t6_boole,axiom, % 0.68/0.84 ! [A] : % 0.68/0.84 ( empty(A) % 0.68/0.84 => A = empty_set ) ). % 0.68/0.84 % 0.68/0.84 fof(t7_boole,axiom, % 0.68/0.84 ! [A,B] : % 0.68/0.84 ~ ( in(A,B) % 0.68/0.84 & empty(B) ) ). % 0.68/0.84 % 0.68/0.84 fof(l40_tops_1,conjecture, % 0.68/0.84 ! [A] : % 0.68/0.84 ( ( ~ empty_carrier(A) % 0.68/0.84 & one_sorted_str(A) ) % 0.68/0.84 => ! [B] : % 0.68/0.84 ( element(B,powerset(the_carrier(A))) % 0.68/0.84 => ! [C] : % 0.68/0.84 ( element(C,the_carrier(A)) % 0.68/0.84 => ( in(C,subset_complement(the_carrier(A),B)) % 0.68/0.84 <=> ~ in(C,B) ) ) ) ) ). % 0.68/0.84 % 0.68/0.84 fof(t50_subset_1,axiom, % 0.68/0.84 ! [A] : % 0.68/0.84 ( A != empty_set % 0.68/0.84 => ! [B] : % 0.68/0.84 ( element(B,powerset(A)) % 0.68/0.84 => ! [C] : % 0.68/0.84 ( element(C,A) % 0.68/0.84 => ( ~ in(C,B) % 0.68/0.84 => in(C,subset_complement(A,B)) ) ) ) ) ). % 0.68/0.84 % 0.68/0.84 fof(t54_subset_1,axiom, % 0.68/0.84 ! [A,B,C] : % 0.68/0.84 ( element(C,powerset(A)) % 0.68/0.84 => ~ ( in(B,subset_complement(A,C)) % 0.68/0.84 & in(B,C) ) ) ). % 0.68/0.84 % 0.68/0.84 %------------------------------------------------------------------------------ % 0.68/0.84 %------------------------------------------- % 0.68/0.84 % Proof found % 0.68/0.84 % SZS status Theorem for theBenchmark % 0.68/0.84 % SZS output start Proof % 0.68/0.85 %ClaNum:107(EqnAxiom:28) % 0.68/0.85 %VarNum:221(SingletonVarNum:105) % 0.68/0.85 %MaxLitNum:5 % 0.68/0.85 %MaxfuncDepth:2 % 0.68/0.85 %SharedTerms:33 % 0.68/0.85 %goalClause: 31 44 46 48 100 104 % 0.68/0.85 %singleGoalClaCount:4 % 0.68/0.85 [29]P1(a1) % 0.68/0.85 [30]P1(a5) % 0.68/0.85 [31]P1(a7) % 0.68/0.85 [32]P2(a2) % 0.68/0.85 [33]P7(a2) % 0.68/0.85 [34]P7(a3) % 0.68/0.85 [35]P8(a2) % 0.68/0.85 [36]P8(a3) % 0.68/0.85 [37]P9(a2) % 0.68/0.85 [38]P9(a3) % 0.68/0.85 [39]P10(a2) % 0.68/0.85 [40]P10(a3) % 0.68/0.85 [41]P11(a2) % 0.68/0.85 [42]P11(a3) % 0.68/0.85 [47]~P4(a5) % 0.68/0.85 [48]~P4(a7) % 0.68/0.85 [49]~P2(a3) % 0.68/0.85 [44]P3(a8,f10(a7)) % 0.68/0.85 [46]P3(a9,f11(f10(a7))) % 0.68/0.85 [43]P12(x431,x431) % 0.68/0.85 [45]P3(f6(x451),x451) % 0.68/0.85 [100]~P5(a8,a9)+P5(a8,f12(f10(a7),a9)) % 0.68/0.85 [104]P5(a8,a9)+~P5(a8,f12(f10(a7),a9)) % 0.68/0.85 [50]~P2(x501)+E(x501,a2) % 0.68/0.85 [51]~P2(x511)+P7(x511) % 0.68/0.85 [52]~P2(x521)+P8(x521) % 0.68/0.85 [53]~P7(x531)+P8(x531) % 0.68/0.85 [54]~P2(x541)+P9(x541) % 0.68/0.85 [55]~P8(x551)+P9(x551) % 0.68/0.85 [56]~P2(x561)+P10(x561) % 0.68/0.85 [57]~P9(x571)+P10(x571) % 0.68/0.85 [58]~P2(x581)+P11(x581) % 0.68/0.85 [59]~P10(x591)+P11(x591) % 0.68/0.85 [63]~P2(x631)+~P5(x632,x631) % 0.68/0.85 [79]~P5(x791,x792)+P3(x791,x792) % 0.68/0.85 [97]~P5(x972,x971)+~P5(x971,x972) % 0.68/0.85 [81]~P12(x811,x812)+P3(x811,f11(x812)) % 0.68/0.85 [98]P12(x981,x982)+~P3(x981,f11(x982)) % 0.68/0.85 [105]~P3(x1052,f11(x1051))+P3(f12(x1051,x1052),f11(x1051)) % 0.68/0.85 [103]~P3(x1032,f11(x1031))+E(f12(x1031,f12(x1031,x1032)),x1032) % 0.68/0.85 [61]~P1(x611)+P4(x611)+~P2(f10(x611)) % 0.68/0.85 [62]~P1(x621)+P4(x621)+~P2(f4(x621)) % 0.68/0.85 [99]~P1(x991)+P4(x991)+P3(f4(x991),f11(f10(x991))) % 0.68/0.85 [60]~P2(x602)+~P2(x601)+E(x601,x602) % 0.68/0.85 [64]~P3(x641,x642)+P14(x641)+~P11(x642) % 0.68/0.85 [65]~P3(x651,x652)+P14(x651)+~P7(x652) % 0.68/0.85 [66]~P3(x661,x662)+P14(x661)+~P8(x662) % 0.68/0.85 [67]~P3(x671,x672)+P14(x671)+~P9(x672) % 0.68/0.85 [68]~P3(x681,x682)+P14(x681)+~P10(x682) % 0.68/0.85 [69]~P3(x691,x692)+P16(x691)+~P7(x692) % 0.68/0.85 [70]~P3(x701,x702)+P16(x701)+~P8(x702) % 0.68/0.85 [71]~P3(x711,x712)+P16(x711)+~P9(x712) % 0.68/0.85 [72]~P3(x721,x722)+P16(x721)+~P10(x722) % 0.68/0.85 [73]~P3(x731,x732)+P15(x731)+~P7(x732) % 0.68/0.85 [74]~P3(x741,x742)+P15(x741)+~P8(x742) % 0.68/0.85 [75]~P3(x751,x752)+P15(x751)+~P9(x752) % 0.68/0.85 [76]~P3(x761,x762)+P13(x761)+~P7(x762) % 0.68/0.85 [77]~P3(x771,x772)+P13(x771)+~P8(x772) % 0.68/0.85 [78]~P3(x781,x782)+P6(x781)+~P7(x782) % 0.68/0.85 [80]~P3(x802,x801)+P2(x801)+P5(x802,x801) % 0.68/0.85 [82]P7(x821)+~P7(x822)+~P3(x821,f11(x822)) % 0.68/0.85 [83]P8(x831)+~P7(x832)+~P3(x831,f11(x832)) % 0.68/0.85 [84]P8(x841)+~P8(x842)+~P3(x841,f11(x842)) % 0.68/0.85 [85]P9(x851)+~P7(x852)+~P3(x851,f11(x852)) % 0.68/0.85 [86]P9(x861)+~P8(x862)+~P3(x861,f11(x862)) % 0.68/0.85 [87]P9(x871)+~P9(x872)+~P3(x871,f11(x872)) % 0.68/0.85 [88]P10(x881)+~P7(x882)+~P3(x881,f11(x882)) % 0.68/0.85 [89]P10(x891)+~P8(x892)+~P3(x891,f11(x892)) % 0.68/0.85 [90]P10(x901)+~P9(x902)+~P3(x901,f11(x902)) % 0.68/0.85 [91]P10(x911)+~P10(x912)+~P3(x911,f11(x912)) % 0.68/0.85 [92]P11(x921)+~P11(x922)+~P3(x921,f11(x922)) % 0.68/0.85 [93]P11(x931)+~P7(x932)+~P3(x931,f11(x932)) % 0.68/0.85 [94]P11(x941)+~P8(x942)+~P3(x941,f11(x942)) % 0.68/0.85 [95]P11(x951)+~P9(x952)+~P3(x951,f11(x952)) % 0.68/0.85 [96]P11(x961)+~P10(x962)+~P3(x961,f11(x962)) % 0.68/0.85 [101]~P2(x1011)+~P5(x1012,x1013)+~P3(x1013,f11(x1011)) % 0.68/0.85 [102]P3(x1021,x1022)+~P5(x1021,x1023)+~P3(x1023,f11(x1022)) % 0.68/0.85 [107]~P5(x1071,x1072)+~P5(x1071,f12(x1073,x1072))+~P3(x1072,f11(x1073)) % 0.68/0.85 [106]~P3(x1062,x1061)+P5(x1062,x1063)+P5(x1062,f12(x1061,x1063))+~P3(x1063,f11(x1061))+E(x1061,a2) % 0.68/0.85 %EqnAxiom % 0.68/0.85 [1]E(x11,x11) % 0.68/0.85 [2]E(x22,x21)+~E(x21,x22) % 0.68/0.85 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.68/0.85 [4]~E(x41,x42)+E(f10(x41),f10(x42)) % 0.68/0.85 [5]~E(x51,x52)+E(f6(x51),f6(x52)) % 0.68/0.85 [6]~E(x61,x62)+E(f12(x61,x63),f12(x62,x63)) % 0.68/0.85 [7]~E(x71,x72)+E(f12(x73,x71),f12(x73,x72)) % 0.68/0.85 [8]~E(x81,x82)+E(f11(x81),f11(x82)) % 0.68/0.85 [9]~E(x91,x92)+E(f4(x91),f4(x92)) % 0.68/0.85 [10]~P1(x101)+P1(x102)+~E(x101,x102) % 0.68/0.85 [11]P5(x112,x113)+~E(x111,x112)+~P5(x111,x113) % 0.68/0.85 [12]P5(x123,x122)+~E(x121,x122)+~P5(x123,x121) % 0.68/0.85 [13]P3(x132,x133)+~E(x131,x132)+~P3(x131,x133) % 0.68/0.85 [14]P3(x143,x142)+~E(x141,x142)+~P3(x143,x141) % 0.68/0.85 [15]~P2(x151)+P2(x152)+~E(x151,x152) % 0.68/0.85 [16]~P7(x161)+P7(x162)+~E(x161,x162) % 0.68/0.85 [17]~P10(x171)+P10(x172)+~E(x171,x172) % 0.68/0.85 [18]~P8(x181)+P8(x182)+~E(x181,x182) % 0.68/0.85 [19]~P16(x191)+P16(x192)+~E(x191,x192) % 0.68/0.85 [20]~P9(x201)+P9(x202)+~E(x201,x202) % 0.68/0.85 [21]~P11(x211)+P11(x212)+~E(x211,x212) % 0.68/0.85 [22]~P15(x221)+P15(x222)+~E(x221,x222) % 0.68/0.85 [23]~P14(x231)+P14(x232)+~E(x231,x232) % 0.68/0.85 [24]P12(x242,x243)+~E(x241,x242)+~P12(x241,x243) % 0.68/0.85 [25]P12(x253,x252)+~E(x251,x252)+~P12(x253,x251) % 0.68/0.85 [26]~P13(x261)+P13(x262)+~E(x261,x262) % 0.68/0.85 [27]~P4(x271)+P4(x272)+~E(x271,x272) % 0.68/0.85 [28]~P6(x281)+P6(x282)+~E(x281,x282) % 0.68/0.85 % 0.68/0.85 %------------------------------------------- % 0.68/0.85 cnf(110,plain, % 0.68/0.85 (P12(a9,f10(a7))), % 0.68/0.85 inference(scs_inference,[],[46,32,63,98])). % 0.68/0.85 cnf(112,plain, % 0.68/0.85 (P5(f6(a3),a3)), % 0.68/0.85 inference(scs_inference,[],[46,45,32,49,63,98,80])). % 0.68/0.85 cnf(113,plain, % 0.68/0.85 (P3(f6(x1131),x1131)), % 0.68/0.85 inference(rename_variables,[],[45])). % 0.68/0.85 cnf(116,plain, % 0.68/0.85 (P3(f6(x1161),x1161)), % 0.68/0.85 inference(rename_variables,[],[45])). % 0.68/0.85 cnf(119,plain, % 0.68/0.85 (P3(f6(x1191),x1191)), % 0.68/0.85 inference(rename_variables,[],[45])). % 0.68/0.85 cnf(122,plain, % 0.68/0.85 (P3(f6(x1221),x1221)), % 0.68/0.85 inference(rename_variables,[],[45])). % 0.68/0.85 cnf(125,plain, % 0.68/0.85 (P3(f6(x1251),x1251)), % 0.68/0.85 inference(rename_variables,[],[45])). % 0.68/0.85 cnf(128,plain, % 0.68/0.85 (P3(f6(x1281),x1281)), % 0.68/0.85 inference(rename_variables,[],[45])). % 0.68/0.85 cnf(130,plain, % 0.68/0.85 (~P5(x1301,f6(f11(a2)))), % 0.68/0.85 inference(scs_inference,[],[46,45,113,116,119,122,125,128,32,33,41,49,63,98,80,82,83,85,88,92,101])). % 0.68/0.85 cnf(133,plain, % 0.68/0.85 (~E(a3,a2)), % 0.68/0.85 inference(scs_inference,[],[46,45,113,116,119,122,125,128,32,33,41,49,63,98,80,82,83,85,88,92,101,12])). % 0.68/0.85 cnf(148,plain, % 0.68/0.85 (P12(f6(f11(x1481)),x1481)), % 0.68/0.85 inference(scs_inference,[],[45,98])). % 0.68/0.85 cnf(155,plain, % 0.68/0.85 (~P5(x1551,a9)+~P5(x1551,f12(f10(a7),a9))), % 0.68/0.85 inference(scs_inference,[],[46,130,112,45,98,12,102,107])). % 0.68/0.85 cnf(165,plain, % 0.68/0.85 (P12(f6(f11(x1651)),x1652)+~E(x1651,x1652)), % 0.68/0.85 inference(scs_inference,[],[148,25])). % 0.68/0.85 cnf(185,plain, % 0.68/0.85 (~P2(f10(a7))+~P5(x1851,a9)), % 0.68/0.85 inference(scs_inference,[],[46,148,110,82,83,85,25,24,101])). % 0.68/0.85 cnf(202,plain, % 0.68/0.85 (P12(x2021,x2022)+~E(x2021,x2022)), % 0.68/0.85 inference(scs_inference,[],[46,43,88,25])). % 0.68/0.85 cnf(203,plain, % 0.68/0.85 (P12(x2031,x2032)+~E(x2032,x2031)), % 0.68/0.85 inference(scs_inference,[],[46,43,88,25,24])). % 0.68/0.85 cnf(210,plain, % 0.68/0.85 (P3(f6(x2101),x2102)+~E(x2101,x2102)), % 0.68/0.85 inference(scs_inference,[],[45,14])). % 0.68/0.85 cnf(271,plain, % 0.68/0.85 (~E(a2,f10(a7))+~P5(x2711,a9)), % 0.68/0.85 inference(scs_inference,[],[32,185,15])). % 0.68/0.85 cnf(298,plain, % 0.68/0.85 (~E(f10(a7),a2)+~P5(x2981,a9)), % 0.68/0.85 inference(scs_inference,[],[271,2])). % 0.68/0.85 cnf(300,plain, % 0.68/0.85 (~E(x3001,a2)+~E(f10(a7),x3001)+~P5(x3002,a9)), % 0.68/0.85 inference(scs_inference,[],[298,3])). % 0.68/0.85 cnf(320,plain, % 0.68/0.85 (~P5(a8,a9)), % 0.68/0.85 inference(scs_inference,[],[155,100])). % 0.68/0.85 cnf(321,plain, % 0.68/0.85 (~P5(a8,f12(f10(a7),a9))), % 0.68/0.85 inference(scs_inference,[],[320,104])). % 0.68/0.85 cnf(326,plain, % 0.68/0.85 (E(a2,f10(a7))), % 0.68/0.85 inference(scs_inference,[],[46,44,321,320,106,210,2])). % 0.68/0.85 cnf(333,plain, % 0.68/0.85 (P2(f10(a7))), % 0.68/0.85 inference(scs_inference,[],[46,44,321,133,320,32,106,210,2,165,202,203,300,3,15])). % 0.68/0.85 cnf(369,plain, % 0.68/0.85 ($false), % 0.68/0.85 inference(scs_inference,[],[48,31,333,326,210,61]), % 0.68/0.85 ['proof']). % 0.68/0.85 % SZS output end Proof % 0.68/0.85 % Total time :0.340000s %------------------------------------------------------------------------------