%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : GRP644+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 06:40:14 EDT 2024 % Result : Theorem 0.57s 0.67s % Output : CNFRefutation 0.57s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.11 % Problem : GRP644+1 : TPTP v8.2.0. Released v3.4.0. % 0.10/0.11 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.11/0.32 % Computer : n026.cluster.edu % 0.11/0.32 % Model : x86_64 x86_64 % 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.32 % Memory : 8042.1875MB % 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.32 % CPULimit : 300 % 0.11/0.32 % WCLimit : 300 % 0.11/0.32 % DateTime : Thu Jun 20 07:21:54 EDT 2024 % 0.11/0.32 % CPUTime : % 0.17/0.57 start to proof:theBenchmark % 0.57/0.66 %------------------------------------------- % 0.57/0.66 % File :CSE---1.7 % 0.57/0.66 % Problem :theBenchmark % 0.57/0.66 % Transform :cnf % 0.57/0.66 % Format :tptp:raw % 0.57/0.66 % Command :java -jar mcs_scs.jar %d %s % 0.57/0.66 % 0.57/0.66 % Result :Theorem 0.030000s % 0.57/0.66 % Output :CNFRefutation 0.030000s % 0.57/0.66 %------------------------------------------- % 0.57/0.66 %------------------------------------------------------------------------------ % 0.57/0.66 % File : GRP644+1 : TPTP v8.2.0. Released v3.4.0. % 0.57/0.66 % Domain : Group Theory % 0.57/0.66 % Problem : On the Lattice of Subgroups of a Group T22 % 0.57/0.66 % Version : [Urb08] axioms : Especial. % 0.57/0.66 % English : % 0.57/0.66 % 0.57/0.66 % Refs : [Gan96] Ganczarski (1996), On the Lattice of Subgroups of a Gr % 0.57/0.66 % : [Urb07] Urban (2007), MPTP 0.2: Design, Implementation, and In % 0.57/0.66 % : [Urb08] Urban (2006), Email to G. Sutcliffe % 0.57/0.66 % Source : [Urb08] % 0.57/0.66 % Names : t22_latsubgr [Urb08] % 0.57/0.66 % 0.57/0.66 % Status : Theorem % 0.57/0.66 % Rating : 0.17 v8.2.0, 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.2.0, 0.16 v6.1.0, 0.13 v6.0.0, 0.17 v5.5.0, 0.11 v5.4.0, 0.18 v5.3.0, 0.22 v5.2.0, 0.10 v5.0.0, 0.17 v4.1.0, 0.22 v4.0.0, 0.25 v3.7.0, 0.20 v3.5.0, 0.21 v3.4.0 % 0.57/0.66 % Syntax : Number of formulae : 55 ( 19 unt; 0 def) % 0.57/0.66 % Number of atoms : 167 ( 6 equ) % 0.57/0.66 % Maximal formula atoms : 9 ( 3 avg) % 0.57/0.66 % Number of connectives : 143 ( 31 ~; 1 |; 65 &) % 0.57/0.66 % ( 3 <=>; 43 =>; 0 <=; 0 <~>) % 0.57/0.66 % Maximal formula depth : 10 ( 5 avg) % 0.57/0.66 % Maximal term depth : 3 ( 1 avg) % 0.57/0.66 % Number of predicates : 20 ( 18 usr; 1 prp; 0-3 aty) % 0.57/0.66 % Number of functors : 10 ( 10 usr; 1 con; 0-2 aty) % 0.57/0.66 % Number of variables : 94 ( 80 !; 14 ?) % 0.57/0.66 % SPC : FOF_THM_RFO_SEQ % 0.57/0.66 % 0.57/0.66 % Comments : Normal version: includes the axioms (which may be theorems from % 0.57/0.66 % other articles) and background that are possibly necessary. % 0.57/0.66 % : Translated by MPTP from the Mizar Mathematical Library 4.48.930. % 0.57/0.66 % : The problem encoding is based on set theory. % 0.57/0.66 %------------------------------------------------------------------------------ % 0.57/0.66 fof(t22_latsubgr,conjecture, % 0.57/0.66 ! [A] : % 0.57/0.66 ( ( ~ v3_struct_0(A) % 0.57/0.66 & v3_group_1(A) % 0.57/0.66 & v4_group_1(A) % 0.57/0.66 & l1_group_1(A) ) % 0.57/0.66 => ! [B] : % 0.57/0.66 ( ( v1_group_1(B) % 0.57/0.66 & m1_group_2(B,A) ) % 0.57/0.66 => ! [C] : % 0.57/0.66 ( m1_subset_1(C,u1_struct_0(A)) % 0.57/0.66 => ( r2_hidden(C,k1_funct_1(k1_latsubgr(A),B)) % 0.57/0.66 => r2_hidden(k3_group_1(A,C),k1_funct_1(k1_latsubgr(A),B)) ) ) ) ) ). % 0.57/0.66 % 0.57/0.66 fof(abstractness_v1_group_1,axiom, % 0.57/0.66 ! [A] : % 0.57/0.66 ( l1_group_1(A) % 0.57/0.66 => ( v1_group_1(A) % 0.57/0.66 => A = g1_group_1(u1_struct_0(A),u1_group_1(A)) ) ) ). % 0.57/0.66 % 0.57/0.66 fof(antisymmetry_r2_hidden,axiom, % 0.57/0.66 ! [A,B] : % 0.57/0.66 ( r2_hidden(A,B) % 0.57/0.66 => ~ r2_hidden(B,A) ) ). % 0.57/0.66 % 0.57/0.66 fof(cc1_funct_2,axiom, % 0.57/0.66 ! [A,B,C] : % 0.57/0.66 ( m1_relset_1(C,A,B) % 0.57/0.66 => ( ( v1_funct_1(C) % 0.57/0.66 & v1_partfun1(C,A,B) ) % 0.57/0.66 => ( v1_funct_1(C) % 0.57/0.66 & v1_funct_2(C,A,B) ) ) ) ). % 0.57/0.66 % 0.57/0.66 fof(cc1_relset_1,axiom, % 0.57/0.66 ! [A,B,C] : % 0.57/0.66 ( m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))) % 0.57/0.66 => v1_relat_1(C) ) ). % 0.57/0.66 % 0.57/0.66 fof(cc5_funct_2,axiom, % 0.57/0.66 ! [A,B] : % 0.57/0.66 ( ~ v1_xboole_0(B) % 0.57/0.66 => ! [C] : % 0.57/0.66 ( m1_relset_1(C,A,B) % 0.57/0.66 => ( ( v1_funct_1(C) % 0.57/0.66 & v1_funct_2(C,A,B) ) % 0.57/0.66 => ( v1_funct_1(C) % 0.57/0.66 & v1_partfun1(C,A,B) % 0.57/0.66 & v1_funct_2(C,A,B) ) ) ) ) ). % 0.57/0.66 % 0.57/0.66 fof(cc6_funct_2,axiom, % 0.57/0.66 ! [A,B] : % 0.57/0.66 ( ( ~ v1_xboole_0(A) % 0.57/0.66 & ~ v1_xboole_0(B) ) % 0.57/0.67 => ! [C] : % 0.57/0.67 ( m1_relset_1(C,A,B) % 0.57/0.67 => ( ( v1_funct_1(C) % 0.57/0.67 & v1_funct_2(C,A,B) ) % 0.57/0.67 => ( v1_funct_1(C) % 0.57/0.67 & ~ v1_xboole_0(C) % 0.57/0.67 & v1_partfun1(C,A,B) % 0.57/0.67 & v1_funct_2(C,A,B) ) ) ) ) ). % 0.57/0.67 % 0.57/0.67 fof(dt_g1_group_1,axiom, % 0.57/0.67 ! [A,B] : % 0.57/0.67 ( ( v1_funct_1(B) % 0.57/0.67 & v1_funct_2(B,k2_zfmisc_1(A,A),A) % 0.57/0.67 & m1_relset_1(B,k2_zfmisc_1(A,A),A) ) % 0.57/0.67 => ( v1_group_1(g1_group_1(A,B)) % 0.57/0.67 & l1_group_1(g1_group_1(A,B)) ) ) ). % 0.57/0.67 % 0.57/0.67 fof(dt_k1_funct_1,axiom, % 0.57/0.67 $true ). % 0.57/0.67 % 0.57/0.67 fof(dt_k1_group_3,axiom, % 0.57/0.67 $true ). % 0.57/0.67 % 0.57/0.67 fof(dt_k1_latsubgr,axiom, % 0.57/0.67 ! [A] : % 0.57/0.67 ( ( ~ v3_struct_0(A) % 0.57/0.67 & v3_group_1(A) % 0.57/0.67 & v4_group_1(A) % 0.57/0.67 & l1_group_1(A) ) % 0.57/0.67 => ( v1_funct_1(k1_latsubgr(A)) % 0.57/0.67 & v1_funct_2(k1_latsubgr(A),k1_group_3(A),k1_zfmisc_1(u1_struct_0(A))) % 0.57/0.67 & m2_relset_1(k1_latsubgr(A),k1_group_3(A),k1_zfmisc_1(u1_struct_0(A))) ) ) ). % 0.57/0.67 % 0.57/0.67 fof(dt_k1_xboole_0,axiom, % 0.57/0.67 $true ). % 0.57/0.67 % 0.57/0.67 fof(dt_k1_zfmisc_1,axiom, % 0.57/0.67 $true ). % 0.57/0.67 % 0.57/0.67 fof(dt_k2_zfmisc_1,axiom, % 0.57/0.67 $true ). % 0.57/0.67 % 0.57/0.67 fof(dt_k3_group_1,axiom, % 0.57/0.67 ! [A,B] : % 0.57/0.67 ( ( ~ v3_struct_0(A) % 0.57/0.67 & v3_group_1(A) % 0.57/0.67 & v4_group_1(A) % 0.57/0.67 & l1_group_1(A) % 0.57/0.67 & m1_subset_1(B,u1_struct_0(A)) ) % 0.57/0.67 => m1_subset_1(k3_group_1(A,B),u1_struct_0(A)) ) ). % 0.57/0.67 % 0.57/0.67 fof(dt_l1_group_1,axiom, % 0.57/0.67 ! [A] : % 0.57/0.67 ( l1_group_1(A) % 0.57/0.67 => l1_struct_0(A) ) ). % 0.57/0.67 % 0.57/0.67 fof(dt_l1_struct_0,axiom, % 0.57/0.67 $true ). % 0.57/0.67 % 0.57/0.67 fof(dt_m1_group_2,axiom, % 0.57/0.67 ! [A] : % 0.57/0.67 ( ( ~ v3_struct_0(A) % 0.57/0.67 & v3_group_1(A) % 0.57/0.67 & l1_group_1(A) ) % 0.57/0.67 => ! [B] : % 0.57/0.67 ( m1_group_2(B,A) % 0.57/0.67 => ( ~ v3_struct_0(B) % 0.57/0.67 & v3_group_1(B) % 0.57/0.67 & l1_group_1(B) ) ) ) ). % 0.57/0.67 % 0.57/0.67 fof(dt_m1_relset_1,axiom, % 0.57/0.67 $true ). % 0.57/0.67 % 0.57/0.67 fof(dt_m1_subset_1,axiom, % 0.57/0.67 $true ). % 0.57/0.67 % 0.57/0.67 fof(dt_m2_relset_1,axiom, % 0.57/0.67 ! [A,B,C] : % 0.57/0.67 ( m2_relset_1(C,A,B) % 0.57/0.67 => m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))) ) ). % 0.57/0.67 % 0.57/0.67 fof(dt_u1_group_1,axiom, % 0.57/0.67 ! [A] : % 0.57/0.67 ( l1_group_1(A) % 0.57/0.67 => ( v1_funct_1(u1_group_1(A)) % 0.57/0.67 & v1_funct_2(u1_group_1(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A)) % 0.57/0.67 & m2_relset_1(u1_group_1(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A)) ) ) ). % 0.57/0.67 % 0.57/0.67 fof(dt_u1_struct_0,axiom, % 0.57/0.67 $true ). % 0.57/0.67 % 0.57/0.67 fof(existence_l1_group_1,axiom, % 0.57/0.67 ? [A] : l1_group_1(A) ). % 0.57/0.67 % 0.57/0.67 fof(existence_l1_struct_0,axiom, % 0.57/0.67 ? [A] : l1_struct_0(A) ). % 0.57/0.67 % 0.57/0.67 fof(existence_m1_group_2,axiom, % 0.57/0.67 ! [A] : % 0.57/0.67 ( ( ~ v3_struct_0(A) % 0.57/0.67 & v3_group_1(A) % 0.57/0.67 & l1_group_1(A) ) % 0.57/0.67 => ? [B] : m1_group_2(B,A) ) ). % 0.57/0.67 % 0.57/0.67 fof(existence_m1_relset_1,axiom, % 0.57/0.67 ! [A,B] : % 0.57/0.67 ? [C] : m1_relset_1(C,A,B) ). % 0.57/0.67 % 0.57/0.67 fof(existence_m1_subset_1,axiom, % 0.57/0.67 ! [A] : % 0.57/0.67 ? [B] : m1_subset_1(B,A) ). % 0.57/0.67 % 0.57/0.67 fof(existence_m2_relset_1,axiom, % 0.57/0.67 ! [A,B] : % 0.57/0.67 ? [C] : m2_relset_1(C,A,B) ). % 0.57/0.67 % 0.57/0.67 fof(fc1_group_3,axiom, % 0.57/0.67 ! [A] : % 0.57/0.67 ( ( ~ v3_struct_0(A) % 0.57/0.67 & v3_group_1(A) % 0.57/0.67 & v4_group_1(A) % 0.57/0.67 & l1_group_1(A) ) % 0.57/0.67 => ~ v1_xboole_0(k1_group_3(A)) ) ). % 0.57/0.67 % 0.57/0.67 fof(fc1_struct_0,axiom, % 0.57/0.67 ! [A] : % 0.57/0.67 ( ( ~ v3_struct_0(A) % 0.57/0.67 & l1_struct_0(A) ) % 0.57/0.67 => ~ v1_xboole_0(u1_struct_0(A)) ) ). % 0.57/0.67 % 0.57/0.67 fof(fc1_subset_1,axiom, % 0.57/0.67 ! [A] : ~ v1_xboole_0(k1_zfmisc_1(A)) ). % 0.57/0.67 % 0.57/0.67 fof(fc1_xboole_0,axiom, % 0.57/0.67 v1_xboole_0(k1_xboole_0) ). % 0.57/0.67 % 0.57/0.67 fof(fc4_subset_1,axiom, % 0.57/0.67 ! [A,B] : % 0.57/0.67 ( ( ~ v1_xboole_0(A) % 0.57/0.67 & ~ v1_xboole_0(B) ) % 0.57/0.67 => ~ v1_xboole_0(k2_zfmisc_1(A,B)) ) ). % 0.57/0.67 % 0.57/0.67 fof(free_g1_group_1,axiom, % 0.57/0.67 ! [A,B] : % 0.57/0.67 ( ( v1_funct_1(B) % 0.57/0.67 & v1_funct_2(B,k2_zfmisc_1(A,A),A) % 0.57/0.67 & m1_relset_1(B,k2_zfmisc_1(A,A),A) ) % 0.57/0.67 => ! [C,D] : % 0.57/0.67 ( g1_group_1(A,B) = g1_group_1(C,D) % 0.57/0.67 => ( A = C % 0.57/0.67 & B = D ) ) ) ). % 0.57/0.67 % 0.57/0.67 fof(rc1_funct_2,axiom, % 0.57/0.67 ! [A,B] : % 0.57/0.67 ? [C] : % 0.57/0.67 ( m1_relset_1(C,A,B) % 0.57/0.67 & v1_relat_1(C) % 0.57/0.67 & v1_funct_1(C) % 0.57/0.67 & v1_funct_2(C,A,B) ) ). % 0.57/0.67 % 0.57/0.67 fof(rc1_subset_1,axiom, % 0.57/0.67 ! [A] : % 0.57/0.67 ( ~ v1_xboole_0(A) % 0.57/0.67 => ? [B] : % 0.57/0.67 ( m1_subset_1(B,k1_zfmisc_1(A)) % 0.57/0.67 & ~ v1_xboole_0(B) ) ) ). % 0.57/0.67 % 0.57/0.67 fof(rc1_xboole_0,axiom, % 0.57/0.67 ? [A] : v1_xboole_0(A) ). % 0.57/0.67 % 0.57/0.67 fof(rc2_partfun1,axiom, % 0.57/0.67 ! [A,B] : % 0.57/0.67 ? [C] : % 0.57/0.67 ( m1_relset_1(C,A,B) % 0.57/0.67 & v1_relat_1(C) % 0.57/0.67 & v1_funct_1(C) ) ). % 0.57/0.67 % 0.57/0.67 fof(rc2_subset_1,axiom, % 0.57/0.67 ! [A] : % 0.57/0.67 ? [B] : % 0.57/0.67 ( m1_subset_1(B,k1_zfmisc_1(A)) % 0.57/0.67 & v1_xboole_0(B) ) ). % 0.57/0.67 % 0.57/0.67 fof(rc2_xboole_0,axiom, % 0.57/0.67 ? [A] : ~ v1_xboole_0(A) ). % 0.57/0.67 % 0.57/0.67 fof(rc3_struct_0,axiom, % 0.57/0.67 ? [A] : % 0.57/0.67 ( l1_struct_0(A) % 0.57/0.67 & ~ v3_struct_0(A) ) ). % 0.57/0.67 % 0.57/0.67 fof(rc5_struct_0,axiom, % 0.57/0.67 ! [A] : % 0.57/0.67 ( ( ~ v3_struct_0(A) % 0.57/0.67 & l1_struct_0(A) ) % 0.57/0.67 => ? [B] : % 0.57/0.67 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 0.57/0.67 & ~ v1_xboole_0(B) ) ) ). % 0.57/0.67 % 0.57/0.67 fof(redefinition_m2_relset_1,axiom, % 0.57/0.67 ! [A,B,C] : % 0.57/0.67 ( m2_relset_1(C,A,B) % 0.57/0.67 <=> m1_relset_1(C,A,B) ) ). % 0.57/0.67 % 0.57/0.67 fof(reflexivity_r1_tarski,axiom, % 0.57/0.67 ! [A,B] : r1_tarski(A,A) ). % 0.57/0.67 % 0.57/0.67 fof(t18_latsubgr,axiom, % 0.57/0.67 ! [A] : % 0.57/0.67 ( ( ~ v3_struct_0(A) % 0.57/0.67 & v3_group_1(A) % 0.57/0.67 & v4_group_1(A) % 0.57/0.67 & l1_group_1(A) ) % 0.57/0.67 => ! [B] : % 0.57/0.67 ( ( v1_group_1(B) % 0.57/0.67 & m1_group_2(B,A) ) % 0.57/0.67 => ! [C] : % 0.57/0.67 ( m1_subset_1(C,u1_struct_0(A)) % 0.57/0.67 => ( r2_hidden(C,k1_funct_1(k1_latsubgr(A),B)) % 0.57/0.67 <=> r1_rlvect_1(B,C) ) ) ) ) ). % 0.57/0.67 % 0.57/0.67 fof(t1_subset,axiom, % 0.57/0.67 ! [A,B] : % 0.57/0.67 ( r2_hidden(A,B) % 0.57/0.67 => m1_subset_1(A,B) ) ). % 0.57/0.67 % 0.57/0.67 fof(t2_subset,axiom, % 0.57/0.67 ! [A,B] : % 0.57/0.67 ( m1_subset_1(A,B) % 0.57/0.67 => ( v1_xboole_0(B) % 0.57/0.67 | r2_hidden(A,B) ) ) ). % 0.57/0.67 % 0.57/0.67 fof(t3_subset,axiom, % 0.57/0.67 ! [A,B] : % 0.57/0.67 ( m1_subset_1(A,k1_zfmisc_1(B)) % 0.57/0.67 <=> r1_tarski(A,B) ) ). % 0.57/0.67 % 0.57/0.67 fof(t4_subset,axiom, % 0.57/0.67 ! [A,B,C] : % 0.57/0.67 ( ( r2_hidden(A,B) % 0.57/0.67 & m1_subset_1(B,k1_zfmisc_1(C)) ) % 0.57/0.67 => m1_subset_1(A,C) ) ). % 0.57/0.67 % 0.57/0.67 fof(t5_subset,axiom, % 0.57/0.67 ! [A,B,C] : % 0.57/0.67 ~ ( r2_hidden(A,B) % 0.57/0.67 & m1_subset_1(B,k1_zfmisc_1(C)) % 0.57/0.67 & v1_xboole_0(C) ) ). % 0.57/0.67 % 0.57/0.67 fof(t60_group_2,axiom, % 0.57/0.67 ! [A] : % 0.57/0.67 ( ( ~ v3_struct_0(A) % 0.57/0.67 & v3_group_1(A) % 0.57/0.67 & v4_group_1(A) % 0.57/0.67 & l1_group_1(A) ) % 0.57/0.67 => ! [B] : % 0.57/0.67 ( m1_subset_1(B,u1_struct_0(A)) % 0.57/0.67 => ! [C] : % 0.57/0.67 ( m1_group_2(C,A) % 0.57/0.67 => ( r1_rlvect_1(C,B) % 0.57/0.67 => r1_rlvect_1(C,k3_group_1(A,B)) ) ) ) ) ). % 0.57/0.67 % 0.57/0.67 fof(t6_boole,axiom, % 0.57/0.67 ! [A] : % 0.57/0.67 ( v1_xboole_0(A) % 0.57/0.67 => A = k1_xboole_0 ) ). % 0.57/0.67 % 0.57/0.67 fof(t7_boole,axiom, % 0.57/0.67 ! [A,B] : % 0.57/0.67 ~ ( r2_hidden(A,B) % 0.57/0.67 & v1_xboole_0(B) ) ). % 0.57/0.67 % 0.57/0.67 fof(t8_boole,axiom, % 0.57/0.67 ! [A,B] : % 0.57/0.67 ~ ( v1_xboole_0(A) % 0.57/0.67 & A != B % 0.57/0.67 & v1_xboole_0(B) ) ). % 0.57/0.67 % 0.57/0.67 %------------------------------------------------------------------------------ % 0.57/0.67 %------------------------------------------- % 0.57/0.67 % Proof found % 0.57/0.67 % SZS status Theorem for theBenchmark % 0.57/0.67 % SZS output start Proof % 0.57/0.67 %ClaNum:135(EqnAxiom:60) % 0.57/0.67 %VarNum:317(SingletonVarNum:111) % 0.57/0.67 %MaxLitNum:9 % 0.57/0.67 %MaxfuncDepth:2 % 0.57/0.67 %SharedTerms:29 % 0.57/0.67 %goalClause: 61 62 63 65 71 73 80 86 90 % 0.57/0.67 %singleGoalClaCount:9 % 0.57/0.67 [61]P1(a1) % 0.57/0.67 [62]P17(a1) % 0.57/0.67 [63]P2(a1) % 0.57/0.67 [64]P2(a10) % 0.57/0.67 [65]P3(a11) % 0.57/0.67 [66]P14(a13) % 0.57/0.67 [67]P14(a2) % 0.57/0.67 [68]P4(a14) % 0.57/0.67 [69]P4(a5) % 0.57/0.67 [71]P5(a11,a1) % 0.57/0.67 [86]~P18(a1) % 0.57/0.67 [87]~P18(a5) % 0.57/0.67 [88]~P14(a8) % 0.57/0.67 [73]P7(a12,f23(a1)) % 0.57/0.67 [80]P12(a12,f19(f18(a1),a11)) % 0.57/0.67 [90]~P12(f25(a1,a12),f19(f18(a1),a11)) % 0.57/0.67 [72]P6(x721,x721) % 0.57/0.67 [70]P14(f6(x701)) % 0.57/0.67 [74]P7(f15(x741),x741) % 0.57/0.67 [75]P7(f6(x751),f24(x751)) % 0.57/0.67 [89]~P14(f24(x891)) % 0.57/0.67 [76]P11(f3(x761,x762)) % 0.57/0.67 [77]P11(f7(x771,x772)) % 0.57/0.67 [78]P15(f3(x781,x782)) % 0.57/0.67 [79]P15(f7(x791,x792)) % 0.57/0.67 [81]P8(f16(x811,x812),x811,x812) % 0.57/0.67 [82]P8(f3(x821,x822),x821,x822) % 0.57/0.67 [83]P8(f7(x831,x832),x831,x832) % 0.57/0.67 [84]P13(f3(x841,x842),x841,x842) % 0.57/0.67 [85]P9(f20(x851,x852),x851,x852) % 0.57/0.67 [91]~P14(x911)+E(x911,a13) % 0.57/0.67 [92]~P2(x921)+P4(x921) % 0.57/0.67 [94]~P2(x941)+P11(f27(x941)) % 0.57/0.67 [95]P14(x951)+~P14(f4(x951)) % 0.57/0.67 [99]P14(x991)+P7(f4(x991),f24(x991)) % 0.57/0.67 [120]~P2(x1201)+P13(f27(x1201),f26(f23(x1201),f23(x1201)),f23(x1201)) % 0.57/0.67 [121]~P2(x1211)+P9(f27(x1211),f26(f23(x1211),f23(x1211)),f23(x1211)) % 0.57/0.67 [98]~P14(x981)+~P12(x982,x981) % 0.57/0.67 [101]~P12(x1011,x1012)+P7(x1011,x1012) % 0.57/0.67 [107]~P12(x1072,x1071)+~P12(x1071,x1072) % 0.57/0.67 [106]~P6(x1061,x1062)+P7(x1061,f24(x1062)) % 0.57/0.67 [110]P6(x1101,x1102)+~P7(x1101,f24(x1102)) % 0.57/0.67 [122]~P9(x1221,x1222,x1223)+P8(x1221,x1222,x1223) % 0.57/0.67 [123]~P8(x1231,x1232,x1233)+P9(x1231,x1232,x1233) % 0.57/0.67 [119]P15(x1191)+~P7(x1191,f24(f26(x1192,x1193))) % 0.57/0.67 [125]~P9(x1251,x1252,x1253)+P7(x1251,f24(f26(x1252,x1253))) % 0.57/0.67 [96]~P4(x961)+P18(x961)+~P14(f23(x961)) % 0.57/0.67 [97]~P4(x971)+P18(x971)+~P14(f9(x971)) % 0.57/0.67 [104]~P2(x1041)+~P3(x1041)+E(f21(f23(x1041),f27(x1041)),x1041) % 0.57/0.67 [112]~P4(x1121)+P18(x1121)+P7(f9(x1121),f24(f23(x1121))) % 0.57/0.67 [93]~P14(x932)+~P14(x931)+E(x931,x932) % 0.57/0.67 [103]~P7(x1032,x1031)+P14(x1031)+P12(x1032,x1031) % 0.57/0.68 [113]P14(x1131)+P14(x1132)+~P14(f26(x1132,x1131)) % 0.57/0.68 [114]~P14(x1141)+~P12(x1142,x1143)+~P7(x1143,f24(x1141)) % 0.57/0.68 [115]P7(x1151,x1152)+~P12(x1151,x1153)+~P7(x1153,f24(x1152)) % 0.57/0.68 [102]~P1(x1021)+~P2(x1021)+P18(x1021)+P5(f17(x1021),x1021) % 0.57/0.68 [132]~P11(x1322)+~P8(x1322,f26(x1321,x1321),x1321)+~P13(x1322,f26(x1321,x1321),x1321)+P2(f21(x1321,x1322)) % 0.57/0.68 [133]~P11(x1332)+~P8(x1332,f26(x1331,x1331),x1331)+~P13(x1332,f26(x1331,x1331),x1331)+P3(f21(x1331,x1332)) % 0.57/0.68 [129]~P11(x1291)+~P8(x1291,x1292,x1293)+~P16(x1291,x1292,x1293)+P13(x1291,x1292,x1293) % 0.57/0.68 [100]~P1(x1001)+~P17(x1001)+~P2(x1001)+P18(x1001)+P11(f18(x1001)) % 0.57/0.68 [105]~P1(x1051)+~P17(x1051)+~P2(x1051)+P18(x1051)+~P14(f22(x1051)) % 0.57/0.68 [117]~P1(x1171)+~P17(x1171)+~P2(x1171)+P18(x1171)+P13(f18(x1171),f22(x1171),f24(f23(x1171))) % 0.57/0.68 [118]~P1(x1181)+~P17(x1181)+~P2(x1181)+P18(x1181)+P9(f18(x1181),f22(x1181),f24(f23(x1181))) % 0.57/0.68 [108]~P1(x1081)+~P2(x1081)+~P5(x1082,x1081)+P18(x1081)+P1(x1082) % 0.57/0.68 [109]~P1(x1091)+~P2(x1091)+~P5(x1092,x1091)+P18(x1091)+P2(x1092) % 0.57/0.68 [111]~P1(x1111)+~P2(x1111)+~P5(x1112,x1111)+P18(x1111)+~P18(x1112) % 0.57/0.68 [130]~P11(x1302)+~P8(x1302,x1303,x1301)+~P13(x1302,x1303,x1301)+P14(x1301)+P16(x1302,x1303,x1301) % 0.57/0.68 [134]~P11(x1341)+E(x1341,x1342)+~P8(x1341,f26(x1343,x1343),x1343)+~P13(x1341,f26(x1343,x1343),x1343)+~E(f21(x1343,x1341),f21(x1344,x1342)) % 0.57/0.68 [135]~P11(x1353)+E(x1351,x1352)+~P8(x1353,f26(x1351,x1351),x1351)+~P13(x1353,f26(x1351,x1351),x1351)+~E(f21(x1351,x1353),f21(x1352,x1354)) % 0.57/0.68 [116]~P1(x1161)+~P17(x1161)+~P2(x1161)+P18(x1161)+~P7(x1162,f23(x1161))+P7(f25(x1161,x1162),f23(x1161)) % 0.57/0.68 [128]~P14(x1283)+~P8(x1283,x1282,x1281)+~P13(x1283,x1282,x1281)+P14(x1281)+P14(x1282)+~P11(x1283) % 0.57/0.68 [124]~P1(x1241)+~P17(x1241)+~P2(x1241)+~P5(x1242,x1241)+~P10(x1242,x1243)+P18(x1241)+~P7(x1243,f23(x1241))+P10(x1242,f25(x1241,x1243)) % 0.57/0.68 [126]~P1(x1261)+~P17(x1261)+~P2(x1261)+~P3(x1263)+~P5(x1263,x1261)+~P10(x1263,x1262)+P18(x1261)+~P7(x1262,f23(x1261))+P12(x1262,f19(f18(x1261),x1263)) % 0.57/0.68 [127]~P1(x1271)+~P17(x1271)+~P2(x1271)+~P3(x1272)+~P5(x1272,x1271)+P18(x1271)+P10(x1272,x1273)+~P7(x1273,f23(x1271))+~P12(x1273,f19(f18(x1271),x1272)) % 0.57/0.68 %EqnAxiom % 0.57/0.68 [1]E(x11,x11) % 0.57/0.68 [2]E(x22,x21)+~E(x21,x22) % 0.57/0.68 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.57/0.68 [4]~E(x41,x42)+E(f6(x41),f6(x42)) % 0.57/0.68 [5]~E(x51,x52)+E(f23(x51),f23(x52)) % 0.57/0.68 [6]~E(x61,x62)+E(f15(x61),f15(x62)) % 0.57/0.68 [7]~E(x71,x72)+E(f26(x71,x73),f26(x72,x73)) % 0.57/0.68 [8]~E(x81,x82)+E(f26(x83,x81),f26(x83,x82)) % 0.57/0.68 [9]~E(x91,x92)+E(f24(x91),f24(x92)) % 0.57/0.68 [10]~E(x101,x102)+E(f3(x101,x103),f3(x102,x103)) % 0.57/0.68 [11]~E(x111,x112)+E(f3(x113,x111),f3(x113,x112)) % 0.57/0.68 [12]~E(x121,x122)+E(f7(x121,x123),f7(x122,x123)) % 0.57/0.68 [13]~E(x131,x132)+E(f7(x133,x131),f7(x133,x132)) % 0.57/0.68 [14]~E(x141,x142)+E(f18(x141),f18(x142)) % 0.57/0.68 [15]~E(x151,x152)+E(f25(x151,x153),f25(x152,x153)) % 0.57/0.68 [16]~E(x161,x162)+E(f25(x163,x161),f25(x163,x162)) % 0.57/0.68 [17]~E(x171,x172)+E(f21(x171,x173),f21(x172,x173)) % 0.57/0.68 [18]~E(x181,x182)+E(f21(x183,x181),f21(x183,x182)) % 0.57/0.68 [19]~E(x191,x192)+E(f19(x191,x193),f19(x192,x193)) % 0.57/0.68 [20]~E(x201,x202)+E(f19(x203,x201),f19(x203,x202)) % 0.57/0.68 [21]~E(x211,x212)+E(f16(x211,x213),f16(x212,x213)) % 0.57/0.68 [22]~E(x221,x222)+E(f16(x223,x221),f16(x223,x222)) % 0.57/0.68 [23]~E(x231,x232)+E(f9(x231),f9(x232)) % 0.57/0.68 [24]~E(x241,x242)+E(f22(x241),f22(x242)) % 0.57/0.68 [25]~E(x251,x252)+E(f4(x251),f4(x252)) % 0.57/0.68 [26]~E(x261,x262)+E(f20(x261,x263),f20(x262,x263)) % 0.57/0.68 [27]~E(x271,x272)+E(f20(x273,x271),f20(x273,x272)) % 0.57/0.68 [28]~E(x281,x282)+E(f27(x281),f27(x282)) % 0.57/0.68 [29]~E(x291,x292)+E(f17(x291),f17(x292)) % 0.57/0.68 [30]~P1(x301)+P1(x302)+~E(x301,x302) % 0.57/0.68 [31]~P17(x311)+P17(x312)+~E(x311,x312) % 0.57/0.68 [32]~P2(x321)+P2(x322)+~E(x321,x322) % 0.57/0.68 [33]P8(x332,x333,x334)+~E(x331,x332)+~P8(x331,x333,x334) % 0.57/0.68 [34]P8(x343,x342,x344)+~E(x341,x342)+~P8(x343,x341,x344) % 0.57/0.68 [35]P8(x353,x354,x352)+~E(x351,x352)+~P8(x353,x354,x351) % 0.57/0.68 [36]~P3(x361)+P3(x362)+~E(x361,x362) % 0.57/0.68 [37]~P14(x371)+P14(x372)+~E(x371,x372) % 0.57/0.68 [38]P5(x382,x383)+~E(x381,x382)+~P5(x381,x383) % 0.57/0.68 [39]P5(x393,x392)+~E(x391,x392)+~P5(x393,x391) % 0.57/0.68 [40]~P4(x401)+P4(x402)+~E(x401,x402) % 0.57/0.68 [41]P7(x412,x413)+~E(x411,x412)+~P7(x411,x413) % 0.57/0.68 [42]P7(x423,x422)+~E(x421,x422)+~P7(x423,x421) % 0.57/0.68 [43]P10(x432,x433)+~E(x431,x432)+~P10(x431,x433) % 0.57/0.68 [44]P10(x443,x442)+~E(x441,x442)+~P10(x443,x441) % 0.57/0.68 [45]~P18(x451)+P18(x452)+~E(x451,x452) % 0.57/0.68 [46]P6(x462,x463)+~E(x461,x462)+~P6(x461,x463) % 0.57/0.68 [47]P6(x473,x472)+~E(x471,x472)+~P6(x473,x471) % 0.57/0.68 [48]~P11(x481)+P11(x482)+~E(x481,x482) % 0.57/0.68 [49]P13(x492,x493,x494)+~E(x491,x492)+~P13(x491,x493,x494) % 0.57/0.68 [50]P13(x503,x502,x504)+~E(x501,x502)+~P13(x503,x501,x504) % 0.57/0.68 [51]P13(x513,x514,x512)+~E(x511,x512)+~P13(x513,x514,x511) % 0.57/0.68 [52]P9(x522,x523,x524)+~E(x521,x522)+~P9(x521,x523,x524) % 0.57/0.68 [53]P9(x533,x532,x534)+~E(x531,x532)+~P9(x533,x531,x534) % 0.57/0.68 [54]P9(x543,x544,x542)+~E(x541,x542)+~P9(x543,x544,x541) % 0.57/0.68 [55]~P15(x551)+P15(x552)+~E(x551,x552) % 0.57/0.68 [56]P12(x562,x563)+~E(x561,x562)+~P12(x561,x563) % 0.57/0.68 [57]P12(x573,x572)+~E(x571,x572)+~P12(x573,x571) % 0.57/0.68 [58]P16(x582,x583,x584)+~E(x581,x582)+~P16(x581,x583,x584) % 0.57/0.68 [59]P16(x593,x592,x594)+~E(x591,x592)+~P16(x593,x591,x594) % 0.57/0.68 [60]P16(x603,x604,x602)+~E(x601,x602)+~P16(x603,x604,x601) % 0.57/0.68 % 0.57/0.68 %------------------------------------------- % 0.57/0.68 cnf(143,plain, % 0.57/0.68 (P7(f15(x1431),x1431)), % 0.57/0.68 inference(rename_variables,[],[74])). % 0.57/0.68 cnf(148,plain, % 0.57/0.68 (P12(f15(a8),a8)), % 0.57/0.68 inference(scs_inference,[],[80,74,143,75,66,88,98,107,110,119,103])). % 0.57/0.68 cnf(149,plain, % 0.57/0.68 (P7(f15(x1491),x1491)), % 0.57/0.68 inference(rename_variables,[],[74])). % 0.57/0.68 cnf(151,plain, % 0.57/0.68 (~P12(x1511,f15(f24(a13)))), % 0.57/0.68 inference(scs_inference,[],[80,74,143,149,75,66,88,98,107,110,119,103,114])). % 0.57/0.68 cnf(152,plain, % 0.57/0.68 (P7(f15(x1521),x1521)), % 0.57/0.68 inference(rename_variables,[],[74])). % 0.57/0.68 cnf(156,plain, % 0.57/0.68 (~P14(f19(f18(a1),a11))), % 0.57/0.68 inference(scs_inference,[],[90,80,74,143,149,75,66,88,98,107,110,119,103,114,56,57,93])). % 0.57/0.68 cnf(165,plain, % 0.57/0.68 (P13(f3(x1651,x1652),x1651,x1652)), % 0.57/0.68 inference(rename_variables,[],[84])). % 0.57/0.68 cnf(166,plain, % 0.57/0.68 (P11(f3(x1661,x1662))), % 0.57/0.68 inference(rename_variables,[],[76])). % 0.57/0.68 cnf(167,plain, % 0.57/0.68 (P8(f3(x1671,x1672),x1671,x1672)), % 0.57/0.68 inference(rename_variables,[],[82])). % 0.57/0.68 cnf(169,plain, % 0.57/0.68 (~P14(f3(a8,a8))), % 0.57/0.68 inference(scs_inference,[],[61,63,71,86,90,80,74,143,149,82,167,84,165,75,66,88,76,166,98,107,110,119,103,114,56,57,93,108,109,111,130,128])). % 0.57/0.68 cnf(179,plain, % 0.57/0.68 (P10(a11,f25(a1,a12))), % 0.57/0.68 inference(scs_inference,[],[61,62,63,65,71,86,73,90,80,74,143,149,152,82,167,84,165,75,66,88,76,166,98,107,110,119,103,114,56,57,93,108,109,111,130,128,127,115,124])). % 0.57/0.68 cnf(189,plain, % 0.57/0.68 (~P12(x1891,f15(f24(a2)))), % 0.57/0.68 inference(scs_inference,[],[148,74,67,75,110,98,107,114])). % 0.57/0.68 cnf(196,plain, % 0.57/0.68 (~P7(f25(a1,a12),f23(a1))), % 0.57/0.68 inference(scs_inference,[],[61,65,90,62,80,63,86,71,151,179,148,156,74,67,75,110,98,107,114,57,103,126])). % 0.57/0.68 cnf(221,plain, % 0.57/0.68 (P13(f3(x2211,x2212),x2211,x2212)), % 0.57/0.68 inference(rename_variables,[],[84])). % 0.57/0.68 cnf(222,plain, % 0.57/0.68 (P11(f3(x2221,x2222))), % 0.57/0.68 inference(rename_variables,[],[76])). % 0.57/0.68 cnf(223,plain, % 0.57/0.68 (P8(f3(x2231,x2232),x2231,x2232)), % 0.57/0.68 inference(rename_variables,[],[82])). % 0.57/0.68 cnf(230,plain, % 0.57/0.68 ($false), % 0.57/0.68 inference(scs_inference,[],[61,63,73,80,62,86,189,196,169,74,70,82,223,84,221,76,222,98,103,57,130,128,116]), % 0.57/0.68 ['proof']). % 0.57/0.68 % SZS output end Proof % 0.57/0.68 % Total time :0.030000s %------------------------------------------------------------------------------