%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SEU325+1 : TPTP v8.2.0. Released v3.3.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n027.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:02:28 EDT 2024 % Result : Theorem 0.58s 1.09s % Output : CNFRefutation 0.58s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.13 % Problem : SEU325+1 : TPTP v8.2.0. Released v3.3.0. % 0.12/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.34 % Computer : n027.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Fri Jun 21 13:20:24 EDT 2024 % 0.12/0.34 % CPUTime : % 0.21/0.58 start to proof:theBenchmark % 0.57/1.08 %------------------------------------------- % 0.57/1.08 % File :CSE---1.7 % 0.57/1.08 % Problem :theBenchmark % 0.57/1.08 % Transform :cnf % 0.57/1.08 % Format :tptp:raw % 0.57/1.08 % Command :java -jar mcs_scs.jar %d %s % 0.57/1.08 % 0.57/1.08 % Result :Theorem 0.450000s % 0.57/1.08 % Output :CNFRefutation 0.450000s % 0.57/1.08 %------------------------------------------- % 0.57/1.08 %------------------------------------------------------------------------------ % 0.57/1.08 % File : SEU325+1 : TPTP v8.2.0. Released v3.3.0. % 0.57/1.08 % Domain : Set theory % 0.57/1.08 % Problem : MPTP bushy problem t5_tops_2 % 0.57/1.08 % Version : [Urb07] axioms : Especial. % 0.57/1.08 % English : % 0.57/1.08 % 0.57/1.08 % Refs : [Ban01] Bancerek et al. (2001), On the Characterizations of Co % 0.57/1.08 % : [Urb07] Urban (2006), Email to G. Sutcliffe % 0.57/1.08 % Source : [Urb07] % 0.57/1.08 % Names : bushy-t5_tops_2 [Urb07] % 0.57/1.08 % 0.57/1.08 % Status : Theorem % 0.57/1.08 % Rating : 0.36 v8.2.0, 0.33 v8.1.0, 0.31 v7.5.0, 0.34 v7.4.0, 0.27 v7.3.0, 0.28 v7.2.0, 0.24 v7.1.0, 0.26 v7.0.0, 0.20 v6.4.0, 0.23 v6.3.0, 0.21 v6.2.0, 0.28 v6.1.0, 0.37 v6.0.0, 0.35 v5.5.0, 0.33 v5.4.0, 0.36 v5.3.0, 0.37 v5.2.0, 0.15 v5.1.0, 0.14 v5.0.0, 0.29 v4.1.0, 0.35 v4.0.1, 0.30 v4.0.0, 0.33 v3.7.0, 0.30 v3.5.0, 0.32 v3.3.0 % 0.57/1.08 % Syntax : Number of formulae : 49 ( 10 unt; 0 def) % 0.57/1.08 % Number of atoms : 146 ( 7 equ) % 0.57/1.08 % Maximal formula atoms : 7 ( 2 avg) % 0.57/1.08 % Number of connectives : 115 ( 18 ~; 1 |; 50 &) % 0.57/1.08 % ( 4 <=>; 42 =>; 0 <=; 0 <~>) % 0.57/1.08 % Maximal formula depth : 9 ( 5 avg) % 0.57/1.08 % Maximal term depth : 4 ( 1 avg) % 0.57/1.08 % Number of predicates : 19 ( 17 usr; 1 prp; 0-2 aty) % 0.57/1.08 % Number of functors : 6 ( 6 usr; 1 con; 0-2 aty) % 0.57/1.08 % Number of variables : 74 ( 66 !; 8 ?) % 0.57/1.08 % SPC : FOF_THM_RFO_SEQ % 0.57/1.08 % 0.57/1.08 % Comments : Translated by MPTP 0.2 from the original problem in the Mizar % 0.57/1.08 % library, www.mizar.org % 0.57/1.08 %------------------------------------------------------------------------------ % 0.57/1.08 fof(antisymmetry_r2_hidden,axiom, % 0.57/1.08 ! [A,B] : % 0.57/1.08 ( in(A,B) % 0.57/1.08 => ~ in(B,A) ) ). % 0.57/1.08 % 0.57/1.08 fof(cc10_membered,axiom, % 0.57/1.08 ! [A] : % 0.57/1.08 ( v1_membered(A) % 0.57/1.08 => ! [B] : % 0.57/1.08 ( element(B,A) % 0.57/1.08 => v1_xcmplx_0(B) ) ) ). % 0.57/1.08 % 0.57/1.08 fof(cc11_membered,axiom, % 0.57/1.08 ! [A] : % 0.57/1.08 ( v2_membered(A) % 0.57/1.08 => ! [B] : % 0.57/1.08 ( element(B,A) % 0.57/1.08 => ( v1_xcmplx_0(B) % 0.57/1.08 & v1_xreal_0(B) ) ) ) ). % 0.57/1.08 % 0.57/1.08 fof(cc12_membered,axiom, % 0.57/1.08 ! [A] : % 0.57/1.08 ( v3_membered(A) % 0.57/1.08 => ! [B] : % 0.57/1.08 ( element(B,A) % 0.57/1.08 => ( v1_xcmplx_0(B) % 0.57/1.08 & v1_xreal_0(B) % 0.57/1.08 & v1_rat_1(B) ) ) ) ). % 0.57/1.08 % 0.57/1.08 fof(cc13_membered,axiom, % 0.57/1.08 ! [A] : % 0.57/1.08 ( v4_membered(A) % 0.57/1.08 => ! [B] : % 0.57/1.08 ( element(B,A) % 0.57/1.08 => ( v1_xcmplx_0(B) % 0.57/1.08 & v1_xreal_0(B) % 0.57/1.08 & v1_int_1(B) % 0.57/1.08 & v1_rat_1(B) ) ) ) ). % 0.57/1.08 % 0.57/1.08 fof(cc14_membered,axiom, % 0.57/1.08 ! [A] : % 0.57/1.08 ( v5_membered(A) % 0.57/1.08 => ! [B] : % 0.57/1.08 ( element(B,A) % 0.57/1.09 => ( v1_xcmplx_0(B) % 0.57/1.09 & natural(B) % 0.57/1.09 & v1_xreal_0(B) % 0.57/1.09 & v1_int_1(B) % 0.57/1.09 & v1_rat_1(B) ) ) ) ). % 0.57/1.09 % 0.57/1.09 fof(cc15_membered,axiom, % 0.57/1.09 ! [A] : % 0.57/1.09 ( empty(A) % 0.57/1.09 => ( v1_membered(A) % 0.57/1.09 & v2_membered(A) % 0.57/1.09 & v3_membered(A) % 0.57/1.09 & v4_membered(A) % 0.57/1.09 & v5_membered(A) ) ) ). % 0.57/1.09 % 0.57/1.09 fof(cc16_membered,axiom, % 0.57/1.09 ! [A] : % 0.57/1.09 ( v1_membered(A) % 0.57/1.09 => ! [B] : % 0.57/1.09 ( element(B,powerset(A)) % 0.57/1.09 => v1_membered(B) ) ) ). % 0.57/1.09 % 0.57/1.09 fof(cc17_membered,axiom, % 0.57/1.09 ! [A] : % 0.57/1.09 ( v2_membered(A) % 0.57/1.09 => ! [B] : % 0.57/1.09 ( element(B,powerset(A)) % 0.57/1.09 => ( v1_membered(B) % 0.57/1.09 & v2_membered(B) ) ) ) ). % 0.57/1.09 % 0.57/1.09 fof(cc18_membered,axiom, % 0.57/1.09 ! [A] : % 0.57/1.09 ( v3_membered(A) % 0.57/1.09 => ! [B] : % 0.57/1.09 ( element(B,powerset(A)) % 0.57/1.09 => ( v1_membered(B) % 0.57/1.09 & v2_membered(B) % 0.57/1.09 & v3_membered(B) ) ) ) ). % 0.57/1.09 % 0.57/1.09 fof(cc19_membered,axiom, % 0.57/1.09 ! [A] : % 0.57/1.09 ( v4_membered(A) % 0.57/1.09 => ! [B] : % 0.57/1.09 ( element(B,powerset(A)) % 0.57/1.09 => ( v1_membered(B) % 0.57/1.09 & v2_membered(B) % 0.57/1.09 & v3_membered(B) % 0.57/1.09 & v4_membered(B) ) ) ) ). % 0.57/1.09 % 0.57/1.09 fof(cc1_membered,axiom, % 0.57/1.09 ! [A] : % 0.57/1.09 ( v5_membered(A) % 0.57/1.09 => v4_membered(A) ) ). % 0.57/1.09 % 0.57/1.09 fof(cc20_membered,axiom, % 0.57/1.09 ! [A] : % 0.57/1.09 ( v5_membered(A) % 0.57/1.09 => ! [B] : % 0.57/1.09 ( element(B,powerset(A)) % 0.57/1.09 => ( v1_membered(B) % 0.57/1.09 & v2_membered(B) % 0.57/1.09 & v3_membered(B) % 0.57/1.09 & v4_membered(B) % 0.57/1.09 & v5_membered(B) ) ) ) ). % 0.58/1.09 % 0.58/1.09 fof(cc2_membered,axiom, % 0.58/1.09 ! [A] : % 0.58/1.09 ( v4_membered(A) % 0.58/1.09 => v3_membered(A) ) ). % 0.58/1.09 % 0.58/1.09 fof(cc3_membered,axiom, % 0.58/1.09 ! [A] : % 0.58/1.09 ( v3_membered(A) % 0.58/1.09 => v2_membered(A) ) ). % 0.58/1.09 % 0.58/1.09 fof(cc4_membered,axiom, % 0.58/1.09 ! [A] : % 0.58/1.09 ( v2_membered(A) % 0.58/1.09 => v1_membered(A) ) ). % 0.58/1.09 % 0.58/1.09 fof(d3_pre_topc,axiom, % 0.58/1.09 ! [A] : % 0.58/1.09 ( one_sorted_str(A) % 0.58/1.09 => cast_as_carrier_subset(A) = the_carrier(A) ) ). % 0.58/1.09 % 0.58/1.09 fof(d4_tarski,axiom, % 0.58/1.09 ! [A,B] : % 0.58/1.09 ( B = union(A) % 0.58/1.09 <=> ! [C] : % 0.58/1.09 ( in(C,B) % 0.58/1.09 <=> ? [D] : % 0.58/1.09 ( in(C,D) % 0.58/1.09 & in(D,A) ) ) ) ). % 0.58/1.09 % 0.58/1.09 fof(d8_pre_topc,axiom, % 0.58/1.09 ! [A] : % 0.58/1.09 ( one_sorted_str(A) % 0.58/1.09 => ! [B] : % 0.58/1.09 ( element(B,powerset(powerset(the_carrier(A)))) % 0.58/1.09 => ( is_a_cover_of_carrier(A,B) % 0.58/1.09 <=> cast_as_carrier_subset(A) = union_of_subsets(the_carrier(A),B) ) ) ) ). % 0.58/1.09 % 0.58/1.09 fof(dt_k1_xboole_0,axiom, % 0.58/1.09 $true ). % 0.58/1.09 % 0.58/1.09 fof(dt_k1_zfmisc_1,axiom, % 0.58/1.09 $true ). % 0.58/1.09 % 0.58/1.09 fof(dt_k2_pre_topc,axiom, % 0.58/1.09 ! [A] : % 0.58/1.09 ( one_sorted_str(A) % 0.58/1.09 => element(cast_as_carrier_subset(A),powerset(the_carrier(A))) ) ). % 0.58/1.09 % 0.58/1.09 fof(dt_k3_tarski,axiom, % 0.58/1.09 $true ). % 0.58/1.09 % 0.58/1.09 fof(dt_k5_setfam_1,axiom, % 0.58/1.09 ! [A,B] : % 0.58/1.09 ( element(B,powerset(powerset(A))) % 0.58/1.09 => element(union_of_subsets(A,B),powerset(A)) ) ). % 0.58/1.09 % 0.58/1.09 fof(dt_l1_struct_0,axiom, % 0.58/1.09 $true ). % 0.58/1.09 % 0.58/1.09 fof(dt_m1_subset_1,axiom, % 0.58/1.09 $true ). % 0.58/1.09 % 0.58/1.09 fof(dt_u1_struct_0,axiom, % 0.58/1.09 $true ). % 0.58/1.09 % 0.58/1.09 fof(existence_l1_struct_0,axiom, % 0.58/1.09 ? [A] : one_sorted_str(A) ). % 0.58/1.09 % 0.58/1.09 fof(existence_m1_subset_1,axiom, % 0.58/1.09 ! [A] : % 0.58/1.09 ? [B] : element(B,A) ). % 0.58/1.09 % 0.58/1.09 fof(fc1_struct_0,axiom, % 0.58/1.09 ! [A] : % 0.58/1.09 ( ( ~ empty_carrier(A) % 0.58/1.09 & one_sorted_str(A) ) % 0.58/1.09 => ~ empty(the_carrier(A)) ) ). % 0.58/1.09 % 0.58/1.09 fof(fc1_subset_1,axiom, % 0.58/1.09 ! [A] : ~ empty(powerset(A)) ). % 0.58/1.09 % 0.58/1.09 fof(fc2_pre_topc,axiom, % 0.58/1.09 ! [A] : % 0.58/1.09 ( ( ~ empty_carrier(A) % 0.58/1.09 & one_sorted_str(A) ) % 0.58/1.09 => ~ empty(cast_as_carrier_subset(A)) ) ). % 0.58/1.09 % 0.58/1.09 fof(fc6_membered,axiom, % 0.58/1.09 ( empty(empty_set) % 0.58/1.09 & v1_membered(empty_set) % 0.58/1.09 & v2_membered(empty_set) % 0.58/1.09 & v3_membered(empty_set) % 0.58/1.09 & v4_membered(empty_set) % 0.58/1.09 & v5_membered(empty_set) ) ). % 0.58/1.09 % 0.58/1.09 fof(rc1_membered,axiom, % 0.58/1.09 ? [A] : % 0.58/1.09 ( ~ empty(A) % 0.58/1.09 & v1_membered(A) % 0.58/1.09 & v2_membered(A) % 0.58/1.09 & v3_membered(A) % 0.58/1.09 & v4_membered(A) % 0.58/1.09 & v5_membered(A) ) ). % 0.58/1.09 % 0.58/1.09 fof(rc1_subset_1,axiom, % 0.58/1.09 ! [A] : % 0.58/1.09 ( ~ empty(A) % 0.58/1.09 => ? [B] : % 0.58/1.09 ( element(B,powerset(A)) % 0.58/1.09 & ~ empty(B) ) ) ). % 0.58/1.09 % 0.58/1.09 fof(rc2_subset_1,axiom, % 0.58/1.09 ! [A] : % 0.58/1.09 ? [B] : % 0.58/1.09 ( element(B,powerset(A)) % 0.58/1.09 & empty(B) ) ). % 0.58/1.09 % 0.58/1.09 fof(rc3_struct_0,axiom, % 0.58/1.09 ? [A] : % 0.58/1.09 ( one_sorted_str(A) % 0.58/1.09 & ~ empty_carrier(A) ) ). % 0.58/1.09 % 0.58/1.09 fof(rc5_struct_0,axiom, % 0.58/1.09 ! [A] : % 0.58/1.09 ( ( ~ empty_carrier(A) % 0.58/1.09 & one_sorted_str(A) ) % 0.58/1.09 => ? [B] : % 0.58/1.09 ( element(B,powerset(the_carrier(A))) % 0.58/1.09 & ~ empty(B) ) ) ). % 0.58/1.09 % 0.58/1.09 fof(redefinition_k5_setfam_1,axiom, % 0.58/1.09 ! [A,B] : % 0.58/1.09 ( element(B,powerset(powerset(A))) % 0.58/1.09 => union_of_subsets(A,B) = union(B) ) ). % 0.58/1.09 % 0.58/1.09 fof(reflexivity_r1_tarski,axiom, % 0.58/1.09 ! [A,B] : subset(A,A) ). % 0.58/1.09 % 0.58/1.09 fof(t1_subset,axiom, % 0.58/1.09 ! [A,B] : % 0.58/1.09 ( in(A,B) % 0.58/1.09 => element(A,B) ) ). % 0.58/1.09 % 0.58/1.09 fof(t2_subset,axiom, % 0.58/1.09 ! [A,B] : % 0.58/1.09 ( element(A,B) % 0.58/1.09 => ( empty(B) % 0.58/1.09 | in(A,B) ) ) ). % 0.58/1.09 % 0.58/1.09 fof(t3_subset,axiom, % 0.58/1.09 ! [A,B] : % 0.58/1.09 ( element(A,powerset(B)) % 0.58/1.09 <=> subset(A,B) ) ). % 0.58/1.09 % 0.58/1.09 fof(t4_subset,axiom, % 0.58/1.09 ! [A,B,C] : % 0.58/1.09 ( ( in(A,B) % 0.58/1.09 & element(B,powerset(C)) ) % 0.58/1.09 => element(A,C) ) ). % 0.58/1.09 % 0.58/1.09 fof(t5_subset,axiom, % 0.58/1.09 ! [A,B,C] : % 0.58/1.09 ~ ( in(A,B) % 0.58/1.09 & element(B,powerset(C)) % 0.58/1.09 & empty(C) ) ). % 0.58/1.09 % 0.58/1.09 fof(t5_tops_2,conjecture, % 0.58/1.09 ! [A] : % 0.58/1.09 ( ( ~ empty_carrier(A) % 0.58/1.09 & one_sorted_str(A) ) % 0.58/1.09 => ! [B] : % 0.58/1.09 ( element(B,powerset(powerset(the_carrier(A)))) % 0.58/1.09 => ~ ( is_a_cover_of_carrier(A,B) % 0.58/1.09 & B = empty_set ) ) ) ). % 0.58/1.09 % 0.58/1.09 fof(t6_boole,axiom, % 0.58/1.09 ! [A] : % 0.58/1.09 ( empty(A) % 0.58/1.09 => A = empty_set ) ). % 0.58/1.09 % 0.58/1.09 fof(t7_boole,axiom, % 0.58/1.09 ! [A,B] : % 0.58/1.09 ~ ( in(A,B) % 0.58/1.09 & empty(B) ) ). % 0.58/1.09 % 0.58/1.09 fof(t8_boole,axiom, % 0.58/1.09 ! [A,B] : % 0.58/1.09 ~ ( empty(A) % 0.58/1.09 & A != B % 0.58/1.09 & empty(B) ) ). % 0.58/1.09 % 0.58/1.09 %------------------------------------------------------------------------------ % 0.58/1.09 %------------------------------------------- % 0.58/1.09 % Proof found % 0.58/1.09 % SZS status Theorem for theBenchmark % 0.58/1.09 % SZS output start Proof % 0.58/1.09 %ClaNum:133(EqnAxiom:41) % 0.58/1.09 %VarNum:288(SingletonVarNum:128) % 0.58/1.09 %MaxLitNum:4 % 0.58/1.09 %MaxfuncDepth:3 % 0.58/1.09 %SharedTerms:29 % 0.58/1.09 %goalClause: 42 56 58 62 65 % 0.58/1.09 %singleGoalClaCount:5 % 0.58/1.09 [42]E(a1,a2) % 0.58/1.09 [43]P1(a2) % 0.58/1.09 [44]P1(a6) % 0.58/1.09 [45]P11(a2) % 0.58/1.09 [46]P11(a6) % 0.58/1.09 [47]P15(a2) % 0.58/1.09 [48]P15(a6) % 0.58/1.09 [49]P16(a2) % 0.58/1.09 [50]P16(a6) % 0.58/1.09 [51]P17(a2) % 0.58/1.09 [52]P17(a6) % 0.58/1.09 [53]P2(a2) % 0.58/1.09 [54]P4(a7) % 0.58/1.09 [55]P4(a12) % 0.58/1.09 [56]P4(a4) % 0.58/1.09 [58]P5(a4,a1) % 0.58/1.09 [63]~P2(a6) % 0.58/1.09 [64]~P6(a12) % 0.58/1.09 [65]~P6(a4) % 0.58/1.09 [62]P3(a1,f15(f15(f16(a4)))) % 0.58/1.09 [59]P9(x591,x591) % 0.58/1.09 [57]P2(f13(x571)) % 0.58/1.09 [60]P3(f11(x601),x601) % 0.58/1.09 [61]P3(f13(x611),f15(x611)) % 0.58/1.09 [66]~P2(f15(x661)) % 0.58/1.09 [67]~P2(x671)+E(x671,a2) % 0.58/1.09 [68]~P11(x681)+P1(x681) % 0.58/1.09 [69]~P2(x691)+P1(x691) % 0.58/1.09 [70]~P15(x701)+P11(x701) % 0.58/1.09 [71]~P2(x711)+P11(x711) % 0.58/1.09 [72]~P16(x721)+P15(x721) % 0.58/1.09 [73]~P2(x731)+P15(x731) % 0.58/1.09 [74]~P17(x741)+P16(x741) % 0.58/1.09 [75]~P2(x751)+P16(x751) % 0.58/1.09 [76]~P2(x761)+P17(x761) % 0.58/1.09 [77]~P4(x771)+E(f3(x771),f16(x771)) % 0.58/1.09 [79]P2(x791)+~P2(f14(x791)) % 0.58/1.09 [84]P2(x841)+P3(f14(x841),f15(x841)) % 0.58/1.09 [119]~P4(x1191)+P3(f3(x1191),f15(f16(x1191))) % 0.58/1.09 [83]~P2(x831)+~P7(x832,x831) % 0.58/1.09 [100]~P7(x1001,x1002)+P3(x1001,x1002) % 0.58/1.09 [118]~P7(x1182,x1181)+~P7(x1181,x1182) % 0.58/1.09 [102]~P9(x1021,x1022)+P3(x1021,f15(x1022)) % 0.58/1.09 [120]P9(x1201,x1202)+~P3(x1201,f15(x1202)) % 0.58/1.09 [125]E(f18(x1251,x1252),f17(x1252))+~P3(x1252,f15(f15(x1251))) % 0.58/1.09 [127]P3(f18(x1271,x1272),f15(x1271))+~P3(x1272,f15(f15(x1271))) % 0.58/1.09 [80]~P4(x801)+P6(x801)+~P2(f3(x801)) % 0.58/1.09 [81]~P4(x811)+P6(x811)+~P2(f16(x811)) % 0.58/1.09 [82]~P4(x821)+P6(x821)+~P2(f5(x821)) % 0.58/1.09 [121]~P4(x1211)+P6(x1211)+P3(f5(x1211),f15(f16(x1211))) % 0.58/1.09 [78]~P2(x782)+~P2(x781)+E(x781,x782) % 0.58/1.09 [85]~P3(x851,x852)+P12(x851)+~P1(x852) % 0.58/1.09 [86]~P3(x861,x862)+P12(x861)+~P11(x862) % 0.58/1.09 [87]~P3(x871,x872)+P12(x871)+~P15(x872) % 0.58/1.09 [88]~P3(x881,x882)+P12(x881)+~P16(x882) % 0.58/1.09 [89]~P3(x891,x892)+P12(x891)+~P17(x892) % 0.58/1.09 [90]~P3(x901,x902)+P14(x901)+~P11(x902) % 0.58/1.09 [91]~P3(x911,x912)+P14(x911)+~P15(x912) % 0.58/1.10 [92]~P3(x921,x922)+P14(x921)+~P16(x922) % 0.58/1.10 [93]~P3(x931,x932)+P14(x931)+~P17(x932) % 0.58/1.10 [94]~P3(x941,x942)+P13(x941)+~P15(x942) % 0.58/1.10 [95]~P3(x951,x952)+P13(x951)+~P16(x952) % 0.58/1.10 [96]~P3(x961,x962)+P13(x961)+~P17(x962) % 0.58/1.10 [97]~P3(x971,x972)+P10(x971)+~P16(x972) % 0.58/1.10 [98]~P3(x981,x982)+P10(x981)+~P17(x982) % 0.58/1.10 [99]~P3(x991,x992)+P8(x991)+~P17(x992) % 0.58/1.10 [101]~P3(x1012,x1011)+P2(x1011)+P7(x1012,x1011) % 0.58/1.10 [103]P1(x1031)+~P1(x1032)+~P3(x1031,f15(x1032)) % 0.58/1.10 [104]P1(x1041)+~P11(x1042)+~P3(x1041,f15(x1042)) % 0.58/1.10 [105]P1(x1051)+~P15(x1052)+~P3(x1051,f15(x1052)) % 0.58/1.10 [106]P1(x1061)+~P16(x1062)+~P3(x1061,f15(x1062)) % 0.58/1.10 [107]P1(x1071)+~P17(x1072)+~P3(x1071,f15(x1072)) % 0.58/1.10 [108]P11(x1081)+~P11(x1082)+~P3(x1081,f15(x1082)) % 0.58/1.10 [109]P11(x1091)+~P15(x1092)+~P3(x1091,f15(x1092)) % 0.58/1.10 [110]P11(x1101)+~P16(x1102)+~P3(x1101,f15(x1102)) % 0.58/1.10 [111]P11(x1111)+~P17(x1112)+~P3(x1111,f15(x1112)) % 0.58/1.10 [112]P15(x1121)+~P15(x1122)+~P3(x1121,f15(x1122)) % 0.58/1.10 [113]P15(x1131)+~P16(x1132)+~P3(x1131,f15(x1132)) % 0.58/1.10 [114]P15(x1141)+~P17(x1142)+~P3(x1141,f15(x1142)) % 0.58/1.10 [115]P16(x1151)+~P16(x1152)+~P3(x1151,f15(x1152)) % 0.58/1.10 [116]P16(x1161)+~P17(x1162)+~P3(x1161,f15(x1162)) % 0.58/1.10 [117]P17(x1171)+~P17(x1172)+~P3(x1171,f15(x1172)) % 0.58/1.10 [126]P7(f8(x1262,x1261),x1261)+P7(f10(x1262,x1261),x1262)+E(x1261,f17(x1262)) % 0.58/1.10 [128]P7(f8(x1282,x1281),x1281)+P7(f8(x1282,x1281),f10(x1282,x1281))+E(x1281,f17(x1282)) % 0.58/1.10 [122]~P2(x1221)+~P7(x1222,x1223)+~P3(x1223,f15(x1221)) % 0.58/1.10 [124]P3(x1241,x1242)+~P7(x1241,x1243)+~P3(x1243,f15(x1242)) % 0.58/1.10 [131]~P7(x1311,x1313)+~E(x1313,f17(x1312))+P7(x1311,f9(x1312,x1313,x1311)) % 0.58/1.10 [132]~P7(x1323,x1322)+~E(x1322,f17(x1321))+P7(f9(x1321,x1322,x1323),x1321) % 0.58/1.10 [129]~P4(x1291)+~P5(x1291,x1292)+E(f18(f16(x1291),x1292),f3(x1291))+~P3(x1292,f15(f15(f16(x1291)))) % 0.58/1.10 [130]~P4(x1301)+P5(x1301,x1302)+~E(f18(f16(x1301),x1302),f3(x1301))+~P3(x1302,f15(f15(f16(x1301)))) % 0.58/1.10 [133]~P7(x1333,x1332)+~P7(f8(x1332,x1331),x1333)+~P7(f8(x1332,x1331),x1331)+E(x1331,f17(x1332)) % 0.58/1.10 [123]~P7(x1231,x1234)+P7(x1231,x1232)+~P7(x1234,x1233)+~E(x1232,f17(x1233)) % 0.58/1.10 %EqnAxiom % 0.58/1.10 [1]E(x11,x11) % 0.58/1.10 [2]E(x22,x21)+~E(x21,x22) % 0.58/1.10 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.58/1.10 [4]~E(x41,x42)+E(f13(x41),f13(x42)) % 0.58/1.10 [5]~E(x51,x52)+E(f11(x51),f11(x52)) % 0.58/1.10 [6]~E(x61,x62)+E(f8(x61,x63),f8(x62,x63)) % 0.58/1.10 [7]~E(x71,x72)+E(f8(x73,x71),f8(x73,x72)) % 0.58/1.10 [8]~E(x81,x82)+E(f15(x81),f15(x82)) % 0.58/1.10 [9]~E(x91,x92)+E(f16(x91),f16(x92)) % 0.58/1.10 [10]~E(x101,x102)+E(f17(x101),f17(x102)) % 0.58/1.10 [11]~E(x111,x112)+E(f9(x111,x113,x114),f9(x112,x113,x114)) % 0.58/1.10 [12]~E(x121,x122)+E(f9(x123,x121,x124),f9(x123,x122,x124)) % 0.58/1.10 [13]~E(x131,x132)+E(f9(x133,x134,x131),f9(x133,x134,x132)) % 0.58/1.10 [14]~E(x141,x142)+E(f5(x141),f5(x142)) % 0.58/1.10 [15]~E(x151,x152)+E(f3(x151),f3(x152)) % 0.58/1.10 [16]~E(x161,x162)+E(f10(x161,x163),f10(x162,x163)) % 0.58/1.10 [17]~E(x171,x172)+E(f10(x173,x171),f10(x173,x172)) % 0.58/1.10 [18]~E(x181,x182)+E(f14(x181),f14(x182)) % 0.58/1.10 [19]~E(x191,x192)+E(f18(x191,x193),f18(x192,x193)) % 0.58/1.10 [20]~E(x201,x202)+E(f18(x203,x201),f18(x203,x202)) % 0.58/1.10 [21]~P1(x211)+P1(x212)+~E(x211,x212) % 0.58/1.10 [22]P7(x222,x223)+~E(x221,x222)+~P7(x221,x223) % 0.58/1.10 [23]P7(x233,x232)+~E(x231,x232)+~P7(x233,x231) % 0.58/1.10 [24]~P11(x241)+P11(x242)+~E(x241,x242) % 0.58/1.10 [25]P3(x252,x253)+~E(x251,x252)+~P3(x251,x253) % 0.58/1.10 [26]P3(x263,x262)+~E(x261,x262)+~P3(x263,x261) % 0.58/1.10 [27]~P15(x271)+P15(x272)+~E(x271,x272) % 0.58/1.10 [28]~P2(x281)+P2(x282)+~E(x281,x282) % 0.58/1.10 [29]~P16(x291)+P16(x292)+~E(x291,x292) % 0.58/1.10 [30]~P12(x301)+P12(x302)+~E(x301,x302) % 0.58/1.10 [31]~P17(x311)+P17(x312)+~E(x311,x312) % 0.58/1.10 [32]~P4(x321)+P4(x322)+~E(x321,x322) % 0.58/1.10 [33]~P6(x331)+P6(x332)+~E(x331,x332) % 0.58/1.10 [34]~P14(x341)+P14(x342)+~E(x341,x342) % 0.58/1.10 [35]P5(x352,x353)+~E(x351,x352)+~P5(x351,x353) % 0.58/1.10 [36]P5(x363,x362)+~E(x361,x362)+~P5(x363,x361) % 0.58/1.10 [37]~P10(x371)+P10(x372)+~E(x371,x372) % 0.58/1.10 [38]~P13(x381)+P13(x382)+~E(x381,x382) % 0.58/1.10 [39]~P8(x391)+P8(x392)+~E(x391,x392) % 0.58/1.10 [40]P9(x402,x403)+~E(x401,x402)+~P9(x401,x403) % 0.58/1.10 [41]P9(x413,x412)+~E(x411,x412)+~P9(x413,x411) % 0.58/1.10 % 0.58/1.10 %------------------------------------------- % 0.58/1.10 cnf(134,plain, % 0.58/1.10 (~P7(x1341,x1342)+P7(x1341,f17(x1343))+~P7(x1342,x1343)), % 0.58/1.10 inference(equality_inference,[],[123])). % 0.58/1.10 cnf(136,plain, % 0.58/1.10 (~P7(x1361,f17(x1362))+P7(f9(x1362,f17(x1362),x1361),x1362)), % 0.58/1.10 inference(equality_inference,[],[132])). % 0.58/1.10 cnf(137,plain, % 0.58/1.10 (E(a2,a1)), % 0.58/1.10 inference(scs_inference,[],[42,2])). % 0.58/1.10 cnf(138,plain, % 0.58/1.10 (~P7(x1381,a2)), % 0.58/1.10 inference(scs_inference,[],[42,53,2,83])). % 0.58/1.10 cnf(142,plain, % 0.58/1.10 (E(f18(f16(a4),a1),f17(a1))), % 0.58/1.10 inference(scs_inference,[],[42,62,53,2,83,120,125])). % 0.58/1.10 cnf(144,plain, % 0.58/1.10 (P3(f18(f16(a4),a1),f15(f16(a4)))), % 0.58/1.10 inference(scs_inference,[],[42,62,53,2,83,120,125,127])). % 0.58/1.10 cnf(146,plain, % 0.58/1.10 (~P7(x1461,f17(a2))), % 0.58/1.10 inference(scs_inference,[],[42,62,53,2,83,120,125,127,136])). % 0.58/1.10 cnf(149,plain, % 0.58/1.10 (P11(a1)), % 0.58/1.10 inference(scs_inference,[],[42,62,43,45,53,2,83,120,125,127,136,21,24])). % 0.58/1.10 cnf(150,plain, % 0.58/1.10 (P3(a2,f15(f15(f16(a4))))), % 0.58/1.10 inference(scs_inference,[],[42,62,43,45,53,2,83,120,125,127,136,21,24,25])). % 0.58/1.10 cnf(152,plain, % 0.58/1.10 (P3(f11(x1521),x1521)), % 0.58/1.10 inference(rename_variables,[],[60])). % 0.58/1.10 cnf(153,plain, % 0.58/1.10 (P15(a1)), % 0.58/1.10 inference(scs_inference,[],[42,62,60,43,45,47,53,2,83,120,125,127,136,21,24,25,26,27])). % 0.58/1.10 cnf(154,plain, % 0.58/1.10 (P2(a1)), % 0.58/1.10 inference(scs_inference,[],[42,62,60,43,45,47,53,2,83,120,125,127,136,21,24,25,26,27,28])). % 0.58/1.10 cnf(155,plain, % 0.58/1.10 (P16(a1)), % 0.58/1.10 inference(scs_inference,[],[42,62,60,43,45,47,49,53,2,83,120,125,127,136,21,24,25,26,27,28,29])). % 0.58/1.10 cnf(156,plain, % 0.58/1.10 (P17(a1)), % 0.58/1.10 inference(scs_inference,[],[42,62,60,43,45,47,49,51,53,2,83,120,125,127,136,21,24,25,26,27,28,29,31])). % 0.58/1.10 cnf(157,plain, % 0.58/1.10 (P5(a4,a2)), % 0.58/1.10 inference(scs_inference,[],[42,58,62,60,43,45,47,49,51,53,2,83,120,125,127,136,21,24,25,26,27,28,29,31,36])). % 0.58/1.10 cnf(159,plain, % 0.58/1.10 (P9(x1591,x1591)), % 0.58/1.10 inference(rename_variables,[],[59])). % 0.58/1.10 cnf(162,plain, % 0.58/1.10 (P7(f11(a6),a6)), % 0.58/1.10 inference(scs_inference,[],[42,58,62,59,159,60,152,43,45,47,49,51,53,63,2,83,120,125,127,136,21,24,25,26,27,28,29,31,36,40,41,101])). % 0.58/1.10 cnf(163,plain, % 0.58/1.10 (P3(f11(x1631),x1631)), % 0.58/1.10 inference(rename_variables,[],[60])). % 0.58/1.10 cnf(165,plain, % 0.58/1.10 (P1(f11(f15(a2)))), % 0.58/1.10 inference(scs_inference,[],[42,58,62,59,159,60,152,163,43,45,47,49,51,53,63,2,83,120,125,127,136,21,24,25,26,27,28,29,31,36,40,41,101,103])). % 0.58/1.10 cnf(166,plain, % 0.58/1.10 (P3(f11(x1661),x1661)), % 0.58/1.10 inference(rename_variables,[],[60])). % 0.58/1.10 cnf(169,plain, % 0.58/1.10 (P3(f13(x1691),f15(x1691))), % 0.58/1.10 inference(rename_variables,[],[61])). % 0.58/1.10 cnf(171,plain, % 0.58/1.10 (P11(f11(f15(a2)))), % 0.58/1.10 inference(scs_inference,[],[42,58,62,59,159,60,152,163,166,61,43,45,47,49,51,53,63,2,83,120,125,127,136,21,24,25,26,27,28,29,31,36,40,41,101,103,104,108])). % 0.58/1.10 cnf(172,plain, % 0.58/1.10 (P3(f11(x1721),x1721)), % 0.58/1.10 inference(rename_variables,[],[60])). % 0.58/1.10 cnf(175,plain, % 0.58/1.10 (P3(f13(x1751),f15(x1751))), % 0.58/1.10 inference(rename_variables,[],[61])). % 0.58/1.10 cnf(177,plain, % 0.58/1.10 (P15(f11(f15(a2)))), % 0.58/1.10 inference(scs_inference,[],[42,58,62,59,159,60,152,163,166,172,61,169,43,45,47,49,51,53,63,2,83,120,125,127,136,21,24,25,26,27,28,29,31,36,40,41,101,103,104,108,109,112])). % 0.58/1.10 cnf(178,plain, % 0.58/1.10 (P3(f11(x1781),x1781)), % 0.58/1.10 inference(rename_variables,[],[60])). % 0.58/1.10 cnf(181,plain, % 0.58/1.10 (P3(f13(x1811),f15(x1811))), % 0.58/1.10 inference(rename_variables,[],[61])). % 0.58/1.10 cnf(183,plain, % 0.58/1.10 (P16(f11(f15(a2)))), % 0.58/1.10 inference(scs_inference,[],[42,58,62,59,159,60,152,163,166,172,178,61,169,175,43,45,47,49,51,53,63,2,83,120,125,127,136,21,24,25,26,27,28,29,31,36,40,41,101,103,104,108,109,112,113,115])). % 0.58/1.10 cnf(184,plain, % 0.58/1.10 (P3(f11(x1841),x1841)), % 0.58/1.10 inference(rename_variables,[],[60])). % 0.58/1.10 cnf(189,plain, % 0.58/1.10 (P17(f11(f15(a2)))), % 0.58/1.10 inference(scs_inference,[],[42,58,62,59,159,60,152,163,166,172,178,184,61,169,175,181,43,45,47,49,51,53,63,2,83,120,125,127,136,21,24,25,26,27,28,29,31,36,40,41,101,103,104,108,109,112,113,115,116,117])). % 0.58/1.10 cnf(190,plain, % 0.58/1.10 (P3(f11(x1901),x1901)), % 0.58/1.10 inference(rename_variables,[],[60])). % 0.58/1.10 cnf(192,plain, % 0.58/1.10 (~P7(x1921,f11(f15(a2)))), % 0.58/1.10 inference(scs_inference,[],[42,58,62,59,159,60,152,163,166,172,178,184,190,61,169,175,181,43,45,47,49,51,53,63,2,83,120,125,127,136,21,24,25,26,27,28,29,31,36,40,41,101,103,104,108,109,112,113,115,116,117,122])). % 0.58/1.10 cnf(195,plain, % 0.58/1.10 (E(f11(f15(a2)),f17(f17(a2)))), % 0.58/1.10 inference(scs_inference,[],[42,58,62,59,159,60,152,163,166,172,178,184,190,61,169,175,181,43,45,47,49,51,53,63,2,83,120,125,127,136,21,24,25,26,27,28,29,31,36,40,41,101,103,104,108,109,112,113,115,116,117,122,126])). % 0.58/1.10 cnf(197,plain, % 0.58/1.10 (E(f18(f16(a4),a1),f3(a4))), % 0.58/1.10 inference(scs_inference,[],[42,56,58,62,59,159,60,152,163,166,172,178,184,190,61,169,175,181,43,45,47,49,51,53,63,2,83,120,125,127,136,21,24,25,26,27,28,29,31,36,40,41,101,103,104,108,109,112,113,115,116,117,122,126,129])). % 0.58/1.10 cnf(207,plain, % 0.58/1.10 (E(f18(f16(a4),a2),f17(a2))), % 0.58/1.10 inference(scs_inference,[],[150,120,125])). % 0.58/1.10 cnf(209,plain, % 0.58/1.10 (E(f17(a1),f18(f16(a4),a1))), % 0.58/1.10 inference(scs_inference,[],[150,142,120,125,2])). % 0.58/1.10 cnf(210,plain, % 0.58/1.10 (~P7(x2101,a1)), % 0.58/1.10 inference(scs_inference,[],[150,154,142,120,125,2,83])). % 0.58/1.10 cnf(212,plain, % 0.58/1.10 (~P7(x2121,f17(f11(f15(a2))))), % 0.58/1.10 inference(scs_inference,[],[150,154,192,142,120,125,2,83,136])). % 0.58/1.10 cnf(213,plain, % 0.58/1.10 (~P7(x2131,f11(f15(a2)))), % 0.58/1.10 inference(rename_variables,[],[192])). % 0.58/1.10 cnf(215,plain, % 0.58/1.10 (P3(f18(f16(a4),a2),f15(f16(a4)))), % 0.58/1.10 inference(scs_inference,[],[150,154,192,142,120,125,2,83,136,127])). % 0.58/1.10 cnf(218,plain, % 0.58/1.10 (~P7(x2181,f11(f15(a2)))), % 0.58/1.10 inference(rename_variables,[],[192])). % 0.58/1.10 cnf(221,plain, % 0.58/1.10 (P3(f11(x2211),x2211)), % 0.58/1.10 inference(rename_variables,[],[60])). % 0.58/1.10 cnf(224,plain, % 0.58/1.10 (P3(f13(x2241),f15(x2241))), % 0.58/1.10 inference(rename_variables,[],[61])). % 0.58/1.10 cnf(227,plain, % 0.58/1.10 (P3(f11(x2271),x2271)), % 0.58/1.10 inference(rename_variables,[],[60])). % 0.58/1.10 cnf(230,plain, % 0.58/1.10 (P3(f13(x2301),f15(x2301))), % 0.58/1.10 inference(rename_variables,[],[61])). % 0.58/1.10 cnf(233,plain, % 0.58/1.10 (P3(f11(x2331),x2331)), % 0.58/1.10 inference(rename_variables,[],[60])). % 0.58/1.10 cnf(236,plain, % 0.58/1.10 (P3(f13(x2361),f15(x2361))), % 0.58/1.10 inference(rename_variables,[],[61])). % 0.58/1.10 cnf(239,plain, % 0.58/1.10 (P3(f11(x2391),x2391)), % 0.58/1.10 inference(rename_variables,[],[60])). % 0.58/1.10 cnf(241,plain, % 0.58/1.10 (~P7(x2411,f11(f15(a1)))), % 0.58/1.10 inference(scs_inference,[],[150,153,154,155,156,192,213,142,162,60,221,227,233,239,61,224,230,120,125,2,83,136,127,132,105,106,110,111,114,112,116,122])). % 0.58/1.10 cnf(242,plain, % 0.58/1.10 (P3(f11(x2421),x2421)), % 0.58/1.10 inference(rename_variables,[],[60])). % 0.58/1.10 cnf(251,plain, % 0.58/1.10 (P3(f17(a1),f15(f16(a4)))), % 0.58/1.10 inference(scs_inference,[],[150,153,154,155,156,192,213,142,144,171,195,162,60,221,227,233,239,242,61,224,230,236,120,125,2,83,136,127,132,105,106,110,111,114,112,116,122,117,24,115,25])). % 0.58/1.10 cnf(255,plain, % 0.58/1.10 (~E(a6,f11(f15(a2)))), % 0.58/1.10 inference(scs_inference,[],[62,150,153,154,155,156,192,213,218,142,144,171,195,162,66,60,221,227,233,239,242,61,224,230,236,120,125,2,83,136,127,132,105,106,110,111,114,112,116,122,117,24,115,25,101,23])). % 0.58/1.10 cnf(256,plain, % 0.58/1.10 (~P7(x2561,f11(f15(a2)))), % 0.58/1.10 inference(rename_variables,[],[192])). % 0.58/1.10 cnf(257,plain, % 0.58/1.10 (P17(f17(f17(a2)))), % 0.58/1.10 inference(scs_inference,[],[62,150,153,154,155,156,192,213,218,142,144,171,189,195,162,66,60,221,227,233,239,242,61,224,230,236,120,125,2,83,136,127,132,105,106,110,111,114,112,116,122,117,24,115,25,101,23,31])). % 0.58/1.10 cnf(258,plain, % 0.58/1.10 (P7(f8(f11(f15(a2)),a6),a6)), % 0.58/1.10 inference(scs_inference,[],[62,150,153,154,155,156,192,213,218,256,142,144,171,189,195,162,66,60,221,227,233,239,242,61,224,230,236,120,125,2,83,136,127,132,105,106,110,111,114,112,116,122,117,24,115,25,101,23,31,126])). % 0.58/1.10 cnf(262,plain, % 0.58/1.10 (P7(a2,f15(f15(f16(a4))))), % 0.58/1.10 inference(scs_inference,[],[42,62,150,153,154,155,156,192,213,218,256,142,144,171,183,189,195,162,66,60,221,227,233,239,242,61,224,230,236,120,125,2,83,136,127,132,105,106,110,111,114,112,116,122,117,24,115,25,101,23,31,126,29,22])). % 0.58/1.10 cnf(264,plain, % 0.58/1.10 (P15(f17(f17(a2)))), % 0.58/1.10 inference(scs_inference,[],[42,62,150,153,154,155,156,192,213,218,256,142,144,165,171,177,183,189,195,162,66,60,221,227,233,239,242,61,224,230,236,120,125,2,83,136,127,132,105,106,110,111,114,112,116,122,117,24,115,25,101,23,31,126,29,22,21,27])). % 0.58/1.10 cnf(265,plain, % 0.58/1.10 (E(f17(a1),f3(a4))), % 0.58/1.10 inference(scs_inference,[],[42,62,150,153,154,155,156,192,213,218,256,142,144,165,171,177,183,189,195,197,162,66,60,221,227,233,239,242,61,224,230,236,120,125,2,83,136,127,132,105,106,110,111,114,112,116,122,117,24,115,25,101,23,31,126,29,22,21,27,3])). % 0.58/1.10 cnf(266,plain, % 0.58/1.10 (E(f18(f16(a4),a2),f3(a4))), % 0.58/1.10 inference(scs_inference,[],[42,62,56,150,153,154,155,156,157,192,213,218,256,142,144,165,171,177,183,189,195,197,162,66,60,221,227,233,239,242,61,224,230,236,120,125,2,83,136,127,132,105,106,110,111,114,112,116,122,117,24,115,25,101,23,31,126,29,22,21,27,3,129])). % 0.58/1.10 cnf(278,plain, % 0.58/1.10 (~P7(x2781,f13(x2782))), % 0.58/1.10 inference(scs_inference,[],[251,57,120,83])). % 0.58/1.10 cnf(280,plain, % 0.58/1.10 (E(f3(a4),f17(a1))), % 0.58/1.10 inference(scs_inference,[],[251,265,57,120,83,2])). % 0.58/1.10 cnf(285,plain, % 0.58/1.10 (P3(f13(x2851),f15(x2851))), % 0.58/1.10 inference(rename_variables,[],[61])). % 0.58/1.10 cnf(287,plain, % 0.58/1.10 (P1(f13(f17(f17(a2))))), % 0.58/1.10 inference(scs_inference,[],[257,251,265,241,57,61,285,120,83,2,136,127,107])). % 0.58/1.10 cnf(288,plain, % 0.58/1.10 (P3(f13(x2881),f15(x2881))), % 0.58/1.10 inference(rename_variables,[],[61])). % 0.58/1.10 cnf(290,plain, % 0.58/1.10 (P11(f13(f17(f17(a2))))), % 0.58/1.10 inference(scs_inference,[],[257,264,251,265,241,57,61,285,288,120,83,2,136,127,107,109])). % 0.58/1.10 cnf(291,plain, % 0.58/1.10 (P3(f13(x2911),f15(x2911))), % 0.58/1.10 inference(rename_variables,[],[61])). % 0.58/1.10 cnf(293,plain, % 0.58/1.10 (P15(f13(f17(f17(a2))))), % 0.58/1.10 inference(scs_inference,[],[257,264,251,265,241,57,61,285,288,291,120,83,2,136,127,107,109,114])). % 0.58/1.10 cnf(294,plain, % 0.58/1.10 (P3(f13(x2941),f15(x2941))), % 0.58/1.10 inference(rename_variables,[],[61])). % 0.58/1.10 cnf(296,plain, % 0.58/1.10 (P16(f13(f17(f17(a2))))), % 0.58/1.10 inference(scs_inference,[],[257,264,251,265,241,57,61,285,288,291,294,120,83,2,136,127,107,109,114,116])). % 0.58/1.10 cnf(297,plain, % 0.58/1.10 (P3(f13(x2971),f15(x2971))), % 0.58/1.10 inference(rename_variables,[],[61])). % 0.58/1.10 cnf(299,plain, % 0.58/1.10 (P17(f13(f17(f17(a2))))), % 0.58/1.10 inference(scs_inference,[],[257,264,251,265,241,57,61,285,288,291,294,297,120,83,2,136,127,107,109,114,116,117])). % 0.58/1.10 cnf(303,plain, % 0.58/1.10 (~P7(x3031,f18(f16(a4),a2))), % 0.58/1.10 inference(scs_inference,[],[209,257,264,251,265,241,207,138,57,61,285,288,291,294,297,120,83,2,136,127,107,109,114,116,117,40,132])). % 0.58/1.10 cnf(314,plain, % 0.58/1.10 (P3(f3(a4),f15(f16(a4)))), % 0.58/1.10 inference(scs_inference,[],[209,257,264,251,265,149,154,212,241,215,146,266,207,138,57,61,285,288,291,294,297,120,83,2,136,127,107,109,114,116,117,40,132,122,108,126,25])). % 0.58/1.10 cnf(333,plain, % 0.58/1.10 (~P7(x3331,f17(f13(x3332)))), % 0.58/1.10 inference(scs_inference,[],[314,278,120,136])). % 0.58/1.10 cnf(334,plain, % 0.58/1.10 (~P7(x3341,f13(x3342))), % 0.58/1.10 inference(rename_variables,[],[278])). % 0.58/1.10 cnf(336,plain, % 0.58/1.10 (E(f17(f17(a2)),f11(f15(a2)))), % 0.58/1.10 inference(scs_inference,[],[314,195,278,120,136,2])). % 0.58/1.10 cnf(338,plain, % 0.58/1.10 (~P7(x3381,f13(x3382))), % 0.58/1.10 inference(rename_variables,[],[278])). % 0.58/1.10 cnf(340,plain, % 0.58/1.10 (E(f13(x3401),f17(f18(f16(a4),a2)))), % 0.58/1.10 inference(scs_inference,[],[262,314,195,278,334,338,303,120,136,2,132,126])). % 0.58/1.10 cnf(342,plain, % 0.58/1.10 (~P7(x3421,f13(x3422))), % 0.58/1.10 inference(rename_variables,[],[278])). % 0.58/1.10 cnf(344,plain, % 0.58/1.10 (P1(f17(f18(f16(a4),a2)))), % 0.58/1.10 inference(scs_inference,[],[262,314,195,278,334,338,303,287,120,136,2,132,126,21])). % 0.58/1.10 cnf(345,plain, % 0.58/1.10 (P11(f17(f18(f16(a4),a2)))), % 0.58/1.10 inference(scs_inference,[],[262,314,195,278,334,338,303,287,290,120,136,2,132,126,21,24])). % 0.58/1.10 cnf(346,plain, % 0.58/1.10 (P3(f17(f17(a2)),f15(a2))), % 0.58/1.10 inference(scs_inference,[],[262,314,195,60,278,334,338,303,287,290,120,136,2,132,126,21,24,25])). % 0.58/1.10 cnf(349,plain, % 0.58/1.10 (P16(f17(f18(f16(a4),a2)))), % 0.58/1.10 inference(scs_inference,[],[280,209,262,314,195,60,278,334,338,303,287,290,296,120,136,2,132,126,21,24,25,3,29])). % 0.58/1.10 cnf(352,plain, % 0.58/1.10 (P15(f17(f18(f16(a4),a2)))), % 0.58/1.10 inference(scs_inference,[],[280,209,262,314,195,60,278,334,338,342,303,287,290,293,296,120,136,2,132,126,21,24,25,3,29,23,27])). % 0.58/1.10 cnf(355,plain, % 0.58/1.10 (P2(f17(f18(f16(a4),a2)))), % 0.58/1.10 inference(scs_inference,[],[280,209,262,314,195,60,278,334,338,342,303,287,290,293,296,57,120,136,2,132,126,21,24,25,3,29,23,27,106,28])). % 0.58/1.10 cnf(357,plain, % 0.58/1.10 (~P7(x3571,f17(f17(a2)))), % 0.58/1.10 inference(scs_inference,[],[280,209,262,314,195,60,278,334,338,342,303,287,290,293,296,57,53,120,136,2,132,126,21,24,25,3,29,23,27,106,28,122])). % 0.58/1.10 cnf(359,plain, % 0.58/1.10 (P17(f17(f18(f16(a4),a2)))), % 0.58/1.10 inference(scs_inference,[],[280,209,262,314,195,60,278,334,338,342,303,287,290,293,296,299,57,53,120,136,2,132,126,21,24,25,3,29,23,27,106,28,122,31])). % 0.58/1.10 cnf(374,plain, % 0.58/1.10 (~P7(x3741,f17(f17(f13(x3742))))), % 0.58/1.10 inference(scs_inference,[],[346,333,120,136])). % 0.58/1.10 cnf(375,plain, % 0.58/1.10 (~P7(x3751,f17(f13(x3752)))), % 0.58/1.10 inference(rename_variables,[],[333])). % 0.58/1.10 cnf(377,plain, % 0.58/1.10 (E(f17(f18(f16(a4),a2)),f13(x3771))), % 0.58/1.10 inference(scs_inference,[],[346,333,340,120,136,2])). % 0.58/1.10 cnf(379,plain, % 0.58/1.10 (~P7(x3791,f3(a4))), % 0.58/1.10 inference(scs_inference,[],[137,280,346,333,340,210,120,136,2,41,132])). % 0.58/1.10 cnf(382,plain, % 0.58/1.10 (P9(f11(f15(a2)),a2)), % 0.58/1.10 inference(scs_inference,[],[137,336,280,346,333,340,210,120,136,2,41,132,40])). % 0.58/1.10 cnf(383,plain, % 0.58/1.10 (P17(f13(x3831))), % 0.58/1.10 inference(scs_inference,[],[137,336,280,359,346,333,340,210,120,136,2,41,132,40,31])). % 0.58/1.10 cnf(384,plain, % 0.58/1.10 (E(f17(f13(x3841)),f17(f17(f17(a2))))), % 0.58/1.10 inference(scs_inference,[],[137,336,280,359,346,333,375,340,357,210,120,136,2,41,132,40,31,126])). % 0.58/1.10 cnf(386,plain, % 0.58/1.10 (~P7(x3861,f17(f13(x3862)))), % 0.58/1.10 inference(rename_variables,[],[333])). % 0.58/1.10 cnf(388,plain, % 0.58/1.10 (P3(f17(f18(f16(a4),a2)),f15(x3881))), % 0.58/1.10 inference(scs_inference,[],[137,336,280,359,346,61,333,375,340,357,210,120,136,2,41,132,40,31,126,25])). % 0.58/1.10 cnf(390,plain, % 0.58/1.10 (~E(a6,f17(f17(a2)))), % 0.58/1.10 inference(scs_inference,[],[137,336,280,255,359,346,61,333,375,340,357,210,120,136,2,41,132,40,31,126,25,3])). % 0.58/1.10 cnf(391,plain, % 0.58/1.10 (P1(f13(x3911))), % 0.58/1.10 inference(scs_inference,[],[137,336,280,255,344,359,346,61,333,375,340,357,210,120,136,2,41,132,40,31,126,25,3,21])). % 0.58/1.10 cnf(392,plain, % 0.58/1.10 (P15(f13(x3921))), % 0.58/1.10 inference(scs_inference,[],[137,336,280,255,344,352,359,346,61,333,375,340,357,210,120,136,2,41,132,40,31,126,25,3,21,27])). % 0.58/1.10 cnf(393,plain, % 0.58/1.10 (P11(f13(x3931))), % 0.58/1.10 inference(scs_inference,[],[137,336,280,255,344,345,352,359,346,61,333,375,340,357,210,120,136,2,41,132,40,31,126,25,3,21,27,24])). % 0.58/1.10 cnf(394,plain, % 0.58/1.10 (P16(f13(x3941))), % 0.58/1.10 inference(scs_inference,[],[137,336,280,255,344,345,349,352,359,346,61,333,375,340,357,210,120,136,2,41,132,40,31,126,25,3,21,27,24,29])). % 0.58/1.10 cnf(395,plain, % 0.58/1.10 (~E(a6,f17(f13(x3951)))), % 0.58/1.10 inference(scs_inference,[],[137,336,280,255,344,345,349,352,359,346,61,258,333,375,386,340,357,210,120,136,2,41,132,40,31,126,25,3,21,27,24,29,23])). % 0.58/1.10 cnf(404,plain, % 0.58/1.10 (~P7(x4041,f17(f3(a4)))), % 0.58/1.10 inference(scs_inference,[],[388,379,120,136])). % 0.58/1.10 cnf(405,plain, % 0.58/1.10 (~P7(x4051,f3(a4))), % 0.58/1.10 inference(rename_variables,[],[379])). % 0.58/1.10 cnf(407,plain, % 0.58/1.10 (E(f17(f17(f17(a2))),f17(f13(x4071)))), % 0.58/1.10 inference(scs_inference,[],[388,384,379,120,136,2])). % 0.58/1.10 cnf(409,plain, % 0.58/1.10 (P3(f11(x4091),x4091)), % 0.58/1.10 inference(rename_variables,[],[60])). % 0.58/1.10 cnf(412,plain, % 0.58/1.10 (P3(f11(x4121),x4121)), % 0.58/1.10 inference(rename_variables,[],[60])). % 0.58/1.10 cnf(415,plain, % 0.58/1.10 (P3(f11(x4151),x4151)), % 0.58/1.10 inference(rename_variables,[],[60])). % 0.58/1.10 cnf(418,plain, % 0.58/1.10 (P3(f11(x4181),x4181)), % 0.58/1.10 inference(rename_variables,[],[60])). % 0.58/1.10 cnf(433,plain, % 0.58/1.10 (~E(a6,f17(f17(f13(x4331))))), % 0.58/1.10 inference(scs_inference,[],[137,377,262,383,388,395,382,162,60,409,412,415,418,374,384,379,405,278,120,136,2,116,107,111,114,117,132,41,126,40,25,3,23])). % 0.58/1.10 cnf(435,plain, % 0.58/1.10 (E(f18(x4351,f13(x4352)),f17(f13(x4352)))), % 0.58/1.10 inference(scs_inference,[],[137,377,262,383,388,395,382,162,60,409,412,415,418,374,384,379,405,278,120,136,2,116,107,111,114,117,132,41,126,40,25,3,23,125])). % 0.58/1.10 cnf(439,plain, % 0.58/1.10 (P3(f18(x4391,f13(x4392)),f15(x4391))), % 0.58/1.10 inference(scs_inference,[],[137,377,262,383,388,395,382,162,60,409,412,415,418,374,384,379,405,278,120,136,2,116,107,111,114,117,132,41,126,40,25,3,23,125,118,127])). % 0.58/1.10 cnf(449,plain, % 0.58/1.10 (~P7(x4491,f18(f13(x4492),f13(x4493)))), % 0.58/1.10 inference(scs_inference,[],[137,377,262,383,392,393,394,388,395,382,162,60,409,412,415,418,57,374,384,379,405,278,120,136,2,116,107,111,114,117,132,41,126,40,25,3,23,125,118,127,134,104,109,113,122])). % 0.58/1.10 cnf(454,plain, % 0.58/1.10 (P15(f17(f13(x4541)))), % 0.58/1.10 inference(scs_inference,[],[137,377,262,383,392,393,394,388,395,382,162,60,409,412,415,418,57,374,384,379,405,278,120,136,2,116,107,111,114,117,132,41,126,40,25,3,23,125,118,127,134,104,109,113,122,115,27])). % 0.58/1.10 cnf(455,plain, % 0.58/1.10 (P16(f17(f13(x4551)))), % 0.58/1.10 inference(scs_inference,[],[137,377,262,383,392,393,394,388,395,382,162,60,409,412,415,418,57,374,384,379,405,278,120,136,2,116,107,111,114,117,132,41,126,40,25,3,23,125,118,127,134,104,109,113,122,115,27,29])). % 0.58/1.10 cnf(456,plain, % 0.58/1.10 (P11(f17(f13(x4561)))), % 0.58/1.10 inference(scs_inference,[],[137,377,262,383,392,393,394,388,395,382,162,60,409,412,415,418,57,374,384,379,405,278,120,136,2,116,107,111,114,117,132,41,126,40,25,3,23,125,118,127,134,104,109,113,122,115,27,29,24])). % 0.58/1.10 cnf(457,plain, % 0.58/1.10 (P1(f17(f13(x4571)))), % 0.58/1.10 inference(scs_inference,[],[137,377,262,383,392,393,394,388,395,382,162,60,409,412,415,418,57,374,384,379,405,278,120,136,2,116,107,111,114,117,132,41,126,40,25,3,23,125,118,127,134,104,109,113,122,115,27,29,24,21])). % 0.58/1.10 cnf(466,plain, % 0.58/1.10 (P3(f18(x4661,f18(f15(x4661),f13(x4662))),f15(x4661))), % 0.58/1.10 inference(scs_inference,[],[60,439,120,127])). % 0.58/1.10 cnf(467,plain, % 0.58/1.10 (P3(f18(x4671,f13(x4672)),f15(x4671))), % 0.58/1.10 inference(rename_variables,[],[439])). % 0.58/1.10 cnf(470,plain, % 0.58/1.10 (~P7(x4701,f18(f13(x4702),f13(x4703)))), % 0.58/1.10 inference(rename_variables,[],[449])). % 0.58/1.10 cnf(472,plain, % 0.58/1.10 (E(f17(f13(x4721)),f18(x4722,f13(x4721)))), % 0.58/1.10 inference(scs_inference,[],[60,439,435,449,120,127,136,2])). % 0.58/1.10 cnf(474,plain, % 0.58/1.10 (P3(f18(x4741,f13(x4742)),f15(x4741))), % 0.58/1.10 inference(rename_variables,[],[439])). % 0.58/1.10 cnf(477,plain, % 0.58/1.10 (P3(f18(x4771,f13(x4772)),f15(x4771))), % 0.58/1.10 inference(rename_variables,[],[439])). % 0.58/1.10 cnf(482,plain, % 0.58/1.10 (P3(f18(x4821,f13(x4822)),f15(x4821))), % 0.58/1.10 inference(rename_variables,[],[439])). % 0.58/1.10 cnf(485,plain, % 0.58/1.10 (P3(f18(x4851,f13(x4852)),f15(x4851))), % 0.58/1.10 inference(rename_variables,[],[439])). % 0.58/1.10 cnf(488,plain, % 0.58/1.10 (P3(f18(x4881,f13(x4882)),f15(x4881))), % 0.58/1.10 inference(rename_variables,[],[439])). % 0.58/1.10 cnf(493,plain, % 0.58/1.10 (P3(f18(x4931,f13(x4932)),f15(x4931))), % 0.58/1.10 inference(rename_variables,[],[439])). % 0.58/1.10 cnf(496,plain, % 0.58/1.10 (P3(f18(x4961,f13(x4962)),f15(x4961))), % 0.58/1.10 inference(rename_variables,[],[439])). % 0.58/1.10 cnf(501,plain, % 0.58/1.10 (P3(f18(x5011,f13(x5012)),f15(x5011))), % 0.58/1.10 inference(rename_variables,[],[439])). % 0.58/1.10 cnf(506,plain, % 0.58/1.10 (~P7(x5061,f18(a1,f13(x5062)))), % 0.58/1.10 inference(scs_inference,[],[407,154,391,454,455,456,359,392,394,60,439,467,474,477,482,485,488,493,496,501,435,449,278,120,127,136,2,116,108,103,113,105,117,110,107,111,112,114,132,122])). % 0.58/1.10 cnf(507,plain, % 0.58/1.10 (P3(f18(x5071,f13(x5072)),f15(x5071))), % 0.58/1.10 inference(rename_variables,[],[439])). % 0.58/1.10 cnf(510,plain, % 0.58/1.10 (P3(f18(x5101,f13(x5102)),f15(x5101))), % 0.58/1.10 inference(rename_variables,[],[439])). % 0.58/1.10 cnf(513,plain, % 0.58/1.10 (P17(f17(f13(x5131)))), % 0.58/1.10 inference(scs_inference,[],[42,407,154,391,454,455,456,359,392,394,60,439,467,474,477,482,485,488,493,496,501,507,435,449,278,120,127,136,2,116,108,103,113,105,117,110,107,111,112,114,132,122,115,41,31])). % 0.58/1.10 cnf(514,plain, % 0.58/1.10 (E(f18(x5141,f13(x5142)),f17(f13(x5142)))), % 0.58/1.10 inference(rename_variables,[],[435])). % 0.58/1.10 cnf(515,plain, % 0.58/1.10 (E(f18(f13(x5151),f13(x5152)),f17(f17(f3(a4))))), % 0.58/1.10 inference(scs_inference,[],[42,407,154,391,454,455,456,359,392,394,60,439,467,474,477,482,485,488,493,496,501,507,435,449,470,404,278,120,127,136,2,116,108,103,113,105,117,110,107,111,112,114,132,122,115,41,31,126])). % 0.58/1.10 cnf(519,plain, % 0.58/1.10 (P3(f17(f13(x5191)),f15(x5192))), % 0.58/1.10 inference(scs_inference,[],[42,407,154,391,454,455,456,359,392,394,60,439,467,474,477,482,485,488,493,496,501,507,510,435,514,449,470,404,278,120,127,136,2,116,108,103,113,105,117,110,107,111,112,114,132,122,115,41,31,126,25])). % 0.58/1.10 cnf(521,plain, % 0.58/1.10 (P16(f17(f17(f17(a2))))), % 0.58/1.10 inference(scs_inference,[],[42,407,154,391,454,455,456,359,392,394,60,439,467,474,477,482,485,488,493,496,501,507,510,435,514,449,470,404,384,278,120,127,136,2,116,108,103,113,105,117,110,107,111,112,114,132,122,115,41,31,126,25,29])). % 0.58/1.10 cnf(522,plain, % 0.58/1.10 (E(f17(f13(x5221)),f17(f17(f17(a2))))), % 0.58/1.10 inference(rename_variables,[],[384])). % 0.58/1.10 cnf(523,plain, % 0.58/1.10 (~E(a6,f18(x5231,f13(x5232)))), % 0.58/1.10 inference(scs_inference,[],[42,407,395,154,391,454,455,456,359,392,394,60,439,467,474,477,482,485,488,493,496,501,507,510,435,514,449,470,404,384,278,120,127,136,2,116,108,103,113,105,117,110,107,111,112,114,132,122,115,41,31,126,25,29,3])). % 0.58/1.10 cnf(525,plain, % 0.58/1.10 (P15(f17(f17(f17(a2))))), % 0.58/1.10 inference(scs_inference,[],[42,407,395,154,391,454,455,456,359,392,394,60,439,467,474,477,482,485,488,493,496,501,507,510,435,514,449,470,404,384,522,278,120,127,136,2,116,108,103,113,105,117,110,107,111,112,114,132,122,115,41,31,126,25,29,3,27])). % 0.58/1.10 cnf(526,plain, % 0.58/1.10 (E(f17(f13(x5261)),f17(f17(f17(a2))))), % 0.58/1.10 inference(rename_variables,[],[384])). % 0.58/1.10 cnf(528,plain, % 0.58/1.10 (E(f17(f13(x5281)),f17(f17(f17(a2))))), % 0.58/1.10 inference(rename_variables,[],[384])). % 0.58/1.10 cnf(529,plain, % 0.58/1.10 (P11(f17(f17(f17(a2))))), % 0.58/1.10 inference(scs_inference,[],[42,407,395,154,391,454,455,456,457,359,392,394,60,439,467,474,477,482,485,488,493,496,501,507,510,435,514,449,470,404,384,522,526,528,278,120,127,136,2,116,108,103,113,105,117,110,107,111,112,114,132,122,115,41,31,126,25,29,3,27,21,24])). % 0.58/1.10 cnf(544,plain, % 0.58/1.10 (P3(f18(x5441,f17(f13(x5442))),f15(x5441))), % 0.58/1.10 inference(scs_inference,[],[519,120,127])). % 0.58/1.10 cnf(545,plain, % 0.58/1.10 (P3(f17(f13(x5451)),f15(x5452))), % 0.58/1.10 inference(rename_variables,[],[519])). % 0.58/1.10 cnf(550,plain, % 0.58/1.10 (E(f17(f17(f3(a4))),f18(f13(x5501),f13(x5502)))), % 0.58/1.10 inference(scs_inference,[],[519,515,506,120,127,136,2])). % 0.58/1.10 cnf(552,plain, % 0.58/1.10 (P3(f18(x5521,f13(x5522)),f15(x5521))), % 0.58/1.10 inference(rename_variables,[],[439])). % 0.58/1.10 cnf(555,plain, % 0.58/1.10 (P3(f18(x5551,f13(x5552)),f15(x5551))), % 0.58/1.10 inference(rename_variables,[],[439])). % 0.58/1.10 cnf(560,plain, % 0.58/1.10 (P3(f18(x5601,f13(x5602)),f15(x5601))), % 0.58/1.10 inference(rename_variables,[],[439])). % 0.58/1.10 cnf(569,plain, % 0.58/1.10 (P3(f18(x5691,f13(x5692)),f15(x5691))), % 0.58/1.10 inference(rename_variables,[],[439])). % 0.58/1.10 cnf(570,plain, % 0.58/1.10 (P17(f17(f13(x5701)))), % 0.58/1.10 inference(rename_variables,[],[513])). % 0.58/1.10 cnf(582,plain, % 0.58/1.10 (P17(f18(x5821,f13(x5822)))), % 0.58/1.10 inference(scs_inference,[],[472,154,433,519,513,570,521,525,529,454,456,466,515,506,439,552,555,560,569,333,120,127,136,2,104,113,116,109,107,108,112,117,122,115,40,126,31])). % 0.58/1.10 cnf(583,plain, % 0.58/1.10 (E(f17(f13(x5831)),f18(x5832,f13(x5831)))), % 0.58/1.10 inference(rename_variables,[],[472])). % 0.58/1.10 cnf(584,plain, % 0.58/1.10 (P3(f18(x5841,f13(x5842)),f15(x5843))), % 0.58/1.10 inference(scs_inference,[],[472,583,154,433,519,545,513,570,521,525,529,454,456,466,515,506,439,552,555,560,569,333,120,127,136,2,104,113,116,109,107,108,112,117,122,115,40,126,31,25])). % 0.58/1.10 cnf(586,plain, % 0.58/1.10 (P16(f18(x5861,f13(x5862)))), % 0.58/1.10 inference(scs_inference,[],[472,583,154,433,519,545,513,570,521,525,529,454,456,455,466,515,506,439,552,555,560,569,333,120,127,136,2,104,113,116,109,107,108,112,117,122,115,40,126,31,25,29])). % 0.58/1.10 cnf(587,plain, % 0.58/1.10 (E(f17(f13(x5871)),f18(x5872,f13(x5871)))), % 0.58/1.10 inference(rename_variables,[],[472])). % 0.58/1.10 cnf(589,plain, % 0.58/1.10 (E(f17(f13(x5891)),f18(x5892,f13(x5891)))), % 0.58/1.10 inference(rename_variables,[],[472])). % 0.58/1.10 cnf(590,plain, % 0.58/1.10 (E(f17(f13(x5901)),f17(f17(f3(a4))))), % 0.58/1.10 inference(scs_inference,[],[472,583,587,589,154,433,519,545,513,570,521,525,529,457,454,456,455,466,515,506,439,552,555,560,569,333,120,127,136,2,104,113,116,109,107,108,112,117,122,115,40,126,31,25,29,21,3])). % 0.58/1.10 cnf(592,plain, % 0.58/1.10 (E(f17(f13(x5921)),f18(x5922,f13(x5921)))), % 0.58/1.10 inference(rename_variables,[],[472])). % 0.58/1.10 cnf(594,plain, % 0.58/1.10 (E(f17(f13(x5941)),f18(x5942,f13(x5941)))), % 0.58/1.10 inference(rename_variables,[],[472])). % 0.58/1.10 cnf(596,plain, % 0.58/1.10 (P15(f18(x5961,f13(x5962)))), % 0.58/1.10 inference(scs_inference,[],[472,583,587,589,592,594,154,433,519,545,513,570,521,525,529,457,454,456,455,466,515,506,439,552,555,560,569,333,120,127,136,2,104,113,116,109,107,108,112,117,122,115,40,126,31,25,29,21,3,24,27])). % 0.58/1.10 cnf(614,plain, % 0.58/1.10 (P3(f18(x6141,f18(x6142,f13(x6143))),f15(x6141))), % 0.58/1.10 inference(scs_inference,[],[584,404,120,136,127])). % 0.58/1.10 cnf(615,plain, % 0.58/1.10 (P3(f18(x6151,f13(x6152)),f15(x6153))), % 0.58/1.10 inference(rename_variables,[],[584])). % 0.58/1.10 cnf(619,plain, % 0.58/1.10 (P3(f18(x6191,f17(f13(x6192))),f15(x6191))), % 0.58/1.10 inference(rename_variables,[],[544])). % 0.58/1.10 cnf(622,plain, % 0.58/1.10 (P3(f18(x6221,f17(f13(x6222))),f15(x6221))), % 0.58/1.10 inference(rename_variables,[],[544])). % 0.58/1.10 cnf(629,plain, % 0.58/1.10 (P3(f18(x6291,f17(f13(x6292))),f15(x6291))), % 0.58/1.10 inference(rename_variables,[],[544])). % 0.58/1.10 cnf(632,plain, % 0.58/1.10 (P3(f18(x6321,f17(f13(x6322))),f15(x6321))), % 0.58/1.10 inference(rename_variables,[],[544])). % 0.58/1.10 cnf(639,plain, % 0.58/1.10 (~P7(x6391,f18(x6392,f13(x6393)))), % 0.58/1.10 inference(scs_inference,[],[154,584,615,582,586,596,590,404,544,619,622,629,632,120,136,127,2,106,109,105,111,113,117,116,114,122])). % 0.58/1.10 cnf(644,plain, % 0.58/1.10 (E(f17(f17(a2)),f17(f18(f16(a4),a2)))), % 0.58/1.10 inference(scs_inference,[],[154,584,615,582,586,596,590,303,357,404,544,619,622,629,632,120,136,127,2,106,109,105,111,113,117,116,114,122,115,126])). % 0.58/1.10 cnf(649,plain, % 0.58/1.10 (E(f17(f13(x6491)),f17(f17(f3(a4))))), % 0.58/1.10 inference(rename_variables,[],[590])). % 0.58/1.10 cnf(651,plain, % 0.58/1.10 (E(f17(f13(x6511)),f17(f17(f3(a4))))), % 0.58/1.10 inference(rename_variables,[],[590])). % 0.58/1.10 cnf(652,plain, % 0.58/1.10 (P3(f17(a2),f15(f16(a4)))), % 0.58/1.10 inference(scs_inference,[],[154,584,615,582,586,596,590,649,513,455,303,357,404,544,619,622,629,632,207,215,120,136,127,2,106,109,105,111,113,117,116,114,122,115,126,31,29,25])). % 0.58/1.10 cnf(654,plain, % 0.58/1.10 (E(f17(f13(x6541)),f17(f17(f3(a4))))), % 0.58/1.10 inference(rename_variables,[],[590])). % 0.58/1.10 cnf(656,plain, % 0.58/1.10 (E(f17(f13(x6561)),f17(f17(f3(a4))))), % 0.58/1.10 inference(rename_variables,[],[590])). % 0.58/1.10 cnf(659,plain, % 0.58/1.10 (~E(a6,f17(f17(f3(a4))))), % 0.58/1.10 inference(scs_inference,[],[550,154,523,584,615,582,586,596,590,649,651,654,656,457,513,454,455,456,303,357,404,544,619,622,629,632,207,215,120,136,127,2,106,109,105,111,113,117,116,114,122,115,126,31,29,25,24,21,27,3])). % 0.58/1.10 cnf(671,plain, % 0.58/1.10 (~P7(x6711,f17(a1))), % 0.58/1.10 inference(scs_inference,[],[652,210,120,136])). % 0.58/1.10 cnf(674,plain, % 0.58/1.10 (E(f17(f18(f16(a4),a2)),f17(f17(a2)))), % 0.58/1.10 inference(scs_inference,[],[652,210,644,120,136,2])). % 0.58/1.10 cnf(677,plain, % 0.58/1.10 (P2(f17(f17(a2)))), % 0.58/1.10 inference(scs_inference,[],[262,355,652,210,644,120,136,2,132,28])). % 0.58/1.10 cnf(686,plain, % 0.58/1.10 (E(f11(f15(a2)),f17(f18(f16(a4),a2)))), % 0.58/1.10 inference(scs_inference,[],[390,262,154,355,652,513,195,146,210,614,644,384,120,136,2,132,28,122,126,31,3])). % 0.58/1.10 cnf(705,plain, % 0.58/1.10 (P3(f18(x7051,f17(f13(x7052))),f15(x7051))), % 0.58/1.10 inference(rename_variables,[],[544])). % 0.58/1.10 cnf(710,plain, % 0.58/1.10 (E(f3(a4),f17(f18(f16(a4),a2)))), % 0.58/1.10 inference(scs_inference,[],[42,336,154,686,677,155,544,705,379,303,639,120,136,2,41,28,115,122,126])). % 0.58/1.10 cnf(714,plain, % 0.58/1.10 (~E(a6,f17(f18(f16(a4),a2)))), % 0.58/1.10 inference(scs_inference,[],[42,336,674,390,154,686,677,155,544,705,379,303,639,120,136,2,41,28,115,122,126,3])). % 0.58/1.10 cnf(725,plain, % 0.58/1.10 (~P7(x7251,f17(f17(a1)))), % 0.58/1.10 inference(scs_inference,[],[614,671,120,136])). % 0.58/1.10 cnf(763,plain, % 0.58/1.10 (E(f17(f18(f16(a4),a2)),f3(a4))), % 0.58/1.10 inference(scs_inference,[],[215,725,710,120,136,2])). % 0.58/1.10 cnf(801,plain, % 0.58/1.10 ($false), % 0.58/1.10 inference(scs_inference,[],[763,65,56,355,714,659,344,345,349,352,359,340,404,266,2,28,126,31,29,24,27,3,21,118,80]), % 0.58/1.10 ['proof']). % 0.58/1.10 % SZS output end Proof % 0.58/1.10 % Total time :0.450000s %------------------------------------------------------------------------------