%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : LAT327+1 : TPTP v8.2.0. Released v3.4.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 10:18:54 EDT 2024 % Result : Theorem 12.15s 12.26s % Output : CNFRefutation 12.15s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.12 % Problem : LAT327+1 : TPTP v8.2.0. Released v3.4.0. % 0.12/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n026.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Fri Jun 21 21:31:09 EDT 2024 % 0.12/0.33 % CPUTime : % 0.20/0.58 start to proof:theBenchmark % 12.15/12.24 %------------------------------------------- % 12.15/12.24 % File :CSE---1.7 % 12.15/12.24 % Problem :theBenchmark % 12.15/12.24 % Transform :cnf % 12.15/12.24 % Format :tptp:raw % 12.15/12.24 % Command :java -jar mcs_scs.jar %d %s % 12.15/12.24 % 12.15/12.24 % Result :Theorem 11.610000s % 12.15/12.24 % Output :CNFRefutation 11.610000s % 12.15/12.24 %------------------------------------------- % 12.15/12.24 %------------------------------------------------------------------------------ % 12.15/12.24 % File : LAT327+1 : TPTP v8.2.0. Released v3.4.0. % 12.15/12.24 % Domain : Lattice Theory % 12.15/12.24 % Problem : Ideals T64 % 12.15/12.24 % Version : [Urb08] axioms : Especial. % 12.15/12.24 % English : % 12.15/12.24 % 12.15/12.24 % Refs : [Ban96] Bancerek (1996), Ideals % 12.15/12.24 % : [Urb07] Urban (2007), MPTP 0.2: Design, Implementation, and In % 12.15/12.24 % : [Urb08] Urban (2006), Email to G. Sutcliffe % 12.15/12.24 % Source : [Urb08] % 12.15/12.24 % Names : t64_filter_2 [Urb08] % 12.15/12.24 % 12.15/12.24 % Status : Theorem % 12.15/12.24 % Rating : 0.19 v8.2.0, 0.17 v8.1.0, 0.11 v7.5.0, 0.12 v7.4.0, 0.10 v7.2.0, 0.07 v7.1.0, 0.09 v7.0.0, 0.03 v6.4.0, 0.08 v6.1.0, 0.17 v6.0.0, 0.22 v5.5.0, 0.19 v5.4.0, 0.25 v5.3.0, 0.30 v5.2.0, 0.05 v5.1.0, 0.10 v5.0.0, 0.12 v4.1.0, 0.17 v4.0.0, 0.21 v3.7.0, 0.15 v3.5.0, 0.16 v3.4.0 % 12.15/12.24 % Syntax : Number of formulae : 43 ( 15 unt; 0 def) % 12.15/12.24 % Number of atoms : 136 ( 2 equ) % 12.15/12.24 % Maximal formula atoms : 10 ( 3 avg) % 12.15/12.24 % Number of connectives : 121 ( 28 ~; 1 |; 57 &) % 12.15/12.24 % ( 3 <=>; 32 =>; 0 <=; 0 <~>) % 12.15/12.25 % Maximal formula depth : 12 ( 5 avg) % 12.15/12.25 % Maximal term depth : 3 ( 1 avg) % 12.15/12.25 % Number of predicates : 22 ( 20 usr; 1 prp; 0-3 aty) % 12.15/12.25 % Number of functors : 4 ( 4 usr; 1 con; 0-3 aty) % 12.15/12.25 % Number of variables : 66 ( 53 !; 13 ?) % 12.15/12.25 % SPC : FOF_THM_RFO_SEQ % 12.15/12.25 % 12.15/12.25 % Comments : Normal version: includes the axioms (which may be theorems from % 12.15/12.25 % other articles) and background that are possibly necessary. % 12.15/12.25 % : Translated by MPTP from the Mizar Mathematical Library 4.48.930. % 12.15/12.25 % : The problem encoding is based on set theory. % 12.15/12.25 %------------------------------------------------------------------------------ % 12.15/12.25 fof(t64_filter_2,conjecture, % 12.15/12.25 ! [A] : % 12.15/12.25 ( ( ~ v3_struct_0(A) % 12.15/12.25 & v10_lattices(A) % 12.15/12.25 & l3_lattices(A) ) % 12.15/12.25 => ! [B] : % 12.15/12.25 ( m1_subset_1(B,u1_struct_0(A)) % 12.15/12.25 => ! [C] : % 12.15/12.25 ( m1_subset_1(C,u1_struct_0(A)) % 12.15/12.25 => ( r3_lattices(A,B,C) % 12.15/12.25 => ( r2_hidden(B,k22_filter_2(A,B,C)) % 12.15/12.25 & r2_hidden(C,k22_filter_2(A,B,C)) ) ) ) ) ) ). % 12.15/12.25 % 12.15/12.25 fof(reflexivity_r1_tarski,axiom, % 12.15/12.25 ! [A,B] : r1_tarski(A,A) ). % 12.15/12.25 % 12.15/12.25 fof(dt_k1_xboole_0,axiom, % 12.15/12.25 $true ). % 12.15/12.25 % 12.15/12.25 fof(dt_k1_zfmisc_1,axiom, % 12.15/12.25 $true ). % 12.15/12.25 % 12.15/12.25 fof(fc1_subset_1,axiom, % 12.15/12.25 ! [A] : ~ v1_xboole_0(k1_zfmisc_1(A)) ). % 12.15/12.25 % 12.15/12.25 fof(fc1_xboole_0,axiom, % 12.15/12.25 v1_xboole_0(k1_xboole_0) ). % 12.15/12.25 % 12.15/12.25 fof(rc1_subset_1,axiom, % 12.15/12.25 ! [A] : % 12.15/12.25 ( ~ v1_xboole_0(A) % 12.15/12.25 => ? [B] : % 12.15/12.25 ( m1_subset_1(B,k1_zfmisc_1(A)) % 12.15/12.25 & ~ v1_xboole_0(B) ) ) ). % 12.15/12.25 % 12.15/12.25 fof(rc2_subset_1,axiom, % 12.15/12.25 ! [A] : % 12.15/12.25 ? [B] : % 12.15/12.25 ( m1_subset_1(B,k1_zfmisc_1(A)) % 12.15/12.25 & v1_xboole_0(B) ) ). % 12.15/12.25 % 12.15/12.25 fof(rc5_struct_0,axiom, % 12.15/12.25 ! [A] : % 12.15/12.25 ( ( ~ v3_struct_0(A) % 12.15/12.25 & l1_struct_0(A) ) % 12.15/12.25 => ? [B] : % 12.15/12.25 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 12.15/12.25 & ~ v1_xboole_0(B) ) ) ). % 12.15/12.25 % 12.15/12.25 fof(t3_subset,axiom, % 12.15/12.25 ! [A,B] : % 12.15/12.25 ( m1_subset_1(A,k1_zfmisc_1(B)) % 12.15/12.25 <=> r1_tarski(A,B) ) ). % 12.15/12.25 % 12.15/12.25 fof(t4_subset,axiom, % 12.15/12.25 ! [A,B,C] : % 12.15/12.25 ( ( r2_hidden(A,B) % 12.15/12.25 & m1_subset_1(B,k1_zfmisc_1(C)) ) % 12.15/12.25 => m1_subset_1(A,C) ) ). % 12.15/12.25 % 12.15/12.25 fof(t5_subset,axiom, % 12.15/12.25 ! [A,B,C] : % 12.15/12.25 ~ ( r2_hidden(A,B) % 12.15/12.25 & m1_subset_1(B,k1_zfmisc_1(C)) % 12.15/12.25 & v1_xboole_0(C) ) ). % 12.15/12.25 % 12.15/12.25 fof(t8_boole,axiom, % 12.15/12.25 ! [A,B] : % 12.15/12.25 ~ ( v1_xboole_0(A) % 12.15/12.25 & A != B % 12.15/12.25 & v1_xboole_0(B) ) ). % 12.15/12.25 % 12.15/12.25 fof(existence_l1_lattices,axiom, % 12.15/12.25 ? [A] : l1_lattices(A) ). % 12.15/12.25 % 12.15/12.25 fof(existence_l1_struct_0,axiom, % 12.15/12.25 ? [A] : l1_struct_0(A) ). % 12.15/12.25 % 12.15/12.25 fof(existence_l2_lattices,axiom, % 12.15/12.25 ? [A] : l2_lattices(A) ). % 12.15/12.25 % 12.15/12.25 fof(existence_m2_lattice4,axiom, % 12.15/12.25 ! [A] : % 12.15/12.25 ( ( ~ v3_struct_0(A) % 12.15/12.25 & v10_lattices(A) % 12.15/12.25 & l3_lattices(A) ) % 12.15/12.25 => ? [B] : m2_lattice4(B,A) ) ). % 12.15/12.25 % 12.15/12.25 fof(dt_l1_lattices,axiom, % 12.15/12.25 ! [A] : % 12.15/12.25 ( l1_lattices(A) % 12.15/12.25 => l1_struct_0(A) ) ). % 12.15/12.25 % 12.15/12.25 fof(dt_l1_struct_0,axiom, % 12.15/12.25 $true ). % 12.15/12.25 % 12.15/12.25 fof(dt_l2_lattices,axiom, % 12.15/12.25 ! [A] : % 12.15/12.25 ( l2_lattices(A) % 12.15/12.25 => l1_struct_0(A) ) ). % 12.15/12.25 % 12.15/12.25 fof(dt_m2_lattice4,axiom, % 12.15/12.25 ! [A] : % 12.15/12.25 ( ( ~ v3_struct_0(A) % 12.15/12.25 & v10_lattices(A) % 12.15/12.25 & l3_lattices(A) ) % 12.15/12.25 => ! [B] : % 12.15/12.25 ( m2_lattice4(B,A) % 12.15/12.25 => m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) ) ) ). % 12.15/12.25 % 12.15/12.25 fof(cc1_funct_1,axiom, % 12.15/12.25 ! [A] : % 12.15/12.25 ( v1_xboole_0(A) % 12.15/12.25 => v1_funct_1(A) ) ). % 12.15/12.25 % 12.15/12.25 fof(cc2_lattices,axiom, % 12.15/12.25 ! [A] : % 12.15/12.25 ( l3_lattices(A) % 12.15/12.25 => ( ( ~ v3_struct_0(A) % 12.15/12.25 & v4_lattices(A) % 12.15/12.25 & v5_lattices(A) % 12.15/12.25 & v6_lattices(A) % 12.15/12.25 & v7_lattices(A) % 12.15/12.25 & v8_lattices(A) % 12.15/12.25 & v9_lattices(A) ) % 12.15/12.25 => ( ~ v3_struct_0(A) % 12.15/12.25 & v10_lattices(A) ) ) ) ). % 12.15/12.25 % 12.15/12.25 fof(fc1_struct_0,axiom, % 12.15/12.25 ! [A] : % 12.15/12.25 ( ( ~ v3_struct_0(A) % 12.15/12.25 & l1_struct_0(A) ) % 12.15/12.25 => ~ v1_xboole_0(u1_struct_0(A)) ) ). % 12.15/12.25 % 12.15/12.25 fof(rc1_lattice4,axiom, % 12.15/12.25 ! [A] : % 12.15/12.25 ( ( ~ v3_struct_0(A) % 12.15/12.25 & v10_lattices(A) % 12.15/12.25 & l3_lattices(A) ) % 12.15/12.25 => ? [B] : % 12.15/12.25 ( m2_lattice4(B,A) % 12.15/12.25 & ~ v1_xboole_0(B) ) ) ). % 12.15/12.25 % 12.15/12.25 fof(rc1_xboole_0,axiom, % 12.15/12.25 ? [A] : v1_xboole_0(A) ). % 12.15/12.25 % 12.15/12.25 fof(rc2_xboole_0,axiom, % 12.15/12.25 ? [A] : ~ v1_xboole_0(A) ). % 12.15/12.25 % 12.15/12.25 fof(rc3_struct_0,axiom, % 12.15/12.25 ? [A] : % 12.15/12.25 ( l1_struct_0(A) % 12.15/12.25 & ~ v3_struct_0(A) ) ). % 12.15/12.25 % 12.15/12.25 fof(t2_subset,axiom, % 12.15/12.25 ! [A,B] : % 12.15/12.25 ( m1_subset_1(A,B) % 12.15/12.25 => ( v1_xboole_0(B) % 12.15/12.25 | r2_hidden(A,B) ) ) ). % 12.15/12.25 % 12.15/12.25 fof(t6_boole,axiom, % 12.15/12.25 ! [A] : % 12.15/12.25 ( v1_xboole_0(A) % 12.15/12.25 => A = k1_xboole_0 ) ). % 12.15/12.25 % 12.15/12.25 fof(antisymmetry_r2_hidden,axiom, % 12.15/12.25 ! [A,B] : % 12.15/12.25 ( r2_hidden(A,B) % 12.15/12.25 => ~ r2_hidden(B,A) ) ). % 12.15/12.25 % 12.15/12.25 fof(reflexivity_r3_lattices,axiom, % 12.15/12.25 ! [A,B,C] : % 12.15/12.25 ( ( ~ v3_struct_0(A) % 12.15/12.25 & v6_lattices(A) % 12.15/12.25 & v8_lattices(A) % 12.15/12.25 & v9_lattices(A) % 12.15/12.25 & l3_lattices(A) % 12.15/12.25 & m1_subset_1(B,u1_struct_0(A)) % 12.15/12.25 & m1_subset_1(C,u1_struct_0(A)) ) % 12.15/12.25 => r3_lattices(A,B,B) ) ). % 12.15/12.25 % 12.15/12.25 fof(existence_l3_lattices,axiom, % 12.15/12.25 ? [A] : l3_lattices(A) ). % 12.15/12.25 % 12.15/12.25 fof(existence_m1_subset_1,axiom, % 12.15/12.25 ! [A] : % 12.15/12.25 ? [B] : m1_subset_1(B,A) ). % 12.15/12.25 % 12.15/12.25 fof(redefinition_r3_lattices,axiom, % 12.15/12.25 ! [A,B,C] : % 12.15/12.25 ( ( ~ v3_struct_0(A) % 12.15/12.25 & v6_lattices(A) % 12.15/12.25 & v8_lattices(A) % 12.15/12.25 & v9_lattices(A) % 12.15/12.25 & l3_lattices(A) % 12.15/12.25 & m1_subset_1(B,u1_struct_0(A)) % 12.15/12.25 & m1_subset_1(C,u1_struct_0(A)) ) % 12.15/12.25 => ( r3_lattices(A,B,C) % 12.15/12.25 <=> r1_lattices(A,B,C) ) ) ). % 12.15/12.25 % 12.15/12.25 fof(dt_k22_filter_2,axiom, % 12.15/12.25 ! [A,B,C] : % 12.15/12.25 ( ( ~ v3_struct_0(A) % 12.15/12.25 & v10_lattices(A) % 12.15/12.25 & l3_lattices(A) % 12.15/12.25 & m1_subset_1(B,u1_struct_0(A)) % 12.15/12.25 & m1_subset_1(C,u1_struct_0(A)) ) % 12.15/12.25 => ( ~ v1_xboole_0(k22_filter_2(A,B,C)) % 12.15/12.25 & m2_lattice4(k22_filter_2(A,B,C),A) ) ) ). % 12.15/12.25 % 12.15/12.25 fof(dt_l3_lattices,axiom, % 12.15/12.25 ! [A] : % 12.15/12.25 ( l3_lattices(A) % 12.15/12.25 => ( l1_lattices(A) % 12.15/12.25 & l2_lattices(A) ) ) ). % 12.15/12.25 % 12.15/12.25 fof(dt_m1_subset_1,axiom, % 12.15/12.25 $true ). % 12.15/12.25 % 12.15/12.25 fof(dt_u1_struct_0,axiom, % 12.15/12.25 $true ). % 12.15/12.25 % 12.15/12.25 fof(cc1_lattices,axiom, % 12.15/12.25 ! [A] : % 12.15/12.26 ( l3_lattices(A) % 12.15/12.26 => ( ( ~ v3_struct_0(A) % 12.15/12.26 & v10_lattices(A) ) % 12.15/12.26 => ( ~ v3_struct_0(A) % 12.15/12.26 & v4_lattices(A) % 12.15/12.26 & v5_lattices(A) % 12.15/12.26 & v6_lattices(A) % 12.15/12.26 & v7_lattices(A) % 12.15/12.26 & v8_lattices(A) % 12.15/12.26 & v9_lattices(A) ) ) ) ). % 12.15/12.26 % 12.15/12.26 fof(t1_subset,axiom, % 12.15/12.26 ! [A,B] : % 12.15/12.26 ( r2_hidden(A,B) % 12.15/12.26 => m1_subset_1(A,B) ) ). % 12.15/12.26 % 12.15/12.26 fof(t7_boole,axiom, % 12.15/12.26 ! [A,B] : % 12.15/12.26 ~ ( r2_hidden(A,B) % 12.15/12.26 & v1_xboole_0(B) ) ). % 12.15/12.26 % 12.15/12.26 fof(t63_filter_2,axiom, % 12.15/12.26 ! [A] : % 12.15/12.26 ( ( ~ v3_struct_0(A) % 12.15/12.26 & v10_lattices(A) % 12.15/12.26 & l3_lattices(A) ) % 12.15/12.26 => ! [B] : % 12.15/12.26 ( m1_subset_1(B,u1_struct_0(A)) % 12.15/12.26 => ! [C] : % 12.15/12.26 ( m1_subset_1(C,u1_struct_0(A)) % 12.15/12.26 => ! [D] : % 12.15/12.26 ( m1_subset_1(D,u1_struct_0(A)) % 12.15/12.26 => ( r3_lattices(A,B,C) % 12.15/12.26 => ( r2_hidden(D,k22_filter_2(A,B,C)) % 12.15/12.26 <=> ( r3_lattices(A,B,D) % 12.15/12.26 & r3_lattices(A,D,C) ) ) ) ) ) ) ) ). % 12.15/12.26 % 12.15/12.26 %------------------------------------------------------------------------------ % 12.15/12.26 %------------------------------------------- % 12.15/12.26 % Proof found % 12.15/12.26 % SZS status Theorem for theBenchmark % 12.15/12.26 % SZS output start Proof % 12.15/12.26 %ClaNum:102(EqnAxiom:42) % 12.15/12.26 %VarNum:251(SingletonVarNum:75) % 12.15/12.26 %MaxLitNum:10 % 12.15/12.26 %MaxfuncDepth:2 % 12.15/12.26 %SharedTerms:30 % 12.15/12.26 %goalClause: 43 44 54 55 58 59 99 % 12.15/12.26 %singleGoalClaCount:6 % 12.15/12.26 [43]P1(a1) % 12.15/12.26 [44]P2(a1) % 12.15/12.26 [45]P2(a2) % 12.15/12.26 [46]P12(a9) % 12.15/12.26 [47]P12(a3) % 12.15/12.26 [48]P3(a10) % 12.15/12.26 [49]P3(a6) % 12.15/12.26 [50]P4(a11) % 12.15/12.26 [51]P5(a17) % 12.15/12.26 [58]P10(a1,a13,a14) % 12.15/12.26 [59]~P14(a1) % 12.15/12.26 [60]~P14(a6) % 12.15/12.26 [61]~P12(a7) % 12.15/12.26 [54]P7(a13,f18(a1)) % 12.15/12.26 [55]P7(a14,f18(a1)) % 12.15/12.26 [53]P6(x531,x531) % 12.15/12.26 [52]P12(f12(x521)) % 12.15/12.26 [56]P7(f8(x561),x561) % 12.15/12.26 [57]P7(f12(x571),f19(x571)) % 12.15/12.26 [62]~P12(f19(x621)) % 12.15/12.26 [99]~P11(a14,f20(a1,a13,a14))+~P11(a13,f20(a1,a13,a14)) % 12.15/12.26 [63]~P12(x631)+E(x631,a9) % 12.15/12.26 [64]~P4(x641)+P3(x641) % 12.15/12.26 [65]~P5(x651)+P3(x651) % 12.15/12.26 [66]~P2(x661)+P4(x661) % 12.15/12.26 [67]~P2(x671)+P5(x671) % 12.15/12.26 [68]~P12(x681)+P13(x681) % 12.15/12.26 [70]P12(x701)+~P12(f15(x701)) % 12.15/12.26 [80]P12(x801)+P7(f15(x801),f19(x801)) % 12.15/12.26 [79]~P12(x791)+~P11(x792,x791) % 12.15/12.26 [82]~P11(x821,x822)+P7(x821,x822) % 12.15/12.26 [87]~P11(x872,x871)+~P11(x871,x872) % 12.15/12.26 [86]~P6(x861,x862)+P7(x861,f19(x862)) % 12.15/12.26 [88]P6(x881,x882)+~P7(x881,f19(x882)) % 12.15/12.26 [77]~P3(x771)+P14(x771)+~P12(f18(x771)) % 12.15/12.26 [78]~P3(x781)+P14(x781)+~P12(f16(x781)) % 12.15/12.26 [89]~P3(x891)+P14(x891)+P7(f16(x891),f19(f18(x891))) % 12.15/12.26 [69]~P12(x692)+~P12(x691)+E(x691,x692) % 12.15/12.26 [85]~P7(x852,x851)+P12(x851)+P11(x852,x851) % 12.15/12.26 [91]~P12(x911)+~P11(x912,x913)+~P7(x913,f19(x911)) % 12.15/12.26 [92]P7(x921,x922)+~P11(x921,x923)+~P7(x923,f19(x922)) % 12.15/12.26 [71]P15(x711)+~P1(x711)+~P2(x711)+P14(x711) % 12.15/12.26 [72]P16(x721)+~P1(x721)+~P2(x721)+P14(x721) % 12.15/12.26 [73]P17(x731)+~P1(x731)+~P2(x731)+P14(x731) % 12.15/12.26 [74]P18(x741)+~P1(x741)+~P2(x741)+P14(x741) % 12.15/12.26 [75]P19(x751)+~P1(x751)+~P2(x751)+P14(x751) % 12.15/12.26 [76]P20(x761)+~P1(x761)+~P2(x761)+P14(x761) % 12.15/12.26 [81]~P1(x811)+~P2(x811)+P14(x811)+~P12(f4(x811)) % 12.15/12.26 [83]~P1(x831)+~P2(x831)+P14(x831)+P8(f5(x831),x831) % 12.15/12.26 [84]~P1(x841)+~P2(x841)+P14(x841)+P8(f4(x841),x841) % 12.15/12.26 [93]~P1(x931)+~P2(x931)+~P8(x932,x931)+P14(x931)+P7(x932,f19(f18(x931))) % 12.15/12.26 [95]~P1(x951)+~P2(x951)+P14(x951)+~P7(x953,f18(x951))+~P7(x952,f18(x951))+P8(f20(x951,x952,x953),x951) % 12.15/12.26 [98]~P1(x981)+~P2(x981)+P14(x981)+~P7(x982,f18(x981))+~P7(x983,f18(x981))+~P12(f20(x981,x983,x982)) % 12.15/12.26 [94]~P2(x941)+~P17(x941)+~P19(x941)+~P20(x941)+P10(x941,x942,x942)+P14(x941)+~P7(x942,f18(x941))+~P7(x943,f18(x941)) % 12.15/12.26 [90]P1(x901)+~P2(x901)+~P15(x901)+~P16(x901)+~P17(x901)+~P18(x901)+~P19(x901)+~P20(x901)+P14(x901) % 12.15/12.26 [96]~P2(x961)+~P17(x961)+~P19(x961)+~P20(x961)+~P9(x961,x962,x963)+P14(x961)+P10(x961,x962,x963)+~P7(x963,f18(x961))+~P7(x962,f18(x961)) % 12.15/12.26 [97]~P2(x971)+~P17(x971)+~P19(x971)+~P20(x971)+~P10(x971,x972,x973)+P14(x971)+P9(x971,x972,x973)+~P7(x973,f18(x971))+~P7(x972,f18(x971)) % 12.15/12.26 [100]~P1(x1001)+~P2(x1001)+P14(x1001)+P10(x1001,x1002,x1003)+~P10(x1001,x1004,x1003)+~P7(x1004,f18(x1001))+~P7(x1003,f18(x1001))+~P7(x1002,f18(x1001))+~P11(x1002,f20(x1001,x1004,x1003)) % 12.15/12.26 [101]~P1(x1011)+~P2(x1011)+P14(x1011)+P10(x1011,x1012,x1013)+~P10(x1011,x1012,x1014)+~P7(x1014,f18(x1011))+~P7(x1013,f18(x1011))+~P7(x1012,f18(x1011))+~P11(x1013,f20(x1011,x1012,x1014)) % 12.15/12.26 [102]~P1(x1021)+~P2(x1021)+~P10(x1021,x1022,x1024)+~P10(x1021,x1023,x1024)+~P10(x1021,x1023,x1022)+P14(x1021)+~P7(x1024,f18(x1021))+~P7(x1022,f18(x1021))+~P7(x1023,f18(x1021))+P11(x1022,f20(x1021,x1023,x1024)) % 12.15/12.26 %EqnAxiom % 12.15/12.26 [1]E(x11,x11) % 12.15/12.26 [2]E(x22,x21)+~E(x21,x22) % 12.15/12.26 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 12.15/12.26 [4]~E(x41,x42)+E(f12(x41),f12(x42)) % 12.15/12.26 [5]~E(x51,x52)+E(f18(x51),f18(x52)) % 12.15/12.26 [6]~E(x61,x62)+E(f20(x61,x63,x64),f20(x62,x63,x64)) % 12.15/12.26 [7]~E(x71,x72)+E(f20(x73,x71,x74),f20(x73,x72,x74)) % 12.15/12.26 [8]~E(x81,x82)+E(f20(x83,x84,x81),f20(x83,x84,x82)) % 12.15/12.26 [9]~E(x91,x92)+E(f8(x91),f8(x92)) % 12.15/12.26 [10]~E(x101,x102)+E(f19(x101),f19(x102)) % 12.15/12.26 [11]~E(x111,x112)+E(f16(x111),f16(x112)) % 12.15/12.26 [12]~E(x121,x122)+E(f4(x121),f4(x122)) % 12.15/12.26 [13]~E(x131,x132)+E(f15(x131),f15(x132)) % 12.15/12.26 [14]~E(x141,x142)+E(f5(x141),f5(x142)) % 12.15/12.26 [15]~P1(x151)+P1(x152)+~E(x151,x152) % 12.15/12.26 [16]~P2(x161)+P2(x162)+~E(x161,x162) % 12.15/12.26 [17]P10(x172,x173,x174)+~E(x171,x172)+~P10(x171,x173,x174) % 12.15/12.26 [18]P10(x183,x182,x184)+~E(x181,x182)+~P10(x183,x181,x184) % 12.15/12.26 [19]P10(x193,x194,x192)+~E(x191,x192)+~P10(x193,x194,x191) % 12.15/12.26 [20]~P12(x201)+P12(x202)+~E(x201,x202) % 12.15/12.26 [21]~P20(x211)+P20(x212)+~E(x211,x212) % 12.15/12.26 [22]~P3(x221)+P3(x222)+~E(x221,x222) % 12.15/12.26 [23]P7(x232,x233)+~E(x231,x232)+~P7(x231,x233) % 12.15/12.26 [24]P7(x243,x242)+~E(x241,x242)+~P7(x243,x241) % 12.15/12.26 [25]~P4(x251)+P4(x252)+~E(x251,x252) % 12.15/12.26 [26]~P5(x261)+P5(x262)+~E(x261,x262) % 12.15/12.26 [27]~P19(x271)+P19(x272)+~E(x271,x272) % 12.15/12.26 [28]P6(x282,x283)+~E(x281,x282)+~P6(x281,x283) % 12.15/12.26 [29]P6(x293,x292)+~E(x291,x292)+~P6(x293,x291) % 12.15/12.26 [30]P11(x302,x303)+~E(x301,x302)+~P11(x301,x303) % 12.15/12.26 [31]P11(x313,x312)+~E(x311,x312)+~P11(x313,x311) % 12.15/12.26 [32]~P14(x321)+P14(x322)+~E(x321,x322) % 12.15/12.26 [33]~P18(x331)+P18(x332)+~E(x331,x332) % 12.15/12.26 [34]~P17(x341)+P17(x342)+~E(x341,x342) % 12.15/12.26 [35]~P16(x351)+P16(x352)+~E(x351,x352) % 12.15/12.26 [36]P9(x362,x363,x364)+~E(x361,x362)+~P9(x361,x363,x364) % 12.15/12.26 [37]P9(x373,x372,x374)+~E(x371,x372)+~P9(x373,x371,x374) % 12.15/12.26 [38]P9(x383,x384,x382)+~E(x381,x382)+~P9(x383,x384,x381) % 12.15/12.26 [39]~P13(x391)+P13(x392)+~E(x391,x392) % 12.15/12.26 [40]P8(x402,x403)+~E(x401,x402)+~P8(x401,x403) % 12.15/12.26 [41]P8(x413,x412)+~E(x411,x412)+~P8(x413,x411) % 12.15/12.26 [42]~P15(x421)+P15(x422)+~E(x421,x422) % 12.15/12.26 % 12.15/12.26 %------------------------------------------- % 12.15/12.26 cnf(106,plain, % 12.15/12.26 (P7(f8(x1061),x1061)), % 12.15/12.26 inference(rename_variables,[],[56])). % 12.15/12.26 cnf(108,plain, % 12.15/12.26 (P11(f8(a7),a7)), % 12.15/12.26 inference(scs_inference,[],[56,106,46,61,79,88,85])). % 12.15/12.26 cnf(109,plain, % 12.15/12.26 (P7(f8(x1091),x1091)), % 12.15/12.26 inference(rename_variables,[],[56])). % 12.15/12.26 cnf(112,plain, % 12.15/12.26 (~P11(x1121,f8(f19(a9)))), % 12.15/12.26 inference(scs_inference,[],[56,106,109,46,61,79,88,85,31,91])). % 12.15/12.26 cnf(119,plain, % 12.15/12.26 (P17(a1)), % 12.15/12.26 inference(scs_inference,[],[43,44,59,56,106,109,46,61,79,88,85,31,91,71,72,73])). % 12.15/12.26 cnf(123,plain, % 12.15/12.26 (P19(a1)), % 12.15/12.26 inference(scs_inference,[],[43,44,59,56,106,109,46,61,79,88,85,31,91,71,72,73,74,75])). % 12.15/12.26 cnf(125,plain, % 12.15/12.26 (P20(a1)), % 12.15/12.26 inference(scs_inference,[],[43,44,59,56,106,109,46,61,79,88,85,31,91,71,72,73,74,75,76])). % 12.15/12.26 cnf(127,plain, % 12.15/12.26 (P10(a1,a13,a13)), % 12.15/12.26 inference(scs_inference,[],[43,44,59,54,56,106,109,46,61,79,88,85,31,91,71,72,73,74,75,76,94])). % 12.15/12.26 cnf(131,plain, % 12.15/12.26 (P11(a13,f20(a1,a13,a13))), % 12.15/12.26 inference(scs_inference,[],[43,44,59,54,56,106,109,46,61,79,88,85,31,91,71,72,73,74,75,76,94,97,102])). % 12.15/12.26 cnf(161,plain, % 12.15/12.26 (P10(a1,a14,a14)), % 12.15/12.26 inference(scs_inference,[],[44,55,59,108,131,119,123,125,112,57,47,62,88,79,87,85,31,91,94])). % 12.15/12.26 cnf(165,plain, % 12.15/12.26 (P11(a14,f20(a1,a14,a14))), % 12.15/12.26 inference(scs_inference,[],[43,44,55,59,108,131,119,123,125,112,57,47,62,88,79,87,85,31,91,94,97,102])). % 12.15/12.26 cnf(4596,plain, % 12.15/12.26 (~P11(a14,f20(a1,a13,a14))), % 12.15/12.26 inference(scs_inference,[],[55,54,44,127,59,43,58,99,102])). % 12.15/12.26 cnf(4598,plain, % 12.15/12.26 ($false), % 12.15/12.26 inference(scs_inference,[],[58,54,55,43,44,4596,59,161,165,31,102]), % 12.15/12.26 ['proof']). % 12.15/12.26 % SZS output end Proof % 12.15/12.26 % Total time :11.610000s %------------------------------------------------------------------------------