%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SEU341+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 : n026.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:32 EDT 2024 % Result : Theorem 0.53s 0.70s % Output : CNFRefutation 0.53s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.02/0.11 % Problem : SEU341+1 : TPTP v8.2.0. Released v3.3.0. % 0.02/0.11 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.10/0.31 % Computer : n026.cluster.edu % 0.10/0.31 % Model : x86_64 x86_64 % 0.10/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.31 % Memory : 8042.1875MB % 0.10/0.31 % OS : Linux 3.10.0-693.el7.x86_64 % 0.10/0.31 % CPULimit : 300 % 0.10/0.31 % WCLimit : 300 % 0.10/0.31 % DateTime : Fri Jun 21 13:27:24 EDT 2024 % 0.10/0.32 % CPUTime : % 0.52/0.57 start to proof:theBenchmark % 0.53/0.68 %------------------------------------------- % 0.53/0.68 % File :CSE---1.7 % 0.53/0.68 % Problem :theBenchmark % 0.53/0.68 % Transform :cnf % 0.53/0.68 % Format :tptp:raw % 0.53/0.68 % Command :java -jar mcs_scs.jar %d %s % 0.53/0.68 % 0.53/0.68 % Result :Theorem 0.060000s % 0.53/0.68 % Output :CNFRefutation 0.060000s % 0.53/0.68 %------------------------------------------- % 0.53/0.69 %------------------------------------------------------------------------------ % 0.53/0.69 % File : SEU341+1 : TPTP v8.2.0. Released v3.3.0. % 0.53/0.69 % Domain : Set theory % 0.53/0.69 % Problem : MPTP bushy problem t5_connsp_2 % 0.53/0.69 % Version : [Urb07] axioms : Especial. % 0.53/0.69 % English : % 0.53/0.69 % 0.53/0.69 % Refs : [Ban01] Bancerek et al. (2001), On the Characterizations of Co % 0.53/0.69 % : [Urb07] Urban (2006), Email to G. Sutcliffe % 0.53/0.69 % Source : [Urb07] % 0.53/0.69 % Names : bushy-t5_connsp_2 [Urb07] % 0.53/0.69 % 0.53/0.69 % Status : Theorem % 0.53/0.69 % Rating : 0.14 v8.1.0, 0.08 v7.5.0, 0.09 v7.4.0, 0.10 v7.2.0, 0.07 v7.1.0, 0.09 v7.0.0, 0.07 v6.4.0, 0.12 v6.3.0, 0.17 v6.2.0, 0.16 v6.1.0, 0.20 v6.0.0, 0.13 v5.5.0, 0.15 v5.4.0, 0.21 v5.3.0, 0.22 v5.2.0, 0.10 v5.1.0, 0.14 v5.0.0, 0.17 v4.1.0, 0.22 v4.0.0, 0.25 v3.7.0, 0.15 v3.5.0, 0.16 v3.3.0 % 0.53/0.69 % Syntax : Number of formulae : 45 ( 10 unt; 0 def) % 0.53/0.69 % Number of atoms : 153 ( 4 equ) % 0.53/0.69 % Maximal formula atoms : 9 ( 3 avg) % 0.53/0.69 % Number of connectives : 121 ( 13 ~; 1 |; 56 &) % 0.53/0.69 % ( 2 <=>; 49 =>; 0 <=; 0 <~>) % 0.53/0.69 % Maximal formula depth : 11 ( 5 avg) % 0.53/0.69 % Maximal term depth : 3 ( 1 avg) % 0.53/0.69 % Number of predicates : 22 ( 20 usr; 1 prp; 0-3 aty) % 0.53/0.69 % Number of functors : 4 ( 4 usr; 1 con; 0-2 aty) % 0.53/0.69 % Number of variables : 75 ( 68 !; 7 ?) % 0.53/0.69 % SPC : FOF_THM_RFO_SEQ % 0.53/0.69 % 0.53/0.69 % Comments : Translated by MPTP 0.2 from the original problem in the Mizar % 0.53/0.69 % library, www.mizar.org % 0.53/0.69 %------------------------------------------------------------------------------ % 0.53/0.69 fof(antisymmetry_r2_hidden,axiom, % 0.53/0.69 ! [A,B] : % 0.53/0.69 ( in(A,B) % 0.53/0.69 => ~ in(B,A) ) ). % 0.53/0.69 % 0.53/0.69 fof(cc10_membered,axiom, % 0.53/0.69 ! [A] : % 0.53/0.69 ( v1_membered(A) % 0.53/0.69 => ! [B] : % 0.53/0.69 ( element(B,A) % 0.53/0.69 => v1_xcmplx_0(B) ) ) ). % 0.53/0.69 % 0.53/0.69 fof(cc11_membered,axiom, % 0.53/0.69 ! [A] : % 0.53/0.69 ( v2_membered(A) % 0.53/0.69 => ! [B] : % 0.53/0.69 ( element(B,A) % 0.53/0.69 => ( v1_xcmplx_0(B) % 0.53/0.69 & v1_xreal_0(B) ) ) ) ). % 0.53/0.69 % 0.53/0.69 fof(cc12_membered,axiom, % 0.53/0.69 ! [A] : % 0.53/0.69 ( v3_membered(A) % 0.53/0.69 => ! [B] : % 0.53/0.69 ( element(B,A) % 0.53/0.69 => ( v1_xcmplx_0(B) % 0.53/0.69 & v1_xreal_0(B) % 0.53/0.69 & v1_rat_1(B) ) ) ) ). % 0.53/0.69 % 0.53/0.69 fof(cc13_membered,axiom, % 0.53/0.69 ! [A] : % 0.53/0.69 ( v4_membered(A) % 0.53/0.69 => ! [B] : % 0.53/0.69 ( element(B,A) % 0.53/0.69 => ( v1_xcmplx_0(B) % 0.53/0.69 & v1_xreal_0(B) % 0.53/0.69 & v1_int_1(B) % 0.53/0.69 & v1_rat_1(B) ) ) ) ). % 0.53/0.69 % 0.53/0.69 fof(cc14_membered,axiom, % 0.53/0.69 ! [A] : % 0.53/0.69 ( v5_membered(A) % 0.53/0.69 => ! [B] : % 0.53/0.69 ( element(B,A) % 0.53/0.69 => ( v1_xcmplx_0(B) % 0.53/0.69 & natural(B) % 0.53/0.69 & v1_xreal_0(B) % 0.53/0.69 & v1_int_1(B) % 0.53/0.69 & v1_rat_1(B) ) ) ) ). % 0.53/0.69 % 0.53/0.69 fof(cc15_membered,axiom, % 0.53/0.69 ! [A] : % 0.53/0.69 ( empty(A) % 0.53/0.69 => ( v1_membered(A) % 0.53/0.69 & v2_membered(A) % 0.53/0.69 & v3_membered(A) % 0.53/0.69 & v4_membered(A) % 0.53/0.69 & v5_membered(A) ) ) ). % 0.53/0.69 % 0.53/0.69 fof(cc16_membered,axiom, % 0.53/0.69 ! [A] : % 0.53/0.69 ( v1_membered(A) % 0.53/0.69 => ! [B] : % 0.53/0.69 ( element(B,powerset(A)) % 0.53/0.69 => v1_membered(B) ) ) ). % 0.53/0.69 % 0.53/0.69 fof(cc17_membered,axiom, % 0.53/0.69 ! [A] : % 0.53/0.69 ( v2_membered(A) % 0.53/0.69 => ! [B] : % 0.53/0.69 ( element(B,powerset(A)) % 0.53/0.69 => ( v1_membered(B) % 0.53/0.69 & v2_membered(B) ) ) ) ). % 0.53/0.69 % 0.53/0.69 fof(cc18_membered,axiom, % 0.53/0.69 ! [A] : % 0.53/0.69 ( v3_membered(A) % 0.53/0.69 => ! [B] : % 0.53/0.69 ( element(B,powerset(A)) % 0.53/0.69 => ( v1_membered(B) % 0.53/0.69 & v2_membered(B) % 0.53/0.69 & v3_membered(B) ) ) ) ). % 0.53/0.69 % 0.53/0.69 fof(cc19_membered,axiom, % 0.53/0.69 ! [A] : % 0.53/0.69 ( v4_membered(A) % 0.53/0.69 => ! [B] : % 0.53/0.69 ( element(B,powerset(A)) % 0.53/0.69 => ( v1_membered(B) % 0.53/0.69 & v2_membered(B) % 0.53/0.69 & v3_membered(B) % 0.53/0.69 & v4_membered(B) ) ) ) ). % 0.53/0.69 % 0.53/0.69 fof(cc1_membered,axiom, % 0.53/0.69 ! [A] : % 0.53/0.69 ( v5_membered(A) % 0.53/0.69 => v4_membered(A) ) ). % 0.53/0.69 % 0.53/0.69 fof(cc20_membered,axiom, % 0.53/0.69 ! [A] : % 0.53/0.69 ( v5_membered(A) % 0.53/0.69 => ! [B] : % 0.53/0.69 ( element(B,powerset(A)) % 0.53/0.69 => ( v1_membered(B) % 0.53/0.69 & v2_membered(B) % 0.53/0.69 & v3_membered(B) % 0.53/0.69 & v4_membered(B) % 0.53/0.69 & v5_membered(B) ) ) ) ). % 0.53/0.69 % 0.53/0.69 fof(cc2_membered,axiom, % 0.53/0.69 ! [A] : % 0.53/0.69 ( v4_membered(A) % 0.53/0.69 => v3_membered(A) ) ). % 0.53/0.69 % 0.53/0.69 fof(cc3_membered,axiom, % 0.53/0.69 ! [A] : % 0.53/0.69 ( v3_membered(A) % 0.53/0.69 => v2_membered(A) ) ). % 0.53/0.69 % 0.53/0.69 fof(cc4_membered,axiom, % 0.53/0.69 ! [A] : % 0.53/0.69 ( v2_membered(A) % 0.53/0.69 => v1_membered(A) ) ). % 0.53/0.69 % 0.53/0.69 fof(d1_connsp_2,axiom, % 0.53/0.69 ! [A] : % 0.53/0.69 ( ( ~ empty_carrier(A) % 0.53/0.69 & topological_space(A) % 0.53/0.69 & top_str(A) ) % 0.53/0.69 => ! [B] : % 0.53/0.69 ( element(B,the_carrier(A)) % 0.53/0.69 => ! [C] : % 0.53/0.69 ( element(C,powerset(the_carrier(A))) % 0.53/0.69 => ( point_neighbourhood(C,A,B) % 0.53/0.69 <=> in(B,interior(A,C)) ) ) ) ) ). % 0.53/0.69 % 0.53/0.69 fof(dt_k1_tops_1,axiom, % 0.53/0.69 ! [A,B] : % 0.53/0.69 ( ( top_str(A) % 0.53/0.69 & element(B,powerset(the_carrier(A))) ) % 0.53/0.69 => element(interior(A,B),powerset(the_carrier(A))) ) ). % 0.53/0.69 % 0.53/0.69 fof(dt_k1_xboole_0,axiom, % 0.53/0.69 $true ). % 0.53/0.69 % 0.53/0.69 fof(dt_k1_zfmisc_1,axiom, % 0.53/0.69 $true ). % 0.53/0.69 % 0.53/0.69 fof(dt_l1_pre_topc,axiom, % 0.53/0.69 ! [A] : % 0.53/0.69 ( top_str(A) % 0.53/0.69 => one_sorted_str(A) ) ). % 0.53/0.69 % 0.53/0.69 fof(dt_l1_struct_0,axiom, % 0.53/0.69 $true ). % 0.53/0.69 % 0.53/0.69 fof(dt_m1_connsp_2,axiom, % 0.53/0.69 ! [A,B] : % 0.53/0.69 ( ( ~ empty_carrier(A) % 0.53/0.69 & topological_space(A) % 0.53/0.69 & top_str(A) % 0.53/0.69 & element(B,the_carrier(A)) ) % 0.53/0.69 => ! [C] : % 0.53/0.69 ( point_neighbourhood(C,A,B) % 0.53/0.70 => element(C,powerset(the_carrier(A))) ) ) ). % 0.53/0.70 % 0.53/0.70 fof(dt_m1_subset_1,axiom, % 0.53/0.70 $true ). % 0.53/0.70 % 0.53/0.70 fof(dt_u1_struct_0,axiom, % 0.53/0.70 $true ). % 0.53/0.70 % 0.53/0.70 fof(existence_l1_pre_topc,axiom, % 0.53/0.70 ? [A] : top_str(A) ). % 0.53/0.70 % 0.53/0.70 fof(existence_l1_struct_0,axiom, % 0.53/0.70 ? [A] : one_sorted_str(A) ). % 0.53/0.70 % 0.53/0.70 fof(existence_m1_connsp_2,axiom, % 0.53/0.70 ! [A,B] : % 0.53/0.70 ( ( ~ empty_carrier(A) % 0.53/0.70 & topological_space(A) % 0.53/0.70 & top_str(A) % 0.53/0.70 & element(B,the_carrier(A)) ) % 0.53/0.70 => ? [C] : point_neighbourhood(C,A,B) ) ). % 0.53/0.70 % 0.53/0.70 fof(existence_m1_subset_1,axiom, % 0.53/0.70 ! [A] : % 0.53/0.70 ? [B] : element(B,A) ). % 0.53/0.70 % 0.53/0.70 fof(fc1_subset_1,axiom, % 0.53/0.70 ! [A] : ~ empty(powerset(A)) ). % 0.53/0.70 % 0.53/0.70 fof(fc6_membered,axiom, % 0.53/0.70 ( empty(empty_set) % 0.53/0.70 & v1_membered(empty_set) % 0.53/0.70 & v2_membered(empty_set) % 0.53/0.70 & v3_membered(empty_set) % 0.53/0.70 & v4_membered(empty_set) % 0.53/0.70 & v5_membered(empty_set) ) ). % 0.53/0.70 % 0.53/0.70 fof(rc1_membered,axiom, % 0.53/0.70 ? [A] : % 0.53/0.70 ( ~ empty(A) % 0.53/0.70 & v1_membered(A) % 0.53/0.70 & v2_membered(A) % 0.53/0.70 & v3_membered(A) % 0.53/0.70 & v4_membered(A) % 0.53/0.70 & v5_membered(A) ) ). % 0.53/0.70 % 0.53/0.70 fof(rc1_subset_1,axiom, % 0.53/0.70 ! [A] : % 0.53/0.70 ( ~ empty(A) % 0.53/0.70 => ? [B] : % 0.53/0.70 ( element(B,powerset(A)) % 0.53/0.70 & ~ empty(B) ) ) ). % 0.53/0.70 % 0.53/0.70 fof(rc2_subset_1,axiom, % 0.53/0.70 ! [A] : % 0.53/0.70 ? [B] : % 0.53/0.70 ( element(B,powerset(A)) % 0.53/0.70 & empty(B) ) ). % 0.53/0.70 % 0.53/0.70 fof(reflexivity_r1_tarski,axiom, % 0.53/0.70 ! [A,B] : subset(A,A) ). % 0.53/0.70 % 0.53/0.70 fof(t1_subset,axiom, % 0.53/0.70 ! [A,B] : % 0.53/0.70 ( in(A,B) % 0.53/0.70 => element(A,B) ) ). % 0.53/0.70 % 0.53/0.70 fof(t2_subset,axiom, % 0.53/0.70 ! [A,B] : % 0.53/0.70 ( element(A,B) % 0.53/0.70 => ( empty(B) % 0.53/0.70 | in(A,B) ) ) ). % 0.53/0.70 % 0.53/0.70 fof(t3_subset,axiom, % 0.53/0.70 ! [A,B] : % 0.53/0.70 ( element(A,powerset(B)) % 0.53/0.70 <=> subset(A,B) ) ). % 0.53/0.70 % 0.53/0.70 fof(t4_subset,axiom, % 0.53/0.70 ! [A,B,C] : % 0.53/0.70 ( ( in(A,B) % 0.53/0.70 & element(B,powerset(C)) ) % 0.53/0.70 => element(A,C) ) ). % 0.53/0.70 % 0.53/0.70 fof(t55_tops_1,axiom, % 0.53/0.70 ! [A] : % 0.53/0.70 ( ( topological_space(A) % 0.53/0.70 & top_str(A) ) % 0.53/0.70 => ! [B] : % 0.53/0.70 ( top_str(B) % 0.53/0.70 => ! [C] : % 0.53/0.70 ( element(C,powerset(the_carrier(A))) % 0.53/0.70 => ! [D] : % 0.53/0.70 ( element(D,powerset(the_carrier(B))) % 0.53/0.70 => ( ( open_subset(D,B) % 0.53/0.70 => interior(B,D) = D ) % 0.53/0.70 & ( interior(A,C) = C % 0.53/0.70 => open_subset(C,A) ) ) ) ) ) ) ). % 0.53/0.70 % 0.53/0.70 fof(t5_connsp_2,conjecture, % 0.53/0.70 ! [A] : % 0.53/0.70 ( ( ~ empty_carrier(A) % 0.53/0.70 & topological_space(A) % 0.53/0.70 & top_str(A) ) % 0.53/0.70 => ! [B] : % 0.53/0.70 ( element(B,powerset(the_carrier(A))) % 0.53/0.70 => ! [C] : % 0.53/0.70 ( element(C,the_carrier(A)) % 0.53/0.70 => ( ( open_subset(B,A) % 0.53/0.70 & in(C,B) ) % 0.53/0.70 => point_neighbourhood(B,A,C) ) ) ) ) ). % 0.53/0.70 % 0.53/0.70 fof(t5_subset,axiom, % 0.53/0.70 ! [A,B,C] : % 0.53/0.70 ~ ( in(A,B) % 0.53/0.70 & element(B,powerset(C)) % 0.53/0.70 & empty(C) ) ). % 0.53/0.70 % 0.53/0.70 fof(t6_boole,axiom, % 0.53/0.70 ! [A] : % 0.53/0.70 ( empty(A) % 0.53/0.70 => A = empty_set ) ). % 0.53/0.70 % 0.53/0.70 fof(t7_boole,axiom, % 0.53/0.70 ! [A,B] : % 0.53/0.70 ~ ( in(A,B) % 0.53/0.70 & empty(B) ) ). % 0.53/0.70 % 0.53/0.70 fof(t8_boole,axiom, % 0.53/0.70 ! [A,B] : % 0.53/0.70 ~ ( empty(A) % 0.53/0.70 & A != B % 0.53/0.70 & empty(B) ) ). % 0.53/0.70 % 0.53/0.70 %------------------------------------------------------------------------------ % 0.53/0.70 %------------------------------------------- % 0.53/0.70 % Proof found % 0.53/0.70 % SZS status Theorem for theBenchmark % 0.53/0.70 % SZS output start Proof % 0.53/0.70 %ClaNum:124(EqnAxiom:38) % 0.53/0.70 %VarNum:269(SingletonVarNum:119) % 0.53/0.70 %MaxLitNum:7 % 0.53/0.70 %MaxfuncDepth:2 % 0.53/0.70 %SharedTerms:31 % 0.53/0.70 %goalClause: 50 52 55 56 58 60 63 65 % 0.53/0.70 %singleGoalClaCount:8 % 0.53/0.70 [39]P1(a1) % 0.53/0.70 [40]P1(a2) % 0.53/0.70 [41]P14(a1) % 0.53/0.70 [42]P14(a2) % 0.53/0.70 [43]P18(a1) % 0.53/0.70 [44]P18(a2) % 0.53/0.70 [45]P19(a1) % 0.53/0.70 [46]P19(a2) % 0.53/0.70 [47]P20(a1) % 0.53/0.70 [48]P20(a2) % 0.53/0.70 [49]P2(a1) % 0.53/0.70 [50]P4(a8) % 0.53/0.70 [51]P5(a3) % 0.53/0.70 [52]P5(a8) % 0.53/0.70 [53]P6(a5) % 0.53/0.70 [55]P7(a4,a11) % 0.53/0.70 [56]P10(a11,a8) % 0.53/0.70 [62]~P2(a2) % 0.53/0.70 [63]~P8(a8) % 0.53/0.70 [65]~P12(a11,a8,a4) % 0.53/0.70 [58]P3(a4,f12(a8)) % 0.53/0.70 [60]P3(a11,f13(f12(a8))) % 0.53/0.70 [57]P11(x571,x571) % 0.53/0.70 [54]P2(f9(x541)) % 0.53/0.70 [59]P3(f6(x591),x591) % 0.53/0.70 [61]P3(f9(x611),f13(x611)) % 0.53/0.70 [64]~P2(f13(x641)) % 0.53/0.70 [66]~P2(x661)+E(x661,a1) % 0.53/0.70 [67]~P14(x671)+P1(x671) % 0.53/0.70 [68]~P2(x681)+P1(x681) % 0.53/0.70 [69]~P18(x691)+P14(x691) % 0.53/0.70 [70]~P2(x701)+P14(x701) % 0.53/0.70 [71]~P19(x711)+P18(x711) % 0.53/0.70 [72]~P2(x721)+P18(x721) % 0.53/0.70 [73]~P20(x731)+P19(x731) % 0.53/0.70 [74]~P2(x741)+P19(x741) % 0.53/0.70 [75]~P2(x751)+P20(x751) % 0.53/0.70 [76]~P5(x761)+P6(x761) % 0.53/0.70 [78]P2(x781)+~P2(f10(x781)) % 0.53/0.70 [80]P2(x801)+P3(f10(x801),f13(x801)) % 0.53/0.70 [79]~P2(x791)+~P7(x792,x791) % 0.53/0.70 [96]~P7(x961,x962)+P3(x961,x962) % 0.53/0.70 [114]~P7(x1142,x1141)+~P7(x1141,x1142) % 0.53/0.70 [98]~P11(x981,x982)+P3(x981,f13(x982)) % 0.53/0.70 [115]P11(x1151,x1152)+~P3(x1151,f13(x1152)) % 0.53/0.70 [77]~P2(x772)+~P2(x771)+E(x771,x772) % 0.53/0.70 [81]~P3(x811,x812)+P15(x811)+~P1(x812) % 0.53/0.70 [82]~P3(x821,x822)+P15(x821)+~P14(x822) % 0.53/0.70 [83]~P3(x831,x832)+P15(x831)+~P18(x832) % 0.53/0.70 [84]~P3(x841,x842)+P15(x841)+~P19(x842) % 0.53/0.70 [85]~P3(x851,x852)+P15(x851)+~P20(x852) % 0.53/0.70 [86]~P3(x861,x862)+P17(x861)+~P14(x862) % 0.53/0.70 [87]~P3(x871,x872)+P17(x871)+~P18(x872) % 0.53/0.70 [88]~P3(x881,x882)+P17(x881)+~P19(x882) % 0.53/0.70 [89]~P3(x891,x892)+P17(x891)+~P20(x892) % 0.53/0.70 [90]~P3(x901,x902)+P16(x901)+~P18(x902) % 0.53/0.70 [91]~P3(x911,x912)+P16(x911)+~P19(x912) % 0.53/0.70 [92]~P3(x921,x922)+P16(x921)+~P20(x922) % 0.53/0.70 [93]~P3(x931,x932)+P13(x931)+~P19(x932) % 0.53/0.70 [94]~P3(x941,x942)+P13(x941)+~P20(x942) % 0.53/0.70 [95]~P3(x951,x952)+P9(x951)+~P20(x952) % 0.53/0.70 [97]~P3(x972,x971)+P2(x971)+P7(x972,x971) % 0.53/0.70 [99]P1(x991)+~P1(x992)+~P3(x991,f13(x992)) % 0.53/0.70 [100]P1(x1001)+~P14(x1002)+~P3(x1001,f13(x1002)) % 0.53/0.70 [101]P1(x1011)+~P18(x1012)+~P3(x1011,f13(x1012)) % 0.53/0.70 [102]P1(x1021)+~P19(x1022)+~P3(x1021,f13(x1022)) % 0.53/0.70 [103]P1(x1031)+~P20(x1032)+~P3(x1031,f13(x1032)) % 0.53/0.70 [104]P14(x1041)+~P14(x1042)+~P3(x1041,f13(x1042)) % 0.53/0.70 [105]P14(x1051)+~P18(x1052)+~P3(x1051,f13(x1052)) % 0.53/0.70 [106]P14(x1061)+~P19(x1062)+~P3(x1061,f13(x1062)) % 0.53/0.70 [107]P14(x1071)+~P20(x1072)+~P3(x1071,f13(x1072)) % 0.53/0.70 [108]P18(x1081)+~P18(x1082)+~P3(x1081,f13(x1082)) % 0.53/0.70 [109]P18(x1091)+~P19(x1092)+~P3(x1091,f13(x1092)) % 0.53/0.70 [110]P18(x1101)+~P20(x1102)+~P3(x1101,f13(x1102)) % 0.53/0.70 [111]P19(x1111)+~P19(x1112)+~P3(x1111,f13(x1112)) % 0.53/0.70 [112]P19(x1121)+~P20(x1122)+~P3(x1121,f13(x1122)) % 0.53/0.70 [113]P20(x1131)+~P20(x1132)+~P3(x1131,f13(x1132)) % 0.53/0.70 [118]~P5(x1181)+~P3(x1182,f13(f12(x1181)))+P3(f14(x1181,x1182),f13(f12(x1181))) % 0.53/0.70 [116]~P2(x1161)+~P7(x1162,x1163)+~P3(x1163,f13(x1161)) % 0.53/0.70 [117]P3(x1171,x1172)+~P7(x1171,x1173)+~P3(x1173,f13(x1172)) % 0.53/0.70 [119]~P4(x1191)+~P5(x1191)+P8(x1191)+P12(f7(x1191,x1192),x1191,x1192)+~P3(x1192,f12(x1191)) % 0.53/0.70 [122]~P4(x1221)+~P5(x1221)+P8(x1221)+~P12(x1222,x1221,x1223)+~P3(x1223,f12(x1221))+P3(x1222,f13(f12(x1221))) % 0.53/0.70 [123]~P4(x1231)+~P5(x1231)+P8(x1231)+P12(x1232,x1231,x1233)+~P3(x1233,f12(x1231))+~P7(x1233,f14(x1231,x1232))+~P3(x1232,f13(f12(x1231))) % 0.53/0.70 [124]~P4(x1241)+~P5(x1241)+~P12(x1243,x1241,x1242)+P8(x1241)+~P3(x1242,f12(x1241))+P7(x1242,f14(x1241,x1243))+~P3(x1243,f13(f12(x1241))) % 0.53/0.70 [120]~P5(x1203)+~P5(x1201)+~P10(x1202,x1201)+~P4(x1203)+E(f14(x1201,x1202),x1202)+~P3(x1202,f13(f12(x1201)))+~P3(x1204,f13(f12(x1203))) % 0.53/0.70 [121]~P4(x1212)+~P5(x1212)+P10(x1211,x1212)+~P5(x1213)+~E(f14(x1212,x1211),x1211)+~P3(x1211,f13(f12(x1212)))+~P3(x1214,f13(f12(x1213))) % 0.53/0.70 %EqnAxiom % 0.53/0.70 [1]E(x11,x11) % 0.53/0.70 [2]E(x22,x21)+~E(x21,x22) % 0.53/0.70 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.53/0.70 [4]~E(x41,x42)+E(f9(x41),f9(x42)) % 0.53/0.70 [5]~E(x51,x52)+E(f12(x51),f12(x52)) % 0.53/0.70 [6]~E(x61,x62)+E(f6(x61),f6(x62)) % 0.53/0.70 [7]~E(x71,x72)+E(f14(x71,x73),f14(x72,x73)) % 0.53/0.70 [8]~E(x81,x82)+E(f14(x83,x81),f14(x83,x82)) % 0.53/0.70 [9]~E(x91,x92)+E(f13(x91),f13(x92)) % 0.53/0.70 [10]~E(x101,x102)+E(f7(x101,x103),f7(x102,x103)) % 0.53/0.70 [11]~E(x111,x112)+E(f7(x113,x111),f7(x113,x112)) % 0.53/0.70 [12]~E(x121,x122)+E(f10(x121),f10(x122)) % 0.53/0.70 [13]~P1(x131)+P1(x132)+~E(x131,x132) % 0.53/0.70 [14]P3(x142,x143)+~E(x141,x142)+~P3(x141,x143) % 0.53/0.70 [15]P3(x153,x152)+~E(x151,x152)+~P3(x153,x151) % 0.53/0.70 [16]~P14(x161)+P14(x162)+~E(x161,x162) % 0.53/0.70 [17]~P18(x171)+P18(x172)+~E(x171,x172) % 0.53/0.70 [18]~P19(x181)+P19(x182)+~E(x181,x182) % 0.53/0.70 [19]P7(x192,x193)+~E(x191,x192)+~P7(x191,x193) % 0.53/0.70 [20]P7(x203,x202)+~E(x201,x202)+~P7(x203,x201) % 0.53/0.70 [21]~P20(x211)+P20(x212)+~E(x211,x212) % 0.53/0.70 [22]~P8(x221)+P8(x222)+~E(x221,x222) % 0.53/0.70 [23]~P16(x231)+P16(x232)+~E(x231,x232) % 0.53/0.70 [24]~P5(x241)+P5(x242)+~E(x241,x242) % 0.53/0.70 [25]~P2(x251)+P2(x252)+~E(x251,x252) % 0.53/0.70 [26]~P4(x261)+P4(x262)+~E(x261,x262) % 0.53/0.70 [27]~P17(x271)+P17(x272)+~E(x271,x272) % 0.53/0.70 [28]~P15(x281)+P15(x282)+~E(x281,x282) % 0.53/0.70 [29]~P6(x291)+P6(x292)+~E(x291,x292) % 0.53/0.70 [30]~P13(x301)+P13(x302)+~E(x301,x302) % 0.53/0.70 [31]P11(x312,x313)+~E(x311,x312)+~P11(x311,x313) % 0.53/0.70 [32]P11(x323,x322)+~E(x321,x322)+~P11(x323,x321) % 0.53/0.70 [33]P10(x332,x333)+~E(x331,x332)+~P10(x331,x333) % 0.53/0.70 [34]P10(x343,x342)+~E(x341,x342)+~P10(x343,x341) % 0.53/0.70 [35]P12(x352,x353,x354)+~E(x351,x352)+~P12(x351,x353,x354) % 0.53/0.70 [36]P12(x363,x362,x364)+~E(x361,x362)+~P12(x363,x361,x364) % 0.53/0.70 [37]P12(x373,x374,x372)+~E(x371,x372)+~P12(x373,x374,x371) % 0.53/0.70 [38]~P9(x381)+P9(x382)+~E(x381,x382) % 0.53/0.70 % 0.53/0.70 %------------------------------------------- % 0.53/0.70 cnf(125,plain, % 0.53/0.70 (~P7(x1251,a1)), % 0.53/0.70 inference(scs_inference,[],[49,79])). % 0.53/0.70 cnf(131,plain, % 0.53/0.70 (P7(f6(a2),a2)), % 0.53/0.70 inference(scs_inference,[],[55,60,59,49,62,79,114,115,97])). % 0.53/0.70 cnf(132,plain, % 0.53/0.70 (P3(f6(x1321),x1321)), % 0.53/0.70 inference(rename_variables,[],[59])). % 0.53/0.70 cnf(135,plain, % 0.53/0.70 (P3(f6(x1351),x1351)), % 0.53/0.70 inference(rename_variables,[],[59])). % 0.53/0.70 cnf(138,plain, % 0.53/0.70 (P3(f9(x1381),f13(x1381))), % 0.53/0.70 inference(rename_variables,[],[61])). % 0.53/0.70 cnf(141,plain, % 0.53/0.70 (P3(f6(x1411),x1411)), % 0.53/0.70 inference(rename_variables,[],[59])). % 0.53/0.70 cnf(143,plain, % 0.53/0.70 (P14(f9(a1))), % 0.53/0.70 inference(scs_inference,[],[55,60,59,132,135,61,138,39,41,43,49,62,79,114,115,97,99,100,104,105])). % 0.53/0.70 cnf(144,plain, % 0.53/0.70 (P3(f9(x1441),f13(x1441))), % 0.53/0.70 inference(rename_variables,[],[61])). % 0.53/0.70 cnf(147,plain, % 0.53/0.70 (P3(f6(x1471),x1471)), % 0.53/0.70 inference(rename_variables,[],[59])). % 0.53/0.70 cnf(150,plain, % 0.53/0.70 (P3(f9(x1501),f13(x1501))), % 0.53/0.70 inference(rename_variables,[],[61])). % 0.53/0.70 cnf(153,plain, % 0.53/0.70 (P3(f6(x1531),x1531)), % 0.53/0.70 inference(rename_variables,[],[59])). % 0.53/0.70 cnf(159,plain, % 0.53/0.70 (P3(f6(x1591),x1591)), % 0.53/0.70 inference(rename_variables,[],[59])). % 0.53/0.70 cnf(161,plain, % 0.53/0.70 (~P2(f12(a8))), % 0.53/0.70 inference(scs_inference,[],[55,60,59,132,135,141,147,153,61,138,144,150,39,41,43,45,47,49,62,79,114,115,97,99,100,104,105,108,109,111,112,113,116])). % 0.53/0.70 cnf(164,plain, % 0.53/0.70 (~P2(a11)), % 0.53/0.70 inference(scs_inference,[],[55,60,59,132,135,141,147,153,61,138,144,150,39,41,43,45,47,49,62,79,114,115,97,99,100,104,105,108,109,111,112,113,116,20,77])). % 0.53/0.70 cnf(168,plain, % 0.53/0.70 (E(f14(a8,a11),a11)), % 0.53/0.70 inference(scs_inference,[],[50,52,55,56,63,58,60,59,132,135,141,147,153,61,138,144,150,39,41,43,45,47,49,62,79,114,115,97,99,100,104,105,108,109,111,112,113,116,20,77,119,120])). % 0.53/0.70 cnf(170,plain, % 0.53/0.70 (~P7(a4,f14(a8,a11))), % 0.53/0.70 inference(scs_inference,[],[50,52,55,56,63,65,58,60,59,132,135,141,147,153,61,138,144,150,39,41,43,45,47,49,62,79,114,115,97,99,100,104,105,108,109,111,112,113,116,20,77,119,120,123])). % 0.53/0.70 cnf(172,plain, % 0.53/0.70 (E(a11,f14(a8,a11))), % 0.53/0.70 inference(scs_inference,[],[50,52,55,56,63,65,58,60,59,132,135,141,147,153,61,138,144,150,39,41,43,45,47,49,62,79,114,115,97,99,100,104,105,108,109,111,112,113,116,20,77,119,120,123,2])). % 0.53/0.70 cnf(175,plain, % 0.53/0.70 (P3(f14(a8,a11),f13(f12(a8)))), % 0.53/0.70 inference(scs_inference,[],[50,52,55,56,63,65,58,60,59,132,135,141,147,153,61,138,144,150,39,41,43,45,47,49,62,79,114,115,97,99,100,104,105,108,109,111,112,113,116,20,77,119,120,123,2,101,14])). % 0.53/0.70 cnf(176,plain, % 0.53/0.70 (P3(f6(f14(a8,a11)),a11)), % 0.53/0.70 inference(scs_inference,[],[50,52,55,56,63,65,58,60,59,132,135,141,147,153,159,61,138,144,150,39,41,43,45,47,49,62,79,114,115,97,99,100,104,105,108,109,111,112,113,116,20,77,119,120,123,2,101,14,15])). % 0.53/0.70 cnf(178,plain, % 0.53/0.70 (P10(f14(a8,a11),a8)), % 0.53/0.70 inference(scs_inference,[],[50,52,55,56,63,65,58,60,59,132,135,141,147,153,159,61,138,144,150,39,41,43,45,47,49,62,79,114,115,97,99,100,104,105,108,109,111,112,113,116,20,77,119,120,123,2,101,14,15,33])). % 0.53/0.70 cnf(193,plain, % 0.53/0.70 (~P7(x1931,f9(x1932))), % 0.53/0.70 inference(scs_inference,[],[175,131,54,114,115,79])). % 0.53/0.70 cnf(195,plain, % 0.53/0.70 (P7(a4,f12(a8))), % 0.53/0.70 inference(scs_inference,[],[58,175,161,131,54,114,115,79,97])). % 0.53/0.70 cnf(198,plain, % 0.53/0.70 (P11(x1981,x1981)), % 0.53/0.70 inference(rename_variables,[],[57])). % 0.53/0.70 cnf(199,plain, % 0.53/0.70 (~P2(f14(a8,a11))), % 0.53/0.70 inference(scs_inference,[],[58,175,161,131,168,164,54,57,114,115,79,97,32,25])). % 0.53/0.70 cnf(204,plain, % 0.53/0.70 (E(f14(a8,f14(a8,a11)),f14(a8,a11))), % 0.53/0.70 inference(scs_inference,[],[50,58,52,175,125,161,178,131,168,164,54,57,198,114,115,79,97,32,25,31,20,120])). % 0.53/0.70 cnf(224,plain, % 0.53/0.70 (~E(f12(a8),f14(a8,a11))), % 0.53/0.70 inference(scs_inference,[],[58,170,195,59,199,115,114,97,15])). % 0.53/0.70 cnf(242,plain, % 0.53/0.70 (P7(f14(a8,a11),f13(f12(a8)))), % 0.53/0.70 inference(scs_inference,[],[60,172,61,64,115,97,19])). % 0.53/0.70 cnf(247,plain, % 0.53/0.70 (~P7(f13(f12(a8)),a11)), % 0.53/0.70 inference(scs_inference,[],[60,168,204,224,193,195,172,61,64,115,97,19,3,32,20,114])). % 0.53/0.70 cnf(256,plain, % 0.53/0.70 (P3(f9(x2561),f13(x2561))), % 0.53/0.71 inference(rename_variables,[],[61])). % 0.53/0.71 cnf(266,plain, % 0.53/0.71 ($false), % 0.53/0.71 inference(scs_inference,[],[55,176,242,143,247,170,224,172,61,256,164,114,100,97,104,19,14,3,20]), % 0.53/0.71 ['proof']). % 0.53/0.71 % SZS output end Proof % 0.53/0.71 % Total time :0.060000s %------------------------------------------------------------------------------