%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : GRP623+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 : n001.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:05 EDT 2024 % Result : Theorem 58.92s 59.01s % Output : CNFRefutation 59.08s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.13/0.13 % Problem : GRP623+1 : TPTP v8.2.0. Released v3.4.0. % 0.13/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.13/0.34 % Computer : n001.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Thu Jun 20 10:48:38 EDT 2024 % 0.13/0.34 % CPUTime : % 0.56/0.61 start to proof:theBenchmark % 58.92/58.99 %------------------------------------------- % 58.92/58.99 % File :CSE---1.7 % 58.92/58.99 % Problem :theBenchmark % 58.92/58.99 % Transform :cnf % 58.92/58.99 % Format :tptp:raw % 58.92/58.99 % Command :java -jar mcs_scs.jar %d %s % 58.92/58.99 % 58.92/58.99 % Result :Theorem 58.330000s % 58.92/58.99 % Output :CNFRefutation 58.330000s % 58.92/58.99 %------------------------------------------- % 58.92/59.00 %------------------------------------------------------------------------------ % 58.92/59.00 % File : GRP623+1 : TPTP v8.2.0. Released v3.4.0. % 58.92/59.00 % Domain : Group Theory % 58.92/59.00 % Problem : On the Group of Inner Automorphisms T14 % 58.92/59.00 % Version : [Urb08] axioms : Especial. % 58.92/59.00 % English : % 58.92/59.00 % 58.92/59.00 % Refs : [Kor96] Kornilowicz (1996), On the Group of Inner Automorphism % 58.92/59.00 % : [Urb07] Urban (2007), MPTP 0.2: Design, Implementation, and In % 58.92/59.00 % : [Urb08] Urban (2006), Email to G. Sutcliffe % 58.92/59.00 % Source : [Urb08] % 58.92/59.00 % Names : t14_autgroup [Urb08] % 58.92/59.00 % 58.92/59.00 % Status : Theorem % 58.92/59.00 % Rating : 0.33 v8.2.0, 0.31 v8.1.0, 0.33 v7.5.0, 0.31 v7.4.0, 0.27 v7.3.0, 0.21 v7.2.0, 0.17 v7.1.0, 0.22 v7.0.0, 0.30 v6.4.0, 0.31 v6.3.0, 0.29 v6.2.0, 0.32 v6.1.0, 0.50 v6.0.0, 0.48 v5.5.0, 0.56 v5.4.0, 0.54 v5.3.0, 0.56 v5.2.0, 0.40 v5.1.0, 0.48 v5.0.0, 0.46 v4.1.0, 0.48 v4.0.1, 0.52 v4.0.0, 0.50 v3.7.0, 0.45 v3.5.0, 0.47 v3.4.0 % 58.92/59.00 % Syntax : Number of formulae : 64 ( 17 unt; 0 def) % 58.92/59.00 % Number of atoms : 194 ( 6 equ) % 58.92/59.00 % Maximal formula atoms : 9 ( 3 avg) % 58.92/59.00 % Number of connectives : 160 ( 30 ~; 1 |; 83 &) % 58.92/59.00 % ( 4 <=>; 42 =>; 0 <=; 0 <~>) % 58.92/59.00 % Maximal formula depth : 10 ( 5 avg) % 58.92/59.00 % Maximal term depth : 3 ( 1 avg) % 58.92/59.00 % Number of predicates : 23 ( 21 usr; 1 prp; 0-4 aty) % 58.92/59.00 % Number of functors : 8 ( 8 usr; 1 con; 0-2 aty) % 58.92/59.00 % Number of variables : 111 ( 90 !; 21 ?) % 58.92/59.00 % SPC : FOF_THM_RFO_SEQ % 58.92/59.00 % 58.92/59.00 % Comments : Normal version: includes the axioms (which may be theorems from % 58.92/59.00 % other articles) and background that are possibly necessary. % 58.92/59.00 % : Translated by MPTP from the Mizar Mathematical Library 4.48.930. % 58.92/59.00 % : The problem encoding is based on set theory. % 58.92/59.00 %------------------------------------------------------------------------------ % 58.92/59.00 fof(t14_autgroup,conjecture, % 58.92/59.00 ! [A] : % 58.92/59.00 ( ( ~ v3_struct_0(A) % 58.92/59.00 & v1_group_1(A) % 58.92/59.00 & v3_group_1(A) % 58.92/59.00 & v4_group_1(A) % 58.92/59.00 & l1_group_1(A) ) % 58.92/59.00 => r1_tarski(k4_autgroup(A),k1_autgroup(A)) ) ). % 58.92/59.00 % 58.92/59.00 fof(abstractness_v1_group_1,axiom, % 58.92/59.00 ! [A] : % 58.92/59.00 ( l1_group_1(A) % 58.92/59.00 => ( v1_group_1(A) % 58.92/59.00 => A = g1_group_1(u1_struct_0(A),u1_group_1(A)) ) ) ). % 58.92/59.00 % 58.92/59.00 fof(antisymmetry_r2_hidden,axiom, % 58.92/59.00 ! [A,B] : % 58.92/59.00 ( r2_hidden(A,B) % 58.92/59.00 => ~ r2_hidden(B,A) ) ). % 58.92/59.00 % 58.92/59.00 fof(cc1_fraenkel,axiom, % 58.92/59.00 ! [A] : % 58.92/59.00 ( v1_fraenkel(A) % 58.92/59.00 => ! [B] : % 58.92/59.00 ( m1_subset_1(B,A) % 58.92/59.00 => ( v1_relat_1(B) % 58.92/59.00 & v1_funct_1(B) ) ) ) ). % 58.92/59.00 % 58.92/59.00 fof(cc1_funct_1,axiom, % 58.92/59.00 ! [A] : % 58.92/59.00 ( v1_xboole_0(A) % 58.92/59.00 => v1_funct_1(A) ) ). % 58.92/59.00 % 58.92/59.00 fof(cc1_funct_2,axiom, % 58.92/59.00 ! [A,B,C] : % 58.92/59.00 ( m1_relset_1(C,A,B) % 58.92/59.00 => ( ( v1_funct_1(C) % 58.92/59.00 & v1_partfun1(C,A,B) ) % 58.92/59.00 => ( v1_funct_1(C) % 58.92/59.00 & v1_funct_2(C,A,B) ) ) ) ). % 58.92/59.00 % 58.92/59.00 fof(cc1_group_1,axiom, % 58.92/59.00 ! [A] : % 58.92/59.00 ( l1_group_1(A) % 58.92/59.00 => ( ( ~ v3_struct_0(A) % 58.92/59.00 & v3_group_1(A) ) % 58.92/59.00 => ( ~ v3_struct_0(A) % 58.92/59.00 & v2_group_1(A) ) ) ) ). % 58.92/59.00 % 58.92/59.00 fof(cc1_relset_1,axiom, % 58.92/59.00 ! [A,B,C] : % 58.92/59.00 ( m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))) % 58.92/59.00 => v1_relat_1(C) ) ). % 58.92/59.00 % 58.92/59.00 fof(cc2_funct_1,axiom, % 58.92/59.00 ! [A] : % 58.92/59.00 ( ( v1_relat_1(A) % 58.92/59.00 & v1_xboole_0(A) % 58.92/59.00 & v1_funct_1(A) ) % 58.92/59.00 => ( v1_relat_1(A) % 58.92/59.00 & v1_funct_1(A) % 58.92/59.00 & v2_funct_1(A) ) ) ). % 58.92/59.00 % 58.92/59.00 fof(cc5_funct_2,axiom, % 58.92/59.00 ! [A,B] : % 58.92/59.00 ( ~ v1_xboole_0(B) % 58.92/59.00 => ! [C] : % 58.92/59.00 ( m1_relset_1(C,A,B) % 58.92/59.00 => ( ( v1_funct_1(C) % 58.92/59.00 & v1_funct_2(C,A,B) ) % 58.92/59.00 => ( v1_funct_1(C) % 58.92/59.00 & v1_partfun1(C,A,B) % 58.92/59.00 & v1_funct_2(C,A,B) ) ) ) ) ). % 58.92/59.00 % 58.92/59.00 fof(cc6_funct_2,axiom, % 58.92/59.00 ! [A,B] : % 58.92/59.00 ( ( ~ v1_xboole_0(A) % 58.92/59.00 & ~ v1_xboole_0(B) ) % 58.92/59.00 => ! [C] : % 58.92/59.00 ( m1_relset_1(C,A,B) % 58.92/59.00 => ( ( v1_funct_1(C) % 58.92/59.00 & v1_funct_2(C,A,B) ) % 58.92/59.00 => ( v1_funct_1(C) % 58.92/59.00 & ~ v1_xboole_0(C) % 58.92/59.00 & v1_partfun1(C,A,B) % 58.92/59.00 & v1_funct_2(C,A,B) ) ) ) ) ). % 58.92/59.00 % 58.92/59.00 fof(d3_tarski,axiom, % 58.92/59.00 ! [A,B] : % 58.92/59.00 ( r1_tarski(A,B) % 58.92/59.00 <=> ! [C] : % 58.92/59.00 ( r2_hidden(C,A) % 58.92/59.00 => r2_hidden(C,B) ) ) ). % 58.92/59.00 % 58.92/59.00 fof(dt_g1_group_1,axiom, % 58.92/59.00 ! [A,B] : % 58.92/59.00 ( ( v1_funct_1(B) % 58.92/59.00 & v1_funct_2(B,k2_zfmisc_1(A,A),A) % 58.92/59.00 & m1_relset_1(B,k2_zfmisc_1(A,A),A) ) % 58.92/59.00 => ( v1_group_1(g1_group_1(A,B)) % 58.92/59.00 & l1_group_1(g1_group_1(A,B)) ) ) ). % 58.92/59.00 % 58.92/59.00 fof(dt_k1_autgroup,axiom, % 58.92/59.00 ! [A] : % 58.92/59.00 ( ( ~ v3_struct_0(A) % 58.92/59.00 & v1_group_1(A) % 58.92/59.00 & v3_group_1(A) % 58.92/59.00 & v4_group_1(A) % 58.92/59.00 & l1_group_1(A) ) % 58.92/59.00 => m1_fraenkel(k1_autgroup(A),u1_struct_0(A),u1_struct_0(A)) ) ). % 58.92/59.00 % 58.92/59.00 fof(dt_k1_xboole_0,axiom, % 58.92/59.00 $true ). % 58.92/59.00 % 58.92/59.00 fof(dt_k1_zfmisc_1,axiom, % 58.92/59.00 $true ). % 58.92/59.00 % 58.92/59.00 fof(dt_k2_zfmisc_1,axiom, % 58.92/59.00 $true ). % 58.92/59.00 % 58.92/59.00 fof(dt_k4_autgroup,axiom, % 58.92/59.00 ! [A] : % 58.92/59.00 ( ( ~ v3_struct_0(A) % 58.92/59.00 & v1_group_1(A) % 58.92/59.00 & v3_group_1(A) % 58.92/59.00 & v4_group_1(A) % 58.92/59.00 & l1_group_1(A) ) % 58.92/59.00 => m1_fraenkel(k4_autgroup(A),u1_struct_0(A),u1_struct_0(A)) ) ). % 58.92/59.00 % 58.92/59.01 fof(dt_l1_group_1,axiom, % 58.92/59.01 ! [A] : % 58.92/59.01 ( l1_group_1(A) % 58.92/59.01 => l1_struct_0(A) ) ). % 58.92/59.01 % 58.92/59.01 fof(dt_l1_struct_0,axiom, % 58.92/59.01 $true ). % 58.92/59.01 % 58.92/59.01 fof(dt_m1_fraenkel,axiom, % 58.92/59.01 ! [A,B,C] : % 58.92/59.01 ( m1_fraenkel(C,A,B) % 58.92/59.01 => ( ~ v1_xboole_0(C) % 58.92/59.01 & v1_fraenkel(C) ) ) ). % 58.92/59.01 % 58.92/59.01 fof(dt_m1_relset_1,axiom, % 58.92/59.01 $true ). % 58.92/59.01 % 58.92/59.01 fof(dt_m1_subset_1,axiom, % 58.92/59.01 $true ). % 58.92/59.01 % 58.92/59.01 fof(dt_m2_fraenkel,axiom, % 58.92/59.01 ! [A,B,C] : % 58.92/59.01 ( ( ~ v1_xboole_0(B) % 58.92/59.01 & m1_fraenkel(C,A,B) ) % 58.92/59.01 => ! [D] : % 58.92/59.01 ( m2_fraenkel(D,A,B,C) % 58.92/59.01 => ( v1_funct_1(D) % 58.92/59.01 & v1_funct_2(D,A,B) % 58.92/59.01 & m2_relset_1(D,A,B) ) ) ) ). % 58.92/59.01 % 58.92/59.01 fof(dt_m2_relset_1,axiom, % 58.92/59.01 ! [A,B,C] : % 58.92/59.01 ( m2_relset_1(C,A,B) % 58.92/59.01 => m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))) ) ). % 58.92/59.01 % 58.92/59.01 fof(dt_u1_group_1,axiom, % 58.92/59.01 ! [A] : % 58.92/59.01 ( l1_group_1(A) % 58.92/59.01 => ( v1_funct_1(u1_group_1(A)) % 58.92/59.01 & v1_funct_2(u1_group_1(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A)) % 58.92/59.01 & m2_relset_1(u1_group_1(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A)) ) ) ). % 58.92/59.01 % 58.92/59.01 fof(dt_u1_struct_0,axiom, % 58.92/59.01 $true ). % 58.92/59.01 % 58.92/59.01 fof(existence_l1_group_1,axiom, % 58.92/59.01 ? [A] : l1_group_1(A) ). % 58.92/59.01 % 58.92/59.01 fof(existence_l1_struct_0,axiom, % 58.92/59.01 ? [A] : l1_struct_0(A) ). % 58.92/59.01 % 58.92/59.01 fof(existence_m1_fraenkel,axiom, % 58.92/59.01 ! [A,B] : % 58.92/59.01 ? [C] : m1_fraenkel(C,A,B) ). % 58.92/59.01 % 58.92/59.01 fof(existence_m1_relset_1,axiom, % 58.92/59.01 ! [A,B] : % 58.92/59.01 ? [C] : m1_relset_1(C,A,B) ). % 58.92/59.01 % 58.92/59.01 fof(existence_m1_subset_1,axiom, % 58.92/59.01 ! [A] : % 58.92/59.01 ? [B] : m1_subset_1(B,A) ). % 58.92/59.01 % 58.92/59.01 fof(existence_m2_fraenkel,axiom, % 58.92/59.01 ! [A,B,C] : % 58.92/59.01 ( ( ~ v1_xboole_0(B) % 58.92/59.01 & m1_fraenkel(C,A,B) ) % 58.92/59.01 => ? [D] : m2_fraenkel(D,A,B,C) ) ). % 58.92/59.01 % 58.92/59.01 fof(existence_m2_relset_1,axiom, % 58.92/59.01 ! [A,B] : % 58.92/59.01 ? [C] : m2_relset_1(C,A,B) ). % 58.92/59.01 % 58.92/59.01 fof(fc1_group_1,axiom, % 58.92/59.01 ! [A,B] : % 58.92/59.01 ( ( ~ v1_xboole_0(A) % 58.92/59.01 & v1_funct_1(B) % 58.92/59.01 & v1_funct_2(B,k2_zfmisc_1(A,A),A) % 58.92/59.01 & m1_relset_1(B,k2_zfmisc_1(A,A),A) ) % 58.92/59.01 => ( ~ v3_struct_0(g1_group_1(A,B)) % 58.92/59.01 & v1_group_1(g1_group_1(A,B)) ) ) ). % 58.92/59.01 % 58.92/59.01 fof(fc1_struct_0,axiom, % 58.92/59.01 ! [A] : % 58.92/59.01 ( ( ~ v3_struct_0(A) % 58.92/59.01 & l1_struct_0(A) ) % 58.92/59.01 => ~ v1_xboole_0(u1_struct_0(A)) ) ). % 58.92/59.01 % 58.92/59.01 fof(fc1_xboole_0,axiom, % 58.92/59.01 v1_xboole_0(k1_xboole_0) ). % 58.92/59.01 % 58.92/59.01 fof(free_g1_group_1,axiom, % 58.92/59.01 ! [A,B] : % 58.92/59.01 ( ( v1_funct_1(B) % 58.92/59.01 & v1_funct_2(B,k2_zfmisc_1(A,A),A) % 58.92/59.01 & m1_relset_1(B,k2_zfmisc_1(A,A),A) ) % 58.92/59.01 => ! [C,D] : % 58.92/59.01 ( g1_group_1(A,B) = g1_group_1(C,D) % 58.92/59.01 => ( A = C % 58.92/59.01 & B = D ) ) ) ). % 58.92/59.01 % 58.92/59.01 fof(rc1_fraenkel,axiom, % 58.92/59.01 ? [A] : % 58.92/59.01 ( ~ v1_xboole_0(A) % 58.92/59.01 & v1_fraenkel(A) ) ). % 58.92/59.01 % 58.92/59.01 fof(rc1_funct_1,axiom, % 58.92/59.01 ? [A] : % 58.92/59.01 ( v1_relat_1(A) % 58.92/59.01 & v1_funct_1(A) ) ). % 58.92/59.01 % 58.92/59.01 fof(rc1_funct_2,axiom, % 58.92/59.01 ! [A,B] : % 58.92/59.01 ? [C] : % 58.92/59.01 ( m1_relset_1(C,A,B) % 58.92/59.01 & v1_relat_1(C) % 58.92/59.01 & v1_funct_1(C) % 58.92/59.01 & v1_funct_2(C,A,B) ) ). % 58.92/59.01 % 58.92/59.01 fof(rc1_group_1,axiom, % 58.92/59.01 ? [A] : % 58.92/59.01 ( l1_group_1(A) % 58.92/59.01 & v1_group_1(A) ) ). % 58.92/59.01 % 58.92/59.01 fof(rc1_partfun1,axiom, % 58.92/59.01 ? [A] : % 58.92/59.01 ( v1_relat_1(A) % 58.92/59.01 & v1_funct_1(A) % 58.92/59.01 & v2_funct_1(A) % 58.92/59.01 & v1_xboole_0(A) ) ). % 58.92/59.01 % 58.92/59.01 fof(rc1_xboole_0,axiom, % 58.92/59.01 ? [A] : v1_xboole_0(A) ). % 58.92/59.01 % 58.92/59.01 fof(rc2_funct_1,axiom, % 58.92/59.01 ? [A] : % 58.92/59.01 ( v1_relat_1(A) % 58.92/59.01 & v1_xboole_0(A) % 58.92/59.01 & v1_funct_1(A) ) ). % 58.92/59.01 % 58.92/59.01 fof(rc2_group_1,axiom, % 58.92/59.01 ? [A] : % 58.92/59.01 ( l1_group_1(A) % 58.92/59.01 & ~ v3_struct_0(A) % 58.92/59.01 & v1_group_1(A) ) ). % 58.92/59.01 % 58.92/59.01 fof(rc2_partfun1,axiom, % 58.92/59.01 ! [A,B] : % 58.92/59.01 ? [C] : % 58.92/59.01 ( m1_relset_1(C,A,B) % 58.92/59.01 & v1_relat_1(C) % 58.92/59.01 & v1_funct_1(C) ) ). % 58.92/59.01 % 58.92/59.01 fof(rc2_xboole_0,axiom, % 58.92/59.01 ? [A] : ~ v1_xboole_0(A) ). % 58.92/59.01 % 58.92/59.01 fof(rc3_funct_1,axiom, % 58.92/59.01 ? [A] : % 58.92/59.01 ( v1_relat_1(A) % 58.92/59.01 & v1_funct_1(A) % 58.92/59.01 & v2_funct_1(A) ) ). % 58.92/59.01 % 58.92/59.01 fof(rc3_group_1,axiom, % 58.92/59.01 ? [A] : % 58.92/59.01 ( l1_group_1(A) % 58.92/59.01 & ~ v3_struct_0(A) % 58.92/59.01 & v1_group_1(A) % 58.92/59.01 & v2_group_1(A) % 58.92/59.01 & v3_group_1(A) % 58.92/59.01 & v4_group_1(A) ) ). % 58.92/59.01 % 58.92/59.01 fof(rc3_struct_0,axiom, % 58.92/59.01 ? [A] : % 58.92/59.01 ( l1_struct_0(A) % 58.92/59.01 & ~ v3_struct_0(A) ) ). % 58.92/59.01 % 58.92/59.01 fof(rc5_struct_0,axiom, % 58.92/59.01 ! [A] : % 58.92/59.01 ( ( ~ v3_struct_0(A) % 58.92/59.01 & l1_struct_0(A) ) % 58.92/59.01 => ? [B] : % 58.92/59.01 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 58.92/59.01 & ~ v1_xboole_0(B) ) ) ). % 58.92/59.01 % 58.92/59.01 fof(redefinition_m2_fraenkel,axiom, % 58.92/59.01 ! [A,B,C] : % 58.92/59.01 ( ( ~ v1_xboole_0(B) % 58.92/59.01 & m1_fraenkel(C,A,B) ) % 58.92/59.01 => ! [D] : % 58.92/59.01 ( m2_fraenkel(D,A,B,C) % 58.92/59.01 <=> m1_subset_1(D,C) ) ) ). % 58.92/59.01 % 58.92/59.01 fof(redefinition_m2_relset_1,axiom, % 58.92/59.01 ! [A,B,C] : % 58.92/59.01 ( m2_relset_1(C,A,B) % 58.92/59.01 <=> m1_relset_1(C,A,B) ) ). % 58.92/59.01 % 58.92/59.01 fof(reflexivity_r1_tarski,axiom, % 58.92/59.01 ! [A,B] : r1_tarski(A,A) ). % 58.92/59.01 % 58.92/59.01 fof(t13_autgroup,axiom, % 58.92/59.01 ! [A] : % 58.92/59.01 ( ( ~ v3_struct_0(A) % 58.92/59.01 & v1_group_1(A) % 58.92/59.01 & v3_group_1(A) % 58.92/59.01 & v4_group_1(A) % 58.92/59.01 & l1_group_1(A) ) % 58.92/59.01 => ! [B] : % 58.92/59.01 ( m2_fraenkel(B,u1_struct_0(A),u1_struct_0(A),k4_autgroup(A)) % 58.92/59.01 => m2_fraenkel(B,u1_struct_0(A),u1_struct_0(A),k1_autgroup(A)) ) ) ). % 58.92/59.01 % 58.92/59.01 fof(t1_subset,axiom, % 58.92/59.01 ! [A,B] : % 58.92/59.01 ( r2_hidden(A,B) % 58.92/59.01 => m1_subset_1(A,B) ) ). % 58.92/59.01 % 58.92/59.01 fof(t2_subset,axiom, % 58.92/59.01 ! [A,B] : % 58.92/59.01 ( m1_subset_1(A,B) % 58.92/59.01 => ( v1_xboole_0(B) % 58.92/59.01 | r2_hidden(A,B) ) ) ). % 58.92/59.01 % 58.92/59.01 fof(t3_subset,axiom, % 58.92/59.01 ! [A,B] : % 58.92/59.01 ( m1_subset_1(A,k1_zfmisc_1(B)) % 58.92/59.01 <=> r1_tarski(A,B) ) ). % 58.92/59.01 % 58.92/59.01 fof(t4_subset,axiom, % 58.92/59.01 ! [A,B,C] : % 58.92/59.01 ( ( r2_hidden(A,B) % 58.92/59.01 & m1_subset_1(B,k1_zfmisc_1(C)) ) % 58.92/59.01 => m1_subset_1(A,C) ) ). % 58.92/59.01 % 58.92/59.01 fof(t5_subset,axiom, % 58.92/59.01 ! [A,B,C] : % 58.92/59.01 ~ ( r2_hidden(A,B) % 58.92/59.01 & m1_subset_1(B,k1_zfmisc_1(C)) % 58.92/59.01 & v1_xboole_0(C) ) ). % 58.92/59.01 % 58.92/59.01 fof(t6_boole,axiom, % 58.92/59.01 ! [A] : % 58.92/59.01 ( v1_xboole_0(A) % 58.92/59.01 => A = k1_xboole_0 ) ). % 58.92/59.01 % 58.92/59.01 fof(t7_boole,axiom, % 58.92/59.01 ! [A,B] : % 58.92/59.01 ~ ( r2_hidden(A,B) % 58.92/59.01 & v1_xboole_0(B) ) ). % 58.92/59.01 % 58.92/59.01 fof(t8_boole,axiom, % 58.92/59.01 ! [A,B] : % 58.92/59.01 ~ ( v1_xboole_0(A) % 58.92/59.01 & A != B % 58.92/59.01 & v1_xboole_0(B) ) ). % 58.92/59.01 % 58.92/59.01 %------------------------------------------------------------------------------ % 58.92/59.01 %------------------------------------------- % 58.92/59.01 % Proof found % 58.92/59.01 % SZS status Theorem for theBenchmark % 58.92/59.01 % SZS output start Proof % 58.92/59.01 %ClaNum:167(EqnAxiom:66) % 58.92/59.01 %VarNum:355(SingletonVarNum:133) % 58.92/59.01 %MaxLitNum:7 % 58.92/59.01 %MaxfuncDepth:2 % 58.92/59.01 %SharedTerms:55 % 58.92/59.01 %goalClause: 67 71 73 75 110 116 % 58.92/59.01 %singleGoalClaCount:6 % 58.92/59.01 [67]P1(a1) % 58.92/59.01 [68]P1(a2) % 58.92/59.01 [69]P1(a6) % 58.92/59.01 [70]P1(a12) % 58.92/59.01 [71]P14(a1) % 58.92/59.01 [72]P14(a12) % 58.92/59.01 [73]P20(a1) % 58.92/59.01 [74]P20(a12) % 58.92/59.01 [75]P2(a1) % 58.92/59.01 [76]P2(a14) % 58.92/59.01 [77]P2(a2) % 58.92/59.01 [78]P2(a6) % 58.92/59.01 [79]P2(a12) % 58.92/59.01 [80]P3(a3) % 58.92/59.01 [81]P15(a4) % 58.92/59.01 [82]P15(a7) % 58.92/59.01 [83]P15(a8) % 58.92/59.01 [84]P15(a13) % 58.92/59.01 [85]P12(a4) % 58.92/59.01 [86]P12(a7) % 58.92/59.01 [87]P12(a8) % 58.92/59.01 [88]P12(a13) % 58.92/59.01 [89]P17(a18) % 58.92/59.01 [90]P17(a7) % 58.92/59.01 [91]P17(a9) % 58.92/59.01 [92]P17(a8) % 58.92/59.01 [93]P18(a12) % 58.92/59.01 [94]P19(a7) % 58.92/59.01 [95]P19(a13) % 58.92/59.01 [96]P4(a19) % 58.92/59.01 [97]P4(a15) % 58.92/59.01 [110]~P21(a1) % 58.92/59.02 [111]~P21(a6) % 58.92/59.02 [112]~P21(a12) % 58.92/59.02 [113]~P21(a15) % 58.92/59.02 [114]~P17(a3) % 58.92/59.02 [115]~P17(a11) % 58.92/59.02 [116]~P5(f27(a1),f25(a1)) % 58.92/59.02 [98]P5(x981,x981) % 58.92/59.02 [99]P6(f20(x991),x991) % 58.92/59.02 [100]P15(f5(x1001,x1002)) % 58.92/59.02 [101]P15(f10(x1011,x1012)) % 58.92/59.02 [102]P12(f5(x1021,x1022)) % 58.92/59.02 [103]P12(f10(x1031,x1032)) % 58.92/59.02 [104]P7(f21(x1041,x1042),x1041,x1042) % 58.92/59.02 [105]P7(f5(x1051,x1052),x1051,x1052) % 58.92/59.02 [106]P7(f10(x1061,x1062),x1061,x1062) % 58.92/59.02 [107]P13(f5(x1071,x1072),x1071,x1072) % 58.92/59.02 [108]P8(f22(x1081,x1082),x1081,x1082) % 58.92/59.02 [109]P9(f23(x1091,x1092),x1091,x1092) % 58.92/59.02 [117]~P17(x1171)+E(x1171,a18) % 58.92/59.02 [118]~P17(x1181)+P12(x1181) % 58.92/59.02 [119]~P2(x1191)+P4(x1191) % 58.92/59.02 [121]~P2(x1211)+P12(f30(x1211)) % 58.92/59.02 [146]~P2(x1461)+P13(f30(x1461),f29(f31(x1461),f31(x1461)),f31(x1461)) % 58.92/59.02 [147]~P2(x1471)+P9(f30(x1471),f29(f31(x1471),f31(x1471)),f31(x1471)) % 58.92/59.02 [126]~P17(x1261)+~P11(x1262,x1261) % 58.92/59.02 [129]~P11(x1291,x1292)+P6(x1291,x1292) % 58.92/59.02 [133]~P11(x1332,x1331)+~P11(x1331,x1332) % 58.92/59.02 [132]~P5(x1321,x1322)+P6(x1321,f28(x1322)) % 58.92/59.02 [134]P5(x1341,x1342)+~P6(x1341,f28(x1342)) % 58.92/59.02 [136]P5(x1361,x1362)+P11(f17(x1361,x1362),x1361) % 58.92/59.02 [140]P5(x1401,x1402)+~P11(f17(x1401,x1402),x1402) % 58.92/59.02 [141]P3(x1411)+~P8(x1411,x1412,x1413) % 58.92/59.02 [142]~P17(x1421)+~P8(x1421,x1422,x1423) % 58.92/59.02 [148]~P9(x1481,x1482,x1483)+P7(x1481,x1482,x1483) % 58.92/59.02 [149]~P7(x1491,x1492,x1493)+P9(x1491,x1492,x1493) % 58.92/59.02 [145]P15(x1451)+~P6(x1451,f28(f29(x1452,x1453))) % 58.92/59.02 [150]~P9(x1501,x1502,x1503)+P6(x1501,f28(f29(x1502,x1503))) % 58.92/59.02 [124]~P4(x1241)+P21(x1241)+~P17(f31(x1241)) % 58.92/59.02 [125]~P4(x1251)+P21(x1251)+~P17(f16(x1251)) % 58.92/59.02 [131]~P1(x1311)+~P2(x1311)+E(f26(f31(x1311),f30(x1311)),x1311) % 58.92/59.02 [135]~P4(x1351)+P21(x1351)+P6(f16(x1351),f28(f31(x1351))) % 58.92/59.02 [120]~P17(x1202)+~P17(x1201)+E(x1201,x1202) % 58.92/59.02 [127]~P6(x1271,x1272)+P15(x1271)+~P3(x1272) % 58.92/59.02 [128]~P6(x1281,x1282)+P12(x1281)+~P3(x1282) % 58.92/59.02 [130]~P6(x1302,x1301)+P17(x1301)+P11(x1302,x1301) % 58.92/59.02 [137]~P11(x1371,x1373)+P11(x1371,x1372)+~P5(x1373,x1372) % 58.92/59.02 [138]~P17(x1381)+~P11(x1382,x1383)+~P6(x1383,f28(x1381)) % 58.92/59.02 [139]P6(x1391,x1392)+~P11(x1391,x1393)+~P6(x1393,f28(x1392)) % 58.92/59.02 [162]~P8(x1623,x1622,x1621)+P17(x1621)+P10(f24(x1622,x1621,x1623),x1622,x1621,x1623) % 58.92/59.02 [122]P18(x1221)+~P14(x1221)+~P2(x1221)+P21(x1221) % 58.92/59.02 [123]~P15(x1231)+~P12(x1231)+~P17(x1231)+P19(x1231) % 58.92/59.02 [155]~P12(x1552)+~P7(x1552,f29(x1551,x1551),x1551)+~P13(x1552,f29(x1551,x1551),x1551)+P1(f26(x1551,x1552)) % 58.92/59.02 [156]~P12(x1562)+~P7(x1562,f29(x1561,x1561),x1561)+~P13(x1562,f29(x1561,x1561),x1561)+P2(f26(x1561,x1562)) % 58.92/59.02 [152]~P12(x1521)+~P7(x1521,x1522,x1523)+~P16(x1521,x1522,x1523)+P13(x1521,x1522,x1523) % 58.92/59.02 [161]~P6(x1612,x1614)+~P8(x1614,x1613,x1611)+P17(x1611)+P10(x1612,x1613,x1611,x1614) % 58.92/59.02 [163]~P10(x1631,x1634,x1632,x1633)+P12(x1631)+~P8(x1633,x1634,x1632)+P17(x1632) % 58.92/59.02 [164]~P10(x1642,x1644,x1641,x1643)+P17(x1641)+~P8(x1643,x1644,x1641)+P6(x1642,x1643) % 58.92/59.02 [165]~P10(x1652,x1653,x1651,x1654)+P17(x1651)+P13(x1652,x1653,x1651)+~P8(x1654,x1653,x1651) % 58.92/59.02 [166]~P10(x1662,x1663,x1661,x1664)+P17(x1661)+P9(x1662,x1663,x1661)+~P8(x1664,x1663,x1661) % 58.92/59.02 [160]P17(x1601)+~P12(x1602)+~P7(x1602,f29(x1601,x1601),x1601)+~P13(x1602,f29(x1601,x1601),x1601)+~P21(f26(x1601,x1602)) % 58.92/59.02 [153]~P12(x1532)+~P7(x1532,x1533,x1531)+~P13(x1532,x1533,x1531)+P17(x1531)+P16(x1532,x1533,x1531) % 58.92/59.02 [158]~P12(x1581)+E(x1581,x1582)+~P7(x1581,f29(x1583,x1583),x1583)+~P13(x1581,f29(x1583,x1583),x1583)+~E(f26(x1583,x1581),f26(x1584,x1582)) % 58.92/59.02 [159]~P12(x1593)+E(x1591,x1592)+~P7(x1593,f29(x1591,x1591),x1591)+~P13(x1593,f29(x1591,x1591),x1591)+~E(f26(x1591,x1593),f26(x1592,x1594)) % 58.92/59.02 [143]~P1(x1431)+~P14(x1431)+~P20(x1431)+~P2(x1431)+P21(x1431)+P8(f27(x1431),f31(x1431),f31(x1431)) % 58.92/59.02 [144]~P1(x1441)+~P14(x1441)+~P20(x1441)+~P2(x1441)+P21(x1441)+P8(f25(x1441),f31(x1441),f31(x1441)) % 58.92/59.02 [151]~P17(x1513)+~P7(x1513,x1512,x1511)+~P13(x1513,x1512,x1511)+P17(x1511)+P17(x1512)+~P12(x1513) % 58.92/59.02 [167]~P1(x1671)+~P14(x1671)+~P20(x1671)+~P2(x1671)+P21(x1671)+~P10(x1672,f31(x1671),f31(x1671),f27(x1671))+P10(x1672,f31(x1671),f31(x1671),f25(x1671)) % 58.92/59.02 %EqnAxiom % 58.92/59.02 [1]E(x11,x11) % 58.92/59.02 [2]E(x22,x21)+~E(x21,x22) % 58.92/59.02 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 58.92/59.02 [4]~E(x41,x42)+E(f20(x41),f20(x42)) % 58.92/59.02 [5]~E(x51,x52)+E(f5(x51,x53),f5(x52,x53)) % 58.92/59.02 [6]~E(x61,x62)+E(f5(x63,x61),f5(x63,x62)) % 58.92/59.02 [7]~E(x71,x72)+E(f10(x71,x73),f10(x72,x73)) % 58.92/59.02 [8]~E(x81,x82)+E(f10(x83,x81),f10(x83,x82)) % 58.92/59.02 [9]~E(x91,x92)+E(f27(x91),f27(x92)) % 58.92/59.02 [10]~E(x101,x102)+E(f25(x101),f25(x102)) % 58.92/59.02 [11]~E(x111,x112)+E(f21(x111,x113),f21(x112,x113)) % 58.92/59.02 [12]~E(x121,x122)+E(f21(x123,x121),f21(x123,x122)) % 58.92/59.02 [13]~E(x131,x132)+E(f31(x131),f31(x132)) % 58.92/59.02 [14]~E(x141,x142)+E(f26(x141,x143),f26(x142,x143)) % 58.92/59.02 [15]~E(x151,x152)+E(f26(x153,x151),f26(x153,x152)) % 58.92/59.02 [16]~E(x161,x162)+E(f29(x161,x163),f29(x162,x163)) % 58.92/59.02 [17]~E(x171,x172)+E(f29(x173,x171),f29(x173,x172)) % 58.92/59.02 [18]~E(x181,x182)+E(f22(x181,x183),f22(x182,x183)) % 58.92/59.02 [19]~E(x191,x192)+E(f22(x193,x191),f22(x193,x192)) % 58.92/59.02 [20]~E(x201,x202)+E(f23(x201,x203),f23(x202,x203)) % 58.92/59.02 [21]~E(x211,x212)+E(f23(x213,x211),f23(x213,x212)) % 58.92/59.02 [22]~E(x221,x222)+E(f30(x221),f30(x222)) % 58.92/59.02 [23]~E(x231,x232)+E(f28(x231),f28(x232)) % 58.92/59.02 [24]~E(x241,x242)+E(f17(x241,x243),f17(x242,x243)) % 58.92/59.02 [25]~E(x251,x252)+E(f17(x253,x251),f17(x253,x252)) % 58.92/59.02 [26]~E(x261,x262)+E(f16(x261),f16(x262)) % 58.92/59.02 [27]~E(x271,x272)+E(f24(x271,x273,x274),f24(x272,x273,x274)) % 58.92/59.02 [28]~E(x281,x282)+E(f24(x283,x281,x284),f24(x283,x282,x284)) % 58.92/59.02 [29]~E(x291,x292)+E(f24(x293,x294,x291),f24(x293,x294,x292)) % 58.92/59.02 [30]~P1(x301)+P1(x302)+~E(x301,x302) % 58.92/59.02 [31]P10(x312,x313,x314,x315)+~E(x311,x312)+~P10(x311,x313,x314,x315) % 58.92/59.02 [32]P10(x323,x322,x324,x325)+~E(x321,x322)+~P10(x323,x321,x324,x325) % 58.92/59.02 [33]P10(x333,x334,x332,x335)+~E(x331,x332)+~P10(x333,x334,x331,x335) % 58.92/59.02 [34]P10(x343,x344,x345,x342)+~E(x341,x342)+~P10(x343,x344,x345,x341) % 58.92/59.02 [35]~P2(x351)+P2(x352)+~E(x351,x352) % 58.92/59.02 [36]~P20(x361)+P20(x362)+~E(x361,x362) % 58.92/59.02 [37]~P14(x371)+P14(x372)+~E(x371,x372) % 58.92/59.02 [38]~P17(x381)+P17(x382)+~E(x381,x382) % 58.92/59.02 [39]P13(x392,x393,x394)+~E(x391,x392)+~P13(x391,x393,x394) % 58.92/59.02 [40]P13(x403,x402,x404)+~E(x401,x402)+~P13(x403,x401,x404) % 58.92/59.02 [41]P13(x413,x414,x412)+~E(x411,x412)+~P13(x413,x414,x411) % 58.92/59.02 [42]P7(x422,x423,x424)+~E(x421,x422)+~P7(x421,x423,x424) % 58.92/59.02 [43]P7(x433,x432,x434)+~E(x431,x432)+~P7(x433,x431,x434) % 58.92/59.02 [44]P7(x443,x444,x442)+~E(x441,x442)+~P7(x443,x444,x441) % 58.92/59.02 [45]P8(x452,x453,x454)+~E(x451,x452)+~P8(x451,x453,x454) % 58.92/59.02 [46]P8(x463,x462,x464)+~E(x461,x462)+~P8(x463,x461,x464) % 58.92/59.02 [47]P8(x473,x474,x472)+~E(x471,x472)+~P8(x473,x474,x471) % 58.92/59.02 [48]P6(x482,x483)+~E(x481,x482)+~P6(x481,x483) % 58.92/59.02 [49]P6(x493,x492)+~E(x491,x492)+~P6(x493,x491) % 58.92/59.02 [50]~P12(x501)+P12(x502)+~E(x501,x502) % 58.92/59.02 [51]~P21(x511)+P21(x512)+~E(x511,x512) % 58.92/59.02 [52]P9(x522,x523,x524)+~E(x521,x522)+~P9(x521,x523,x524) % 58.92/59.02 [53]P9(x533,x532,x534)+~E(x531,x532)+~P9(x533,x531,x534) % 58.92/59.02 [54]P9(x543,x544,x542)+~E(x541,x542)+~P9(x543,x544,x541) % 58.92/59.02 [55]~P3(x551)+P3(x552)+~E(x551,x552) % 58.92/59.02 [56]~P15(x561)+P15(x562)+~E(x561,x562) % 58.92/59.02 [57]~P4(x571)+P4(x572)+~E(x571,x572) % 58.92/59.02 [58]~P19(x581)+P19(x582)+~E(x581,x582) % 58.92/59.02 [59]P11(x592,x593)+~E(x591,x592)+~P11(x591,x593) % 58.92/59.02 [60]P11(x603,x602)+~E(x601,x602)+~P11(x603,x601) % 58.92/59.02 [61]P5(x612,x613)+~E(x611,x612)+~P5(x611,x613) % 58.92/59.02 [62]P5(x623,x622)+~E(x621,x622)+~P5(x623,x621) % 58.92/59.02 [63]P16(x632,x633,x634)+~E(x631,x632)+~P16(x631,x633,x634) % 58.92/59.02 [64]P16(x643,x642,x644)+~E(x641,x642)+~P16(x643,x641,x644) % 58.92/59.02 [65]P16(x653,x654,x652)+~E(x651,x652)+~P16(x653,x654,x651) % 58.92/59.02 [66]~P18(x661)+P18(x662)+~E(x661,x662) % 58.92/59.02 % 58.92/59.02 %------------------------------------------- % 58.92/59.02 cnf(170,plain, % 58.92/59.02 (P5(f20(f28(x1701)),x1701)), % 58.92/59.02 inference(scs_inference,[],[99,134])). % 58.92/59.02 cnf(171,plain, % 58.92/59.02 (P6(f20(x1711),x1711)), % 58.92/59.02 inference(rename_variables,[],[99])). % 58.92/59.02 cnf(173,plain, % 58.92/59.02 (~P11(x1731,a18)), % 58.92/59.02 inference(scs_inference,[],[99,89,134,126])). % 58.92/59.02 cnf(175,plain, % 58.92/59.02 (~P8(a18,x1751,x1752)), % 58.92/59.02 inference(scs_inference,[],[99,89,134,126,142])). % 58.92/59.02 cnf(178,plain, % 58.92/59.02 (P5(x1781,x1781)), % 58.92/59.02 inference(rename_variables,[],[98])). % 58.92/59.02 cnf(182,plain, % 58.92/59.02 (P8(f22(x1821,x1822),x1821,x1822)), % 58.92/59.02 inference(rename_variables,[],[108])). % 58.92/59.02 cnf(183,plain, % 58.92/59.02 (~P17(f22(x1831,x1832))), % 58.92/59.02 inference(scs_inference,[],[116,98,178,108,99,89,134,126,142,61,62,45,120])). % 58.92/59.02 cnf(185,plain, % 58.92/59.02 (P11(f20(a3),a3)), % 58.92/59.02 inference(scs_inference,[],[116,98,178,108,99,171,89,114,134,126,142,61,62,45,120,130])). % 58.92/59.02 cnf(186,plain, % 58.92/59.02 (P6(f20(x1861),x1861)), % 58.92/59.02 inference(rename_variables,[],[99])). % 58.92/59.02 cnf(188,plain, % 58.92/59.02 (~P11(x1881,f20(f28(a18)))), % 58.92/59.02 inference(scs_inference,[],[116,98,178,108,99,171,89,114,134,126,142,61,62,45,120,130,137])). % 58.92/59.02 cnf(190,plain, % 58.92/59.02 (P18(a1)), % 58.92/59.02 inference(scs_inference,[],[71,75,110,116,98,178,108,99,171,89,114,134,126,142,61,62,45,120,130,137,122])). % 58.92/59.02 cnf(196,plain, % 58.92/59.02 (P8(f22(x1961,x1962),x1961,x1962)), % 58.92/59.02 inference(rename_variables,[],[108])). % 58.92/59.02 cnf(198,plain, % 58.92/59.02 (P13(f20(f22(x1981,a3)),x1981,a3)), % 58.92/59.02 inference(scs_inference,[],[71,75,110,116,98,178,108,182,196,99,171,186,83,87,89,92,114,134,126,142,61,62,45,120,130,137,122,123,161,165])). % 58.92/59.02 cnf(199,plain, % 58.92/59.02 (P8(f22(x1991,x1992),x1991,x1992)), % 58.92/59.02 inference(rename_variables,[],[108])). % 58.92/59.02 cnf(201,plain, % 58.92/59.02 (P9(f20(f22(x2011,a3)),x2011,a3)), % 58.92/59.02 inference(scs_inference,[],[71,75,110,116,98,178,108,182,196,199,99,171,186,83,87,89,92,114,134,126,142,61,62,45,120,130,137,122,123,161,165,166])). % 58.92/59.02 cnf(204,plain, % 58.92/59.02 (P16(f5(x2041,a3),x2041,a3)), % 58.92/59.02 inference(scs_inference,[],[71,75,110,116,98,178,105,107,108,182,196,199,99,171,186,83,87,89,92,114,102,134,126,142,61,62,45,120,130,137,122,123,161,165,166,153])). % 58.92/59.02 cnf(205,plain, % 58.92/59.02 (P13(f5(x2051,x2052),x2051,x2052)), % 58.92/59.02 inference(rename_variables,[],[107])). % 58.92/59.02 cnf(206,plain, % 58.92/59.02 (P12(f5(x2061,x2062))), % 58.92/59.02 inference(rename_variables,[],[102])). % 58.92/59.02 cnf(207,plain, % 58.92/59.02 (P7(f5(x2071,x2072),x2071,x2072)), % 58.92/59.02 inference(rename_variables,[],[105])). % 58.92/59.02 cnf(209,plain, % 58.92/59.02 (~P17(f5(a3,a3))), % 58.92/59.02 inference(scs_inference,[],[71,75,110,116,98,178,105,207,107,205,108,182,196,199,99,171,186,83,87,89,92,114,102,206,134,126,142,61,62,45,120,130,137,122,123,161,165,166,153,151])). % 58.92/59.02 cnf(210,plain, % 58.92/59.02 (P13(f5(x2101,x2102),x2101,x2102)), % 58.92/59.02 inference(rename_variables,[],[107])). % 58.92/59.02 cnf(214,plain, % 58.92/59.02 (P5(a18,x2141)), % 58.92/59.02 inference(scs_inference,[],[71,75,110,116,98,178,105,207,107,205,108,182,196,199,99,171,186,83,87,89,92,114,102,206,134,126,142,61,62,45,120,130,137,122,123,161,165,166,153,151,136])). % 58.92/59.02 cnf(219,plain, % 58.92/59.02 (P10(f20(f22(x2191,a3)),x2192,a3,f22(x2191,a3))+~E(x2191,x2192)), % 58.92/59.02 inference(scs_inference,[],[71,75,110,116,98,178,105,207,107,205,108,182,196,199,99,171,186,83,87,89,92,114,102,206,134,126,142,61,62,45,120,130,137,122,123,161,165,166,153,151,136,133,31,32])). % 58.92/59.02 cnf(221,plain, % 58.92/59.02 (P10(f20(f22(x2211,a3)),x2211,a3,x2212)+~E(f22(x2211,a3),x2212)), % 58.92/59.02 inference(scs_inference,[],[71,75,110,116,98,178,105,207,107,205,108,182,196,199,99,171,186,83,87,89,92,114,102,206,134,126,142,61,62,45,120,130,137,122,123,161,165,166,153,151,136,133,31,32,33,34])). % 58.92/59.02 cnf(223,plain, % 58.92/59.02 (P13(f5(x2231,x2232),x2233,x2232)+~E(x2231,x2233)), % 58.92/59.02 inference(scs_inference,[],[71,75,110,116,98,178,105,207,107,205,210,108,182,196,199,99,171,186,83,87,89,92,114,102,206,134,126,142,61,62,45,120,130,137,122,123,161,165,166,153,151,136,133,31,32,33,34,39,40])). % 58.92/59.02 cnf(230,plain, % 58.92/59.02 (~P11(x2301,a7)), % 58.92/59.02 inference(scs_inference,[],[90,126])). % 58.92/59.02 cnf(232,plain, % 58.92/59.02 (P5(f20(f28(a18)),x2321)), % 58.92/59.02 inference(scs_inference,[],[188,90,126,136])). % 58.92/59.02 cnf(233,plain, % 58.92/59.02 (~P11(x2331,f20(f28(a18)))), % 58.92/59.02 inference(rename_variables,[],[188])). % 58.92/59.02 cnf(235,plain, % 58.92/59.02 (~P8(a7,x2351,x2352)), % 58.92/59.02 inference(scs_inference,[],[188,90,126,136,142])). % 58.92/59.02 cnf(239,plain, % 58.92/59.02 (~P11(x2391,f20(f28(a7)))), % 58.92/59.02 inference(scs_inference,[],[188,233,185,90,99,126,136,142,60,138])). % 58.92/59.02 cnf(240,plain, % 58.92/59.02 (P6(f20(x2401),x2401)), % 58.92/59.02 inference(rename_variables,[],[99])). % 58.92/59.02 cnf(244,plain, % 58.92/59.02 (P11(f20(f22(x2441,x2442)),f22(x2441,x2442))), % 58.92/59.02 inference(scs_inference,[],[116,214,183,188,233,185,90,99,240,126,136,142,60,138,61,130])). % 58.92/59.02 cnf(245,plain, % 58.92/59.02 (P6(f20(x2451),x2451)), % 58.92/59.02 inference(rename_variables,[],[99])). % 58.92/59.02 cnf(247,plain, % 58.92/59.02 (P10(f20(f22(x2471,a11)),x2471,a11,f22(x2471,a11))), % 58.92/59.02 inference(scs_inference,[],[116,214,183,188,233,185,90,115,108,99,240,245,126,136,142,60,138,61,130,161])). % 58.92/59.02 cnf(249,plain, % 58.92/59.02 (P8(f22(x2491,x2492),x2491,x2492)), % 58.92/59.02 inference(rename_variables,[],[108])). % 58.92/59.02 cnf(251,plain, % 58.92/59.02 (P9(f20(f22(x2511,a11)),x2511,a11)), % 58.92/59.02 inference(scs_inference,[],[116,214,183,188,233,185,90,115,108,249,99,240,245,126,136,142,60,138,61,130,161,166])). % 58.92/59.02 cnf(252,plain, % 58.92/59.02 (P8(f22(x2521,x2522),x2521,x2522)), % 58.92/59.02 inference(rename_variables,[],[108])). % 58.92/59.02 cnf(254,plain, % 58.92/59.02 (P13(f20(f22(x2541,a11)),x2541,a11)), % 58.92/59.02 inference(scs_inference,[],[116,214,183,188,233,185,90,115,108,249,252,99,240,245,126,136,142,60,138,61,130,161,166,165])). % 58.92/59.02 cnf(255,plain, % 58.92/59.02 (P8(f22(x2551,x2552),x2551,x2552)), % 58.92/59.02 inference(rename_variables,[],[108])). % 58.92/59.02 cnf(257,plain, % 58.92/59.02 (~P11(f22(x2571,x2572),f20(f22(x2571,x2572)))), % 58.92/59.02 inference(scs_inference,[],[116,214,183,188,233,185,90,115,108,249,252,99,240,245,126,136,142,60,138,61,130,161,166,165,133])). % 58.92/59.02 cnf(260,plain, % 58.92/59.02 (~P17(f27(a1))), % 58.92/59.02 inference(scs_inference,[],[116,214,183,188,233,185,198,90,115,108,249,252,99,240,245,89,126,136,142,60,138,61,130,161,166,165,133,41,120])). % 58.92/59.02 cnf(263,plain, % 58.92/59.02 (P7(f21(x2631,x2632),x2633,x2632)+~E(x2631,x2633)), % 58.92/59.02 inference(scs_inference,[],[116,214,183,188,233,104,185,198,90,115,108,249,252,99,240,245,89,126,136,142,60,138,61,130,161,166,165,133,41,120,42,43])). % 58.92/59.02 cnf(264,plain, % 58.92/59.02 (P7(f21(x2641,x2642),x2641,x2643)+~E(x2642,x2643)), % 58.92/59.02 inference(scs_inference,[],[116,214,183,188,233,104,185,198,90,115,108,249,252,99,240,245,89,126,136,142,60,138,61,130,161,166,165,133,41,120,42,43,44])). % 58.92/59.02 cnf(265,plain, % 58.92/59.02 (P8(f22(x2651,x2652),x2653,x2652)+~E(x2651,x2653)), % 58.92/59.02 inference(scs_inference,[],[116,214,183,188,233,104,185,198,90,115,108,249,252,255,99,240,245,89,126,136,142,60,138,61,130,161,166,165,133,41,120,42,43,44,46])). % 58.92/59.02 cnf(266,plain, % 58.92/59.02 (P8(f22(x2661,x2662),x2661,x2663)+~E(x2662,x2663)), % 58.92/59.02 inference(scs_inference,[],[116,214,183,188,233,104,185,198,90,115,108,249,252,255,99,240,245,89,126,136,142,60,138,61,130,161,166,165,133,41,120,42,43,44,46,47])). % 58.92/59.02 cnf(273,plain, % 58.92/59.02 (~P11(x2731,a9)), % 58.92/59.02 inference(scs_inference,[],[91,126])). % 58.92/59.02 cnf(275,plain, % 58.92/59.02 (P5(f20(f28(a7)),x2751)), % 58.92/59.02 inference(scs_inference,[],[239,91,126,136])). % 58.92/59.02 cnf(276,plain, % 58.92/59.02 (~P11(x2761,f20(f28(a7)))), % 58.92/59.02 inference(rename_variables,[],[239])). % 58.92/59.02 cnf(278,plain, % 58.92/59.02 (~P8(a9,x2781,x2782)), % 58.92/59.02 inference(scs_inference,[],[239,91,126,136,142])). % 58.92/59.02 cnf(280,plain, % 58.92/59.02 (~P11(x2801,f20(f28(a9)))), % 58.92/59.02 inference(scs_inference,[],[239,91,99,126,136,142,138])). % 58.92/59.02 cnf(281,plain, % 58.92/59.02 (P6(f20(x2811),x2811)), % 58.92/59.02 inference(rename_variables,[],[99])). % 58.92/59.02 cnf(287,plain, % 58.92/59.02 (P11(f20(a11),a11)), % 58.92/59.02 inference(scs_inference,[],[116,232,115,244,239,276,91,99,281,126,136,142,138,60,61,130])). % 58.92/59.02 cnf(288,plain, % 58.92/59.02 (P6(f20(x2881),x2881)), % 58.92/59.02 inference(rename_variables,[],[99])). % 58.92/59.02 cnf(292,plain, % 58.92/59.02 (P6(x2921,x2922)+~E(f20(x2922),x2921)), % 58.92/59.02 inference(scs_inference,[],[116,232,115,244,239,276,91,99,281,288,126,136,142,138,60,61,130,133,48])). % 58.92/59.02 cnf(300,plain, % 58.92/59.02 (P5(f20(f28(a9)),x3001)), % 58.92/59.02 inference(scs_inference,[],[280,136])). % 58.92/59.02 cnf(301,plain, % 58.92/59.02 (~P11(x3011,f20(f28(a9)))), % 58.92/59.02 inference(rename_variables,[],[280])). % 58.92/59.02 cnf(303,plain, % 58.92/59.02 (~P11(x3031,a8)), % 58.92/59.02 inference(scs_inference,[],[280,92,136,126])). % 58.92/59.02 cnf(307,plain, % 58.92/59.02 (~P11(x3071,f20(f28(a8)))), % 58.92/59.02 inference(scs_inference,[],[280,92,99,136,126,142,138])). % 58.92/59.02 cnf(308,plain, % 58.92/59.02 (P6(f20(x3081),x3081)), % 58.92/59.02 inference(rename_variables,[],[99])). % 58.92/59.02 cnf(314,plain, % 58.92/59.02 (P11(f20(f5(a3,a3)),f5(a3,a3))), % 58.92/59.02 inference(scs_inference,[],[116,275,280,301,209,287,92,99,308,136,126,142,138,61,60,130])). % 58.92/59.02 cnf(315,plain, % 58.92/59.02 (P6(f20(x3151),x3151)), % 58.92/59.02 inference(rename_variables,[],[99])). % 58.92/59.02 cnf(319,plain, % 59.08/59.03 (P16(x3191,x3192,a3)+~E(f5(x3192,a3),x3191)), % 59.08/59.03 inference(scs_inference,[],[116,275,204,280,301,209,287,92,99,308,136,126,142,138,61,60,130,133,63])). % 59.08/59.03 cnf(320,plain, % 59.08/59.03 (P16(f5(x3201,a3),x3202,a3)+~E(x3201,x3202)), % 59.08/59.03 inference(scs_inference,[],[116,275,204,280,301,209,287,92,99,308,136,126,142,138,61,60,130,133,63,64])). % 59.08/59.03 cnf(326,plain, % 59.08/59.03 (P6(x3261,x3262)+~E(x3263,x3261)+~P11(x3263,f20(f28(x3262)))), % 59.08/59.03 inference(scs_inference,[],[116,275,204,280,301,247,209,287,92,99,308,315,136,126,142,138,61,60,130,133,139,48])). % 59.08/59.03 cnf(332,plain, % 59.08/59.03 (P5(f20(f28(a8)),x3321)), % 59.08/59.03 inference(scs_inference,[],[307,136])). % 59.08/59.03 cnf(333,plain, % 59.08/59.03 (~P11(x3331,f20(f28(a8)))), % 59.08/59.03 inference(rename_variables,[],[307])). % 59.08/59.03 cnf(337,plain, % 59.08/59.03 (P11(f20(f27(a1)),f27(a1))), % 59.08/59.03 inference(scs_inference,[],[314,307,333,260,99,136,60,130])). % 59.08/59.03 cnf(344,plain, % 59.08/59.03 (P10(f20(f22(x3441,a11)),x3442,a11,f22(x3441,a11))+~E(x3441,x3442)), % 59.08/59.03 inference(scs_inference,[],[116,300,314,307,333,260,247,99,136,60,130,61,133,32])). % 59.08/59.03 cnf(345,plain, % 59.08/59.03 (P13(f20(f22(x3451,a11)),x3452,a11)+~E(x3451,x3452)), % 59.08/59.03 inference(scs_inference,[],[116,300,314,307,333,254,260,247,99,136,60,130,61,133,32,40])). % 59.08/59.03 cnf(347,plain, % 59.08/59.03 (P7(f10(x3471,x3472),x3471,x3473)+~E(x3472,x3473)), % 59.08/59.03 inference(scs_inference,[],[116,300,314,307,333,106,254,260,247,99,136,60,130,61,133,32,40,39,44])). % 59.08/59.03 cnf(349,plain, % 59.08/59.03 (P13(f5(x3491,x3492),x3491,x3493)+~E(x3492,x3493)), % 59.08/59.03 inference(scs_inference,[],[116,300,107,314,307,333,106,254,260,247,99,136,60,130,61,133,32,40,39,44,59,41])). % 59.08/59.03 cnf(356,plain, % 59.08/59.03 (P5(a7,x3561)), % 59.08/59.03 inference(scs_inference,[],[230,136])). % 59.08/59.03 cnf(363,plain, % 59.08/59.03 (P6(f20(x3631),x3632)+~E(x3631,x3632)), % 59.08/59.03 inference(scs_inference,[],[116,332,337,173,230,99,136,60,61,49])). % 59.08/59.03 cnf(374,plain, % 59.08/59.03 (P5(a9,x3741)), % 59.08/59.03 inference(scs_inference,[],[273,136])). % 59.08/59.03 cnf(375,plain, % 59.08/59.03 (~P11(x3751,a9)), % 59.08/59.03 inference(rename_variables,[],[273])). % 59.08/59.03 cnf(384,plain, % 59.08/59.03 (P7(f5(x3841,x3842),x3843,x3842)+~E(x3841,x3843)), % 59.08/59.03 inference(scs_inference,[],[116,356,108,185,235,273,375,105,247,136,45,60,61,33,43])). % 59.08/59.03 cnf(386,plain, % 59.08/59.03 (P5(f20(f28(x3861)),x3862)+~E(x3861,x3862)), % 59.08/59.03 inference(scs_inference,[],[116,170,356,108,185,235,201,273,375,105,247,136,45,60,61,33,43,54,62])). % 59.08/59.03 cnf(388,plain, % 59.08/59.03 (P9(f20(f22(x3881,a3)),x3882,a3)+~E(x3881,x3882)), % 59.08/59.03 inference(scs_inference,[],[116,170,356,108,185,235,201,273,375,105,247,136,45,60,61,33,43,54,62,42,53])). % 59.08/59.03 cnf(395,plain, % 59.08/59.03 (P5(a8,x3951)), % 59.08/59.03 inference(scs_inference,[],[303,136])). % 59.08/59.03 cnf(396,plain, % 59.08/59.03 (~P11(x3961,a8)), % 59.08/59.03 inference(rename_variables,[],[303])). % 59.08/59.03 cnf(405,plain, % 59.08/59.03 (P10(f20(f22(x4051,a11)),x4051,a11,x4052)+~E(f22(x4051,a11),x4052)), % 59.08/59.03 inference(scs_inference,[],[116,374,108,287,278,251,303,396,247,136,45,60,61,52,34])). % 59.08/59.03 cnf(406,plain, % 59.08/59.03 (P7(f5(x4061,x4062),x4061,x4063)+~E(x4062,x4063)), % 59.08/59.03 inference(scs_inference,[],[116,374,108,287,278,251,303,396,247,105,136,45,60,61,52,34,44])). % 59.08/59.03 cnf(407,plain, % 59.08/59.03 (P7(f10(x4071,x4072),x4073,x4072)+~E(x4071,x4073)), % 59.08/59.03 inference(scs_inference,[],[116,374,108,287,278,251,303,396,106,247,105,136,45,60,61,52,34,44,43])). % 59.08/59.03 cnf(408,plain, % 59.08/59.03 (P13(f20(f22(x4081,a3)),x4082,a3)+~E(x4081,x4082)), % 59.08/59.03 inference(scs_inference,[],[116,374,108,287,278,251,303,396,106,198,247,105,136,45,60,61,52,34,44,43,40])). % 59.08/59.03 cnf(434,plain, % 59.08/59.03 (P9(f20(f22(x4341,a11)),x4342,a11)+~E(x4341,x4342)), % 59.08/59.03 inference(scs_inference,[],[185,239,251,254,60,41,54,53])). % 59.08/59.03 cnf(445,plain, % 59.08/59.03 (P9(f23(x4451,x4452),x4453,x4452)+~E(x4451,x4453)), % 59.08/59.03 inference(scs_inference,[],[314,287,280,201,109,60,52,59,53])). % 59.08/59.03 cnf(446,plain, % 59.08/59.03 (P9(f23(x4461,x4462),x4461,x4463)+~E(x4462,x4463)), % 59.08/59.03 inference(scs_inference,[],[314,287,280,201,109,60,52,59,53,54])). % 59.08/59.03 cnf(500,plain, % 59.08/59.03 (~E(a9,x5001)+P12(x5001)), % 59.08/59.03 inference(scs_inference,[],[91,118,50])). % 59.08/59.03 cnf(501,plain, % 59.08/59.03 (P12(a9)), % 59.08/59.03 inference(equality_inference,[],[500])). % 59.08/59.03 cnf(519,plain, % 59.08/59.03 (P11(f20(f10(x5191,x5192)),f10(x5191,x5192))+P19(f10(x5191,x5192))), % 59.08/59.03 inference(scs_inference,[],[99,314,239,101,103,60,123,130])). % 59.08/59.03 cnf(528,plain, % 59.08/59.03 (P11(f20(f5(x5281,x5282)),f5(x5281,x5282))+P19(f5(x5281,x5282))), % 59.08/59.03 inference(scs_inference,[],[99,337,280,100,102,60,123,130])). % 59.08/59.03 cnf(598,plain, % 59.08/59.03 (~P17(f31(a1))), % 59.08/59.03 inference(scs_inference,[],[75,110,119,124])). % 59.08/59.03 cnf(599,plain, % 59.08/59.03 (P11(f20(f31(a1)),f31(a1))), % 59.08/59.03 inference(scs_inference,[],[598,99,130])). % 59.08/59.03 cnf(604,plain, % 59.08/59.03 (P16(f5(x6041,f31(a1)),x6041,f31(a1))), % 59.08/59.03 inference(scs_inference,[],[598,107,99,105,102,273,130,60,153])). % 59.08/59.03 cnf(605,plain, % 59.08/59.03 (P13(f5(x6051,x6052),x6051,x6052)), % 59.08/59.03 inference(rename_variables,[],[107])). % 59.08/59.03 cnf(606,plain, % 59.08/59.03 (P12(f5(x6061,x6062))), % 59.08/59.03 inference(rename_variables,[],[102])). % 59.08/59.03 cnf(607,plain, % 59.08/59.03 (P7(f5(x6071,x6072),x6071,x6072)), % 59.08/59.03 inference(rename_variables,[],[105])). % 59.08/59.03 cnf(609,plain, % 59.08/59.03 (~P17(f5(f31(a1),f31(a1)))), % 59.08/59.03 inference(scs_inference,[],[598,107,605,99,105,607,102,606,273,130,60,153,151])). % 59.08/59.03 cnf(616,plain, % 59.08/59.03 (P16(f5(x6161,f31(a1)),x6162,f31(a1))+~E(x6161,x6162)), % 59.08/59.03 inference(scs_inference,[],[598,107,605,99,105,607,102,606,273,130,60,153,151,133,64])). % 59.08/59.03 cnf(617,plain, % 59.08/59.03 (P16(x6171,x6172,f31(a1))+~E(f5(x6172,f31(a1)),x6171)), % 59.08/59.03 inference(scs_inference,[],[598,107,605,99,105,607,102,606,273,130,60,153,151,133,64,63])). % 59.08/59.03 cnf(640,plain, % 59.08/59.03 (~P9(a9,f31(a1),f31(a1))+~P10(a9,f31(a1),f31(a1),f22(f31(a1),f31(a1)))), % 59.08/59.03 inference(scs_inference,[],[598,501,108,287,91,188,60,165,151,148])). % 59.08/59.03 cnf(650,plain, % 59.08/59.03 (~P10(a9,f31(a1),f31(a1),f22(f31(a1),f31(a1)))), % 59.08/59.03 inference(scs_inference,[],[598,108,287,239,60,166,640])). % 59.08/59.03 cnf(655,plain, % 59.08/59.03 (~P6(a9,f22(f31(a1),f31(a1)))), % 59.08/59.03 inference(scs_inference,[],[598,108,185,280,650,60,161])). % 59.08/59.03 cnf(956,plain, % 59.08/59.03 (E(a1,f26(f31(a1),f30(a1)))), % 59.08/59.03 inference(scs_inference,[],[75,67,2,131])). % 59.08/59.03 cnf(960,plain, % 59.08/59.03 (P7(f21(x9601,a1),x9601,f26(f31(a1),f30(a1)))), % 59.08/59.03 inference(scs_inference,[],[956,386,223,263,264])). % 59.08/59.03 cnf(961,plain, % 59.08/59.03 (P8(f22(a1,x9611),f26(f31(a1),f30(a1)),x9611)), % 59.08/59.03 inference(scs_inference,[],[956,386,223,263,264,265])). % 59.08/59.03 cnf(966,plain, % 59.08/59.03 (P7(f5(a1,x9661),f26(f31(a1),f30(a1)),x9661)), % 59.08/59.03 inference(scs_inference,[],[956,386,223,263,264,265,266,347,349,363,384])). % 59.08/59.03 cnf(968,plain, % 59.08/59.03 (P7(f10(a1,x9681),f26(f31(a1),f30(a1)),x9681)), % 59.08/59.03 inference(scs_inference,[],[956,386,223,263,264,265,266,347,349,363,384,406,407])). % 59.08/59.03 cnf(969,plain, % 59.08/59.03 (P9(f23(a1,x9691),f26(f31(a1),f30(a1)),x9691)), % 59.08/59.03 inference(scs_inference,[],[956,386,223,263,264,265,266,347,349,363,384,406,407,445])). % 59.08/59.03 cnf(970,plain, % 59.08/59.03 (P9(f23(x9701,a1),x9701,f26(f31(a1),f30(a1)))), % 59.08/59.03 inference(scs_inference,[],[956,386,223,263,264,265,266,347,349,363,384,406,407,445,446])). % 59.08/59.03 cnf(971,plain, % 59.08/59.03 (E(f26(f31(a1),f30(a1)),a1)), % 59.08/59.03 inference(scs_inference,[],[956,386,223,263,264,265,266,347,349,363,384,406,407,445,446,2])). % 59.08/59.03 cnf(981,plain, % 59.08/59.03 (P8(f22(a1,a1),f26(f31(a1),f30(a1)),f26(f31(a1),f30(a1)))), % 59.08/59.03 inference(scs_inference,[],[67,71,73,110,75,190,956,198,386,223,263,264,265,266,347,349,363,384,406,407,445,446,2,30,35,36,37,51,66,40,44,47])). % 59.08/59.03 cnf(1010,plain, % 59.08/59.03 (P13(f20(f22(a1,a11)),f26(f31(a1),f30(a1)),a11)), % 59.08/59.03 inference(scs_inference,[],[956,254,40])). % 59.08/59.03 cnf(1014,plain, % 59.08/59.03 (P10(f20(f22(a1,a11)),f26(f31(a1),f30(a1)),a11,f22(a1,a11))), % 59.08/59.03 inference(scs_inference,[],[956,966,247,254,40,44,32])). % 59.08/59.03 cnf(1016,plain, % 59.08/59.03 (P9(f20(f22(a1,a11)),f26(f31(a1),f30(a1)),a11)), % 59.08/59.03 inference(scs_inference,[],[956,966,247,254,251,40,44,32,53])). % 59.08/59.03 cnf(1228,plain, % 59.08/59.03 (P6(a18,f28(x12281))), % 59.08/59.03 inference(scs_inference,[],[173,132,136])). % 59.08/59.03 cnf(1229,plain, % 59.08/59.03 (P15(a18)), % 59.08/59.03 inference(scs_inference,[],[1228,145])). % 59.08/59.03 cnf(1232,plain, % 59.08/59.03 (~E(f31(a1),a7)), % 59.08/59.03 inference(scs_inference,[],[599,230,1228,145,60])). % 59.08/59.03 cnf(7289,plain, % 59.08/59.03 (~P11(f10(x72891,x72892),f20(f10(x72891,x72892)))+P19(f10(x72891,x72892))), % 59.08/59.03 inference(scs_inference,[],[519,133])). % 59.08/59.03 cnf(7350,plain, % 59.08/59.03 (~P11(f5(x73501,x73502),f20(f5(x73501,x73502)))+P19(f5(x73501,x73502))), % 59.08/59.03 inference(scs_inference,[],[528,133])). % 59.08/59.03 cnf(9283,plain, % 59.08/59.03 (~E(f10(x92831,x92832),x92833)+~P11(f10(x92831,x92832),f20(f10(x92831,x92832)))+P19(x92833)), % 59.08/59.03 inference(scs_inference,[],[7289,58])). % 59.08/59.03 cnf(9345,plain, % 59.08/59.03 (~E(f5(x93451,x93452),x93453)+~P11(f5(x93451,x93452),f20(f5(x93451,x93452)))+P19(x93453)), % 59.08/59.03 inference(scs_inference,[],[7350,58])). % 59.08/59.03 cnf(11555,plain, % 59.08/59.03 (P12(f30(a14))), % 59.08/59.03 inference(scs_inference,[],[76,89,118,119,121])). % 59.08/59.03 cnf(11557,plain, % 59.08/59.03 (P6(x115571,f28(x115571))), % 59.08/59.03 inference(scs_inference,[],[76,98,89,118,119,121,132])). % 59.08/59.03 cnf(11563,plain, % 59.08/59.03 (P13(f30(a14),f29(f31(a14),f31(a14)),f31(a14))), % 59.08/59.03 inference(scs_inference,[],[76,98,960,251,89,118,119,121,132,149,150,146])). % 59.08/59.03 cnf(11565,plain, % 59.08/59.03 (P9(f30(a14),f29(f31(a14),f31(a14)),f31(a14))), % 59.08/59.03 inference(scs_inference,[],[76,98,960,251,89,118,119,121,132,149,150,146,147])). % 59.08/59.03 cnf(11567,plain, % 59.08/59.03 (E(a7,a18)), % 59.08/59.03 inference(scs_inference,[],[76,98,960,251,89,90,118,119,121,132,149,150,146,147,117])). % 59.08/59.03 cnf(11574,plain, % 59.08/59.03 (P3(f22(a1,a1))), % 59.08/59.03 inference(scs_inference,[],[76,1232,981,98,960,1016,251,89,90,116,118,119,121,132,149,150,146,147,117,148,2,134,141])). % 59.08/59.03 cnf(11576,plain, % 59.08/59.03 (~P11(f17(f27(a1),f25(a1)),f25(a1))), % 59.08/59.03 inference(scs_inference,[],[76,1232,981,98,960,1016,251,89,90,116,118,119,121,132,149,150,146,147,117,148,2,134,141,140])). % 59.08/59.03 cnf(11578,plain, % 59.08/59.03 (P11(f17(f27(a1),f25(a1)),f27(a1))), % 59.08/59.03 inference(scs_inference,[],[76,1232,981,98,960,1016,251,89,90,116,118,119,121,132,149,150,146,147,117,148,2,134,141,140,136])). % 59.08/59.03 cnf(11583,plain, % 59.08/59.03 (P6(f20(x115831),x115831)), % 59.08/59.03 inference(rename_variables,[],[99])). % 59.08/59.03 cnf(11586,plain, % 59.08/59.03 (P6(f20(x115861),x115861)), % 59.08/59.03 inference(rename_variables,[],[99])). % 59.08/59.03 cnf(11588,plain, % 59.08/59.03 (~P17(f31(a15))), % 59.08/59.03 inference(scs_inference,[],[76,80,97,113,1232,981,98,960,1016,251,89,90,116,99,11583,118,119,121,132,149,150,146,147,117,148,2,134,141,140,136,133,127,128,124])). % 59.08/59.03 cnf(11590,plain, % 59.08/59.03 (~P17(f16(a15))), % 59.08/59.03 inference(scs_inference,[],[76,80,97,113,1232,981,98,960,1016,251,89,90,116,99,11583,118,119,121,132,149,150,146,147,117,148,2,134,141,140,136,133,127,128,124,125])). % 59.08/59.03 cnf(11596,plain, % 59.08/59.03 (P17(f20(f28(a18)))), % 59.08/59.03 inference(scs_inference,[],[68,76,77,80,97,113,1232,981,98,960,1016,188,251,89,90,116,99,11583,11586,118,119,121,132,149,150,146,147,117,148,2,134,141,140,136,133,127,128,124,125,135,131,130])). % 59.08/59.03 cnf(11597,plain, % 59.08/59.03 (~P11(x115971,f20(f28(a18)))), % 59.08/59.03 inference(rename_variables,[],[188])). % 59.08/59.03 cnf(11601,plain, % 59.08/59.03 (~P11(x116011,f20(f28(a18)))), % 59.08/59.03 inference(rename_variables,[],[188])). % 59.08/59.03 cnf(11602,plain, % 59.08/59.03 (~P6(f31(a1),f28(a18))), % 59.08/59.03 inference(scs_inference,[],[68,76,77,80,97,113,1232,981,98,960,1016,188,11597,251,599,89,90,116,99,11583,11586,118,119,121,132,149,150,146,147,117,148,2,134,141,140,136,133,127,128,124,125,135,131,130,60,138])). % 59.08/59.03 cnf(11606,plain, % 59.08/59.03 (~E(f28(a9),f22(f31(a1),f31(a1)))), % 59.08/59.03 inference(scs_inference,[],[68,76,77,80,97,113,1232,655,981,98,960,1016,188,11597,1228,251,599,89,90,116,99,11583,11586,118,119,121,132,149,150,146,147,117,148,2,134,141,140,136,133,127,128,124,125,135,131,130,60,138,48,49])). % 59.08/59.03 cnf(11613,plain, % 59.08/59.03 (P8(f27(a12),f31(a12),f31(a12))), % 59.08/59.03 inference(scs_inference,[],[68,70,74,76,77,79,80,97,112,113,1229,1232,655,981,72,98,609,960,1016,188,11597,11601,1228,251,599,89,90,116,99,11583,11586,118,119,121,132,149,150,146,147,117,148,2,134,141,140,136,133,127,128,124,125,135,131,130,60,138,48,49,137,38,123,143])). % 59.08/59.03 cnf(11615,plain, % 59.08/59.03 (P8(f25(a12),f31(a12),f31(a12))), % 59.08/59.03 inference(scs_inference,[],[68,70,74,76,77,79,80,97,112,113,1229,1232,655,981,72,98,609,960,1016,188,11597,11601,1228,251,599,89,90,116,99,11583,11586,118,119,121,132,149,150,146,147,117,148,2,134,141,140,136,133,127,128,124,125,135,131,130,60,138,48,49,137,38,123,143,144])). % 59.08/59.03 cnf(11618,plain, % 59.08/59.03 (E(f20(a7),f20(a18))), % 59.08/59.03 inference(scs_inference,[],[68,70,74,76,77,79,80,97,112,113,1229,1232,655,981,72,98,609,960,1016,188,11597,11601,1228,251,599,89,90,116,99,11583,11586,118,119,121,132,149,150,146,147,117,148,2,134,141,140,136,133,127,128,124,125,135,131,130,60,138,48,49,137,38,123,143,144,292,4])). % 59.08/59.03 cnf(11623,plain, % 59.08/59.03 (E(f28(a7),f28(a18))), % 59.08/59.03 inference(scs_inference,[],[68,70,74,76,77,79,80,97,112,113,1229,1232,655,981,72,98,609,960,1016,188,11597,11601,1228,251,599,89,90,116,99,11583,11586,118,119,121,132,149,150,146,147,117,148,2,134,141,140,136,133,127,128,124,125,135,131,130,60,138,48,49,137,38,123,143,144,292,4,9,10,13,22,23])). % 59.08/59.03 cnf(11626,plain, % 59.08/59.03 (E(f5(a7,x116261),f5(a18,x116261))), % 59.08/59.03 inference(scs_inference,[],[68,70,74,76,77,79,80,97,112,113,1229,1232,655,981,72,98,609,960,1016,188,11597,11601,1228,251,599,89,90,116,99,11583,11586,118,119,121,132,149,150,146,147,117,148,2,134,141,140,136,133,127,128,124,125,135,131,130,60,138,48,49,137,38,123,143,144,292,4,9,10,13,22,23,26,320,5])). % 59.08/59.03 cnf(11627,plain, % 59.08/59.03 (E(f5(x116271,a7),f5(x116271,a18))), % 59.08/59.03 inference(scs_inference,[],[68,70,74,76,77,79,80,97,112,113,1229,1232,655,981,72,98,609,960,1016,188,11597,11601,1228,251,599,89,90,116,99,11583,11586,118,119,121,132,149,150,146,147,117,148,2,134,141,140,136,133,127,128,124,125,135,131,130,60,138,48,49,137,38,123,143,144,292,4,9,10,13,22,23,26,320,5,6])). % 59.08/59.03 cnf(11628,plain, % 59.08/59.03 (E(f10(a7,x116281),f10(a18,x116281))), % 59.08/59.03 inference(scs_inference,[],[68,70,74,76,77,79,80,97,112,113,1229,1232,655,981,72,98,609,960,1016,188,11597,11601,1228,251,599,89,90,116,99,11583,11586,118,119,121,132,149,150,146,147,117,148,2,134,141,140,136,133,127,128,124,125,135,131,130,60,138,48,49,137,38,123,143,144,292,4,9,10,13,22,23,26,320,5,6,7])). % 59.08/59.03 cnf(11636,plain, % 59.08/59.03 (E(f22(a7,x116361),f22(a18,x116361))), % 59.08/59.03 inference(scs_inference,[],[68,70,74,76,77,79,80,97,112,113,1229,1232,655,981,72,98,609,960,1016,188,11597,11601,1228,251,599,89,90,116,99,11583,11586,118,119,121,132,149,150,146,147,117,148,2,134,141,140,136,133,127,128,124,125,135,131,130,60,138,48,49,137,38,123,143,144,292,4,9,10,13,22,23,26,320,5,6,7,8,11,12,14,15,16,17,18])). % 59.08/59.03 cnf(11637,plain, % 59.08/59.03 (E(f22(x116371,a7),f22(x116371,a18))), % 59.08/59.03 inference(scs_inference,[],[68,70,74,76,77,79,80,97,112,113,1229,1232,655,981,72,98,609,960,1016,188,11597,11601,1228,251,599,89,90,116,99,11583,11586,118,119,121,132,149,150,146,147,117,148,2,134,141,140,136,133,127,128,124,125,135,131,130,60,138,48,49,137,38,123,143,144,292,4,9,10,13,22,23,26,320,5,6,7,8,11,12,14,15,16,17,18,19])). % 59.08/59.03 cnf(11646,plain, % 59.08/59.03 (E(f24(a7,x116461,x116462),f24(a18,x116461,x116462))), % 59.08/59.03 inference(scs_inference,[],[68,70,74,76,77,79,80,97,112,113,1229,1232,655,981,72,98,609,960,1016,188,11597,11601,1228,251,599,89,90,116,99,11583,11586,118,119,121,132,149,150,146,147,117,148,2,134,141,140,136,133,127,128,124,125,135,131,130,60,138,48,49,137,38,123,143,144,292,4,9,10,13,22,23,26,320,5,6,7,8,11,12,14,15,16,17,18,19,20,21,24,25,345,388,408,434,27])). % 59.08/59.03 cnf(11647,plain, % 59.08/59.03 (E(f24(x116471,a7,x116472),f24(x116471,a18,x116472))), % 59.08/59.03 inference(scs_inference,[],[68,70,74,76,77,79,80,97,112,113,1229,1232,655,981,72,98,609,960,1016,188,11597,11601,1228,251,599,89,90,116,99,11583,11586,118,119,121,132,149,150,146,147,117,148,2,134,141,140,136,133,127,128,124,125,135,131,130,60,138,48,49,137,38,123,143,144,292,4,9,10,13,22,23,26,320,5,6,7,8,11,12,14,15,16,17,18,19,20,21,24,25,345,388,408,434,27,28])). % 59.08/59.03 cnf(11648,plain, % 59.08/59.03 (E(f24(x116481,x116482,a7),f24(x116481,x116482,a18))), % 59.08/59.03 inference(scs_inference,[],[68,70,74,76,77,79,80,97,112,113,1229,1232,655,981,72,98,609,960,1016,188,11597,11601,1228,251,599,89,90,116,99,11583,11586,118,119,121,132,149,150,146,147,117,148,2,134,141,140,136,133,127,128,124,125,135,131,130,60,138,48,49,137,38,123,143,144,292,4,9,10,13,22,23,26,320,5,6,7,8,11,12,14,15,16,17,18,19,20,21,24,25,345,388,408,434,27,28,29])). % 59.08/59.03 cnf(11652,plain, % 59.08/59.03 (P10(f20(f22(a7,a3)),a7,a3,f22(a18,a3))), % 59.08/59.03 inference(scs_inference,[],[68,70,74,76,77,79,80,97,112,113,1229,1232,655,981,72,98,609,960,1016,188,11597,11601,1228,251,599,89,90,116,99,11583,11586,118,119,121,132,149,150,146,147,117,148,2,134,141,140,136,133,127,128,124,125,135,131,130,60,138,48,49,137,38,123,143,144,292,4,9,10,13,22,23,26,320,5,6,7,8,11,12,14,15,16,17,18,19,20,21,24,25,345,388,408,434,27,28,29,616,617,219,221])). % 59.08/59.03 cnf(11654,plain, % 59.08/59.03 (P6(f17(f27(a1),f25(a1)),f27(a1))), % 59.08/59.03 inference(scs_inference,[],[68,70,74,76,77,79,80,97,112,113,1229,1232,655,981,72,98,609,960,1016,188,11597,11601,1228,251,599,89,90,116,99,11583,11586,118,119,121,132,149,150,146,147,117,148,2,134,141,140,136,133,127,128,124,125,135,131,130,60,138,48,49,137,38,123,143,144,292,4,9,10,13,22,23,26,320,5,6,7,8,11,12,14,15,16,17,18,19,20,21,24,25,345,388,408,434,27,28,29,616,617,219,221,344,129])). % 59.08/59.03 cnf(11656,plain, % 59.08/59.03 (~P17(f27(a12))), % 59.08/59.03 inference(scs_inference,[],[68,70,74,76,77,79,80,97,112,113,1229,1232,655,981,72,98,609,960,1016,188,11597,11601,1228,251,599,89,90,116,99,11583,11586,118,119,121,132,149,150,146,147,117,148,2,134,141,140,136,133,127,128,124,125,135,131,130,60,138,48,49,137,38,123,143,144,292,4,9,10,13,22,23,26,320,5,6,7,8,11,12,14,15,16,17,18,19,20,21,24,25,345,388,408,434,27,28,29,616,617,219,221,344,129,142])). % 59.08/59.03 cnf(11660,plain, % 59.08/59.03 (P8(f22(a18,a3),a7,a3)), % 59.08/59.03 inference(scs_inference,[],[68,70,74,76,77,79,80,97,112,113,1229,1232,655,981,72,98,609,960,1016,188,11597,11601,1228,251,599,89,90,116,99,11583,11586,971,108,118,119,121,132,149,150,146,147,117,148,2,134,141,140,136,133,127,128,124,125,135,131,130,60,138,48,49,137,38,123,143,144,292,4,9,10,13,22,23,26,320,5,6,7,8,11,12,14,15,16,17,18,19,20,21,24,25,345,388,408,434,27,28,29,616,617,219,221,344,129,142,326,45])). % 59.08/59.03 cnf(11661,plain, % 59.08/59.03 (P8(f22(x116611,x116612),x116611,x116612)), % 59.08/59.03 inference(rename_variables,[],[108])). % 59.08/59.03 cnf(11662,plain, % 59.08/59.03 (P7(f21(a7,a1),a18,f26(f31(a1),f30(a1)))), % 59.08/59.03 inference(scs_inference,[],[68,70,74,76,77,79,80,97,112,113,1229,1232,655,981,72,98,609,960,1016,188,11597,11601,1228,251,599,89,90,116,99,11583,11586,971,108,118,119,121,132,149,150,146,147,117,148,2,134,141,140,136,133,127,128,124,125,135,131,130,60,138,48,49,137,38,123,143,144,292,4,9,10,13,22,23,26,320,5,6,7,8,11,12,14,15,16,17,18,19,20,21,24,25,345,388,408,434,27,28,29,616,617,219,221,344,129,142,326,45,43])). % 59.08/59.03 cnf(11666,plain, % 59.08/59.03 (P13(f5(x116661,x116662),x116661,x116662)), % 59.08/59.03 inference(rename_variables,[],[107])). % 59.08/59.03 cnf(11671,plain, % 59.08/59.03 (P7(f10(a1,a7),f26(f31(a1),f30(a1)),a18)), % 59.08/59.03 inference(scs_inference,[],[68,70,74,76,77,79,80,97,112,113,1229,1232,257,655,981,72,98,609,960,1016,968,188,11597,11601,1228,251,599,89,90,116,107,11666,99,11583,11586,971,108,118,119,121,132,149,150,146,147,117,148,2,134,141,140,136,133,127,128,124,125,135,131,130,60,138,48,49,137,38,123,143,144,292,4,9,10,13,22,23,26,320,5,6,7,8,11,12,14,15,16,17,18,19,20,21,24,25,345,388,408,434,27,28,29,616,617,219,221,344,129,142,326,45,43,3,41,59,39,44])). % 59.08/59.03 cnf(11680,plain, % 59.08/59.03 (P7(f5(a18,f31(a1)),a7,f31(a1))), % 59.08/59.03 inference(scs_inference,[],[68,70,74,76,77,79,80,97,112,113,1229,1232,257,655,981,72,98,609,604,960,1016,970,968,969,188,11597,11601,1228,251,599,89,90,116,105,107,11666,99,11583,11586,971,108,118,119,121,132,149,150,146,147,117,148,2,134,141,140,136,133,127,128,124,125,135,131,130,60,138,48,49,137,38,123,143,144,292,4,9,10,13,22,23,26,320,5,6,7,8,11,12,14,15,16,17,18,19,20,21,24,25,345,388,408,434,27,28,29,616,617,219,221,344,129,142,326,45,43,3,41,59,39,44,64,52,54,53,42])). % 59.08/59.03 cnf(11687,plain, % 59.08/59.03 (P10(f24(x116871,a11,f22(x116871,a11)),x116871,a11,f22(x116871,a11))), % 59.08/59.03 inference(scs_inference,[],[68,70,74,76,77,79,80,97,112,113,1229,1232,257,655,981,72,98,609,604,960,1016,1010,970,968,1014,969,188,11597,11601,1228,251,599,89,90,115,116,105,107,11666,99,11583,11586,971,108,11661,961,118,119,121,132,149,150,146,147,117,148,2,134,141,140,136,133,127,128,124,125,135,131,130,60,138,48,49,137,38,123,143,144,292,4,9,10,13,22,23,26,320,5,6,7,8,11,12,14,15,16,17,18,19,20,21,24,25,345,388,408,434,27,28,29,616,617,219,221,344,129,142,326,45,43,3,41,59,39,44,64,52,54,53,42,163,153,162])). % 59.08/59.03 cnf(11695,plain, % 59.08/59.03 (E(f22(a7,x116951),f22(a18,x116951))), % 59.08/59.03 inference(rename_variables,[],[11636])). % 59.08/59.03 cnf(11696,plain, % 59.08/59.03 (P12(f30(a6))), % 59.08/59.03 inference(scs_inference,[],[78,11626,11636,319,405,121])). % 59.08/59.03 cnf(11702,plain, % 59.08/59.03 (P6(f20(f28(a8)),f28(x117021))), % 59.08/59.03 inference(scs_inference,[],[78,11626,11636,11596,332,109,319,405,121,118,150,132])). % 59.08/59.03 cnf(11708,plain, % 59.08/59.03 (P13(f30(a6),f29(f31(a6),f31(a6)),f31(a6))), % 59.08/59.03 inference(scs_inference,[],[78,11626,11636,11680,11596,332,109,319,405,121,118,150,132,149,119,146])). % 59.08/59.03 cnf(11712,plain, % 59.08/59.03 (E(f20(f28(a18)),a18)), % 59.08/59.03 inference(scs_inference,[],[78,11626,11636,11565,11680,11596,332,109,319,405,121,118,150,132,149,119,146,148,117])). % 59.08/59.03 cnf(11714,plain, % 59.08/59.03 (P9(f30(a6),f29(f31(a6),f31(a6)),f31(a6))), % 59.08/59.03 inference(scs_inference,[],[78,11626,11636,11565,11680,11596,332,109,319,405,121,118,150,132,149,119,146,148,117,147])). % 59.08/59.03 cnf(11719,plain, % 59.08/59.03 (P3(f27(a12))), % 59.08/59.03 inference(scs_inference,[],[78,11646,11626,11636,11613,11565,11680,11596,11606,332,109,319,405,121,118,150,132,149,119,146,148,117,147,320,2,616,141])). % 59.08/59.03 cnf(11726,plain, % 59.08/59.03 (P6(f20(x117261),x117261)), % 59.08/59.03 inference(rename_variables,[],[99])). % 59.08/59.03 cnf(11729,plain, % 59.08/59.03 (P6(f20(x117291),x117291)), % 59.08/59.03 inference(rename_variables,[],[99])). % 59.08/59.03 cnf(11739,plain, % 59.08/59.03 (~E(f27(a12),a7)), % 59.08/59.03 inference(scs_inference,[],[69,78,111,11574,11646,11626,11636,11613,11615,11660,11565,11680,11596,11606,235,332,109,99,11726,114,319,405,121,118,150,132,149,119,146,148,117,147,320,2,616,141,142,135,128,127,124,162,125,131,45])). % 59.08/59.03 cnf(11741,plain, % 59.08/59.03 (P17(f20(f28(a7)))), % 59.08/59.03 inference(scs_inference,[],[69,78,111,11574,11646,11626,11636,11613,11615,11660,11565,11680,11596,11606,235,332,239,109,99,11726,11729,114,319,405,121,118,150,132,149,119,146,148,117,147,320,2,616,141,142,135,128,127,124,162,125,131,45,130])). % 59.08/59.03 cnf(11742,plain, % 59.08/59.03 (P6(f20(x117421),x117421)), % 59.08/59.03 inference(rename_variables,[],[99])). % 59.08/59.03 cnf(11743,plain, % 59.08/59.03 (~P11(x117431,f20(f28(a7)))), % 59.08/59.03 inference(rename_variables,[],[239])). % 59.08/59.03 cnf(11745,plain, % 59.08/59.03 (~P6(f27(a1),f28(a8))), % 59.08/59.03 inference(scs_inference,[],[69,78,111,11574,11646,11626,11636,11613,11615,11660,11578,11565,11680,11596,11606,235,332,239,109,92,99,11726,11729,114,319,405,121,118,150,132,149,119,146,148,117,147,320,2,616,141,142,135,128,127,124,162,125,131,45,130,138])). % 59.08/59.03 cnf(11747,plain, % 59.08/59.03 (P11(f20(f22(a7,x117471)),f22(a18,x117471))), % 59.08/59.03 inference(scs_inference,[],[69,78,111,11574,11646,11626,11636,11695,11613,11615,11660,11578,11565,11680,11596,11606,235,332,239,244,109,92,99,11726,11729,114,319,405,121,118,150,132,149,119,146,148,117,147,320,2,616,141,142,135,128,127,124,162,125,131,45,130,138,60])). % 59.08/59.03 cnf(11748,plain, % 59.08/59.03 (E(f22(a7,x117481),f22(a18,x117481))), % 59.08/59.03 inference(rename_variables,[],[11636])). % 59.08/59.03 cnf(11750,plain, % 59.08/59.03 (~P11(f31(a1),f28(a18))), % 59.08/59.03 inference(scs_inference,[],[69,78,111,11557,11574,11646,11626,11636,11695,11602,11613,11615,11660,11578,11565,11680,11596,11606,235,332,239,244,109,92,99,11726,11729,114,319,405,121,118,150,132,149,119,146,148,117,147,320,2,616,141,142,135,128,127,124,162,125,131,45,130,138,60,139])). % 59.08/59.03 cnf(11751,plain, % 59.08/59.03 (P6(x117511,f28(x117511))), % 59.08/59.03 inference(rename_variables,[],[11557])). % 59.08/59.03 cnf(11754,plain, % 59.08/59.03 (P6(f20(x117541),x117541)), % 59.08/59.03 inference(rename_variables,[],[99])). % 59.08/59.03 cnf(11755,plain, % 59.08/59.03 (~P11(f22(a7,x117551),f20(f22(a18,x117551)))), % 59.08/59.03 inference(scs_inference,[],[69,78,111,11567,11557,11574,11646,11626,11636,11695,11748,11602,11613,11615,11660,11578,11565,11680,11596,11606,235,257,332,239,244,109,92,99,11726,11729,11742,114,319,405,121,118,150,132,149,119,146,148,117,147,320,2,616,141,142,135,128,127,124,162,125,131,45,130,138,60,139,49,59])). % 59.08/59.03 cnf(11758,plain, % 59.08/59.03 (~P5(f27(a1),f20(f28(a7)))), % 59.08/59.03 inference(scs_inference,[],[69,78,111,11567,11557,11574,11646,11626,11636,11695,11748,11602,11613,11615,11660,11578,11565,11680,11596,11606,235,257,332,239,11743,244,109,92,99,11726,11729,11742,114,319,405,121,118,150,132,149,119,146,148,117,147,320,2,616,141,142,135,128,127,124,162,125,131,45,130,138,60,139,49,59,137])). % 59.08/59.03 cnf(11761,plain, % 59.08/59.03 (P6(f24(a18,x117611,x117612),f28(f24(a7,x117611,x117612)))), % 59.08/59.03 inference(scs_inference,[],[69,78,111,11567,11557,11751,11574,11646,11626,11636,11695,11748,11602,11613,11615,11660,11578,11565,11680,11596,11606,235,257,332,239,11743,244,109,92,99,11726,11729,11742,114,319,405,121,118,150,132,149,119,146,148,117,147,320,2,616,141,142,135,128,127,124,162,125,131,45,130,138,60,139,49,59,137,48])). % 59.08/59.03 cnf(11766,plain, % 59.08/59.03 (P2(f26(f31(a14),f30(a14)))), % 59.08/59.03 inference(scs_inference,[],[69,78,111,11567,11557,11751,11574,11646,11626,11636,11695,11748,11555,11588,11602,11613,11615,11660,11578,11565,11563,11680,11596,11606,235,257,332,239,11743,244,109,92,99,11726,11729,11742,114,319,405,121,118,150,132,149,119,146,148,117,147,320,2,616,141,142,135,128,127,124,162,125,131,45,130,138,60,139,49,59,137,48,38,155,156])). % 59.08/59.03 cnf(11776,plain, % 59.08/59.03 (P10(f24(x117761,a11,f22(x117761,a11)),x117761,a11,f22(x117761,a11))), % 59.08/59.03 inference(rename_variables,[],[11687])). % 59.08/59.03 cnf(11777,plain, % 59.08/59.03 (P8(f22(x117771,x117772),x117771,x117772)), % 59.08/59.03 inference(rename_variables,[],[108])). % 59.08/59.03 cnf(11788,plain, % 59.08/59.03 (P8(f27(a1),f31(a1),f31(a1))), % 59.08/59.03 inference(scs_inference,[],[67,69,78,111,11567,11557,11751,11574,11646,11626,11636,11695,11748,11555,11588,11602,11613,11615,11660,11652,11578,11687,11776,11565,11563,11680,11596,11606,235,257,332,73,239,11743,110,71,244,109,92,75,115,105,107,99,11726,11729,11742,11754,114,102,108,11777,319,405,121,118,150,132,149,119,146,148,117,147,320,2,616,141,142,135,128,127,124,162,125,131,45,130,138,60,139,49,59,137,48,38,155,156,161,163,164,165,166,153,143])). % 59.08/59.03 cnf(11790,plain, % 59.08/59.03 (P8(f25(a1),f31(a1),f31(a1))), % 59.08/59.03 inference(scs_inference,[],[67,69,78,111,11567,11557,11751,11574,11646,11626,11636,11695,11748,11555,11588,11602,11613,11615,11660,11652,11578,11687,11776,11565,11563,11680,11596,11606,235,257,332,73,239,11743,110,71,244,109,92,75,115,105,107,99,11726,11729,11742,11754,114,102,108,11777,319,405,121,118,150,132,149,119,146,148,117,147,320,2,616,141,142,135,128,127,124,162,125,131,45,130,138,60,139,49,59,137,48,38,155,156,161,163,164,165,166,153,143,144])). % 59.08/59.03 cnf(11794,plain, % 59.08/59.03 (~P11(f22(a18,x117941),f20(f22(a7,x117941)))), % 59.08/59.03 inference(scs_inference,[],[67,69,78,111,11567,11557,11751,11574,11646,11626,11636,11695,11748,11555,11588,11602,11613,11615,11660,11652,11578,11687,11776,11565,11563,11680,11596,11606,235,257,332,73,239,11743,110,71,244,109,92,75,115,105,107,99,11726,11729,11742,11754,114,102,108,11777,319,405,121,118,150,132,149,119,146,148,117,147,320,2,616,141,142,135,128,127,124,162,125,131,45,130,138,60,139,49,59,137,48,38,155,156,161,163,164,165,166,153,143,144,129,133])). % 59.08/59.03 cnf(11799,plain, % 59.08/59.03 (P5(f24(a18,x117991,x117992),f24(a7,x117991,x117992))), % 59.08/59.03 inference(scs_inference,[],[67,69,78,111,11567,11557,11751,11574,11646,11626,11628,11636,11695,11748,11555,11588,11602,11613,11615,11660,11652,11578,11687,11776,11565,11563,11680,11596,11606,235,257,332,73,98,239,11743,110,71,244,109,92,75,115,105,107,99,11726,11729,11742,11754,114,102,108,11777,319,405,121,118,150,132,149,119,146,148,117,147,320,2,616,141,142,135,128,127,124,162,125,131,45,130,138,60,139,49,59,137,48,38,155,156,161,163,164,165,166,153,143,144,129,133,9283,32,61])). % 59.08/59.03 cnf(11802,plain, % 59.08/59.03 (~E(a18,f31(a15))), % 59.08/59.03 inference(scs_inference,[],[67,69,78,111,11567,11557,11751,11574,11646,11626,11628,11636,11695,11748,11555,11588,11602,11613,11615,11660,11652,11578,11687,11776,11565,11563,11680,11596,11606,235,257,332,73,98,239,11743,110,71,244,109,92,75,115,105,107,99,11726,11729,11742,11754,114,102,108,11777,319,405,121,118,150,132,149,119,146,148,117,147,320,2,616,141,142,135,128,127,124,162,125,131,45,130,138,60,139,49,59,137,48,38,155,156,161,163,164,165,166,153,143,144,129,133,9283,32,61,51,3])). % 59.08/59.03 cnf(11831,plain, % 59.08/59.03 (~E(a7,f27(a12))), % 59.08/59.03 inference(scs_inference,[],[11739,11714,11766,11741,11662,11618,77,300,121,118,132,148,117,149,119,146,320,147,2])). % 59.08/59.03 cnf(11847,plain, % 59.08/59.03 (~P8(f20(f28(a18)),x118471,x118472)), % 59.08/59.03 inference(scs_inference,[],[11788,11790,11739,11654,11714,11766,11741,11758,11662,11712,11618,77,300,175,70,79,98,598,121,118,132,148,117,149,119,146,320,147,2,141,616,142,128,62,127,131,162,45])). % 59.08/59.03 cnf(11850,plain, % 59.08/59.03 (E(f24(x118501,a7,a7),f24(x118501,a18,a18))), % 59.08/59.03 inference(scs_inference,[],[11788,11790,11739,11576,11654,11714,11766,11741,11758,11662,11712,11618,11647,11648,77,300,175,70,79,98,598,121,118,132,148,117,149,119,146,320,147,2,141,616,142,128,62,127,131,162,45,130,3])). % 59.08/59.03 cnf(11865,plain, % 59.08/59.03 (P2(f26(f31(a6),f30(a6)))), % 59.08/59.03 inference(scs_inference,[],[11590,11696,11745,11750,11788,11790,11739,11576,11654,11702,11747,11714,11708,11766,11755,11741,11758,11662,11712,11618,11623,11647,11648,11637,77,11557,11602,300,175,70,79,98,188,598,121,118,132,148,117,149,119,146,320,147,2,141,616,142,128,62,127,131,162,45,130,3,60,137,59,49,48,38,156])). % 59.08/59.03 cnf(11871,plain, % 59.08/59.03 (~P10(f17(f27(a1),f25(a1)),f31(a1),f31(a1),f25(a1))), % 59.08/59.03 inference(scs_inference,[],[11590,11696,11745,11750,11788,11790,11739,11576,11654,11702,11747,11714,11708,11766,11755,11741,11758,11662,11712,11618,11623,11647,11648,11637,77,11557,11602,300,175,70,79,98,188,598,121,118,132,148,117,149,119,146,320,147,2,141,616,142,128,62,127,131,162,45,130,3,60,137,59,49,48,38,156,155,163,164])). % 59.08/59.03 cnf(11875,plain, % 59.08/59.03 (P9(f24(f31(a1),f31(a1),f27(a1)),f31(a1),f31(a1))), % 59.08/59.03 inference(scs_inference,[],[11590,11696,11745,11750,11788,11790,11739,11576,11654,11702,11747,11714,11708,11766,11755,11741,11758,11662,11712,11618,11623,11647,11648,11637,77,11557,11602,300,175,70,79,98,188,598,121,118,132,148,117,149,119,146,320,147,2,141,616,142,128,62,127,131,162,45,130,3,60,137,59,49,48,38,156,155,163,164,165,166])). % 59.08/59.03 cnf(11882,plain, % 59.08/59.03 (P10(f24(f31(a1),f31(a1),f27(a1)),f31(a1),f31(a1),f25(a1))), % 59.08/59.03 inference(scs_inference,[],[67,11590,11696,11745,11750,11788,11790,11739,11576,11654,11702,11747,11714,11708,11766,11755,11741,11758,11662,11712,11618,11623,11647,11648,11637,77,11557,11602,300,175,70,79,98,73,188,110,71,75,105,107,102,598,121,118,132,148,117,149,119,146,320,147,2,141,616,142,128,62,127,131,162,45,130,3,60,137,59,49,48,38,156,155,163,164,165,166,151,167])). % 59.08/59.03 cnf(11888,plain, % 59.08/59.03 (P10(f17(f27(a1),f25(a1)),f31(a1),f31(a1),f27(a1))), % 59.08/59.03 inference(scs_inference,[],[67,11590,11696,11745,11750,11788,11790,11739,11576,11654,11702,11747,11714,11708,11766,11755,11741,11758,11662,11712,11618,11623,11647,11648,11627,11637,77,11557,11602,300,175,70,79,98,73,188,110,71,90,75,105,107,102,598,121,118,132,148,117,149,119,146,320,147,2,141,616,142,128,62,127,131,162,45,130,3,60,137,59,49,48,38,156,155,163,164,165,166,151,167,9345,138,161])). % 59.08/59.03 cnf(11915,plain, % 59.08/59.03 (P6(f20(x119151),x119151)), % 59.08/59.03 inference(rename_variables,[],[99])). % 59.08/59.03 cnf(11918,plain, % 59.08/59.03 (P6(f20(x119181),x119181)), % 59.08/59.03 inference(rename_variables,[],[99])). % 59.08/59.03 cnf(11923,plain, % 59.08/59.03 (E(f24(x119231,a7,a7),f24(x119231,a18,a18))), % 59.08/59.03 inference(rename_variables,[],[11850])). % 59.08/59.03 cnf(11932,plain, % 59.08/59.03 (E(f22(x119321,a7),f22(x119321,a18))), % 59.08/59.03 inference(rename_variables,[],[11637])). % 59.08/59.03 cnf(11945,plain, % 59.08/59.03 ($false), % 59.08/59.03 inference(scs_inference,[],[67,11799,11850,11923,11802,11656,11719,11831,11875,11888,11871,11882,11865,11847,11761,11794,11671,11615,11637,11932,395,11790,11747,79,11596,11567,73,239,110,71,92,75,99,11915,11918,598,121,132,148,149,117,147,119,2,146,320,141,616,128,127,162,62,45,3,137,60,59,49,48,38,164,167]), % 59.08/59.03 ['proof']). % 59.08/59.03 % SZS output end Proof % 59.08/59.03 % Total time :58.330000s %------------------------------------------------------------------------------