%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : GRP643+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 : n020.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 58.78s 58.80s % Output : CNFRefutation 58.78s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.15 % Problem : GRP643+1 : TPTP v8.2.0. Released v3.4.0. % 0.04/0.15 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.14/0.37 % Computer : n020.cluster.edu % 0.14/0.37 % Model : x86_64 x86_64 % 0.14/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.37 % Memory : 8042.1875MB % 0.14/0.37 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.37 % CPULimit : 300 % 0.14/0.37 % WCLimit : 300 % 0.14/0.37 % DateTime : Thu Jun 20 09:24:24 EDT 2024 % 0.14/0.37 % CPUTime : % 0.57/0.66 start to proof:theBenchmark % 58.68/58.77 %------------------------------------------- % 58.68/58.77 % File :CSE---1.7 % 58.68/58.77 % Problem :theBenchmark % 58.68/58.77 % Transform :cnf % 58.68/58.77 % Format :tptp:raw % 58.68/58.77 % Command :java -jar mcs_scs.jar %d %s % 58.68/58.77 % 58.68/58.77 % Result :Theorem 58.040000s % 58.68/58.77 % Output :CNFRefutation 58.040000s % 58.68/58.77 %------------------------------------------- % 58.68/58.78 %------------------------------------------------------------------------------ % 58.68/58.78 % File : GRP643+1 : TPTP v8.2.0. Released v3.4.0. % 58.68/58.78 % Domain : Group Theory % 58.68/58.78 % Problem : On the Lattice of Subgroups of a Group T21 % 58.68/58.78 % Version : [Urb08] axioms : Especial. % 58.68/58.78 % English : % 58.68/58.78 % 58.68/58.78 % Refs : [Gan96] Ganczarski (1996), On the Lattice of Subgroups of a Gr % 58.68/58.78 % : [Urb07] Urban (2007), MPTP 0.2: Design, Implementation, and In % 58.68/58.78 % : [Urb08] Urban (2006), Email to G. Sutcliffe % 58.68/58.78 % Source : [Urb08] % 58.68/58.78 % Names : t21_latsubgr [Urb08] % 58.68/58.78 % 58.68/58.78 % Status : Theorem % 58.68/58.78 % Rating : 0.19 v8.1.0, 0.08 v7.5.0, 0.12 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.1.0, 0.17 v5.5.0, 0.15 v5.4.0, 0.25 v5.3.0, 0.30 v5.2.0, 0.10 v5.1.0, 0.14 v5.0.0, 0.21 v4.1.0, 0.26 v4.0.1, 0.30 v4.0.0, 0.33 v3.7.0, 0.30 v3.5.0, 0.32 v3.4.0 % 58.68/58.78 % Syntax : Number of formulae : 55 ( 19 unt; 0 def) % 58.68/58.78 % Number of atoms : 170 ( 6 equ) % 58.68/58.78 % Maximal formula atoms : 11 ( 3 avg) % 58.68/58.78 % Number of connectives : 146 ( 31 ~; 1 |; 66 &) % 58.68/58.78 % ( 3 <=>; 45 =>; 0 <=; 0 <~>) % 58.68/58.78 % Maximal formula depth : 11 ( 5 avg) % 58.68/58.78 % Maximal term depth : 3 ( 1 avg) % 58.68/58.78 % Number of predicates : 20 ( 18 usr; 1 prp; 0-3 aty) % 58.68/58.78 % Number of functors : 10 ( 10 usr; 1 con; 0-3 aty) % 58.68/58.78 % Number of variables : 97 ( 83 !; 14 ?) % 58.68/58.78 % SPC : FOF_THM_RFO_SEQ % 58.68/58.78 % 58.68/58.78 % Comments : Normal version: includes the axioms (which may be theorems from % 58.68/58.78 % other articles) and background that are possibly necessary. % 58.68/58.78 % : Translated by MPTP from the Mizar Mathematical Library 4.48.930. % 58.68/58.78 % : The problem encoding is based on set theory. % 58.68/58.78 %------------------------------------------------------------------------------ % 58.68/58.78 fof(t21_latsubgr,conjecture, % 58.68/58.78 ! [A] : % 58.68/58.78 ( ( ~ v3_struct_0(A) % 58.68/58.78 & v3_group_1(A) % 58.68/58.78 & v4_group_1(A) % 58.68/58.78 & l1_group_1(A) ) % 58.68/58.78 => ! [B] : % 58.68/58.78 ( ( v1_group_1(B) % 58.68/58.78 & m1_group_2(B,A) ) % 58.68/58.78 => ! [C] : % 58.68/58.78 ( m1_subset_1(C,u1_struct_0(A)) % 58.68/58.79 => ! [D] : % 58.68/58.79 ( m1_subset_1(D,u1_struct_0(A)) % 58.68/58.79 => ( ( r2_hidden(C,k1_funct_1(k1_latsubgr(A),B)) % 58.68/58.79 & r2_hidden(D,k1_funct_1(k1_latsubgr(A),B)) ) % 58.68/58.79 => r2_hidden(k1_group_1(A,C,D),k1_funct_1(k1_latsubgr(A),B)) ) ) ) ) ) ). % 58.68/58.79 % 58.68/58.79 fof(abstractness_v1_group_1,axiom, % 58.68/58.79 ! [A] : % 58.68/58.79 ( l1_group_1(A) % 58.68/58.79 => ( v1_group_1(A) % 58.68/58.79 => A = g1_group_1(u1_struct_0(A),u1_group_1(A)) ) ) ). % 58.68/58.79 % 58.68/58.79 fof(antisymmetry_r2_hidden,axiom, % 58.68/58.79 ! [A,B] : % 58.68/58.79 ( r2_hidden(A,B) % 58.68/58.79 => ~ r2_hidden(B,A) ) ). % 58.68/58.79 % 58.68/58.79 fof(cc1_funct_2,axiom, % 58.68/58.79 ! [A,B,C] : % 58.68/58.79 ( m1_relset_1(C,A,B) % 58.68/58.79 => ( ( v1_funct_1(C) % 58.68/58.79 & v1_partfun1(C,A,B) ) % 58.68/58.79 => ( v1_funct_1(C) % 58.68/58.79 & v1_funct_2(C,A,B) ) ) ) ). % 58.68/58.79 % 58.68/58.79 fof(cc1_relset_1,axiom, % 58.68/58.79 ! [A,B,C] : % 58.68/58.79 ( m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))) % 58.68/58.79 => v1_relat_1(C) ) ). % 58.68/58.79 % 58.68/58.79 fof(cc5_funct_2,axiom, % 58.68/58.79 ! [A,B] : % 58.68/58.79 ( ~ v1_xboole_0(B) % 58.68/58.79 => ! [C] : % 58.68/58.79 ( m1_relset_1(C,A,B) % 58.68/58.79 => ( ( v1_funct_1(C) % 58.68/58.79 & v1_funct_2(C,A,B) ) % 58.68/58.79 => ( v1_funct_1(C) % 58.68/58.79 & v1_partfun1(C,A,B) % 58.68/58.79 & v1_funct_2(C,A,B) ) ) ) ) ). % 58.68/58.79 % 58.78/58.79 fof(cc6_funct_2,axiom, % 58.78/58.79 ! [A,B] : % 58.78/58.79 ( ( ~ v1_xboole_0(A) % 58.78/58.79 & ~ v1_xboole_0(B) ) % 58.78/58.79 => ! [C] : % 58.78/58.79 ( m1_relset_1(C,A,B) % 58.78/58.79 => ( ( v1_funct_1(C) % 58.78/58.79 & v1_funct_2(C,A,B) ) % 58.78/58.79 => ( v1_funct_1(C) % 58.78/58.79 & ~ v1_xboole_0(C) % 58.78/58.79 & v1_partfun1(C,A,B) % 58.78/58.79 & v1_funct_2(C,A,B) ) ) ) ) ). % 58.78/58.79 % 58.78/58.79 fof(dt_g1_group_1,axiom, % 58.78/58.79 ! [A,B] : % 58.78/58.79 ( ( v1_funct_1(B) % 58.78/58.79 & v1_funct_2(B,k2_zfmisc_1(A,A),A) % 58.78/58.79 & m1_relset_1(B,k2_zfmisc_1(A,A),A) ) % 58.78/58.79 => ( v1_group_1(g1_group_1(A,B)) % 58.78/58.79 & l1_group_1(g1_group_1(A,B)) ) ) ). % 58.78/58.79 % 58.78/58.79 fof(dt_k1_funct_1,axiom, % 58.78/58.79 $true ). % 58.78/58.79 % 58.78/58.79 fof(dt_k1_group_1,axiom, % 58.78/58.79 ! [A,B,C] : % 58.78/58.79 ( ( ~ v3_struct_0(A) % 58.78/58.79 & l1_group_1(A) % 58.78/58.79 & m1_subset_1(B,u1_struct_0(A)) % 58.78/58.79 & m1_subset_1(C,u1_struct_0(A)) ) % 58.78/58.79 => m1_subset_1(k1_group_1(A,B,C),u1_struct_0(A)) ) ). % 58.78/58.79 % 58.78/58.79 fof(dt_k1_group_3,axiom, % 58.78/58.79 $true ). % 58.78/58.79 % 58.78/58.79 fof(dt_k1_latsubgr,axiom, % 58.78/58.79 ! [A] : % 58.78/58.79 ( ( ~ v3_struct_0(A) % 58.78/58.79 & v3_group_1(A) % 58.78/58.79 & v4_group_1(A) % 58.78/58.79 & l1_group_1(A) ) % 58.78/58.79 => ( v1_funct_1(k1_latsubgr(A)) % 58.78/58.79 & v1_funct_2(k1_latsubgr(A),k1_group_3(A),k1_zfmisc_1(u1_struct_0(A))) % 58.78/58.79 & m2_relset_1(k1_latsubgr(A),k1_group_3(A),k1_zfmisc_1(u1_struct_0(A))) ) ) ). % 58.78/58.79 % 58.78/58.79 fof(dt_k1_xboole_0,axiom, % 58.78/58.79 $true ). % 58.78/58.79 % 58.78/58.79 fof(dt_k1_zfmisc_1,axiom, % 58.78/58.79 $true ). % 58.78/58.79 % 58.78/58.79 fof(dt_k2_zfmisc_1,axiom, % 58.78/58.79 $true ). % 58.78/58.79 % 58.78/58.79 fof(dt_l1_group_1,axiom, % 58.78/58.79 ! [A] : % 58.78/58.79 ( l1_group_1(A) % 58.78/58.79 => l1_struct_0(A) ) ). % 58.78/58.79 % 58.78/58.79 fof(dt_l1_struct_0,axiom, % 58.78/58.79 $true ). % 58.78/58.79 % 58.78/58.79 fof(dt_m1_group_2,axiom, % 58.78/58.79 ! [A] : % 58.78/58.79 ( ( ~ v3_struct_0(A) % 58.78/58.79 & v3_group_1(A) % 58.78/58.79 & l1_group_1(A) ) % 58.78/58.79 => ! [B] : % 58.78/58.79 ( m1_group_2(B,A) % 58.78/58.79 => ( ~ v3_struct_0(B) % 58.78/58.79 & v3_group_1(B) % 58.78/58.79 & l1_group_1(B) ) ) ) ). % 58.78/58.79 % 58.78/58.79 fof(dt_m1_relset_1,axiom, % 58.78/58.79 $true ). % 58.78/58.79 % 58.78/58.79 fof(dt_m1_subset_1,axiom, % 58.78/58.79 $true ). % 58.78/58.79 % 58.78/58.79 fof(dt_m2_relset_1,axiom, % 58.78/58.79 ! [A,B,C] : % 58.78/58.79 ( m2_relset_1(C,A,B) % 58.78/58.79 => m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))) ) ). % 58.78/58.79 % 58.78/58.79 fof(dt_u1_group_1,axiom, % 58.78/58.79 ! [A] : % 58.78/58.79 ( l1_group_1(A) % 58.78/58.79 => ( v1_funct_1(u1_group_1(A)) % 58.78/58.79 & v1_funct_2(u1_group_1(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A)) % 58.78/58.79 & m2_relset_1(u1_group_1(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A)) ) ) ). % 58.78/58.79 % 58.78/58.79 fof(dt_u1_struct_0,axiom, % 58.78/58.79 $true ). % 58.78/58.79 % 58.78/58.79 fof(existence_l1_group_1,axiom, % 58.78/58.79 ? [A] : l1_group_1(A) ). % 58.78/58.79 % 58.78/58.79 fof(existence_l1_struct_0,axiom, % 58.78/58.79 ? [A] : l1_struct_0(A) ). % 58.78/58.79 % 58.78/58.79 fof(existence_m1_group_2,axiom, % 58.78/58.79 ! [A] : % 58.78/58.79 ( ( ~ v3_struct_0(A) % 58.78/58.79 & v3_group_1(A) % 58.78/58.79 & l1_group_1(A) ) % 58.78/58.79 => ? [B] : m1_group_2(B,A) ) ). % 58.78/58.79 % 58.78/58.79 fof(existence_m1_relset_1,axiom, % 58.78/58.79 ! [A,B] : % 58.78/58.79 ? [C] : m1_relset_1(C,A,B) ). % 58.78/58.79 % 58.78/58.79 fof(existence_m1_subset_1,axiom, % 58.78/58.79 ! [A] : % 58.78/58.79 ? [B] : m1_subset_1(B,A) ). % 58.78/58.79 % 58.78/58.79 fof(existence_m2_relset_1,axiom, % 58.78/58.79 ! [A,B] : % 58.78/58.79 ? [C] : m2_relset_1(C,A,B) ). % 58.78/58.79 % 58.78/58.79 fof(fc1_group_3,axiom, % 58.78/58.79 ! [A] : % 58.78/58.79 ( ( ~ v3_struct_0(A) % 58.78/58.79 & v3_group_1(A) % 58.78/58.79 & v4_group_1(A) % 58.78/58.79 & l1_group_1(A) ) % 58.78/58.79 => ~ v1_xboole_0(k1_group_3(A)) ) ). % 58.78/58.79 % 58.78/58.79 fof(fc1_struct_0,axiom, % 58.78/58.79 ! [A] : % 58.78/58.79 ( ( ~ v3_struct_0(A) % 58.78/58.79 & l1_struct_0(A) ) % 58.78/58.79 => ~ v1_xboole_0(u1_struct_0(A)) ) ). % 58.78/58.79 % 58.78/58.79 fof(fc1_subset_1,axiom, % 58.78/58.79 ! [A] : ~ v1_xboole_0(k1_zfmisc_1(A)) ). % 58.78/58.79 % 58.78/58.79 fof(fc1_xboole_0,axiom, % 58.78/58.79 v1_xboole_0(k1_xboole_0) ). % 58.78/58.79 % 58.78/58.79 fof(fc4_subset_1,axiom, % 58.78/58.79 ! [A,B] : % 58.78/58.79 ( ( ~ v1_xboole_0(A) % 58.78/58.79 & ~ v1_xboole_0(B) ) % 58.78/58.79 => ~ v1_xboole_0(k2_zfmisc_1(A,B)) ) ). % 58.78/58.79 % 58.78/58.79 fof(free_g1_group_1,axiom, % 58.78/58.79 ! [A,B] : % 58.78/58.79 ( ( v1_funct_1(B) % 58.78/58.79 & v1_funct_2(B,k2_zfmisc_1(A,A),A) % 58.78/58.79 & m1_relset_1(B,k2_zfmisc_1(A,A),A) ) % 58.78/58.79 => ! [C,D] : % 58.78/58.79 ( g1_group_1(A,B) = g1_group_1(C,D) % 58.78/58.79 => ( A = C % 58.78/58.79 & B = D ) ) ) ). % 58.78/58.79 % 58.78/58.79 fof(rc1_funct_2,axiom, % 58.78/58.79 ! [A,B] : % 58.78/58.79 ? [C] : % 58.78/58.79 ( m1_relset_1(C,A,B) % 58.78/58.79 & v1_relat_1(C) % 58.78/58.79 & v1_funct_1(C) % 58.78/58.79 & v1_funct_2(C,A,B) ) ). % 58.78/58.79 % 58.78/58.79 fof(rc1_subset_1,axiom, % 58.78/58.79 ! [A] : % 58.78/58.79 ( ~ v1_xboole_0(A) % 58.78/58.79 => ? [B] : % 58.78/58.79 ( m1_subset_1(B,k1_zfmisc_1(A)) % 58.78/58.79 & ~ v1_xboole_0(B) ) ) ). % 58.78/58.79 % 58.78/58.79 fof(rc1_xboole_0,axiom, % 58.78/58.79 ? [A] : v1_xboole_0(A) ). % 58.78/58.79 % 58.78/58.79 fof(rc2_partfun1,axiom, % 58.78/58.79 ! [A,B] : % 58.78/58.79 ? [C] : % 58.78/58.79 ( m1_relset_1(C,A,B) % 58.78/58.79 & v1_relat_1(C) % 58.78/58.79 & v1_funct_1(C) ) ). % 58.78/58.79 % 58.78/58.79 fof(rc2_subset_1,axiom, % 58.78/58.79 ! [A] : % 58.78/58.79 ? [B] : % 58.78/58.79 ( m1_subset_1(B,k1_zfmisc_1(A)) % 58.78/58.79 & v1_xboole_0(B) ) ). % 58.78/58.79 % 58.78/58.79 fof(rc2_xboole_0,axiom, % 58.78/58.79 ? [A] : ~ v1_xboole_0(A) ). % 58.78/58.79 % 58.78/58.79 fof(rc3_struct_0,axiom, % 58.78/58.79 ? [A] : % 58.78/58.79 ( l1_struct_0(A) % 58.78/58.79 & ~ v3_struct_0(A) ) ). % 58.78/58.79 % 58.78/58.79 fof(rc5_struct_0,axiom, % 58.78/58.79 ! [A] : % 58.78/58.79 ( ( ~ v3_struct_0(A) % 58.78/58.79 & l1_struct_0(A) ) % 58.78/58.79 => ? [B] : % 58.78/58.79 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 58.78/58.79 & ~ v1_xboole_0(B) ) ) ). % 58.78/58.79 % 58.78/58.79 fof(redefinition_m2_relset_1,axiom, % 58.78/58.79 ! [A,B,C] : % 58.78/58.79 ( m2_relset_1(C,A,B) % 58.78/58.79 <=> m1_relset_1(C,A,B) ) ). % 58.78/58.79 % 58.78/58.79 fof(reflexivity_r1_tarski,axiom, % 58.78/58.79 ! [A,B] : r1_tarski(A,A) ). % 58.78/58.79 % 58.78/58.79 fof(t18_latsubgr,axiom, % 58.78/58.79 ! [A] : % 58.78/58.79 ( ( ~ v3_struct_0(A) % 58.78/58.79 & v3_group_1(A) % 58.78/58.80 & v4_group_1(A) % 58.78/58.80 & l1_group_1(A) ) % 58.78/58.80 => ! [B] : % 58.78/58.80 ( ( v1_group_1(B) % 58.78/58.80 & m1_group_2(B,A) ) % 58.78/58.80 => ! [C] : % 58.78/58.80 ( m1_subset_1(C,u1_struct_0(A)) % 58.78/58.80 => ( r2_hidden(C,k1_funct_1(k1_latsubgr(A),B)) % 58.78/58.80 <=> r1_rlvect_1(B,C) ) ) ) ) ). % 58.78/58.80 % 58.78/58.80 fof(t1_subset,axiom, % 58.78/58.80 ! [A,B] : % 58.78/58.80 ( r2_hidden(A,B) % 58.78/58.80 => m1_subset_1(A,B) ) ). % 58.78/58.80 % 58.78/58.80 fof(t2_subset,axiom, % 58.78/58.80 ! [A,B] : % 58.78/58.80 ( m1_subset_1(A,B) % 58.78/58.80 => ( v1_xboole_0(B) % 58.78/58.80 | r2_hidden(A,B) ) ) ). % 58.78/58.80 % 58.78/58.80 fof(t3_subset,axiom, % 58.78/58.80 ! [A,B] : % 58.78/58.80 ( m1_subset_1(A,k1_zfmisc_1(B)) % 58.78/58.80 <=> r1_tarski(A,B) ) ). % 58.78/58.80 % 58.78/58.80 fof(t4_subset,axiom, % 58.78/58.80 ! [A,B,C] : % 58.78/58.80 ( ( r2_hidden(A,B) % 58.78/58.80 & m1_subset_1(B,k1_zfmisc_1(C)) ) % 58.78/58.80 => m1_subset_1(A,C) ) ). % 58.78/58.80 % 58.78/58.80 fof(t59_group_2,axiom, % 58.78/58.80 ! [A] : % 58.78/58.80 ( ( ~ v3_struct_0(A) % 58.78/58.80 & v3_group_1(A) % 58.78/58.80 & v4_group_1(A) % 58.78/58.80 & l1_group_1(A) ) % 58.78/58.80 => ! [B] : % 58.78/58.80 ( m1_subset_1(B,u1_struct_0(A)) % 58.78/58.80 => ! [C] : % 58.78/58.80 ( m1_subset_1(C,u1_struct_0(A)) % 58.78/58.80 => ! [D] : % 58.78/58.80 ( m1_group_2(D,A) % 58.78/58.80 => ( ( r1_rlvect_1(D,B) % 58.78/58.80 & r1_rlvect_1(D,C) ) % 58.78/58.80 => r1_rlvect_1(D,k1_group_1(A,B,C)) ) ) ) ) ) ). % 58.78/58.80 % 58.78/58.80 fof(t5_subset,axiom, % 58.78/58.80 ! [A,B,C] : % 58.78/58.80 ~ ( r2_hidden(A,B) % 58.78/58.80 & m1_subset_1(B,k1_zfmisc_1(C)) % 58.78/58.80 & v1_xboole_0(C) ) ). % 58.78/58.80 % 58.78/58.80 fof(t6_boole,axiom, % 58.78/58.80 ! [A] : % 58.78/58.80 ( v1_xboole_0(A) % 58.78/58.80 => A = k1_xboole_0 ) ). % 58.78/58.80 % 58.78/58.80 fof(t7_boole,axiom, % 58.78/58.80 ! [A,B] : % 58.78/58.80 ~ ( r2_hidden(A,B) % 58.78/58.80 & v1_xboole_0(B) ) ). % 58.78/58.80 % 58.78/58.80 fof(t8_boole,axiom, % 58.78/58.80 ! [A,B] : % 58.78/58.80 ~ ( v1_xboole_0(A) % 58.78/58.80 & A != B % 58.78/58.80 & v1_xboole_0(B) ) ). % 58.78/58.80 % 58.78/58.80 %------------------------------------------------------------------------------ % 58.78/58.80 %------------------------------------------- % 58.78/58.80 % Proof found % 58.78/58.80 % SZS status Theorem for theBenchmark % 58.78/58.80 % SZS output start Proof % 58.78/58.80 %ClaNum:138(EqnAxiom:61) % 58.78/58.80 %VarNum:323(SingletonVarNum:113) % 58.78/58.80 %MaxLitNum:10 % 58.78/58.80 %MaxfuncDepth:2 % 58.78/58.80 %SharedTerms:32 % 58.78/58.80 %goalClause: 62 63 64 66 72 74 75 82 83 89 93 % 58.78/58.80 %singleGoalClaCount:11 % 58.78/58.80 [62]P1(a1) % 58.78/58.80 [63]P17(a1) % 58.78/58.80 [64]P2(a1) % 58.78/58.80 [65]P2(a11) % 58.78/58.80 [66]P3(a12) % 58.78/58.80 [67]P14(a15) % 58.78/58.80 [68]P14(a2) % 58.78/58.80 [69]P4(a16) % 58.78/58.80 [70]P4(a6) % 58.78/58.80 [72]P5(a12,a1) % 58.78/58.80 [89]~P18(a1) % 58.78/58.80 [90]~P18(a6) % 58.78/58.80 [91]~P14(a9) % 58.78/58.80 [74]P7(a13,f25(a1)) % 58.78/58.80 [75]P7(a14,f25(a1)) % 58.78/58.80 [82]P12(a13,f21(f20(a1),a12)) % 58.78/58.80 [83]P12(a14,f21(f20(a1),a12)) % 58.78/58.80 [93]~P12(f23(a1,a13,a14),f21(f20(a1),a12)) % 58.78/58.80 [73]P6(x731,x731) % 58.78/58.80 [71]P14(f7(x711)) % 58.78/58.80 [76]P7(f17(x761),x761) % 58.78/58.80 [77]P7(f7(x771),f26(x771)) % 58.78/58.80 [92]~P14(f26(x921)) % 58.78/58.80 [78]P11(f3(x781,x782)) % 58.78/58.80 [79]P11(f8(x791,x792)) % 58.78/58.80 [80]P15(f3(x801,x802)) % 58.78/58.80 [81]P15(f8(x811,x812)) % 58.78/58.80 [84]P8(f18(x841,x842),x841,x842) % 58.78/58.80 [85]P8(f3(x851,x852),x851,x852) % 58.78/58.80 [86]P8(f8(x861,x862),x861,x862) % 58.78/58.80 [87]P13(f3(x871,x872),x871,x872) % 58.78/58.80 [88]P9(f4(x881,x882),x881,x882) % 58.78/58.80 [94]~P14(x941)+E(x941,a15) % 58.78/58.80 [95]~P2(x951)+P4(x951) % 58.78/58.80 [97]~P2(x971)+P11(f27(x971)) % 58.78/58.80 [98]P14(x981)+~P14(f5(x981)) % 58.78/58.80 [102]P14(x1021)+P7(f5(x1021),f26(x1021)) % 58.78/58.80 [122]~P2(x1221)+P13(f27(x1221),f28(f25(x1221),f25(x1221)),f25(x1221)) % 58.78/58.80 [123]~P2(x1231)+P9(f27(x1231),f28(f25(x1231),f25(x1231)),f25(x1231)) % 58.78/58.80 [101]~P14(x1011)+~P12(x1012,x1011) % 58.78/58.80 [104]~P12(x1041,x1042)+P7(x1041,x1042) % 58.78/58.80 [110]~P12(x1102,x1101)+~P12(x1101,x1102) % 58.78/58.80 [109]~P6(x1091,x1092)+P7(x1091,f26(x1092)) % 58.78/58.80 [113]P6(x1131,x1132)+~P7(x1131,f26(x1132)) % 58.78/58.80 [124]~P9(x1241,x1242,x1243)+P8(x1241,x1242,x1243) % 58.78/58.80 [125]~P8(x1251,x1252,x1253)+P9(x1251,x1252,x1253) % 58.78/58.80 [121]P15(x1211)+~P7(x1211,f26(f28(x1212,x1213))) % 58.78/58.80 [126]~P9(x1261,x1262,x1263)+P7(x1261,f26(f28(x1262,x1263))) % 58.78/58.80 [99]~P4(x991)+P18(x991)+~P14(f25(x991)) % 58.78/58.80 [100]~P4(x1001)+P18(x1001)+~P14(f10(x1001)) % 58.78/58.80 [107]~P2(x1071)+~P3(x1071)+E(f22(f25(x1071),f27(x1071)),x1071) % 58.78/58.80 [115]~P4(x1151)+P18(x1151)+P7(f10(x1151),f26(f25(x1151))) % 58.78/58.80 [96]~P14(x962)+~P14(x961)+E(x961,x962) % 58.78/58.80 [106]~P7(x1062,x1061)+P14(x1061)+P12(x1062,x1061) % 58.78/58.80 [116]P14(x1161)+P14(x1162)+~P14(f28(x1162,x1161)) % 58.78/58.80 [117]~P14(x1171)+~P12(x1172,x1173)+~P7(x1173,f26(x1171)) % 58.78/58.80 [118]P7(x1181,x1182)+~P12(x1181,x1183)+~P7(x1183,f26(x1182)) % 58.78/58.80 [105]~P1(x1051)+~P2(x1051)+P18(x1051)+P5(f19(x1051),x1051) % 58.78/58.80 [135]~P11(x1352)+~P8(x1352,f28(x1351,x1351),x1351)+~P13(x1352,f28(x1351,x1351),x1351)+P2(f22(x1351,x1352)) % 58.78/58.80 [136]~P11(x1362)+~P8(x1362,f28(x1361,x1361),x1361)+~P13(x1362,f28(x1361,x1361),x1361)+P3(f22(x1361,x1362)) % 58.78/58.80 [131]~P11(x1311)+~P8(x1311,x1312,x1313)+~P16(x1311,x1312,x1313)+P13(x1311,x1312,x1313) % 58.78/58.80 [103]~P1(x1031)+~P17(x1031)+~P2(x1031)+P18(x1031)+P11(f20(x1031)) % 58.78/58.80 [108]~P1(x1081)+~P17(x1081)+~P2(x1081)+P18(x1081)+~P14(f24(x1081)) % 58.78/58.80 [119]~P1(x1191)+~P17(x1191)+~P2(x1191)+P18(x1191)+P13(f20(x1191),f24(x1191),f26(f25(x1191))) % 58.78/58.80 [120]~P1(x1201)+~P17(x1201)+~P2(x1201)+P18(x1201)+P9(f20(x1201),f24(x1201),f26(f25(x1201))) % 58.78/58.80 [111]~P1(x1111)+~P2(x1111)+~P5(x1112,x1111)+P18(x1111)+P1(x1112) % 58.78/58.80 [112]~P1(x1121)+~P2(x1121)+~P5(x1122,x1121)+P18(x1121)+P2(x1122) % 58.78/58.80 [114]~P1(x1141)+~P2(x1141)+~P5(x1142,x1141)+P18(x1141)+~P18(x1142) % 58.78/58.80 [132]~P11(x1322)+~P8(x1322,x1323,x1321)+~P13(x1322,x1323,x1321)+P14(x1321)+P16(x1322,x1323,x1321) % 58.78/58.80 [130]~P2(x1301)+P18(x1301)+~P7(x1303,f25(x1301))+~P7(x1302,f25(x1301))+P7(f23(x1301,x1302,x1303),f25(x1301)) % 58.78/58.80 [137]~P11(x1371)+E(x1371,x1372)+~P8(x1371,f28(x1373,x1373),x1373)+~P13(x1371,f28(x1373,x1373),x1373)+~E(f22(x1373,x1371),f22(x1374,x1372)) % 58.78/58.80 [138]~P11(x1383)+E(x1381,x1382)+~P8(x1383,f28(x1381,x1381),x1381)+~P13(x1383,f28(x1381,x1381),x1381)+~E(f22(x1381,x1383),f22(x1382,x1384)) % 58.78/58.80 [129]~P14(x1293)+~P8(x1293,x1292,x1291)+~P13(x1293,x1292,x1291)+P14(x1291)+P14(x1292)+~P11(x1293) % 58.78/58.80 [127]~P1(x1271)+~P17(x1271)+~P2(x1271)+~P3(x1273)+~P5(x1273,x1271)+~P10(x1273,x1272)+P18(x1271)+~P7(x1272,f25(x1271))+P12(x1272,f21(f20(x1271),x1273)) % 58.78/58.80 [128]~P1(x1281)+~P17(x1281)+~P2(x1281)+~P3(x1282)+~P5(x1282,x1281)+P18(x1281)+P10(x1282,x1283)+~P7(x1283,f25(x1281))+~P12(x1283,f21(f20(x1281),x1282)) % 58.78/58.80 [134]~P1(x1341)+~P17(x1341)+~P2(x1341)+~P5(x1342,x1341)+~P10(x1342,x1344)+~P10(x1342,x1343)+P18(x1341)+~P7(x1344,f25(x1341))+~P7(x1343,f25(x1341))+P10(x1342,f23(x1341,x1343,x1344)) % 58.78/58.80 %EqnAxiom % 58.78/58.80 [1]E(x11,x11) % 58.78/58.80 [2]E(x22,x21)+~E(x21,x22) % 58.78/58.80 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 58.78/58.80 [4]~E(x41,x42)+E(f7(x41),f7(x42)) % 58.78/58.80 [5]~E(x51,x52)+E(f25(x51),f25(x52)) % 58.78/58.80 [6]~E(x61,x62)+E(f28(x61,x63),f28(x62,x63)) % 58.78/58.80 [7]~E(x71,x72)+E(f28(x73,x71),f28(x73,x72)) % 58.78/58.80 [8]~E(x81,x82)+E(f17(x81),f17(x82)) % 58.78/58.80 [9]~E(x91,x92)+E(f23(x91,x93,x94),f23(x92,x93,x94)) % 58.78/58.80 [10]~E(x101,x102)+E(f23(x103,x101,x104),f23(x103,x102,x104)) % 58.78/58.80 [11]~E(x111,x112)+E(f23(x113,x114,x111),f23(x113,x114,x112)) % 58.78/58.80 [12]~E(x121,x122)+E(f26(x121),f26(x122)) % 58.78/58.80 [13]~E(x131,x132)+E(f3(x131,x133),f3(x132,x133)) % 58.78/58.80 [14]~E(x141,x142)+E(f3(x143,x141),f3(x143,x142)) % 58.78/58.80 [15]~E(x151,x152)+E(f8(x151,x153),f8(x152,x153)) % 58.78/58.80 [16]~E(x161,x162)+E(f8(x163,x161),f8(x163,x162)) % 58.78/58.80 [17]~E(x171,x172)+E(f20(x171),f20(x172)) % 58.78/58.80 [18]~E(x181,x182)+E(f22(x181,x183),f22(x182,x183)) % 58.78/58.80 [19]~E(x191,x192)+E(f22(x193,x191),f22(x193,x192)) % 58.78/58.80 [20]~E(x201,x202)+E(f24(x201),f24(x202)) % 58.78/58.80 [21]~E(x211,x212)+E(f21(x211,x213),f21(x212,x213)) % 58.78/58.80 [22]~E(x221,x222)+E(f21(x223,x221),f21(x223,x222)) % 58.78/58.80 [23]~E(x231,x232)+E(f10(x231),f10(x232)) % 58.78/58.80 [24]~E(x241,x242)+E(f19(x241),f19(x242)) % 58.78/58.80 [25]~E(x251,x252)+E(f18(x251,x253),f18(x252,x253)) % 58.78/58.80 [26]~E(x261,x262)+E(f18(x263,x261),f18(x263,x262)) % 58.78/58.80 [27]~E(x271,x272)+E(f27(x271),f27(x272)) % 58.78/58.80 [28]~E(x281,x282)+E(f5(x281),f5(x282)) % 58.78/58.80 [29]~E(x291,x292)+E(f4(x291,x293),f4(x292,x293)) % 58.78/58.80 [30]~E(x301,x302)+E(f4(x303,x301),f4(x303,x302)) % 58.78/58.80 [31]~P1(x311)+P1(x312)+~E(x311,x312) % 58.78/58.80 [32]~P17(x321)+P17(x322)+~E(x321,x322) % 58.78/58.80 [33]~P2(x331)+P2(x332)+~E(x331,x332) % 58.78/58.80 [34]P5(x342,x343)+~E(x341,x342)+~P5(x341,x343) % 58.78/58.80 [35]P5(x353,x352)+~E(x351,x352)+~P5(x353,x351) % 58.78/58.80 [36]~P3(x361)+P3(x362)+~E(x361,x362) % 58.78/58.80 [37]~P14(x371)+P14(x372)+~E(x371,x372) % 58.78/58.80 [38]P12(x382,x383)+~E(x381,x382)+~P12(x381,x383) % 58.78/58.80 [39]P12(x393,x392)+~E(x391,x392)+~P12(x393,x391) % 58.78/58.80 [40]~P4(x401)+P4(x402)+~E(x401,x402) % 58.78/58.80 [41]P7(x412,x413)+~E(x411,x412)+~P7(x411,x413) % 58.78/58.80 [42]P7(x423,x422)+~E(x421,x422)+~P7(x423,x421) % 58.78/58.80 [43]~P11(x431)+P11(x432)+~E(x431,x432) % 58.78/58.80 [44]~P18(x441)+P18(x442)+~E(x441,x442) % 58.78/58.80 [45]P6(x452,x453)+~E(x451,x452)+~P6(x451,x453) % 58.78/58.80 [46]P6(x463,x462)+~E(x461,x462)+~P6(x463,x461) % 58.78/58.80 [47]P8(x472,x473,x474)+~E(x471,x472)+~P8(x471,x473,x474) % 58.78/58.80 [48]P8(x483,x482,x484)+~E(x481,x482)+~P8(x483,x481,x484) % 58.78/58.80 [49]P8(x493,x494,x492)+~E(x491,x492)+~P8(x493,x494,x491) % 58.78/58.80 [50]P9(x502,x503,x504)+~E(x501,x502)+~P9(x501,x503,x504) % 58.78/58.80 [51]P9(x513,x512,x514)+~E(x511,x512)+~P9(x513,x511,x514) % 58.78/58.80 [52]P9(x523,x524,x522)+~E(x521,x522)+~P9(x523,x524,x521) % 58.78/58.80 [53]P16(x532,x533,x534)+~E(x531,x532)+~P16(x531,x533,x534) % 58.78/58.80 [54]P16(x543,x542,x544)+~E(x541,x542)+~P16(x543,x541,x544) % 58.78/58.80 [55]P16(x553,x554,x552)+~E(x551,x552)+~P16(x553,x554,x551) % 58.78/58.80 [56]P13(x562,x563,x564)+~E(x561,x562)+~P13(x561,x563,x564) % 58.78/58.80 [57]P13(x573,x572,x574)+~E(x571,x572)+~P13(x573,x571,x574) % 58.78/58.80 [58]P13(x583,x584,x582)+~E(x581,x582)+~P13(x583,x584,x581) % 58.78/58.80 [59]P10(x592,x593)+~E(x591,x592)+~P10(x591,x593) % 58.78/58.80 [60]P10(x603,x602)+~E(x601,x602)+~P10(x603,x601) % 58.78/58.80 [61]~P15(x611)+P15(x612)+~E(x611,x612) % 58.78/58.80 % 58.78/58.80 %------------------------------------------- % 58.78/58.81 cnf(141,plain, % 58.78/58.81 (~P12(x1411,a15)), % 58.78/58.81 inference(scs_inference,[],[67,101])). % 58.78/58.81 cnf(145,plain, % 58.78/58.81 (P6(f17(f26(x1451)),x1451)), % 58.78/58.81 inference(scs_inference,[],[83,76,67,101,110,113])). % 58.78/58.81 cnf(146,plain, % 58.78/58.81 (P7(f17(x1461),x1461)), % 58.78/58.81 inference(rename_variables,[],[76])). % 58.78/58.81 cnf(148,plain, % 58.78/58.81 (P15(f7(f28(x1481,x1482)))), % 58.78/58.81 inference(scs_inference,[],[83,76,77,67,101,110,113,121])). % 58.78/58.81 cnf(151,plain, % 58.78/58.81 (P12(f17(a9),a9)), % 58.78/58.81 inference(scs_inference,[],[83,76,146,77,67,91,101,110,113,121,106])). % 58.78/58.81 cnf(152,plain, % 58.78/58.81 (P7(f17(x1521),x1521)), % 58.78/58.81 inference(rename_variables,[],[76])). % 58.78/58.81 cnf(154,plain, % 58.78/58.81 (~P12(x1541,f17(f26(a15)))), % 58.78/58.81 inference(scs_inference,[],[83,76,146,152,77,67,91,101,110,113,121,106,117])). % 58.78/58.81 cnf(155,plain, % 58.78/58.81 (P7(f17(x1551),x1551)), % 58.78/58.81 inference(rename_variables,[],[76])). % 58.78/58.81 cnf(159,plain, % 58.78/58.81 (~P14(f21(f20(a1),a12))), % 58.78/58.81 inference(scs_inference,[],[93,83,76,146,152,77,67,91,101,110,113,121,106,117,38,39,96])). % 58.78/58.81 cnf(161,plain, % 58.78/58.81 (P1(a12)), % 58.78/58.81 inference(scs_inference,[],[62,64,72,89,93,83,76,146,152,77,67,91,101,110,113,121,106,117,38,39,96,111])). % 58.78/58.81 cnf(163,plain, % 58.78/58.81 (P2(a12)), % 58.78/58.81 inference(scs_inference,[],[62,64,72,89,93,83,76,146,152,77,67,91,101,110,113,121,106,117,38,39,96,111,112])). % 58.78/58.81 cnf(165,plain, % 58.78/58.81 (~P18(a12)), % 58.78/58.81 inference(scs_inference,[],[62,64,72,89,93,83,76,146,152,77,67,91,101,110,113,121,106,117,38,39,96,111,112,114])). % 58.78/58.81 cnf(167,plain, % 58.78/58.81 (P16(f3(x1671,a9),x1671,a9)), % 58.78/58.81 inference(scs_inference,[],[62,64,72,89,93,83,76,146,152,85,87,77,67,91,78,101,110,113,121,106,117,38,39,96,111,112,114,132])). % 58.78/58.81 cnf(168,plain, % 58.78/58.81 (P13(f3(x1681,x1682),x1681,x1682)), % 58.78/58.81 inference(rename_variables,[],[87])). % 58.78/58.81 cnf(169,plain, % 58.78/58.81 (P11(f3(x1691,x1692))), % 58.78/58.81 inference(rename_variables,[],[78])). % 58.78/58.81 cnf(170,plain, % 58.78/58.81 (P8(f3(x1701,x1702),x1701,x1702)), % 58.78/58.81 inference(rename_variables,[],[85])). % 58.78/58.81 cnf(172,plain, % 58.78/58.81 (~P14(f3(a9,a9))), % 58.78/58.81 inference(scs_inference,[],[62,64,72,89,93,83,76,146,152,85,170,87,168,77,67,91,78,169,101,110,113,121,106,117,38,39,96,111,112,114,132,129])). % 58.78/58.81 cnf(177,plain, % 58.78/58.81 (P10(a12,a14)), % 58.78/58.81 inference(scs_inference,[],[62,63,64,66,72,89,75,93,83,76,146,152,85,170,87,168,77,67,91,78,169,101,110,113,121,106,117,38,39,96,111,112,114,132,129,128])). % 58.78/58.81 cnf(179,plain, % 58.78/58.81 (P10(a12,f23(a1,a14,a14))), % 58.78/58.81 inference(scs_inference,[],[62,63,64,66,72,89,75,93,83,76,146,152,85,170,87,168,77,67,91,78,169,101,110,113,121,106,117,38,39,96,111,112,114,132,129,128,134])). % 58.78/58.81 cnf(188,plain, % 58.78/58.81 (P6(x1881,x1882)+~E(x1882,x1881)), % 58.78/58.81 inference(scs_inference,[],[62,63,64,66,72,89,74,75,93,83,76,146,152,155,73,85,170,87,168,77,67,91,78,169,101,110,113,121,106,117,38,39,96,111,112,114,132,129,128,134,118,34,35,41,42,45])). % 58.78/58.81 cnf(196,plain, % 58.78/58.81 (~P12(x1961,a2)), % 58.78/58.81 inference(scs_inference,[],[82,68,110,101])). % 58.78/58.81 cnf(198,plain, % 58.78/58.81 (P6(f7(x1981),x1981)), % 58.78/58.81 inference(scs_inference,[],[82,68,77,110,101,113])). % 58.78/58.81 cnf(200,plain, % 58.78/58.81 (~P7(f23(a1,a13,a14),f21(f20(a1),a12))), % 58.78/58.81 inference(scs_inference,[],[82,93,159,68,77,110,101,113,106])). % 58.78/58.81 cnf(202,plain, % 58.78/58.81 (~P12(x2021,f17(f26(a2)))), % 58.78/58.81 inference(scs_inference,[],[82,93,159,76,68,77,110,101,113,106,117])). % 58.78/58.81 cnf(207,plain, % 58.78/58.81 (~E(a13,f23(a1,a13,a14))), % 58.78/58.81 inference(scs_inference,[],[82,93,154,159,76,68,77,110,101,113,106,117,39,38])). % 58.78/58.81 cnf(208,plain, % 58.78/58.81 (P10(a12,a13)), % 58.78/58.81 inference(scs_inference,[],[62,82,66,93,74,63,64,89,72,154,159,76,68,77,110,101,113,106,117,39,38,128])). % 58.78/58.81 cnf(210,plain, % 58.78/58.81 (P10(a12,f23(a1,a13,a13))), % 58.78/58.81 inference(scs_inference,[],[62,82,66,93,74,63,64,89,72,154,159,76,68,77,110,101,113,106,117,39,38,128,134])). % 58.78/58.81 cnf(212,plain, % 58.78/58.81 (P6(f17(f26(x2121)),x2122)+~E(x2121,x2122)), % 58.78/58.81 inference(scs_inference,[],[62,82,66,93,74,63,64,89,72,154,159,76,145,68,77,110,101,113,106,117,39,38,128,134,46])). % 58.78/58.81 cnf(214,plain, % 58.78/58.81 (P8(f18(x2141,x2142),x2143,x2142)+~E(x2141,x2143)), % 58.78/58.81 inference(scs_inference,[],[62,82,66,93,74,63,64,89,72,154,159,76,145,84,68,77,110,101,113,106,117,39,38,128,134,46,47,48])). % 58.78/58.81 cnf(215,plain, % 58.78/58.81 (P8(f18(x2151,x2152),x2151,x2153)+~E(x2152,x2153)), % 58.78/58.81 inference(scs_inference,[],[62,82,66,93,74,63,64,89,72,154,159,76,145,84,68,77,110,101,113,106,117,39,38,128,134,46,47,48,49])). % 58.78/58.81 cnf(217,plain, % 58.78/58.81 (P9(f4(x2171,x2172),x2173,x2172)+~E(x2171,x2173)), % 58.78/58.81 inference(scs_inference,[],[62,82,66,93,74,63,64,89,72,154,159,76,145,84,88,68,77,110,101,113,106,117,39,38,128,134,46,47,48,49,50,51])). % 58.78/58.81 cnf(224,plain, % 58.78/58.81 (~P12(x2241,f7(x2242))), % 58.78/58.81 inference(scs_inference,[],[71,101])). % 58.78/58.81 cnf(228,plain, % 58.78/58.81 (P12(f17(f3(a9,a9)),f3(a9,a9))), % 58.78/58.81 inference(scs_inference,[],[151,172,76,71,101,110,106])). % 58.78/58.81 cnf(233,plain, % 58.78/58.81 (P16(f3(x2331,f3(a9,a9)),x2331,f3(a9,a9))), % 58.78/58.81 inference(scs_inference,[],[83,202,151,172,76,71,85,87,78,101,110,106,39,132])). % 58.78/58.81 cnf(234,plain, % 58.78/58.81 (P13(f3(x2341,x2342),x2341,x2342)), % 58.78/58.81 inference(rename_variables,[],[87])). % 58.78/58.81 cnf(235,plain, % 58.78/58.81 (P11(f3(x2351,x2352))), % 58.78/58.81 inference(rename_variables,[],[78])). % 58.78/58.81 cnf(236,plain, % 58.78/58.81 (P8(f3(x2361,x2362),x2361,x2362)), % 58.78/58.81 inference(rename_variables,[],[85])). % 58.78/58.81 cnf(238,plain, % 58.78/58.81 (~P14(f3(f3(a9,a9),f3(a9,a9)))), % 58.78/58.81 inference(scs_inference,[],[83,202,151,172,76,71,85,236,87,234,78,235,101,110,106,39,132,129])). % 58.78/58.81 cnf(239,plain, % 58.78/58.81 (P13(f3(x2391,x2392),x2391,x2392)), % 58.78/58.81 inference(rename_variables,[],[87])). % 58.78/58.81 cnf(243,plain, % 58.78/58.81 (P9(f4(x2431,x2432),x2431,x2433)+~E(x2432,x2433)), % 58.78/58.81 inference(scs_inference,[],[83,202,151,172,76,71,85,236,87,234,78,235,88,101,110,106,39,132,129,52])). % 58.78/58.81 cnf(245,plain, % 58.78/58.81 (P16(f3(x2451,a9),x2452,a9)+~E(x2451,x2452)), % 58.78/58.81 inference(scs_inference,[],[83,202,151,167,172,76,71,85,236,87,234,78,235,88,101,110,106,39,132,129,52,53,54])). % 58.78/58.81 cnf(248,plain, % 58.78/58.81 (P13(f3(x2481,x2482),x2483,x2482)+~E(x2481,x2483)), % 58.78/58.81 inference(scs_inference,[],[83,202,151,167,172,76,71,85,236,87,234,239,78,235,88,101,110,106,39,132,129,52,53,54,55,56,57])). % 58.78/58.81 cnf(257,plain, % 58.78/58.81 (P12(f17(f26(x2571)),f26(x2571))), % 58.78/58.81 inference(scs_inference,[],[228,76,92,110,106])). % 58.78/58.81 cnf(262,plain, % 58.78/58.81 (P13(f3(x2621,x2622),x2621,x2623)+~E(x2622,x2623)), % 58.78/58.81 inference(scs_inference,[],[82,224,228,76,92,87,110,106,39,58])). % 58.78/58.81 cnf(266,plain, % 58.78/58.81 (P6(x2661,x2662)+~E(f7(x2662),x2661)), % 58.78/58.81 inference(scs_inference,[],[82,75,224,179,228,76,198,92,87,110,106,39,58,59,60,42,45])). % 58.78/58.81 cnf(267,plain, % 58.78/58.81 (P8(f8(x2671,x2672),x2673,x2672)+~E(x2671,x2673)), % 58.78/58.81 inference(scs_inference,[],[82,75,224,179,228,76,198,86,92,87,110,106,39,58,59,60,42,45,48])). % 58.78/58.81 cnf(290,plain, % 58.78/58.81 (P16(f3(x2901,f3(a9,a9)),x2902,f3(a9,a9))+~E(x2901,x2902)), % 58.78/58.81 inference(scs_inference,[],[83,210,196,233,39,53,59,60,54])). % 58.78/58.81 cnf(292,plain, % 58.78/58.81 (P6(x2921,x2922)+~E(x2921,x2922)), % 58.78/58.81 inference(scs_inference,[],[83,210,196,233,73,145,39,53,59,60,54,45,46])). % 58.78/58.81 cnf(303,plain, % 58.78/58.81 (P8(f3(x3031,x3032),x3031,x3033)+~E(x3032,x3033)), % 58.78/58.81 inference(scs_inference,[],[228,224,233,85,39,55,47,49])). % 58.78/58.81 cnf(307,plain, % 58.78/58.81 (P8(f3(x3071,x3072),x3073,x3072)+~E(x3071,x3073)), % 58.78/58.81 inference(scs_inference,[],[228,207,177,224,233,85,39,55,47,49,96,60,48])). % 58.78/58.81 cnf(316,plain, % 58.78/58.81 (P7(f17(x3161),x3162)+~E(x3161,x3162)), % 58.78/58.81 inference(scs_inference,[],[75,151,154,76,39,41,42])). % 58.78/58.81 cnf(317,plain, % 58.78/58.81 (P8(f8(x3171,x3172),x3171,x3173)+~E(x3172,x3173)), % 58.78/58.81 inference(scs_inference,[],[75,151,154,76,86,39,41,42,49])). % 58.78/58.81 cnf(329,plain, % 58.78/58.81 (P6(f7(x3291),x3292)+~E(x3291,x3292)), % 58.78/58.81 inference(scs_inference,[],[257,202,198,39,46])). % 58.78/58.81 cnf(334,plain, % 58.78/58.81 (P7(x3341,f26(x3342))+~E(f7(x3342),x3341)), % 58.78/58.81 inference(scs_inference,[],[228,141,77,39,41])). % 58.78/58.81 cnf(382,plain, % 58.78/58.81 (~P14(f25(a1))), % 58.78/58.81 inference(scs_inference,[],[64,89,95,99])). % 58.78/58.81 cnf(388,plain, % 58.78/58.81 (P13(f3(x3881,x3882),x3881,x3882)), % 58.78/58.81 inference(rename_variables,[],[87])). % 58.78/58.81 cnf(389,plain, % 58.78/58.81 (P11(f3(x3891,x3892))), % 58.78/58.81 inference(rename_variables,[],[78])). % 58.78/58.81 cnf(390,plain, % 58.78/58.81 (P8(f3(x3901,x3902),x3901,x3902)), % 58.78/58.81 inference(rename_variables,[],[85])). % 58.78/58.81 cnf(400,plain, % 58.78/58.81 (P16(f3(x4001,f25(a1)),x4002,f25(a1))+~E(x4001,x4002)), % 58.78/58.81 inference(scs_inference,[],[74,257,382,224,87,388,85,390,78,389,106,39,132,129,110,53,54])). % 58.78/58.81 cnf(413,plain, % 58.78/58.81 (~P10(a12,f23(a1,a13,a14))+~P7(f23(a1,a13,a14),f25(a1))), % 58.78/58.81 inference(scs_inference,[],[62,64,72,93,66,63,89,228,154,39,127])). % 58.78/58.81 cnf(432,plain, % 58.78/58.81 (~E(a9,a2)), % 58.78/58.81 inference(scs_inference,[],[151,196,39])). % 58.78/58.81 cnf(754,plain, % 58.78/58.81 (E(a15,f7(x7541))), % 58.78/58.81 inference(scs_inference,[],[71,2,94])). % 58.78/58.81 cnf(756,plain, % 58.78/58.81 (P6(f7(x7561),a15)), % 58.78/58.81 inference(scs_inference,[],[754,316,188])). % 58.78/58.81 cnf(758,plain, % 58.78/58.81 (P8(f18(a15,x7581),f7(x7582),x7581)), % 58.78/58.81 inference(scs_inference,[],[754,316,188,212,214])). % 58.78/58.81 cnf(760,plain, % 58.78/58.81 (P9(f4(a15,x7601),f7(x7602),x7601)), % 58.78/58.81 inference(scs_inference,[],[754,316,188,212,214,215,217])). % 58.78/58.81 cnf(761,plain, % 58.78/58.81 (P9(f4(x7611,a15),x7611,f7(x7612))), % 58.78/58.81 inference(scs_inference,[],[754,316,188,212,214,215,217,243])). % 58.78/58.81 cnf(762,plain, % 58.78/58.81 (P13(f3(a15,x7621),f7(x7622),x7621)), % 58.78/58.81 inference(scs_inference,[],[754,316,188,212,214,215,217,243,248])). % 58.78/58.81 cnf(763,plain, % 58.78/58.81 (P13(f3(x7631,a15),x7631,f7(x7632))), % 58.78/58.81 inference(scs_inference,[],[754,316,188,212,214,215,217,243,248,262])). % 58.78/58.81 cnf(768,plain, % 58.78/58.81 (P8(f8(x7681,a15),x7681,f7(x7682))), % 58.78/58.81 inference(scs_inference,[],[754,316,188,212,214,215,217,243,248,262,267,292,303,307,317])). % 58.78/58.81 cnf(770,plain, % 58.78/58.81 (E(f7(x7701),a15)), % 58.78/58.81 inference(scs_inference,[],[754,316,188,212,214,215,217,243,248,262,267,292,303,307,317,329,2])). % 58.78/58.81 cnf(771,plain, % 58.78/58.81 (P15(a15)), % 58.78/58.81 inference(scs_inference,[],[754,148,316,188,212,214,215,217,243,248,262,267,292,303,307,317,329,2,61])). % 58.78/58.81 cnf(773,plain, % 58.78/58.81 (E(a15,f7(x7731))), % 58.78/58.81 inference(rename_variables,[],[754])). % 58.78/58.81 cnf(778,plain, % 58.78/58.81 (P7(a15,f26(f28(x7781,x7782)))), % 58.78/58.81 inference(scs_inference,[],[754,773,77,148,316,188,212,214,215,217,243,248,262,267,292,303,307,317,329,2,61,57,58,51,52,46,41])). % 58.78/58.81 cnf(790,plain, % 58.78/58.81 (P7(a15,f26(x7901))), % 58.78/58.81 inference(scs_inference,[],[770,334])). % 58.78/58.81 cnf(792,plain, % 58.78/58.81 (P8(f3(x7921,f7(x7922)),x7921,a15)), % 58.78/58.81 inference(scs_inference,[],[770,334,266,303])). % 58.78/58.81 cnf(793,plain, % 58.78/58.81 (P8(f18(f7(x7931),x7932),a15,x7932)), % 58.78/58.81 inference(scs_inference,[],[770,334,266,303,214])). % 58.78/58.81 cnf(794,plain, % 58.78/58.81 (P8(f8(x7941,f7(x7942)),x7941,a15)), % 58.78/58.81 inference(scs_inference,[],[770,334,266,303,214,317])). % 58.78/58.81 cnf(796,plain, % 58.78/58.81 (P9(f4(f7(x7961),x7962),a15,x7962)), % 58.78/58.81 inference(scs_inference,[],[770,334,266,303,214,317,307,217])). % 58.78/58.81 cnf(797,plain, % 58.78/58.81 (P13(f3(x7971,f7(x7972)),x7971,a15)), % 58.78/58.81 inference(scs_inference,[],[770,334,266,303,214,317,307,217,262])). % 58.78/58.81 cnf(798,plain, % 58.78/58.81 (P13(f3(f7(x7981),x7982),a15,x7982)), % 58.78/58.81 inference(scs_inference,[],[770,334,266,303,214,317,307,217,262,248])). % 58.78/58.81 cnf(799,plain, % 58.78/58.81 (P9(f4(x7991,f7(x7992)),x7991,a15)), % 58.78/58.81 inference(scs_inference,[],[770,334,266,303,214,317,307,217,262,248,243])). % 58.78/58.81 cnf(817,plain, % 58.78/58.81 (P16(f3(f7(x8171),a9),a15,a9)), % 58.78/58.81 inference(scs_inference,[],[778,167,760,761,762,763,756,770,771,754,92,334,266,303,214,317,307,217,262,248,243,316,215,267,61,106,58,51,57,52,46,41,54])). % 58.78/58.81 cnf(837,plain, % 58.78/58.81 (P9(f4(f7(x8371),x8372),f7(x8373),x8372)), % 58.78/58.81 inference(scs_inference,[],[754,796,51])). % 58.78/58.81 cnf(838,plain, % 58.78/58.81 (P13(f3(x8381,f7(x8382)),x8381,f7(x8383))), % 58.78/58.81 inference(scs_inference,[],[754,796,797,51,58])). % 58.78/58.81 cnf(839,plain, % 58.78/58.81 (P9(f4(x8391,f7(x8392)),x8391,f7(x8393))), % 58.78/58.81 inference(scs_inference,[],[754,796,797,799,51,58,52])). % 58.78/58.81 cnf(840,plain, % 58.78/58.81 (P13(f3(f7(x8401),x8402),f7(x8403),x8402)), % 58.78/58.81 inference(scs_inference,[],[754,796,797,798,799,51,58,52,57])). % 58.78/58.81 cnf(861,plain, % 58.78/58.81 (P9(f4(f7(x8611),f7(x8612)),a15,f7(x8613))), % 58.78/58.81 inference(scs_inference,[],[790,770,839,92,106,51])). % 58.78/58.81 cnf(867,plain, % 58.78/58.81 (P13(f3(f7(x8671),f7(x8672)),a15,f7(x8673))), % 58.78/58.81 inference(scs_inference,[],[790,770,837,838,839,840,92,106,51,58,52,57])). % 58.78/58.81 cnf(873,plain, % 58.78/58.81 (P8(f3(x8731,f7(x8732)),x8731,f7(x8733))), % 58.78/58.81 inference(scs_inference,[],[790,233,770,754,837,838,839,840,768,792,92,106,51,58,52,57,54,48,49])). % 58.78/58.81 cnf(874,plain, % 58.78/58.81 (P12(f7(x8741),f26(x8742))), % 58.78/58.81 inference(scs_inference,[],[790,233,770,754,837,838,839,840,768,792,92,106,51,58,52,57,54,48,49,38])). % 58.78/58.81 cnf(882,plain, % 58.78/58.81 (P9(f4(f7(x8821),f7(x8822)),a15,a15)), % 58.78/58.81 inference(scs_inference,[],[770,861,52])). % 58.78/58.81 cnf(883,plain, % 58.78/58.81 (P9(f4(f7(x8831),f7(x8832)),a15,f7(x8833))), % 58.78/58.81 inference(rename_variables,[],[861])). % 58.78/58.81 cnf(891,plain, % 58.78/58.81 (P8(f18(f7(x8911),f7(x8912)),a15,a15)), % 58.78/58.81 inference(scs_inference,[],[770,754,817,798,873,861,883,867,793,52,58,51,57,54,48,49])). % 58.78/58.81 cnf(1068,plain, % 58.78/58.81 (P8(f8(x10681,f7(x10682)),x10681,f7(x10683))), % 58.78/58.81 inference(scs_inference,[],[754,794,49])). % 58.78/58.81 cnf(3881,plain, % 58.78/58.81 (P7(f18(f7(x38811),f7(x38812)),f26(f28(a15,a15)))), % 58.78/58.81 inference(scs_inference,[],[891,125,126])). % 58.78/58.81 cnf(4755,plain, % 58.78/58.81 (~P10(a12,f23(a1,a13,a14))), % 58.78/58.81 inference(scs_inference,[],[75,74,89,64,413,130])). % 58.78/58.81 cnf(5675,plain, % 58.78/58.81 (P9(f4(a15,a15),f7(x56751),f7(x56752))), % 58.78/58.81 inference(scs_inference,[],[761,754,758,49,51])). % 58.78/58.81 cnf(6377,plain, % 58.78/58.81 ($false), % 58.78/58.81 inference(scs_inference,[],[62,70,90,238,432,874,1068,5675,882,4755,92,67,68,200,73,177,3881,179,208,161,165,163,82,75,74,754,66,63,64,89,72,95,97,98,109,124,125,102,4,5,8,12,17,20,23,24,27,28,126,245,6,7,13,14,15,16,18,19,21,22,25,26,29,30,9,400,122,123,290,94,10,104,2,11,99,100,116,115,107,37,3,106,59,117,42,105,103,108,119,120,130,111,114,112,127,134]), % 58.78/58.81 ['proof']). % 58.78/58.81 % SZS output end Proof % 58.78/58.81 % Total time :58.040000s %------------------------------------------------------------------------------