%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : TOP028+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 : n024.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 21:15:09 EDT 2024 % Result : Theorem 59.25s 59.26s % Output : CNFRefutation 59.25s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : TOP028+1 : TPTP v8.2.0. Released v3.4.0. % 0.07/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n024.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Tue Jun 18 10:59:54 EDT 2024 % 0.12/0.33 % CPUTime : % 0.43/0.57 start to proof:theBenchmark % 59.18/59.23 %------------------------------------------- % 59.18/59.23 % File :CSE---1.7 % 59.18/59.23 % Problem :theBenchmark % 59.18/59.23 % Transform :cnf % 59.18/59.23 % Format :tptp:raw % 59.18/59.23 % Command :java -jar mcs_scs.jar %d %s % 59.18/59.23 % 59.18/59.23 % Result :Theorem 58.580000s % 59.18/59.23 % Output :CNFRefutation 58.580000s % 59.18/59.23 %------------------------------------------- % 59.18/59.24 %------------------------------------------------------------------------------ % 59.18/59.24 % File : TOP028+1 : TPTP v8.2.0. Released v3.4.0. % 59.18/59.24 % Domain : Topology % 59.18/59.24 % Problem : Maximal Kolmogorov Subspaces of a Topological Space T10 % 59.18/59.24 % Version : [Urb08] axioms : Especial. % 59.18/59.24 % English : % 59.18/59.24 % 59.18/59.24 % Refs : [Kar96] Karno (1996), Maximal Kolmogorov Subspaces of a Topolo % 59.18/59.24 % : [Urb07] Urban (2007), MPTP 0.2: Design, Implementation, and In % 59.18/59.24 % : [Urb08] Urban (2006), Email to G. Sutcliffe % 59.18/59.24 % Source : [Urb08] % 59.18/59.24 % Names : t10_tsp_2 [Urb08] % 59.18/59.24 % 59.18/59.24 % Status : Theorem % 59.18/59.24 % Rating : 0.17 v8.2.0, 0.14 v8.1.0, 0.17 v7.5.0, 0.19 v7.4.0, 0.13 v7.3.0, 0.14 v7.2.0, 0.10 v7.1.0, 0.09 v7.0.0, 0.10 v6.4.0, 0.15 v6.3.0, 0.21 v6.2.0, 0.24 v6.1.0, 0.20 v6.0.0, 0.17 v5.5.0, 0.19 v5.4.0, 0.21 v5.3.0, 0.26 v5.2.0, 0.15 v5.1.0, 0.24 v5.0.0, 0.21 v4.1.0, 0.26 v4.0.1, 0.30 v4.0.0, 0.33 v3.7.0, 0.20 v3.5.0, 0.21 v3.4.0 % 59.18/59.24 % Syntax : Number of formulae : 63 ( 10 unt; 0 def) % 59.18/59.24 % Number of atoms : 266 ( 2 equ) % 59.18/59.24 % Maximal formula atoms : 15 ( 4 avg) % 59.18/59.24 % Number of connectives : 227 ( 24 ~; 1 |; 129 &) % 59.18/59.24 % ( 1 <=>; 72 =>; 0 <=; 0 <~>) % 59.18/59.24 % Maximal formula depth : 15 ( 6 avg) % 59.18/59.24 % Maximal term depth : 3 ( 1 avg) % 59.18/59.24 % Number of predicates : 27 ( 25 usr; 1 prp; 0-2 aty) % 59.18/59.24 % Number of functors : 4 ( 4 usr; 1 con; 0-1 aty) % 59.18/59.24 % Number of variables : 100 ( 84 !; 16 ?) % 59.18/59.24 % SPC : FOF_THM_RFO_SEQ % 59.18/59.24 % 59.18/59.24 % Comments : Normal version: includes the axioms (which may be theorems from % 59.18/59.24 % other articles) and background that are possibly necessary. % 59.18/59.24 % : Translated by MPTP from the Mizar Mathematical Library 4.48.930. % 59.18/59.24 % : The problem encoding is based on set theory. % 59.18/59.24 %------------------------------------------------------------------------------ % 59.18/59.24 fof(t10_tsp_2,conjecture, % 59.18/59.24 ! [A] : % 59.18/59.24 ( ( ~ v3_struct_0(A) % 59.18/59.24 & v2_pre_topc(A) % 59.18/59.24 & l1_pre_topc(A) ) % 59.18/59.24 => ? [B] : % 59.18/59.24 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 59.18/59.24 & v1_tsp_2(B,A) ) ) ). % 59.18/59.24 % 59.18/59.24 fof(antisymmetry_r2_hidden,axiom, % 59.18/59.24 ! [A,B] : % 59.18/59.24 ( r2_hidden(A,B) % 59.18/59.24 => ~ r2_hidden(B,A) ) ). % 59.18/59.24 % 59.18/59.24 fof(cc10_membered,axiom, % 59.18/59.24 ! [A] : % 59.18/59.24 ( v1_membered(A) % 59.18/59.24 => ! [B] : % 59.18/59.24 ( m1_subset_1(B,A) % 59.18/59.24 => v1_xcmplx_0(B) ) ) ). % 59.18/59.24 % 59.18/59.24 fof(cc11_membered,axiom, % 59.18/59.24 ! [A] : % 59.18/59.24 ( v2_membered(A) % 59.18/59.24 => ! [B] : % 59.18/59.24 ( m1_subset_1(B,A) % 59.18/59.24 => ( v1_xcmplx_0(B) % 59.18/59.24 & v1_xreal_0(B) ) ) ) ). % 59.18/59.24 % 59.18/59.24 fof(cc12_membered,axiom, % 59.18/59.24 ! [A] : % 59.18/59.24 ( v3_membered(A) % 59.18/59.24 => ! [B] : % 59.18/59.24 ( m1_subset_1(B,A) % 59.18/59.24 => ( v1_xcmplx_0(B) % 59.18/59.24 & v1_xreal_0(B) % 59.18/59.24 & v1_rat_1(B) ) ) ) ). % 59.18/59.24 % 59.18/59.24 fof(cc13_membered,axiom, % 59.18/59.24 ! [A] : % 59.18/59.24 ( v4_membered(A) % 59.18/59.24 => ! [B] : % 59.18/59.24 ( m1_subset_1(B,A) % 59.18/59.24 => ( v1_xcmplx_0(B) % 59.18/59.24 & v1_xreal_0(B) % 59.18/59.24 & v1_int_1(B) % 59.18/59.24 & v1_rat_1(B) ) ) ) ). % 59.18/59.24 % 59.18/59.24 fof(cc14_membered,axiom, % 59.18/59.24 ! [A] : % 59.18/59.24 ( v5_membered(A) % 59.18/59.24 => ! [B] : % 59.18/59.24 ( m1_subset_1(B,A) % 59.18/59.24 => ( v1_xcmplx_0(B) % 59.18/59.24 & v4_ordinal2(B) % 59.18/59.24 & v1_xreal_0(B) % 59.18/59.24 & v1_int_1(B) % 59.18/59.24 & v1_rat_1(B) ) ) ) ). % 59.18/59.24 % 59.18/59.24 fof(cc15_membered,axiom, % 59.18/59.24 ! [A] : % 59.18/59.24 ( v1_xboole_0(A) % 59.18/59.24 => ( v1_membered(A) % 59.18/59.24 & v2_membered(A) % 59.18/59.24 & v3_membered(A) % 59.18/59.24 & v4_membered(A) % 59.18/59.24 & v5_membered(A) ) ) ). % 59.18/59.24 % 59.18/59.24 fof(cc16_membered,axiom, % 59.18/59.24 ! [A] : % 59.18/59.24 ( v1_membered(A) % 59.18/59.24 => ! [B] : % 59.18/59.24 ( m1_subset_1(B,k1_zfmisc_1(A)) % 59.18/59.24 => v1_membered(B) ) ) ). % 59.18/59.24 % 59.18/59.24 fof(cc17_membered,axiom, % 59.18/59.24 ! [A] : % 59.18/59.24 ( v2_membered(A) % 59.18/59.24 => ! [B] : % 59.18/59.24 ( m1_subset_1(B,k1_zfmisc_1(A)) % 59.18/59.24 => ( v1_membered(B) % 59.18/59.24 & v2_membered(B) ) ) ) ). % 59.18/59.24 % 59.18/59.24 fof(cc18_membered,axiom, % 59.18/59.24 ! [A] : % 59.18/59.24 ( v3_membered(A) % 59.18/59.24 => ! [B] : % 59.18/59.24 ( m1_subset_1(B,k1_zfmisc_1(A)) % 59.18/59.24 => ( v1_membered(B) % 59.18/59.24 & v2_membered(B) % 59.18/59.24 & v3_membered(B) ) ) ) ). % 59.18/59.24 % 59.18/59.24 fof(cc19_membered,axiom, % 59.18/59.24 ! [A] : % 59.18/59.24 ( v4_membered(A) % 59.18/59.24 => ! [B] : % 59.18/59.24 ( m1_subset_1(B,k1_zfmisc_1(A)) % 59.18/59.24 => ( v1_membered(B) % 59.18/59.24 & v2_membered(B) % 59.18/59.24 & v3_membered(B) % 59.18/59.24 & v4_membered(B) ) ) ) ). % 59.18/59.24 % 59.18/59.24 fof(cc1_membered,axiom, % 59.18/59.24 ! [A] : % 59.18/59.24 ( v5_membered(A) % 59.18/59.24 => v4_membered(A) ) ). % 59.18/59.24 % 59.18/59.24 fof(cc1_tops_1,axiom, % 59.18/59.24 ! [A] : % 59.18/59.24 ( ( v2_pre_topc(A) % 59.18/59.24 & l1_pre_topc(A) ) % 59.18/59.24 => ! [B] : % 59.18/59.24 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 59.18/59.25 => ( v1_xboole_0(B) % 59.18/59.25 => ( v3_pre_topc(B,A) % 59.18/59.25 & v4_pre_topc(B,A) ) ) ) ) ). % 59.18/59.25 % 59.18/59.25 fof(cc20_membered,axiom, % 59.18/59.25 ! [A] : % 59.18/59.25 ( v5_membered(A) % 59.18/59.25 => ! [B] : % 59.18/59.25 ( m1_subset_1(B,k1_zfmisc_1(A)) % 59.18/59.25 => ( v1_membered(B) % 59.18/59.25 & v2_membered(B) % 59.18/59.25 & v3_membered(B) % 59.18/59.25 & v4_membered(B) % 59.18/59.25 & v5_membered(B) ) ) ) ). % 59.18/59.25 % 59.18/59.25 fof(cc2_membered,axiom, % 59.18/59.25 ! [A] : % 59.18/59.25 ( v4_membered(A) % 59.18/59.25 => v3_membered(A) ) ). % 59.18/59.25 % 59.18/59.25 fof(cc2_tops_1,axiom, % 59.18/59.25 ! [A] : % 59.18/59.25 ( l1_pre_topc(A) % 59.18/59.25 => ! [B] : % 59.18/59.25 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 59.18/59.25 => ( v1_xboole_0(B) % 59.18/59.25 => v2_tops_1(B,A) ) ) ) ). % 59.18/59.25 % 59.18/59.25 fof(cc3_membered,axiom, % 59.18/59.25 ! [A] : % 59.18/59.25 ( v3_membered(A) % 59.18/59.25 => v2_membered(A) ) ). % 59.18/59.25 % 59.18/59.25 fof(cc3_tops_1,axiom, % 59.18/59.25 ! [A] : % 59.18/59.25 ( ( v2_pre_topc(A) % 59.18/59.25 & l1_pre_topc(A) ) % 59.18/59.25 => ! [B] : % 59.18/59.25 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 59.18/59.25 => ( v1_xboole_0(B) % 59.18/59.25 => v3_tops_1(B,A) ) ) ) ). % 59.18/59.25 % 59.18/59.25 fof(cc4_membered,axiom, % 59.18/59.25 ! [A] : % 59.18/59.25 ( v2_membered(A) % 59.18/59.25 => v1_membered(A) ) ). % 59.18/59.25 % 59.18/59.25 fof(cc4_tops_1,axiom, % 59.18/59.25 ! [A] : % 59.18/59.25 ( ( v2_pre_topc(A) % 59.18/59.25 & l1_pre_topc(A) ) % 59.18/59.25 => ! [B] : % 59.18/59.25 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 59.18/59.25 => ( v3_tops_1(B,A) % 59.18/59.25 => v2_tops_1(B,A) ) ) ) ). % 59.18/59.25 % 59.18/59.25 fof(cc5_tops_1,axiom, % 59.18/59.25 ! [A] : % 59.18/59.25 ( ( v2_pre_topc(A) % 59.18/59.25 & l1_pre_topc(A) ) % 59.18/59.25 => ! [B] : % 59.18/59.25 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 59.18/59.25 => ( ( v4_pre_topc(B,A) % 59.18/59.25 & v2_tops_1(B,A) ) % 59.18/59.25 => ( v2_tops_1(B,A) % 59.18/59.25 & v3_tops_1(B,A) ) ) ) ) ). % 59.18/59.25 % 59.18/59.25 fof(cc6_tops_1,axiom, % 59.18/59.25 ! [A] : % 59.18/59.25 ( ( v2_pre_topc(A) % 59.18/59.25 & l1_pre_topc(A) ) % 59.18/59.25 => ! [B] : % 59.18/59.25 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 59.18/59.25 => ( ( v3_pre_topc(B,A) % 59.18/59.25 & v3_tops_1(B,A) ) % 59.18/59.25 => ( v1_xboole_0(B) % 59.18/59.25 & v3_pre_topc(B,A) % 59.18/59.25 & v4_pre_topc(B,A) % 59.18/59.25 & v1_membered(B) % 59.18/59.25 & v2_membered(B) % 59.18/59.25 & v3_membered(B) % 59.18/59.25 & v4_membered(B) % 59.18/59.25 & v5_membered(B) % 59.18/59.25 & v2_tops_1(B,A) % 59.18/59.25 & v3_tops_1(B,A) ) ) ) ) ). % 59.18/59.25 % 59.18/59.25 fof(dt_k1_pre_topc,axiom, % 59.18/59.25 ! [A] : % 59.18/59.25 ( l1_struct_0(A) % 59.18/59.25 => m1_subset_1(k1_pre_topc(A),k1_zfmisc_1(u1_struct_0(A))) ) ). % 59.18/59.25 % 59.18/59.25 fof(dt_k1_xboole_0,axiom, % 59.18/59.25 $true ). % 59.18/59.25 % 59.18/59.25 fof(dt_k1_zfmisc_1,axiom, % 59.18/59.25 $true ). % 59.18/59.25 % 59.18/59.25 fof(dt_l1_pre_topc,axiom, % 59.18/59.25 ! [A] : % 59.18/59.25 ( l1_pre_topc(A) % 59.18/59.25 => l1_struct_0(A) ) ). % 59.18/59.25 % 59.18/59.25 fof(dt_l1_struct_0,axiom, % 59.18/59.25 $true ). % 59.18/59.25 % 59.18/59.25 fof(dt_m1_subset_1,axiom, % 59.18/59.25 $true ). % 59.18/59.25 % 59.18/59.25 fof(dt_u1_struct_0,axiom, % 59.18/59.25 $true ). % 59.18/59.25 % 59.18/59.25 fof(existence_l1_pre_topc,axiom, % 59.18/59.25 ? [A] : l1_pre_topc(A) ). % 59.18/59.25 % 59.18/59.25 fof(existence_l1_struct_0,axiom, % 59.18/59.25 ? [A] : l1_struct_0(A) ). % 59.18/59.25 % 59.18/59.25 fof(existence_m1_subset_1,axiom, % 59.18/59.25 ! [A] : % 59.18/59.25 ? [B] : m1_subset_1(B,A) ). % 59.18/59.25 % 59.18/59.25 fof(fc1_pre_topc,axiom, % 59.18/59.25 ! [A] : % 59.18/59.25 ( l1_struct_0(A) % 59.18/59.25 => ( v1_xboole_0(k1_pre_topc(A)) % 59.18/59.25 & v1_membered(k1_pre_topc(A)) % 59.18/59.25 & v2_membered(k1_pre_topc(A)) % 59.18/59.25 & v3_membered(k1_pre_topc(A)) % 59.18/59.25 & v4_membered(k1_pre_topc(A)) % 59.18/59.25 & v5_membered(k1_pre_topc(A)) ) ) ). % 59.18/59.25 % 59.18/59.25 fof(fc1_struct_0,axiom, % 59.18/59.25 ! [A] : % 59.18/59.25 ( ( ~ v3_struct_0(A) % 59.18/59.25 & l1_struct_0(A) ) % 59.18/59.25 => ~ v1_xboole_0(u1_struct_0(A)) ) ). % 59.18/59.25 % 59.18/59.25 fof(fc1_subset_1,axiom, % 59.18/59.25 ! [A] : ~ v1_xboole_0(k1_zfmisc_1(A)) ). % 59.18/59.25 % 59.18/59.25 fof(fc1_tops_1,axiom, % 59.18/59.25 ! [A] : % 59.18/59.25 ( ( v2_pre_topc(A) % 59.18/59.25 & l1_pre_topc(A) ) % 59.18/59.25 => ( v1_xboole_0(k1_pre_topc(A)) % 59.18/59.25 & v4_pre_topc(k1_pre_topc(A),A) % 59.18/59.25 & v1_membered(k1_pre_topc(A)) % 59.18/59.25 & v2_membered(k1_pre_topc(A)) % 59.18/59.25 & v3_membered(k1_pre_topc(A)) % 59.18/59.25 & v4_membered(k1_pre_topc(A)) % 59.18/59.25 & v5_membered(k1_pre_topc(A)) ) ) ). % 59.18/59.25 % 59.18/59.25 fof(fc6_membered,axiom, % 59.18/59.25 ( v1_xboole_0(k1_xboole_0) % 59.18/59.25 & v1_membered(k1_xboole_0) % 59.18/59.25 & v2_membered(k1_xboole_0) % 59.18/59.25 & v3_membered(k1_xboole_0) % 59.18/59.25 & v4_membered(k1_xboole_0) % 59.18/59.25 & v5_membered(k1_xboole_0) ) ). % 59.18/59.25 % 59.18/59.25 fof(fc7_tops_1,axiom, % 59.18/59.25 ! [A] : % 59.18/59.25 ( ( v2_pre_topc(A) % 59.18/59.25 & l1_pre_topc(A) ) % 59.18/59.25 => ( v1_xboole_0(k1_pre_topc(A)) % 59.18/59.25 & v3_pre_topc(k1_pre_topc(A),A) % 59.18/59.25 & v4_pre_topc(k1_pre_topc(A),A) % 59.18/59.25 & v1_membered(k1_pre_topc(A)) % 59.18/59.25 & v2_membered(k1_pre_topc(A)) % 59.18/59.25 & v3_membered(k1_pre_topc(A)) % 59.18/59.25 & v4_membered(k1_pre_topc(A)) % 59.18/59.25 & v5_membered(k1_pre_topc(A)) ) ) ). % 59.18/59.25 % 59.18/59.25 fof(rc1_membered,axiom, % 59.18/59.25 ? [A] : % 59.18/59.25 ( ~ v1_xboole_0(A) % 59.18/59.25 & v1_membered(A) % 59.18/59.25 & v2_membered(A) % 59.18/59.25 & v3_membered(A) % 59.18/59.25 & v4_membered(A) % 59.18/59.25 & v5_membered(A) ) ). % 59.18/59.25 % 59.18/59.25 fof(rc1_subset_1,axiom, % 59.18/59.25 ! [A] : % 59.18/59.25 ( ~ v1_xboole_0(A) % 59.18/59.25 => ? [B] : % 59.18/59.25 ( m1_subset_1(B,k1_zfmisc_1(A)) % 59.18/59.25 & ~ v1_xboole_0(B) ) ) ). % 59.18/59.25 % 59.18/59.25 fof(rc1_tops_1,axiom, % 59.18/59.25 ! [A] : % 59.18/59.25 ( ( v2_pre_topc(A) % 59.18/59.25 & l1_pre_topc(A) ) % 59.18/59.25 => ? [B] : % 59.18/59.25 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 59.18/59.25 & v3_pre_topc(B,A) ) ) ). % 59.18/59.25 % 59.18/59.25 fof(rc2_subset_1,axiom, % 59.18/59.25 ! [A] : % 59.18/59.25 ? [B] : % 59.18/59.25 ( m1_subset_1(B,k1_zfmisc_1(A)) % 59.18/59.25 & v1_xboole_0(B) ) ). % 59.18/59.25 % 59.18/59.25 fof(rc2_tops_1,axiom, % 59.18/59.25 ! [A] : % 59.18/59.25 ( ( v2_pre_topc(A) % 59.18/59.25 & l1_pre_topc(A) ) % 59.18/59.25 => ? [B] : % 59.18/59.25 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 59.18/59.25 & v3_pre_topc(B,A) % 59.18/59.25 & v4_pre_topc(B,A) ) ) ). % 59.18/59.25 % 59.18/59.25 fof(rc3_struct_0,axiom, % 59.18/59.25 ? [A] : % 59.25/59.25 ( l1_struct_0(A) % 59.25/59.25 & ~ v3_struct_0(A) ) ). % 59.25/59.25 % 59.25/59.25 fof(rc3_tops_1,axiom, % 59.25/59.25 ! [A] : % 59.25/59.25 ( ( ~ v3_struct_0(A) % 59.25/59.25 & v2_pre_topc(A) % 59.25/59.25 & l1_pre_topc(A) ) % 59.25/59.25 => ? [B] : % 59.25/59.25 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 59.25/59.25 & ~ v1_xboole_0(B) % 59.25/59.25 & v3_pre_topc(B,A) % 59.25/59.25 & v4_pre_topc(B,A) ) ) ). % 59.25/59.25 % 59.25/59.25 fof(rc4_tops_1,axiom, % 59.25/59.25 ! [A] : % 59.25/59.25 ( l1_pre_topc(A) % 59.25/59.25 => ? [B] : % 59.25/59.25 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 59.25/59.25 & v1_xboole_0(B) % 59.25/59.25 & v1_membered(B) % 59.25/59.25 & v2_membered(B) % 59.25/59.25 & v3_membered(B) % 59.25/59.25 & v4_membered(B) % 59.25/59.25 & v5_membered(B) % 59.25/59.25 & v2_tops_1(B,A) ) ) ). % 59.25/59.25 % 59.25/59.25 fof(rc5_struct_0,axiom, % 59.25/59.25 ! [A] : % 59.25/59.25 ( ( ~ v3_struct_0(A) % 59.25/59.25 & l1_struct_0(A) ) % 59.25/59.25 => ? [B] : % 59.25/59.25 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 59.25/59.25 & ~ v1_xboole_0(B) ) ) ). % 59.25/59.25 % 59.25/59.25 fof(rc5_tops_1,axiom, % 59.25/59.25 ! [A] : % 59.25/59.25 ( ( v2_pre_topc(A) % 59.25/59.25 & l1_pre_topc(A) ) % 59.25/59.25 => ? [B] : % 59.25/59.25 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 59.25/59.25 & v1_xboole_0(B) % 59.25/59.25 & v3_pre_topc(B,A) % 59.25/59.25 & v4_pre_topc(B,A) % 59.25/59.25 & v1_membered(B) % 59.25/59.25 & v2_membered(B) % 59.25/59.25 & v3_membered(B) % 59.25/59.25 & v4_membered(B) % 59.25/59.25 & v5_membered(B) % 59.25/59.25 & v2_tops_1(B,A) % 59.25/59.26 & v3_tops_1(B,A) ) ) ). % 59.25/59.26 % 59.25/59.26 fof(rc6_pre_topc,axiom, % 59.25/59.26 ! [A] : % 59.25/59.26 ( ( v2_pre_topc(A) % 59.25/59.26 & l1_pre_topc(A) ) % 59.25/59.26 => ? [B] : % 59.25/59.26 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 59.25/59.26 & v4_pre_topc(B,A) ) ) ). % 59.25/59.26 % 59.25/59.26 fof(rc7_pre_topc,axiom, % 59.25/59.26 ! [A] : % 59.25/59.26 ( ( ~ v3_struct_0(A) % 59.25/59.26 & v2_pre_topc(A) % 59.25/59.26 & l1_pre_topc(A) ) % 59.25/59.26 => ? [B] : % 59.25/59.26 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 59.25/59.26 & ~ v1_xboole_0(B) % 59.25/59.26 & v4_pre_topc(B,A) ) ) ). % 59.25/59.26 % 59.25/59.26 fof(reflexivity_r1_tarski,axiom, % 59.25/59.26 ! [A,B] : r1_tarski(A,A) ). % 59.25/59.26 % 59.25/59.26 fof(t11_tsp_1,axiom, % 59.25/59.26 ! [A] : % 59.25/59.26 ( ( ~ v3_struct_0(A) % 59.25/59.26 & l1_pre_topc(A) ) % 59.25/59.26 => ! [B] : % 59.25/59.26 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 59.25/59.26 => ( v3_tex_2(B,A) % 59.25/59.26 => v1_tsp_1(B,A) ) ) ) ). % 59.25/59.26 % 59.25/59.26 fof(t1_subset,axiom, % 59.25/59.26 ! [A,B] : % 59.25/59.26 ( r2_hidden(A,B) % 59.25/59.26 => m1_subset_1(A,B) ) ). % 59.25/59.26 % 59.25/59.26 fof(t2_subset,axiom, % 59.25/59.26 ! [A,B] : % 59.25/59.26 ( m1_subset_1(A,B) % 59.25/59.26 => ( v1_xboole_0(B) % 59.25/59.26 | r2_hidden(A,B) ) ) ). % 59.25/59.26 % 59.25/59.26 fof(t35_tex_2,axiom, % 59.25/59.26 ! [A] : % 59.25/59.26 ( ( ~ v3_struct_0(A) % 59.25/59.26 & v2_pre_topc(A) % 59.25/59.26 & l1_pre_topc(A) ) % 59.25/59.26 => ! [B] : % 59.25/59.26 ( ( v1_xboole_0(B) % 59.25/59.26 & m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) ) % 59.25/59.26 => v3_tex_2(B,A) ) ) ). % 59.25/59.26 % 59.25/59.26 fof(t3_subset,axiom, % 59.25/59.26 ! [A,B] : % 59.25/59.26 ( m1_subset_1(A,k1_zfmisc_1(B)) % 59.25/59.26 <=> r1_tarski(A,B) ) ). % 59.25/59.26 % 59.25/59.26 fof(t4_subset,axiom, % 59.25/59.26 ! [A,B,C] : % 59.25/59.26 ( ( r2_hidden(A,B) % 59.25/59.26 & m1_subset_1(B,k1_zfmisc_1(C)) ) % 59.25/59.26 => m1_subset_1(A,C) ) ). % 59.25/59.26 % 59.25/59.26 fof(t5_subset,axiom, % 59.25/59.26 ! [A,B,C] : % 59.25/59.26 ~ ( r2_hidden(A,B) % 59.25/59.26 & m1_subset_1(B,k1_zfmisc_1(C)) % 59.25/59.26 & v1_xboole_0(C) ) ). % 59.25/59.26 % 59.25/59.26 fof(t6_boole,axiom, % 59.25/59.26 ! [A] : % 59.25/59.26 ( v1_xboole_0(A) % 59.25/59.26 => A = k1_xboole_0 ) ). % 59.25/59.26 % 59.25/59.26 fof(t7_boole,axiom, % 59.25/59.26 ! [A,B] : % 59.25/59.26 ~ ( r2_hidden(A,B) % 59.25/59.26 & v1_xboole_0(B) ) ). % 59.25/59.26 % 59.25/59.26 fof(t8_boole,axiom, % 59.25/59.26 ! [A,B] : % 59.25/59.26 ~ ( v1_xboole_0(A) % 59.25/59.26 & A != B % 59.25/59.26 & v1_xboole_0(B) ) ). % 59.25/59.26 % 59.25/59.26 fof(t9_tsp_2,axiom, % 59.25/59.26 ! [A] : % 59.25/59.26 ( ( ~ v3_struct_0(A) % 59.25/59.26 & v2_pre_topc(A) % 59.25/59.26 & l1_pre_topc(A) ) % 59.25/59.26 => ! [B] : % 59.25/59.26 ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) % 59.25/59.26 => ~ ( v1_tsp_1(B,A) % 59.25/59.26 & ! [C] : % 59.25/59.26 ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) % 59.25/59.26 => ~ ( r1_tarski(B,C) % 59.25/59.26 & v1_tsp_2(C,A) ) ) ) ) ) ). % 59.25/59.26 % 59.25/59.26 %------------------------------------------------------------------------------ % 59.25/59.26 %------------------------------------------- % 59.25/59.26 % Proof found % 59.25/59.26 % SZS status Theorem for theBenchmark % 59.25/59.26 % SZS output start Proof % 59.25/59.26 %ClaNum:208(EqnAxiom:54) % 59.25/59.26 %VarNum:519(SingletonVarNum:186) % 59.25/59.26 %MaxLitNum:6 % 59.25/59.26 %MaxfuncDepth:2 % 59.25/59.26 %SharedTerms:27 % 59.25/59.26 %goalClause: 55 56 75 187 % 59.25/59.26 %singleGoalClaCount:3 % 59.25/59.26 [55]P1(a1) % 59.25/59.26 [56]P2(a1) % 59.25/59.26 [57]P2(a10) % 59.25/59.26 [58]P3(a11) % 59.25/59.26 [59]P3(a12) % 59.25/59.26 [60]P9(a11) % 59.25/59.26 [61]P9(a12) % 59.25/59.26 [62]P16(a11) % 59.25/59.26 [63]P16(a12) % 59.25/59.26 [64]P18(a11) % 59.25/59.26 [65]P18(a12) % 59.25/59.26 [66]P23(a11) % 59.25/59.26 [67]P23(a12) % 59.25/59.26 [68]P10(a11) % 59.25/59.26 [69]P4(a13) % 59.25/59.26 [70]P4(a2) % 59.25/59.26 [75]~P19(a1) % 59.25/59.26 [76]~P19(a2) % 59.25/59.26 [77]~P10(a12) % 59.25/59.26 [72]P5(x721,x721) % 59.25/59.26 [71]P10(f15(x711)) % 59.25/59.26 [73]P6(f14(x731),x731) % 59.25/59.26 [74]P6(f15(x741),f20(x741)) % 59.25/59.26 [78]~P10(f20(x781)) % 59.25/59.26 [79]~P10(x791)+E(x791,a11) % 59.25/59.26 [80]~P9(x801)+P3(x801) % 59.25/59.26 [81]~P10(x811)+P3(x811) % 59.25/59.26 [82]~P16(x821)+P9(x821) % 59.25/59.26 [83]~P10(x831)+P9(x831) % 59.25/59.26 [84]~P18(x841)+P16(x841) % 59.25/59.26 [85]~P10(x851)+P16(x851) % 59.25/59.26 [86]~P23(x861)+P18(x861) % 59.25/59.26 [87]~P10(x871)+P18(x871) % 59.25/59.26 [88]~P10(x881)+P23(x881) % 59.25/59.26 [89]~P2(x891)+P4(x891) % 59.25/59.26 [91]~P4(x911)+P3(f18(x911)) % 59.25/59.26 [92]~P2(x921)+P3(f3(x921)) % 59.25/59.26 [93]~P4(x931)+P9(f18(x931)) % 59.25/59.26 [94]~P2(x941)+P9(f3(x941)) % 59.25/59.26 [95]~P4(x951)+P16(f18(x951)) % 59.25/59.26 [96]~P2(x961)+P16(f3(x961)) % 59.25/59.26 [97]~P4(x971)+P18(f18(x971)) % 59.25/59.26 [98]~P2(x981)+P18(f3(x981)) % 59.25/59.26 [99]~P4(x991)+P23(f18(x991)) % 59.25/59.26 [100]~P2(x1001)+P23(f3(x1001)) % 59.25/59.26 [101]~P4(x1011)+P10(f18(x1011)) % 59.25/59.26 [102]~P2(x1021)+P10(f3(x1021)) % 59.25/59.26 [103]P10(x1031)+~P10(f16(x1031)) % 59.25/59.26 [122]~P2(x1221)+P17(f3(x1221),x1221) % 59.25/59.26 [126]P10(x1261)+P6(f16(x1261),f20(x1261)) % 59.25/59.26 [177]~P4(x1771)+P6(f18(x1771),f20(f21(x1771))) % 59.25/59.26 [178]~P2(x1781)+P6(f3(x1781),f20(f21(x1781))) % 59.25/59.26 [187]~P12(x1871,a1)+~P6(x1871,f20(f21(a1))) % 59.25/59.26 [125]~P10(x1251)+~P7(x1252,x1251) % 59.25/59.26 [155]~P7(x1551,x1552)+P6(x1551,x1552) % 59.25/59.26 [176]~P7(x1762,x1761)+~P7(x1761,x1762) % 59.25/59.26 [160]~P5(x1601,x1602)+P6(x1601,f20(x1602)) % 59.25/59.26 [179]P5(x1791,x1792)+~P6(x1791,f20(x1792)) % 59.25/59.26 [105]~P1(x1051)+~P2(x1051)+P3(f18(x1051)) % 59.25/59.26 [106]~P1(x1061)+~P2(x1061)+P3(f5(x1061)) % 59.25/59.26 [108]~P1(x1081)+~P2(x1081)+P9(f18(x1081)) % 59.25/59.26 [109]~P1(x1091)+~P2(x1091)+P9(f5(x1091)) % 59.25/59.26 [111]~P1(x1111)+~P2(x1111)+P16(f18(x1111)) % 59.25/59.26 [112]~P1(x1121)+~P2(x1121)+P16(f5(x1121)) % 59.25/59.26 [114]~P1(x1141)+~P2(x1141)+P18(f18(x1141)) % 59.25/59.26 [115]~P1(x1151)+~P2(x1151)+P18(f5(x1151)) % 59.25/59.26 [117]~P1(x1171)+~P2(x1171)+P23(f18(x1171)) % 59.25/59.26 [118]~P1(x1181)+~P2(x1181)+P23(f5(x1181)) % 59.25/59.26 [120]~P1(x1201)+~P2(x1201)+P10(f18(x1201)) % 59.25/59.26 [121]~P1(x1211)+~P2(x1211)+P10(f5(x1211)) % 59.25/59.26 [123]~P4(x1231)+P19(x1231)+~P10(f21(x1231)) % 59.25/59.26 [124]~P4(x1241)+P19(x1241)+~P10(f6(x1241)) % 59.25/59.26 [142]~P1(x1421)+~P2(x1421)+P20(f18(x1421),x1421) % 59.25/59.26 [143]~P1(x1431)+~P2(x1431)+P20(f17(x1431),x1431) % 59.25/59.26 [144]~P1(x1441)+~P2(x1441)+P20(f19(x1441),x1441) % 59.25/59.26 [145]~P1(x1451)+~P2(x1451)+P20(f5(x1451),x1451) % 59.25/59.26 [147]~P1(x1471)+~P2(x1471)+P25(f18(x1471),x1471) % 59.25/59.26 [148]~P1(x1481)+~P2(x1481)+P25(f19(x1481),x1481) % 59.25/59.26 [149]~P1(x1491)+~P2(x1491)+P25(f5(x1491),x1491) % 59.25/59.26 [150]~P1(x1501)+~P2(x1501)+P25(f7(x1501),x1501) % 59.25/59.26 [151]~P1(x1511)+~P2(x1511)+P17(f5(x1511),x1511) % 59.25/59.26 [152]~P1(x1521)+~P2(x1521)+P21(f5(x1521),x1521) % 59.25/59.26 [180]~P4(x1801)+P19(x1801)+P6(f6(x1801),f20(f21(x1801))) % 59.25/59.26 [181]~P1(x1811)+~P2(x1811)+P6(f17(x1811),f20(f21(x1811))) % 59.25/59.26 [182]~P1(x1821)+~P2(x1821)+P6(f19(x1821),f20(f21(x1821))) % 59.25/59.26 [183]~P1(x1831)+~P2(x1831)+P6(f5(x1831),f20(f21(x1831))) % 59.25/59.26 [184]~P1(x1841)+~P2(x1841)+P6(f7(x1841),f20(f21(x1841))) % 59.25/59.26 [90]~P10(x902)+~P10(x901)+E(x901,x902) % 59.25/59.26 [127]~P6(x1271,x1272)+P14(x1271)+~P3(x1272) % 59.25/59.26 [128]~P6(x1281,x1282)+P14(x1281)+~P9(x1282) % 59.25/59.26 [129]~P6(x1291,x1292)+P14(x1291)+~P16(x1292) % 59.25/59.26 [130]~P6(x1301,x1302)+P14(x1301)+~P18(x1302) % 59.25/59.26 [131]~P6(x1311,x1312)+P14(x1311)+~P23(x1312) % 59.25/59.26 [132]~P6(x1321,x1322)+P15(x1321)+~P9(x1322) % 59.25/59.26 [133]~P6(x1331,x1332)+P15(x1331)+~P16(x1332) % 59.25/59.26 [134]~P6(x1341,x1342)+P15(x1341)+~P18(x1342) % 59.25/59.26 [135]~P6(x1351,x1352)+P15(x1351)+~P23(x1352) % 59.25/59.26 [136]~P6(x1361,x1362)+P11(x1361)+~P16(x1362) % 59.25/59.26 [137]~P6(x1371,x1372)+P11(x1371)+~P18(x1372) % 59.25/59.26 [138]~P6(x1381,x1382)+P11(x1381)+~P23(x1382) % 59.25/59.26 [139]~P6(x1391,x1392)+P8(x1391)+~P18(x1392) % 59.25/59.26 [140]~P6(x1401,x1402)+P8(x1401)+~P23(x1402) % 59.25/59.26 [141]~P6(x1411,x1412)+P24(x1411)+~P23(x1412) % 59.25/59.26 [159]~P6(x1592,x1591)+P10(x1591)+P7(x1592,x1591) % 59.25/59.26 [161]P3(x1611)+~P3(x1612)+~P6(x1611,f20(x1612)) % 59.25/59.26 [162]P3(x1621)+~P9(x1622)+~P6(x1621,f20(x1622)) % 59.25/59.26 [163]P3(x1631)+~P16(x1632)+~P6(x1631,f20(x1632)) % 59.25/59.26 [164]P3(x1641)+~P18(x1642)+~P6(x1641,f20(x1642)) % 59.25/59.26 [165]P3(x1651)+~P23(x1652)+~P6(x1651,f20(x1652)) % 59.25/59.26 [166]P9(x1661)+~P9(x1662)+~P6(x1661,f20(x1662)) % 59.25/59.26 [167]P9(x1671)+~P16(x1672)+~P6(x1671,f20(x1672)) % 59.25/59.26 [168]P9(x1681)+~P18(x1682)+~P6(x1681,f20(x1682)) % 59.25/59.26 [169]P9(x1691)+~P23(x1692)+~P6(x1691,f20(x1692)) % 59.25/59.26 [170]P16(x1701)+~P16(x1702)+~P6(x1701,f20(x1702)) % 59.25/59.26 [171]P16(x1711)+~P18(x1712)+~P6(x1711,f20(x1712)) % 59.25/59.26 [172]P16(x1721)+~P23(x1722)+~P6(x1721,f20(x1722)) % 59.25/59.26 [173]P18(x1731)+~P18(x1732)+~P6(x1731,f20(x1732)) % 59.25/59.26 [174]P18(x1741)+~P23(x1742)+~P6(x1741,f20(x1742)) % 59.25/59.26 [175]P23(x1751)+~P23(x1752)+~P6(x1751,f20(x1752)) % 59.25/59.26 [188]~P10(x1881)+~P7(x1882,x1883)+~P6(x1883,f20(x1881)) % 59.25/59.26 [189]P6(x1891,x1892)+~P7(x1891,x1893)+~P6(x1893,f20(x1892)) % 59.25/59.26 [153]~P1(x1531)+~P2(x1531)+P19(x1531)+~P10(f4(x1531)) % 59.25/59.26 [154]~P1(x1541)+~P2(x1541)+P19(x1541)+~P10(f8(x1541)) % 59.25/59.26 [156]~P1(x1561)+~P2(x1561)+P19(x1561)+P20(f4(x1561),x1561) % 59.25/59.26 [157]~P1(x1571)+~P2(x1571)+P19(x1571)+P25(f4(x1571),x1571) % 59.25/59.26 [158]~P1(x1581)+~P2(x1581)+P19(x1581)+P25(f8(x1581),x1581) % 59.25/59.26 [185]~P1(x1851)+~P2(x1851)+P19(x1851)+P6(f4(x1851),f20(f21(x1851))) % 59.25/59.26 [186]~P1(x1861)+~P2(x1861)+P19(x1861)+P6(f8(x1861),f20(f21(x1861))) % 59.25/59.26 [190]~P2(x1902)+~P10(x1901)+P17(x1901,x1902)+~P6(x1901,f20(f21(x1902))) % 59.25/59.26 [191]~P1(x1912)+~P2(x1912)+~P10(x1911)+P20(x1911,x1912)+~P6(x1911,f20(f21(x1912))) % 59.25/59.26 [192]~P1(x1922)+~P2(x1922)+~P10(x1921)+P25(x1921,x1922)+~P6(x1921,f20(f21(x1922))) % 59.25/59.26 [193]~P1(x1932)+~P2(x1932)+~P10(x1931)+P21(x1931,x1932)+~P6(x1931,f20(f21(x1932))) % 59.25/59.26 [195]~P2(x1951)+~P22(x1952,x1951)+P19(x1951)+P13(x1952,x1951)+~P6(x1952,f20(f21(x1951))) % 59.25/59.26 [196]~P1(x1962)+~P2(x1962)+~P21(x1961,x1962)+P17(x1961,x1962)+~P6(x1961,f20(f21(x1962))) % 59.25/59.26 [194]~P1(x1941)+~P2(x1941)+~P10(x1942)+P19(x1941)+P22(x1942,x1941)+~P6(x1942,f20(f21(x1941))) % 59.25/59.26 [197]~P2(x1972)+~P20(x1971,x1972)+~P21(x1971,x1972)+P3(x1971)+~P1(x1972)+~P6(x1971,f20(f21(x1972))) % 59.25/59.26 [198]~P2(x1982)+~P20(x1981,x1982)+~P21(x1981,x1982)+P9(x1981)+~P1(x1982)+~P6(x1981,f20(f21(x1982))) % 59.25/59.26 [199]~P2(x1992)+~P20(x1991,x1992)+~P21(x1991,x1992)+P16(x1991)+~P1(x1992)+~P6(x1991,f20(f21(x1992))) % 59.25/59.26 [200]~P2(x2002)+~P20(x2001,x2002)+~P21(x2001,x2002)+P18(x2001)+~P1(x2002)+~P6(x2001,f20(f21(x2002))) % 59.25/59.26 [201]~P2(x2012)+~P20(x2011,x2012)+~P21(x2011,x2012)+P23(x2011)+~P1(x2012)+~P6(x2011,f20(f21(x2012))) % 59.25/59.26 [202]~P2(x2022)+~P20(x2021,x2022)+~P21(x2021,x2022)+P10(x2021)+~P1(x2022)+~P6(x2021,f20(f21(x2022))) % 59.25/59.26 [203]~P1(x2032)+~P2(x2032)+~P20(x2031,x2032)+~P21(x2031,x2032)+P25(x2031,x2032)+~P6(x2031,f20(f21(x2032))) % 59.25/59.26 [205]~P1(x2052)+~P2(x2052)+~P25(x2051,x2052)+~P17(x2051,x2052)+P21(x2051,x2052)+~P6(x2051,f20(f21(x2052))) % 59.25/59.26 [206]~P1(x2061)+~P2(x2061)+~P13(x2062,x2061)+P19(x2061)+P5(x2062,f9(x2061,x2062))+~P6(x2062,f20(f21(x2061))) % 59.25/59.26 [207]~P1(x2071)+~P2(x2071)+~P13(x2072,x2071)+P19(x2071)+P12(f9(x2071,x2072),x2071)+~P6(x2072,f20(f21(x2071))) % 59.25/59.26 [208]~P1(x2081)+~P2(x2081)+~P13(x2082,x2081)+P19(x2081)+~P6(x2082,f20(f21(x2081)))+P6(f9(x2081,x2082),f20(f21(x2081))) % 59.25/59.26 %EqnAxiom % 59.25/59.26 [1]E(x11,x11) % 59.25/59.26 [2]E(x22,x21)+~E(x21,x22) % 59.25/59.26 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 59.25/59.26 [4]~E(x41,x42)+E(f15(x41),f15(x42)) % 59.25/59.26 [5]~E(x51,x52)+E(f14(x51),f14(x52)) % 59.25/59.26 [6]~E(x61,x62)+E(f20(x61),f20(x62)) % 59.25/59.26 [7]~E(x71,x72)+E(f21(x71),f21(x72)) % 59.25/59.26 [8]~E(x81,x82)+E(f4(x81),f4(x82)) % 59.25/59.26 [9]~E(x91,x92)+E(f18(x91),f18(x92)) % 59.25/59.26 [10]~E(x101,x102)+E(f3(x101),f3(x102)) % 59.25/59.26 [11]~E(x111,x112)+E(f17(x111),f17(x112)) % 59.25/59.26 [12]~E(x121,x122)+E(f19(x121),f19(x122)) % 59.25/59.26 [13]~E(x131,x132)+E(f5(x131),f5(x132)) % 59.25/59.26 [14]~E(x141,x142)+E(f9(x141,x143),f9(x142,x143)) % 59.25/59.26 [15]~E(x151,x152)+E(f9(x153,x151),f9(x153,x152)) % 59.25/59.26 [16]~E(x161,x162)+E(f6(x161),f6(x162)) % 59.25/59.26 [17]~E(x171,x172)+E(f16(x171),f16(x172)) % 59.25/59.26 [18]~E(x181,x182)+E(f7(x181),f7(x182)) % 59.25/59.26 [19]~E(x191,x192)+E(f8(x191),f8(x192)) % 59.25/59.26 [20]~P1(x201)+P1(x202)+~E(x201,x202) % 59.25/59.26 [21]~P2(x211)+P2(x212)+~E(x211,x212) % 59.25/59.26 [22]P20(x222,x223)+~E(x221,x222)+~P20(x221,x223) % 59.25/59.26 [23]P20(x233,x232)+~E(x231,x232)+~P20(x233,x231) % 59.25/59.26 [24]~P3(x241)+P3(x242)+~E(x241,x242) % 59.25/59.26 [25]P5(x252,x253)+~E(x251,x252)+~P5(x251,x253) % 59.25/59.26 [26]P5(x263,x262)+~E(x261,x262)+~P5(x263,x261) % 59.25/59.26 [27]~P9(x271)+P9(x272)+~E(x271,x272) % 59.25/59.26 [28]P6(x282,x283)+~E(x281,x282)+~P6(x281,x283) % 59.25/59.26 [29]P6(x293,x292)+~E(x291,x292)+~P6(x293,x291) % 59.25/59.26 [30]~P16(x301)+P16(x302)+~E(x301,x302) % 59.25/59.26 [31]~P19(x311)+P19(x312)+~E(x311,x312) % 59.25/59.26 [32]~P18(x321)+P18(x322)+~E(x321,x322) % 59.25/59.26 [33]~P15(x331)+P15(x332)+~E(x331,x332) % 59.25/59.26 [34]~P23(x341)+P23(x342)+~E(x341,x342) % 59.25/59.26 [35]~P10(x351)+P10(x352)+~E(x351,x352) % 59.25/59.26 [36]~P4(x361)+P4(x362)+~E(x361,x362) % 59.25/59.26 [37]~P11(x371)+P11(x372)+~E(x371,x372) % 59.25/59.26 [38]P21(x382,x383)+~E(x381,x382)+~P21(x381,x383) % 59.25/59.26 [39]P21(x393,x392)+~E(x391,x392)+~P21(x393,x391) % 59.25/59.26 [40]P22(x402,x403)+~E(x401,x402)+~P22(x401,x403) % 59.25/59.26 [41]P22(x413,x412)+~E(x411,x412)+~P22(x413,x411) % 59.25/59.26 [42]P13(x422,x423)+~E(x421,x422)+~P13(x421,x423) % 59.25/59.26 [43]P13(x433,x432)+~E(x431,x432)+~P13(x433,x431) % 59.25/59.26 [44]P17(x442,x443)+~E(x441,x442)+~P17(x441,x443) % 59.25/59.26 [45]P17(x453,x452)+~E(x451,x452)+~P17(x453,x451) % 59.25/59.26 [46]P25(x462,x463)+~E(x461,x462)+~P25(x461,x463) % 59.25/59.26 [47]P25(x473,x472)+~E(x471,x472)+~P25(x473,x471) % 59.25/59.26 [48]~P14(x481)+P14(x482)+~E(x481,x482) % 59.25/59.26 [49]~P24(x491)+P24(x492)+~E(x491,x492) % 59.25/59.26 [50]P7(x502,x503)+~E(x501,x502)+~P7(x501,x503) % 59.25/59.26 [51]P7(x513,x512)+~E(x511,x512)+~P7(x513,x511) % 59.25/59.26 [52]~P8(x521)+P8(x522)+~E(x521,x522) % 59.25/59.26 [53]P12(x532,x533)+~E(x531,x532)+~P12(x531,x533) % 59.25/59.26 [54]P12(x543,x542)+~E(x541,x542)+~P12(x543,x541) % 59.25/59.26 % 59.25/59.26 %------------------------------------------- % 59.25/59.27 cnf(209,plain, % 59.25/59.27 (~P12(f15(f21(a1)),a1)), % 59.25/59.27 inference(scs_inference,[],[74,187])). % 59.25/59.27 cnf(210,plain, % 59.25/59.27 (P6(f15(x2101),f20(x2101))), % 59.25/59.27 inference(rename_variables,[],[74])). % 59.25/59.27 cnf(212,plain, % 59.25/59.27 (~P7(x2121,a11)), % 59.25/59.27 inference(scs_inference,[],[74,68,187,125])). % 59.25/59.27 cnf(214,plain, % 59.25/59.27 (P5(f14(f20(x2141)),x2141)), % 59.25/59.27 inference(scs_inference,[],[73,74,68,187,125,179])). % 59.25/59.27 cnf(215,plain, % 59.25/59.27 (P6(f14(x2151),x2151)), % 59.25/59.27 inference(rename_variables,[],[73])). % 59.25/59.27 cnf(217,plain, % 59.25/59.27 (P7(f14(a12),a12)), % 59.25/59.27 inference(scs_inference,[],[73,215,74,68,77,187,125,179,159])). % 59.25/59.27 cnf(218,plain, % 59.25/59.27 (P6(f14(x2181),x2181)), % 59.25/59.27 inference(rename_variables,[],[73])). % 59.25/59.27 cnf(221,plain, % 59.25/59.27 (P6(f14(x2211),x2211)), % 59.25/59.27 inference(rename_variables,[],[73])). % 59.25/59.27 cnf(224,plain, % 59.25/59.27 (P6(f15(x2241),f20(x2241))), % 59.25/59.27 inference(rename_variables,[],[74])). % 59.25/59.27 cnf(227,plain, % 59.25/59.27 (P6(f14(x2271),x2271)), % 59.25/59.27 inference(rename_variables,[],[73])). % 59.25/59.27 cnf(230,plain, % 59.25/59.27 (P6(f15(x2301),f20(x2301))), % 59.25/59.27 inference(rename_variables,[],[74])). % 59.25/59.27 cnf(233,plain, % 59.25/59.27 (P6(f14(x2331),x2331)), % 59.25/59.27 inference(rename_variables,[],[73])). % 59.25/59.27 cnf(236,plain, % 59.25/59.27 (P6(f15(x2361),f20(x2361))), % 59.25/59.27 inference(rename_variables,[],[74])). % 59.25/59.27 cnf(239,plain, % 59.25/59.27 (P6(f14(x2391),x2391)), % 59.25/59.27 inference(rename_variables,[],[73])). % 59.25/59.27 cnf(241,plain, % 59.25/59.27 (P18(f15(a11))), % 59.25/59.27 inference(scs_inference,[],[73,215,218,221,227,233,74,210,224,230,236,58,60,62,64,66,68,77,187,125,179,159,161,162,166,167,170,171,173,174])). % 59.25/59.27 cnf(242,plain, % 59.25/59.27 (P6(f15(x2421),f20(x2421))), % 59.25/59.27 inference(rename_variables,[],[74])). % 59.25/59.27 cnf(245,plain, % 59.25/59.27 (P6(f14(x2451),x2451)), % 59.25/59.27 inference(rename_variables,[],[73])). % 59.25/59.27 cnf(247,plain, % 59.25/59.27 (~P7(x2471,f14(f20(a11)))), % 59.25/59.27 inference(scs_inference,[],[73,215,218,221,227,233,239,245,74,210,224,230,236,58,60,62,64,66,68,77,187,125,179,159,161,162,166,167,170,171,173,174,175,188])). % 59.25/59.27 cnf(248,plain, % 59.25/59.27 (P6(f14(x2481),x2481)), % 59.25/59.27 inference(rename_variables,[],[73])). % 59.25/59.27 cnf(250,plain, % 59.25/59.27 (~E(a12,a11)), % 59.25/59.27 inference(scs_inference,[],[73,215,218,221,227,233,239,245,74,210,224,230,236,58,60,62,64,66,68,77,187,125,179,159,161,162,166,167,170,171,173,174,175,188,51])). % 59.25/59.27 cnf(251,plain, % 59.25/59.27 (P17(f15(f21(a1)),a1)), % 59.25/59.27 inference(scs_inference,[],[56,73,215,218,221,227,233,239,245,74,210,224,230,236,242,58,60,62,64,66,68,77,71,187,125,179,159,161,162,166,167,170,171,173,174,175,188,51,190])). % 59.25/59.27 cnf(252,plain, % 59.25/59.27 (P6(f15(x2521),f20(x2521))), % 59.25/59.27 inference(rename_variables,[],[74])). % 59.25/59.27 cnf(253,plain, % 59.25/59.27 (P10(f15(x2531))), % 59.25/59.27 inference(rename_variables,[],[71])). % 59.25/59.27 cnf(255,plain, % 59.25/59.27 (P20(f15(f21(a1)),a1)), % 59.25/59.27 inference(scs_inference,[],[55,56,73,215,218,221,227,233,239,245,74,210,224,230,236,242,252,58,60,62,64,66,68,77,71,253,187,125,179,159,161,162,166,167,170,171,173,174,175,188,51,190,191])). % 59.25/59.27 cnf(256,plain, % 59.25/59.27 (P6(f15(x2561),f20(x2561))), % 59.25/59.27 inference(rename_variables,[],[74])). % 59.25/59.27 cnf(257,plain, % 59.25/59.27 (P10(f15(x2571))), % 59.25/59.27 inference(rename_variables,[],[71])). % 59.25/59.27 cnf(259,plain, % 59.25/59.27 (P25(f15(f21(a1)),a1)), % 59.25/59.27 inference(scs_inference,[],[55,56,73,215,218,221,227,233,239,245,74,210,224,230,236,242,252,256,58,60,62,64,66,68,77,71,253,257,187,125,179,159,161,162,166,167,170,171,173,174,175,188,51,190,191,192])). % 59.25/59.27 cnf(260,plain, % 59.25/59.27 (P6(f15(x2601),f20(x2601))), % 59.25/59.27 inference(rename_variables,[],[74])). % 59.25/59.27 cnf(261,plain, % 59.25/59.27 (P10(f15(x2611))), % 59.25/59.27 inference(rename_variables,[],[71])). % 59.25/59.27 cnf(263,plain, % 59.25/59.27 (P21(f15(f21(a1)),a1)), % 59.25/59.27 inference(scs_inference,[],[55,56,73,215,218,221,227,233,239,245,74,210,224,230,236,242,252,256,260,58,60,62,64,66,68,77,71,253,257,261,187,125,179,159,161,162,166,167,170,171,173,174,175,188,51,190,191,192,193])). % 59.25/59.27 cnf(264,plain, % 59.25/59.27 (P6(f15(x2641),f20(x2641))), % 59.25/59.27 inference(rename_variables,[],[74])). % 59.25/59.27 cnf(265,plain, % 59.25/59.27 (P10(f15(x2651))), % 59.25/59.27 inference(rename_variables,[],[71])). % 59.25/59.27 cnf(267,plain, % 59.25/59.27 (P22(f15(f21(a1)),a1)), % 59.25/59.27 inference(scs_inference,[],[55,56,75,73,215,218,221,227,233,239,245,74,210,224,230,236,242,252,256,260,264,58,60,62,64,66,68,77,71,253,257,261,265,187,125,179,159,161,162,166,167,170,171,173,174,175,188,51,190,191,192,193,194])). % 59.25/59.27 cnf(268,plain, % 59.25/59.27 (P6(f15(x2681),f20(x2681))), % 59.25/59.27 inference(rename_variables,[],[74])). % 59.25/59.27 cnf(272,plain, % 59.25/59.27 (P6(f15(x2721),f20(x2721))), % 59.25/59.27 inference(rename_variables,[],[74])). % 59.25/59.27 cnf(275,plain, % 59.25/59.27 (P6(f15(x2751),f20(x2751))), % 59.25/59.27 inference(rename_variables,[],[74])). % 59.25/59.27 cnf(278,plain, % 59.25/59.27 (P6(f15(x2781),f20(x2781))), % 59.25/59.27 inference(rename_variables,[],[74])). % 59.25/59.27 cnf(281,plain, % 59.25/59.27 (P6(f15(x2811),f20(x2811))), % 59.25/59.27 inference(rename_variables,[],[74])). % 59.25/59.27 cnf(284,plain, % 59.25/59.27 (P6(f15(x2841),f20(x2841))), % 59.25/59.27 inference(rename_variables,[],[74])). % 59.25/59.27 cnf(289,plain, % 59.25/59.27 (P6(f14(x2891),x2891)), % 59.25/59.27 inference(rename_variables,[],[73])). % 59.25/59.27 cnf(291,plain, % 59.25/59.27 (P13(f15(f21(a1)),a1)), % 59.25/59.27 inference(scs_inference,[],[55,56,75,73,215,218,221,227,233,239,245,248,74,210,224,230,236,242,252,256,260,264,268,272,275,278,281,284,58,60,62,64,66,68,77,71,253,257,261,265,187,125,179,159,161,162,166,167,170,171,173,174,175,188,51,190,191,192,193,194,197,198,199,200,201,176,189,195])). % 59.25/59.27 cnf(295,plain, % 59.25/59.27 (P6(f14(x2951),x2952)+~E(x2951,x2952)), % 59.25/59.27 inference(scs_inference,[],[55,56,75,73,215,218,221,227,233,239,245,248,289,74,210,224,230,236,242,252,256,260,264,268,272,275,278,281,284,58,60,62,64,66,68,77,71,253,257,261,265,187,125,179,159,161,162,166,167,170,171,173,174,175,188,51,190,191,192,193,194,197,198,199,200,201,176,189,195,28,29])). % 59.25/59.27 cnf(306,plain, % 59.25/59.27 (~P7(x3061,f15(x3062))), % 59.25/59.27 inference(scs_inference,[],[71,125])). % 59.25/59.27 cnf(308,plain, % 59.25/59.27 (P5(f15(x3081),x3081)), % 59.25/59.27 inference(scs_inference,[],[74,71,125,179])). % 59.25/59.27 cnf(310,plain, % 59.25/59.27 (P7(f14(f20(x3101)),f20(x3101))), % 59.25/59.27 inference(scs_inference,[],[73,74,78,71,125,179,159])). % 59.25/59.27 cnf(318,plain, % 59.25/59.27 (P17(x3181,a1)+~E(f15(f21(a1)),x3181)), % 59.25/59.27 inference(scs_inference,[],[251,263,73,74,247,217,78,71,125,179,159,51,176,39,44])). % 59.25/59.27 cnf(320,plain, % 59.25/59.27 (P25(x3201,a1)+~E(f15(f21(a1)),x3201)), % 59.25/59.27 inference(scs_inference,[],[251,259,263,73,74,247,217,78,71,125,179,159,51,176,39,44,45,46])). % 59.25/59.27 cnf(329,plain, % 59.25/59.28 (P7(f15(x3291),f20(x3291))), % 59.25/59.28 inference(scs_inference,[],[74,78,159])). % 59.25/59.28 cnf(334,plain, % 59.25/59.28 (P5(f15(x3341),x3342)+~E(x3341,x3342)), % 59.25/59.28 inference(scs_inference,[],[74,308,310,306,78,159,51,26])). % 59.25/59.28 cnf(335,plain, % 59.25/59.28 (P22(x3351,a1)+~E(f15(f21(a1)),x3351)), % 59.25/59.28 inference(scs_inference,[],[74,267,308,310,306,78,159,51,26,40])). % 59.25/59.28 cnf(337,plain, % 59.25/59.28 (P13(x3371,a1)+~E(f15(f21(a1)),x3371)), % 59.25/59.28 inference(scs_inference,[],[74,267,291,308,310,306,78,159,51,26,40,41,42])). % 59.25/59.28 cnf(339,plain, % 59.25/59.28 (P7(x3391,f20(x3392))+~E(f14(f20(x3392)),x3391)), % 59.25/59.28 inference(scs_inference,[],[74,267,291,308,310,306,78,159,51,26,40,41,42,43,50])). % 59.25/59.28 cnf(348,plain, % 59.25/59.28 (P20(x3481,a1)+~E(f15(f21(a1)),x3481)), % 59.25/59.28 inference(scs_inference,[],[255,310,212,51,22])). % 59.25/59.28 cnf(349,plain, % 59.25/59.28 (P21(x3491,a1)+~E(f15(f21(a1)),x3491)), % 59.25/59.28 inference(scs_inference,[],[255,263,310,212,51,22,38])). % 59.25/59.28 cnf(351,plain, % 59.25/59.28 (P6(x3511,f20(x3512))+~E(f15(x3512),x3511)), % 59.25/59.28 inference(scs_inference,[],[74,255,263,310,212,51,22,38,23,28])). % 59.25/59.28 cnf(392,plain, % 59.25/59.28 (P7(x3921,f20(x3922))+~E(f15(x3922),x3921)), % 59.25/59.28 inference(scs_inference,[],[329,308,214,25,26,50])). % 59.25/59.28 cnf(400,plain, % 59.25/59.28 (P5(x4001,x4002)+~E(x4002,x4001)), % 59.25/59.28 inference(scs_inference,[],[72,25])). % 59.25/59.28 cnf(401,plain, % 59.25/59.28 (P5(x4011,x4012)+~E(x4011,x4012)), % 59.25/59.28 inference(scs_inference,[],[72,25,26])). % 59.25/59.28 cnf(1529,plain, % 59.25/59.28 (E(f18(a13),a11)), % 59.25/59.28 inference(scs_inference,[],[69,79,101])). % 59.25/59.28 cnf(1532,plain, % 59.25/59.28 (P5(a11,f18(a13))), % 59.25/59.28 inference(scs_inference,[],[1529,295,334,400])). % 59.25/59.28 cnf(1533,plain, % 59.25/59.28 (P5(f18(a13),a11)), % 59.25/59.28 inference(scs_inference,[],[1529,295,334,400,401])). % 59.25/59.28 cnf(1534,plain, % 59.25/59.28 (E(a11,f18(a13))), % 59.25/59.28 inference(scs_inference,[],[1529,295,334,400,401,2])). % 59.25/59.28 cnf(1540,plain, % 59.25/59.28 (P10(f18(a13))), % 59.25/59.28 inference(scs_inference,[],[1529,68,58,60,62,64,66,295,334,400,401,2,24,27,30,32,34,35])). % 59.25/59.28 cnf(2409,plain, % 59.25/59.28 (P23(f18(a1))), % 59.25/59.28 inference(scs_inference,[],[56,99,89])). % 59.25/59.28 cnf(2817,plain, % 59.25/59.28 (~P10(f16(a12))), % 59.25/59.28 inference(scs_inference,[],[217,103,125])). % 59.25/59.28 cnf(2818,plain, % 59.25/59.28 (P7(f14(f16(a12)),f16(a12))), % 59.25/59.28 inference(scs_inference,[],[73,2817,159])). % 59.25/59.28 cnf(2849,plain, % 59.25/59.28 (~E(f16(a12),f15(x28491))), % 59.25/59.28 inference(scs_inference,[],[2818,306,51])). % 59.25/59.28 cnf(2881,plain, % 59.25/59.28 (P17(x28811,a10)+~E(f15(f21(a10)),x28811)), % 59.25/59.28 inference(scs_inference,[],[57,74,71,190,44])). % 59.25/59.28 cnf(2893,plain, % 59.25/59.28 (P25(f15(f21(a10)),a10)+~P1(a10)), % 59.25/59.28 inference(scs_inference,[],[57,74,71,192])). % 59.25/59.28 cnf(6428,plain, % 59.25/59.28 (P6(f16(a12),f20(a12))), % 59.25/59.28 inference(scs_inference,[],[250,126,79])). % 59.25/59.28 cnf(6441,plain, % 59.25/59.28 (P6(f14(f16(a12)),a12)), % 59.25/59.28 inference(scs_inference,[],[6428,2818,65,67,179,165,171,168,174,175,189])). % 59.25/59.28 cnf(6595,plain, % 59.25/59.28 (P6(f15(f18(a13)),f20(a11))), % 59.25/59.28 inference(scs_inference,[],[1529,160,334])). % 59.25/59.28 cnf(6628,plain, % 59.25/59.28 (P6(x66281,f20(a11))+~E(f15(f18(a13)),x66281)), % 59.25/59.28 inference(scs_inference,[],[6595,28])). % 59.25/59.28 cnf(6765,plain, % 59.25/59.28 (P25(x67651,a10)+~E(f15(f21(a10)),x67651)+~P1(a10)), % 59.25/59.28 inference(scs_inference,[],[2893,46])). % 59.25/59.28 cnf(7342,plain, % 59.25/59.28 (P7(f14(f16(a12)),a12)), % 59.25/59.28 inference(scs_inference,[],[6441,77,159])). % 59.25/59.28 cnf(7356,plain, % 59.25/59.28 (P16(f15(a12))), % 59.25/59.28 inference(scs_inference,[],[63,74,170])). % 59.25/59.28 cnf(7773,plain, % 59.25/59.28 (E(f15(a11),f15(f18(a13)))), % 59.25/59.28 inference(scs_inference,[],[1529,4,2])). % 59.25/59.28 cnf(7774,plain, % 59.25/59.28 (P7(f15(f18(a13)),f20(a11))), % 59.25/59.28 inference(scs_inference,[],[7773,392])). % 59.25/59.28 cnf(7775,plain, % 59.25/59.28 (E(f15(f18(a13)),f15(a11))), % 59.25/59.28 inference(scs_inference,[],[7773,392,2])). % 59.25/59.28 cnf(7804,plain, % 59.25/59.28 (P7(f15(a11),f20(f18(a13)))), % 59.25/59.28 inference(scs_inference,[],[7775,392])). % 59.25/59.28 cnf(10298,plain, % 59.25/59.28 (~P7(f20(a12),f16(a12))), % 59.25/59.28 inference(scs_inference,[],[6428,78,159,176])). % 59.25/59.28 cnf(10300,plain, % 59.25/59.28 (~E(f14(f16(a12)),f20(a12))), % 59.25/59.28 inference(scs_inference,[],[6428,2818,78,159,176,50])). % 59.25/59.28 cnf(10306,plain, % 59.25/59.28 (~P6(f20(a12),f16(a12))), % 59.25/59.28 inference(scs_inference,[],[2817,10298,159])). % 59.25/59.28 cnf(15526,plain, % 59.25/59.28 (E(f20(a11),f20(f18(a13)))), % 59.25/59.28 inference(scs_inference,[],[1529,6,2])). % 59.25/59.28 cnf(15527,plain, % 59.25/59.28 (P6(f14(f20(a11)),f20(f18(a13)))), % 59.25/59.28 inference(scs_inference,[],[15526,295])). % 59.25/59.28 cnf(15528,plain, % 59.25/59.28 (P5(f15(f20(a11)),f20(f18(a13)))), % 59.25/59.28 inference(scs_inference,[],[15526,295,334])). % 59.25/59.28 cnf(15529,plain, % 59.25/59.28 (E(f20(f18(a13)),f20(a11))), % 59.25/59.28 inference(scs_inference,[],[15526,295,334,2])). % 59.25/59.28 cnf(15564,plain, % 59.25/59.28 (P6(x155641,f20(f18(a13)))+~E(f14(f20(a11)),x155641)), % 59.25/59.28 inference(scs_inference,[],[15527,15526,15528,25,20,28])). % 59.25/59.28 cnf(15578,plain, % 59.25/59.28 (~P9(f20(a11))+P9(f20(f18(a13)))), % 59.25/59.28 inference(scs_inference,[],[15526,15529,21,34,31,27])). % 59.25/59.28 cnf(18906,plain, % 59.25/59.28 (P3(f20(f18(a13)))+~P9(f20(a11))), % 59.25/59.28 inference(scs_inference,[],[15578,80])). % 59.25/59.28 cnf(20327,plain, % 59.25/59.28 (P14(f14(f20(a11)))+~P9(f20(a11))), % 59.25/59.28 inference(scs_inference,[],[15527,18906,127])). % 59.25/59.28 cnf(20871,plain, % 59.25/59.28 (~E(f14(f20(a11)),x208711)+P14(x208711)+~P9(f20(a11))), % 59.25/59.28 inference(scs_inference,[],[20327,48])). % 59.25/59.28 cnf(25096,plain, % 59.25/59.28 (P18(f15(x250961))), % 59.25/59.28 inference(scs_inference,[],[71,87])). % 59.25/59.28 cnf(25100,plain, % 59.25/59.28 (P3(f3(a10))), % 59.25/59.28 inference(scs_inference,[],[70,71,57,87,91,92])). % 59.25/59.28 cnf(25102,plain, % 59.25/59.28 (P9(f18(a2))), % 59.25/59.28 inference(scs_inference,[],[70,71,57,87,91,92,93])). % 59.25/59.28 cnf(25104,plain, % 59.25/59.28 (P9(f3(a10))), % 59.25/59.28 inference(scs_inference,[],[70,71,57,87,91,92,93,94])). % 59.25/59.28 cnf(25106,plain, % 59.25/59.28 (P16(f18(a2))), % 59.25/59.28 inference(scs_inference,[],[70,71,57,87,91,92,93,94,95])). % 59.25/59.28 cnf(25110,plain, % 59.25/59.28 (P18(f18(a2))), % 59.25/59.28 inference(scs_inference,[],[70,71,57,87,91,92,93,94,95,96,97])). % 59.25/59.28 cnf(25114,plain, % 59.25/59.28 (P23(f18(a2))), % 59.25/59.28 inference(scs_inference,[],[70,71,57,87,91,92,93,94,95,96,97,98,99])). % 59.25/59.28 cnf(25116,plain, % 59.25/59.28 (P23(f3(a10))), % 59.25/59.28 inference(scs_inference,[],[70,71,57,87,91,92,93,94,95,96,97,98,99,100])). % 59.25/59.28 cnf(25118,plain, % 59.25/59.28 (P10(f18(a2))), % 59.25/59.28 inference(scs_inference,[],[70,71,57,87,91,92,93,94,95,96,97,98,99,100,101])). % 59.25/59.28 cnf(25120,plain, % 59.25/59.28 (P10(f3(a10))), % 59.25/59.28 inference(scs_inference,[],[70,71,57,87,91,92,93,94,95,96,97,98,99,100,101,102])). % 59.25/59.28 cnf(25122,plain, % 59.25/59.28 (~P10(f16(f16(a12)))), % 59.25/59.28 inference(scs_inference,[],[70,2817,71,57,87,91,92,93,94,95,96,97,98,99,100,101,102,103])). % 59.25/59.28 cnf(25138,plain, % 59.25/59.28 (P6(f18(a2),f20(f21(a2)))), % 59.25/59.28 inference(scs_inference,[],[70,1532,2817,1534,71,57,87,91,92,93,94,95,96,97,98,99,100,101,102,103,122,160,8,9,10,11,12,13,16,17,18,19,177])). % 59.25/59.28 cnf(25144,plain, % 59.25/59.28 (E(f15(x251441),a11)), % 59.25/59.28 inference(scs_inference,[],[70,1532,2817,1534,71,57,87,91,92,93,94,95,96,97,98,99,100,101,102,103,122,160,8,9,10,11,12,13,16,17,18,19,177,178,14,15,79])). % 59.25/59.28 cnf(25150,plain, % 59.25/59.28 (P23(f15(x251501))), % 59.25/59.28 inference(scs_inference,[],[70,1532,2817,1534,71,57,87,91,92,93,94,95,96,97,98,99,100,101,102,103,122,160,8,9,10,11,12,13,16,17,18,19,177,178,14,15,79,83,80,88])). % 59.25/59.28 cnf(25154,plain, % 59.25/59.28 (P4(a10)), % 59.25/59.28 inference(scs_inference,[],[70,1532,2817,1534,71,57,87,91,92,93,94,95,96,97,98,99,100,101,102,103,122,160,8,9,10,11,12,13,16,17,18,19,177,178,14,15,79,83,80,88,85,89])). % 59.25/59.28 cnf(25158,plain, % 59.25/59.28 (P6(f14(x251581),x251581)), % 59.25/59.28 inference(rename_variables,[],[73])). % 59.25/59.28 cnf(25161,plain, % 59.25/59.28 (P6(f14(x251611),x251611)), % 59.25/59.28 inference(rename_variables,[],[73])). % 59.25/59.28 cnf(25164,plain, % 59.25/59.28 (P6(f14(x251641),x251641)), % 59.25/59.28 inference(rename_variables,[],[73])). % 59.25/59.28 cnf(25167,plain, % 59.25/59.28 (P6(f14(x251671),x251671)), % 59.25/59.28 inference(rename_variables,[],[73])). % 59.25/59.28 cnf(25172,plain, % 59.25/59.28 (P6(f14(x251721),x251721)), % 59.25/59.28 inference(rename_variables,[],[73])). % 59.25/59.28 cnf(25178,plain, % 59.25/59.28 (P16(f5(a1))), % 59.25/59.28 inference(scs_inference,[],[55,70,241,2409,10300,1532,2817,65,6441,1534,73,25158,25161,25164,25167,71,57,56,87,91,92,93,94,95,96,97,98,99,100,101,102,103,122,160,8,9,10,11,12,13,16,17,18,19,177,178,14,15,79,83,80,88,85,89,2,130,131,134,135,137,138,106,109,112])). % 59.25/59.28 cnf(25180,plain, % 59.25/59.28 (P18(f5(a1))), % 59.25/59.28 inference(scs_inference,[],[55,70,241,2409,10300,1532,2817,65,6441,1534,73,25158,25161,25164,25167,71,57,56,87,91,92,93,94,95,96,97,98,99,100,101,102,103,122,160,8,9,10,11,12,13,16,17,18,19,177,178,14,15,79,83,80,88,85,89,2,130,131,134,135,137,138,106,109,112,115])). % 59.25/59.28 cnf(25182,plain, % 59.25/59.28 (P23(f5(a1))), % 59.25/59.28 inference(scs_inference,[],[55,70,241,2409,10300,1532,2817,65,6441,1534,73,25158,25161,25164,25167,71,57,56,87,91,92,93,94,95,96,97,98,99,100,101,102,103,122,160,8,9,10,11,12,13,16,17,18,19,177,178,14,15,79,83,80,88,85,89,2,130,131,134,135,137,138,106,109,112,115,118])). % 59.25/59.28 cnf(25184,plain, % 59.25/59.28 (P10(f18(a1))), % 59.25/59.28 inference(scs_inference,[],[55,70,241,2409,10300,1532,2817,65,6441,1534,73,25158,25161,25164,25167,71,57,56,87,91,92,93,94,95,96,97,98,99,100,101,102,103,122,160,8,9,10,11,12,13,16,17,18,19,177,178,14,15,79,83,80,88,85,89,2,130,131,134,135,137,138,106,109,112,115,118,120])). % 59.25/59.28 cnf(25186,plain, % 59.25/59.28 (P10(f5(a1))), % 59.25/59.28 inference(scs_inference,[],[55,70,241,2409,10300,1532,2817,65,6441,1534,73,25158,25161,25164,25167,71,57,56,87,91,92,93,94,95,96,97,98,99,100,101,102,103,122,160,8,9,10,11,12,13,16,17,18,19,177,178,14,15,79,83,80,88,85,89,2,130,131,134,135,137,138,106,109,112,115,118,120,121])). % 59.25/59.28 cnf(25188,plain, % 59.25/59.28 (~P10(f21(a2))), % 59.25/59.28 inference(scs_inference,[],[55,70,241,2409,10300,1532,2817,65,6441,1534,76,73,25158,25161,25164,25167,71,57,56,87,91,92,93,94,95,96,97,98,99,100,101,102,103,122,160,8,9,10,11,12,13,16,17,18,19,177,178,14,15,79,83,80,88,85,89,2,130,131,134,135,137,138,106,109,112,115,118,120,121,123])). % 59.25/59.28 cnf(25190,plain, % 59.25/59.28 (~P10(f6(a2))), % 59.25/59.28 inference(scs_inference,[],[55,70,241,2409,10300,1532,2817,65,6441,1534,76,73,25158,25161,25164,25167,71,57,56,87,91,92,93,94,95,96,97,98,99,100,101,102,103,122,160,8,9,10,11,12,13,16,17,18,19,177,178,14,15,79,83,80,88,85,89,2,130,131,134,135,137,138,106,109,112,115,118,120,121,123,124])). % 59.25/59.28 cnf(25208,plain, % 59.25/59.28 (P17(f5(a1),a1)), % 59.25/59.28 inference(scs_inference,[],[55,70,241,2409,10300,1532,2817,65,6441,1534,76,73,25158,25161,25164,25167,71,57,56,87,91,92,93,94,95,96,97,98,99,100,101,102,103,122,160,8,9,10,11,12,13,16,17,18,19,177,178,14,15,79,83,80,88,85,89,2,130,131,134,135,137,138,106,109,112,115,118,120,121,123,124,142,143,144,145,147,148,149,150,151])). % 59.25/59.28 cnf(25218,plain, % 59.25/59.28 (P6(f5(a1),f20(f21(a1)))), % 59.25/59.28 inference(scs_inference,[],[55,70,241,2409,10300,1532,2817,65,6441,1534,76,73,25158,25161,25164,25167,71,57,56,87,91,92,93,94,95,96,97,98,99,100,101,102,103,122,160,8,9,10,11,12,13,16,17,18,19,177,178,14,15,79,83,80,88,85,89,2,130,131,134,135,137,138,106,109,112,115,118,120,121,123,124,142,143,144,145,147,148,149,150,151,152,180,181,182,183])). % 59.25/59.28 cnf(25225,plain, % 59.25/59.28 (P6(f14(x252251),x252251)), % 59.25/59.28 inference(rename_variables,[],[73])). % 59.25/59.28 cnf(25232,plain, % 59.25/59.28 (P6(f14(x252321),x252321)), % 59.25/59.28 inference(rename_variables,[],[73])). % 59.25/59.28 cnf(25235,plain, % 59.25/59.28 (P6(f14(x252351),x252351)), % 59.25/59.28 inference(rename_variables,[],[73])). % 59.25/59.28 cnf(25237,plain, % 59.25/59.28 (P10(f14(f20(a11)))), % 59.25/59.28 inference(scs_inference,[],[55,70,241,2409,7356,10300,1532,59,2817,61,247,65,6441,1534,76,73,25158,25161,25164,25167,25172,25225,25232,25235,71,57,56,87,91,92,93,94,95,96,97,98,99,100,101,102,103,122,160,8,9,10,11,12,13,16,17,18,19,177,178,14,15,79,83,80,88,85,89,2,130,131,134,135,137,138,106,109,112,115,118,120,121,123,124,142,143,144,145,147,148,149,150,151,152,180,181,182,183,184,127,129,132,139,128,140,159])). % 59.25/59.28 cnf(25245,plain, % 59.25/59.28 (~P6(f20(a11),f20(a11))), % 59.25/59.28 inference(scs_inference,[],[55,70,241,2409,7356,10300,7774,1532,59,2817,61,247,1540,65,6441,67,1534,15526,76,73,25158,25161,25164,25167,25172,25225,25232,25235,71,57,56,87,91,92,93,94,95,96,97,98,99,100,101,102,103,122,160,8,9,10,11,12,13,16,17,18,19,177,178,14,15,79,83,80,88,85,89,2,130,131,134,135,137,138,106,109,112,115,118,120,121,123,124,142,143,144,145,147,148,149,150,151,152,180,181,182,183,184,127,129,132,139,128,140,159,141,188,29])). % 59.25/59.28 cnf(25246,plain, % 59.25/59.28 (~P6(f20(f18(a13)),f20(a11))), % 59.25/59.28 inference(scs_inference,[],[55,70,241,2409,7356,10300,7774,1532,59,2817,61,247,1540,65,6441,67,1534,15529,15526,76,73,25158,25161,25164,25167,25172,25225,25232,25235,71,57,56,87,91,92,93,94,95,96,97,98,99,100,101,102,103,122,160,8,9,10,11,12,13,16,17,18,19,177,178,14,15,79,83,80,88,85,89,2,130,131,134,135,137,138,106,109,112,115,118,120,121,123,124,142,143,144,145,147,148,149,150,151,152,180,181,182,183,184,127,129,132,139,128,140,159,141,188,29,28])). % 59.25/59.28 cnf(25249,plain, % 59.25/59.28 (~P10(f4(a1))), % 59.25/59.28 inference(scs_inference,[],[55,70,241,2409,7356,10300,7774,1532,59,2817,61,247,1540,65,6441,67,1534,15529,15526,1529,76,73,25158,25161,25164,25167,25172,25225,25232,25235,71,57,75,56,87,91,92,93,94,95,96,97,98,99,100,101,102,103,122,160,8,9,10,11,12,13,16,17,18,19,177,178,14,15,79,83,80,88,85,89,2,130,131,134,135,137,138,106,109,112,115,118,120,121,123,124,142,143,144,145,147,148,149,150,151,152,180,181,182,183,184,127,129,132,139,128,140,159,141,188,29,28,35,3,153])). % 59.25/59.28 cnf(25251,plain, % 59.25/59.28 (~P10(f8(a1))), % 59.25/59.28 inference(scs_inference,[],[55,70,241,2409,7356,10300,7774,1532,59,2817,61,247,1540,65,6441,67,1534,15529,15526,1529,76,73,25158,25161,25164,25167,25172,25225,25232,25235,71,57,75,56,87,91,92,93,94,95,96,97,98,99,100,101,102,103,122,160,8,9,10,11,12,13,16,17,18,19,177,178,14,15,79,83,80,88,85,89,2,130,131,134,135,137,138,106,109,112,115,118,120,121,123,124,142,143,144,145,147,148,149,150,151,152,180,181,182,183,184,127,129,132,139,128,140,159,141,188,29,28,35,3,153,154])). % 59.25/59.28 cnf(25253,plain, % 59.25/59.28 (P20(f4(a1),a1)), % 59.25/59.28 inference(scs_inference,[],[55,70,241,2409,7356,10300,7774,1532,59,2817,61,247,1540,65,6441,67,1534,15529,15526,1529,76,73,25158,25161,25164,25167,25172,25225,25232,25235,71,57,75,56,87,91,92,93,94,95,96,97,98,99,100,101,102,103,122,160,8,9,10,11,12,13,16,17,18,19,177,178,14,15,79,83,80,88,85,89,2,130,131,134,135,137,138,106,109,112,115,118,120,121,123,124,142,143,144,145,147,148,149,150,151,152,180,181,182,183,184,127,129,132,139,128,140,159,141,188,29,28,35,3,153,154,156])). % 59.25/59.28 cnf(25255,plain, % 59.25/59.28 (P25(f4(a1),a1)), % 59.25/59.28 inference(scs_inference,[],[55,70,241,2409,7356,10300,7774,1532,59,2817,61,247,1540,65,6441,67,1534,15529,15526,1529,76,73,25158,25161,25164,25167,25172,25225,25232,25235,71,57,75,56,87,91,92,93,94,95,96,97,98,99,100,101,102,103,122,160,8,9,10,11,12,13,16,17,18,19,177,178,14,15,79,83,80,88,85,89,2,130,131,134,135,137,138,106,109,112,115,118,120,121,123,124,142,143,144,145,147,148,149,150,151,152,180,181,182,183,184,127,129,132,139,128,140,159,141,188,29,28,35,3,153,154,156,157])). % 59.25/59.28 cnf(25259,plain, % 59.25/59.28 (P6(f4(a1),f20(f21(a1)))), % 59.25/59.28 inference(scs_inference,[],[55,70,241,2409,7356,10300,7774,1532,59,2817,61,247,1540,65,6441,67,1534,15529,15526,1529,76,73,25158,25161,25164,25167,25172,25225,25232,25235,71,57,75,56,87,91,92,93,94,95,96,97,98,99,100,101,102,103,122,160,8,9,10,11,12,13,16,17,18,19,177,178,14,15,79,83,80,88,85,89,2,130,131,134,135,137,138,106,109,112,115,118,120,121,123,124,142,143,144,145,147,148,149,150,151,152,180,181,182,183,184,127,129,132,139,128,140,159,141,188,29,28,35,3,153,154,156,157,158,185])). % 59.25/59.28 cnf(25263,plain, % 59.25/59.28 (E(f15(f15(x252631)),f15(a11))), % 59.25/59.28 inference(scs_inference,[],[55,70,241,2409,7356,10300,7774,1532,59,2817,61,247,1540,65,6441,67,1534,15529,15526,1529,76,73,25158,25161,25164,25167,25172,25225,25232,25235,71,57,75,56,87,91,92,93,94,95,96,97,98,99,100,101,102,103,122,160,8,9,10,11,12,13,16,17,18,19,177,178,14,15,79,83,80,88,85,89,2,130,131,134,135,137,138,106,109,112,115,118,120,121,123,124,142,143,144,145,147,148,149,150,151,152,180,181,182,183,184,127,129,132,139,128,140,159,141,188,29,28,35,3,153,154,156,157,158,185,186,4])). % 59.25/59.28 cnf(25265,plain, % 59.25/59.28 (E(f20(f15(x252651)),f20(a11))), % 59.25/59.28 inference(scs_inference,[],[55,70,241,2409,7356,10300,7774,1532,59,2817,61,247,1540,65,6441,67,1534,15529,15526,1529,76,73,25158,25161,25164,25167,25172,25225,25232,25235,71,57,75,56,87,91,92,93,94,95,96,97,98,99,100,101,102,103,122,160,8,9,10,11,12,13,16,17,18,19,177,178,14,15,79,83,80,88,85,89,2,130,131,134,135,137,138,106,109,112,115,118,120,121,123,124,142,143,144,145,147,148,149,150,151,152,180,181,182,183,184,127,129,132,139,128,140,159,141,188,29,28,35,3,153,154,156,157,158,185,186,4,5,6])). % 59.25/59.28 cnf(25267,plain, % 59.25/59.28 (P17(a11,a1)), % 59.25/59.28 inference(scs_inference,[],[55,70,241,2409,7356,10300,7774,1532,59,2817,61,247,1540,65,6441,67,1534,15529,15526,1529,76,73,25158,25161,25164,25167,25172,25225,25232,25235,71,57,75,56,87,91,92,93,94,95,96,97,98,99,100,101,102,103,122,160,8,9,10,11,12,13,16,17,18,19,177,178,14,15,79,83,80,88,85,89,2,130,131,134,135,137,138,106,109,112,115,118,120,121,123,124,142,143,144,145,147,148,149,150,151,152,180,181,182,183,184,127,129,132,139,128,140,159,141,188,29,28,35,3,153,154,156,157,158,185,186,4,5,6,7,318])). % 59.25/59.28 cnf(25268,plain, % 59.25/59.28 (P25(a11,a1)), % 59.25/59.28 inference(scs_inference,[],[55,70,241,2409,7356,10300,7774,1532,59,2817,61,247,1540,65,6441,67,1534,15529,15526,1529,76,73,25158,25161,25164,25167,25172,25225,25232,25235,71,57,75,56,87,91,92,93,94,95,96,97,98,99,100,101,102,103,122,160,8,9,10,11,12,13,16,17,18,19,177,178,14,15,79,83,80,88,85,89,2,130,131,134,135,137,138,106,109,112,115,118,120,121,123,124,142,143,144,145,147,148,149,150,151,152,180,181,182,183,184,127,129,132,139,128,140,159,141,188,29,28,35,3,153,154,156,157,158,185,186,4,5,6,7,318,320])). % 59.25/59.28 cnf(25269,plain, % 59.25/59.28 (P22(a11,a1)), % 59.25/59.28 inference(scs_inference,[],[55,70,241,2409,7356,10300,7774,1532,59,2817,61,247,1540,65,6441,67,1534,15529,15526,1529,76,73,25158,25161,25164,25167,25172,25225,25232,25235,71,57,75,56,87,91,92,93,94,95,96,97,98,99,100,101,102,103,122,160,8,9,10,11,12,13,16,17,18,19,177,178,14,15,79,83,80,88,85,89,2,130,131,134,135,137,138,106,109,112,115,118,120,121,123,124,142,143,144,145,147,148,149,150,151,152,180,181,182,183,184,127,129,132,139,128,140,159,141,188,29,28,35,3,153,154,156,157,158,185,186,4,5,6,7,318,320,335])). % 59.25/59.28 cnf(25270,plain, % 59.25/59.28 (P13(a11,a1)), % 59.25/59.28 inference(scs_inference,[],[55,70,241,2409,7356,10300,7774,1532,59,2817,61,247,1540,65,6441,67,1534,15529,15526,1529,76,73,25158,25161,25164,25167,25172,25225,25232,25235,71,57,75,56,87,91,92,93,94,95,96,97,98,99,100,101,102,103,122,160,8,9,10,11,12,13,16,17,18,19,177,178,14,15,79,83,80,88,85,89,2,130,131,134,135,137,138,106,109,112,115,118,120,121,123,124,142,143,144,145,147,148,149,150,151,152,180,181,182,183,184,127,129,132,139,128,140,159,141,188,29,28,35,3,153,154,156,157,158,185,186,4,5,6,7,318,320,335,337])). % 59.25/59.28 cnf(25271,plain, % 59.25/59.28 (P20(a11,a1)), % 59.25/59.28 inference(scs_inference,[],[55,70,241,2409,7356,10300,7774,1532,59,2817,61,247,1540,65,6441,67,1534,15529,15526,1529,76,73,25158,25161,25164,25167,25172,25225,25232,25235,71,57,75,56,87,91,92,93,94,95,96,97,98,99,100,101,102,103,122,160,8,9,10,11,12,13,16,17,18,19,177,178,14,15,79,83,80,88,85,89,2,130,131,134,135,137,138,106,109,112,115,118,120,121,123,124,142,143,144,145,147,148,149,150,151,152,180,181,182,183,184,127,129,132,139,128,140,159,141,188,29,28,35,3,153,154,156,157,158,185,186,4,5,6,7,318,320,335,337,348])). % 59.25/59.28 cnf(25272,plain, % 59.25/59.28 (P21(a11,a1)), % 59.25/59.28 inference(scs_inference,[],[55,70,241,2409,7356,10300,7774,1532,59,2817,61,247,1540,65,6441,67,1534,15529,15526,1529,76,73,25158,25161,25164,25167,25172,25225,25232,25235,71,57,75,56,87,91,92,93,94,95,96,97,98,99,100,101,102,103,122,160,8,9,10,11,12,13,16,17,18,19,177,178,14,15,79,83,80,88,85,89,2,130,131,134,135,137,138,106,109,112,115,118,120,121,123,124,142,143,144,145,147,148,149,150,151,152,180,181,182,183,184,127,129,132,139,128,140,159,141,188,29,28,35,3,153,154,156,157,158,185,186,4,5,6,7,318,320,335,337,348,349])). % 59.25/59.28 cnf(25274,plain, % 59.25/59.28 (~E(f15(f18(a13)),f20(a11))), % 59.25/59.28 inference(scs_inference,[],[55,70,241,2409,7356,10300,7774,1532,59,2817,61,247,1540,65,6441,67,1534,15529,15526,1529,76,73,25158,25161,25164,25167,25172,25225,25232,25235,71,57,75,56,87,91,92,93,94,95,96,97,98,99,100,101,102,103,122,160,8,9,10,11,12,13,16,17,18,19,177,178,14,15,79,83,80,88,85,89,2,130,131,134,135,137,138,106,109,112,115,118,120,121,123,124,142,143,144,145,147,148,149,150,151,152,180,181,182,183,184,127,129,132,139,128,140,159,141,188,29,28,35,3,153,154,156,157,158,185,186,4,5,6,7,318,320,335,337,348,349,15564,351])). % 59.25/59.28 cnf(25294,plain, % 59.25/59.28 (P17(a11,a10)), % 59.25/59.28 inference(scs_inference,[],[25144,2881])). % 59.25/59.28 cnf(25295,plain, % 59.25/59.28 (E(f15(x252951),a11)), % 59.25/59.28 inference(rename_variables,[],[25144])). % 59.25/59.28 cnf(25297,plain, % 59.25/59.28 (E(f15(x252971),a11)), % 59.25/59.28 inference(rename_variables,[],[25144])). % 59.25/59.28 cnf(25300,plain, % 59.25/59.28 (E(f18(a2),a11)), % 59.25/59.28 inference(scs_inference,[],[25118,25144,25295,56,2881,6628,122,79])). % 59.25/59.28 cnf(25302,plain, % 59.25/59.28 (P10(f3(a1))), % 59.25/59.28 inference(scs_inference,[],[25118,25144,25295,56,2881,6628,122,79,102])). % 59.25/59.28 cnf(25304,plain, % 59.25/59.28 (P18(f3(a1))), % 59.25/59.28 inference(scs_inference,[],[25118,25144,25295,56,2881,6628,122,79,102,98])). % 59.25/59.28 cnf(25306,plain, % 59.25/59.28 (P10(f18(a10))), % 59.25/59.28 inference(scs_inference,[],[25154,25118,25144,25295,56,2881,6628,122,79,102,98,101])). % 59.25/59.28 cnf(25308,plain, % 59.25/59.28 (~P10(f16(f21(a2)))), % 59.25/59.28 inference(scs_inference,[],[25154,25118,25144,25295,25188,56,2881,6628,122,79,102,98,101,103])). % 59.25/59.28 cnf(25310,plain, % 59.25/59.28 (P23(f3(a1))), % 59.25/59.28 inference(scs_inference,[],[25154,25118,25144,25295,25188,56,2881,6628,122,79,102,98,101,103,100])). % 59.25/59.28 cnf(25312,plain, % 59.25/59.28 (P16(f3(a1))), % 59.25/59.28 inference(scs_inference,[],[25154,25118,25144,25295,25188,56,2881,6628,122,79,102,98,101,103,100,96])). % 59.25/59.28 cnf(25318,plain, % 59.25/59.28 (P23(f18(a10))), % 59.25/59.28 inference(scs_inference,[],[25154,25118,25144,25295,25188,1533,56,2881,6628,122,79,102,98,101,103,100,96,92,160,99])). % 59.25/59.28 cnf(25323,plain, % 59.25/59.28 (P9(f18(a10))), % 59.25/59.28 inference(scs_inference,[],[25154,25118,25144,25295,25297,25188,1533,56,2881,6628,122,79,102,98,101,103,100,96,92,160,99,87,18,93])). % 59.25/59.28 cnf(25327,plain, % 59.25/59.28 (P6(f18(a10),f20(f21(a10)))), % 59.25/59.28 inference(scs_inference,[],[25154,25118,25144,25295,25297,25188,1533,56,2881,6628,122,79,102,98,101,103,100,96,92,160,99,87,18,93,178,177])). % 59.25/59.28 cnf(25330,plain, % 59.25/59.28 (E(f20(f18(a2)),f20(a11))), % 59.25/59.28 inference(scs_inference,[],[25154,25118,25144,25295,25297,25188,1533,56,2881,6628,122,79,102,98,101,103,100,96,92,160,99,87,18,93,178,177,14,6])). % 59.25/59.28 cnf(25351,plain, % 59.25/59.28 (P4(a1)), % 59.25/59.28 inference(scs_inference,[],[25154,25118,25144,25295,25297,25188,25245,1533,56,2881,6628,122,79,102,98,101,103,100,96,92,160,99,87,18,93,178,177,14,6,91,95,19,11,94,13,10,17,12,16,4,5,15,8,7,9,351,89])). % 59.25/59.28 cnf(25355,plain, % 59.25/59.28 (P6(f14(x253551),x253551)), % 59.25/59.28 inference(rename_variables,[],[73])). % 59.25/59.28 cnf(25358,plain, % 59.25/59.28 (P6(f14(x253581),x253581)), % 59.25/59.28 inference(rename_variables,[],[73])). % 59.25/59.28 cnf(25360,plain, % 59.25/59.28 (~P10(f21(a1))), % 59.25/59.28 inference(scs_inference,[],[25154,25096,25150,25118,25144,25295,25297,25188,25245,2849,1533,73,25355,75,56,2881,6628,122,79,102,98,101,103,100,96,92,160,99,87,18,93,178,177,14,6,91,95,19,11,94,13,10,17,12,16,4,5,15,8,7,9,351,89,2,131,137,123])). % 59.25/59.28 cnf(25363,plain, % 59.25/59.28 (P6(f14(x253631),x253631)), % 59.25/59.28 inference(rename_variables,[],[73])). % 59.25/59.28 cnf(25366,plain, % 59.25/59.28 (P6(f14(x253661),x253661)), % 59.25/59.28 inference(rename_variables,[],[73])). % 59.25/59.28 cnf(25369,plain, % 59.25/59.28 (P6(f14(x253691),x253691)), % 59.25/59.28 inference(rename_variables,[],[73])). % 59.25/59.28 cnf(25372,plain, % 59.25/59.28 (P6(f14(x253721),x253721)), % 59.25/59.28 inference(rename_variables,[],[73])). % 59.25/59.28 cnf(25376,plain, % 59.25/59.28 (~P10(f6(a1))), % 59.25/59.28 inference(scs_inference,[],[25154,25096,25150,25100,25106,25118,25144,25295,25297,25188,25245,2849,1533,73,25355,25358,25363,25366,25369,75,56,2881,6628,122,79,102,98,101,103,100,96,92,160,99,87,18,93,178,177,14,6,91,95,19,11,94,13,10,17,12,16,4,5,15,8,7,9,351,89,2,131,137,123,134,136,127,140,180,124])). % 59.25/59.28 cnf(25379,plain, % 59.25/59.28 (P6(f14(x253791),x253791)), % 59.25/59.28 inference(rename_variables,[],[73])). % 59.25/59.28 cnf(25382,plain, % 59.25/59.28 (P6(f14(x253821),x253821)), % 59.25/59.28 inference(rename_variables,[],[73])). % 59.25/59.28 cnf(25384,plain, % 59.25/59.28 (P7(f18(a2),f20(f21(a2)))), % 59.25/59.28 inference(scs_inference,[],[25154,25096,25150,25100,25102,25106,25110,25118,25144,25295,25297,25188,25245,25138,2849,1533,78,73,25355,25358,25363,25366,25369,25372,25379,75,56,2881,6628,122,79,102,98,101,103,100,96,92,160,99,87,18,93,178,177,14,6,91,95,19,11,94,13,10,17,12,16,4,5,15,8,7,9,351,89,2,131,137,123,134,136,127,140,180,124,139,132,159])). % 59.25/59.28 cnf(25388,plain, % 59.25/59.28 (P6(f14(x253881),x253881)), % 59.25/59.28 inference(rename_variables,[],[73])). % 59.25/59.28 cnf(25394,plain, % 59.25/59.28 (~E(f18(a2),f21(a2))), % 59.25/59.28 inference(scs_inference,[],[25154,25096,25150,25100,25102,25106,25110,25118,25144,25295,25297,25188,25245,25263,25138,2849,1533,78,73,25355,25358,25363,25366,25369,25372,25379,25382,25388,74,75,56,2881,6628,122,79,102,98,101,103,100,96,92,160,99,87,18,93,178,177,14,6,91,95,19,11,94,13,10,17,12,16,4,5,15,8,7,9,351,89,2,131,137,123,134,136,127,140,180,124,139,132,159,141,29,28,35])). % 59.25/59.28 cnf(25395,plain, % 59.25/59.28 (~E(a11,f20(a11))), % 59.25/59.28 inference(scs_inference,[],[25154,25096,25150,25100,25102,25106,25110,25118,25144,25295,25297,25188,25245,25274,25263,25138,2849,1533,78,73,25355,25358,25363,25366,25369,25372,25379,25382,25388,74,75,56,2881,6628,122,79,102,98,101,103,100,96,92,160,99,87,18,93,178,177,14,6,91,95,19,11,94,13,10,17,12,16,4,5,15,8,7,9,351,89,2,131,137,123,134,136,127,140,180,124,139,132,159,141,29,28,35,3])). % 59.25/59.28 cnf(25396,plain, % 59.25/59.28 (E(f15(x253961),a11)), % 59.25/59.28 inference(rename_variables,[],[25144])). % 59.25/59.28 cnf(25402,plain, % 59.25/59.28 (P7(f15(f15(x254021)),f20(a11))), % 59.25/59.28 inference(scs_inference,[],[25154,25096,25150,25100,25102,25106,25110,25118,25144,25295,25297,25396,25188,25245,25274,25263,25265,25138,2849,1533,329,78,73,25355,25358,25363,25366,25369,25372,25379,25382,25388,74,75,56,2881,6628,122,79,102,98,101,103,100,96,92,160,99,87,18,93,178,177,14,6,91,95,19,11,94,13,10,17,12,16,4,5,15,8,7,9,351,89,2,131,137,123,134,136,127,140,180,124,139,132,159,141,29,28,35,3,176,6765,51])). % 59.25/59.28 cnf(25410,plain, % 59.25/59.28 (P6(x254101,f20(x254101))), % 59.25/59.28 inference(scs_inference,[],[72,160])). % 59.25/59.28 cnf(25412,plain, % 59.25/59.28 (E(f3(a1),a11)), % 59.25/59.28 inference(scs_inference,[],[25302,72,160,79])). % 59.25/59.28 cnf(25437,plain, % 59.25/59.28 (P6(f14(x254371),x254371)), % 59.25/59.28 inference(rename_variables,[],[73])). % 59.25/59.28 cnf(25440,plain, % 59.25/59.28 (P6(f14(x254401),x254401)), % 59.25/59.28 inference(rename_variables,[],[73])). % 59.25/59.28 cnf(25443,plain, % 59.25/59.28 (P6(f14(x254431),x254431)), % 59.25/59.28 inference(rename_variables,[],[73])). % 59.25/59.28 cnf(25446,plain, % 59.25/59.28 (P6(f14(x254461),x254461)), % 59.25/59.28 inference(rename_variables,[],[73])). % 59.25/59.28 cnf(25449,plain, % 59.25/59.28 (P6(f14(x254491),x254491)), % 59.25/59.28 inference(rename_variables,[],[73])). % 59.25/59.28 cnf(25453,plain, % 59.25/59.28 (P6(f14(x254531),x254531)), % 59.25/59.28 inference(rename_variables,[],[73])). % 59.25/59.28 cnf(25456,plain, % 59.25/59.28 (P6(f14(x254561),x254561)), % 59.25/59.28 inference(rename_variables,[],[73])). % 59.25/59.28 cnf(25458,plain, % 59.25/59.28 (~P6(f20(a11),f20(f3(a1)))), % 59.25/59.28 inference(scs_inference,[],[25351,25190,25302,25304,25310,25312,25318,25323,25394,25300,25246,25402,212,72,73,25437,25440,25443,25446,25449,25453,160,79,103,18,6,14,177,13,11,12,4,7,19,10,17,9,8,15,5,16,351,2,131,136,134,138,140,51,128,132,188])). % 59.25/59.28 cnf(25463,plain, % 59.25/59.28 (~P6(f20(f18(a2)),f20(a11))), % 59.25/59.28 inference(scs_inference,[],[25351,25190,25302,25304,25310,25312,25318,25323,25394,25300,25246,25402,25330,25245,212,72,73,25437,25440,25443,25446,25449,25453,25456,160,79,103,18,6,14,177,13,11,12,4,7,19,10,17,9,8,15,5,16,351,2,131,136,134,138,140,51,128,132,188,141,28])). % 59.25/59.28 cnf(25465,plain, % 59.25/59.28 (~E(f3(a1),f6(a2))), % 59.25/59.28 inference(scs_inference,[],[25351,25190,25302,25304,25310,25312,25318,25323,25394,25300,25246,25402,25330,25245,212,72,73,25437,25440,25443,25446,25449,25453,25456,160,79,103,18,6,14,177,13,11,12,4,7,19,10,17,9,8,15,5,16,351,2,131,136,134,138,140,51,128,132,188,141,28,29,35])). % 59.25/59.28 cnf(25467,plain, % 59.25/59.28 (~P21(f4(a1),a1)), % 59.25/59.28 inference(scs_inference,[],[55,25351,25253,25190,25249,25302,25304,25310,25312,25318,25323,25394,25300,25246,25402,25330,25259,25245,212,72,73,25437,25440,25443,25446,25449,25453,25456,56,160,79,103,18,6,14,177,13,11,12,4,7,19,10,17,9,8,15,5,16,351,2,131,136,134,138,140,51,128,132,188,141,28,29,35,3,202])). % 59.25/59.28 cnf(25495,plain, % 59.25/59.28 (E(f18(a10),a11)), % 59.25/59.28 inference(scs_inference,[],[25306,79])). % 59.25/59.28 cnf(25520,plain, % 59.25/59.28 (P6(f14(x255201),x255201)), % 59.25/59.28 inference(rename_variables,[],[73])). % 59.25/59.28 cnf(25523,plain, % 59.25/59.28 (P6(f14(x255231),x255231)), % 59.25/59.28 inference(rename_variables,[],[73])). % 59.25/59.28 cnf(25526,plain, % 59.25/59.28 (P6(f14(x255261),x255261)), % 59.25/59.28 inference(rename_variables,[],[73])). % 59.25/59.28 cnf(25529,plain, % 59.25/59.28 (P6(f14(x255291),x255291)), % 59.25/59.28 inference(rename_variables,[],[73])). % 59.25/59.28 cnf(25531,plain, % 59.25/59.28 (~P6(a12,f20(f18(a10)))), % 59.25/59.28 inference(scs_inference,[],[25251,25465,25412,25463,25178,25180,25306,7342,69,73,25520,25523,25526,79,103,177,18,11,17,19,4,7,12,6,10,14,13,9,5,16,8,15,351,2,130,134,136,139,188])). % 59.25/59.28 cnf(25533,plain, % 59.25/59.28 (~P7(x255331,f3(a1))), % 59.25/59.28 inference(scs_inference,[],[25251,25465,25412,25463,25178,25180,25306,7342,69,212,73,25520,25523,25526,79,103,177,18,11,17,19,4,7,12,6,10,14,13,9,5,16,8,15,351,2,130,134,136,139,188,51])). % 59.25/59.28 cnf(25535,plain, % 59.25/59.28 (P6(f14(x255351),x255351)), % 59.25/59.28 inference(rename_variables,[],[73])). % 59.25/59.28 cnf(25540,plain, % 59.25/59.28 (~P7(f20(f18(a2)),f20(a11))), % 59.25/59.28 inference(scs_inference,[],[25410,25251,25465,25412,25463,25104,25114,25178,25180,25306,7342,69,212,73,25520,25523,25526,25529,25535,79,103,177,18,11,17,19,4,7,12,6,10,14,13,9,5,16,8,15,351,2,130,134,136,139,188,51,132,141,189])). % 59.25/59.28 cnf(25541,plain, % 59.25/59.28 (P6(x255411,f20(x255411))), % 59.25/59.28 inference(rename_variables,[],[25410])). % 59.25/59.28 cnf(25543,plain, % 59.25/59.28 (P21(f18(a13),a1)), % 59.25/59.28 inference(scs_inference,[],[25410,25251,25465,25412,25463,25104,25114,25178,25180,25306,7342,25272,69,212,1534,73,25520,25523,25526,25529,25535,79,103,177,18,11,17,19,4,7,12,6,10,14,13,9,5,16,8,15,351,2,130,134,136,139,188,51,132,141,189,38])). % 59.25/59.28 cnf(25546,plain, % 59.25/59.28 (~E(f18(a10),f8(a1))), % 59.25/59.28 inference(scs_inference,[],[25410,25541,25251,25465,25412,25463,25104,25114,25178,25180,25306,7342,25272,69,212,1534,73,25520,25523,25526,25529,25535,79,103,177,18,11,17,19,4,7,12,6,10,14,13,9,5,16,8,15,351,2,130,134,136,139,188,51,132,141,189,38,28,35])). % 59.25/59.28 cnf(25580,plain, % 59.25/59.28 (P6(f14(x255801),x255801)), % 59.25/59.28 inference(rename_variables,[],[73])). % 59.25/59.28 cnf(25582,plain, % 59.25/59.28 (~P6(f20(f21(a2)),f20(a11))), % 59.25/59.28 inference(scs_inference,[],[25360,25546,25495,25458,25384,25116,25237,68,73,79,103,14,18,19,10,9,11,13,12,17,15,16,351,8,2,140,188])). % 59.25/59.28 cnf(25589,plain, % 59.25/59.28 (~E(f18(a13),f4(a1))), % 59.25/59.28 inference(scs_inference,[],[25533,25467,25543,25360,25546,25495,25458,25384,25116,25237,68,73,25580,79,103,14,18,19,10,9,11,13,12,17,15,16,351,8,2,140,188,51,141,38])). % 59.25/59.28 cnf(25590,plain, % 59.25/59.28 (~E(f18(a10),a12)), % 59.25/59.28 inference(scs_inference,[],[25533,25467,25543,25360,25546,25495,25458,25531,25384,25116,25237,25410,68,73,25580,79,103,14,18,19,10,9,11,13,12,17,15,16,351,8,2,140,188,51,141,38,28])). % 59.25/59.28 cnf(25591,plain, % 59.25/59.28 (P6(x255911,f20(x255911))), % 59.25/59.28 inference(rename_variables,[],[25410])). % 59.25/59.28 cnf(25596,plain, % 59.25/59.28 (~P17(f4(a1),a1)), % 59.25/59.28 inference(scs_inference,[],[55,25533,25395,25467,25543,25360,25546,25495,25458,25531,25384,25116,25237,25410,25591,25255,25259,68,1534,73,25580,56,79,103,14,18,19,10,9,11,13,12,17,15,16,351,8,2,140,188,51,141,38,28,35,29,3,205])). % 59.25/59.28 cnf(25598,plain, % 59.25/59.28 (P7(a11,f20(a11))), % 59.25/59.28 inference(scs_inference,[],[55,25533,25395,25467,25543,25360,25546,25495,25458,25531,25384,25116,25237,25410,25591,25255,25259,68,1534,73,25580,56,79,103,14,18,19,10,9,11,13,12,17,15,16,351,8,2,140,188,51,141,38,28,35,29,3,205,339])). % 59.25/59.28 cnf(25601,plain, % 59.25/59.28 (~E(a11,f4(a1))), % 59.25/59.28 inference(scs_inference,[],[55,25267,25533,25395,25467,25543,25360,25546,25495,25458,25531,25384,25116,25237,25410,25591,25255,25259,68,1534,73,25580,56,79,103,14,18,19,10,9,11,13,12,17,15,16,351,8,2,140,188,51,141,38,28,35,29,3,205,339,20871,44])). % 59.25/59.28 cnf(25605,plain, % 59.25/59.28 (E(f3(a10),a11)), % 59.25/59.28 inference(scs_inference,[],[25120,79])). % 59.25/59.28 cnf(25610,plain, % 59.25/59.28 (E(f20(f3(a10)),f20(a11))), % 59.25/59.28 inference(scs_inference,[],[25376,25120,79,103,7,6])). % 59.25/59.28 cnf(25628,plain, % 59.25/59.28 (P6(f14(x256281),x256281)), % 59.25/59.28 inference(rename_variables,[],[73])). % 59.25/59.28 cnf(25631,plain, % 59.25/59.28 (~P6(f20(a11),f20(f3(a10)))), % 59.25/59.28 inference(scs_inference,[],[25601,25376,25598,25582,25540,25120,25318,1529,73,79,103,7,6,4,5,14,13,9,18,17,10,19,12,11,16,15,8,351,2,140,50,188])). % 59.25/59.28 cnf(25634,plain, % 59.25/59.28 (P6(f14(x256341),x256341)), % 59.25/59.28 inference(rename_variables,[],[73])). % 59.25/59.28 cnf(25637,plain, % 59.25/59.28 (~P7(x256371,f18(a10))), % 59.25/59.28 inference(scs_inference,[],[25294,25601,25376,25598,25582,25540,25182,25120,25318,212,25495,1534,1529,73,25628,79,103,7,6,4,5,14,13,9,18,17,10,19,12,11,16,15,8,351,2,140,50,188,141,44,51])). % 59.25/59.28 cnf(25639,plain, % 59.25/59.28 (P6(f14(f18(a10)),a11)), % 59.25/59.28 inference(scs_inference,[],[25294,25601,25376,25598,25582,25327,25540,25182,25120,25318,212,25495,1534,1529,73,25628,25634,79,103,7,6,4,5,14,13,9,18,17,10,19,12,11,16,15,8,351,2,140,50,188,141,44,51,28,29])). % 59.25/59.28 cnf(25641,plain, % 59.25/59.28 (~E(f3(a10),f6(a1))), % 59.25/59.28 inference(scs_inference,[],[25294,25601,25376,25598,25582,25327,25540,25182,25120,25318,212,25495,1534,1529,73,25628,25634,79,103,7,6,4,5,14,13,9,18,17,10,19,12,11,16,15,8,351,2,140,50,188,141,44,51,28,29,35])). % 59.25/59.28 cnf(25659,plain, % 59.25/59.28 (E(f5(a1),a11)), % 59.25/59.28 inference(scs_inference,[],[25186,79])). % 59.25/59.28 cnf(25665,plain, % 59.25/59.28 (E(f9(f3(a10),x256651),f9(a11,x256651))), % 59.25/59.28 inference(scs_inference,[],[25605,25186,25249,79,103,7,6,14])). % 59.25/59.28 cnf(25678,plain, % 59.25/59.28 (E(f9(x256781,f3(a10)),f9(x256781,a11))), % 59.25/59.28 inference(scs_inference,[],[25605,25631,25186,25249,79,103,7,6,14,9,4,10,19,5,17,11,12,18,13,16,351,15])). % 59.25/59.28 cnf(25683,plain, % 59.25/59.28 (P5(a11,f3(a10))), % 59.25/59.28 inference(scs_inference,[],[25589,25605,25631,25186,25249,308,72,79,103,7,6,14,9,4,10,19,5,17,11,12,18,13,16,351,15,8,2,26,25])). % 59.25/59.28 cnf(25694,plain, % 59.25/59.28 (~P6(f20(f3(a10)),f20(a11))), % 59.25/59.28 inference(scs_inference,[],[25268,25269,25270,25271,25208,25637,25596,25589,25605,25610,25631,25639,25186,7804,25249,25245,308,72,66,1534,79,103,7,6,14,9,4,10,19,5,17,11,12,18,13,16,351,15,8,2,26,25,42,40,141,44,22,51,46,28])). % 59.25/59.28 cnf(25702,plain, % 59.25/59.28 (P22(f5(a1),a1)), % 59.25/59.28 inference(scs_inference,[],[55,25268,25269,25270,25271,25208,25637,25596,25589,25641,25605,25610,209,25218,25631,25122,25639,25186,7804,25249,10306,25410,25245,308,72,66,1534,75,56,79,103,7,6,14,9,4,10,19,5,17,11,12,18,13,16,351,15,8,2,26,25,42,40,141,44,22,51,46,28,35,29,3,160,54,194])). % 59.25/59.28 cnf(25734,plain, % 59.25/59.28 (P6(f14(x257341),x257341)), % 59.25/59.28 inference(rename_variables,[],[73])). % 59.25/59.28 cnf(25753,plain, % 59.25/59.28 ($false), % 59.25/59.28 inference(scs_inference,[],[55,25590,25659,25683,25702,25665,25678,25694,25308,25267,25270,25218,25402,25184,2409,212,78,1534,73,25734,75,56,160,79,103,7,6,19,4,11,12,13,17,18,9,5,14,10,16,8,351,15,2,188,141,44,51,35,28,29,3,195,206,207,208,187]), % 59.25/59.28 ['proof']). % 59.25/59.29 % SZS output end Proof % 59.25/59.29 % Total time :58.580000s %------------------------------------------------------------------------------