%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SEU439+1 : TPTP v8.2.0. Released v3.4.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n022.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 15:03:12 EDT 2024 % Result : Theorem 59.27s 59.33s % Output : CNFRefutation 59.27s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.13 % Problem : SEU439+1 : TPTP v8.2.0. Released v3.4.0. % 0.08/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.13/0.35 % Computer : n022.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 300 % 0.13/0.35 % DateTime : Fri Jun 21 15:36:39 EDT 2024 % 0.13/0.35 % CPUTime : % 0.44/0.61 start to proof:theBenchmark % 59.27/59.31 %------------------------------------------- % 59.27/59.31 % File :CSE---1.7 % 59.27/59.31 % Problem :theBenchmark % 59.27/59.31 % Transform :cnf % 59.27/59.31 % Format :tptp:raw % 59.27/59.31 % Command :java -jar mcs_scs.jar %d %s % 59.27/59.31 % 59.27/59.31 % Result :Theorem 58.630000s % 59.27/59.31 % Output :CNFRefutation 58.630000s % 59.27/59.31 %------------------------------------------- % 59.27/59.32 %------------------------------------------------------------------------------ % 59.27/59.32 % File : SEU439+1 : TPTP v8.2.0. Released v3.4.0. % 59.27/59.32 % Domain : Set Theory % 59.27/59.32 % Problem : First and Second Order Cutting of Binary Relations T43 % 59.27/59.32 % Version : [Urb08] axioms : Especial. % 59.27/59.32 % English : % 59.27/59.32 % 59.27/59.32 % Refs : [Ret05] Retel (2005), Properties of First and Second Order Cut % 59.27/59.32 % : [Urb07] Urban (2007), MPTP 0.2: Design, Implementation, and In % 59.27/59.32 % : [Urb08] Urban (2006), Email to G. Sutcliffe % 59.27/59.32 % Source : [Urb08] % 59.27/59.32 % Names : t43_relset_2 [Urb08] % 59.27/59.32 % 59.27/59.32 % Status : Theorem % 59.27/59.32 % Rating : 0.72 v8.2.0, 0.78 v8.1.0, 0.72 v7.5.0, 0.69 v7.4.0, 0.70 v7.3.0, 0.69 v7.2.0, 0.66 v7.1.0, 0.78 v7.0.0, 0.70 v6.4.0, 0.73 v6.3.0, 0.79 v6.2.0, 0.76 v6.1.0, 0.87 v6.0.0, 0.78 v5.4.0, 0.79 v5.3.0, 0.81 v5.2.0, 0.75 v5.1.0, 0.76 v5.0.0, 0.83 v4.1.0, 0.87 v4.0.1, 0.83 v3.7.0, 0.85 v3.5.0, 0.89 v3.4.0 % 59.27/59.32 % Syntax : Number of formulae : 60 ( 22 unt; 0 def) % 59.27/59.32 % Number of atoms : 122 ( 11 equ) % 59.27/59.32 % Maximal formula atoms : 5 ( 2 avg) % 59.27/59.32 % Number of connectives : 78 ( 16 ~; 1 |; 23 &) % 59.27/59.32 % ( 7 <=>; 31 =>; 0 <=; 0 <~>) % 59.27/59.32 % Maximal formula depth : 11 ( 4 avg) % 59.27/59.32 % Maximal term depth : 4 ( 1 avg) % 59.27/59.32 % Number of predicates : 13 ( 11 usr; 1 prp; 0-3 aty) % 59.27/59.32 % Number of functors : 14 ( 14 usr; 1 con; 0-4 aty) % 59.27/59.32 % Number of variables : 119 ( 108 !; 11 ?) % 59.27/59.32 % SPC : FOF_THM_RFO_SEQ % 59.27/59.32 % 59.27/59.32 % Comments : Normal version: includes the axioms (which may be theorems from % 59.27/59.32 % other articles) and background that are possibly necessary. % 59.27/59.32 % : Translated by MPTP from the Mizar Mathematical Library 4.48.930. % 59.27/59.32 % : The problem encoding is based on set theory. % 59.27/59.32 %------------------------------------------------------------------------------ % 59.27/59.32 fof(t43_relset_2,conjecture, % 59.27/59.32 ! [A,B,C] : % 59.27/59.32 ( m1_subset_1(C,k1_zfmisc_1(A)) % 59.27/59.32 => ! [D] : % 59.27/59.32 ( m1_subset_1(D,k1_zfmisc_1(k2_zfmisc_1(A,B))) % 59.27/59.32 => ( C != k1_xboole_0 % 59.27/59.32 => r1_tarski(k8_relset_2(A,B,C,D),k9_relat_1(D,C)) ) ) ) ). % 59.27/59.32 % 59.27/59.32 fof(antisymmetry_r2_hidden,axiom, % 59.27/59.32 ! [A,B] : % 59.27/59.32 ( r2_hidden(A,B) % 59.27/59.32 => ~ r2_hidden(B,A) ) ). % 59.27/59.32 % 59.27/59.32 fof(cc1_relat_1,axiom, % 59.27/59.32 ! [A] : % 59.27/59.32 ( v1_xboole_0(A) % 59.27/59.32 => v1_relat_1(A) ) ). % 59.27/59.32 % 59.27/59.32 fof(cc1_relset_1,axiom, % 59.27/59.32 ! [A,B,C] : % 59.27/59.32 ( m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))) % 59.27/59.32 => v1_relat_1(C) ) ). % 59.27/59.32 % 59.27/59.32 fof(commutativity_k2_tarski,axiom, % 59.27/59.32 ! [A,B] : k2_tarski(A,B) = k2_tarski(B,A) ). % 59.27/59.32 % 59.27/59.32 fof(d13_relat_1,axiom, % 59.27/59.32 ! [A] : % 59.27/59.32 ( v1_relat_1(A) % 59.27/59.32 => ! [B,C] : % 59.27/59.32 ( C = k9_relat_1(A,B) % 59.27/59.32 <=> ! [D] : % 59.27/59.32 ( r2_hidden(D,C) % 59.27/59.32 <=> ? [E] : % 59.27/59.32 ( r2_hidden(k4_tarski(E,D),A) % 59.27/59.32 & r2_hidden(E,B) ) ) ) ) ). % 59.27/59.32 % 59.27/59.32 fof(d1_xboole_0,axiom, % 59.27/59.32 ! [A] : % 59.27/59.32 ( A = k1_xboole_0 % 59.27/59.32 <=> ! [B] : ~ r2_hidden(B,A) ) ). % 59.27/59.32 % 59.27/59.32 fof(d3_tarski,axiom, % 59.27/59.32 ! [A,B] : % 59.27/59.32 ( r1_tarski(A,B) % 59.27/59.32 <=> ! [C] : % 59.27/59.32 ( r2_hidden(C,A) % 59.27/59.32 => r2_hidden(C,B) ) ) ). % 59.27/59.32 % 59.27/59.32 fof(d4_relset_2,axiom, % 59.27/59.32 ! [A,B,C] : % 59.27/59.32 ( m1_subset_1(C,k1_zfmisc_1(A)) % 59.27/59.32 => ! [D] : % 59.27/59.32 ( m1_subset_1(D,k1_zfmisc_1(k2_zfmisc_1(A,B))) % 59.27/59.32 => k7_relset_2(A,B,C,D) = k8_setfam_1(B,k4_relset_2(k1_zfmisc_1(A),B,k6_relset_2(B,A,D),k3_pua2mss1(C))) ) ) ). % 59.27/59.32 % 59.27/59.32 fof(d5_tarski,axiom, % 59.27/59.32 ! [A,B] : k4_tarski(A,B) = k2_tarski(k2_tarski(A,B),k1_tarski(A)) ). % 59.27/59.32 % 59.27/59.32 fof(dt_k1_tarski,axiom, % 59.27/59.32 $true ). % 59.27/59.32 % 59.27/59.32 fof(dt_k1_xboole_0,axiom, % 59.27/59.32 $true ). % 59.27/59.32 % 59.27/59.32 fof(dt_k1_zfmisc_1,axiom, % 59.27/59.32 $true ). % 59.27/59.32 % 59.27/59.32 fof(dt_k2_tarski,axiom, % 59.27/59.32 $true ). % 59.27/59.32 % 59.27/59.32 fof(dt_k2_zfmisc_1,axiom, % 59.27/59.32 $true ). % 59.27/59.32 % 59.27/59.32 fof(dt_k3_pua2mss1,axiom, % 59.27/59.32 ! [A] : m1_eqrel_1(k3_pua2mss1(A),A) ). % 59.27/59.32 % 59.27/59.32 fof(dt_k4_relset_2,axiom, % 59.27/59.32 ! [A,B,C,D] : % 59.27/59.32 ( m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,k1_zfmisc_1(B)))) % 59.27/59.32 => m1_subset_1(k4_relset_2(A,B,C,D),k1_zfmisc_1(k1_zfmisc_1(B))) ) ). % 59.27/59.32 % 59.27/59.32 fof(dt_k4_tarski,axiom, % 59.27/59.32 $true ). % 59.27/59.32 % 59.27/59.32 fof(dt_k5_relset_2,axiom, % 59.27/59.32 ! [A,B] : % 59.27/59.32 ( v1_relat_1(B) % 59.27/59.33 => ( v1_relat_1(k5_relset_2(A,B)) % 59.27/59.33 & v1_funct_1(k5_relset_2(A,B)) ) ) ). % 59.27/59.33 % 59.27/59.33 fof(dt_k6_relset_2,axiom, % 59.27/59.33 ! [A,B,C] : % 59.27/59.33 ( m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(B,A))) % 59.27/59.33 => ( v1_funct_1(k6_relset_2(A,B,C)) % 59.27/59.33 & v1_funct_2(k6_relset_2(A,B,C),k1_zfmisc_1(B),k1_zfmisc_1(A)) % 59.27/59.33 & m2_relset_1(k6_relset_2(A,B,C),k1_zfmisc_1(B),k1_zfmisc_1(A)) ) ) ). % 59.27/59.33 % 59.27/59.33 fof(dt_k7_relset_2,axiom, % 59.27/59.33 $true ). % 59.27/59.33 % 59.27/59.33 fof(dt_k8_relset_2,axiom, % 59.27/59.33 ! [A,B,C,D] : % 59.27/59.33 ( ( m1_subset_1(C,k1_zfmisc_1(A)) % 59.27/59.33 & m1_subset_1(D,k1_zfmisc_1(k2_zfmisc_1(A,B))) ) % 59.27/59.33 => m1_subset_1(k8_relset_2(A,B,C,D),k1_zfmisc_1(B)) ) ). % 59.27/59.33 % 59.27/59.33 fof(dt_k8_setfam_1,axiom, % 59.27/59.33 ! [A,B] : % 59.27/59.33 ( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A))) % 59.27/59.33 => m1_subset_1(k8_setfam_1(A,B),k1_zfmisc_1(A)) ) ). % 59.27/59.33 % 59.27/59.33 fof(dt_k9_relat_1,axiom, % 59.27/59.33 $true ). % 59.27/59.33 % 59.27/59.33 fof(dt_m1_eqrel_1,axiom, % 59.27/59.33 ! [A,B] : % 59.27/59.33 ( m1_eqrel_1(B,A) % 59.27/59.33 => m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A))) ) ). % 59.27/59.33 % 59.27/59.33 fof(dt_m1_relset_1,axiom, % 59.27/59.33 $true ). % 59.27/59.33 % 59.27/59.33 fof(dt_m1_subset_1,axiom, % 59.27/59.33 $true ). % 59.27/59.33 % 59.27/59.33 fof(dt_m2_relset_1,axiom, % 59.27/59.33 ! [A,B,C] : % 59.27/59.33 ( m2_relset_1(C,A,B) % 59.27/59.33 => m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))) ) ). % 59.27/59.33 % 59.27/59.33 fof(existence_m1_eqrel_1,axiom, % 59.27/59.33 ! [A] : % 59.27/59.33 ? [B] : m1_eqrel_1(B,A) ). % 59.27/59.33 % 59.27/59.33 fof(existence_m1_relset_1,axiom, % 59.27/59.33 ! [A,B] : % 59.27/59.33 ? [C] : m1_relset_1(C,A,B) ). % 59.27/59.33 % 59.27/59.33 fof(existence_m1_subset_1,axiom, % 59.27/59.33 ! [A] : % 59.27/59.33 ? [B] : m1_subset_1(B,A) ). % 59.27/59.33 % 59.27/59.33 fof(existence_m2_relset_1,axiom, % 59.27/59.33 ! [A,B] : % 59.27/59.33 ? [C] : m2_relset_1(C,A,B) ). % 59.27/59.33 % 59.27/59.33 fof(fc12_relat_1,axiom, % 59.27/59.33 ( v1_xboole_0(k1_xboole_0) % 59.27/59.33 & v1_relat_1(k1_xboole_0) % 59.27/59.33 & v3_relat_1(k1_xboole_0) ) ). % 59.27/59.33 % 59.27/59.33 fof(fc1_subset_1,axiom, % 59.27/59.33 ! [A] : ~ v1_xboole_0(k1_zfmisc_1(A)) ). % 59.27/59.33 % 59.27/59.33 fof(fc1_sysrel,axiom, % 59.27/59.33 ! [A,B] : v1_relat_1(k2_zfmisc_1(A,B)) ). % 59.27/59.33 % 59.27/59.33 fof(fc2_subset_1,axiom, % 59.27/59.33 ! [A] : ~ v1_xboole_0(k1_tarski(A)) ). % 59.27/59.33 % 59.27/59.33 fof(fc3_subset_1,axiom, % 59.27/59.33 ! [A,B] : ~ v1_xboole_0(k2_tarski(A,B)) ). % 59.27/59.33 % 59.27/59.33 fof(fc4_relat_1,axiom, % 59.27/59.33 ( v1_xboole_0(k1_xboole_0) % 59.27/59.33 & v1_relat_1(k1_xboole_0) ) ). % 59.27/59.33 % 59.27/59.33 fof(fc4_subset_1,axiom, % 59.27/59.33 ! [A,B] : % 59.27/59.33 ( ( ~ v1_xboole_0(A) % 59.27/59.33 & ~ v1_xboole_0(B) ) % 59.27/59.33 => ~ v1_xboole_0(k2_zfmisc_1(A,B)) ) ). % 59.27/59.33 % 59.27/59.33 fof(rc1_relat_1,axiom, % 59.27/59.33 ? [A] : % 59.27/59.33 ( v1_xboole_0(A) % 59.27/59.33 & v1_relat_1(A) ) ). % 59.27/59.33 % 59.27/59.33 fof(rc1_subset_1,axiom, % 59.27/59.33 ! [A] : % 59.27/59.33 ( ~ v1_xboole_0(A) % 59.27/59.33 => ? [B] : % 59.27/59.33 ( m1_subset_1(B,k1_zfmisc_1(A)) % 59.27/59.33 & ~ v1_xboole_0(B) ) ) ). % 59.27/59.33 % 59.27/59.33 fof(rc2_partfun1,axiom, % 59.27/59.33 ! [A,B] : % 59.27/59.33 ? [C] : % 59.27/59.33 ( m1_relset_1(C,A,B) % 59.27/59.33 & v1_relat_1(C) % 59.27/59.33 & v1_funct_1(C) ) ). % 59.27/59.33 % 59.27/59.33 fof(rc2_relat_1,axiom, % 59.27/59.33 ? [A] : % 59.27/59.33 ( ~ v1_xboole_0(A) % 59.27/59.33 & v1_relat_1(A) ) ). % 59.27/59.33 % 59.27/59.33 fof(rc2_subset_1,axiom, % 59.27/59.33 ! [A] : % 59.27/59.33 ? [B] : % 59.27/59.33 ( m1_subset_1(B,k1_zfmisc_1(A)) % 59.27/59.33 & v1_xboole_0(B) ) ). % 59.27/59.33 % 59.27/59.33 fof(rc3_relat_1,axiom, % 59.27/59.33 ? [A] : % 59.27/59.33 ( v1_relat_1(A) % 59.27/59.33 & v3_relat_1(A) ) ). % 59.27/59.33 % 59.27/59.33 fof(redefinition_k4_relset_2,axiom, % 59.27/59.33 ! [A,B,C,D] : % 59.27/59.33 ( m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,k1_zfmisc_1(B)))) % 59.27/59.33 => k4_relset_2(A,B,C,D) = k9_relat_1(C,D) ) ). % 59.27/59.33 % 59.27/59.33 fof(redefinition_k6_relset_2,axiom, % 59.27/59.33 ! [A,B,C] : % 59.27/59.33 ( m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(B,A))) % 59.27/59.33 => k6_relset_2(A,B,C) = k5_relset_2(B,C) ) ). % 59.27/59.33 % 59.27/59.33 fof(redefinition_k8_relset_2,axiom, % 59.27/59.33 ! [A,B,C,D] : % 59.27/59.33 ( ( m1_subset_1(C,k1_zfmisc_1(A)) % 59.27/59.33 & m1_subset_1(D,k1_zfmisc_1(k2_zfmisc_1(A,B))) ) % 59.27/59.33 => k8_relset_2(A,B,C,D) = k7_relset_2(A,B,C,D) ) ). % 59.27/59.33 % 59.27/59.33 fof(redefinition_m2_relset_1,axiom, % 59.27/59.33 ! [A,B,C] : % 59.27/59.33 ( m2_relset_1(C,A,B) % 59.27/59.33 <=> m1_relset_1(C,A,B) ) ). % 59.27/59.33 % 59.27/59.33 fof(reflexivity_r1_tarski,axiom, % 59.27/59.33 ! [A,B] : r1_tarski(A,A) ). % 59.27/59.33 % 59.27/59.33 fof(t1_subset,axiom, % 59.27/59.33 ! [A,B] : % 59.27/59.33 ( r2_hidden(A,B) % 59.27/59.33 => m1_subset_1(A,B) ) ). % 59.27/59.33 % 59.27/59.33 fof(t24_relset_2,axiom, % 59.27/59.33 ! [A,B,C,D] : % 59.27/59.33 ( m1_subset_1(D,k1_zfmisc_1(A)) % 59.27/59.33 => ! [E] : % 59.27/59.33 ( m1_subset_1(E,k1_zfmisc_1(k2_zfmisc_1(A,B))) % 59.27/59.33 => ( r2_hidden(C,k8_relset_2(A,B,D,E)) % 59.27/59.33 => ! [F] : % 59.27/59.33 ( r2_hidden(F,D) % 59.27/59.33 => r2_hidden(C,k9_relat_1(E,k1_tarski(F))) ) ) ) ) ). % 59.27/59.33 % 59.27/59.33 fof(t2_subset,axiom, % 59.27/59.33 ! [A,B] : % 59.27/59.33 ( m1_subset_1(A,B) % 59.27/59.33 => ( v1_xboole_0(B) % 59.27/59.33 | r2_hidden(A,B) ) ) ). % 59.27/59.33 % 59.27/59.33 fof(t3_subset,axiom, % 59.27/59.33 ! [A,B] : % 59.27/59.33 ( m1_subset_1(A,k1_zfmisc_1(B)) % 59.27/59.33 <=> r1_tarski(A,B) ) ). % 59.27/59.33 % 59.27/59.33 fof(t4_subset,axiom, % 59.27/59.33 ! [A,B,C] : % 59.27/59.33 ( ( r2_hidden(A,B) % 59.27/59.33 & m1_subset_1(B,k1_zfmisc_1(C)) ) % 59.27/59.33 => m1_subset_1(A,C) ) ). % 59.27/59.33 % 59.27/59.33 fof(t5_subset,axiom, % 59.27/59.33 ! [A,B,C] : % 59.27/59.33 ~ ( r2_hidden(A,B) % 59.27/59.33 & m1_subset_1(B,k1_zfmisc_1(C)) % 59.27/59.33 & v1_xboole_0(C) ) ). % 59.27/59.33 % 59.27/59.33 fof(t6_boole,axiom, % 59.27/59.33 ! [A] : % 59.27/59.33 ( v1_xboole_0(A) % 59.27/59.33 => A = k1_xboole_0 ) ). % 59.27/59.33 % 59.27/59.33 fof(t7_boole,axiom, % 59.27/59.33 ! [A,B] : % 59.27/59.33 ~ ( r2_hidden(A,B) % 59.27/59.33 & v1_xboole_0(B) ) ). % 59.27/59.33 % 59.27/59.33 fof(t8_boole,axiom, % 59.27/59.33 ! [A,B] : % 59.27/59.33 ~ ( v1_xboole_0(A) % 59.27/59.33 & A != B % 59.27/59.33 & v1_xboole_0(B) ) ). % 59.27/59.33 % 59.27/59.33 fof(t9_relset_2,axiom, % 59.27/59.33 ! [A,B,C] : % 59.27/59.33 ( v1_relat_1(C) % 59.27/59.33 => ( r2_hidden(A,k9_relat_1(C,k1_tarski(B))) % 59.27/59.33 <=> r2_hidden(k4_tarski(B,A),C) ) ) ). % 59.27/59.33 % 59.27/59.33 %------------------------------------------------------------------------------ % 59.27/59.33 %------------------------------------------- % 59.27/59.33 % Proof found % 59.27/59.33 % SZS status Theorem for theBenchmark % 59.27/59.33 % SZS output start Proof % 59.27/59.33 %ClaNum:151(EqnAxiom:75) % 59.27/59.33 %VarNum:350(SingletonVarNum:147) % 59.27/59.33 %MaxLitNum:5 % 59.27/59.33 %MaxfuncDepth:3 % 59.27/59.33 %SharedTerms:26 % 59.27/59.33 %goalClause: 88 97 101 106 % 59.27/59.33 %singleGoalClaCount:4 % 59.27/59.33 [77]P1(a1) % 59.27/59.33 [78]P1(a2) % 59.27/59.33 [80]P2(a1) % 59.27/59.33 [81]P2(a2) % 59.27/59.33 [82]P2(a7) % 59.27/59.33 [83]P2(a10) % 59.27/59.33 [84]P11(a1) % 59.27/59.33 [85]P11(a10) % 59.27/59.33 [101]~E(a12,a1) % 59.27/59.33 [102]~P1(a7) % 59.27/59.33 [88]P4(a12,f22(a13)) % 59.27/59.33 [106]~P3(f26(a13,a14,a12,a15),f31(a15,a12)) % 59.27/59.33 [97]P4(a15,f22(f25(a13,a14))) % 59.27/59.33 [87]P3(x871,x871) % 59.27/59.33 [86]P1(f11(x861)) % 59.27/59.33 [89]P4(f3(x891),x891) % 59.27/59.33 [90]P5(f23(x901),x901) % 59.27/59.33 [91]P5(f4(x911),x911) % 59.27/59.33 [92]P4(f11(x921),f22(x921)) % 59.27/59.33 [103]~P1(f22(x1031)) % 59.27/59.33 [104]~P1(f16(x1041)) % 59.27/59.33 [93]E(f24(x931,x932),f24(x932,x931)) % 59.27/59.33 [94]P2(f25(x941,x942)) % 59.27/59.33 [95]P2(f8(x951,x952)) % 59.27/59.33 [96]P8(f8(x961,x962)) % 59.27/59.33 [98]P7(f6(x981,x982),x981,x982) % 59.27/59.33 [99]P6(f5(x991,x992),x991,x992) % 59.27/59.33 [100]P6(f8(x1001,x1002),x1001,x1002) % 59.27/59.33 [105]~P1(f24(x1051,x1052)) % 59.27/59.33 [107]~P1(x1071)+E(x1071,a1) % 59.27/59.33 [108]~P1(x1081)+P2(x1081) % 59.27/59.33 [110]P1(x1101)+~P1(f9(x1101)) % 59.27/59.33 [111]P9(f17(x1111),x1111)+E(x1111,a1) % 59.27/59.33 [114]P1(x1141)+P4(f9(x1141),f22(x1141)) % 59.27/59.33 [112]~P9(x1122,x1121)+~E(x1121,a1) % 59.27/59.33 [113]~P1(x1131)+~P9(x1132,x1131) % 59.27/59.33 [115]~P9(x1151,x1152)+P4(x1151,x1152) % 59.27/59.33 [120]~P9(x1202,x1201)+~P9(x1201,x1202) % 59.27/59.33 [116]~P2(x1162)+P2(f27(x1161,x1162)) % 59.27/59.33 [117]~P2(x1172)+P8(f27(x1171,x1172)) % 59.27/59.33 [119]~P3(x1191,x1192)+P4(x1191,f22(x1192)) % 59.27/59.33 [121]P3(x1211,x1212)+~P4(x1211,f22(x1212)) % 59.27/59.33 [122]P3(x1221,x1222)+P9(f21(x1221,x1222),x1221) % 59.27/59.33 [128]P3(x1281,x1282)+~P9(f21(x1281,x1282),x1282) % 59.27/59.33 [123]~P5(x1231,x1232)+P4(x1231,f22(f22(x1232))) % 59.27/59.33 [129]P4(f32(x1291,x1292),f22(x1291))+~P4(x1292,f22(f22(x1291))) % 59.27/59.33 [131]~P6(x1311,x1312,x1313)+P7(x1311,x1312,x1313) % 59.27/59.33 [132]~P7(x1321,x1322,x1323)+P6(x1321,x1322,x1323) % 59.27/59.33 [130]P2(x1301)+~P4(x1301,f22(f25(x1302,x1303))) % 59.27/59.33 [133]~P7(x1331,x1332,x1333)+P4(x1331,f22(f25(x1332,x1333))) % 59.27/59.33 [134]E(f29(x1341,x1342,x1343),f27(x1342,x1343))+~P4(x1343,f22(f25(x1342,x1341))) % 59.27/59.33 [137]~P4(x1373,f22(f25(x1372,x1371)))+P8(f29(x1371,x1372,x1373)) % 59.27/59.33 [140]P10(f29(x1401,x1402,x1403),f22(x1402),f22(x1401))+~P4(x1403,f22(f25(x1402,x1401))) % 59.27/59.33 [141]P7(f29(x1411,x1412,x1413),f22(x1412),f22(x1411))+~P4(x1413,f22(f25(x1412,x1411))) % 59.27/59.33 [142]E(f28(x1421,x1422,x1423,x1424),f31(x1423,x1424))+~P4(x1423,f22(f25(x1421,f22(x1422)))) % 59.27/59.33 [146]P4(f28(x1461,x1462,x1463,x1464),f22(f22(x1462)))+~P4(x1463,f22(f25(x1461,f22(x1462)))) % 59.27/59.33 [109]~P1(x1092)+~P1(x1091)+E(x1091,x1092) % 59.27/59.33 [118]~P4(x1182,x1181)+P1(x1181)+P9(x1182,x1181) % 59.27/59.33 [124]P1(x1241)+P1(x1242)+~P1(f25(x1242,x1241)) % 59.27/59.33 [125]~P9(x1251,x1253)+P9(x1251,x1252)+~P3(x1253,x1252) % 59.27/59.33 [126]~P1(x1261)+~P9(x1262,x1263)+~P4(x1263,f22(x1261)) % 59.27/59.34 [127]P4(x1271,x1272)+~P9(x1271,x1273)+~P4(x1273,f22(x1272)) % 59.27/59.34 [135]~P2(x1353)+~P9(x1352,f31(x1353,f16(x1351)))+P9(f24(f24(x1351,x1352),f16(x1351)),x1353) % 59.27/59.34 [136]~P2(x1362)+~P9(f24(f24(x1363,x1361),f16(x1363)),x1362)+P9(x1361,f31(x1362,f16(x1363))) % 59.27/59.34 [144]~P4(x1443,f22(x1441))+E(f26(x1441,x1442,x1443,x1444),f30(x1441,x1442,x1443,x1444))+~P4(x1444,f22(f25(x1441,x1442))) % 59.27/59.34 [145]~P4(x1453,f22(x1451))+P4(f26(x1451,x1452,x1453,x1454),f22(x1452))+~P4(x1454,f22(f25(x1451,x1452))) % 59.27/59.34 [149]~P4(x1494,f22(x1492))+~P4(x1493,f22(f25(x1492,x1491)))+E(f32(x1491,f28(f22(x1492),x1491,f29(x1491,x1492,x1493),f23(x1494))),f30(x1492,x1491,x1494,x1493)) % 59.27/59.34 [139]~P2(x1392)+P9(f18(x1392,x1393,x1391),x1391)+P9(f20(x1392,x1393,x1391),x1393)+E(x1391,f31(x1392,x1393)) % 59.27/59.34 [150]~P2(x1502)+P9(f18(x1502,x1503,x1501),x1501)+E(x1501,f31(x1502,x1503))+P9(f24(f24(f20(x1502,x1503,x1501),f18(x1502,x1503,x1501)),f16(f20(x1502,x1503,x1501))),x1502) % 59.27/59.34 [143]~P2(x1431)+~P9(x1434,x1433)+~E(x1433,f31(x1431,x1432))+P9(f19(x1431,x1432,x1433,x1434),x1432) % 59.27/59.34 [151]~P2(x1511)+~P9(x1514,x1513)+~E(x1513,f31(x1511,x1512))+P9(f24(f24(f19(x1511,x1512,x1513,x1514),x1514),f16(f19(x1511,x1512,x1513,x1514))),x1511) % 59.27/59.34 [148]~P2(x1482)+~P9(x1484,x1483)+~P9(f18(x1482,x1483,x1481),x1481)+E(x1481,f31(x1482,x1483))+~P9(f24(f24(x1484,f18(x1482,x1483,x1481)),f16(x1484)),x1482) % 59.27/59.34 [138]~P2(x1383)+P9(x1381,x1382)+~P9(x1385,x1384)+~E(x1382,f31(x1383,x1384))+~P9(f24(f24(x1385,x1381),f16(x1385)),x1383) % 59.27/59.34 [147]~P9(x1473,x1474)+~P9(x1471,f26(x1475,x1476,x1474,x1472))+~P4(x1474,f22(x1475))+P9(x1471,f31(x1472,f16(x1473)))+~P4(x1472,f22(f25(x1475,x1476))) % 59.27/59.34 %EqnAxiom % 59.27/59.34 [1]E(x11,x11) % 59.27/59.34 [2]E(x22,x21)+~E(x21,x22) % 59.27/59.34 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 59.27/59.34 [4]~E(x41,x42)+E(f11(x41),f11(x42)) % 59.27/59.34 [5]~E(x51,x52)+E(f22(x51),f22(x52)) % 59.27/59.34 [6]~E(x61,x62)+E(f3(x61),f3(x62)) % 59.27/59.34 [7]~E(x71,x72)+E(f23(x71),f23(x72)) % 59.27/59.34 [8]~E(x81,x82)+E(f4(x81),f4(x82)) % 59.27/59.34 [9]~E(x91,x92)+E(f31(x91,x93),f31(x92,x93)) % 59.27/59.34 [10]~E(x101,x102)+E(f31(x103,x101),f31(x103,x102)) % 59.27/59.34 [11]~E(x111,x112)+E(f24(x111,x113),f24(x112,x113)) % 59.27/59.34 [12]~E(x121,x122)+E(f24(x123,x121),f24(x123,x122)) % 59.27/59.34 [13]~E(x131,x132)+E(f26(x131,x133,x134,x135),f26(x132,x133,x134,x135)) % 59.27/59.34 [14]~E(x141,x142)+E(f26(x143,x141,x144,x145),f26(x143,x142,x144,x145)) % 59.27/59.34 [15]~E(x151,x152)+E(f26(x153,x154,x151,x155),f26(x153,x154,x152,x155)) % 59.27/59.34 [16]~E(x161,x162)+E(f26(x163,x164,x165,x161),f26(x163,x164,x165,x162)) % 59.27/59.34 [17]~E(x171,x172)+E(f19(x171,x173,x174,x175),f19(x172,x173,x174,x175)) % 59.27/59.34 [18]~E(x181,x182)+E(f19(x183,x181,x184,x185),f19(x183,x182,x184,x185)) % 59.27/59.34 [19]~E(x191,x192)+E(f19(x193,x194,x191,x195),f19(x193,x194,x192,x195)) % 59.27/59.34 [20]~E(x201,x202)+E(f19(x203,x204,x205,x201),f19(x203,x204,x205,x202)) % 59.27/59.34 [21]~E(x211,x212)+E(f25(x211,x213),f25(x212,x213)) % 59.27/59.34 [22]~E(x221,x222)+E(f25(x223,x221),f25(x223,x222)) % 59.27/59.34 [23]~E(x231,x232)+E(f8(x231,x233),f8(x232,x233)) % 59.27/59.34 [24]~E(x241,x242)+E(f8(x243,x241),f8(x243,x242)) % 59.27/59.34 [25]~E(x251,x252)+E(f16(x251),f16(x252)) % 59.27/59.34 [26]~E(x261,x262)+E(f28(x261,x263,x264,x265),f28(x262,x263,x264,x265)) % 59.27/59.34 [27]~E(x271,x272)+E(f28(x273,x271,x274,x275),f28(x273,x272,x274,x275)) % 59.27/59.34 [28]~E(x281,x282)+E(f28(x283,x284,x281,x285),f28(x283,x284,x282,x285)) % 59.27/59.34 [29]~E(x291,x292)+E(f28(x293,x294,x295,x291),f28(x293,x294,x295,x292)) % 59.27/59.34 [30]~E(x301,x302)+E(f32(x301,x303),f32(x302,x303)) % 59.27/59.34 [31]~E(x311,x312)+E(f32(x313,x311),f32(x313,x312)) % 59.27/59.34 [32]~E(x321,x322)+E(f6(x321,x323),f6(x322,x323)) % 59.27/59.34 [33]~E(x331,x332)+E(f6(x333,x331),f6(x333,x332)) % 59.27/59.34 [34]~E(x341,x342)+E(f5(x341,x343),f5(x342,x343)) % 59.27/59.34 [35]~E(x351,x352)+E(f5(x353,x351),f5(x353,x352)) % 59.27/59.34 [36]~E(x361,x362)+E(f18(x361,x363,x364),f18(x362,x363,x364)) % 59.27/59.34 [37]~E(x371,x372)+E(f18(x373,x371,x374),f18(x373,x372,x374)) % 59.27/59.34 [38]~E(x381,x382)+E(f18(x383,x384,x381),f18(x383,x384,x382)) % 59.27/59.34 [39]~E(x391,x392)+E(f20(x391,x393,x394),f20(x392,x393,x394)) % 59.27/59.34 [40]~E(x401,x402)+E(f20(x403,x401,x404),f20(x403,x402,x404)) % 59.27/59.34 [41]~E(x411,x412)+E(f20(x413,x414,x411),f20(x413,x414,x412)) % 59.27/59.34 [42]~E(x421,x422)+E(f27(x421,x423),f27(x422,x423)) % 59.27/59.34 [43]~E(x431,x432)+E(f27(x433,x431),f27(x433,x432)) % 59.27/59.34 [44]~E(x441,x442)+E(f30(x441,x443,x444,x445),f30(x442,x443,x444,x445)) % 59.27/59.34 [45]~E(x451,x452)+E(f30(x453,x451,x454,x455),f30(x453,x452,x454,x455)) % 59.27/59.34 [46]~E(x461,x462)+E(f30(x463,x464,x461,x465),f30(x463,x464,x462,x465)) % 59.27/59.34 [47]~E(x471,x472)+E(f30(x473,x474,x475,x471),f30(x473,x474,x475,x472)) % 59.27/59.34 [48]~E(x481,x482)+E(f29(x481,x483,x484),f29(x482,x483,x484)) % 59.27/59.34 [49]~E(x491,x492)+E(f29(x493,x491,x494),f29(x493,x492,x494)) % 59.27/59.34 [50]~E(x501,x502)+E(f29(x503,x504,x501),f29(x503,x504,x502)) % 59.27/59.34 [51]~E(x511,x512)+E(f21(x511,x513),f21(x512,x513)) % 59.27/59.34 [52]~E(x521,x522)+E(f21(x523,x521),f21(x523,x522)) % 59.27/59.34 [53]~E(x531,x532)+E(f9(x531),f9(x532)) % 59.27/59.34 [54]~E(x541,x542)+E(f17(x541),f17(x542)) % 59.27/59.34 [55]~P1(x551)+P1(x552)+~E(x551,x552) % 59.27/59.34 [56]P9(x562,x563)+~E(x561,x562)+~P9(x561,x563) % 59.27/59.34 [57]P9(x573,x572)+~E(x571,x572)+~P9(x573,x571) % 59.27/59.34 [58]~P2(x581)+P2(x582)+~E(x581,x582) % 59.27/59.34 [59]P7(x592,x593,x594)+~E(x591,x592)+~P7(x591,x593,x594) % 59.27/59.34 [60]P7(x603,x602,x604)+~E(x601,x602)+~P7(x603,x601,x604) % 59.27/59.34 [61]P7(x613,x614,x612)+~E(x611,x612)+~P7(x613,x614,x611) % 59.27/59.34 [62]P4(x622,x623)+~E(x621,x622)+~P4(x621,x623) % 59.27/59.34 [63]P4(x633,x632)+~E(x631,x632)+~P4(x633,x631) % 59.27/59.34 [64]P3(x642,x643)+~E(x641,x642)+~P3(x641,x643) % 59.27/59.34 [65]P3(x653,x652)+~E(x651,x652)+~P3(x653,x651) % 59.27/59.34 [66]~P8(x661)+P8(x662)+~E(x661,x662) % 59.27/59.34 [67]P6(x672,x673,x674)+~E(x671,x672)+~P6(x671,x673,x674) % 59.27/59.34 [68]P6(x683,x682,x684)+~E(x681,x682)+~P6(x683,x681,x684) % 59.27/59.34 [69]P6(x693,x694,x692)+~E(x691,x692)+~P6(x693,x694,x691) % 59.27/59.34 [70]~P11(x701)+P11(x702)+~E(x701,x702) % 59.27/59.34 [71]P10(x712,x713,x714)+~E(x711,x712)+~P10(x711,x713,x714) % 59.27/59.34 [72]P10(x723,x722,x724)+~E(x721,x722)+~P10(x723,x721,x724) % 59.27/59.34 [73]P10(x733,x734,x732)+~E(x731,x732)+~P10(x733,x734,x731) % 59.27/59.34 [74]P5(x742,x743)+~E(x741,x742)+~P5(x741,x743) % 59.27/59.34 [75]P5(x753,x752)+~E(x751,x752)+~P5(x753,x751) % 59.27/59.34 % 59.27/59.34 %------------------------------------------- % 59.27/59.34 cnf(152,plain, % 59.27/59.34 (~P9(x1521,a1)), % 59.27/59.34 inference(equality_inference,[],[112])). % 59.27/59.34 cnf(153,plain, % 59.27/59.34 (~P2(x1531)+P9(x1532,f31(x1531,x1533))+~P9(x1534,x1533)+~P9(f24(f24(x1534,x1532),f16(x1534)),x1531)), % 59.27/59.34 inference(equality_inference,[],[138])). % 59.27/59.34 cnf(154,plain, % 59.27/59.34 (~P2(x1541)+~P9(x1542,f31(x1541,x1543))+P9(f19(x1541,x1543,f31(x1541,x1543),x1542),x1543)), % 59.27/59.34 inference(equality_inference,[],[143])). % 59.27/59.34 cnf(156,plain, % 59.27/59.34 (P3(a12,a13)), % 59.27/59.34 inference(scs_inference,[],[88,121])). % 59.27/59.34 cnf(158,plain, % 59.27/59.34 (~P1(a12)), % 59.27/59.34 inference(scs_inference,[],[88,101,121,107])). % 59.27/59.34 cnf(160,plain, % 59.27/59.34 (P9(f17(a12),a12)), % 59.27/59.34 inference(scs_inference,[],[88,101,121,107,111])). % 59.27/59.34 cnf(162,plain, % 59.27/59.34 (P3(a1,x1621)), % 59.27/59.34 inference(scs_inference,[],[88,101,152,121,107,111,122])). % 59.27/59.34 cnf(163,plain, % 59.27/59.34 (~P9(x1631,a1)), % 59.27/59.34 inference(rename_variables,[],[152])). % 59.27/59.34 cnf(165,plain, % 59.27/59.34 (P2(a15)), % 59.27/59.34 inference(scs_inference,[],[88,101,97,152,121,107,111,122,130])). % 59.27/59.34 cnf(167,plain, % 59.27/59.34 (E(f29(a14,a13,a15),f27(a13,a15))), % 59.27/59.34 inference(scs_inference,[],[88,101,97,152,121,107,111,122,130,134])). % 59.27/59.34 cnf(169,plain, % 59.27/59.34 (P10(f29(a14,a13,a15),f22(a13),f22(a14))), % 59.27/59.34 inference(scs_inference,[],[88,101,97,152,121,107,111,122,130,134,140])). % 59.27/59.34 cnf(173,plain, % 59.27/59.34 (E(f27(a13,a15),f29(a14,a13,a15))), % 59.27/59.34 inference(scs_inference,[],[88,101,97,152,121,107,111,122,130,134,140,141,2])). % 59.27/59.34 cnf(174,plain, % 59.27/59.34 (~P9(x1741,a2)), % 59.27/59.34 inference(scs_inference,[],[88,101,97,152,78,121,107,111,122,130,134,140,141,2,113])). % 59.27/59.34 cnf(176,plain, % 59.27/59.34 (~P9(a12,f17(a12))), % 59.27/59.34 inference(scs_inference,[],[88,101,97,152,78,121,107,111,122,130,134,140,141,2,113,120])). % 59.27/59.34 cnf(178,plain, % 59.27/59.34 (P4(f32(x1781,f11(f22(x1781))),f22(x1781))), % 59.27/59.34 inference(scs_inference,[],[88,101,97,152,92,78,121,107,111,122,130,134,140,141,2,113,120,129])). % 59.27/59.34 cnf(181,plain, % 59.27/59.34 (P9(f3(a7),a7)), % 59.27/59.34 inference(scs_inference,[],[88,101,97,152,89,92,78,102,121,107,111,122,130,134,140,141,2,113,120,129,118])). % 59.27/59.34 cnf(182,plain, % 59.27/59.34 (P4(f3(x1821),x1821)), % 59.27/59.34 inference(rename_variables,[],[89])). % 59.27/59.34 cnf(186,plain, % 59.27/59.34 (P4(f17(a12),a13)), % 59.27/59.34 inference(scs_inference,[],[88,101,97,152,89,92,78,102,121,107,111,122,130,134,140,141,2,113,120,129,118,126,127])). % 59.27/59.34 cnf(188,plain, % 59.27/59.34 (E(f26(a13,a14,a12,a15),f30(a13,a14,a12,a15))), % 59.27/59.34 inference(scs_inference,[],[88,101,97,152,89,92,78,102,121,107,111,122,130,134,140,141,2,113,120,129,118,126,127,144])). % 59.27/59.34 cnf(190,plain, % 59.27/59.34 (P4(f26(a13,a14,a12,a15),f22(a14))), % 59.27/59.34 inference(scs_inference,[],[88,101,97,152,89,92,78,102,121,107,111,122,130,134,140,141,2,113,120,129,118,126,127,144,145])). % 59.27/59.34 cnf(192,plain, % 59.27/59.34 (P4(f30(a13,a14,a12,a15),f22(a14))), % 59.27/59.34 inference(scs_inference,[],[88,101,97,152,89,92,78,102,121,107,111,122,130,134,140,141,2,113,120,129,118,126,127,144,145,62])). % 59.27/59.34 cnf(193,plain, % 59.27/59.34 (P4(f3(f24(x1931,x1932)),f24(x1932,x1931))), % 59.27/59.34 inference(scs_inference,[],[88,101,97,152,89,182,92,78,102,93,121,107,111,122,130,134,140,141,2,113,120,129,118,126,127,144,145,62,63])). % 59.27/59.34 cnf(195,plain, % 59.27/59.34 (~E(f31(a15,a12),f26(a13,a14,a12,a15))), % 59.27/59.34 inference(scs_inference,[],[88,101,106,97,152,89,182,92,78,102,87,93,121,107,111,122,130,134,140,141,2,113,120,129,118,126,127,144,145,62,63,64])). % 59.27/59.34 cnf(196,plain, % 59.27/59.34 (P3(x1961,x1961)), % 59.27/59.34 inference(rename_variables,[],[87])). % 59.27/59.34 cnf(201,plain, % 59.27/59.34 (~P9(x2011,f31(a1,f16(x2012)))), % 59.27/59.34 inference(scs_inference,[],[88,101,106,97,152,163,89,182,92,78,102,87,196,93,80,121,107,111,122,130,134,140,141,2,113,120,129,118,126,127,144,145,62,63,64,65,125,135])). % 59.27/59.34 cnf(202,plain, % 59.27/59.34 (~P9(x2021,a1)), % 59.27/59.34 inference(rename_variables,[],[152])). % 59.27/59.34 cnf(204,plain, % 59.27/59.34 (~P9(x2041,f31(a1,a1))), % 59.27/59.34 inference(scs_inference,[],[88,101,106,97,152,163,202,89,182,92,78,102,87,196,93,80,121,107,111,122,130,134,140,141,2,113,120,129,118,126,127,144,145,62,63,64,65,125,135,154])). % 59.27/59.34 cnf(205,plain, % 59.27/59.34 (~P9(x2051,a1)), % 59.27/59.34 inference(rename_variables,[],[152])). % 59.27/59.34 cnf(207,plain, % 59.27/59.34 (~E(a7,a1)), % 59.27/59.34 inference(scs_inference,[],[88,101,106,97,152,163,202,205,89,182,92,78,102,87,196,93,80,121,107,111,122,130,134,140,141,2,113,120,129,118,126,127,144,145,62,63,64,65,125,135,154,57])). % 59.27/59.34 cnf(208,plain, % 59.27/59.34 (~P9(x2081,a1)), % 59.27/59.34 inference(rename_variables,[],[152])). % 59.27/59.34 cnf(209,plain, % 59.27/59.34 (P7(f27(a13,a15),f22(a13),f22(a14))), % 59.27/59.34 inference(scs_inference,[],[88,101,106,97,152,163,202,205,89,182,92,78,102,87,196,93,80,121,107,111,122,130,134,140,141,2,113,120,129,118,126,127,144,145,62,63,64,65,125,135,154,57,59])). % 59.27/59.34 cnf(210,plain, % 59.27/59.34 (P7(f6(f24(x2101,x2102),x2103),f24(x2102,x2101),x2103)), % 59.27/59.34 inference(scs_inference,[],[88,101,106,97,152,163,202,205,89,182,92,78,102,87,196,98,93,80,121,107,111,122,130,134,140,141,2,113,120,129,118,126,127,144,145,62,63,64,65,125,135,154,57,59,60])). % 59.27/59.34 cnf(211,plain, % 59.27/59.34 (P7(f6(x2111,x2112),x2111,x2112)), % 59.27/59.34 inference(rename_variables,[],[98])). % 59.27/59.34 cnf(212,plain, % 59.27/59.34 (P7(f6(x2121,f24(x2122,x2123)),x2121,f24(x2123,x2122))), % 59.27/59.34 inference(scs_inference,[],[88,101,106,97,152,163,202,205,89,182,92,78,102,87,196,98,211,93,80,121,107,111,122,130,134,140,141,2,113,120,129,118,126,127,144,145,62,63,64,65,125,135,154,57,59,60,61])). % 59.27/59.34 cnf(214,plain, % 59.27/59.34 (P6(f5(f24(x2141,x2142),x2143),f24(x2142,x2141),x2143)), % 59.27/59.34 inference(scs_inference,[],[88,101,106,97,152,163,202,205,89,182,92,78,102,87,196,98,211,99,93,80,121,107,111,122,130,134,140,141,2,113,120,129,118,126,127,144,145,62,63,64,65,125,135,154,57,59,60,61,68])). % 59.27/59.34 cnf(215,plain, % 59.27/59.34 (P6(f5(x2151,x2152),x2151,x2152)), % 59.27/59.34 inference(rename_variables,[],[99])). % 59.27/59.34 cnf(216,plain, % 59.27/59.34 (P6(f5(x2161,f24(x2162,x2163)),x2161,f24(x2163,x2162))), % 59.27/59.34 inference(scs_inference,[],[88,101,106,97,152,163,202,205,89,182,92,78,102,87,196,98,211,99,215,93,80,121,107,111,122,130,134,140,141,2,113,120,129,118,126,127,144,145,62,63,64,65,125,135,154,57,59,60,61,68,69])). % 59.27/59.34 cnf(219,plain, % 59.27/59.34 (P5(f23(f24(x2191,x2192)),f24(x2192,x2191))), % 59.27/59.34 inference(scs_inference,[],[88,101,106,97,152,163,202,205,89,182,92,78,102,87,196,98,211,99,215,90,93,80,121,107,111,122,130,134,140,141,2,113,120,129,118,126,127,144,145,62,63,64,65,125,135,154,57,59,60,61,68,69,71,75])). % 59.27/59.34 cnf(221,plain, % 59.27/59.34 (E(a2,f31(a1,a1))), % 59.27/59.34 inference(scs_inference,[],[88,101,106,97,152,163,202,205,208,89,182,92,78,102,87,196,98,211,99,215,90,93,80,121,107,111,122,130,134,140,141,2,113,120,129,118,126,127,144,145,62,63,64,65,125,135,154,57,59,60,61,68,69,71,75,139])). % 59.27/59.34 cnf(222,plain, % 59.27/59.34 (~P9(x2221,a1)), % 59.27/59.34 inference(rename_variables,[],[152])). % 59.27/59.34 cnf(226,plain, % 59.27/59.34 (P9(f18(a1,f31(a1,f16(x2261)),a12),a12)), % 59.27/59.34 inference(scs_inference,[],[88,101,106,97,152,163,202,205,208,222,89,182,92,78,102,87,196,98,211,99,215,90,93,80,121,107,111,122,130,134,140,141,2,113,120,129,118,126,127,144,145,62,63,64,65,125,135,154,57,59,60,61,68,69,71,75,139,143,150])). % 59.27/59.34 cnf(231,plain, % 59.27/59.34 (P1(f31(a1,a1))), % 59.27/59.34 inference(scs_inference,[],[88,101,106,97,152,163,202,205,208,222,89,182,92,78,102,87,196,98,211,99,215,90,93,80,121,107,111,122,130,134,140,141,2,113,120,129,118,126,127,144,145,62,63,64,65,125,135,154,57,59,60,61,68,69,71,75,139,143,150,109,55])). % 59.27/59.34 cnf(232,plain, % 59.27/59.34 (P2(f31(a1,a1))), % 59.27/59.34 inference(scs_inference,[],[88,101,106,97,152,163,202,205,208,222,89,182,92,78,102,87,196,98,211,99,215,90,93,80,81,121,107,111,122,130,134,140,141,2,113,120,129,118,126,127,144,145,62,63,64,65,125,135,154,57,59,60,61,68,69,71,75,139,143,150,109,55,58])). % 59.27/59.34 cnf(233,plain, % 59.27/59.34 (~E(a12,f31(f31(a1,a1),x2331))), % 59.27/59.34 inference(scs_inference,[],[88,101,106,97,152,163,202,205,208,222,89,182,92,78,102,87,196,98,211,99,215,90,93,80,81,121,107,111,122,130,134,140,141,2,113,120,129,118,126,127,144,145,62,63,64,65,125,135,154,57,59,60,61,68,69,71,75,139,143,150,109,55,58,151])). % 59.27/59.34 cnf(239,plain, % 59.27/59.34 (P2(f3(f22(f25(x2391,x2392))))), % 59.27/59.34 inference(scs_inference,[],[89,130])). % 59.27/59.34 cnf(240,plain, % 59.27/59.34 (P4(f3(x2401),x2401)), % 59.27/59.34 inference(rename_variables,[],[89])). % 59.27/59.34 cnf(242,plain, % 59.27/59.34 (P9(f17(a7),a7)), % 59.27/59.34 inference(scs_inference,[],[207,89,130,111])). % 59.27/59.34 cnf(244,plain, % 59.27/59.34 (P3(f31(a1,f16(x2441)),x2442)), % 59.27/59.34 inference(scs_inference,[],[201,207,89,130,111,122])). % 59.27/59.34 cnf(245,plain, % 59.27/59.34 (~P9(x2451,f31(a1,f16(x2452)))), % 59.27/59.34 inference(rename_variables,[],[201])). % 59.27/59.34 cnf(247,plain, % 59.27/59.34 (P7(f29(x2471,x2472,f11(f25(x2472,x2471))),f22(x2472),f22(x2471))), % 59.27/59.34 inference(scs_inference,[],[201,207,89,92,130,111,122,141])). % 59.27/59.34 cnf(248,plain, % 59.27/59.34 (P4(f11(x2481),f22(x2481))), % 59.27/59.34 inference(rename_variables,[],[92])). % 59.27/59.34 cnf(250,plain, % 59.27/59.34 (P3(a15,f25(a13,a14))), % 59.27/59.34 inference(scs_inference,[],[97,201,207,89,92,130,111,122,141,121])). % 59.27/59.34 cnf(252,plain, % 59.27/59.34 (P10(f29(x2521,x2522,f11(f25(x2522,x2521))),f22(x2522),f22(x2521))), % 59.27/59.34 inference(scs_inference,[],[97,201,207,89,92,248,130,111,122,141,121,140])). % 59.27/59.34 cnf(253,plain, % 59.27/59.34 (P4(f11(x2531),f22(x2531))), % 59.27/59.34 inference(rename_variables,[],[92])). % 59.27/59.34 cnf(257,plain, % 59.27/59.34 (E(f30(a13,a14,a12,a15),f26(a13,a14,a12,a15))), % 59.27/59.34 inference(scs_inference,[],[97,188,181,201,207,89,92,248,130,111,122,141,121,140,120,2])). % 59.27/59.34 cnf(258,plain, % 59.27/59.34 (~P9(x2581,f11(x2582))), % 59.27/59.34 inference(scs_inference,[],[97,188,181,201,207,86,89,92,248,130,111,122,141,121,140,120,2,113])). % 59.27/59.34 cnf(260,plain, % 59.27/59.34 (~P9(x2601,f31(f31(a1,a1),f16(x2602)))), % 59.27/59.34 inference(scs_inference,[],[97,188,181,232,201,204,207,86,89,92,248,130,111,122,141,121,140,120,2,113,135])). % 59.27/59.34 cnf(261,plain, % 59.27/59.34 (~P9(x2611,f31(a1,a1))), % 59.27/59.34 inference(rename_variables,[],[204])). % 59.27/59.34 cnf(263,plain, % 59.27/59.34 (P4(f26(a13,x2631,a12,f11(f25(a13,x2631))),f22(x2631))), % 59.27/59.34 inference(scs_inference,[],[88,97,188,181,232,201,204,207,86,89,92,248,253,130,111,122,141,121,140,120,2,113,135,145])). % 59.27/59.34 cnf(266,plain, % 59.27/59.34 (P6(f5(f27(a13,a15),f24(x2661,x2662)),f29(a14,a13,a15),f24(x2662,x2661))), % 59.27/59.34 inference(scs_inference,[],[88,97,173,188,181,216,232,201,204,207,86,89,92,248,253,130,111,122,141,121,140,120,2,113,135,145,68])). % 59.27/59.34 cnf(268,plain, % 59.27/59.34 (~P9(x2681,f3(f22(f31(a1,a1))))), % 59.27/59.34 inference(scs_inference,[],[88,97,173,188,181,216,232,231,201,204,207,86,89,240,92,248,253,130,111,122,141,121,140,120,2,113,135,145,68,126])). % 59.27/59.34 cnf(269,plain, % 59.27/59.34 (P4(f3(x2691),x2691)), % 59.27/59.34 inference(rename_variables,[],[89])). % 59.27/59.34 cnf(272,plain, % 59.27/59.34 (P4(f3(x2721),x2721)), % 59.27/59.34 inference(rename_variables,[],[89])). % 59.27/59.34 cnf(273,plain, % 59.27/59.34 (P9(f3(a12),a12)), % 59.27/59.34 inference(scs_inference,[],[88,97,173,188,181,158,216,232,231,201,204,207,86,89,240,269,272,92,248,253,130,111,122,141,121,140,120,2,113,135,145,68,126,63,118])). % 59.27/59.34 cnf(276,plain, % 59.27/59.34 (P5(f4(f27(a13,a15)),f29(a14,a13,a15))), % 59.27/59.34 inference(scs_inference,[],[88,97,173,188,181,158,216,232,231,201,204,207,86,89,240,269,272,92,248,253,91,130,111,122,141,121,140,120,2,113,135,145,68,126,63,118,75])). % 59.27/59.34 cnf(279,plain, % 59.27/59.34 (~P9(x2791,f31(a1,f16(x2792)))), % 59.27/59.34 inference(rename_variables,[],[201])). % 59.27/59.34 cnf(281,plain, % 59.27/59.34 (~E(a12,f31(a1,f16(x2811)))), % 59.27/59.34 inference(scs_inference,[],[88,97,173,188,160,181,158,165,216,232,231,201,245,279,204,207,86,89,240,269,272,92,248,253,91,130,111,122,141,121,140,120,2,113,135,145,68,126,63,118,75,154,57])). % 59.27/59.34 cnf(282,plain, % 59.27/59.34 (~P9(x2821,f31(a1,f16(x2822)))), % 59.27/59.34 inference(rename_variables,[],[201])). % 59.27/59.34 cnf(283,plain, % 59.27/59.34 (~E(f31(a15,a12),f30(a13,a14,a12,a15))), % 59.27/59.34 inference(scs_inference,[],[88,97,173,188,195,160,181,158,165,216,232,231,201,245,279,204,207,86,89,240,269,272,92,248,253,91,130,111,122,141,121,140,120,2,113,135,145,68,126,63,118,75,154,57,3])). % 59.27/59.34 cnf(284,plain, % 59.27/59.34 (P6(f5(f24(x2841,x2842),f27(a13,a15)),f24(x2842,x2841),f29(a14,a13,a15))), % 59.27/59.34 inference(scs_inference,[],[88,97,173,188,195,160,181,158,165,214,216,232,231,201,245,279,204,207,86,89,240,269,272,92,248,253,91,130,111,122,141,121,140,120,2,113,135,145,68,126,63,118,75,154,57,3,69])). % 59.27/59.34 cnf(286,plain, % 59.27/59.34 (P7(f6(f27(a13,a15),f24(x2861,x2862)),f29(a14,a13,a15),f24(x2862,x2861))), % 59.27/59.34 inference(scs_inference,[],[88,97,173,188,195,160,181,158,165,212,214,216,232,231,201,245,279,204,207,86,89,240,269,272,92,248,253,91,130,111,122,141,121,140,120,2,113,135,145,68,126,63,118,75,154,57,3,69,60])). % 59.27/59.34 cnf(288,plain, % 59.27/59.34 (P7(f6(f24(x2881,x2882),f27(a13,a15)),f24(x2882,x2881),f29(a14,a13,a15))), % 59.27/59.34 inference(scs_inference,[],[88,97,173,188,195,160,181,158,165,210,212,214,216,232,231,201,245,279,204,207,86,89,240,269,272,92,248,253,91,130,111,122,141,121,140,120,2,113,135,145,68,126,63,118,75,154,57,3,69,60,61])). % 59.27/59.34 cnf(290,plain, % 59.27/59.34 (~E(a1,f26(a13,a14,a12,a15))), % 59.27/59.34 inference(scs_inference,[],[88,106,97,173,188,195,160,162,181,158,165,210,212,214,216,232,231,201,245,279,204,207,86,89,240,269,272,92,248,253,91,130,111,122,141,121,140,120,2,113,135,145,68,126,63,118,75,154,57,3,69,60,61,64])). % 59.27/59.34 cnf(293,plain, % 59.27/59.34 (~P9(x2931,f31(a1,f16(x2932)))), % 59.27/59.34 inference(rename_variables,[],[201])). % 59.27/59.34 cnf(294,plain, % 59.27/59.34 (~E(a12,f31(f31(a1,a1),x2941))), % 59.27/59.34 inference(rename_variables,[],[233])). % 59.27/59.34 cnf(296,plain, % 59.27/59.34 (~E(a12,f31(a2,x2961))), % 59.27/59.34 inference(scs_inference,[],[88,106,97,173,188,195,160,162,181,158,165,210,212,214,216,232,231,201,245,279,282,204,174,233,207,86,89,240,269,272,92,248,253,91,81,130,111,122,141,121,140,120,2,113,135,145,68,126,63,118,75,154,57,3,69,60,61,64,139,151])). % 59.27/59.34 cnf(306,plain, % 59.27/59.34 (~P1(f26(a13,a14,a12,a15))), % 59.27/59.34 inference(scs_inference,[],[88,106,97,173,188,195,160,169,162,181,158,165,210,212,214,216,232,231,201,245,279,282,293,204,261,174,233,294,77,207,86,89,240,269,272,92,248,253,91,81,130,111,122,141,121,140,120,2,113,135,145,68,126,63,118,75,154,57,3,69,60,61,64,139,151,150,143,73,109])). % 59.27/59.34 cnf(309,plain, % 59.27/59.34 (~P1(f30(a13,a14,a12,a15))+~E(f22(a14),x3091)), % 59.27/59.34 inference(scs_inference,[],[88,106,97,173,188,195,160,169,162,167,181,158,165,210,212,214,216,232,231,201,245,279,282,293,204,261,174,233,294,77,207,86,89,240,269,272,92,248,253,91,81,130,111,122,141,121,140,120,2,113,135,145,68,126,63,118,75,154,57,3,69,60,61,64,139,151,150,143,73,109,71,55])). % 59.27/59.34 cnf(311,plain, % 59.27/59.34 (P4(x3111,f25(a13,a14))+~P9(x3111,a15)+~E(f22(a14),x3112)), % 59.27/59.34 inference(scs_inference,[],[88,156,106,97,173,188,195,160,169,162,167,181,158,165,210,212,214,216,232,231,201,245,279,282,293,204,261,174,233,294,77,207,86,89,240,269,272,92,248,253,219,91,81,130,111,122,141,121,140,120,2,113,135,145,68,126,63,118,75,154,57,3,69,60,61,64,139,151,150,143,73,109,71,55,127])). % 59.27/59.34 cnf(314,plain, % 59.27/59.34 (~P1(f30(a13,a14,a12,a15))), % 59.27/59.34 inference(equality_inference,[],[309])). % 59.27/59.34 cnf(315,plain, % 59.27/59.34 (P4(x3151,f25(a13,a14))+~P9(x3151,a15)), % 59.27/59.34 inference(equality_inference,[],[311])). % 59.27/59.34 cnf(316,plain, % 59.27/59.34 (P3(f11(x3161),x3162)), % 59.27/59.34 inference(scs_inference,[],[258,122])). % 59.27/59.34 cnf(317,plain, % 59.27/59.34 (~P9(x3171,f11(x3172))), % 59.27/59.34 inference(rename_variables,[],[258])). % 59.27/59.34 cnf(319,plain, % 59.27/59.34 (P3(f26(a13,a14,a12,a15),a14)), % 59.27/59.34 inference(scs_inference,[],[190,258,122,121])). % 59.27/59.34 cnf(321,plain, % 59.27/59.34 (P2(f11(f25(x3211,x3212)))), % 59.27/59.34 inference(scs_inference,[],[190,258,92,122,121,130])). % 59.27/59.34 cnf(322,plain, % 59.27/59.34 (P4(f11(x3221),f22(x3221))), % 59.27/59.34 inference(rename_variables,[],[92])). % 59.27/59.34 cnf(326,plain, % 59.27/59.34 (E(f31(a1,a1),a2)), % 59.27/59.34 inference(scs_inference,[],[190,242,221,258,92,122,121,130,120,2])). % 59.27/59.34 cnf(327,plain, % 59.27/59.34 (~P9(x3271,f31(f11(f25(x3272,x3273)),f16(x3274)))), % 59.27/59.34 inference(scs_inference,[],[190,242,221,258,317,92,122,121,130,120,2,135])). % 59.27/59.34 cnf(328,plain, % 59.27/59.34 (~P9(x3281,f11(x3282))), % 59.27/59.34 inference(rename_variables,[],[258])). % 59.27/59.34 cnf(335,plain, % 59.27/59.34 (~P9(x3351,f11(x3352))), % 59.27/59.34 inference(rename_variables,[],[258])). % 59.27/59.34 cnf(339,plain, % 59.27/59.34 (P9(f3(f26(a13,a14,a12,a15)),f26(a13,a14,a12,a15))), % 59.27/59.34 inference(scs_inference,[],[88,156,190,239,306,242,273,221,258,317,328,284,89,92,93,122,121,130,120,2,135,127,125,154,68,118])). % 59.27/59.34 cnf(340,plain, % 59.27/59.34 (P4(f3(x3401),x3401)), % 59.27/59.34 inference(rename_variables,[],[89])). % 59.27/59.34 cnf(342,plain, % 59.27/59.34 (P5(f23(f30(a13,a14,a12,a15)),f26(a13,a14,a12,a15))), % 59.27/59.34 inference(scs_inference,[],[88,156,190,239,257,306,242,273,221,258,317,328,284,89,92,93,90,122,121,130,120,2,135,127,125,154,68,118,75])). % 59.27/59.34 cnf(345,plain, % 59.27/59.34 (P4(f3(f30(a13,a14,a12,a15)),f26(a13,a14,a12,a15))), % 59.27/59.34 inference(scs_inference,[],[88,156,190,239,257,306,290,242,273,221,258,317,328,284,89,340,92,93,90,122,121,130,120,2,135,127,125,154,68,118,75,3,63])). % 59.27/59.34 cnf(359,plain, % 59.27/59.34 (~P9(x3591,f11(x3592))), % 59.27/59.34 inference(rename_variables,[],[258])). % 59.27/59.34 cnf(362,plain, % 59.27/59.34 (~P9(x3621,f11(x3622))), % 59.27/59.34 inference(rename_variables,[],[258])). % 59.27/59.34 cnf(366,plain, % 59.27/59.34 (~P9(x3661,f11(x3662))), % 59.27/59.34 inference(rename_variables,[],[258])). % 59.27/59.34 cnf(371,plain, % 59.27/59.34 (~P9(x3711,f26(a13,x3712,a12,f11(f25(a13,x3712))))), % 59.27/59.34 inference(scs_inference,[],[88,156,106,190,239,268,257,306,244,290,242,273,221,258,317,328,335,359,362,366,266,284,286,288,296,89,340,92,322,93,90,81,122,121,130,120,2,135,127,125,154,68,118,75,3,63,65,64,60,57,69,61,151,139,143,150,147])). % 59.27/59.34 cnf(376,plain, % 59.27/59.34 (~P1(a14)), % 59.27/59.34 inference(scs_inference,[],[88,156,106,190,239,268,257,306,244,290,242,273,221,258,317,328,335,359,362,366,266,284,286,288,296,89,340,92,322,93,90,81,122,121,130,120,2,135,127,125,154,68,118,75,3,63,65,64,60,57,69,61,151,139,143,150,147,109,126])). % 59.27/59.34 cnf(386,plain, % 59.27/59.34 (P3(f31(f31(a1,a1),f16(x3861)),x3862)), % 59.27/59.34 inference(scs_inference,[],[260,122])). % 59.27/59.34 cnf(387,plain, % 59.27/59.34 (~P9(x3871,f31(f31(a1,a1),f16(x3872)))), % 59.27/59.34 inference(rename_variables,[],[260])). % 59.27/59.34 cnf(391,plain, % 59.27/59.34 (P3(f30(a13,a14,a12,a15),a14)), % 59.27/59.34 inference(scs_inference,[],[192,339,260,122,120,121])). % 59.27/59.34 cnf(393,plain, % 59.27/59.34 (~P9(x3931,f31(a2,f16(x3932)))), % 59.27/59.34 inference(scs_inference,[],[192,339,260,174,81,122,120,121,135])). % 59.27/59.34 cnf(403,plain, % 59.27/59.34 (P9(f3(a14),a14)), % 59.27/59.34 inference(scs_inference,[],[319,192,190,321,339,376,260,387,174,89,81,122,120,121,135,127,125,154,118])). % 59.27/59.34 cnf(404,plain, % 59.27/59.34 (P4(f3(x4041),x4041)), % 59.27/59.34 inference(rename_variables,[],[89])). % 59.27/59.34 cnf(408,plain, % 59.27/59.34 (P4(f3(f26(a13,a14,a12,a15)),f30(a13,a14,a12,a15))), % 59.27/59.34 inference(scs_inference,[],[319,192,190,188,321,339,376,260,387,174,89,404,91,81,122,120,121,135,127,125,154,118,75,63])). % 59.27/59.34 cnf(410,plain, % 59.27/59.34 (P6(f5(f26(a13,a14,a12,a15),f24(x4101,x4102)),f30(a13,a14,a12,a15),f24(x4102,x4101))), % 59.27/59.34 inference(scs_inference,[],[319,192,190,188,321,339,376,260,387,216,174,89,404,91,81,122,120,121,135,127,125,154,118,75,63,68])). % 59.27/59.34 cnf(412,plain, % 59.27/59.34 (~E(f11(x4121),f26(a13,a14,a12,a15))), % 59.27/59.34 inference(scs_inference,[],[319,106,192,190,188,316,321,339,376,260,387,216,174,89,404,91,81,122,120,121,135,127,125,154,118,75,63,68,64])). % 59.27/59.34 cnf(414,plain, % 59.27/59.34 (P7(f6(f26(a13,a14,a12,a15),f24(x4141,x4142)),f30(a13,a14,a12,a15),f24(x4142,x4141))), % 59.27/59.34 inference(scs_inference,[],[319,106,192,190,188,316,321,339,376,260,387,212,216,174,89,404,91,81,122,120,121,135,127,125,154,118,75,63,68,64,60])). % 59.27/59.34 cnf(416,plain, % 59.27/59.34 (P6(f5(f24(x4161,x4162),f26(a13,a14,a12,a15)),f24(x4162,x4161),f30(a13,a14,a12,a15))), % 59.27/59.34 inference(scs_inference,[],[319,106,192,190,188,316,321,339,376,260,387,212,214,216,174,89,404,91,81,122,120,121,135,127,125,154,118,75,63,68,64,60,69])). % 59.27/59.34 cnf(420,plain, % 59.27/59.34 (P7(f6(f24(x4201,x4202),f26(a13,a14,a12,a15)),f24(x4202,x4201),f30(a13,a14,a12,a15))), % 59.27/59.34 inference(scs_inference,[],[319,106,192,190,188,316,321,339,371,376,260,387,210,212,214,216,174,89,404,91,81,122,120,121,135,127,125,154,118,75,63,68,64,60,69,57,61])). % 59.27/59.34 cnf(425,plain, % 59.27/59.34 (P9(f18(a1,f16(x4251),a12),a12)), % 59.27/59.34 inference(scs_inference,[],[319,106,192,190,188,316,321,339,371,376,260,387,281,210,212,214,216,258,152,174,89,404,91,81,80,122,120,121,135,127,125,154,118,75,63,68,64,60,69,57,61,151,150])). % 59.27/59.34 cnf(429,plain, % 59.27/59.34 (~P1(a15)), % 59.27/59.34 inference(scs_inference,[],[319,106,192,190,188,316,321,339,371,376,260,387,281,86,210,212,214,216,258,152,174,89,404,91,81,80,122,120,121,135,127,125,154,118,75,63,68,64,60,69,57,61,151,150,16,109])). % 59.27/59.34 cnf(438,plain, % 59.27/59.34 (P3(f31(f11(f25(x4381,x4382)),f16(x4383)),x4384)), % 59.27/59.34 inference(scs_inference,[],[327,122])). % 59.27/59.34 cnf(439,plain, % 59.27/59.34 (~P9(x4391,f31(f11(f25(x4392,x4393)),f16(x4394)))), % 59.27/59.34 inference(rename_variables,[],[327])). % 59.27/59.34 cnf(448,plain, % 59.27/59.34 (P9(f3(a15),a15)), % 59.27/59.34 inference(scs_inference,[],[263,403,429,321,327,201,89,122,121,120,154,118])). % 59.27/59.34 cnf(451,plain, % 59.27/59.35 (P5(f4(f30(a13,a14,a12,a15)),f26(a13,a14,a12,a15))), % 59.27/59.35 inference(scs_inference,[],[257,263,403,429,321,327,201,89,91,122,121,120,154,118,75])). % 59.27/59.35 cnf(453,plain, % 59.27/59.35 (P6(f5(f24(x4531,x4532),f26(a13,a14,a12,a15)),f24(x4531,x4532),f30(a13,a14,a12,a15))), % 59.27/59.35 inference(scs_inference,[],[257,263,403,429,321,327,201,416,89,93,91,122,121,120,154,118,75,68])). % 59.27/59.35 cnf(459,plain, % 59.27/59.35 (P7(f6(f24(x4591,x4592),f26(a13,a14,a12,a15)),f24(x4591,x4592),f30(a13,a14,a12,a15))), % 59.27/59.35 inference(scs_inference,[],[106,257,386,263,403,429,321,327,201,410,416,420,89,93,91,122,121,120,154,118,75,68,64,69,60])). % 59.27/59.35 cnf(462,plain, % 59.27/59.35 (~P9(x4621,f3(f22(f31(a1,a1))))), % 59.27/59.35 inference(rename_variables,[],[268])). % 59.27/59.35 cnf(471,plain, % 59.27/59.35 (P9(f18(a2,x4711,a12),a12)), % 59.27/59.35 inference(scs_inference,[],[106,257,386,263,403,429,268,321,327,439,201,204,296,410,414,416,420,174,232,89,93,91,81,122,121,120,154,118,75,68,64,69,60,57,61,143,151,150])). % 59.27/59.35 cnf(481,plain, % 59.27/59.35 (~P1(f25(a13,a14))), % 59.27/59.35 inference(scs_inference,[],[97,250,106,257,386,263,403,429,268,462,321,327,439,201,204,296,410,414,416,420,174,232,89,93,91,81,122,121,120,154,118,75,68,64,69,60,57,61,143,151,150,315,135,125,126])). % 59.27/59.35 cnf(483,plain, % 59.27/59.35 (P4(x4831,a14)+~P9(x4831,f30(a13,a14,a12,a15))), % 59.27/59.35 inference(scs_inference,[],[97,250,106,257,192,386,263,403,429,268,462,321,327,439,201,204,296,410,414,416,420,174,232,89,93,91,81,122,121,120,154,118,75,68,64,69,60,57,61,143,151,150,315,135,125,126,127])). % 59.27/59.35 cnf(494,plain, % 59.27/59.35 (~P9(a15,f3(a15))), % 59.27/59.35 inference(scs_inference,[],[448,393,122,120])). % 59.27/59.35 cnf(496,plain, % 59.27/59.35 (P3(f32(x4961,f11(f22(x4961))),x4961)), % 59.27/59.35 inference(scs_inference,[],[448,393,178,122,120,121])). % 59.27/59.35 cnf(501,plain, % 59.27/59.35 (P9(f3(f30(a13,a14,a12,a15)),f26(a13,a14,a12,a15))), % 59.27/59.35 inference(scs_inference,[],[345,448,306,239,393,204,178,122,120,121,154,118])). % 59.27/59.35 cnf(512,plain, % 59.27/59.35 (~P9(x5121,f26(a13,x5122,a12,f11(f25(a13,x5122))))), % 59.27/59.35 inference(rename_variables,[],[371])). % 59.27/59.35 cnf(516,plain, % 59.27/59.35 (~P9(x5161,f11(x5162))), % 59.27/59.35 inference(rename_variables,[],[258])). % 59.27/59.35 cnf(527,plain, % 59.27/59.35 (~P9(x5271,f30(a13,a14,a12,a15))+P9(x5271,a14)), % 59.27/59.35 inference(scs_inference,[],[391,106,257,188,345,252,438,448,306,371,512,239,321,393,258,516,204,178,210,212,214,216,451,122,120,121,154,118,64,68,69,60,57,61,143,151,135,58,72,74,125])). % 59.27/59.35 cnf(529,plain, % 59.27/59.35 (P4(x5291,x5292)+~P9(x5291,f32(x5292,f11(f22(x5292))))), % 59.27/59.35 inference(scs_inference,[],[391,106,257,188,345,252,438,448,306,371,512,239,321,393,258,516,204,178,210,212,214,216,451,122,120,121,154,118,64,68,69,60,57,61,143,151,135,58,72,74,125,127])). % 59.27/59.35 cnf(536,plain, % 59.27/59.35 (P3(f3(f22(x5361)),x5361)), % 59.27/59.35 inference(scs_inference,[],[89,204,122,121])). % 59.27/59.35 cnf(544,plain, % 59.27/59.35 (P9(f3(f26(a13,a14,a12,a15)),f30(a13,a14,a12,a15))), % 59.27/59.35 inference(scs_inference,[],[408,501,165,260,89,204,314,122,121,120,154,118])). % 59.27/59.35 cnf(551,plain, % 59.27/59.35 (P3(f3(f22(f30(a13,a14,a12,a15))),f26(a13,a14,a12,a15))), % 59.27/59.35 inference(scs_inference,[],[319,257,190,412,408,501,165,260,89,204,314,122,121,120,154,118,127,3,125,65])). % 59.27/59.35 cnf(583,plain, % 59.27/59.35 (~P9(x5831,a2)), % 59.27/59.35 inference(rename_variables,[],[174])). % 59.27/59.35 cnf(585,plain, % 59.27/59.35 (~P9(f30(a13,a14,a12,a15),f3(f26(a13,a14,a12,a15)))), % 59.27/59.35 inference(scs_inference,[],[544,174,122,120])). % 59.27/59.35 cnf(587,plain, % 59.27/59.35 (P9(a12,f22(a13))), % 59.27/59.35 inference(scs_inference,[],[88,544,174,103,122,120,118])). % 59.27/59.35 cnf(592,plain, % 59.27/59.35 (P6(f8(x5921,f30(a13,a14,a12,a15)),x5921,f26(a13,a14,a12,a15))), % 59.27/59.35 inference(scs_inference,[],[88,536,106,257,544,174,103,100,122,120,118,64,69])). % 59.27/59.35 cnf(593,plain, % 59.27/59.35 (P6(f8(x5931,x5932),x5931,x5932)), % 59.27/59.35 inference(rename_variables,[],[100])). % 59.27/59.35 cnf(594,plain, % 59.27/59.35 (P6(f8(f30(a13,a14,a12,a15),x5941),f26(a13,a14,a12,a15),x5941)), % 59.27/59.35 inference(scs_inference,[],[88,536,106,257,544,174,103,100,593,122,120,118,64,69,68])). % 59.27/59.35 cnf(596,plain, % 59.27/59.35 (P7(f6(f30(a13,a14,a12,a15),x5961),f26(a13,a14,a12,a15),x5961)), % 59.27/59.35 inference(scs_inference,[],[88,536,106,257,544,174,103,100,593,98,122,120,118,64,69,68,60])). % 59.27/59.35 cnf(597,plain, % 59.27/59.35 (P7(f6(x5971,x5972),x5971,x5972)), % 59.27/59.35 inference(rename_variables,[],[98])). % 59.27/59.35 cnf(598,plain, % 59.27/59.35 (P7(f6(x5981,f30(a13,a14,a12,a15)),x5981,f26(a13,a14,a12,a15))), % 59.27/59.35 inference(scs_inference,[],[88,536,106,257,544,174,103,100,593,98,597,122,120,118,64,69,68,60,61])). % 59.27/59.35 cnf(608,plain, % 59.27/59.35 (P4(x6081,x6082)+~P9(x6081,f3(f22(x6082)))), % 59.27/59.35 inference(scs_inference,[],[88,536,106,257,448,371,544,239,89,174,583,204,103,100,593,98,597,81,122,120,118,64,69,68,60,61,57,143,151,127])). % 59.27/59.35 cnf(611,plain, % 59.27/59.35 (P4(f26(a13,a14,a12,a15),x6111)+~P9(f30(a13,a14,a12,a15),f3(f22(x6111)))), % 59.27/59.35 inference(scs_inference,[],[88,536,106,257,448,371,544,239,89,174,583,204,103,100,593,98,597,81,122,120,118,64,69,68,60,61,57,143,151,127,62])). % 59.27/59.35 cnf(618,plain, % 59.27/59.35 (~P9(x6181,f31(a15,f11(x6182)))), % 59.27/59.35 inference(scs_inference,[],[587,165,258,120,154])). % 59.27/59.35 cnf(621,plain, % 59.27/59.35 (~P4(f22(a13),a12)), % 59.27/59.35 inference(scs_inference,[],[587,158,165,258,120,154,118])). % 59.27/59.35 cnf(624,plain, % 59.27/59.35 (P4(f3(x6241),x6241)), % 59.27/59.35 inference(rename_variables,[],[89])). % 59.27/59.35 cnf(626,plain, % 59.27/59.35 (~E(f17(a12),f22(a13))), % 59.27/59.35 inference(scs_inference,[],[587,158,160,165,258,89,120,154,118,127,56])). % 59.27/59.35 cnf(627,plain, % 59.27/59.35 (~E(f3(a12),f22(a13))), % 59.27/59.35 inference(scs_inference,[],[587,158,160,165,258,89,624,120,154,118,127,56,62])). % 59.27/59.35 cnf(653,plain, % 59.27/59.35 (P9(f3(f16(x6531)),f16(x6531))), % 59.27/59.35 inference(scs_inference,[],[273,89,104,120,118])). % 59.27/59.35 cnf(675,plain, % 59.27/59.35 (~P9(f16(x6751),f3(f16(x6751)))), % 59.27/59.35 inference(scs_inference,[],[653,120])). % 59.27/59.35 cnf(677,plain, % 59.27/59.35 (P9(f3(f24(x6771,x6772)),f24(x6772,x6771))), % 59.27/59.35 inference(scs_inference,[],[193,653,105,120,118])). % 59.27/59.35 cnf(693,plain, % 59.27/59.35 (~P9(f24(x6931,x6932),f3(f24(x6932,x6931)))), % 59.27/59.35 inference(scs_inference,[],[677,120])). % 59.27/59.35 cnf(747,plain, % 59.27/59.35 (P6(x7471,x7472,f26(a13,a14,a12,a15))+~E(f8(x7472,f30(a13,a14,a12,a15)),x7471)), % 59.27/59.35 inference(scs_inference,[],[88,326,371,252,403,592,471,693,120,57,135,70,63,71,67])). % 59.27/59.35 cnf(753,plain, % 59.27/59.35 (~P1(f9(a12))), % 59.27/59.35 inference(scs_inference,[],[101,110,107])). % 59.27/59.35 cnf(756,plain, % 59.27/59.35 (P9(f3(f9(a12)),f9(a12))), % 59.27/59.35 inference(scs_inference,[],[89,425,753,120,118])). % 59.27/59.35 cnf(794,plain, % 59.27/59.35 (P3(a12,x7941)+~E(a13,x7941)), % 59.27/59.35 inference(scs_inference,[],[156,167,173,268,544,226,120,57,70,58,65])). % 59.27/59.35 cnf(852,plain, % 59.27/59.35 (P5(x8521,x8522)+~E(f23(x8522),x8521)), % 59.27/59.35 inference(scs_inference,[],[90,74])). % 59.27/59.35 cnf(865,plain, % 59.27/59.35 (P4(x8651,f22(x8652))+~E(f26(a13,x8652,a12,f11(f25(a13,x8652))),x8651)), % 59.27/59.35 inference(scs_inference,[],[263,62])). % 59.27/59.35 cnf(867,plain, % 59.27/59.35 (P3(f22(a13),x8671)+~E(f26(a13,x8671,a12,f11(f25(a13,x8671))),f22(a13))), % 59.27/59.35 inference(scs_inference,[],[263,621,62,63,121])). % 59.27/59.35 cnf(872,plain, % 59.27/59.35 (~P9(x8721,f3(f22(a1)))), % 59.27/59.35 inference(scs_inference,[],[89,77,126])). % 59.27/59.35 cnf(916,plain, % 59.27/59.35 (P4(f26(a13,x9161,a12,f11(f25(a13,x9161))),x9162)+~E(f22(x9161),x9162)), % 59.27/59.35 inference(scs_inference,[],[551,263,186,209,62,60,64,63])). % 59.27/59.35 cnf(931,plain, % 59.27/59.35 (E(f32(a14,f28(f22(a13),a14,f29(a14,a13,a15),f23(a12))),f30(a13,a14,a12,a15))), % 59.27/59.35 inference(scs_inference,[],[587,97,115,149])). % 59.27/59.35 cnf(932,plain, % 59.27/59.35 (E(f30(a13,a14,a12,a15),f32(a14,f28(f22(a13),a14,f29(a14,a13,a15),f23(a12))))), % 59.27/59.35 inference(scs_inference,[],[931,2])). % 59.27/59.35 cnf(934,plain, % 59.27/59.35 (~P1(f32(a14,f28(f22(a13),a14,f29(a14,a13,a15),f23(a12))))), % 59.27/59.35 inference(scs_inference,[],[283,931,314,2,3,55])). % 59.27/59.35 cnf(1006,plain, % 59.27/59.35 (P4(x10061,f22(x10062))+~E(f11(x10062),x10061)), % 59.27/59.35 inference(scs_inference,[],[181,872,92,57,62])). % 59.27/59.35 cnf(1064,plain, % 59.27/59.35 (P4(x10641,f22(x10642))+~E(f32(x10642,f11(f22(x10642))),x10641)), % 59.27/59.35 inference(scs_inference,[],[178,62])). % 59.27/59.35 cnf(1066,plain, % 59.27/59.35 (P3(f22(a13),x10661)+~E(f32(x10661,f11(f22(x10661))),f22(a13))), % 59.27/59.35 inference(scs_inference,[],[621,178,62,63,121])). % 59.27/59.35 cnf(1071,plain, % 59.27/59.35 (P2(f27(x10711,a1))), % 59.27/59.35 inference(scs_inference,[],[77,116,108])). % 59.27/59.35 cnf(1120,plain, % 59.27/59.35 (P6(x11201,f26(a13,a14,a12,a15),x11202)+~E(f8(f30(a13,a14,a12,a15),x11202),x11201)), % 59.27/59.35 inference(scs_inference,[],[594,67])). % 59.27/59.35 cnf(1314,plain, % 59.27/59.35 (P4(f11(x13141),x13142)+~E(f22(x13141),x13142)), % 59.27/59.35 inference(scs_inference,[],[92,63])). % 59.27/59.35 cnf(1349,plain, % 59.27/59.35 (P6(x13491,x13492,x13493)+~E(f8(x13492,x13493),x13491)), % 59.27/59.35 inference(scs_inference,[],[100,67])). % 59.27/59.35 cnf(1362,plain, % 59.27/59.35 (P9(a15,f22(f25(a13,a14)))), % 59.27/59.35 inference(scs_inference,[],[97,103,118])). % 59.27/59.35 cnf(1367,plain, % 59.27/59.35 (~P9(f22(f25(a13,a14)),a15)), % 59.27/59.35 inference(scs_inference,[],[97,872,103,118,57,120])). % 59.27/59.35 cnf(1382,plain, % 59.27/59.35 (~P4(f22(f25(a13,a14)),a15)), % 59.27/59.35 inference(scs_inference,[],[429,1367,118])). % 59.27/59.35 cnf(1413,plain, % 59.27/59.35 (P4(f9(a12),f22(a12))), % 59.27/59.35 inference(scs_inference,[],[101,114,107])). % 59.27/59.35 cnf(1421,plain, % 59.27/59.35 (~P4(f22(a13),f9(a12))), % 59.27/59.35 inference(scs_inference,[],[77,621,178,753,1413,121,127,126,118])). % 59.27/59.35 cnf(1423,plain, % 59.27/59.35 (P9(f3(f9(a12)),a12)), % 59.27/59.35 inference(scs_inference,[],[77,756,621,178,753,1413,121,127,126,118,125])). % 59.27/59.35 cnf(1454,plain, % 59.27/59.35 (E(f22(f3(f30(a13,a14,a12,a15))),f22(f3(f26(a13,a14,a12,a15))))), % 59.27/59.35 inference(scs_inference,[],[257,5,6])). % 59.27/59.35 cnf(1455,plain, % 59.27/59.35 (~P9(x14551,f32(a2,f11(f22(a2))))), % 59.27/59.35 inference(scs_inference,[],[78,178,126])). % 59.27/59.35 cnf(1461,plain, % 59.27/59.35 (E(f23(f4(f30(a13,a14,a12,a15))),f23(f4(f26(a13,a14,a12,a15))))), % 59.27/59.35 inference(scs_inference,[],[257,7,8])). % 59.27/59.35 cnf(1462,plain, % 59.27/59.35 (E(f16(f31(f30(a13,a14,a12,a15),x14621)),f16(f31(f26(a13,a14,a12,a15),x14621)))), % 59.27/59.35 inference(scs_inference,[],[257,25,9])). % 59.27/59.35 cnf(1488,plain, % 59.27/59.35 (~P9(x14881,f31(a1,f11(x14882)))), % 59.27/59.35 inference(scs_inference,[],[80,258,154])). % 59.27/59.35 cnf(1502,plain, % 59.27/59.35 (~P9(x15021,f31(a1,f31(a1,a1)))), % 59.27/59.35 inference(scs_inference,[],[80,204,154])). % 59.27/59.35 cnf(1558,plain, % 59.27/59.35 (~P9(x15581,f31(a1,a2))), % 59.27/59.35 inference(scs_inference,[],[80,174,154])). % 59.27/59.35 cnf(1572,plain, % 59.27/59.35 (P4(f23(f30(a13,a14,a12,a15)),f22(f22(f30(a13,a14,a12,a15))))), % 59.27/59.35 inference(scs_inference,[],[342,188,123,75])). % 59.27/59.35 cnf(1573,plain, % 59.27/59.35 (P4(f32(f30(a13,a14,a12,a15),f23(f30(a13,a14,a12,a15))),f22(f30(a13,a14,a12,a15)))), % 59.27/59.35 inference(scs_inference,[],[1572,129])). % 59.27/59.35 cnf(1583,plain, % 59.27/59.35 (P3(f31(a1,f31(a15,f11(x15831))),x15832)), % 59.27/59.35 inference(scs_inference,[],[80,448,174,618,1572,129,121,154,143,122])). % 59.27/59.35 cnf(1604,plain, % 59.27/59.35 (P3(f31(a1,f31(a1,f11(x16041))),x16042)), % 59.27/59.35 inference(scs_inference,[],[80,106,257,448,1583,618,1488,1573,121,154,65,64,143,122])). % 59.27/59.35 cnf(1622,plain, % 59.27/59.35 (~P9(x16221,f31(a1,f31(a1,a2)))), % 59.27/59.35 inference(scs_inference,[],[80,1558,154])). % 59.27/59.35 cnf(1630,plain, % 59.27/59.35 (P3(f31(a1,f31(a1,a2)),x16301)), % 59.27/59.35 inference(scs_inference,[],[80,106,448,1604,1488,1558,154,64,143,122])). % 59.27/59.35 cnf(1640,plain, % 59.27/59.35 (~P9(x16401,f31(a1,f31(a1,a2)))), % 59.27/59.35 inference(rename_variables,[],[1622])). % 59.27/59.35 cnf(1647,plain, % 59.27/59.35 (P3(f31(a1,f31(a1,f31(a1,a2))),x16471)), % 59.27/59.35 inference(scs_inference,[],[80,106,448,1630,1622,1640,154,64,143,122])). % 59.27/59.35 cnf(1666,plain, % 59.27/59.35 (~P9(x16661,f31(a1,f31(a1,a1)))), % 59.27/59.35 inference(rename_variables,[],[1502])). % 59.27/59.35 cnf(1673,plain, % 59.27/59.35 (P3(f31(a1,f31(a1,f31(a1,a1))),x16731)), % 59.27/59.35 inference(scs_inference,[],[80,106,448,1647,1502,1666,154,64,143,122])). % 59.27/59.35 cnf(1685,plain, % 59.27/59.35 (~E(a15,f31(a1,f31(a1,a2)))), % 59.27/59.35 inference(scs_inference,[],[80,106,448,1673,1558,64,143])). % 59.27/59.35 cnf(3376,plain, % 59.27/59.35 (E(f24(x33761,f11(f30(a13,a14,a12,a15))),f24(x33761,f11(f26(a13,a14,a12,a15))))), % 59.27/59.35 inference(scs_inference,[],[257,12,4])). % 59.27/59.35 cnf(3383,plain, % 59.27/59.35 (E(f8(f23(f30(a13,a14,a12,a15)),x33831),f8(f23(f26(a13,a14,a12,a15)),x33831))), % 59.27/59.35 inference(scs_inference,[],[257,23,7])). % 59.27/59.35 cnf(3384,plain, % 59.27/59.35 (P4(f26(a13,a14,f3(f22(a13)),a15),f22(a14))), % 59.27/59.35 inference(scs_inference,[],[89,97,145])). % 59.27/59.35 cnf(3385,plain, % 59.27/59.35 (P4(f3(x33851),x33851)), % 59.27/59.35 inference(rename_variables,[],[89])). % 59.27/59.35 cnf(3390,plain, % 59.27/59.35 (P3(f26(a13,a14,f3(f22(a13)),a15),a14)), % 59.27/59.35 inference(scs_inference,[],[89,3385,97,481,145,118,121])). % 59.27/59.35 cnf(3411,plain, % 59.27/59.35 (E(f8(x34111,f4(f30(a13,a14,a12,a15))),f8(x34111,f4(f26(a13,a14,a12,a15))))), % 59.27/59.35 inference(scs_inference,[],[257,24,8])). % 59.27/59.35 cnf(3412,plain, % 59.27/59.35 (P4(f26(x34121,x34122,f3(f22(x34121)),f11(f25(x34121,x34122))),f22(x34122))), % 59.27/59.35 inference(scs_inference,[],[89,92,145])). % 59.27/59.35 cnf(3416,plain, % 59.27/59.35 (~P9(f22(a13),f26(x34161,a12,f3(f22(x34161)),f11(f25(x34161,a12))))), % 59.27/59.35 inference(scs_inference,[],[89,621,92,145,127])). % 59.27/59.35 cnf(3449,plain, % 59.27/59.35 (P3(f26(x34491,x34492,f3(f22(x34491)),f11(f25(x34491,x34492))),x34492)), % 59.27/59.35 inference(scs_inference,[],[3412,121])). % 59.27/59.35 cnf(3489,plain, % 59.27/59.35 (P4(x34891,f22(x34892))+~E(f26(x34893,x34892,f3(f22(x34893)),f11(f25(x34893,x34892))),x34891)), % 59.27/59.35 inference(scs_inference,[],[89,3390,3412,105,118,120,65,62])). % 59.27/59.35 cnf(3507,plain, % 59.27/59.35 (P9(f3(f30(a13,a14,a12,a15)),f30(a13,a14,a12,a15))), % 59.27/59.35 inference(scs_inference,[],[89,314,118])). % 59.27/59.35 cnf(3725,plain, % 59.27/59.35 (E(f32(f31(f30(a13,a14,a12,a15),x37251),x37252),f32(f31(f26(a13,a14,a12,a15),x37251),x37252))), % 59.27/59.35 inference(scs_inference,[],[257,30,9])). % 59.27/59.35 cnf(3738,plain, % 59.27/59.35 (P4(f11(f3(f30(a13,a14,a12,a15))),f22(f3(f26(a13,a14,a12,a15))))), % 59.27/59.35 inference(scs_inference,[],[1454,1314])). % 59.27/59.35 cnf(3739,plain, % 59.27/59.35 (P6(f8(f23(f26(a13,a14,a12,a15)),f30(a13,a14,a12,a15)),f23(f30(a13,a14,a12,a15)),f26(a13,a14,a12,a15))), % 59.27/59.35 inference(scs_inference,[],[3383,1454,1314,747])). % 59.27/59.35 cnf(3740,plain, % 59.27/59.35 (E(f8(f23(f30(a13,a14,a12,a15)),x37401),f8(f23(f26(a13,a14,a12,a15)),x37401))), % 59.27/59.35 inference(rename_variables,[],[3383])). % 59.27/59.35 cnf(3742,plain, % 59.27/59.35 (E(f8(x37421,f4(f30(a13,a14,a12,a15))),f8(x37421,f4(f26(a13,a14,a12,a15))))), % 59.27/59.35 inference(rename_variables,[],[3411])). % 59.27/59.35 cnf(3743,plain, % 59.27/59.35 (P6(f8(x37431,f4(f26(a13,a14,a12,a15))),x37431,f4(f30(a13,a14,a12,a15)))), % 59.27/59.35 inference(scs_inference,[],[3411,3742,3383,1454,1314,747,1120,1349])). % 59.27/59.35 cnf(3745,plain, % 59.27/59.35 (E(f29(x37451,x37452,f11(f25(x37452,x37451))),f27(x37452,f11(f25(x37452,x37451))))), % 59.27/59.35 inference(scs_inference,[],[92,3411,3742,1461,3383,1454,1314,747,1120,1349,852,134])). % 59.27/59.35 cnf(3748,plain, % 59.27/59.35 (P4(f32(x37481,f3(f22(f22(x37481)))),f22(x37481))), % 59.27/59.35 inference(scs_inference,[],[89,92,3411,3742,1461,3383,1454,1314,747,1120,1349,852,134,129])). % 59.27/59.35 cnf(3749,plain, % 59.27/59.35 (P4(f3(x37491),x37491)), % 59.27/59.35 inference(rename_variables,[],[89])). % 59.27/59.35 cnf(3752,plain, % 59.27/59.35 (P4(f3(x37521),x37521)), % 59.27/59.35 inference(rename_variables,[],[89])). % 59.27/59.35 cnf(3758,plain, % 59.27/59.35 (P4(f3(x37581),x37581)), % 59.27/59.35 inference(rename_variables,[],[89])). % 59.27/59.35 cnf(3763,plain, % 59.27/59.35 (P3(f26(a13,x37631,a12,f11(f25(a13,x37631))),x37632)), % 59.27/59.35 inference(scs_inference,[],[89,3749,3752,263,371,92,1462,3411,3742,1461,3383,1454,1314,747,1120,1349,852,134,129,141,130,140,2,121,122])). % 59.27/59.35 cnf(3764,plain, % 59.27/59.35 (~P9(x37641,f26(a13,x37642,a12,f11(f25(a13,x37642))))), % 59.27/59.35 inference(rename_variables,[],[371])). % 59.27/59.35 cnf(3770,plain, % 59.27/59.35 (E(f24(x37701,f11(f30(a13,a14,a12,a15))),f24(x37701,f11(f26(a13,a14,a12,a15))))), % 59.27/59.35 inference(rename_variables,[],[3376])). % 59.27/59.35 cnf(3783,plain, % 59.27/59.35 (P10(f27(x37831,f11(f25(x37831,x37832))),f22(x37831),f22(x37832))), % 59.27/59.35 inference(scs_inference,[],[89,3749,3752,3758,97,536,188,252,263,872,371,621,3412,92,453,231,1462,3376,3770,3411,3742,1461,3383,1454,93,1314,747,1120,1349,852,134,129,141,130,140,2,121,122,144,3,127,126,69,125,68,71])). % 59.27/59.35 cnf(3788,plain, % 59.27/59.35 (P7(f27(x37881,f11(f25(x37881,x37882))),f22(x37881),f22(x37882))), % 59.27/59.35 inference(scs_inference,[],[89,3749,3752,3758,97,536,257,188,252,247,263,872,371,621,3412,92,453,459,231,1462,3376,3770,3411,3742,1461,3383,1454,93,1314,747,1120,1349,852,134,129,141,130,140,2,121,122,144,3,127,126,69,125,68,71,60,61,59])). % 59.27/59.35 cnf(3792,plain, % 59.27/59.35 (P3(f32(f30(a13,a14,a12,a15),f11(f22(f30(a13,a14,a12,a15)))),f26(a13,a14,a12,a15))), % 59.27/59.35 inference(scs_inference,[],[89,3749,3752,3758,97,536,496,257,188,252,247,263,872,371,621,3412,92,453,459,231,1462,3376,3770,3411,3742,1461,3383,3740,1454,93,1314,747,1120,1349,852,134,129,141,130,140,2,121,122,144,3,127,126,69,125,68,71,60,61,59,67,65])). % 59.27/59.35 cnf(3795,plain, % 59.27/59.35 (~P9(x37951,f31(f3(f22(f25(x37952,x37953))),f3(f22(a1))))), % 59.27/59.35 inference(scs_inference,[],[89,3749,3752,3758,97,536,496,257,188,252,247,263,872,3384,371,621,3412,239,92,453,459,231,1462,3376,3770,3411,3742,1461,3383,3740,1454,93,1314,747,1120,1349,852,134,129,141,130,140,2,121,122,144,3,127,126,69,125,68,71,60,61,59,67,65,62,154])). % 59.27/59.35 cnf(3796,plain, % 59.27/59.35 (~P9(x37961,f3(f22(a1)))), % 59.27/59.35 inference(rename_variables,[],[872])). % 59.27/59.35 cnf(3802,plain, % 59.27/59.35 (~E(a15,f31(f3(f22(f25(x38021,x38022))),f3(f22(a1))))), % 59.27/59.35 inference(scs_inference,[],[89,3749,3752,3758,97,536,3390,496,257,188,252,247,263,448,872,3796,3384,371,3764,621,3412,239,92,453,459,231,1462,3376,3770,3411,3742,1461,3383,3740,1454,93,1314,747,1120,1349,852,134,129,141,130,140,2,121,122,144,3,127,126,69,125,68,71,60,61,59,67,65,62,154,135,64,143])). % 59.27/59.35 cnf(3822,plain, % 59.27/59.35 (~E(f30(a13,a14,a12,a15),a1)), % 59.27/59.35 inference(scs_inference,[],[934,3507,110,112])). % 59.27/59.35 cnf(3830,plain, % 59.27/59.35 (P4(f9(a7),f22(a7))), % 59.27/59.35 inference(scs_inference,[],[1071,3788,934,3507,102,110,112,116,117,132,114])). % 59.27/59.35 cnf(3841,plain, % 59.27/59.35 (E(f16(f31(a1,a1)),f16(a2))), % 59.27/59.35 inference(scs_inference,[],[1071,3788,934,1421,3507,102,276,326,110,112,116,117,132,114,123,608,4,5,6,7,8,25])). % 59.27/59.35 cnf(3876,plain, % 59.27/59.35 (E(f26(f31(a1,a1),x38761,x38762,x38763),f26(a2,x38761,x38762,x38763))), % 59.27/59.35 inference(scs_inference,[],[1071,3788,934,1421,3507,102,276,326,92,110,112,116,117,132,114,123,608,4,5,6,7,8,25,53,54,9,10,11,12,21,22,23,24,30,31,32,33,34,35,42,43,51,52,529,137,36,37,38,39,40,41,48,49,50,13])). % 59.27/59.35 cnf(3877,plain, % 59.27/59.35 (E(f26(x38771,f31(a1,a1),x38772,x38773),f26(x38771,a2,x38772,x38773))), % 59.27/59.35 inference(scs_inference,[],[1071,3788,934,1421,3507,102,276,326,92,110,112,116,117,132,114,123,608,4,5,6,7,8,25,53,54,9,10,11,12,21,22,23,24,30,31,32,33,34,35,42,43,51,52,529,137,36,37,38,39,40,41,48,49,50,13,14])). % 59.27/59.35 cnf(3894,plain, % 59.27/59.35 (P2(f11(x38941))), % 59.27/59.35 inference(scs_inference,[],[1071,3788,3739,934,1421,3507,102,276,326,86,92,110,112,116,117,132,114,123,608,4,5,6,7,8,25,53,54,9,10,11,12,21,22,23,24,30,31,32,33,34,35,42,43,51,52,529,137,36,37,38,39,40,41,48,49,50,13,14,15,17,18,19,20,26,27,28,29,44,45,46,47,916,131,108])). % 59.27/59.35 cnf(3897,plain, % 59.27/59.35 (E(f11(x38971),a1)), % 59.27/59.35 inference(scs_inference,[],[1071,3788,3739,934,1421,3507,102,276,326,86,92,110,112,116,117,132,114,123,608,4,5,6,7,8,25,53,54,9,10,11,12,21,22,23,24,30,31,32,33,34,35,42,43,51,52,529,137,36,37,38,39,40,41,48,49,50,13,14,15,17,18,19,20,26,27,28,29,44,45,46,47,916,131,108,16,107])). % 59.27/59.35 cnf(3904,plain, % 59.27/59.35 (P4(f26(a13,x39041,a12,f11(f25(a13,x39041))),f22(x39042))), % 59.27/59.35 inference(scs_inference,[],[1071,3788,3739,3763,934,1421,1455,1423,3507,102,276,326,86,92,110,112,116,117,132,114,123,608,4,5,6,7,8,25,53,54,9,10,11,12,21,22,23,24,30,31,32,33,34,35,42,43,51,52,529,137,36,37,38,39,40,41,48,49,50,13,14,15,17,18,19,20,26,27,28,29,44,45,46,47,916,131,108,16,107,111,115,119])). % 59.27/59.35 cnf(3908,plain, % 59.27/59.35 (~P9(f21(f26(a13,a14,a12,a15),f31(a15,a12)),f31(a15,a12))), % 59.27/59.35 inference(scs_inference,[],[1071,3788,3739,3763,934,1421,1455,1423,3507,102,276,326,86,92,106,110,112,116,117,132,114,123,608,4,5,6,7,8,25,53,54,9,10,11,12,21,22,23,24,30,31,32,33,34,35,42,43,51,52,529,137,36,37,38,39,40,41,48,49,50,13,14,15,17,18,19,20,26,27,28,29,44,45,46,47,916,131,108,16,107,111,115,119,133,128])). % 59.27/59.35 cnf(3911,plain, % 59.27/59.35 (~P4(f26(a13,a14,a12,a15),f22(f31(a15,a12)))), % 59.27/59.35 inference(scs_inference,[],[626,1071,3788,3739,3763,934,1421,1455,1423,3507,102,276,326,86,92,106,110,112,116,117,132,114,123,608,4,5,6,7,8,25,53,54,9,10,11,12,21,22,23,24,30,31,32,33,34,35,42,43,51,52,529,137,36,37,38,39,40,41,48,49,50,13,14,15,17,18,19,20,26,27,28,29,44,45,46,47,916,131,108,16,107,111,115,119,133,128,2,121])). % 59.27/59.35 cnf(3913,plain, % 59.27/59.35 (P9(f21(f26(a13,a14,a12,a15),f31(a15,a12)),f26(a13,a14,a12,a15))), % 59.27/59.35 inference(scs_inference,[],[626,1071,3788,3739,3763,934,1421,1455,1423,3507,102,276,326,86,92,106,110,112,116,117,132,114,123,608,4,5,6,7,8,25,53,54,9,10,11,12,21,22,23,24,30,31,32,33,34,35,42,43,51,52,529,137,36,37,38,39,40,41,48,49,50,13,14,15,17,18,19,20,26,27,28,29,44,45,46,47,916,131,108,16,107,111,115,119,133,128,2,121,122])). % 59.27/59.35 cnf(3915,plain, % 59.27/59.35 (~P1(f25(a7,a7))), % 59.27/59.35 inference(scs_inference,[],[626,1071,3788,3739,3763,934,1421,1455,1423,3507,102,276,326,86,92,106,110,112,116,117,132,114,123,608,4,5,6,7,8,25,53,54,9,10,11,12,21,22,23,24,30,31,32,33,34,35,42,43,51,52,529,137,36,37,38,39,40,41,48,49,50,13,14,15,17,18,19,20,26,27,28,29,44,45,46,47,916,131,108,16,107,111,115,119,133,128,2,121,122,124])). % 59.27/59.35 cnf(3924,plain, % 59.27/59.35 (P1(f31(f3(f22(f25(x39241,x39242))),f3(f22(a1))))), % 59.27/59.35 inference(scs_inference,[],[626,1071,3788,3739,3763,934,3748,3725,3795,1421,1382,1455,1423,3507,102,276,326,86,92,89,106,110,112,116,117,132,114,123,608,4,5,6,7,8,25,53,54,9,10,11,12,21,22,23,24,30,31,32,33,34,35,42,43,51,52,529,137,36,37,38,39,40,41,48,49,50,13,14,15,17,18,19,20,26,27,28,29,44,45,46,47,916,131,108,16,107,111,115,119,133,128,2,121,122,124,3,127,126,118])). % 59.27/59.35 cnf(3925,plain, % 59.27/59.35 (~P9(x39251,f31(f3(f22(f25(x39252,x39253))),f3(f22(a1))))), % 59.27/59.35 inference(rename_variables,[],[3795])). % 59.27/59.35 cnf(3929,plain, % 59.27/59.35 (P5(f23(x39291),x39291)), % 59.27/59.35 inference(rename_variables,[],[90])). % 59.27/59.35 cnf(3937,plain, % 59.27/59.35 (~P4(f30(a13,a14,a12,a15),f22(f31(a15,a12)))), % 59.27/59.35 inference(scs_inference,[],[626,1071,3788,3739,3763,934,3748,3745,3725,3795,3925,1421,1382,1455,1423,3507,102,87,276,326,86,90,92,89,106,257,110,112,116,117,132,114,123,608,4,5,6,7,8,25,53,54,9,10,11,12,21,22,23,24,30,31,32,33,34,35,42,43,51,52,529,137,36,37,38,39,40,41,48,49,50,13,14,15,17,18,19,20,26,27,28,29,44,45,46,47,916,131,108,16,107,111,115,119,133,128,2,121,122,124,3,127,126,118,75,125,55,66,65,62])). % 59.27/59.35 cnf(3941,plain, % 59.27/59.35 (~P3(f30(a13,a14,a12,a15),f31(a15,a12))), % 59.27/59.35 inference(scs_inference,[],[494,626,1071,585,3788,3739,3763,934,3748,3745,3725,3795,3925,1421,1382,1455,1423,3507,102,87,276,1362,326,86,90,190,931,92,89,106,257,110,112,116,117,132,114,123,608,4,5,6,7,8,25,53,54,9,10,11,12,21,22,23,24,30,31,32,33,34,35,42,43,51,52,529,137,36,37,38,39,40,41,48,49,50,13,14,15,17,18,19,20,26,27,28,29,44,45,46,47,916,131,108,16,107,111,115,119,133,128,2,121,122,124,3,127,126,118,75,125,55,66,65,62,56,63,57,64])). % 59.27/59.35 cnf(3946,plain, % 59.27/59.35 (~P9(x39461,f31(f31(a1,a1),x39462))), % 59.27/59.35 inference(scs_inference,[],[494,626,1071,585,3788,3739,3763,934,3748,3745,3725,3795,3925,3802,1421,1382,1455,1423,3507,102,87,276,1362,326,86,90,190,931,174,92,81,239,872,89,106,257,110,112,116,117,132,114,123,608,4,5,6,7,8,25,53,54,9,10,11,12,21,22,23,24,30,31,32,33,34,35,42,43,51,52,529,137,36,37,38,39,40,41,48,49,50,13,14,15,17,18,19,20,26,27,28,29,44,45,46,47,916,131,108,16,107,111,115,119,133,128,2,121,122,124,3,127,126,118,75,125,55,66,65,62,56,63,57,64,139,151])). % 59.27/59.35 cnf(3947,plain, % 59.27/59.35 (~P9(x39471,a2)), % 59.27/59.35 inference(rename_variables,[],[174])). % 59.27/59.35 cnf(3949,plain, % 59.27/59.35 (P9(f18(a1,f31(a1,a2),a15),a15)), % 59.27/59.35 inference(scs_inference,[],[494,626,1071,585,3788,3739,3763,934,3748,3745,3725,3795,3925,3802,1421,1382,1455,1685,1423,3507,102,87,276,1362,326,86,90,190,931,152,174,92,81,80,239,872,89,106,257,110,112,116,117,132,114,123,608,4,5,6,7,8,25,53,54,9,10,11,12,21,22,23,24,30,31,32,33,34,35,42,43,51,52,529,137,36,37,38,39,40,41,48,49,50,13,14,15,17,18,19,20,26,27,28,29,44,45,46,47,916,131,108,16,107,111,115,119,133,128,2,121,122,124,3,127,126,118,75,125,55,66,65,62,56,63,57,64,139,151,150])). % 59.27/59.35 cnf(3952,plain, % 59.27/59.35 (~P9(x39521,f31(f27(x39522,a1),f31(a1,a1)))), % 59.27/59.35 inference(scs_inference,[],[494,626,1071,585,3788,3739,3763,934,3748,3745,3725,3795,3925,3802,1421,1382,1455,1685,1423,3507,102,87,276,1362,326,86,90,190,931,152,174,3947,92,81,80,239,872,89,106,257,110,112,116,117,132,114,123,608,4,5,6,7,8,25,53,54,9,10,11,12,21,22,23,24,30,31,32,33,34,35,42,43,51,52,529,137,36,37,38,39,40,41,48,49,50,13,14,15,17,18,19,20,26,27,28,29,44,45,46,47,916,131,108,16,107,111,115,119,133,128,2,121,122,124,3,127,126,118,75,125,55,66,65,62,56,63,57,64,139,151,150,143])). % 59.27/59.35 cnf(3970,plain, % 59.27/59.35 (P6(f8(x39701,f31(a1,a1)),x39701,a2)), % 59.27/59.35 inference(scs_inference,[],[88,494,626,1071,585,3788,3739,3763,934,3748,3745,3725,3795,3925,3802,1421,1382,1455,1685,1423,3507,102,87,276,1362,100,326,86,90,190,931,152,339,174,3947,92,81,80,239,872,89,106,257,97,110,112,116,117,132,114,123,608,4,5,6,7,8,25,53,54,9,10,11,12,21,22,23,24,30,31,32,33,34,35,42,43,51,52,529,137,36,37,38,39,40,41,48,49,50,13,14,15,17,18,19,20,26,27,28,29,44,45,46,47,916,131,108,16,107,111,115,119,133,128,2,121,122,124,3,127,126,118,75,125,55,66,65,62,56,63,57,64,139,151,150,143,147,794,1064,865,3489,611,113,1006,120,136,69])). % 59.27/59.35 cnf(3975,plain, % 59.27/59.35 (P10(f27(x39751,f11(f25(x39751,x39752))),f22(x39751),f22(x39752))), % 59.27/59.35 inference(rename_variables,[],[3783])). % 59.27/59.35 cnf(3977,plain, % 59.27/59.35 (P10(f27(x39771,f11(f25(x39771,x39772))),f22(x39771),f22(x39772))), % 59.27/59.35 inference(rename_variables,[],[3783])). % 59.27/59.35 cnf(3981,plain, % 59.27/59.35 (P7(f6(x39811,f30(a13,a14,a12,a15)),x39811,f26(a13,a14,a12,a15))), % 59.27/59.35 inference(rename_variables,[],[598])). % 59.27/59.35 cnf(3982,plain, % 59.27/59.35 (P5(f23(a2),f31(a1,a1))), % 59.27/59.35 inference(scs_inference,[],[88,494,626,1071,585,3783,3975,3977,3788,3739,3763,934,3743,3748,3745,3725,3795,3925,3802,1421,1382,1455,1685,1423,3507,102,87,276,1362,598,100,326,86,90,3929,190,931,152,339,174,3947,92,81,80,239,872,89,106,257,97,110,112,116,117,132,114,123,608,4,5,6,7,8,25,53,54,9,10,11,12,21,22,23,24,30,31,32,33,34,35,42,43,51,52,529,137,36,37,38,39,40,41,48,49,50,13,14,15,17,18,19,20,26,27,28,29,44,45,46,47,916,131,108,16,107,111,115,119,133,128,2,121,122,124,3,127,126,118,75,125,55,66,65,62,56,63,57,64,139,151,150,143,147,794,1064,865,3489,611,113,1006,120,136,69,68,71,72,73,60,74])). % 59.27/59.35 cnf(3986,plain, % 59.27/59.35 (P7(f6(a2,f30(a13,a14,a12,a15)),f31(a1,a1),f26(a13,a14,a12,a15))), % 59.27/59.35 inference(scs_inference,[],[88,494,626,1071,585,3783,3975,3977,3788,3739,3763,934,3743,3748,3745,3725,3795,3925,3802,1421,1382,1455,1685,1423,3507,102,87,276,1362,596,598,3981,100,326,86,90,3929,190,931,152,339,174,3947,92,81,80,239,872,89,106,257,97,110,112,116,117,132,114,123,608,4,5,6,7,8,25,53,54,9,10,11,12,21,22,23,24,30,31,32,33,34,35,42,43,51,52,529,137,36,37,38,39,40,41,48,49,50,13,14,15,17,18,19,20,26,27,28,29,44,45,46,47,916,131,108,16,107,111,115,119,133,128,2,121,122,124,3,127,126,118,75,125,55,66,65,62,56,63,57,64,139,151,150,143,147,794,1064,865,3489,611,113,1006,120,136,69,68,71,72,73,60,74,61,59])). % 59.27/59.35 cnf(4005,plain, % 59.27/59.35 (P4(f26(a13,x40051,a12,f11(f25(a13,x40051))),f22(x40052))), % 59.27/59.35 inference(rename_variables,[],[3904])). % 59.27/59.35 cnf(4067,plain, % 59.27/59.35 (~P9(x40671,f31(f31(a1,a1),x40672))), % 59.27/59.35 inference(rename_variables,[],[3946])). % 59.27/59.35 cnf(4106,plain, % 59.27/59.35 (P3(f26(x41061,x41062,f3(f22(x41061)),f11(f25(x41061,x41062))),x41062)), % 59.27/59.35 inference(rename_variables,[],[3449])). % 59.27/59.35 cnf(4110,plain, % 59.27/59.35 (E(f11(x41101),a1)), % 59.27/59.35 inference(rename_variables,[],[3897])). % 59.27/59.35 cnf(4122,plain, % 59.27/59.35 (~P9(x41221,f31(f31(a1,a1),x41222))), % 59.27/59.35 inference(rename_variables,[],[3946])). % 59.27/59.35 cnf(4126,plain, % 59.27/59.35 (P2(f11(x41261))), % 59.27/59.35 inference(rename_variables,[],[3894])). % 59.27/59.35 cnf(4127,plain, % 59.27/59.35 (~P9(x41271,f11(x41272))), % 59.27/59.35 inference(rename_variables,[],[258])). % 59.27/59.35 cnf(4130,plain, % 59.27/59.35 (~P9(x41301,f31(f31(a1,a1),x41302))), % 59.27/59.35 inference(rename_variables,[],[3946])). % 59.27/59.35 cnf(4131,plain, % 59.27/59.35 (P2(f11(x41311))), % 59.27/59.35 inference(rename_variables,[],[3894])). % 59.27/59.35 cnf(4135,plain, % 59.27/59.35 (~P9(x41351,f31(f31(a1,a1),x41352))), % 59.27/59.35 inference(rename_variables,[],[3946])). % 59.27/59.35 cnf(4154,plain, % 59.27/59.35 ($false), % 59.27/59.35 inference(scs_inference,[],[88,176,627,3894,4126,4131,3941,3982,3822,3830,3897,4110,3915,95,3913,3876,3877,3986,3841,3908,675,3946,4067,4122,4130,4135,3952,3911,3937,3970,3949,3904,4005,3449,4106,3416,3792,3738,3924,1382,471,103,932,190,587,258,4127,165,89,97,114,112,529,132,608,137,39,22,46,33,44,3489,123,35,51,53,41,29,36,21,19,131,9,108,11,40,23,48,14,52,42,10,117,12,13,110,7,5,27,45,865,18,28,38,26,54,116,43,17,24,25,30,8,47,31,49,50,1064,20,111,6,37,34,107,4,133,15,32,115,16,119,128,2,120,122,124,145,3,127,118,125,55,65,56,62,63,57,64,153,139,151,150,143,147,1066,867,483,527,113,121,154,135]), % 59.27/59.35 ['proof']). % 59.27/59.35 % SZS output end Proof % 59.27/59.35 % Total time :58.630000s %------------------------------------------------------------------------------