%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : GRP642+1 : TPTP v8.2.0. Released v3.4.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/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:13 EDT 2024 % Result : Theorem 58.76s 58.82s % Output : CNFRefutation 58.76s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.12 % Problem : GRP642+1 : TPTP v8.2.0. Released v3.4.0. % 0.10/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n020.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 : Thu Jun 20 09:09:09 EDT 2024 % 0.12/0.33 % CPUTime : % 0.21/0.57 start to proof:theBenchmark % 58.76/58.80 %------------------------------------------- % 58.76/58.80 % File :CSE---1.7 % 58.76/58.80 % Problem :theBenchmark % 58.76/58.80 % Transform :cnf % 58.76/58.80 % Format :tptp:raw % 58.76/58.80 % Command :java -jar mcs_scs.jar %d %s % 58.76/58.80 % 58.76/58.80 % Result :Theorem 58.180000s % 58.76/58.80 % Output :CNFRefutation 58.180000s % 58.76/58.80 %------------------------------------------- % 58.76/58.81 %------------------------------------------------------------------------------ % 58.76/58.81 % File : GRP642+1 : TPTP v8.2.0. Released v3.4.0. % 58.76/58.81 % Domain : Group Theory % 58.76/58.81 % Problem : On the Lattice of Subgroups of a Group T20 % 58.76/58.81 % Version : [Urb08] axioms : Especial. % 58.76/58.81 % English : % 58.76/58.81 % 58.76/58.81 % Refs : [Gan96] Ganczarski (1996), On the Lattice of Subgroups of a Gr % 58.76/58.81 % : [Urb07] Urban (2007), MPTP 0.2: Design, Implementation, and In % 58.76/58.81 % : [Urb08] Urban (2006), Email to G. Sutcliffe % 58.76/58.81 % Source : [Urb08] % 58.76/58.81 % Names : t20_latsubgr [Urb08] % 58.76/58.81 % 58.76/58.81 % Status : Theorem % 58.76/58.81 % Rating : 0.25 v8.2.0, 0.22 v8.1.0, 0.17 v7.5.0, 0.19 v7.4.0, 0.13 v7.3.0, 0.28 v7.2.0, 0.24 v7.1.0, 0.22 v7.0.0, 0.17 v6.4.0, 0.23 v6.3.0, 0.25 v6.2.0, 0.28 v6.1.0, 0.30 v6.0.0, 0.26 v5.5.0, 0.33 v5.4.0, 0.39 v5.3.0, 0.48 v5.2.0, 0.30 v5.1.0, 0.33 v5.0.0, 0.46 v4.1.0, 0.48 v4.0.0, 0.50 v3.7.0, 0.40 v3.5.0, 0.42 v3.4.0 % 58.76/58.81 % Syntax : Number of formulae : 53 ( 19 unt; 0 def) % 58.76/58.81 % Number of atoms : 153 ( 9 equ) % 58.76/58.81 % Maximal formula atoms : 11 ( 2 avg) % 58.76/58.81 % Number of connectives : 130 ( 30 ~; 1 |; 60 &) % 58.76/58.81 % ( 3 <=>; 36 =>; 0 <=; 0 <~>) % 58.76/58.81 % Maximal formula depth : 10 ( 4 avg) % 58.76/58.81 % Maximal term depth : 3 ( 1 avg) % 58.76/58.81 % Number of predicates : 19 ( 17 usr; 1 prp; 0-3 aty) % 58.76/58.81 % Number of functors : 9 ( 9 usr; 1 con; 0-2 aty) % 58.76/58.81 % Number of variables : 88 ( 74 !; 14 ?) % 58.76/58.81 % SPC : FOF_THM_RFO_SEQ % 58.76/58.81 % 58.76/58.81 % Comments : Normal version: includes the axioms (which may be theorems from % 58.76/58.81 % other articles) and background that are possibly necessary. % 58.76/58.81 % : Translated by MPTP from the Mizar Mathematical Library 4.48.930. % 58.76/58.81 % : The problem encoding is based on set theory. % 58.76/58.81 %------------------------------------------------------------------------------ % 58.76/58.81 fof(t20_latsubgr,conjecture, % 58.76/58.81 ! [A] : % 58.76/58.81 ( ( ~ v3_struct_0(A) % 58.76/58.81 & v3_group_1(A) % 58.76/58.81 & v4_group_1(A) % 58.76/58.81 & l1_group_1(A) ) % 58.76/58.81 => ! [B] : % 58.76/58.81 ( ( v1_group_1(B) % 58.76/58.81 & m1_group_2(B,A) ) % 58.76/58.81 => k1_funct_1(k1_latsubgr(A),B) != k1_xboole_0 ) ) ). % 58.76/58.81 % 58.76/58.81 fof(abstractness_v1_group_1,axiom, % 58.76/58.81 ! [A] : % 58.76/58.81 ( l1_group_1(A) % 58.76/58.81 => ( v1_group_1(A) % 58.76/58.81 => A = g1_group_1(u1_struct_0(A),u1_group_1(A)) ) ) ). % 58.76/58.81 % 58.76/58.81 fof(antisymmetry_r2_hidden,axiom, % 58.76/58.81 ! [A,B] : % 58.76/58.81 ( r2_hidden(A,B) % 58.76/58.81 => ~ r2_hidden(B,A) ) ). % 58.76/58.81 % 58.76/58.81 fof(cc1_funct_2,axiom, % 58.76/58.81 ! [A,B,C] : % 58.76/58.81 ( m1_relset_1(C,A,B) % 58.76/58.81 => ( ( v1_funct_1(C) % 58.76/58.81 & v1_partfun1(C,A,B) ) % 58.76/58.81 => ( v1_funct_1(C) % 58.76/58.81 & v1_funct_2(C,A,B) ) ) ) ). % 58.76/58.81 % 58.76/58.81 fof(cc1_relset_1,axiom, % 58.76/58.81 ! [A,B,C] : % 58.76/58.81 ( m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))) % 58.76/58.81 => v1_relat_1(C) ) ). % 58.76/58.81 % 58.76/58.81 fof(cc5_funct_2,axiom, % 58.76/58.81 ! [A,B] : % 58.76/58.81 ( ~ v1_xboole_0(B) % 58.76/58.81 => ! [C] : % 58.76/58.81 ( m1_relset_1(C,A,B) % 58.76/58.81 => ( ( v1_funct_1(C) % 58.76/58.81 & v1_funct_2(C,A,B) ) % 58.76/58.81 => ( v1_funct_1(C) % 58.76/58.81 & v1_partfun1(C,A,B) % 58.76/58.81 & v1_funct_2(C,A,B) ) ) ) ) ). % 58.76/58.81 % 58.76/58.81 fof(cc6_funct_2,axiom, % 58.76/58.81 ! [A,B] : % 58.76/58.81 ( ( ~ v1_xboole_0(A) % 58.76/58.81 & ~ v1_xboole_0(B) ) % 58.76/58.81 => ! [C] : % 58.76/58.81 ( m1_relset_1(C,A,B) % 58.76/58.81 => ( ( v1_funct_1(C) % 58.76/58.81 & v1_funct_2(C,A,B) ) % 58.76/58.81 => ( v1_funct_1(C) % 58.76/58.81 & ~ v1_xboole_0(C) % 58.76/58.81 & v1_partfun1(C,A,B) % 58.76/58.81 & v1_funct_2(C,A,B) ) ) ) ) ). % 58.76/58.81 % 58.76/58.81 fof(d1_latsubgr,axiom, % 58.76/58.81 ! [A] : % 58.76/58.81 ( ( ~ v3_struct_0(A) % 58.76/58.81 & v3_group_1(A) % 58.76/58.81 & v4_group_1(A) % 58.76/58.81 & l1_group_1(A) ) % 58.76/58.81 => ! [B] : % 58.76/58.81 ( ( v1_funct_1(B) % 58.76/58.81 & v1_funct_2(B,k1_group_3(A),k1_zfmisc_1(u1_struct_0(A))) % 58.76/58.81 & m2_relset_1(B,k1_group_3(A),k1_zfmisc_1(u1_struct_0(A))) ) % 58.76/58.81 => ( B = k1_latsubgr(A) % 58.76/58.81 <=> ! [C] : % 58.76/58.81 ( ( v1_group_1(C) % 58.76/58.81 & m1_group_2(C,A) ) % 58.76/58.81 => k1_funct_1(B,C) = u1_struct_0(C) ) ) ) ) ). % 58.76/58.81 % 58.76/58.81 fof(dt_g1_group_1,axiom, % 58.76/58.81 ! [A,B] : % 58.76/58.81 ( ( v1_funct_1(B) % 58.76/58.81 & v1_funct_2(B,k2_zfmisc_1(A,A),A) % 58.76/58.81 & m1_relset_1(B,k2_zfmisc_1(A,A),A) ) % 58.76/58.81 => ( v1_group_1(g1_group_1(A,B)) % 58.76/58.81 & l1_group_1(g1_group_1(A,B)) ) ) ). % 58.76/58.81 % 58.76/58.81 fof(dt_k1_funct_1,axiom, % 58.76/58.81 $true ). % 58.76/58.81 % 58.76/58.81 fof(dt_k1_group_3,axiom, % 58.76/58.81 $true ). % 58.76/58.81 % 58.76/58.81 fof(dt_k1_latsubgr,axiom, % 58.76/58.81 ! [A] : % 58.76/58.81 ( ( ~ v3_struct_0(A) % 58.76/58.81 & v3_group_1(A) % 58.76/58.81 & v4_group_1(A) % 58.76/58.81 & l1_group_1(A) ) % 58.76/58.81 => ( v1_funct_1(k1_latsubgr(A)) % 58.76/58.81 & v1_funct_2(k1_latsubgr(A),k1_group_3(A),k1_zfmisc_1(u1_struct_0(A))) % 58.76/58.81 & m2_relset_1(k1_latsubgr(A),k1_group_3(A),k1_zfmisc_1(u1_struct_0(A))) ) ) ). % 58.76/58.81 % 58.76/58.81 fof(dt_k1_xboole_0,axiom, % 58.76/58.81 $true ). % 58.76/58.81 % 58.76/58.81 fof(dt_k1_zfmisc_1,axiom, % 58.76/58.81 $true ). % 58.76/58.81 % 58.76/58.81 fof(dt_k2_zfmisc_1,axiom, % 58.76/58.81 $true ). % 58.76/58.81 % 58.76/58.81 fof(dt_l1_group_1,axiom, % 58.76/58.81 ! [A] : % 58.76/58.81 ( l1_group_1(A) % 58.76/58.81 => l1_struct_0(A) ) ). % 58.76/58.81 % 58.76/58.81 fof(dt_l1_struct_0,axiom, % 58.76/58.81 $true ). % 58.76/58.81 % 58.76/58.81 fof(dt_m1_group_2,axiom, % 58.76/58.81 ! [A] : % 58.76/58.81 ( ( ~ v3_struct_0(A) % 58.76/58.81 & v3_group_1(A) % 58.76/58.81 & l1_group_1(A) ) % 58.76/58.81 => ! [B] : % 58.76/58.81 ( m1_group_2(B,A) % 58.76/58.81 => ( ~ v3_struct_0(B) % 58.76/58.81 & v3_group_1(B) % 58.76/58.81 & l1_group_1(B) ) ) ) ). % 58.76/58.81 % 58.76/58.81 fof(dt_m1_relset_1,axiom, % 58.76/58.81 $true ). % 58.76/58.81 % 58.76/58.81 fof(dt_m1_subset_1,axiom, % 58.76/58.81 $true ). % 58.76/58.81 % 58.76/58.81 fof(dt_m2_relset_1,axiom, % 58.76/58.82 ! [A,B,C] : % 58.76/58.82 ( m2_relset_1(C,A,B) % 58.76/58.82 => m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))) ) ). % 58.76/58.82 % 58.76/58.82 fof(dt_u1_group_1,axiom, % 58.76/58.82 ! [A] : % 58.76/58.82 ( l1_group_1(A) % 58.76/58.82 => ( v1_funct_1(u1_group_1(A)) % 58.76/58.82 & v1_funct_2(u1_group_1(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A)) % 58.76/58.82 & m2_relset_1(u1_group_1(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A)) ) ) ). % 58.76/58.82 % 58.76/58.82 fof(dt_u1_struct_0,axiom, % 58.76/58.82 $true ). % 58.76/58.82 % 58.76/58.82 fof(existence_l1_group_1,axiom, % 58.76/58.82 ? [A] : l1_group_1(A) ). % 58.76/58.82 % 58.76/58.82 fof(existence_l1_struct_0,axiom, % 58.76/58.82 ? [A] : l1_struct_0(A) ). % 58.76/58.82 % 58.76/58.82 fof(existence_m1_group_2,axiom, % 58.76/58.82 ! [A] : % 58.76/58.82 ( ( ~ v3_struct_0(A) % 58.76/58.82 & v3_group_1(A) % 58.76/58.82 & l1_group_1(A) ) % 58.76/58.82 => ? [B] : m1_group_2(B,A) ) ). % 58.76/58.82 % 58.76/58.82 fof(existence_m1_relset_1,axiom, % 58.76/58.82 ! [A,B] : % 58.76/58.82 ? [C] : m1_relset_1(C,A,B) ). % 58.76/58.82 % 58.76/58.82 fof(existence_m1_subset_1,axiom, % 58.76/58.82 ! [A] : % 58.76/58.82 ? [B] : m1_subset_1(B,A) ). % 58.76/58.82 % 58.76/58.82 fof(existence_m2_relset_1,axiom, % 58.76/58.82 ! [A,B] : % 58.76/58.82 ? [C] : m2_relset_1(C,A,B) ). % 58.76/58.82 % 58.76/58.82 fof(fc1_group_3,axiom, % 58.76/58.82 ! [A] : % 58.76/58.82 ( ( ~ v3_struct_0(A) % 58.76/58.82 & v3_group_1(A) % 58.76/58.82 & v4_group_1(A) % 58.76/58.82 & l1_group_1(A) ) % 58.76/58.82 => ~ v1_xboole_0(k1_group_3(A)) ) ). % 58.76/58.82 % 58.76/58.82 fof(fc1_struct_0,axiom, % 58.76/58.82 ! [A] : % 58.76/58.82 ( ( ~ v3_struct_0(A) % 58.76/58.82 & l1_struct_0(A) ) % 58.76/58.82 => ~ v1_xboole_0(u1_struct_0(A)) ) ). % 58.76/58.82 % 58.76/58.82 fof(fc1_subset_1,axiom, % 58.76/58.82 ! [A] : ~ v1_xboole_0(k1_zfmisc_1(A)) ). % 58.76/58.82 % 58.76/58.82 fof(fc1_xboole_0,axiom, % 58.76/58.82 v1_xboole_0(k1_xboole_0) ). % 58.76/58.82 % 58.76/58.82 fof(fc4_subset_1,axiom, % 58.76/58.82 ! [A,B] : % 58.76/58.82 ( ( ~ v1_xboole_0(A) % 58.76/58.82 & ~ v1_xboole_0(B) ) % 58.76/58.82 => ~ v1_xboole_0(k2_zfmisc_1(A,B)) ) ). % 58.76/58.82 % 58.76/58.82 fof(free_g1_group_1,axiom, % 58.76/58.82 ! [A,B] : % 58.76/58.82 ( ( v1_funct_1(B) % 58.76/58.82 & v1_funct_2(B,k2_zfmisc_1(A,A),A) % 58.76/58.82 & m1_relset_1(B,k2_zfmisc_1(A,A),A) ) % 58.76/58.82 => ! [C,D] : % 58.76/58.82 ( g1_group_1(A,B) = g1_group_1(C,D) % 58.76/58.82 => ( A = C % 58.76/58.82 & B = D ) ) ) ). % 58.76/58.82 % 58.76/58.82 fof(rc1_funct_2,axiom, % 58.76/58.82 ! [A,B] : % 58.76/58.82 ? [C] : % 58.76/58.82 ( m1_relset_1(C,A,B) % 58.76/58.82 & v1_relat_1(C) % 58.76/58.82 & v1_funct_1(C) % 58.76/58.82 & v1_funct_2(C,A,B) ) ). % 58.76/58.82 % 58.76/58.82 fof(rc1_subset_1,axiom, % 58.76/58.82 ! [A] : % 58.76/58.82 ( ~ v1_xboole_0(A) % 58.76/58.82 => ? [B] : % 58.76/58.82 ( m1_subset_1(B,k1_zfmisc_1(A)) % 58.76/58.82 & ~ v1_xboole_0(B) ) ) ). % 58.76/58.82 % 58.76/58.82 fof(rc1_xboole_0,axiom, % 58.76/58.82 ? [A] : v1_xboole_0(A) ). % 58.76/58.82 % 58.76/58.82 fof(rc2_partfun1,axiom, % 58.76/58.82 ! [A,B] : % 58.76/58.82 ? [C] : % 58.76/58.82 ( m1_relset_1(C,A,B) % 58.76/58.82 & v1_relat_1(C) % 58.76/58.82 & v1_funct_1(C) ) ). % 58.76/58.82 % 58.76/58.82 fof(rc2_subset_1,axiom, % 58.76/58.82 ! [A] : % 58.76/58.82 ? [B] : % 58.76/58.82 ( m1_subset_1(B,k1_zfmisc_1(A)) % 58.76/58.82 & v1_xboole_0(B) ) ). % 58.76/58.82 % 58.76/58.82 fof(rc2_xboole_0,axiom, % 58.76/58.82 ? [A] : ~ v1_xboole_0(A) ). % 58.76/58.82 % 58.76/58.82 fof(rc3_struct_0,axiom, % 58.76/58.82 ? [A] : % 58.76/58.82 ( l1_struct_0(A) % 58.76/58.82 & ~ v3_struct_0(A) ) ). % 58.76/58.82 % 58.76/58.82 fof(rc5_struct_0,axiom, % 58.76/58.82 ! [A] : % 58.76/58.82 ( ( ~ v3_struct_0(A) % 58.76/58.82 & l1_struct_0(A) ) % 58.76/58.82 => ? [B] : % 58.76/58.82 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 58.76/58.82 & ~ v1_xboole_0(B) ) ) ). % 58.76/58.82 % 58.76/58.82 fof(redefinition_m2_relset_1,axiom, % 58.76/58.82 ! [A,B,C] : % 58.76/58.82 ( m2_relset_1(C,A,B) % 58.76/58.82 <=> m1_relset_1(C,A,B) ) ). % 58.76/58.82 % 58.76/58.82 fof(reflexivity_r1_tarski,axiom, % 58.76/58.82 ! [A,B] : r1_tarski(A,A) ). % 58.76/58.82 % 58.76/58.82 fof(t1_subset,axiom, % 58.76/58.82 ! [A,B] : % 58.76/58.82 ( r2_hidden(A,B) % 58.76/58.82 => m1_subset_1(A,B) ) ). % 58.76/58.82 % 58.76/58.82 fof(t2_subset,axiom, % 58.76/58.82 ! [A,B] : % 58.76/58.82 ( m1_subset_1(A,B) % 58.76/58.82 => ( v1_xboole_0(B) % 58.76/58.82 | r2_hidden(A,B) ) ) ). % 58.76/58.82 % 58.76/58.82 fof(t3_subset,axiom, % 58.76/58.82 ! [A,B] : % 58.76/58.82 ( m1_subset_1(A,k1_zfmisc_1(B)) % 58.76/58.82 <=> r1_tarski(A,B) ) ). % 58.76/58.82 % 58.76/58.82 fof(t4_subset,axiom, % 58.76/58.82 ! [A,B,C] : % 58.76/58.82 ( ( r2_hidden(A,B) % 58.76/58.82 & m1_subset_1(B,k1_zfmisc_1(C)) ) % 58.76/58.82 => m1_subset_1(A,C) ) ). % 58.76/58.82 % 58.76/58.82 fof(t5_subset,axiom, % 58.76/58.82 ! [A,B,C] : % 58.76/58.82 ~ ( r2_hidden(A,B) % 58.76/58.82 & m1_subset_1(B,k1_zfmisc_1(C)) % 58.76/58.82 & v1_xboole_0(C) ) ). % 58.76/58.82 % 58.76/58.82 fof(t6_boole,axiom, % 58.76/58.82 ! [A] : % 58.76/58.82 ( v1_xboole_0(A) % 58.76/58.82 => A = k1_xboole_0 ) ). % 58.76/58.82 % 58.76/58.82 fof(t7_boole,axiom, % 58.76/58.82 ! [A,B] : % 58.76/58.82 ~ ( r2_hidden(A,B) % 58.76/58.82 & v1_xboole_0(B) ) ). % 58.76/58.82 % 58.76/58.82 fof(t8_boole,axiom, % 58.76/58.82 ! [A,B] : % 58.76/58.82 ~ ( v1_xboole_0(A) % 58.76/58.82 & A != B % 58.76/58.82 & v1_xboole_0(B) ) ). % 58.76/58.82 % 58.76/58.82 %------------------------------------------------------------------------------ % 58.76/58.82 %------------------------------------------- % 58.76/58.82 % Proof found % 58.76/58.82 % SZS status Theorem for theBenchmark % 58.76/58.82 % SZS output start Proof % 58.76/58.82 %ClaNum:131(EqnAxiom:58) % 58.76/58.82 %VarNum:335(SingletonVarNum:109) % 58.76/58.82 %MaxLitNum:11 % 58.76/58.82 %MaxfuncDepth:2 % 58.76/58.82 %SharedTerms:24 % 58.76/58.82 %goalClause: 59 60 61 63 69 71 83 % 58.76/58.82 %singleGoalClaCount:7 % 58.76/58.82 [59]P1(a1) % 58.76/58.82 [60]P16(a1) % 58.76/58.82 [61]P2(a1) % 58.76/58.82 [62]P2(a10) % 58.76/58.82 [63]P3(a11) % 58.76/58.82 [64]P13(a13) % 58.76/58.82 [65]P13(a2) % 58.76/58.82 [66]P4(a14) % 58.76/58.82 [67]P4(a5) % 58.76/58.82 [69]P5(a11,a1) % 58.76/58.82 [83]~P17(a1) % 58.76/58.82 [84]~P17(a5) % 58.76/58.82 [85]~P13(a8) % 58.76/58.82 [71]E(f16(f15(a1),a11),a13) % 58.76/58.82 [70]P6(x701,x701) % 58.76/58.82 [68]P13(f6(x681)) % 58.76/58.82 [72]P7(f17(x721),x721) % 58.76/58.82 [73]P7(f6(x731),f23(x731)) % 58.76/58.82 [86]~P13(f23(x861)) % 58.76/58.82 [74]P10(f3(x741,x742)) % 58.76/58.82 [75]P10(f7(x751,x752)) % 58.76/58.82 [76]P14(f3(x761,x762)) % 58.76/58.82 [77]P14(f7(x771,x772)) % 58.76/58.82 [78]P8(f18(x781,x782),x781,x782) % 58.76/58.82 [79]P8(f3(x791,x792),x791,x792) % 58.76/58.82 [80]P8(f7(x801,x802),x801,x802) % 58.76/58.82 [81]P12(f3(x811,x812),x811,x812) % 58.76/58.82 [82]P9(f20(x821,x822),x821,x822) % 58.76/58.82 [87]~P13(x871)+E(x871,a13) % 58.76/58.82 [88]~P2(x881)+P4(x881) % 58.76/58.82 [90]~P2(x901)+P10(f24(x901)) % 58.76/58.82 [91]P13(x911)+~P13(f4(x911)) % 58.76/58.82 [95]P13(x951)+P7(f4(x951),f23(x951)) % 58.76/58.82 [115]~P2(x1151)+P12(f24(x1151),f25(f26(x1151),f26(x1151)),f26(x1151)) % 58.76/58.82 [116]~P2(x1161)+P9(f24(x1161),f25(f26(x1161),f26(x1161)),f26(x1161)) % 58.76/58.82 [94]~P13(x941)+~P11(x942,x941) % 58.76/58.82 [97]~P11(x971,x972)+P7(x971,x972) % 58.76/58.82 [103]~P11(x1032,x1031)+~P11(x1031,x1032) % 58.76/58.82 [102]~P6(x1021,x1022)+P7(x1021,f23(x1022)) % 58.76/58.82 [106]P6(x1061,x1062)+~P7(x1061,f23(x1062)) % 58.76/58.82 [117]~P9(x1171,x1172,x1173)+P8(x1171,x1172,x1173) % 58.76/58.82 [118]~P8(x1181,x1182,x1183)+P9(x1181,x1182,x1183) % 58.76/58.82 [114]P14(x1141)+~P7(x1141,f23(f25(x1142,x1143))) % 58.76/58.82 [119]~P9(x1191,x1192,x1193)+P7(x1191,f23(f25(x1192,x1193))) % 58.76/58.82 [92]~P4(x921)+P17(x921)+~P13(f26(x921)) % 58.76/58.82 [93]~P4(x931)+P17(x931)+~P13(f9(x931)) % 58.76/58.82 [100]~P2(x1001)+~P3(x1001)+E(f21(f26(x1001),f24(x1001)),x1001) % 58.76/58.82 [108]~P4(x1081)+P17(x1081)+P7(f9(x1081),f23(f26(x1081))) % 58.76/58.82 [89]~P13(x892)+~P13(x891)+E(x891,x892) % 58.76/58.82 [99]~P7(x992,x991)+P13(x991)+P11(x992,x991) % 58.76/58.82 [109]P13(x1091)+P13(x1092)+~P13(f25(x1092,x1091)) % 58.76/58.82 [110]~P13(x1101)+~P11(x1102,x1103)+~P7(x1103,f23(x1101)) % 58.76/58.82 [111]P7(x1111,x1112)+~P11(x1111,x1113)+~P7(x1113,f23(x1112)) % 58.76/58.82 [98]~P1(x981)+~P2(x981)+P17(x981)+P5(f19(x981),x981) % 58.76/58.82 [124]~P10(x1242)+~P8(x1242,f25(x1241,x1241),x1241)+~P12(x1242,f25(x1241,x1241),x1241)+P2(f21(x1241,x1242)) % 58.76/58.82 [125]~P10(x1252)+~P8(x1252,f25(x1251,x1251),x1251)+~P12(x1252,f25(x1251,x1251),x1251)+P3(f21(x1251,x1252)) % 58.76/58.82 [121]~P10(x1211)+~P8(x1211,x1212,x1213)+~P15(x1211,x1212,x1213)+P12(x1211,x1212,x1213) % 58.76/58.82 [96]~P1(x961)+~P16(x961)+~P2(x961)+P17(x961)+P10(f15(x961)) % 58.76/58.82 [101]~P1(x1011)+~P16(x1011)+~P2(x1011)+P17(x1011)+~P13(f22(x1011)) % 58.76/58.82 [112]~P1(x1121)+~P16(x1121)+~P2(x1121)+P17(x1121)+P12(f15(x1121),f22(x1121),f23(f26(x1121))) % 58.76/58.82 [113]~P1(x1131)+~P16(x1131)+~P2(x1131)+P17(x1131)+P9(f15(x1131),f22(x1131),f23(f26(x1131))) % 58.76/58.82 [104]~P1(x1041)+~P2(x1041)+~P5(x1042,x1041)+P17(x1041)+P1(x1042) % 58.76/58.82 [105]~P1(x1051)+~P2(x1051)+~P5(x1052,x1051)+P17(x1051)+P2(x1052) % 58.76/58.82 [107]~P1(x1071)+~P2(x1071)+~P5(x1072,x1071)+P17(x1071)+~P17(x1072) % 58.76/58.82 [122]~P10(x1222)+~P8(x1222,x1223,x1221)+~P12(x1222,x1223,x1221)+P13(x1221)+P15(x1222,x1223,x1221) % 58.76/58.82 [126]~P10(x1261)+E(x1261,x1262)+~P8(x1261,f25(x1263,x1263),x1263)+~P12(x1261,f25(x1263,x1263),x1263)+~E(f21(x1263,x1261),f21(x1264,x1262)) % 58.76/58.82 [127]~P10(x1273)+E(x1271,x1272)+~P8(x1273,f25(x1271,x1271),x1271)+~P12(x1273,f25(x1271,x1271),x1271)+~E(f21(x1271,x1273),f21(x1272,x1274)) % 58.76/58.82 [120]~P13(x1203)+~P8(x1203,x1202,x1201)+~P12(x1203,x1202,x1201)+P13(x1201)+P13(x1202)+~P10(x1203) % 58.76/58.82 [128]P17(x1282)+~P1(x1282)+~P16(x1282)+~P2(x1282)+~P10(x1281)+E(x1281,f15(x1282))+~P12(x1281,f22(x1282),f23(f26(x1282)))+~P9(x1281,f22(x1282),f23(f26(x1282)))+P3(f12(x1282,x1281)) % 58.76/58.82 [129]P17(x1292)+~P1(x1292)+~P16(x1292)+~P2(x1292)+~P10(x1291)+P5(f12(x1292,x1291),x1292)+E(x1291,f15(x1292))+~P12(x1291,f22(x1292),f23(f26(x1292)))+~P9(x1291,f22(x1292),f23(f26(x1292))) % 58.76/58.82 [131]P17(x1312)+~P1(x1312)+~P16(x1312)+~P2(x1312)+~P10(x1311)+E(x1311,f15(x1312))+~P12(x1311,f22(x1312),f23(f26(x1312)))+~P9(x1311,f22(x1312),f23(f26(x1312)))+~E(f16(x1311,f12(x1312,x1311)),f26(f12(x1312,x1311))) % 58.76/58.82 [130]~P1(x1303)+~P16(x1303)+~P2(x1303)+~P3(x1302)+~P10(x1301)+~P5(x1302,x1303)+P17(x1303)+~E(x1301,f15(x1303))+E(f16(x1301,x1302),f26(x1302))+~P12(x1301,f22(x1303),f23(f26(x1303)))+~P9(x1301,f22(x1303),f23(f26(x1303))) % 58.76/58.82 %EqnAxiom % 58.76/58.82 [1]E(x11,x11) % 58.76/58.82 [2]E(x22,x21)+~E(x21,x22) % 58.76/58.82 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 58.76/58.82 [4]~E(x41,x42)+E(f6(x41),f6(x42)) % 58.76/58.82 [5]~E(x51,x52)+E(f15(x51),f15(x52)) % 58.76/58.82 [6]~E(x61,x62)+E(f16(x61,x63),f16(x62,x63)) % 58.76/58.82 [7]~E(x71,x72)+E(f16(x73,x71),f16(x73,x72)) % 58.76/58.82 [8]~E(x81,x82)+E(f17(x81),f17(x82)) % 58.76/58.82 [9]~E(x91,x92)+E(f23(x91),f23(x92)) % 58.76/58.82 [10]~E(x101,x102)+E(f12(x101,x103),f12(x102,x103)) % 58.76/58.82 [11]~E(x111,x112)+E(f12(x113,x111),f12(x113,x112)) % 58.76/58.82 [12]~E(x121,x122)+E(f3(x121,x123),f3(x122,x123)) % 58.76/58.82 [13]~E(x131,x132)+E(f3(x133,x131),f3(x133,x132)) % 58.76/58.82 [14]~E(x141,x142)+E(f7(x141,x143),f7(x142,x143)) % 58.76/58.82 [15]~E(x151,x152)+E(f7(x153,x151),f7(x153,x152)) % 58.76/58.82 [16]~E(x161,x162)+E(f26(x161),f26(x162)) % 58.76/58.82 [17]~E(x171,x172)+E(f25(x171,x173),f25(x172,x173)) % 58.76/58.82 [18]~E(x181,x182)+E(f25(x183,x181),f25(x183,x182)) % 58.76/58.82 [19]~E(x191,x192)+E(f18(x191,x193),f18(x192,x193)) % 58.76/58.82 [20]~E(x201,x202)+E(f18(x203,x201),f18(x203,x202)) % 58.76/58.82 [21]~E(x211,x212)+E(f22(x211),f22(x212)) % 58.76/58.82 [22]~E(x221,x222)+E(f24(x221),f24(x222)) % 58.76/58.82 [23]~E(x231,x232)+E(f21(x231,x233),f21(x232,x233)) % 58.76/58.82 [24]~E(x241,x242)+E(f21(x243,x241),f21(x243,x242)) % 58.76/58.82 [25]~E(x251,x252)+E(f20(x251,x253),f20(x252,x253)) % 58.76/58.82 [26]~E(x261,x262)+E(f20(x263,x261),f20(x263,x262)) % 58.76/58.82 [27]~E(x271,x272)+E(f19(x271),f19(x272)) % 58.76/58.82 [28]~E(x281,x282)+E(f9(x281),f9(x282)) % 58.76/58.82 [29]~E(x291,x292)+E(f4(x291),f4(x292)) % 58.76/58.82 [30]~P1(x301)+P1(x302)+~E(x301,x302) % 58.76/58.82 [31]~P16(x311)+P16(x312)+~E(x311,x312) % 58.76/58.82 [32]~P2(x321)+P2(x322)+~E(x321,x322) % 58.76/58.82 [33]~P3(x331)+P3(x332)+~E(x331,x332) % 58.76/58.82 [34]P12(x342,x343,x344)+~E(x341,x342)+~P12(x341,x343,x344) % 58.76/58.82 [35]P12(x353,x352,x354)+~E(x351,x352)+~P12(x353,x351,x354) % 58.76/58.82 [36]P12(x363,x364,x362)+~E(x361,x362)+~P12(x363,x364,x361) % 58.76/58.82 [37]~P13(x371)+P13(x372)+~E(x371,x372) % 58.76/58.82 [38]~P10(x381)+P10(x382)+~E(x381,x382) % 58.76/58.82 [39]~P4(x391)+P4(x392)+~E(x391,x392) % 58.76/58.82 [40]P7(x402,x403)+~E(x401,x402)+~P7(x401,x403) % 58.76/58.83 [41]P7(x413,x412)+~E(x411,x412)+~P7(x413,x411) % 58.76/58.83 [42]P8(x422,x423,x424)+~E(x421,x422)+~P8(x421,x423,x424) % 58.76/58.83 [43]P8(x433,x432,x434)+~E(x431,x432)+~P8(x433,x431,x434) % 58.76/58.83 [44]P8(x443,x444,x442)+~E(x441,x442)+~P8(x443,x444,x441) % 58.76/58.83 [45]P5(x452,x453)+~E(x451,x452)+~P5(x451,x453) % 58.76/58.83 [46]P5(x463,x462)+~E(x461,x462)+~P5(x463,x461) % 58.76/58.83 [47]P6(x472,x473)+~E(x471,x472)+~P6(x471,x473) % 58.76/58.83 [48]P6(x483,x482)+~E(x481,x482)+~P6(x483,x481) % 58.76/58.83 [49]~P17(x491)+P17(x492)+~E(x491,x492) % 58.76/58.83 [50]P11(x502,x503)+~E(x501,x502)+~P11(x501,x503) % 58.76/58.83 [51]P11(x513,x512)+~E(x511,x512)+~P11(x513,x511) % 58.76/58.83 [52]P9(x522,x523,x524)+~E(x521,x522)+~P9(x521,x523,x524) % 58.76/58.83 [53]P9(x533,x532,x534)+~E(x531,x532)+~P9(x533,x531,x534) % 58.76/58.83 [54]P9(x543,x544,x542)+~E(x541,x542)+~P9(x543,x544,x541) % 58.76/58.83 [55]~P14(x551)+P14(x552)+~E(x551,x552) % 58.76/58.83 [56]P15(x562,x563,x564)+~E(x561,x562)+~P15(x561,x563,x564) % 58.76/58.83 [57]P15(x573,x572,x574)+~E(x571,x572)+~P15(x573,x571,x574) % 58.76/58.83 [58]P15(x583,x584,x582)+~E(x581,x582)+~P15(x583,x584,x581) % 58.76/58.83 % 58.76/58.83 %------------------------------------------- % 58.76/58.83 cnf(134,plain, % 58.76/58.83 (~P16(x1341)+~P2(x1341)+~P5(x1342,x1341)+P17(x1341)+~P1(x1341)+~P3(x1342)+~P10(f15(x1341))+E(f16(f15(x1341),x1342),f26(x1342))+~P12(f15(x1341),f22(x1341),f23(f26(x1341)))+~P9(f15(x1341),f22(x1341),f23(f26(x1341)))), % 58.76/58.83 inference(equality_inference,[],[130])). % 58.76/58.83 cnf(135,plain, % 58.76/58.83 (E(a13,f16(f15(a1),a11))), % 58.76/58.83 inference(scs_inference,[],[71,2])). % 58.76/58.83 cnf(136,plain, % 58.76/58.83 (~P11(x1361,a13)), % 58.76/58.83 inference(scs_inference,[],[71,64,2,94])). % 58.76/58.83 cnf(138,plain, % 58.76/58.83 (P6(f17(f23(x1381)),x1381)), % 58.76/58.83 inference(scs_inference,[],[71,72,64,2,94,106])). % 58.76/58.83 cnf(139,plain, % 58.76/58.83 (P7(f17(x1391),x1391)), % 58.76/58.83 inference(rename_variables,[],[72])). % 58.76/58.83 cnf(142,plain, % 58.76/58.83 (P7(f17(x1421),x1421)), % 58.76/58.83 inference(rename_variables,[],[72])). % 58.76/58.83 cnf(144,plain, % 58.76/58.83 (P12(f3(f16(f15(a1),a11),x1441),a13,x1441)), % 58.76/58.83 inference(scs_inference,[],[71,81,72,139,64,2,94,106,114,35])). % 58.76/58.83 cnf(145,plain, % 58.76/58.83 (P12(f3(x1451,x1452),x1451,x1452)), % 58.76/58.83 inference(rename_variables,[],[81])). % 58.76/58.83 cnf(147,plain, % 58.76/58.83 (P12(f3(x1471,x1472),x1471,x1472)), % 58.76/58.83 inference(rename_variables,[],[81])). % 58.76/58.83 cnf(148,plain, % 58.76/58.83 (P13(f16(f15(a1),a11))), % 58.76/58.83 inference(scs_inference,[],[71,81,145,72,139,64,2,94,106,114,35,36,37])). % 58.76/58.83 cnf(150,plain, % 58.76/58.83 (P7(f17(x1501),x1501)), % 58.76/58.83 inference(rename_variables,[],[72])). % 58.76/58.83 cnf(152,plain, % 58.76/58.83 (P8(f18(x1521,x1522),x1521,x1522)), % 58.76/58.83 inference(rename_variables,[],[78])). % 58.76/58.83 cnf(155,plain, % 58.76/58.83 (P6(a13,f16(f15(a1),a11))), % 58.76/58.83 inference(scs_inference,[],[71,70,78,152,81,145,72,139,142,64,2,94,106,114,35,36,37,41,43,44,47])). % 58.76/58.83 cnf(156,plain, % 58.76/58.83 (P6(x1561,x1561)), % 58.76/58.83 inference(rename_variables,[],[70])). % 58.76/58.83 cnf(157,plain, % 58.76/58.83 (P6(f16(f15(a1),a11),a13)), % 58.76/58.83 inference(scs_inference,[],[71,70,156,78,152,81,145,72,139,142,64,2,94,106,114,35,36,37,41,43,44,47,48])). % 58.76/58.83 cnf(159,plain, % 58.76/58.83 (P9(f20(f16(f15(a1),a11),x1591),a13,x1591)), % 58.76/58.83 inference(scs_inference,[],[71,70,156,78,152,81,145,82,72,139,142,64,2,94,106,114,35,36,37,41,43,44,47,48,53])). % 58.76/58.83 cnf(160,plain, % 58.76/58.83 (P9(f20(x1601,x1602),x1601,x1602)), % 58.76/58.83 inference(rename_variables,[],[82])). % 58.76/58.83 cnf(161,plain, % 58.76/58.83 (P9(f20(x1611,f16(f15(a1),a11)),x1611,a13)), % 58.76/58.83 inference(scs_inference,[],[71,70,156,78,152,81,145,82,160,72,139,142,64,2,94,106,114,35,36,37,41,43,44,47,48,53,54])). % 58.76/58.83 cnf(163,plain, % 58.76/58.83 (P11(f17(a8),a8)), % 58.76/58.83 inference(scs_inference,[],[71,70,156,78,152,81,145,82,160,72,139,142,150,64,85,2,94,106,114,35,36,37,41,43,44,47,48,53,54,99])). % 58.76/58.83 cnf(164,plain, % 58.76/58.83 (P7(f17(x1641),x1641)), % 58.76/58.83 inference(rename_variables,[],[72])). % 58.76/58.83 cnf(166,plain, % 58.76/58.83 (~P11(x1661,f17(f23(a13)))), % 58.76/58.83 inference(scs_inference,[],[71,70,156,78,152,81,145,82,160,72,139,142,150,164,64,85,2,94,106,114,35,36,37,41,43,44,47,48,53,54,99,110])). % 58.76/58.83 cnf(169,plain, % 58.76/58.83 (P1(a11)), % 58.76/58.83 inference(scs_inference,[],[59,61,69,83,71,70,156,78,152,81,145,82,160,72,139,142,150,164,64,85,2,94,106,114,35,36,37,41,43,44,47,48,53,54,99,110,104])). % 58.76/58.84 cnf(171,plain, % 58.76/58.84 (P2(a11)), % 58.76/58.84 inference(scs_inference,[],[59,61,69,83,71,70,156,78,152,81,145,82,160,72,139,142,150,164,64,85,2,94,106,114,35,36,37,41,43,44,47,48,53,54,99,110,104,105])). % 58.76/58.84 cnf(173,plain, % 58.76/58.84 (~P17(a11)), % 58.76/58.84 inference(scs_inference,[],[59,61,69,83,71,70,156,78,152,81,145,82,160,72,139,142,150,164,64,85,2,94,106,114,35,36,37,41,43,44,47,48,53,54,99,110,104,105,107])). % 58.76/58.84 cnf(176,plain, % 58.76/58.84 (P12(f3(x1761,x1762),x1761,x1762)), % 58.76/58.84 inference(rename_variables,[],[81])). % 58.76/58.84 cnf(177,plain, % 58.76/58.84 (P10(f3(x1771,x1772))), % 58.76/58.84 inference(rename_variables,[],[74])). % 58.76/58.84 cnf(178,plain, % 58.76/58.84 (P8(f3(x1781,x1782),x1781,x1782)), % 58.76/58.84 inference(rename_variables,[],[79])). % 58.76/58.84 cnf(180,plain, % 58.76/58.84 (~P13(f3(a8,a8))), % 58.76/58.84 inference(scs_inference,[],[59,61,69,83,71,70,156,78,152,79,178,81,145,147,176,82,160,72,139,142,150,164,64,85,74,177,2,94,106,114,35,36,37,41,43,44,47,48,53,54,99,110,104,105,107,122,120])). % 58.76/58.84 cnf(188,plain, % 58.76/58.84 (~E(a8,a13)), % 58.76/58.84 inference(scs_inference,[],[59,61,69,83,71,70,156,78,152,79,178,81,145,147,176,82,160,72,139,142,150,164,64,85,74,177,2,94,106,114,35,36,37,41,43,44,47,48,53,54,99,110,104,105,107,122,120,103,30,51])). % 58.76/58.84 cnf(189,plain, % 58.76/58.84 (P15(f3(f16(f15(a1),a11),a8),a13,a8)), % 58.76/58.84 inference(scs_inference,[],[59,61,69,83,71,70,156,78,152,79,178,81,145,147,176,82,160,72,139,142,150,164,64,85,74,177,2,94,106,114,35,36,37,41,43,44,47,48,53,54,99,110,104,105,107,122,120,103,30,51,57])). % 58.76/58.84 cnf(197,plain, % 58.76/58.84 (P6(f6(x1971),x1971)), % 58.76/58.84 inference(scs_inference,[],[73,106])). % 58.76/58.84 cnf(199,plain, % 58.76/58.84 (~P11(x1991,f16(f15(a1),a11))), % 58.76/58.84 inference(scs_inference,[],[148,73,106,94])). % 58.76/58.84 cnf(201,plain, % 58.76/58.84 (P14(f6(f25(x2011,x2012)))), % 58.76/58.84 inference(scs_inference,[],[148,73,106,94,114])). % 58.76/58.84 cnf(202,plain, % 58.76/58.84 (P7(f6(x2021),f23(x2021))), % 58.76/58.84 inference(rename_variables,[],[73])). % 58.76/58.84 cnf(204,plain, % 58.76/58.84 (~P11(x2041,f6(f16(f15(a1),a11)))), % 58.76/58.84 inference(scs_inference,[],[148,73,202,106,94,114,110])). % 58.76/58.84 cnf(207,plain, % 58.76/58.84 (P11(f17(f3(a8,a8)),f3(a8,a8))), % 58.76/58.84 inference(scs_inference,[],[148,73,202,180,72,106,94,114,110,99])). % 58.76/58.84 cnf(211,plain, % 58.76/58.84 (P8(f7(x2111,x2112),x2111,x2112)), % 58.76/58.84 inference(rename_variables,[],[80])). % 58.76/58.84 cnf(216,plain, % 58.76/58.84 (P15(f3(x2161,f3(a8,a8)),x2161,f3(a8,a8))), % 58.76/58.84 inference(scs_inference,[],[71,148,166,80,211,73,202,180,163,79,81,72,74,106,94,114,110,99,43,51,44,122])). % 58.76/58.84 cnf(235,plain, % 58.76/58.84 (P6(f6(f16(f15(a1),a11)),a13)), % 58.76/58.84 inference(scs_inference,[],[71,197,65,94,48])). % 58.76/58.84 cnf(237,plain, % 58.76/58.84 (P11(f17(f23(x2371)),f23(x2371))), % 58.76/58.84 inference(scs_inference,[],[71,197,65,86,72,94,48,99])). % 58.76/58.84 cnf(238,plain, % 58.76/58.84 (P7(f17(x2381),x2381)), % 58.76/58.84 inference(rename_variables,[],[72])). % 58.76/58.84 cnf(242,plain, % 58.76/58.84 (P8(f3(x2421,f16(f15(a1),a11)),x2421,a13)), % 58.76/58.84 inference(scs_inference,[],[71,197,204,207,65,86,79,72,94,48,99,51,44])). % 58.76/58.84 cnf(243,plain, % 58.76/58.84 (P8(f3(x2431,x2432),x2431,x2432)), % 58.76/58.84 inference(rename_variables,[],[79])). % 58.76/58.84 cnf(244,plain, % 58.76/58.84 (P8(f3(f16(f15(a1),a11),x2441),a13,x2441)), % 58.76/58.84 inference(scs_inference,[],[71,197,204,207,65,86,79,243,72,94,48,99,51,44,43])). % 58.76/58.84 cnf(251,plain, % 58.76/58.84 (P7(x2511,x2512)+~P11(x2511,f17(f23(x2512)))), % 58.76/58.84 inference(scs_inference,[],[71,159,197,204,207,65,86,79,243,72,238,94,48,99,51,44,43,103,50,52,55,111])). % 58.76/58.84 cnf(262,plain, % 58.76/58.84 (P11(f6(x2621),f23(x2621))), % 58.76/58.84 inference(scs_inference,[],[73,68,86,94,99])). % 58.76/58.84 cnf(286,plain, % 58.76/58.84 (P10(f3(x2861,x2862))), % 58.76/58.84 inference(rename_variables,[],[74])). % 58.76/58.84 cnf(289,plain, % 58.76/58.84 (~P13(f3(f23(x2891),f23(x2891)))), % 58.76/58.84 inference(scs_inference,[],[144,244,81,79,237,86,136,74,286,51,122,120])). % 58.76/58.84 cnf(383,plain, % 58.76/58.84 (~P13(f4(a8))), % 58.76/58.84 inference(scs_inference,[],[188,87,91])). % 58.76/58.84 cnf(384,plain, % 58.76/58.84 (P11(f17(f4(a8)),f4(a8))), % 58.76/58.84 inference(scs_inference,[],[72,383,99])). % 58.76/58.84 cnf(389,plain, % 58.76/58.84 (~P11(f4(a8),f17(f4(a8)))), % 58.76/58.84 inference(scs_inference,[],[72,383,199,99,51,103])). % 58.76/58.84 cnf(405,plain, % 58.76/58.84 (P15(x4051,x4052,f3(a8,a8))+~E(f3(x4052,f3(a8,a8)),x4051)), % 58.76/58.84 inference(scs_inference,[],[242,82,216,189,138,384,136,51,58,52,42,47,56])). % 58.76/58.84 cnf(430,plain, % 58.76/58.84 (~E(f4(a8),f17(f23(a13)))), % 58.76/58.84 inference(scs_inference,[],[384,166,51])). % 58.76/58.84 cnf(494,plain, % 58.76/58.84 (P15(f3(x4941,f23(x4942)),x4941,f23(x4942))), % 58.76/58.84 inference(scs_inference,[],[81,79,86,74,122])). % 58.76/58.84 cnf(499,plain, % 58.76/58.84 (P15(f3(x4991,f23(x4992)),x4991,x4993)+~E(f23(x4992),x4993)), % 58.76/58.84 inference(scs_inference,[],[81,79,86,74,122,58])). % 58.76/58.84 cnf(500,plain, % 58.76/58.84 (P15(x5001,x5002,f23(x5003))+~E(f3(x5002,f23(x5003)),x5001)), % 58.76/58.84 inference(scs_inference,[],[81,79,86,74,122,58,56])). % 58.76/58.84 cnf(948,plain, % 58.76/58.84 (P7(f4(a8),f23(a8))), % 58.76/58.84 inference(scs_inference,[],[163,95,94])). % 58.76/58.84 cnf(1026,plain, % 58.76/58.84 (P11(f6(f16(f15(a1),a11)),f23(a13))), % 58.76/58.84 inference(scs_inference,[],[235,86,102,99])). % 58.76/58.84 cnf(1027,plain, % 58.76/58.84 (P11(x10271,f23(a13))+~E(f6(f16(f15(a1),a11)),x10271)), % 58.76/58.84 inference(scs_inference,[],[1026,50])). % 58.76/58.84 cnf(2060,plain, % 58.76/58.84 (E(f6(a13),f6(f16(f15(a1),a11)))), % 58.76/58.84 inference(scs_inference,[],[71,4,2])). % 58.76/58.84 cnf(4494,plain, % 58.76/58.84 (E(f25(x44941,a13),f25(x44941,f16(f15(a1),a11)))), % 58.76/58.84 inference(scs_inference,[],[71,18,2])). % 58.76/58.84 cnf(11893,plain, % 58.76/58.84 (P8(f18(a13,x118931),f16(f15(a1),a11),x118931)), % 58.76/58.84 inference(scs_inference,[],[135,78,43])). % 58.76/58.84 cnf(11894,plain, % 58.76/58.84 (P8(f18(x118941,x118942),x118941,x118942)), % 58.76/58.84 inference(rename_variables,[],[78])). % 58.76/58.84 cnf(11895,plain, % 58.76/58.84 (P8(f18(x118951,a13),x118951,f16(f15(a1),a11))), % 58.76/58.84 inference(scs_inference,[],[135,78,11894,43,44])). % 58.76/58.84 cnf(11903,plain, % 58.76/58.84 (P9(f20(a13,x119031),f16(f15(a1),a11),x119031)), % 58.76/58.84 inference(scs_inference,[],[135,494,82,78,11894,138,72,43,44,48,41,57,53])). % 58.76/58.84 cnf(11904,plain, % 58.76/58.84 (P9(f20(x119041,x119042),x119041,x119042)), % 58.76/58.84 inference(rename_variables,[],[82])). % 58.76/58.84 cnf(11905,plain, % 58.76/58.84 (P12(f3(x119051,a13),x119051,f16(f15(a1),a11))), % 58.76/58.84 inference(scs_inference,[],[135,494,82,78,11894,138,81,72,43,44,48,41,57,53,36])). % 58.76/58.84 cnf(11906,plain, % 58.76/58.84 (P12(f3(x119061,x119062),x119061,x119062)), % 58.76/58.84 inference(rename_variables,[],[81])). % 58.76/58.84 cnf(11907,plain, % 58.76/58.84 (P9(f20(x119071,a13),x119071,f16(f15(a1),a11))), % 58.76/58.84 inference(scs_inference,[],[135,494,82,11904,78,11894,138,81,72,43,44,48,41,57,53,36,54])). % 58.76/58.84 cnf(11909,plain, % 58.76/58.84 (P12(f3(a13,x119091),f16(f15(a1),a11),x119091)), % 58.76/58.84 inference(scs_inference,[],[135,494,82,11904,78,11894,138,81,11906,72,43,44,48,41,57,53,36,54,35])). % 58.76/58.84 cnf(11973,plain, % 58.76/58.84 (P8(f7(a13,x119731),f16(f15(a1),a11),x119731)), % 58.76/58.84 inference(scs_inference,[],[135,80,43])). % 58.76/58.84 cnf(11980,plain, % 58.76/58.84 (P8(f3(a13,x119801),f16(f15(a1),a11),x119801)), % 58.76/58.84 inference(scs_inference,[],[135,79,43])). % 58.76/58.84 cnf(12431,plain, % 58.76/58.84 (P11(f4(a8),f23(a8))), % 58.76/58.84 inference(scs_inference,[],[948,86,99])). % 58.76/58.84 cnf(12435,plain, % 58.76/58.84 (~P11(f23(a8),f4(a8))), % 58.76/58.84 inference(scs_inference,[],[948,389,86,99,51,103])). % 58.76/58.84 cnf(12457,plain, % 58.76/58.84 (~E(f16(f15(a1),a11),a8)), % 58.76/58.84 inference(scs_inference,[],[148,85,37])). % 58.76/58.84 cnf(12462,plain, % 58.76/58.84 (P4(a1)), % 58.76/58.84 inference(scs_inference,[],[61,148,383,37,88])). % 58.76/58.84 cnf(12466,plain, % 58.76/58.84 (P4(a11)), % 58.76/58.84 inference(scs_inference,[],[171,88])). % 58.76/58.84 cnf(12507,plain, % 58.76/58.84 (~E(a13,a8)), % 58.76/58.84 inference(scs_inference,[],[71,430,12457,2,3])). % 58.76/58.84 cnf(13799,plain, % 58.76/58.84 (P10(f24(a1))), % 58.76/58.84 inference(scs_inference,[],[61,90])). % 58.76/58.84 cnf(13832,plain, % 58.76/58.84 (P12(f24(a1),f25(f26(a1),f26(a1)),f26(a1))), % 58.76/58.84 inference(scs_inference,[],[11903,155,11893,289,383,161,135,61,90,91,102,117,118,95,5,16,21,22,27,28,119,6,7,10,11,14,15,17,19,20,23,24,25,26,115])). % 58.76/58.84 cnf(13834,plain, % 58.76/58.84 (P9(f24(a1),f25(f26(a1),f26(a1)),f26(a1))), % 58.76/58.84 inference(scs_inference,[],[11903,155,11893,289,383,161,135,61,90,91,102,117,118,95,5,16,21,22,27,28,119,6,7,10,11,14,15,17,19,20,23,24,25,26,115,116])). % 58.76/58.84 cnf(13836,plain, % 58.76/58.84 (E(a2,a13)), % 58.76/58.84 inference(scs_inference,[],[11903,155,11893,289,383,65,161,135,61,90,91,102,117,118,95,5,16,21,22,27,28,119,6,7,10,11,14,15,17,19,20,23,24,25,26,115,116,87])). % 58.76/58.84 cnf(13844,plain, % 58.76/58.84 (~P13(f26(a5))), % 58.76/58.84 inference(scs_inference,[],[67,84,11903,155,11893,289,383,65,161,135,61,90,91,102,117,118,95,5,16,21,22,27,28,119,6,7,10,11,14,15,17,19,20,23,24,25,26,115,116,87,29,2,8,9,12,13,92])). % 58.76/58.84 cnf(13846,plain, % 58.76/58.84 (~P13(f9(a5))), % 58.76/58.84 inference(scs_inference,[],[67,84,11903,155,11893,289,383,65,161,135,61,90,91,102,117,118,95,5,16,21,22,27,28,119,6,7,10,11,14,15,17,19,20,23,24,25,26,115,116,87,29,2,8,9,12,13,92,93])). % 58.76/58.84 cnf(13865,plain, % 58.76/58.84 (P8(f3(x138651,x138652),x138651,x138652)), % 58.76/58.84 inference(rename_variables,[],[79])). % 58.76/58.84 cnf(13866,plain, % 58.76/58.84 (P12(f3(x138661,x138662),x138661,x138662)), % 58.76/58.84 inference(rename_variables,[],[81])). % 58.76/58.84 cnf(13867,plain, % 58.76/58.84 (P10(f3(x138671,x138672))), % 58.76/58.84 inference(rename_variables,[],[74])). % 58.76/58.84 cnf(13870,plain, % 58.76/58.84 (P8(f3(x138701,x138702),x138701,x138702)), % 58.76/58.84 inference(rename_variables,[],[79])). % 58.76/58.84 cnf(13871,plain, % 58.76/58.84 (P12(f3(x138711,x138712),x138711,x138712)), % 58.76/58.84 inference(rename_variables,[],[81])). % 58.76/58.84 cnf(13872,plain, % 58.76/58.84 (P10(f3(x138721,x138722))), % 58.76/58.84 inference(rename_variables,[],[74])). % 58.76/58.84 cnf(13887,plain, % 58.76/58.84 (P2(f19(a11))), % 58.76/58.84 inference(scs_inference,[],[59,67,84,12507,12431,11903,155,11893,63,289,383,65,161,60,169,173,171,237,72,74,13867,13872,135,81,13866,13871,83,79,13865,13870,61,90,91,102,117,118,95,5,16,21,22,27,28,119,6,7,10,11,14,15,17,19,20,23,24,25,26,115,116,87,29,2,8,9,12,13,92,93,109,108,99,100,51,110,3,98,124,125,96,101,112,113,127,105])). % 58.76/58.84 cnf(13893,plain, % 58.76/58.84 (E(f16(f15(a1),a11),f26(a11))), % 58.76/58.84 inference(scs_inference,[],[59,67,84,12507,12431,11903,155,11893,63,289,383,65,161,60,169,173,171,237,72,74,13867,13872,135,81,13866,13871,83,79,13865,13870,61,69,90,91,102,117,118,95,5,16,21,22,27,28,119,6,7,10,11,14,15,17,19,20,23,24,25,26,115,116,87,29,2,8,9,12,13,92,93,109,108,99,100,51,110,3,98,124,125,96,101,112,113,127,105,104,107,134])). % 58.76/58.84 cnf(13900,plain, % 58.76/58.84 (E(f25(x139001,a2),f25(x139001,a13))), % 58.76/58.84 inference(scs_inference,[],[59,67,84,12507,12431,11903,155,11893,63,289,383,65,161,60,169,173,171,237,72,74,13867,13872,135,81,13866,13871,83,79,13865,13870,61,69,90,91,102,117,118,95,5,16,21,22,27,28,119,6,7,10,11,14,15,17,19,20,23,24,25,26,115,116,87,29,2,8,9,12,13,92,93,109,108,99,100,51,110,3,98,124,125,96,101,112,113,127,105,104,107,134,97,251,4,18])). % 58.76/58.84 cnf(13907,plain, % 58.76/58.84 (P12(f3(a13,x139071),f16(f15(a1),a11),x139071)), % 58.76/58.84 inference(rename_variables,[],[11909])). % 58.76/58.84 cnf(13922,plain, % 58.76/58.84 (P11(f6(a13),f23(a2))), % 58.76/58.84 inference(scs_inference,[],[59,67,84,12507,12431,11903,155,11893,63,289,70,11907,11973,494,11909,13907,383,65,161,60,262,169,173,171,237,4494,72,74,13867,13872,11905,135,81,13866,13871,83,79,13865,13870,61,69,90,91,102,117,118,95,5,16,21,22,27,28,119,6,7,10,11,14,15,17,19,20,23,24,25,26,115,116,87,29,2,8,9,12,13,92,93,109,108,99,100,51,110,3,98,124,125,96,101,112,113,127,105,104,107,134,97,251,4,18,499,103,111,34,35,53,40,36,47,57,42,49,50])). % 58.76/58.84 cnf(13940,plain, % 58.76/58.84 (E(f6(x139401),a13)), % 58.76/58.84 inference(scs_inference,[],[82,68,119,87])). % 58.76/58.84 cnf(13948,plain, % 58.76/58.84 (P9(f24(a10),f25(f26(a10),f26(a10)),f26(a10))), % 58.76/58.84 inference(scs_inference,[],[13844,11895,82,68,62,119,87,95,115,118,116])). % 58.76/58.84 cnf(13953,plain, % 58.76/58.84 (E(f18(x139531,a2),f18(x139531,a13))), % 58.76/58.84 inference(scs_inference,[],[13836,13844,157,11895,82,68,62,119,87,95,115,118,116,102,5,20])). % 58.76/58.84 cnf(13982,plain, % 58.76/58.84 (E(a13,a2)), % 58.76/58.84 inference(scs_inference,[],[13836,13900,13844,13887,13922,13834,157,11895,82,68,62,119,87,95,115,118,116,102,5,20,6,19,97,21,22,4,117,17,16,90,91,28,27,25,7,23,18,14,11,24,15,26,10,29,2])). % 58.76/58.84 cnf(13985,plain, % 58.76/58.84 (E(f3(a2,x139851),f3(a13,x139851))), % 58.76/58.84 inference(scs_inference,[],[13836,13900,13844,13887,13922,13834,157,11895,82,68,62,119,87,95,115,118,116,102,5,20,6,19,97,21,22,4,117,17,16,90,91,28,27,25,7,23,18,14,11,24,15,26,10,29,2,9,8,12])). % 58.76/58.84 cnf(13989,plain, % 58.76/58.84 (P13(f26(a11))), % 58.76/58.84 inference(scs_inference,[],[12462,13836,13900,13844,13887,13922,13893,13834,157,11895,82,68,148,83,62,119,87,95,115,118,116,102,5,20,6,19,97,21,22,4,117,17,16,90,91,28,27,25,7,23,18,14,11,24,15,26,10,29,2,9,8,12,13,93,37])). % 58.76/58.84 cnf(13999,plain, % 58.76/58.84 (P11(f6(f16(f15(a1),a11)),f23(a2))), % 58.76/58.84 inference(scs_inference,[],[12462,13836,13900,13844,13887,13922,13893,13834,157,11895,12435,201,383,82,68,2060,148,83,62,119,87,95,115,118,116,102,5,20,6,19,97,21,22,4,117,17,16,90,91,28,27,25,7,23,18,14,11,24,15,26,10,29,2,9,8,12,13,93,37,92,109,108,55,99,50])). % 58.76/58.84 cnf(14000,plain, % 58.76/58.84 (~P7(f23(a2),f23(a13))), % 58.76/58.84 inference(scs_inference,[],[12462,13836,13900,13844,13887,13922,13893,13834,157,11895,12435,201,383,82,64,68,2060,148,83,62,119,87,95,115,118,116,102,5,20,6,19,97,21,22,4,117,17,16,90,91,28,27,25,7,23,18,14,11,24,15,26,10,29,2,9,8,12,13,93,37,92,109,108,55,99,50,110])). % 58.76/58.84 cnf(14004,plain, % 58.76/58.84 (P2(f21(f26(a1),f24(a1)))), % 58.76/58.84 inference(scs_inference,[],[12462,13836,13900,13799,13844,13887,13922,13893,13834,13832,157,11895,12435,201,383,82,64,68,2060,148,135,83,62,119,87,95,115,118,116,102,5,20,6,19,97,21,22,4,117,17,16,90,91,28,27,25,7,23,18,14,11,24,15,26,10,29,2,9,8,12,13,93,37,92,109,108,55,99,50,110,41,3,124])). % 58.76/58.84 cnf(14035,plain, % 58.76/58.84 (E(f3(a2,x140351),f3(a13,x140351))), % 58.76/58.84 inference(rename_variables,[],[13985])). % 58.76/58.84 cnf(14037,plain, % 58.76/58.84 (E(f3(a2,x140371),f3(a13,x140371))), % 58.76/58.84 inference(rename_variables,[],[13985])). % 58.76/58.84 cnf(14083,plain, % 58.76/58.84 ($false), % 58.76/58.84 inference(scs_inference,[],[12466,13982,13953,13985,14035,14037,13846,13940,13989,14000,13948,14004,13999,11980,70,173,1027,500,405,118,95,102,87,97,21,91,20,22,6,5,251,27,117,28,19,90,24,14,4,11,16,17,23,25,15,7,29,18,26,10,2,12,8,9,13,92]), % 58.76/58.84 ['proof']). % 58.76/58.84 % SZS output end Proof % 58.76/58.84 % Total time :58.180000s %------------------------------------------------------------------------------