%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SEU386+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 : n025.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:46 EDT 2024 % Result : Theorem 13.60s 13.67s % Output : CNFRefutation 13.60s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.13 % Problem : SEU386+1 : TPTP v8.2.0. Released v3.3.0. % 0.04/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.13/0.34 % Computer : n025.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Fri Jun 21 13:08:09 EDT 2024 % 0.13/0.34 % CPUTime : % 0.51/0.57 start to proof:theBenchmark % 13.52/13.65 %------------------------------------------- % 13.52/13.65 % File :CSE---1.7 % 13.52/13.65 % Problem :theBenchmark % 13.52/13.65 % Transform :cnf % 13.52/13.65 % Format :tptp:raw % 13.52/13.65 % Command :java -jar mcs_scs.jar %d %s % 13.52/13.65 % 13.52/13.65 % Result :Theorem 13.020000s % 13.52/13.65 % Output :CNFRefutation 13.020000s % 13.52/13.65 %------------------------------------------- % 13.60/13.65 %------------------------------------------------------------------------------ % 13.60/13.65 % File : SEU386+1 : TPTP v8.2.0. Released v3.3.0. % 13.60/13.65 % Domain : Set theory % 13.60/13.65 % Problem : MPTP bushy problem t29_waybel_9 % 13.60/13.65 % Version : [Urb07] axioms : Especial. % 13.60/13.65 % English : % 13.60/13.65 % 13.60/13.65 % Refs : [Ban01] Bancerek et al. (2001), On the Characterizations of Co % 13.60/13.65 % : [Urb07] Urban (2006), Email to G. Sutcliffe % 13.60/13.65 % Source : [Urb07] % 13.60/13.65 % Names : bushy-t29_waybel_9 [Urb07] % 13.60/13.65 % 13.60/13.65 % Status : Theorem % 13.60/13.65 % Rating : 0.22 v8.2.0, 0.19 v8.1.0, 0.17 v7.5.0, 0.19 v7.4.0, 0.20 v7.3.0, 0.21 v7.2.0, 0.17 v7.0.0, 0.20 v6.4.0, 0.27 v6.3.0, 0.17 v6.2.0, 0.24 v6.1.0, 0.33 v6.0.0, 0.22 v5.5.0, 0.26 v5.4.0, 0.36 v5.3.0, 0.44 v5.2.0, 0.30 v5.1.0, 0.29 v5.0.0, 0.42 v4.1.0, 0.39 v4.0.0, 0.42 v3.7.0, 0.35 v3.5.0, 0.37 v3.3.0 % 13.60/13.65 % Syntax : Number of formulae : 45 ( 13 unt; 0 def) % 13.60/13.65 % Number of atoms : 139 ( 3 equ) % 13.60/13.65 % Maximal formula atoms : 13 ( 3 avg) % 13.60/13.66 % Number of connectives : 123 ( 29 ~; 1 |; 49 &) % 13.60/13.66 % ( 4 <=>; 40 =>; 0 <=; 0 <~>) % 13.60/13.66 % Maximal formula depth : 13 ( 5 avg) % 13.60/13.66 % Maximal term depth : 3 ( 1 avg) % 13.60/13.66 % Number of predicates : 23 ( 21 usr; 1 prp; 0-3 aty) % 13.60/13.66 % Number of functors : 4 ( 4 usr; 1 con; 0-2 aty) % 13.60/13.66 % Number of variables : 73 ( 60 !; 13 ?) % 13.60/13.66 % SPC : FOF_THM_RFO_SEQ % 13.60/13.66 % 13.60/13.66 % Comments : Translated by MPTP 0.2 from the original problem in the Mizar % 13.60/13.66 % library, www.mizar.org % 13.60/13.66 %------------------------------------------------------------------------------ % 13.60/13.66 fof(antisymmetry_r2_hidden,axiom, % 13.60/13.66 ! [A,B] : % 13.60/13.66 ( in(A,B) % 13.60/13.66 => ~ in(B,A) ) ). % 13.60/13.66 % 13.60/13.66 fof(cc1_finset_1,axiom, % 13.60/13.66 ! [A] : % 13.60/13.66 ( empty(A) % 13.60/13.66 => finite(A) ) ). % 13.60/13.66 % 13.60/13.66 fof(cc1_finsub_1,axiom, % 13.60/13.66 ! [A] : % 13.60/13.66 ( preboolean(A) % 13.60/13.66 => ( cup_closed(A) % 13.60/13.66 & diff_closed(A) ) ) ). % 13.60/13.66 % 13.60/13.66 fof(cc1_funct_1,axiom, % 13.60/13.66 ! [A] : % 13.60/13.66 ( empty(A) % 13.60/13.66 => function(A) ) ). % 13.60/13.66 % 13.60/13.66 fof(cc2_finset_1,axiom, % 13.60/13.66 ! [A] : % 13.60/13.66 ( finite(A) % 13.60/13.66 => ! [B] : % 13.60/13.66 ( element(B,powerset(A)) % 13.60/13.66 => finite(B) ) ) ). % 13.60/13.66 % 13.60/13.66 fof(cc2_finsub_1,axiom, % 13.60/13.66 ! [A] : % 13.60/13.66 ( ( cup_closed(A) % 13.60/13.66 & diff_closed(A) ) % 13.60/13.66 => preboolean(A) ) ). % 13.60/13.66 % 13.60/13.66 fof(d18_yellow_6,axiom, % 13.60/13.66 ! [A] : % 13.60/13.66 ( ( ~ empty_carrier(A) % 13.60/13.66 & topological_space(A) % 13.60/13.66 & top_str(A) ) % 13.60/13.66 => ! [B] : % 13.60/13.66 ( ( ~ empty_carrier(B) % 13.60/13.66 & transitive_relstr(B) % 13.60/13.66 & directed_relstr(B) % 13.60/13.66 & net_str(B,A) ) % 13.60/13.66 => ! [C] : % 13.60/13.66 ( element(C,powerset(the_carrier(A))) % 13.60/13.66 => ( C = lim_points_of_net(A,B) % 13.60/13.66 <=> ! [D] : % 13.60/13.66 ( element(D,the_carrier(A)) % 13.60/13.66 => ( in(D,C) % 13.60/13.66 <=> ! [E] : % 13.60/13.66 ( point_neighbourhood(E,A,D) % 13.60/13.66 => is_eventually_in(A,B,E) ) ) ) ) ) ) ) ). % 13.60/13.66 % 13.60/13.66 fof(d9_waybel_9,axiom, % 13.60/13.66 ! [A] : % 13.60/13.66 ( ( ~ empty_carrier(A) % 13.60/13.66 & topological_space(A) % 13.60/13.66 & top_str(A) ) % 13.60/13.66 => ! [B] : % 13.60/13.66 ( ( ~ empty_carrier(B) % 13.60/13.66 & net_str(B,A) ) % 13.60/13.66 => ! [C] : % 13.60/13.66 ( element(C,the_carrier(A)) % 13.60/13.66 => ( is_a_cluster_point_of_netstr(A,B,C) % 13.60/13.66 <=> ! [D] : % 13.60/13.66 ( point_neighbourhood(D,A,C) % 13.60/13.66 => is_often_in(A,B,D) ) ) ) ) ) ). % 13.60/13.66 % 13.60/13.66 fof(dt_k11_yellow_6,axiom, % 13.60/13.66 ! [A,B] : % 13.60/13.66 ( ( ~ empty_carrier(A) % 13.60/13.66 & topological_space(A) % 13.60/13.66 & top_str(A) % 13.60/13.66 & ~ empty_carrier(B) % 13.60/13.66 & transitive_relstr(B) % 13.60/13.66 & directed_relstr(B) % 13.60/13.66 & net_str(B,A) ) % 13.60/13.66 => element(lim_points_of_net(A,B),powerset(the_carrier(A))) ) ). % 13.60/13.66 % 13.60/13.66 fof(dt_k1_xboole_0,axiom, % 13.60/13.66 $true ). % 13.60/13.66 % 13.60/13.66 fof(dt_k1_zfmisc_1,axiom, % 13.60/13.66 $true ). % 13.60/13.66 % 13.60/13.66 fof(dt_l1_orders_2,axiom, % 13.60/13.66 ! [A] : % 13.60/13.66 ( rel_str(A) % 13.60/13.66 => one_sorted_str(A) ) ). % 13.60/13.66 % 13.60/13.66 fof(dt_l1_pre_topc,axiom, % 13.60/13.66 ! [A] : % 13.60/13.66 ( top_str(A) % 13.60/13.66 => one_sorted_str(A) ) ). % 13.60/13.66 % 13.60/13.66 fof(dt_l1_struct_0,axiom, % 13.60/13.66 $true ). % 13.60/13.66 % 13.60/13.66 fof(dt_l1_waybel_0,axiom, % 13.60/13.66 ! [A] : % 13.60/13.66 ( one_sorted_str(A) % 13.60/13.66 => ! [B] : % 13.60/13.66 ( net_str(B,A) % 13.60/13.66 => rel_str(B) ) ) ). % 13.60/13.66 % 13.60/13.66 fof(dt_m1_connsp_2,axiom, % 13.60/13.66 ! [A,B] : % 13.60/13.66 ( ( ~ empty_carrier(A) % 13.60/13.66 & topological_space(A) % 13.60/13.66 & top_str(A) % 13.60/13.66 & element(B,the_carrier(A)) ) % 13.60/13.66 => ! [C] : % 13.60/13.66 ( point_neighbourhood(C,A,B) % 13.60/13.66 => element(C,powerset(the_carrier(A))) ) ) ). % 13.60/13.66 % 13.60/13.66 fof(dt_m1_subset_1,axiom, % 13.60/13.66 $true ). % 13.60/13.66 % 13.60/13.66 fof(dt_u1_struct_0,axiom, % 13.60/13.66 $true ). % 13.60/13.66 % 13.60/13.66 fof(existence_l1_orders_2,axiom, % 13.60/13.66 ? [A] : rel_str(A) ). % 13.60/13.66 % 13.60/13.66 fof(existence_l1_pre_topc,axiom, % 13.60/13.66 ? [A] : top_str(A) ). % 13.60/13.66 % 13.60/13.66 fof(existence_l1_struct_0,axiom, % 13.60/13.66 ? [A] : one_sorted_str(A) ). % 13.60/13.66 % 13.60/13.66 fof(existence_l1_waybel_0,axiom, % 13.60/13.66 ! [A] : % 13.60/13.66 ( one_sorted_str(A) % 13.60/13.66 => ? [B] : net_str(B,A) ) ). % 13.60/13.66 % 13.60/13.66 fof(existence_m1_connsp_2,axiom, % 13.60/13.66 ! [A,B] : % 13.60/13.66 ( ( ~ empty_carrier(A) % 13.60/13.66 & topological_space(A) % 13.60/13.66 & top_str(A) % 13.60/13.66 & element(B,the_carrier(A)) ) % 13.60/13.66 => ? [C] : point_neighbourhood(C,A,B) ) ). % 13.60/13.66 % 13.60/13.66 fof(existence_m1_subset_1,axiom, % 13.60/13.66 ! [A] : % 13.60/13.66 ? [B] : element(B,A) ). % 13.60/13.66 % 13.60/13.66 fof(fc1_finsub_1,axiom, % 13.60/13.66 ! [A] : % 13.60/13.66 ( ~ empty(powerset(A)) % 13.60/13.66 & cup_closed(powerset(A)) % 13.60/13.66 & diff_closed(powerset(A)) % 13.60/13.66 & preboolean(powerset(A)) ) ). % 13.60/13.66 % 13.60/13.66 fof(fc1_struct_0,axiom, % 13.60/13.66 ! [A] : % 13.60/13.66 ( ( ~ empty_carrier(A) % 13.60/13.66 & one_sorted_str(A) ) % 13.60/13.66 => ~ empty(the_carrier(A)) ) ). % 13.60/13.66 % 13.60/13.66 fof(fc1_xboole_0,axiom, % 13.60/13.66 empty(empty_set) ). % 13.60/13.66 % 13.60/13.66 fof(rc1_finset_1,axiom, % 13.60/13.66 ? [A] : % 13.60/13.66 ( ~ empty(A) % 13.60/13.66 & finite(A) ) ). % 13.60/13.66 % 13.60/13.66 fof(rc1_xboole_0,axiom, % 13.60/13.66 ? [A] : empty(A) ). % 13.60/13.66 % 13.60/13.66 fof(rc2_xboole_0,axiom, % 13.60/13.66 ? [A] : ~ empty(A) ). % 13.60/13.66 % 13.60/13.66 fof(rc3_finset_1,axiom, % 13.60/13.66 ! [A] : % 13.60/13.66 ( ~ empty(A) % 13.60/13.66 => ? [B] : % 13.60/13.66 ( element(B,powerset(A)) % 13.60/13.66 & ~ empty(B) % 13.60/13.66 & finite(B) ) ) ). % 13.60/13.66 % 13.60/13.66 fof(rc3_struct_0,axiom, % 13.60/13.66 ? [A] : % 13.60/13.66 ( one_sorted_str(A) % 13.60/13.66 & ~ empty_carrier(A) ) ). % 13.60/13.66 % 13.60/13.66 fof(rc4_finset_1,axiom, % 13.60/13.66 ! [A] : % 13.60/13.66 ( ~ empty(A) % 13.60/13.66 => ? [B] : % 13.60/13.66 ( element(B,powerset(A)) % 13.60/13.66 & ~ empty(B) % 13.60/13.66 & finite(B) ) ) ). % 13.60/13.66 % 13.60/13.66 fof(rc5_struct_0,axiom, % 13.60/13.66 ! [A] : % 13.60/13.66 ( ( ~ empty_carrier(A) % 13.60/13.66 & one_sorted_str(A) ) % 13.60/13.66 => ? [B] : % 13.60/13.66 ( element(B,powerset(the_carrier(A))) % 13.60/13.66 & ~ empty(B) ) ) ). % 13.60/13.66 % 13.60/13.66 fof(reflexivity_r1_tarski,axiom, % 13.60/13.66 ! [A,B] : subset(A,A) ). % 13.60/13.66 % 13.60/13.66 fof(t1_subset,axiom, % 13.60/13.66 ! [A,B] : % 13.60/13.66 ( in(A,B) % 13.60/13.66 => element(A,B) ) ). % 13.60/13.66 % 13.60/13.66 fof(t28_yellow_6,axiom, % 13.60/13.66 ! [A] : % 13.60/13.66 ( ( ~ empty_carrier(A) % 13.60/13.66 & one_sorted_str(A) ) % 13.60/13.66 => ! [B] : % 13.60/13.66 ( ( ~ empty_carrier(B) % 13.60/13.66 & transitive_relstr(B) % 13.60/13.66 & directed_relstr(B) % 13.60/13.66 & net_str(B,A) ) % 13.60/13.66 => ! [C] : % 13.60/13.67 ( is_eventually_in(A,B,C) % 13.60/13.67 => is_often_in(A,B,C) ) ) ) ). % 13.60/13.67 % 13.60/13.67 fof(t29_waybel_9,conjecture, % 13.60/13.67 ! [A] : % 13.60/13.67 ( ( ~ empty_carrier(A) % 13.60/13.67 & topological_space(A) % 13.60/13.67 & top_str(A) ) % 13.60/13.67 => ! [B] : % 13.60/13.67 ( ( ~ empty_carrier(B) % 13.60/13.67 & transitive_relstr(B) % 13.60/13.67 & directed_relstr(B) % 13.60/13.67 & net_str(B,A) ) % 13.60/13.67 => ! [C] : % 13.60/13.67 ( element(C,the_carrier(A)) % 13.60/13.67 => ( in(C,lim_points_of_net(A,B)) % 13.60/13.67 => is_a_cluster_point_of_netstr(A,B,C) ) ) ) ) ). % 13.60/13.67 % 13.60/13.67 fof(t2_subset,axiom, % 13.60/13.67 ! [A,B] : % 13.60/13.67 ( element(A,B) % 13.60/13.67 => ( empty(B) % 13.60/13.67 | in(A,B) ) ) ). % 13.60/13.67 % 13.60/13.67 fof(t3_subset,axiom, % 13.60/13.67 ! [A,B] : % 13.60/13.67 ( element(A,powerset(B)) % 13.60/13.67 <=> subset(A,B) ) ). % 13.60/13.67 % 13.60/13.67 fof(t4_subset,axiom, % 13.60/13.67 ! [A,B,C] : % 13.60/13.67 ( ( in(A,B) % 13.60/13.67 & element(B,powerset(C)) ) % 13.60/13.67 => element(A,C) ) ). % 13.60/13.67 % 13.60/13.67 fof(t5_subset,axiom, % 13.60/13.67 ! [A,B,C] : % 13.60/13.67 ~ ( in(A,B) % 13.60/13.67 & element(B,powerset(C)) % 13.60/13.67 & empty(C) ) ). % 13.60/13.67 % 13.60/13.67 fof(t6_boole,axiom, % 13.60/13.67 ! [A] : % 13.60/13.67 ( empty(A) % 13.60/13.67 => A = empty_set ) ). % 13.60/13.67 % 13.60/13.67 fof(t7_boole,axiom, % 13.60/13.67 ! [A,B] : % 13.60/13.67 ~ ( in(A,B) % 13.60/13.67 & empty(B) ) ). % 13.60/13.67 % 13.60/13.67 fof(t8_boole,axiom, % 13.60/13.67 ! [A,B] : % 13.60/13.67 ~ ( empty(A) % 13.60/13.67 & A != B % 13.60/13.67 & empty(B) ) ). % 13.60/13.67 % 13.60/13.67 %------------------------------------------------------------------------------ % 13.60/13.67 %------------------------------------------- % 13.60/13.67 % Proof found % 13.60/13.67 % SZS status Theorem for theBenchmark % 13.60/13.67 % SZS output start Proof % 13.60/13.67 %ClaNum:129(EqnAxiom:60) % 13.60/13.67 %VarNum:348(SingletonVarNum:94) % 13.60/13.67 %MaxLitNum:13 % 13.60/13.67 %MaxfuncDepth:2 % 13.60/13.67 %SharedTerms:33 % 13.60/13.67 %goalClause: 64 66 67 68 75 77 79 83 84 86 % 13.60/13.67 %singleGoalClaCount:10 % 13.60/13.67 [61]P1(a1) % 13.60/13.67 [62]P1(a2) % 13.60/13.67 [63]P6(a3) % 13.60/13.67 [64]P8(a5) % 13.60/13.67 [65]P9(a11) % 13.60/13.67 [66]P9(a5) % 13.60/13.67 [67]P21(a12) % 13.60/13.67 [68]P2(a12) % 13.60/13.67 [69]P10(a13) % 13.60/13.67 [70]P11(a19) % 13.60/13.67 [71]P11(a6) % 13.60/13.67 [75]P12(a12,a5) % 13.60/13.67 [80]~P1(a3) % 13.60/13.67 [81]~P1(a7) % 13.60/13.67 [82]~P7(a6) % 13.60/13.67 [83]~P7(a5) % 13.60/13.67 [84]~P7(a12) % 13.60/13.67 [86]~P15(a5,a12,a14) % 13.60/13.67 [77]P5(a14,f24(a5)) % 13.60/13.67 [79]P13(a14,f21(a5,a12)) % 13.60/13.67 [76]P20(x761,x761) % 13.60/13.67 [72]P18(f20(x721)) % 13.60/13.67 [73]P3(f20(x731)) % 13.60/13.67 [74]P4(f20(x741)) % 13.60/13.67 [78]P5(f4(x781),x781) % 13.60/13.67 [85]~P1(f20(x851)) % 13.60/13.67 [87]~P1(x871)+E(x871,a1) % 13.60/13.67 [88]~P1(x881)+P6(x881) % 13.60/13.67 [89]~P18(x891)+P3(x891) % 13.60/13.67 [90]~P18(x901)+P4(x901) % 13.60/13.67 [91]~P1(x911)+P14(x911) % 13.60/13.67 [92]~P9(x921)+P11(x921) % 13.60/13.67 [93]~P10(x931)+P11(x931) % 13.60/13.67 [94]P1(x941)+P6(f8(x941)) % 13.60/13.67 [95]P1(x951)+P6(f9(x951)) % 13.60/13.67 [98]P1(x981)+~P1(f8(x981)) % 13.60/13.67 [99]P1(x991)+~P1(f9(x991)) % 13.60/13.67 [100]~P11(x1001)+P12(f22(x1001),x1001) % 13.60/13.67 [104]P1(x1041)+P5(f8(x1041),f20(x1041)) % 13.60/13.67 [105]P1(x1051)+P5(f9(x1051),f20(x1051)) % 13.60/13.67 [103]~P1(x1031)+~P13(x1032,x1031) % 13.60/13.67 [107]~P13(x1071,x1072)+P5(x1071,x1072) % 13.60/13.67 [111]~P13(x1112,x1111)+~P13(x1111,x1112) % 13.60/13.67 [109]~P20(x1091,x1092)+P5(x1091,f20(x1092)) % 13.60/13.67 [112]P20(x1121,x1122)+~P5(x1121,f20(x1122)) % 13.60/13.67 [97]~P3(x971)+~P4(x971)+P18(x971) % 13.60/13.67 [101]~P11(x1011)+P7(x1011)+~P1(f24(x1011)) % 13.60/13.67 [102]~P11(x1021)+P7(x1021)+~P1(f10(x1021)) % 13.60/13.67 [113]~P11(x1131)+P7(x1131)+P5(f10(x1131),f20(f24(x1131))) % 13.60/13.67 [96]~P1(x962)+~P1(x961)+E(x961,x962) % 13.60/13.67 [106]~P12(x1061,x1062)+P10(x1061)+~P11(x1062) % 13.60/13.67 [108]~P5(x1082,x1081)+P1(x1081)+P13(x1082,x1081) % 13.60/13.67 [110]P6(x1101)+~P6(x1102)+~P5(x1101,f20(x1102)) % 13.60/13.67 [114]~P1(x1141)+~P13(x1142,x1143)+~P5(x1143,f20(x1141)) % 13.60/13.67 [115]P5(x1151,x1152)+~P13(x1151,x1153)+~P5(x1153,f20(x1152)) % 13.60/13.67 [117]~P8(x1171)+~P9(x1171)+P7(x1171)+P19(f23(x1171,x1172),x1171,x1172)+~P5(x1172,f24(x1171)) % 13.60/13.67 [118]~P8(x1181)+~P9(x1181)+P7(x1181)+~P19(x1182,x1181,x1183)+~P5(x1183,f24(x1181))+P5(x1182,f20(f24(x1181))) % 13.60/13.67 [116]~P8(x1162)+~P9(x1162)+~P21(x1161)+~P2(x1161)+~P12(x1161,x1162)+P7(x1161)+P7(x1162)+P5(f21(x1162,x1161),f20(f24(x1162))) % 13.60/13.67 [119]~P21(x1191)+~P2(x1191)+~P11(x1192)+~P12(x1191,x1192)+~P17(x1192,x1191,x1193)+P7(x1191)+P16(x1192,x1191,x1193)+P7(x1192) % 13.60/13.67 [121]~P8(x1212)+~P9(x1212)+~P12(x1211,x1212)+P7(x1211)+P15(x1212,x1211,x1213)+P7(x1212)+P19(f17(x1212,x1211,x1213),x1212,x1213)+~P5(x1213,f24(x1212)) % 13.60/13.67 [124]~P8(x1242)+~P9(x1242)+~P12(x1241,x1242)+P7(x1241)+P15(x1242,x1241,x1243)+P7(x1242)+~P16(x1242,x1241,f17(x1242,x1241,x1243))+~P5(x1243,f24(x1242)) % 13.60/13.67 [122]~P8(x1222)+~P9(x1222)+~P12(x1221,x1222)+~P15(x1222,x1221,x1224)+P7(x1221)+P16(x1222,x1221,x1223)+~P19(x1223,x1222,x1224)+P7(x1222)+~P5(x1224,f24(x1222)) % 13.60/13.67 [120]P7(x1203)+P7(x1202)+~P8(x1202)+~P9(x1202)+~P21(x1203)+~P2(x1203)+~P12(x1203,x1202)+P5(f16(x1202,x1203,x1201),f24(x1202))+E(x1201,f21(x1202,x1203))+~P5(x1201,f20(f24(x1202))) % 13.60/13.67 [126]P7(x1263)+P7(x1262)+~P8(x1262)+~P9(x1262)+~P21(x1263)+~P2(x1263)+~P12(x1263,x1262)+~P17(x1262,x1263,f18(x1262,x1263,x1261))+~P13(f16(x1262,x1263,x1261),x1261)+E(x1261,f21(x1262,x1263))+~P5(x1261,f20(f24(x1262))) % 13.60/13.67 [127]P7(x1273)+P7(x1272)+~P8(x1272)+~P9(x1272)+~P21(x1273)+~P2(x1273)+~P12(x1273,x1272)+P19(f18(x1272,x1273,x1271),x1272,f16(x1272,x1273,x1271))+~P13(f16(x1272,x1273,x1271),x1271)+E(x1271,f21(x1272,x1273))+~P5(x1271,f20(f24(x1272))) % 13.60/13.67 [125]P7(x1253)+P7(x1252)+~P8(x1252)+~P9(x1252)+~P21(x1253)+~P2(x1253)+~P12(x1253,x1252)+P17(x1252,x1253,x1254)+~P19(x1254,x1252,f16(x1252,x1253,x1251))+P13(f16(x1252,x1253,x1251),x1251)+E(x1251,f21(x1252,x1253))+~P5(x1251,f20(f24(x1252))) % 13.60/13.67 [128]~P8(x1282)+~P9(x1282)+~P21(x1281)+~P2(x1281)+~P12(x1281,x1282)+P7(x1281)+P7(x1282)+P13(x1283,x1284)+P19(f15(x1282,x1281,x1284,x1283),x1282,x1283)+~E(x1284,f21(x1282,x1281))+~P5(x1283,f24(x1282))+~P5(x1284,f20(f24(x1282))) % 13.60/13.67 [129]~P8(x1292)+~P9(x1292)+~P21(x1291)+~P2(x1291)+~P12(x1291,x1292)+P7(x1291)+P7(x1292)+P13(x1293,x1294)+~P17(x1292,x1291,f15(x1292,x1291,x1294,x1293))+~E(x1294,f21(x1292,x1291))+~P5(x1293,f24(x1292))+~P5(x1294,f20(f24(x1292))) % 13.60/13.67 [123]~P8(x1232)+~P9(x1232)+~P21(x1231)+~P2(x1231)+~P12(x1231,x1232)+~P19(x1233,x1232,x1235)+P7(x1231)+P17(x1232,x1231,x1233)+P7(x1232)+~P13(x1235,x1234)+~P5(x1235,f24(x1232))+~E(x1234,f21(x1232,x1231))+~P5(x1234,f20(f24(x1232))) % 13.60/13.67 %EqnAxiom % 13.60/13.67 [1]E(x11,x11) % 13.60/13.67 [2]E(x22,x21)+~E(x21,x22) % 13.60/13.67 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 13.60/13.67 [4]~E(x41,x42)+E(f20(x41),f20(x42)) % 13.60/13.67 [5]~E(x51,x52)+E(f15(x51,x53,x54,x55),f15(x52,x53,x54,x55)) % 13.60/13.67 [6]~E(x61,x62)+E(f15(x63,x61,x64,x65),f15(x63,x62,x64,x65)) % 13.60/13.67 [7]~E(x71,x72)+E(f15(x73,x74,x71,x75),f15(x73,x74,x72,x75)) % 13.60/13.67 [8]~E(x81,x82)+E(f15(x83,x84,x85,x81),f15(x83,x84,x85,x82)) % 13.60/13.67 [9]~E(x91,x92)+E(f24(x91),f24(x92)) % 13.60/13.67 [10]~E(x101,x102)+E(f16(x101,x103,x104),f16(x102,x103,x104)) % 13.60/13.67 [11]~E(x111,x112)+E(f16(x113,x111,x114),f16(x113,x112,x114)) % 13.60/13.67 [12]~E(x121,x122)+E(f16(x123,x124,x121),f16(x123,x124,x122)) % 13.60/13.67 [13]~E(x131,x132)+E(f4(x131),f4(x132)) % 13.60/13.67 [14]~E(x141,x142)+E(f21(x141,x143),f21(x142,x143)) % 13.60/13.67 [15]~E(x151,x152)+E(f21(x153,x151),f21(x153,x152)) % 13.60/13.67 [16]~E(x161,x162)+E(f18(x161,x163,x164),f18(x162,x163,x164)) % 13.60/13.67 [17]~E(x171,x172)+E(f18(x173,x171,x174),f18(x173,x172,x174)) % 13.60/13.67 [18]~E(x181,x182)+E(f18(x183,x184,x181),f18(x183,x184,x182)) % 13.60/13.67 [19]~E(x191,x192)+E(f8(x191),f8(x192)) % 13.60/13.67 [20]~E(x201,x202)+E(f9(x201),f9(x202)) % 13.60/13.67 [21]~E(x211,x212)+E(f23(x211,x213),f23(x212,x213)) % 13.60/13.67 [22]~E(x221,x222)+E(f23(x223,x221),f23(x223,x222)) % 13.60/13.67 [23]~E(x231,x232)+E(f17(x231,x233,x234),f17(x232,x233,x234)) % 13.60/13.67 [24]~E(x241,x242)+E(f17(x243,x241,x244),f17(x243,x242,x244)) % 13.60/13.67 [25]~E(x251,x252)+E(f17(x253,x254,x251),f17(x253,x254,x252)) % 13.60/13.67 [26]~E(x261,x262)+E(f22(x261),f22(x262)) % 13.60/13.67 [27]~E(x271,x272)+E(f10(x271),f10(x272)) % 13.60/13.67 [28]~P1(x281)+P1(x282)+~E(x281,x282) % 13.60/13.67 [29]P17(x292,x293,x294)+~E(x291,x292)+~P17(x291,x293,x294) % 13.60/13.67 [30]P17(x303,x302,x304)+~E(x301,x302)+~P17(x303,x301,x304) % 13.60/13.67 [31]P17(x313,x314,x312)+~E(x311,x312)+~P17(x313,x314,x311) % 13.60/13.67 [32]~P6(x321)+P6(x322)+~E(x321,x322) % 13.60/13.67 [33]~P8(x331)+P8(x332)+~E(x331,x332) % 13.60/13.67 [34]~P9(x341)+P9(x342)+~E(x341,x342) % 13.60/13.67 [35]P12(x352,x353)+~E(x351,x352)+~P12(x351,x353) % 13.60/13.67 [36]P12(x363,x362)+~E(x361,x362)+~P12(x363,x361) % 13.60/13.67 [37]~P21(x371)+P21(x372)+~E(x371,x372) % 13.60/13.67 [38]~P2(x381)+P2(x382)+~E(x381,x382) % 13.60/13.67 [39]~P10(x391)+P10(x392)+~E(x391,x392) % 13.60/13.67 [40]~P11(x401)+P11(x402)+~E(x401,x402) % 13.60/13.67 [41]~P7(x411)+P7(x412)+~E(x411,x412) % 13.60/13.67 [42]~P18(x421)+P18(x422)+~E(x421,x422) % 13.60/13.67 [43]~P3(x431)+P3(x432)+~E(x431,x432) % 13.60/13.67 [44]~P4(x441)+P4(x442)+~E(x441,x442) % 13.60/13.67 [45]P16(x452,x453,x454)+~E(x451,x452)+~P16(x451,x453,x454) % 13.60/13.67 [46]P16(x463,x462,x464)+~E(x461,x462)+~P16(x463,x461,x464) % 13.60/13.67 [47]P16(x473,x474,x472)+~E(x471,x472)+~P16(x473,x474,x471) % 13.60/13.67 [48]P20(x482,x483)+~E(x481,x482)+~P20(x481,x483) % 13.60/13.67 [49]P20(x493,x492)+~E(x491,x492)+~P20(x493,x491) % 13.60/13.67 [50]P5(x502,x503)+~E(x501,x502)+~P5(x501,x503) % 13.60/13.67 [51]P5(x513,x512)+~E(x511,x512)+~P5(x513,x511) % 13.60/13.67 [52]P13(x522,x523)+~E(x521,x522)+~P13(x521,x523) % 13.60/13.67 [53]P13(x533,x532)+~E(x531,x532)+~P13(x533,x531) % 13.60/13.67 [54]P19(x542,x543,x544)+~E(x541,x542)+~P19(x541,x543,x544) % 13.60/13.67 [55]P19(x553,x552,x554)+~E(x551,x552)+~P19(x553,x551,x554) % 13.60/13.67 [56]P19(x563,x564,x562)+~E(x561,x562)+~P19(x563,x564,x561) % 13.60/13.67 [57]P15(x572,x573,x574)+~E(x571,x572)+~P15(x571,x573,x574) % 13.60/13.67 [58]P15(x583,x582,x584)+~E(x581,x582)+~P15(x583,x581,x584) % 13.60/13.67 [59]P15(x593,x594,x592)+~E(x591,x592)+~P15(x593,x594,x591) % 13.60/13.67 [60]~P14(x601)+P14(x602)+~E(x601,x602) % 13.60/13.67 % 13.60/13.67 %------------------------------------------- % 13.60/13.67 cnf(130,plain, % 13.60/13.67 (~P9(x1301)+~P2(x1302)+~P12(x1302,x1301)+P7(x1302)+P17(x1301,x1302,x1303)+P7(x1301)+~P8(x1301)+~P19(x1303,x1301,x1304)+~P21(x1302)+~P13(x1304,f21(x1301,x1302))+~P5(x1304,f24(x1301))+~P5(f21(x1301,x1302),f20(f24(x1301)))), % 13.60/13.67 inference(equality_inference,[],[123])). % 13.60/13.67 cnf(138,plain, % 13.60/13.67 (P5(f4(x1381),x1381)), % 13.60/13.67 inference(rename_variables,[],[78])). % 13.60/13.67 cnf(140,plain, % 13.60/13.67 (P13(f4(a3),a3)), % 13.60/13.67 inference(scs_inference,[],[79,78,138,61,80,103,111,112,108])). % 13.60/13.67 cnf(141,plain, % 13.60/13.67 (P5(f4(x1411),x1411)), % 13.60/13.67 inference(rename_variables,[],[78])). % 13.60/13.67 cnf(143,plain, % 13.60/13.67 (~P13(x1431,f4(f20(a1)))), % 13.60/13.67 inference(scs_inference,[],[79,78,138,141,61,80,103,111,112,108,114])). % 13.60/13.67 cnf(144,plain, % 13.60/13.67 (P5(f4(x1441),x1441)), % 13.60/13.67 inference(rename_variables,[],[78])). % 13.60/13.67 cnf(150,plain, % 13.60/13.67 (~P1(f21(a5,a12))), % 13.60/13.67 inference(scs_inference,[],[79,78,138,141,144,61,63,80,103,111,112,108,114,53,110,96])). % 13.60/13.67 cnf(167,plain, % 13.60/13.67 (~P13(x1671,a2)), % 13.60/13.67 inference(scs_inference,[],[62,103])). % 13.60/13.67 cnf(171,plain, % 13.60/13.67 (P13(f4(f21(a5,a12)),f21(a5,a12))), % 13.60/13.67 inference(scs_inference,[],[140,78,150,62,103,111,108])). % 13.60/13.67 cnf(172,plain, % 13.60/13.67 (P5(f4(x1721),x1721)), % 13.60/13.67 inference(rename_variables,[],[78])). % 13.60/13.67 cnf(179,plain, % 13.60/13.67 (P19(f17(a5,a12,a14),a5,a14)), % 13.60/13.67 inference(scs_inference,[],[64,84,86,66,83,75,77,79,143,140,78,172,150,62,103,111,108,114,53,121])). % 13.60/13.67 cnf(181,plain, % 13.60/13.67 (~P16(a5,a12,f17(a5,a12,a14))), % 13.60/13.67 inference(scs_inference,[],[64,84,86,66,83,75,77,79,143,140,78,172,150,62,103,111,108,114,53,121,124])). % 13.60/13.67 cnf(197,plain, % 13.60/13.67 (P13(f4(a7),a7)), % 13.60/13.67 inference(scs_inference,[],[171,78,81,111,108])). % 13.60/13.67 cnf(216,plain, % 13.60/13.67 (P13(f4(f20(x2161)),f20(x2161))), % 13.60/13.67 inference(scs_inference,[],[197,78,85,111,108])). % 13.60/13.67 cnf(232,plain, % 13.60/13.67 (~P17(a5,a12,f17(a5,a12,a14))+~P11(a5)), % 13.60/13.67 inference(scs_inference,[],[75,79,67,68,84,83,216,167,181,111,53,52,119])). % 13.60/13.67 cnf(2539,plain, % 13.60/13.67 (~P5(f21(a5,a12),f20(f24(a5)))+~P11(a5)), % 13.60/13.67 inference(scs_inference,[],[75,84,83,64,67,79,77,66,179,68,232,130])). % 13.60/13.67 cnf(2888,plain, % 13.60/13.67 (~P11(a5)), % 13.60/13.67 inference(scs_inference,[],[66,68,75,84,83,64,67,2539,116])). % 13.60/13.67 cnf(2889,plain, % 13.60/13.67 ($false), % 13.60/13.67 inference(scs_inference,[],[66,2888,92]), % 13.60/13.67 ['proof']). % 13.60/13.67 % SZS output end Proof % 13.60/13.67 % Total time :13.020000s %------------------------------------------------------------------------------