%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : ITP006+1 : TPTP v8.2.0. Bugfixed v7.5.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n013.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 09:07:49 EDT 2024 % Result : Theorem 59.55s 59.67s % Output : CNFRefutation 59.67s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : ITP006+1 : TPTP v8.2.0. Bugfixed v7.5.0. % 0.07/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n013.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 : Wed Jun 19 02:34:24 EDT 2024 % 0.12/0.33 % CPUTime : % 0.62/0.64 start to proof:theBenchmark % 59.55/59.64 %------------------------------------------- % 59.55/59.64 % File :CSE---1.7 % 59.55/59.64 % Problem :theBenchmark % 59.55/59.64 % Transform :cnf % 59.55/59.64 % Format :tptp:raw % 59.55/59.64 % Command :java -jar mcs_scs.jar %d %s % 59.55/59.64 % 59.55/59.64 % Result :Theorem 58.890000s % 59.55/59.64 % Output :CNFRefutation 58.890000s % 59.55/59.64 %------------------------------------------- % 59.55/59.65 %------------------------------------------------------------------------------ % 59.55/59.65 % File : ITP006+1 : TPTP v8.2.0. Bugfixed v7.5.0. % 59.55/59.65 % Domain : Interactive Theorem Proving % 59.55/59.65 % Problem : HOL4 syntactic export of thm_2EquantHeuristics_2EGUESS__RULES__WEAKEN__FORALL__POINT.p, bushy mode % 59.55/59.65 % Version : [BG+19] axioms. % 59.55/59.65 % English : % 59.55/59.65 % 59.55/59.65 % Refs : [BG+19] Brown et al. (2019), GRUNGE: A Grand Unified ATP Chall % 59.55/59.65 % : [Gau19] Gauthier (2019), Email to Geoff Sutcliffe % 59.55/59.65 % Source : [BG+19] % 59.55/59.65 % Names : thm_2EquantHeuristics_2EGUESS__RULES__WEAKEN__FORALL__POINT.p [Gau19] % 59.55/59.65 % : HL402501+1.p [TPAP] % 59.55/59.65 % 59.55/59.65 % Status : Theorem % 59.55/59.65 % Rating : 0.44 v8.2.0, 0.50 v8.1.0, 0.53 v7.5.0 % 59.55/59.65 % Syntax : Number of formulae : 49 ( 15 unt; 0 def) % 59.55/59.65 % Number of atoms : 185 ( 30 equ) % 59.55/59.65 % Maximal formula atoms : 16 ( 3 avg) % 59.55/59.65 % Number of connectives : 177 ( 41 ~; 24 |; 26 &) % 59.55/59.65 % ( 45 <=>; 41 =>; 0 <=; 0 <~>) % 59.55/59.65 % Maximal formula depth : 16 ( 6 avg) % 59.55/59.65 % Maximal term depth : 11 ( 2 avg) % 59.55/59.65 % Number of predicates : 2 ( 1 usr; 0 prp; 1-2 aty) % 59.55/59.65 % Number of functors : 35 ( 35 usr; 19 con; 0-2 aty) % 59.55/59.65 % Number of variables : 141 ( 136 !; 5 ?) % 59.55/59.65 % SPC : FOF_THM_RFO_SEQ % 59.55/59.65 % 59.55/59.65 % Comments : % 59.55/59.65 % Bugfixes : v7.5.0 - Bugfixes in axioms and export. % 59.55/59.65 %------------------------------------------------------------------------------ % 59.55/59.65 fof(reserved_2Eho_2Eeq__ext,axiom, % 59.55/59.65 ! [A_27a,A_27b,V0f_2E0,V1g_2E0] : % 59.55/59.65 ( ! [V2x_2E0] : s(A_27b,app_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V0f_2E0),s(A_27a,V2x_2E0))) = s(A_27b,app_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V1g_2E0),s(A_27a,V2x_2E0))) % 59.55/59.65 => s(tyop_2Emin_2Efun(A_27a,A_27b),V0f_2E0) = s(tyop_2Emin_2Efun(A_27a,A_27b),V1g_2E0) ) ). % 59.55/59.65 % 59.55/59.65 fof(reserved_2Eho_2Eboolext,axiom, % 59.55/59.65 ! [V0_2E0,V1_2E0] : % 59.55/59.65 ( ( p(s(tyop_2Emin_2Ebool,V0_2E0)) % 59.55/59.65 <=> p(s(tyop_2Emin_2Ebool,V1_2E0)) ) % 59.55/59.65 => s(tyop_2Emin_2Ebool,V0_2E0) = s(tyop_2Emin_2Ebool,V1_2E0) ) ). % 59.55/59.65 % 59.55/59.65 fof(reserved_2Eho_2Etruth,axiom, % 59.55/59.65 p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) ). % 59.55/59.65 % 59.55/59.65 fof(reserved_2Eho_2Enotfalse,axiom, % 59.55/59.65 ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) ). % 59.55/59.65 % 59.55/59.65 fof(reserved_2Eho_2Ebool__cases__ax,axiom, % 59.55/59.65 ! [V0t_2E0] : % 59.55/59.65 ( s(tyop_2Emin_2Ebool,V0t_2E0) = s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) % 59.55/59.65 | s(tyop_2Emin_2Ebool,V0t_2E0) = s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) ) ). % 59.55/59.65 % 59.55/59.65 fof(reserved_2Eho_2Ei__thm,axiom, % 59.55/59.65 ! [A_27a,V0x_2E0] : s(A_27a,app_2E2(s(tyop_2Emin_2Efun(A_27a,A_27a),combin_i_2E0),s(A_27a,V0x_2E0))) = s(A_27a,V0x_2E0) ). % 59.55/59.65 % 59.55/59.65 fof(reserved_2Eho_2Ek__thm,axiom, % 59.55/59.65 ! [A_27a,A_27b,V0x_2E0,V1y_2E0] : s(A_27a,app_2E2(s(tyop_2Emin_2Efun(A_27b,A_27a),app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Efun(A_27b,A_27a)),combin_k_2E0),s(A_27a,V0x_2E0))),s(A_27b,V1y_2E0))) = s(A_27a,V0x_2E0) ). % 59.55/59.65 % 59.55/59.65 fof(reserved_2Eho_2Es__thm,axiom, % 59.55/59.65 ! [A_27a,A_27b,A_27c,V0f_2E0,V1g_2E0,V2x_2E0] : s(A_27c,app_2E2(s(tyop_2Emin_2Efun(A_27a,A_27c),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27a,A_27b),tyop_2Emin_2Efun(A_27a,A_27c)),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Efun(A_27b,A_27c)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27a,A_27b),tyop_2Emin_2Efun(A_27a,A_27c))),combin_s_2E0),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Efun(A_27b,A_27c)),V0f_2E0))),s(tyop_2Emin_2Efun(A_27a,A_27b),V1g_2E0))),s(A_27a,V2x_2E0))) = s(A_27c,app_2E2(s(tyop_2Emin_2Efun(A_27b,A_27c),app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Efun(A_27b,A_27c)),V0f_2E0),s(A_27a,V2x_2E0))),s(A_27b,app_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V1g_2E0),s(A_27a,V2x_2E0))))) ). % 59.55/59.65 % 59.55/59.65 fof(reserved_2Elogic_2E_2F_5C,axiom, % 59.55/59.65 ! [V0_2E0,V1_2E0] : % 59.55/59.65 ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_2F_5C_2E2(s(tyop_2Emin_2Ebool,V0_2E0),s(tyop_2Emin_2Ebool,V1_2E0)))) % 59.55/59.65 <=> ( p(s(tyop_2Emin_2Ebool,V0_2E0)) % 59.55/59.65 & p(s(tyop_2Emin_2Ebool,V1_2E0)) ) ) ). % 59.55/59.65 % 59.55/59.65 fof(reserved_2Elogic_2E_5C_2F,axiom, % 59.55/59.65 ! [V0_2E0,V1_2E0] : % 59.55/59.65 ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_5C_2F_2E2(s(tyop_2Emin_2Ebool,V0_2E0),s(tyop_2Emin_2Ebool,V1_2E0)))) % 59.55/59.65 <=> ( p(s(tyop_2Emin_2Ebool,V0_2E0)) % 59.55/59.65 | p(s(tyop_2Emin_2Ebool,V1_2E0)) ) ) ). % 59.55/59.65 % 59.55/59.65 fof(reserved_2Elogic_2E_7E,axiom, % 59.55/59.65 ! [V0_2E0] : % 59.55/59.65 ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_7E_2E1(s(tyop_2Emin_2Ebool,V0_2E0)))) % 59.55/59.65 <=> ~ p(s(tyop_2Emin_2Ebool,V0_2E0)) ) ). % 59.55/59.65 % 59.55/59.65 fof(reserved_2Elogic_2E_3D_3D_3E,axiom, % 59.55/59.65 ! [V0_2E0,V1_2E0] : % 59.55/59.65 ( p(s(tyop_2Emin_2Ebool,c_2Emin_2E_3D_3D_3E_2E2(s(tyop_2Emin_2Ebool,V0_2E0),s(tyop_2Emin_2Ebool,V1_2E0)))) % 59.55/59.65 <=> ( p(s(tyop_2Emin_2Ebool,V0_2E0)) % 59.55/59.65 => p(s(tyop_2Emin_2Ebool,V1_2E0)) ) ) ). % 59.55/59.65 % 59.55/59.65 fof(reserved_2Elogic_2E_3D,axiom, % 59.55/59.65 ! [A_27a,V0_2E0,V1_2E0] : % 59.55/59.65 ( p(s(tyop_2Emin_2Ebool,c_2Emin_2E_3D_2E2(s(A_27a,V0_2E0),s(A_27a,V1_2E0)))) % 59.55/59.65 <=> s(A_27a,V0_2E0) = s(A_27a,V1_2E0) ) ). % 59.55/59.65 % 59.55/59.65 fof(reserved_2Equant_2E_21,axiom, % 59.55/59.65 ! [A_27a,V0f_2E0] : % 59.55/59.65 ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_21_2E1(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V0f_2E0)))) % 59.55/59.65 <=> ! [V1x_2E0] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V0f_2E0),s(A_27a,V1x_2E0)))) ) ). % 59.55/59.65 % 59.55/59.65 fof(reserved_2Equant_2E_3F,axiom, % 59.55/59.65 ! [A_27a,V0f_2E0] : % 59.55/59.65 ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_3F_2E1(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V0f_2E0)))) % 59.55/59.66 <=> ? [V1x_2E0] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V0f_2E0),s(A_27a,V1x_2E0)))) ) ). % 59.55/59.66 % 59.55/59.66 fof(arityeq2_2Ec_2Ebool_2E_2F_5C_2E2,axiom, % 59.55/59.66 ! [X0_2E0,X1_2E0] : % 59.55/59.66 ( ( p(s(tyop_2Emin_2Ebool,X0_2E0)) % 59.55/59.66 & p(s(tyop_2Emin_2Ebool,X1_2E0)) ) % 59.55/59.66 <=> p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool)),c_2Ebool_2E_2F_5C_2E0),s(tyop_2Emin_2Ebool,X0_2E0))),s(tyop_2Emin_2Ebool,X1_2E0)))) ) ). % 59.55/59.66 % 59.55/59.66 fof(arityeq2_2Ec_2Ebool_2E_5C_2F_2E2,axiom, % 59.55/59.66 ! [X0_2E0,X1_2E0] : % 59.55/59.66 ( ( p(s(tyop_2Emin_2Ebool,X0_2E0)) % 59.55/59.66 | p(s(tyop_2Emin_2Ebool,X1_2E0)) ) % 59.55/59.66 <=> p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool)),c_2Ebool_2E_5C_2F_2E0),s(tyop_2Emin_2Ebool,X0_2E0))),s(tyop_2Emin_2Ebool,X1_2E0)))) ) ). % 59.55/59.66 % 59.55/59.66 fof(arityeq1_2Ec_2Ebool_2E_7E_2E1,axiom, % 59.55/59.66 ! [X0_2E0] : % 59.55/59.66 ( ~ p(s(tyop_2Emin_2Ebool,X0_2E0)) % 59.55/59.66 <=> p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool),c_2Ebool_2E_7E_2E0),s(tyop_2Emin_2Ebool,X0_2E0)))) ) ). % 59.55/59.66 % 59.55/59.66 fof(arityeq2_2Ec_2Emin_2E_3D_3D_3E_2E2,axiom, % 59.55/59.66 ! [X0_2E0,X1_2E0] : % 59.55/59.66 ( ( p(s(tyop_2Emin_2Ebool,X0_2E0)) % 59.55/59.66 => p(s(tyop_2Emin_2Ebool,X1_2E0)) ) % 59.55/59.66 <=> p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool)),c_2Emin_2E_3D_3D_3E_2E0),s(tyop_2Emin_2Ebool,X0_2E0))),s(tyop_2Emin_2Ebool,X1_2E0)))) ) ). % 59.55/59.66 % 59.55/59.66 fof(arityeq2_2Ec_2Emin_2E_3D_2E2_2Emono_2EA_27a,axiom, % 59.55/59.66 ! [A_27a,X0_2E0,X1_2E0] : % 59.55/59.66 ( s(A_27a,X0_2E0) = s(A_27a,X1_2E0) % 59.55/59.66 <=> p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool)),c_2Emin_2E_3D_2E0),s(A_27a,X0_2E0))),s(A_27a,X1_2E0)))) ) ). % 59.55/59.66 % 59.55/59.66 fof(arityeq1_2Ec_2Ebool_2E_21_2E1_2Emono_2EA_27a,axiom, % 59.55/59.66 ! [A_27a,X0_2E0] : s(tyop_2Emin_2Ebool,c_2Ebool_2E_21_2E1(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),X0_2E0))) = s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool),c_2Ebool_2E_21_2E0),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),X0_2E0))) ). % 59.55/59.66 % 59.55/59.66 fof(arityeq1_2Ec_2Ebool_2E_3F_2E1_2Emono_2EA_27a,axiom, % 59.55/59.66 ! [A_27a,X0_2E0] : s(tyop_2Emin_2Ebool,c_2Ebool_2E_3F_2E1(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),X0_2E0))) = s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool),c_2Ebool_2E_3F_2E0),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),X0_2E0))) ). % 59.55/59.66 % 59.55/59.66 fof(arityeq2_2Ec_2EquantHeuristics_2EGUESS__EXISTS_2E2_2Emono_2EA_27a_20mono_2EA_27b,axiom, % 59.55/59.66 ! [A_27a,A_27b,X0_2E0,X1_2E0] : s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),X0_2E0),s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),X1_2E0))) = s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27a,A_27b),tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool)),c_2EquantHeuristics_2EGUESS__EXISTS_2E0),s(tyop_2Emin_2Efun(A_27a,A_27b),X0_2E0))),s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),X1_2E0))) ). % 59.55/59.66 % 59.55/59.66 fof(arityeq2_2Ec_2EquantHeuristics_2EGUESS__EXISTS__GAP_2E2_2Emono_2EA_27a_20mono_2EA_27b,axiom, % 59.55/59.66 ! [A_27a,A_27b,X0_2E0,X1_2E0] : s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__GAP_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),X0_2E0),s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),X1_2E0))) = s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27a,A_27b),tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool)),c_2EquantHeuristics_2EGUESS__EXISTS__GAP_2E0),s(tyop_2Emin_2Efun(A_27a,A_27b),X0_2E0))),s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),X1_2E0))) ). % 59.55/59.66 % 59.55/59.66 fof(arityeq2_2Ec_2EquantHeuristics_2EGUESS__EXISTS__POINT_2E2_2Emono_2EA_27a_20mono_2EA_27b,axiom, % 59.55/59.66 ! [A_27a,A_27b,X0_2E0,X1_2E0] : s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__POINT_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),X0_2E0),s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),X1_2E0))) = s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27a,A_27b),tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool)),c_2EquantHeuristics_2EGUESS__EXISTS__POINT_2E0),s(tyop_2Emin_2Efun(A_27a,A_27b),X0_2E0))),s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),X1_2E0))) ). % 59.55/59.66 % 59.55/59.66 fof(arityeq2_2Ec_2EquantHeuristics_2EGUESS__FORALL_2E2_2Emono_2EA_27a_20mono_2EA_27b,axiom, % 59.55/59.66 ! [A_27a,A_27b,X0_2E0,X1_2E0] : s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),X0_2E0),s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),X1_2E0))) = s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27a,A_27b),tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool)),c_2EquantHeuristics_2EGUESS__FORALL_2E0),s(tyop_2Emin_2Efun(A_27a,A_27b),X0_2E0))),s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),X1_2E0))) ). % 59.55/59.66 % 59.55/59.66 fof(arityeq2_2Ec_2EquantHeuristics_2EGUESS__FORALL__GAP_2E2_2Emono_2EA_27a_20mono_2EA_27b,axiom, % 59.55/59.66 ! [A_27a,A_27b,X0_2E0,X1_2E0] : s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__GAP_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),X0_2E0),s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),X1_2E0))) = s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27a,A_27b),tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool)),c_2EquantHeuristics_2EGUESS__FORALL__GAP_2E0),s(tyop_2Emin_2Efun(A_27a,A_27b),X0_2E0))),s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),X1_2E0))) ). % 59.55/59.66 % 59.55/59.66 fof(arityeq2_2Ec_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2_2Emono_2EA_27a_20mono_2EA_27b,axiom, % 59.55/59.66 ! [A_27a,A_27b,X0_2E0,X1_2E0] : s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),X0_2E0),s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),X1_2E0))) = s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27a,A_27b),tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool)),c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E0),s(tyop_2Emin_2Efun(A_27a,A_27b),X0_2E0))),s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),X1_2E0))) ). % 59.55/59.66 % 59.55/59.66 fof(arityeq2_2Ec_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2_2Emono_2EA_27b_20mono_2EA_27a,axiom, % 59.55/59.66 ! [A_27a,A_27b,X0_2E0,X1_2E0] : s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(A_27b,A_27a),X0_2E0),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),X1_2E0))) = s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27b,A_27a),tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool)),c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E0),s(tyop_2Emin_2Efun(A_27b,A_27a),X0_2E0))),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),X1_2E0))) ). % 59.55/59.66 % 59.55/59.66 fof(thm_2Ebool_2ETRUTH,axiom, % 59.55/59.66 p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) ). % 59.55/59.66 % 59.55/59.66 fof(thm_2Ebool_2EIMP__CLAUSES,axiom, % 59.55/59.66 ! [V0t_2E0] : % 59.55/59.66 ( ( ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) % 59.55/59.66 => p(s(tyop_2Emin_2Ebool,V0t_2E0)) ) % 59.55/59.66 <=> p(s(tyop_2Emin_2Ebool,V0t_2E0)) ) % 59.55/59.66 & ( ( p(s(tyop_2Emin_2Ebool,V0t_2E0)) % 59.55/59.66 => p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) ) % 59.55/59.66 <=> p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) ) % 59.55/59.66 & ( ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) % 59.55/59.66 => p(s(tyop_2Emin_2Ebool,V0t_2E0)) ) % 59.55/59.66 <=> p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) ) % 59.55/59.66 & ( ( p(s(tyop_2Emin_2Ebool,V0t_2E0)) % 59.55/59.66 => p(s(tyop_2Emin_2Ebool,V0t_2E0)) ) % 59.55/59.66 <=> p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) ) % 59.55/59.66 & ( ( p(s(tyop_2Emin_2Ebool,V0t_2E0)) % 59.55/59.66 => p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) ) % 59.55/59.66 <=> ~ p(s(tyop_2Emin_2Ebool,V0t_2E0)) ) ) ). % 59.55/59.66 % 59.55/59.66 fof(thm_2Ebool_2ENOT__CLAUSES,axiom, % 59.55/59.66 ( ! [V0t_2E0] : % 59.55/59.66 ( ~ ~ p(s(tyop_2Emin_2Ebool,V0t_2E0)) % 59.55/59.66 <=> p(s(tyop_2Emin_2Ebool,V0t_2E0)) ) % 59.55/59.66 & ( ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) % 59.55/59.66 <=> p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) ) % 59.55/59.66 & ( ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) % 59.55/59.66 <=> p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) ) ) ). % 59.55/59.66 % 59.55/59.66 fof(thm_2Ebool_2EEQ__SYM__EQ,axiom, % 59.55/59.66 ! [A_27a,V0x_2E0,V1y_2E0] : % 59.55/59.66 ( s(A_27a,V0x_2E0) = s(A_27a,V1y_2E0) % 59.55/59.66 <=> s(A_27a,V1y_2E0) = s(A_27a,V0x_2E0) ) ). % 59.55/59.66 % 59.55/59.66 fof(thm_2Ebool_2EEQ__CLAUSES,axiom, % 59.55/59.66 ! [V0t_2E0] : % 59.55/59.66 ( ( s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) = s(tyop_2Emin_2Ebool,V0t_2E0) % 59.55/59.66 <=> p(s(tyop_2Emin_2Ebool,V0t_2E0)) ) % 59.55/59.66 & ( s(tyop_2Emin_2Ebool,V0t_2E0) = s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) % 59.55/59.66 <=> p(s(tyop_2Emin_2Ebool,V0t_2E0)) ) % 59.55/59.66 & ( s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) = s(tyop_2Emin_2Ebool,V0t_2E0) % 59.55/59.66 <=> ~ p(s(tyop_2Emin_2Ebool,V0t_2E0)) ) % 59.55/59.66 & ( s(tyop_2Emin_2Ebool,V0t_2E0) = s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) % 59.55/59.66 <=> ~ p(s(tyop_2Emin_2Ebool,V0t_2E0)) ) ) ). % 59.55/59.66 % 59.55/59.66 fof(thm_2Ebool_2EAND__IMP__INTRO,axiom, % 59.55/59.66 ! [V0t1_2E0,V1t2_2E0,V2t3_2E0] : % 59.55/59.66 ( ( p(s(tyop_2Emin_2Ebool,V0t1_2E0)) % 59.55/59.66 => ( p(s(tyop_2Emin_2Ebool,V1t2_2E0)) % 59.55/59.66 => p(s(tyop_2Emin_2Ebool,V2t3_2E0)) ) ) % 59.55/59.66 <=> ( ( p(s(tyop_2Emin_2Ebool,V0t1_2E0)) % 59.55/59.66 & p(s(tyop_2Emin_2Ebool,V1t2_2E0)) ) % 59.55/59.66 => p(s(tyop_2Emin_2Ebool,V2t3_2E0)) ) ) ). % 59.55/59.66 % 59.55/59.66 fof(thm_2Ebool_2EIMP__CONG,axiom, % 59.55/59.66 ! [V0x_2E0,V1x_27_2E0,V2y_2E0,V3y_27_2E0] : % 59.55/59.66 ( ( s(tyop_2Emin_2Ebool,V0x_2E0) = s(tyop_2Emin_2Ebool,V1x_27_2E0) % 59.55/59.66 & ( p(s(tyop_2Emin_2Ebool,V1x_27_2E0)) % 59.55/59.66 => s(tyop_2Emin_2Ebool,V2y_2E0) = s(tyop_2Emin_2Ebool,V3y_27_2E0) ) ) % 59.55/59.66 => ( ( p(s(tyop_2Emin_2Ebool,V0x_2E0)) % 59.55/59.66 => p(s(tyop_2Emin_2Ebool,V2y_2E0)) ) % 59.55/59.66 <=> ( p(s(tyop_2Emin_2Ebool,V1x_27_2E0)) % 59.55/59.66 => p(s(tyop_2Emin_2Ebool,V3y_27_2E0)) ) ) ) ). % 59.55/59.66 % 59.55/59.66 fof(thm_2EquantHeuristics_2EGUESS__REWRITES,axiom, % 59.55/59.66 ! [A_27a,A_27b,V0i_2E0,V1P_2E0] : % 59.55/59.66 ( ( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V0i_2E0),s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V1P_2E0)))) % 59.55/59.66 <=> ! [V2v_2E0] : % 59.55/59.66 ( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V1P_2E0),s(A_27b,V2v_2E0)))) % 59.55/59.66 => ? [V3fv_2E0] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V1P_2E0),s(A_27b,app_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V0i_2E0),s(A_27a,V3fv_2E0)))))) ) ) % 59.55/59.66 & ( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V0i_2E0),s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V1P_2E0)))) % 59.55/59.66 <=> ! [V4v_2E0] : % 59.55/59.66 ( ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V1P_2E0),s(A_27b,V4v_2E0)))) % 59.55/59.66 => ? [V5fv_2E0] : ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V1P_2E0),s(A_27b,app_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V0i_2E0),s(A_27a,V5fv_2E0)))))) ) ) % 59.55/59.66 & ! [V6i_2E0,V7P_2E0] : % 59.55/59.66 ( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__POINT_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V6i_2E0),s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V7P_2E0)))) % 59.55/59.66 <=> ! [V8fv_2E0] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V7P_2E0),s(A_27b,app_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V6i_2E0),s(A_27a,V8fv_2E0)))))) ) % 59.55/59.66 & ! [V9i_2E0,V10P_2E0] : % 59.55/59.66 ( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V9i_2E0),s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V10P_2E0)))) % 59.55/59.66 <=> ! [V11fv_2E0] : ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V10P_2E0),s(A_27b,app_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V9i_2E0),s(A_27a,V11fv_2E0)))))) ) % 59.55/59.66 & ! [V12i_2E0,V13P_2E0] : % 59.55/59.66 ( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__GAP_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V12i_2E0),s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V13P_2E0)))) % 59.55/59.66 <=> ! [V14v_2E0] : % 59.55/59.66 ( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V13P_2E0),s(A_27b,V14v_2E0)))) % 59.55/59.66 => ? [V15fv_2E0] : s(A_27b,V14v_2E0) = s(A_27b,app_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V12i_2E0),s(A_27a,V15fv_2E0))) ) ) % 59.55/59.66 & ! [V16i_2E0,V17P_2E0] : % 59.55/59.66 ( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__GAP_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V16i_2E0),s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V17P_2E0)))) % 59.55/59.66 <=> ! [V18v_2E0] : % 59.55/59.66 ( ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V17P_2E0),s(A_27b,V18v_2E0)))) % 59.55/59.66 => ? [V19fv_2E0] : s(A_27b,V18v_2E0) = s(A_27b,app_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V16i_2E0),s(A_27a,V19fv_2E0))) ) ) ) ). % 59.55/59.66 % 59.55/59.66 fof(thm_2Esat_2ENOT__NOT,axiom, % 59.55/59.66 ! [V0t_2E0] : % 59.55/59.66 ( ~ ~ p(s(tyop_2Emin_2Ebool,V0t_2E0)) % 59.55/59.66 <=> p(s(tyop_2Emin_2Ebool,V0t_2E0)) ) ). % 59.55/59.66 % 59.55/59.66 fof(thm_2Esat_2EAND__INV__IMP,axiom, % 59.55/59.66 ! [V0A_2E0] : % 59.55/59.66 ( p(s(tyop_2Emin_2Ebool,V0A_2E0)) % 59.55/59.66 => ( ~ p(s(tyop_2Emin_2Ebool,V0A_2E0)) % 59.55/59.66 => p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) ) ) ). % 59.55/59.66 % 59.55/59.66 fof(thm_2Esat_2EOR__DUAL2,axiom, % 59.55/59.66 ! [V0B_2E0,V1A_2E0] : % 59.55/59.66 ( ( ~ ( p(s(tyop_2Emin_2Ebool,V1A_2E0)) % 59.55/59.66 | p(s(tyop_2Emin_2Ebool,V0B_2E0)) ) % 59.55/59.66 => p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) ) % 59.55/59.66 <=> ( ( p(s(tyop_2Emin_2Ebool,V1A_2E0)) % 59.55/59.66 => p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) ) % 59.55/59.66 => ( ~ p(s(tyop_2Emin_2Ebool,V0B_2E0)) % 59.55/59.66 => p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) ) ) ) ). % 59.55/59.66 % 59.55/59.66 fof(thm_2Esat_2EOR__DUAL3,axiom, % 59.55/59.66 ! [V0B_2E0,V1A_2E0] : % 59.55/59.66 ( ( ~ ( ~ p(s(tyop_2Emin_2Ebool,V1A_2E0)) % 59.55/59.66 | p(s(tyop_2Emin_2Ebool,V0B_2E0)) ) % 59.55/59.66 => p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) ) % 59.55/59.66 <=> ( p(s(tyop_2Emin_2Ebool,V1A_2E0)) % 59.55/59.66 => ( ~ p(s(tyop_2Emin_2Ebool,V0B_2E0)) % 59.55/59.66 => p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) ) ) ) ). % 59.55/59.66 % 59.55/59.66 fof(thm_2Esat_2EAND__INV2,axiom, % 59.55/59.66 ! [V0A_2E0] : % 59.55/59.66 ( ( ~ p(s(tyop_2Emin_2Ebool,V0A_2E0)) % 59.55/59.66 => p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) ) % 59.55/59.66 => ( ( p(s(tyop_2Emin_2Ebool,V0A_2E0)) % 59.55/59.66 => p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) ) % 59.55/59.66 => p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) ) ) ). % 59.55/59.66 % 59.55/59.66 fof(thm_2Esat_2Edc__eq,axiom, % 59.55/59.66 ! [V0r_2E0,V1q_2E0,V2p_2E0] : % 59.55/59.66 ( ( p(s(tyop_2Emin_2Ebool,V2p_2E0)) % 59.55/59.66 <=> s(tyop_2Emin_2Ebool,V1q_2E0) = s(tyop_2Emin_2Ebool,V0r_2E0) ) % 59.55/59.66 <=> ( ( p(s(tyop_2Emin_2Ebool,V2p_2E0)) % 59.55/59.66 | p(s(tyop_2Emin_2Ebool,V1q_2E0)) % 59.55/59.66 | p(s(tyop_2Emin_2Ebool,V0r_2E0)) ) % 59.55/59.66 & ( p(s(tyop_2Emin_2Ebool,V2p_2E0)) % 59.55/59.66 | ~ p(s(tyop_2Emin_2Ebool,V0r_2E0)) % 59.55/59.66 | ~ p(s(tyop_2Emin_2Ebool,V1q_2E0)) ) % 59.55/59.66 & ( p(s(tyop_2Emin_2Ebool,V1q_2E0)) % 59.55/59.66 | ~ p(s(tyop_2Emin_2Ebool,V0r_2E0)) % 59.55/59.66 | ~ p(s(tyop_2Emin_2Ebool,V2p_2E0)) ) % 59.55/59.66 & ( p(s(tyop_2Emin_2Ebool,V0r_2E0)) % 59.55/59.66 | ~ p(s(tyop_2Emin_2Ebool,V1q_2E0)) % 59.55/59.66 | ~ p(s(tyop_2Emin_2Ebool,V2p_2E0)) ) ) ) ). % 59.55/59.66 % 59.55/59.66 fof(thm_2Esat_2Edc__disj,axiom, % 59.55/59.66 ! [V0r_2E0,V1q_2E0,V2p_2E0] : % 59.55/59.66 ( ( p(s(tyop_2Emin_2Ebool,V2p_2E0)) % 59.55/59.66 <=> ( p(s(tyop_2Emin_2Ebool,V1q_2E0)) % 59.55/59.66 | p(s(tyop_2Emin_2Ebool,V0r_2E0)) ) ) % 59.55/59.66 <=> ( ( p(s(tyop_2Emin_2Ebool,V2p_2E0)) % 59.55/59.66 | ~ p(s(tyop_2Emin_2Ebool,V1q_2E0)) ) % 59.55/59.66 & ( p(s(tyop_2Emin_2Ebool,V2p_2E0)) % 59.55/59.66 | ~ p(s(tyop_2Emin_2Ebool,V0r_2E0)) ) % 59.55/59.66 & ( p(s(tyop_2Emin_2Ebool,V1q_2E0)) % 59.55/59.66 | p(s(tyop_2Emin_2Ebool,V0r_2E0)) % 59.55/59.66 | ~ p(s(tyop_2Emin_2Ebool,V2p_2E0)) ) ) ) ). % 59.55/59.66 % 59.55/59.66 fof(thm_2Esat_2Edc__imp,axiom, % 59.55/59.66 ! [V0r_2E0,V1q_2E0,V2p_2E0] : % 59.55/59.66 ( ( p(s(tyop_2Emin_2Ebool,V2p_2E0)) % 59.55/59.66 <=> ( p(s(tyop_2Emin_2Ebool,V1q_2E0)) % 59.55/59.66 => p(s(tyop_2Emin_2Ebool,V0r_2E0)) ) ) % 59.55/59.66 <=> ( ( p(s(tyop_2Emin_2Ebool,V2p_2E0)) % 59.55/59.66 | p(s(tyop_2Emin_2Ebool,V1q_2E0)) ) % 59.55/59.66 & ( p(s(tyop_2Emin_2Ebool,V2p_2E0)) % 59.55/59.66 | ~ p(s(tyop_2Emin_2Ebool,V0r_2E0)) ) % 59.55/59.66 & ( ~ p(s(tyop_2Emin_2Ebool,V1q_2E0)) % 59.55/59.66 | p(s(tyop_2Emin_2Ebool,V0r_2E0)) % 59.55/59.66 | ~ p(s(tyop_2Emin_2Ebool,V2p_2E0)) ) ) ) ). % 59.55/59.66 % 59.55/59.66 fof(thm_2Esat_2Edc__neg,axiom, % 59.55/59.66 ! [V0q_2E0,V1p_2E0] : % 59.55/59.67 ( ( p(s(tyop_2Emin_2Ebool,V1p_2E0)) % 59.55/59.67 <=> ~ p(s(tyop_2Emin_2Ebool,V0q_2E0)) ) % 59.55/59.67 <=> ( ( p(s(tyop_2Emin_2Ebool,V1p_2E0)) % 59.55/59.67 | p(s(tyop_2Emin_2Ebool,V0q_2E0)) ) % 59.55/59.67 & ( ~ p(s(tyop_2Emin_2Ebool,V0q_2E0)) % 59.55/59.67 | ~ p(s(tyop_2Emin_2Ebool,V1p_2E0)) ) ) ) ). % 59.55/59.67 % 59.55/59.67 fof(thm_2Esat_2Epth__ni1,axiom, % 59.55/59.67 ! [V0q_2E0,V1p_2E0] : % 59.55/59.67 ( ~ ( p(s(tyop_2Emin_2Ebool,V1p_2E0)) % 59.55/59.67 => p(s(tyop_2Emin_2Ebool,V0q_2E0)) ) % 59.55/59.67 => p(s(tyop_2Emin_2Ebool,V1p_2E0)) ) ). % 59.55/59.67 % 59.55/59.67 fof(thm_2Esat_2Epth__ni2,axiom, % 59.55/59.67 ! [V0q_2E0,V1p_2E0] : % 59.55/59.67 ( ~ ( p(s(tyop_2Emin_2Ebool,V1p_2E0)) % 59.55/59.67 => p(s(tyop_2Emin_2Ebool,V0q_2E0)) ) % 59.55/59.67 => ~ p(s(tyop_2Emin_2Ebool,V0q_2E0)) ) ). % 59.55/59.67 % 59.55/59.67 fof(thm_2EquantHeuristics_2EGUESS__RULES__WEAKEN__FORALL__POINT,conjecture, % 59.55/59.67 ! [A_27a,A_27b,V0i_2E0,V1P_2E0,V2Q_2E0] : % 59.55/59.67 ( ! [V3x_2E0] : % 59.55/59.67 ( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V2Q_2E0),s(A_27a,V3x_2E0)))) % 59.55/59.67 => p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V1P_2E0),s(A_27a,V3x_2E0)))) ) % 59.55/59.67 => ( p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(A_27b,A_27a),V0i_2E0),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V1P_2E0)))) % 59.55/59.67 => p(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(A_27b,A_27a),V0i_2E0),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V2Q_2E0)))) ) ) ). % 59.55/59.67 % 59.55/59.67 %------------------------------------------------------------------------------ % 59.55/59.67 %------------------------------------------- % 59.55/59.67 % Proof found % 59.55/59.67 % SZS status Theorem for theBenchmark % 59.55/59.67 % SZS output start Proof % 59.55/59.67 %ClaNum:195(EqnAxiom:86) % 59.55/59.67 %VarNum:652(SingletonVarNum:230) % 59.55/59.67 %MaxLitNum:4 % 59.55/59.67 %MaxfuncDepth:6 % 59.55/59.67 %SharedTerms:47 % 59.55/59.67 %goalClause: 91 104 165 % 59.55/59.67 %singleGoalClaCount:2 % 59.55/59.67 [89]P1(f5(a1,a2)) % 59.55/59.67 [103]~P1(f5(a1,a4)) % 59.55/59.67 [91]P1(f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42)))) % 59.55/59.67 [104]~P1(f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a43)))) % 59.55/59.67 [90]E(f5(x901,f3(f5(f53(x901,x901),a6),f5(x901,x902))),f5(x901,x902)) % 59.55/59.67 [92]E(f5(a1,f3(f5(f53(f53(x921,a1),a1),a8),f5(f53(x921,a1),x922))),f5(a1,f9(f5(f53(x921,a1),x922)))) % 59.55/59.67 [93]E(f5(a1,f3(f5(f53(f53(x931,a1),a1),a10),f5(f53(x931,a1),x932))),f5(a1,f13(f5(f53(x931,a1),x932)))) % 59.55/59.67 [94]E(f5(x941,f3(f5(f53(x942,x941),f3(f5(f53(x941,f53(x942,x941)),a35),f5(x941,x943))),f5(x942,x944))),f5(x941,x943)) % 59.55/59.67 [95]E(f5(a1,f3(f5(f53(f53(x951,a1),a1),f3(f5(f53(f53(x952,x951),f53(f53(x951,a1),a1)),a14),f5(f53(x952,x951),x953))),f5(f53(x951,a1),x954))),f5(a1,f23(f5(f53(x952,x951),x953),f5(f53(x951,a1),x954)))) % 59.55/59.67 [96]E(f5(a1,f3(f5(f53(f53(x961,a1),a1),f3(f5(f53(f53(x962,x961),f53(f53(x961,a1),a1)),a24),f5(f53(x962,x961),x963))),f5(f53(x961,a1),x964))),f5(a1,f25(f5(f53(x962,x961),x963),f5(f53(x961,a1),x964)))) % 59.55/59.67 [97]E(f5(a1,f3(f5(f53(f53(x971,a1),a1),f3(f5(f53(f53(x972,x971),f53(f53(x971,a1),a1)),a26),f5(f53(x972,x971),x973))),f5(f53(x971,a1),x974))),f5(a1,f27(f5(f53(x972,x971),x973),f5(f53(x971,a1),x974)))) % 59.55/59.67 [98]E(f5(a1,f3(f5(f53(f53(x981,a1),a1),f3(f5(f53(f53(x982,x981),f53(f53(x981,a1),a1)),a28),f5(f53(x982,x981),x983))),f5(f53(x981,a1),x984))),f5(a1,f29(f5(f53(x982,x981),x983),f5(f53(x981,a1),x984)))) % 59.55/59.67 [99]E(f5(a1,f3(f5(f53(f53(x991,a1),a1),f3(f5(f53(f53(x992,x991),f53(f53(x991,a1),a1)),a30),f5(f53(x992,x991),x993))),f5(f53(x991,a1),x994))),f5(a1,f31(f5(f53(x992,x991),x993),f5(f53(x991,a1),x994)))) % 59.55/59.67 [101]E(f5(a1,f3(f5(f53(f53(x1011,a1),a1),f3(f5(f53(f53(x1012,x1011),f53(f53(x1011,a1),a1)),a32),f5(f53(x1012,x1011),x1013))),f5(f53(x1011,a1),x1014))),f5(a1,f7(f5(f53(x1012,x1011),x1013),f5(f53(x1011,a1),x1014)))) % 59.55/59.67 [102]E(f5(x1021,f3(f5(f53(x1022,x1021),f3(f5(f53(f53(x1022,x1023),f53(x1022,x1021)),f3(f5(f53(f53(x1022,f53(x1023,x1021)),f53(f53(x1022,x1023),f53(x1022,x1021))),a36),f5(f53(x1022,f53(x1023,x1021)),x1024))),f5(f53(x1022,x1023),x1025))),f5(x1022,x1026))),f5(x1021,f3(f5(f53(x1023,x1021),f3(f5(f53(x1022,f53(x1023,x1021)),x1024),f5(x1022,x1026))),f5(x1023,f3(f5(f53(x1022,x1023),x1025),f5(x1022,x1026)))))) % 59.55/59.67 [105]E(f5(a1,x1051),f5(a1,a2))+E(f5(a1,x1051),f5(a1,a4)) % 59.55/59.67 [109]E(f5(a1,x1091),f5(a1,a4))+P1(f5(a1,x1091)) % 59.55/59.67 [110]E(f5(a1,a4),f5(a1,x1101))+P1(f5(a1,x1101)) % 59.55/59.67 [113]~E(f5(a1,x1131),f5(a1,a2))+P1(f5(a1,x1131)) % 59.55/59.67 [114]~E(f5(a1,a2),f5(a1,x1141))+P1(f5(a1,x1141)) % 59.55/59.67 [115]E(f5(a1,x1151),f5(a1,a2))+~P1(f5(a1,x1151)) % 59.55/59.67 [116]E(f5(a1,a2),f5(a1,x1161))+~P1(f5(a1,x1161)) % 59.55/59.67 [121]~E(f5(a1,x1211),f5(a1,a4))+~P1(f5(a1,x1211)) % 59.55/59.67 [122]~E(f5(a1,a4),f5(a1,x1221))+~P1(f5(a1,x1221)) % 59.55/59.67 [138]P1(f5(a1,x1381))+P1(f5(a1,f15(f5(a1,x1381)))) % 59.55/59.67 [149]~P1(f5(a1,x1491))+~P1(f5(a1,f15(f5(a1,x1491)))) % 59.55/59.67 [158]P1(f5(a1,x1581))+P1(f5(a1,f3(f5(f53(a1,a1),a18),f5(a1,x1581)))) % 59.55/59.67 [162]~P1(f5(a1,x1621))+~P1(f5(a1,f3(f5(f53(a1,a1),a18),f5(a1,x1621)))) % 59.55/59.67 [165]~P1(f5(a1,f3(f5(f53(a34,a1),a43),f5(a34,x1651))))+P1(f5(a1,f3(f5(f53(a34,a1),a42),f5(a34,x1651)))) % 59.55/59.67 [150]P1(f5(a1,x1501))+P1(f5(a1,f19(f5(a1,x1501),f5(a1,x1502)))) % 59.55/59.67 [151]~P1(f5(a1,x1512))+P1(f5(a1,f16(f5(a1,x1511),f5(a1,x1512)))) % 59.55/59.67 [152]~P1(f5(a1,x1521))+P1(f5(a1,f16(f5(a1,x1521),f5(a1,x1522)))) % 59.55/59.67 [153]~P1(f5(a1,x1532))+P1(f5(a1,f19(f5(a1,x1531),f5(a1,x1532)))) % 59.55/59.67 [156]P1(f5(a1,x1561))+~P1(f5(a1,f11(f5(a1,x1562),f5(a1,x1561)))) % 59.55/59.67 [157]P1(f5(a1,x1571))+~P1(f5(a1,f11(f5(a1,x1571),f5(a1,x1572)))) % 59.55/59.67 [172]P1(f5(a1,x1721))+P1(f5(a1,f3(f5(f53(a1,a1),f3(f5(f53(a1,f53(a1,a1)),a22),f5(a1,x1721))),f5(a1,x1722)))) % 59.55/59.67 [173]~P1(f5(a1,x1732))+P1(f5(a1,f3(f5(f53(a1,a1),f3(f5(f53(a1,f53(a1,a1)),a17),f5(a1,x1731))),f5(a1,x1732)))) % 59.55/59.67 [174]~P1(f5(a1,x1741))+P1(f5(a1,f3(f5(f53(a1,a1),f3(f5(f53(a1,f53(a1,a1)),a17),f5(a1,x1741))),f5(a1,x1742)))) % 59.55/59.67 [175]~P1(f5(a1,x1752))+P1(f5(a1,f3(f5(f53(a1,a1),f3(f5(f53(a1,f53(a1,a1)),a22),f5(a1,x1751))),f5(a1,x1752)))) % 59.55/59.67 [182]P1(f5(a1,x1821))+~P1(f5(a1,f3(f5(f53(a1,a1),f3(f5(f53(a1,f53(a1,a1)),a12),f5(a1,x1822))),f5(a1,x1821)))) % 59.55/59.67 [183]P1(f5(a1,x1831))+~P1(f5(a1,f3(f5(f53(a1,a1),f3(f5(f53(a1,f53(a1,a1)),a12),f5(a1,x1831))),f5(a1,x1832)))) % 59.55/59.67 [166]P1(f5(a1,f3(f5(f53(x1661,a1),x1662),f5(x1661,f44(x1661,x1662)))))+~P1(f5(a1,f13(f5(f53(x1661,a1),x1662)))) % 59.55/59.67 [167]~P1(f5(a1,f3(f5(f53(x1671,a1),x1672),f5(x1671,f45(x1671,x1672)))))+P1(f5(a1,f9(f5(f53(x1671,a1),x1672)))) % 59.55/59.67 [154]~E(f5(x1541,x1542),f5(x1541,x1543))+P1(f5(a1,f20(f5(x1541,x1542),f5(x1541,x1543)))) % 59.55/59.67 [160]E(f5(x1601,x1602),f5(x1601,x1603))+~P1(f5(a1,f20(f5(x1601,x1602),f5(x1601,x1603)))) % 59.55/59.67 [177]~E(f5(x1771,x1772),f5(x1771,x1773))+P1(f5(a1,f3(f5(f53(x1771,a1),f3(f5(f53(x1771,f53(x1771,a1)),a21),f5(x1771,x1772))),f5(x1771,x1773)))) % 59.55/59.67 [186]E(f5(x1861,x1862),f5(x1861,x1863))+~P1(f5(a1,f3(f5(f53(x1861,a1),f3(f5(f53(x1861,f53(x1861,a1)),a21),f5(x1861,x1862))),f5(x1861,x1863)))) % 59.55/59.67 [163]P1(f5(a1,f3(f5(f53(x1631,a1),x1632),f5(x1631,x1633))))+~P1(f5(a1,f9(f5(f53(x1631,a1),x1632)))) % 59.55/59.67 [164]~P1(f5(a1,f3(f5(f53(x1641,a1),x1642),f5(x1641,x1643))))+P1(f5(a1,f13(f5(f53(x1641,a1),x1642)))) % 59.55/59.67 [180]P1(f5(a1,f3(f5(f53(x1802,a1),x1804),f5(x1802,f47(x1801,x1802,x1803,x1804)))))+P1(f5(a1,f23(f5(f53(x1801,x1802),x1803),f5(f53(x1802,a1),x1804)))) % 59.55/59.67 [181]P1(f5(a1,f3(f5(f53(x1812,a1),x1814),f5(x1812,f37(x1811,x1812,x1813,x1814)))))+P1(f5(a1,f25(f5(f53(x1811,x1812),x1813),f5(f53(x1812,a1),x1814)))) % 59.55/59.67 [187]E(f5(f53(x1871,x1872),x1873),f5(f53(x1871,x1872),x1874))+~E(f5(x1872,f3(f5(f53(x1871,x1872),x1873),f5(x1871,f46(x1871,x1872,x1873,x1874)))),f5(x1872,f3(f5(f53(x1871,x1872),x1874),f5(x1871,f46(x1871,x1872,x1873,x1874))))) % 59.55/59.67 [188]~P1(f5(a1,f3(f5(f53(x1882,a1),x1884),f5(x1882,f49(x1881,x1882,x1883,x1884)))))+P1(f5(a1,f29(f5(f53(x1881,x1882),x1883),f5(f53(x1882,a1),x1884)))) % 59.55/59.67 [189]~P1(f5(a1,f3(f5(f53(x1892,a1),x1894),f5(x1892,f39(x1891,x1892,x1893,x1894)))))+P1(f5(a1,f31(f5(f53(x1891,x1892),x1893),f5(f53(x1892,a1),x1894)))) % 59.55/59.67 [192]P1(f5(a1,f7(f5(f53(x1921,x1922),x1923),f5(f53(x1922,a1),x1924))))+P1(f5(a1,f3(f5(f53(x1922,a1),x1924),f5(x1922,f3(f5(f53(x1921,x1922),x1923),f5(x1921,f51(x1921,x1922,x1923,x1924))))))) % 59.55/59.67 [194]P1(f5(a1,f27(f5(f53(x1941,x1942),x1943),f5(f53(x1942,a1),x1944))))+~P1(f5(a1,f3(f5(f53(x1942,a1),x1944),f5(x1942,f3(f5(f53(x1941,x1942),x1943),f5(x1941,f52(x1941,x1942,x1943,x1944))))))) % 59.55/59.67 [168]~E(f5(x1682,f37(x1681,x1682,x1683,x1684)),f5(x1682,f3(f5(f53(x1681,x1682),x1683),f5(x1681,x1685))))+P1(f5(a1,f25(f5(f53(x1681,x1682),x1683),f5(f53(x1682,a1),x1684)))) % 59.55/59.67 [169]~E(f5(x1692,f39(x1691,x1692,x1693,x1694)),f5(x1692,f3(f5(f53(x1691,x1692),x1693),f5(x1691,x1695))))+P1(f5(a1,f31(f5(f53(x1691,x1692),x1693),f5(f53(x1692,a1),x1694)))) % 59.55/59.67 [170]P1(f5(a1,f29(f5(f53(x1701,x1702),x1703),f5(f53(x1702,a1),x1704))))+P1(f5(a1,f3(f5(f53(x1702,a1),x1704),f5(x1702,f3(f5(f53(x1701,x1702),x1703),f5(x1701,x1705)))))) % 59.55/59.67 [171]~P1(f5(a1,f27(f5(f53(x1713,x1711),x1714),f5(f53(x1711,a1),x1712))))+P1(f5(a1,f3(f5(f53(x1711,a1),x1712),f5(x1711,f3(f5(f53(x1713,x1711),x1714),f5(x1713,x1715)))))) % 59.55/59.67 [178]P1(f5(a1,f23(f5(f53(x1781,x1782),x1783),f5(f53(x1782,a1),x1784))))+~P1(f5(a1,f3(f5(f53(x1782,a1),x1784),f5(x1782,f3(f5(f53(x1781,x1782),x1783),f5(x1781,x1785)))))) % 59.55/59.67 [179]~P1(f5(a1,f7(f5(f53(x1791,x1792),x1793),f5(f53(x1792,a1),x1794))))+~P1(f5(a1,f3(f5(f53(x1792,a1),x1794),f5(x1792,f3(f5(f53(x1791,x1792),x1793),f5(x1791,x1795)))))) % 59.55/59.67 [120]E(f5(a1,x1201),f5(a1,x1202))+P1(f5(a1,x1201))+P1(f5(a1,x1202)) % 59.55/59.67 [126]E(f5(a1,x1261),f5(a1,x1262))+~P1(f5(a1,x1261))+~P1(f5(a1,x1262)) % 59.55/59.67 [155]~P1(f5(a1,x1551))+~P1(f5(a1,x1552))+P1(f5(a1,f11(f5(a1,x1551),f5(a1,x1552)))) % 59.55/59.67 [159]P1(f5(a1,x1591))+P1(f5(a1,x1592))+~P1(f5(a1,f16(f5(a1,x1592),f5(a1,x1591)))) % 59.55/59.67 [161]P1(f5(a1,x1611))+~P1(f5(a1,x1612))+~P1(f5(a1,f19(f5(a1,x1612),f5(a1,x1611)))) % 59.55/59.67 [176]~P1(f5(a1,x1761))+~P1(f5(a1,x1762))+P1(f5(a1,f3(f5(f53(a1,a1),f3(f5(f53(a1,f53(a1,a1)),a12),f5(a1,x1761))),f5(a1,x1762)))) % 59.55/59.67 [184]P1(f5(a1,x1841))+P1(f5(a1,x1842))+~P1(f5(a1,f3(f5(f53(a1,a1),f3(f5(f53(a1,f53(a1,a1)),a17),f5(a1,x1842))),f5(a1,x1841)))) % 59.55/59.67 [185]P1(f5(a1,x1851))+~P1(f5(a1,x1852))+~P1(f5(a1,f3(f5(f53(a1,a1),f3(f5(f53(a1,f53(a1,a1)),a22),f5(a1,x1852))),f5(a1,x1851)))) % 59.55/59.67 [125]P2(x1253,x1251,x1252)+E(f5(a1,x1251),f5(a1,x1252))+P1(f5(a1,x1253)) % 59.55/59.67 [128]P2(x1281,x1282,x1283)+P1(f5(a1,x1283))+~P1(f5(a1,x1282)) % 59.55/59.67 [130]P2(x1301,x1302,x1303)+P1(f5(a1,x1303))+~P1(f5(a1,x1301)) % 59.55/59.67 [131]P2(x1311,x1312,x1313)+~E(f5(a1,x1312),f5(a1,x1313))+~P1(f5(a1,x1311)) % 59.55/59.67 [133]P2(x1331,x1332,x1333)+~P1(f5(a1,x1331))+~P1(f5(a1,x1332)) % 59.55/59.67 [137]~P2(x1371,x1372,x1373)+~E(f5(a1,x1372),f5(a1,x1373))+P1(f5(a1,x1371)) % 59.55/59.67 [190]E(f5(x1901,f3(f5(f53(x1902,x1901),x1903),f5(x1902,f40(x1902,x1901,x1903,x1904,x1905)))),f5(x1901,x1905))+P1(f5(a1,f3(f5(f53(x1901,a1),x1904),f5(x1901,x1905))))+~P1(f5(a1,f31(f5(f53(x1902,x1901),x1903),f5(f53(x1901,a1),x1904)))) % 59.55/59.67 [191]E(f5(x1911,f3(f5(f53(x1912,x1911),x1913),f5(x1912,f38(x1912,x1911,x1913,x1914,x1915)))),f5(x1911,x1915))+~P1(f5(a1,f3(f5(f53(x1911,a1),x1914),f5(x1911,x1915))))+~P1(f5(a1,f25(f5(f53(x1912,x1911),x1913),f5(f53(x1911,a1),x1914)))) % 59.55/59.67 [193]~P1(f5(a1,f3(f5(f53(x1931,a1),x1932),f5(x1931,x1935))))+~P1(f5(a1,f23(f5(f53(x1933,x1931),x1934),f5(f53(x1931,a1),x1932))))+P1(f5(a1,f3(f5(f53(x1931,a1),x1932),f5(x1931,f3(f5(f53(x1933,x1931),x1934),f5(x1933,f48(x1933,x1931,x1934,x1932))))))) % 59.55/59.67 [195]P1(f5(a1,f3(f5(f53(x1951,a1),x1952),f5(x1951,x1953))))+~P1(f5(a1,f29(f5(f53(x1954,x1951),x1955),f5(f53(x1951,a1),x1952))))+~P1(f5(a1,f3(f5(f53(x1951,a1),x1952),f5(x1951,f3(f5(f53(x1954,x1951),x1955),f5(x1954,f50(x1954,x1951,x1955,x1952))))))) % 59.55/59.67 [136]P2(x1361,x1362,x1363)+P1(f5(a1,x1362))+P1(f5(a1,x1361))+~P1(f5(a1,x1363)) % 59.55/59.67 [139]~P2(x1393,x1392,x1391)+P1(f5(a1,x1391))+P1(f5(a1,x1392))+P1(f5(a1,x1393)) % 59.55/59.67 [143]~P2(x1433,x1431,x1432)+E(f5(a1,x1431),f5(a1,x1432))+P1(f5(a1,x1431))+~P1(f5(a1,x1433)) % 59.55/59.67 [146]~P2(x1463,x1461,x1462)+E(f5(a1,x1461),f5(a1,x1462))+~P1(f5(a1,x1462))+~P1(f5(a1,x1463)) % 59.55/59.67 [147]~P2(x1472,x1471,x1473)+~P1(f5(a1,x1472))+~P1(f5(a1,x1473))+P1(f5(a1,x1471)) % 59.55/59.67 [148]~P2(x1481,x1482,x1483)+~P1(f5(a1,x1482))+~P1(f5(a1,x1483))+P1(f5(a1,x1481)) % 59.55/59.67 %EqnAxiom % 59.55/59.67 [1]E(x11,x11) % 59.55/59.67 [2]E(x22,x21)+~E(x21,x22) % 59.55/59.67 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 59.55/59.67 [4]~E(x41,x42)+E(f5(x41,x43),f5(x42,x43)) % 59.55/59.67 [5]~E(x51,x52)+E(f5(x53,x51),f5(x53,x52)) % 59.55/59.67 [6]~E(x61,x62)+E(f3(x61,x63),f3(x62,x63)) % 59.55/59.67 [7]~E(x71,x72)+E(f3(x73,x71),f3(x73,x72)) % 59.55/59.67 [8]~E(x81,x82)+E(f15(x81),f15(x82)) % 59.55/59.67 [9]~E(x91,x92)+E(f53(x91,x93),f53(x92,x93)) % 59.55/59.67 [10]~E(x101,x102)+E(f53(x103,x101),f53(x103,x102)) % 59.55/59.67 [11]~E(x111,x112)+E(f50(x111,x113,x114,x115),f50(x112,x113,x114,x115)) % 59.55/59.67 [12]~E(x121,x122)+E(f50(x123,x121,x124,x125),f50(x123,x122,x124,x125)) % 59.55/59.67 [13]~E(x131,x132)+E(f50(x133,x134,x131,x135),f50(x133,x134,x132,x135)) % 59.55/59.67 [14]~E(x141,x142)+E(f50(x143,x144,x145,x141),f50(x143,x144,x145,x142)) % 59.55/59.67 [15]~E(x151,x152)+E(f23(x151,x153),f23(x152,x153)) % 59.55/59.67 [16]~E(x161,x162)+E(f23(x163,x161),f23(x163,x162)) % 59.55/59.67 [17]~E(x171,x172)+E(f19(x171,x173),f19(x172,x173)) % 59.55/59.67 [18]~E(x181,x182)+E(f19(x183,x181),f19(x183,x182)) % 59.55/59.67 [19]~E(x191,x192)+E(f7(x191,x193),f7(x192,x193)) % 59.55/59.67 [20]~E(x201,x202)+E(f7(x203,x201),f7(x203,x202)) % 59.55/59.67 [21]~E(x211,x212)+E(f29(x211,x213),f29(x212,x213)) % 59.55/59.67 [22]~E(x221,x222)+E(f29(x223,x221),f29(x223,x222)) % 59.55/59.67 [23]~E(x231,x232)+E(f51(x231,x233,x234,x235),f51(x232,x233,x234,x235)) % 59.55/59.67 [24]~E(x241,x242)+E(f51(x243,x241,x244,x245),f51(x243,x242,x244,x245)) % 59.55/59.67 [25]~E(x251,x252)+E(f51(x253,x254,x251,x255),f51(x253,x254,x252,x255)) % 59.55/59.67 [26]~E(x261,x262)+E(f51(x263,x264,x265,x261),f51(x263,x264,x265,x262)) % 59.55/59.67 [27]~E(x271,x272)+E(f47(x271,x273,x274,x275),f47(x272,x273,x274,x275)) % 59.55/59.67 [28]~E(x281,x282)+E(f47(x283,x281,x284,x285),f47(x283,x282,x284,x285)) % 59.55/59.67 [29]~E(x291,x292)+E(f47(x293,x294,x291,x295),f47(x293,x294,x292,x295)) % 59.55/59.67 [30]~E(x301,x302)+E(f47(x303,x304,x305,x301),f47(x303,x304,x305,x302)) % 59.55/59.67 [31]~E(x311,x312)+E(f25(x311,x313),f25(x312,x313)) % 59.55/59.67 [32]~E(x321,x322)+E(f25(x323,x321),f25(x323,x322)) % 59.55/59.67 [33]~E(x331,x332)+E(f37(x331,x333,x334,x335),f37(x332,x333,x334,x335)) % 59.55/59.67 [34]~E(x341,x342)+E(f37(x343,x341,x344,x345),f37(x343,x342,x344,x345)) % 59.55/59.67 [35]~E(x351,x352)+E(f37(x353,x354,x351,x355),f37(x353,x354,x352,x355)) % 59.55/59.67 [36]~E(x361,x362)+E(f37(x363,x364,x365,x361),f37(x363,x364,x365,x362)) % 59.55/59.67 [37]~E(x371,x372)+E(f44(x371,x373),f44(x372,x373)) % 59.55/59.67 [38]~E(x381,x382)+E(f44(x383,x381),f44(x383,x382)) % 59.55/59.67 [39]~E(x391,x392)+E(f16(x391,x393),f16(x392,x393)) % 59.55/59.67 [40]~E(x401,x402)+E(f16(x403,x401),f16(x403,x402)) % 59.55/59.67 [41]~E(x411,x412)+E(f13(x411),f13(x412)) % 59.55/59.67 [42]~E(x421,x422)+E(f27(x421,x423),f27(x422,x423)) % 59.55/59.67 [43]~E(x431,x432)+E(f27(x433,x431),f27(x433,x432)) % 59.55/59.67 [44]~E(x441,x442)+E(f31(x441,x443),f31(x442,x443)) % 59.55/59.67 [45]~E(x451,x452)+E(f31(x453,x451),f31(x453,x452)) % 59.55/59.67 [46]~E(x461,x462)+E(f48(x461,x463,x464,x465),f48(x462,x463,x464,x465)) % 59.55/59.67 [47]~E(x471,x472)+E(f48(x473,x471,x474,x475),f48(x473,x472,x474,x475)) % 59.55/59.67 [48]~E(x481,x482)+E(f48(x483,x484,x481,x485),f48(x483,x484,x482,x485)) % 59.55/59.67 [49]~E(x491,x492)+E(f48(x493,x494,x495,x491),f48(x493,x494,x495,x492)) % 59.55/59.67 [50]~E(x501,x502)+E(f39(x501,x503,x504,x505),f39(x502,x503,x504,x505)) % 59.55/59.67 [51]~E(x511,x512)+E(f39(x513,x511,x514,x515),f39(x513,x512,x514,x515)) % 59.55/59.67 [52]~E(x521,x522)+E(f39(x523,x524,x521,x525),f39(x523,x524,x522,x525)) % 59.55/59.67 [53]~E(x531,x532)+E(f39(x533,x534,x535,x531),f39(x533,x534,x535,x532)) % 59.65/59.67 [54]~E(x541,x542)+E(f9(x541),f9(x542)) % 59.65/59.67 [55]~E(x551,x552)+E(f20(x551,x553),f20(x552,x553)) % 59.65/59.67 [56]~E(x561,x562)+E(f20(x563,x561),f20(x563,x562)) % 59.65/59.67 [57]~E(x571,x572)+E(f38(x571,x573,x574,x575,x576),f38(x572,x573,x574,x575,x576)) % 59.65/59.67 [58]~E(x581,x582)+E(f38(x583,x581,x584,x585,x586),f38(x583,x582,x584,x585,x586)) % 59.65/59.67 [59]~E(x591,x592)+E(f38(x593,x594,x591,x595,x596),f38(x593,x594,x592,x595,x596)) % 59.65/59.67 [60]~E(x601,x602)+E(f38(x603,x604,x605,x601,x606),f38(x603,x604,x605,x602,x606)) % 59.65/59.67 [61]~E(x611,x612)+E(f38(x613,x614,x615,x616,x611),f38(x613,x614,x615,x616,x612)) % 59.65/59.67 [62]~E(x621,x622)+E(f52(x621,x623,x624,x625),f52(x622,x623,x624,x625)) % 59.65/59.67 [63]~E(x631,x632)+E(f52(x633,x631,x634,x635),f52(x633,x632,x634,x635)) % 59.65/59.67 [64]~E(x641,x642)+E(f52(x643,x644,x641,x645),f52(x643,x644,x642,x645)) % 59.65/59.67 [65]~E(x651,x652)+E(f52(x653,x654,x655,x651),f52(x653,x654,x655,x652)) % 59.65/59.67 [66]~E(x661,x662)+E(f45(x661,x663),f45(x662,x663)) % 59.65/59.67 [67]~E(x671,x672)+E(f45(x673,x671),f45(x673,x672)) % 59.65/59.67 [68]~E(x681,x682)+E(f49(x681,x683,x684,x685),f49(x682,x683,x684,x685)) % 59.65/59.67 [69]~E(x691,x692)+E(f49(x693,x691,x694,x695),f49(x693,x692,x694,x695)) % 59.65/59.67 [70]~E(x701,x702)+E(f49(x703,x704,x701,x705),f49(x703,x704,x702,x705)) % 59.65/59.67 [71]~E(x711,x712)+E(f49(x713,x714,x715,x711),f49(x713,x714,x715,x712)) % 59.65/59.67 [72]~E(x721,x722)+E(f11(x721,x723),f11(x722,x723)) % 59.65/59.67 [73]~E(x731,x732)+E(f11(x733,x731),f11(x733,x732)) % 59.65/59.67 [74]~E(x741,x742)+E(f46(x741,x743,x744,x745),f46(x742,x743,x744,x745)) % 59.65/59.67 [75]~E(x751,x752)+E(f46(x753,x751,x754,x755),f46(x753,x752,x754,x755)) % 59.65/59.67 [76]~E(x761,x762)+E(f46(x763,x764,x761,x765),f46(x763,x764,x762,x765)) % 59.65/59.67 [77]~E(x771,x772)+E(f46(x773,x774,x775,x771),f46(x773,x774,x775,x772)) % 59.65/59.67 [78]~E(x781,x782)+E(f40(x781,x783,x784,x785,x786),f40(x782,x783,x784,x785,x786)) % 59.65/59.67 [79]~E(x791,x792)+E(f40(x793,x791,x794,x795,x796),f40(x793,x792,x794,x795,x796)) % 59.65/59.67 [80]~E(x801,x802)+E(f40(x803,x804,x801,x805,x806),f40(x803,x804,x802,x805,x806)) % 59.65/59.67 [81]~E(x811,x812)+E(f40(x813,x814,x815,x811,x816),f40(x813,x814,x815,x812,x816)) % 59.65/59.67 [82]~E(x821,x822)+E(f40(x823,x824,x825,x826,x821),f40(x823,x824,x825,x826,x822)) % 59.65/59.67 [83]~P1(x831)+P1(x832)+~E(x831,x832) % 59.65/59.67 [84]P2(x842,x843,x844)+~E(x841,x842)+~P2(x841,x843,x844) % 59.65/59.67 [85]P2(x853,x852,x854)+~E(x851,x852)+~P2(x853,x851,x854) % 59.65/59.67 [86]P2(x863,x864,x862)+~E(x861,x862)+~P2(x863,x864,x861) % 59.65/59.67 % 59.65/59.67 %------------------------------------------- % 59.65/59.67 cnf(200,plain, % 59.65/59.67 (P2(x2001,x2002,x2002)+~P1(f5(a1,x2001))), % 59.65/59.67 inference(equality_inference,[],[131])). % 59.65/59.67 cnf(201,plain, % 59.65/59.67 (~P2(x2011,x2012,x2012)+P1(f5(a1,x2011))), % 59.65/59.67 inference(equality_inference,[],[137])). % 59.65/59.67 cnf(202,plain, % 59.65/59.67 (P1(f5(a1,f20(f5(x2021,x2022),f5(x2021,x2022))))), % 59.65/59.67 inference(equality_inference,[],[154])). % 59.65/59.67 cnf(203,plain, % 59.65/59.67 (P1(f5(a1,f3(f5(f53(x2031,a1),f3(f5(f53(x2031,f53(x2031,a1)),a21),f5(x2031,x2032))),f5(x2031,x2032))))), % 59.65/59.67 inference(equality_inference,[],[177])). % 59.65/59.67 cnf(205,plain, % 59.65/59.67 (E(f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42))),f5(a1,a2))), % 59.65/59.67 inference(scs_inference,[],[91,115])). % 59.65/59.67 cnf(207,plain, % 59.65/59.67 (E(f5(a1,a2),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42))))), % 59.65/59.67 inference(scs_inference,[],[91,115,116])). % 59.65/59.67 cnf(209,plain, % 59.65/59.67 (~E(f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42))),f5(a1,a4))), % 59.65/59.67 inference(scs_inference,[],[91,115,116,121])). % 59.65/59.67 cnf(211,plain, % 59.65/59.67 (~E(f5(a1,a4),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42))))), % 59.65/59.67 inference(scs_inference,[],[91,115,116,121,122])). % 59.65/59.67 cnf(213,plain, % 59.65/59.67 (P2(f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42)),x2131,x2131)), % 59.65/59.67 inference(scs_inference,[],[91,115,116,121,122,200])). % 59.65/59.67 cnf(215,plain, % 59.65/59.67 (~P2(f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a43)),x2151,x2151)), % 59.65/59.67 inference(scs_inference,[],[91,104,115,116,121,122,200,201])). % 59.65/59.67 cnf(217,plain, % 59.65/59.67 (E(f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a43))),f5(a1,a4))), % 59.65/59.67 inference(scs_inference,[],[91,104,115,116,121,122,200,201,109])). % 59.65/59.67 cnf(221,plain, % 59.65/59.67 (~E(f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a43))),f5(a1,a2))), % 59.65/59.67 inference(scs_inference,[],[91,104,115,116,121,122,200,201,109,110,113])). % 59.65/59.67 cnf(225,plain, % 59.65/59.67 (E(f5(x2251,x2252),f5(x2251,f3(f5(f53(x2251,x2251),a6),f5(x2251,x2252))))), % 59.65/59.67 inference(scs_inference,[],[91,104,90,115,116,121,122,200,201,109,110,113,114,2])). % 59.65/59.67 cnf(227,plain, % 59.65/59.67 (P2(x2271,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42)),f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a43)))), % 59.65/59.67 inference(scs_inference,[],[91,104,90,115,116,121,122,200,201,109,110,113,114,2,5,128])). % 59.65/59.67 cnf(229,plain, % 59.65/59.67 (P2(f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42)),x2291,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a43)))), % 59.65/59.67 inference(scs_inference,[],[91,104,90,115,116,121,122,200,201,109,110,113,114,2,5,128,130])). % 59.65/59.67 cnf(231,plain, % 59.65/59.67 (P2(f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42)),f3(f5(f53(x2311,a1),f3(f5(f53(a1,f53(x2311,a1)),a35),f5(a1,x2312))),f5(x2311,x2313)),x2312)), % 59.65/59.67 inference(scs_inference,[],[91,104,94,90,115,116,121,122,200,201,109,110,113,114,2,5,128,130,131])). % 59.65/59.67 cnf(232,plain, % 59.65/59.67 (E(f5(x2321,f3(f5(f53(x2322,x2321),f3(f5(f53(x2321,f53(x2322,x2321)),a35),f5(x2321,x2323))),f5(x2322,x2324))),f5(x2321,x2323))), % 59.65/59.67 inference(rename_variables,[],[94])). % 59.65/59.67 cnf(238,plain, % 59.65/59.67 (~P2(f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a43)),f3(f5(f53(x2381,a1),f3(f5(f53(a1,f53(x2381,a1)),a35),f5(a1,x2382))),f5(x2381,x2383)),x2382)), % 59.65/59.67 inference(scs_inference,[],[91,104,94,232,90,115,116,121,122,200,201,109,110,113,114,2,5,128,130,131,125,133,137])). % 59.65/59.67 cnf(239,plain, % 59.65/59.67 (E(f5(x2391,f3(f5(f53(x2392,x2391),f3(f5(f53(x2391,f53(x2392,x2391)),a35),f5(x2391,x2393))),f5(x2392,x2394))),f5(x2391,x2393))), % 59.65/59.67 inference(rename_variables,[],[94])). % 59.65/59.67 cnf(243,plain, % 59.65/59.67 (~P1(f5(a1,f3(f5(f53(x2431,a1),f3(f5(f53(a1,f53(x2431,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a43))))),f5(x2431,x2432))))), % 59.65/59.67 inference(scs_inference,[],[91,104,94,232,239,90,115,116,121,122,200,201,109,110,113,114,2,5,128,130,131,125,133,137,3,83])). % 59.65/59.67 cnf(244,plain, % 59.65/59.67 (E(f5(x2441,f3(f5(f53(x2442,x2441),f3(f5(f53(x2441,f53(x2442,x2441)),a35),f5(x2441,x2443))),f5(x2442,x2444))),f5(x2441,x2443))), % 59.65/59.67 inference(rename_variables,[],[94])). % 59.65/59.67 cnf(246,plain, % 59.65/59.67 (P2(f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42)),f5(x2461,x2462),f5(x2461,f3(f5(f53(x2463,x2461),f3(f5(f53(x2461,f53(x2463,x2461)),a35),f5(x2461,x2462))),f5(x2463,x2464))))), % 59.65/59.67 inference(scs_inference,[],[91,104,94,232,239,244,90,115,116,121,122,200,201,109,110,113,114,2,5,128,130,131,125,133,137,3,83,84,85])). % 59.65/59.67 cnf(248,plain, % 59.65/59.67 (P2(f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a43)),f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a43)),f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42)))), % 59.65/59.67 inference(scs_inference,[],[91,104,94,232,239,244,90,115,116,121,122,200,201,109,110,113,114,2,5,128,130,131,125,133,137,3,83,84,85,86,136])). % 59.65/59.67 cnf(252,plain, % 59.65/59.67 (~P2(f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42)),f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a43)),a2)), % 59.65/59.67 inference(scs_inference,[],[91,104,103,94,232,239,244,90,115,116,121,122,200,201,109,110,113,114,2,5,128,130,131,125,133,137,3,83,84,85,86,136,139,143])). % 59.65/59.67 cnf(254,plain, % 59.65/59.67 (~P2(f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42)),a4,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42)))), % 59.65/59.67 inference(scs_inference,[],[91,104,103,94,232,239,244,90,115,116,121,122,200,201,109,110,113,114,2,5,128,130,131,125,133,137,3,83,84,85,86,136,139,143,146])). % 59.65/59.67 cnf(256,plain, % 59.65/59.67 (~P2(f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42)),f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a43)),f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42)))), % 59.65/59.67 inference(scs_inference,[],[91,104,103,94,232,239,244,90,115,116,121,122,200,201,109,110,113,114,2,5,128,130,131,125,133,137,3,83,84,85,86,136,139,143,146,147])). % 59.65/59.67 cnf(258,plain, % 59.65/59.67 (~E(f5(f53(a34,a1),a42),f5(f53(a34,a1),a43))), % 59.65/59.67 inference(scs_inference,[],[91,104,103,94,232,239,244,90,115,116,121,122,200,201,109,110,113,114,2,5,128,130,131,125,133,137,3,83,84,85,86,136,139,143,146,147,20])). % 59.65/59.67 cnf(259,plain, % 59.65/59.67 (~E(f5(a1,a4),f5(a1,a2))), % 59.65/59.67 inference(scs_inference,[],[103,113])). % 59.65/59.67 cnf(261,plain, % 59.65/59.67 (~P2(a4,x2611,x2611)), % 59.65/59.67 inference(scs_inference,[],[103,113,201])). % 59.65/59.67 cnf(263,plain, % 59.65/59.67 (P2(f20(f5(x2631,x2632),f5(x2631,x2632)),x2633,x2633)), % 59.65/59.67 inference(scs_inference,[],[202,103,113,201,200])). % 59.65/59.67 cnf(265,plain, % 59.65/59.67 (E(f5(a1,a2),f5(a1,f20(f5(x2651,x2652),f5(x2651,x2652))))), % 59.65/59.67 inference(scs_inference,[],[202,103,113,201,200,116])). % 59.65/59.67 cnf(267,plain, % 59.65/59.67 (~E(f5(a1,a2),f5(a1,a4))), % 59.65/59.67 inference(scs_inference,[],[202,103,113,201,200,116,114])). % 59.65/59.67 cnf(269,plain, % 59.65/59.67 (E(f5(a1,f20(f5(x2691,x2692),f5(x2691,x2692))),f5(a1,a2))), % 59.65/59.67 inference(scs_inference,[],[202,103,113,201,200,116,114,115])). % 59.65/59.67 cnf(271,plain, % 59.65/59.67 (E(f5(a1,f9(f5(f53(x2711,a1),x2712))),f5(a1,f3(f5(f53(f53(x2711,a1),a1),a8),f5(f53(x2711,a1),x2712))))), % 59.65/59.67 inference(scs_inference,[],[202,92,103,113,201,200,116,114,115,2])). % 59.65/59.67 cnf(272,plain, % 59.65/59.67 (~E(f5(a1,a4),f5(a1,f20(f5(x2721,x2722),f5(x2721,x2722))))), % 59.65/59.67 inference(scs_inference,[],[202,92,103,113,201,200,116,114,115,2,122])). % 59.65/59.67 cnf(274,plain, % 59.65/59.67 (~E(f5(a1,f20(f5(x2741,x2742),f5(x2741,x2742))),f5(a1,a4))), % 59.67/59.67 inference(scs_inference,[],[202,92,103,113,201,200,116,114,115,2,122,121])). % 59.67/59.67 cnf(277,plain, % 59.67/59.67 (~P2(f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a43)),f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42)),a2)), % 59.67/59.67 inference(scs_inference,[],[205,104,211,202,92,103,113,201,200,116,114,115,2,122,121,5,137])). % 59.67/59.67 cnf(279,plain, % 59.67/59.67 (P2(x2791,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42)),a4)), % 59.67/59.67 inference(scs_inference,[],[91,205,104,211,202,92,103,113,201,200,116,114,115,2,122,121,5,137,128])). % 59.67/59.67 cnf(283,plain, % 59.67/59.67 (P2(f20(f5(x2831,x2832),f5(x2831,x2832)),f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42)),a2)), % 59.67/59.67 inference(scs_inference,[],[91,205,104,211,202,92,103,113,201,200,116,114,115,2,122,121,5,137,128,125,131])). % 59.67/59.67 cnf(288,plain, % 59.67/59.67 (~P2(f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a43)),x2881,x2881)), % 59.67/59.67 inference(rename_variables,[],[215])). % 59.67/59.67 cnf(293,plain, % 59.67/59.67 (P1(f5(a1,f3(f5(f53(a1,a1),a6),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42))))))), % 59.67/59.67 inference(scs_inference,[],[91,205,104,211,231,225,215,248,202,92,103,113,201,200,116,114,115,2,122,121,5,137,128,125,131,130,85,133,86,83])). % 59.67/59.67 cnf(295,plain, % 59.67/59.67 (~E(f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a43))),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42))))), % 59.67/59.67 inference(scs_inference,[],[91,205,104,211,231,225,221,215,248,202,92,103,113,201,200,116,114,115,2,122,121,5,137,128,125,131,130,85,133,86,83,3])). % 59.67/59.67 cnf(297,plain, % 59.67/59.67 (~P2(f20(f5(x2971,x2972),f5(x2971,x2972)),f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a43)),f20(f5(x2971,x2972),f5(x2971,x2972)))), % 59.67/59.68 inference(scs_inference,[],[91,205,104,211,231,225,221,215,288,248,202,92,103,113,201,200,116,114,115,2,122,121,5,137,128,125,131,130,85,133,86,83,3,84,147])). % 59.67/59.68 cnf(301,plain, % 59.67/59.68 (~P2(f20(f5(x3011,x3012),f5(x3011,x3012)),a4,f20(f5(x3011,x3012),f5(x3011,x3012)))), % 59.67/59.68 inference(scs_inference,[],[91,205,104,211,231,225,221,215,288,248,202,92,103,113,201,200,116,114,115,2,122,121,5,137,128,125,131,130,85,133,86,83,3,84,147,136,146])). % 59.67/59.68 cnf(303,plain, % 59.67/59.68 (~P2(f20(f5(x3031,x3032),f5(x3031,x3032)),f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a43)),a2)), % 59.67/59.68 inference(scs_inference,[],[91,205,104,211,231,225,221,215,288,248,202,92,103,113,201,200,116,114,115,2,122,121,5,137,128,125,131,130,85,133,86,83,3,84,147,136,146,143])). % 59.67/59.68 cnf(306,plain, % 59.67/59.68 (E(f5(a1,f3(f5(f53(x3061,a1),f3(f5(f53(x3061,f53(x3061,a1)),a21),f5(x3061,x3062))),f5(x3061,x3062))),f5(a1,a2))), % 59.67/59.68 inference(scs_inference,[],[203,115])). % 59.67/59.68 cnf(308,plain, % 59.67/59.68 (~E(f5(a1,f3(f5(f53(x3081,a1),f3(f5(f53(x3081,f53(x3081,a1)),a21),f5(x3081,x3082))),f5(x3081,x3082))),f5(a1,a4))), % 59.67/59.68 inference(scs_inference,[],[203,115,121])). % 59.67/59.68 cnf(310,plain, % 59.67/59.68 (E(f5(a1,a2),f5(a1,f3(f5(f53(a1,a1),a6),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42))))))), % 59.67/59.68 inference(scs_inference,[],[203,293,115,121,116])). % 59.67/59.68 cnf(312,plain, % 59.67/59.68 (~E(f5(a1,a4),f5(a1,f3(f5(f53(a1,a1),a6),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42))))))), % 59.67/59.68 inference(scs_inference,[],[203,293,115,121,116,122])). % 59.67/59.68 cnf(314,plain, % 59.67/59.68 (P2(f3(f5(f53(x3141,a1),f3(f5(f53(x3141,f53(x3141,a1)),a21),f5(x3141,x3142))),f5(x3141,x3142)),x3143,x3143)), % 59.67/59.68 inference(scs_inference,[],[203,293,115,121,116,122,200])). % 59.67/59.68 cnf(316,plain, % 59.67/59.68 (E(f5(a1,f13(f5(f53(x3161,a1),x3162))),f5(a1,f3(f5(f53(f53(x3161,a1),a1),a10),f5(f53(x3161,a1),x3162))))), % 59.67/59.68 inference(scs_inference,[],[203,293,93,115,121,116,122,200,2])). % 59.67/59.68 cnf(317,plain, % 59.67/59.68 (~E(f20(f5(x3171,x3172),f5(x3171,x3172)),a4)), % 59.67/59.68 inference(scs_inference,[],[274,203,293,93,115,121,116,122,200,2,5])). % 59.67/59.68 cnf(324,plain, % 59.67/59.68 (P2(f3(f5(f53(x3241,a1),f3(f5(f53(x3241,f53(x3241,a1)),a21),f5(x3241,x3242))),f5(x3241,x3242)),f3(f5(f53(x3241,a1),f3(f5(f53(x3241,f53(x3241,a1)),a21),f5(x3241,x3242))),f5(x3241,x3242)),x3243)), % 59.67/59.68 inference(scs_inference,[],[91,269,104,263,274,297,203,293,93,115,121,116,122,200,2,5,137,131,86,133])). % 59.67/59.68 cnf(335,plain, % 59.67/59.68 (~P2(f3(f5(f53(x3351,a1),f3(f5(f53(x3351,f53(x3351,a1)),a21),f5(x3351,x3352))),f5(x3351,x3352)),f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a43)),f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42)))), % 59.67/59.68 inference(scs_inference,[],[91,269,104,263,209,274,279,295,217,297,238,203,293,261,93,115,121,116,122,200,2,5,137,131,86,133,85,3,84,147,146,143])). % 59.67/59.68 cnf(337,plain, % 59.67/59.68 (~P1(f5(a1,f9(f5(f53(x3371,a1),x3372))))+P1(f5(a1,f3(f5(f53(f53(x3371,a1),a1),a8),f5(f53(x3371,a1),x3372))))), % 59.67/59.68 inference(scs_inference,[],[91,269,104,263,209,274,279,295,217,297,238,203,293,271,261,93,115,121,116,122,200,2,5,137,131,86,133,85,3,84,147,146,143,83])). % 59.67/59.68 cnf(340,plain, % 59.67/59.68 (P2(f9(f5(f53(x3401,a1),x3402)),f9(f5(f53(x3401,a1),x3402)),f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42)))+P1(f5(a1,f3(f5(f53(f53(x3401,a1),a1),a8),f5(f53(x3401,a1),x3402))))), % 59.67/59.68 inference(scs_inference,[],[91,269,104,263,209,274,279,295,217,297,238,203,293,271,261,93,115,121,116,122,200,2,5,137,131,86,133,85,3,84,147,146,143,83,139,136])). % 59.67/59.68 cnf(352,plain, % 59.67/59.68 (P2(x3521,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42)),f9(f5(f53(x3522,a1),x3523)))+P1(f5(a1,f3(f5(f53(f53(x3522,a1),a1),a8),f5(f53(x3522,a1),x3523))))), % 59.67/59.68 inference(scs_inference,[],[91,269,104,263,209,274,279,295,217,297,238,203,293,271,261,93,115,121,116,122,200,2,5,137,131,86,133,85,3,84,147,146,143,83,139,136,109,113,110,201,114,128])). % 59.67/59.68 cnf(354,plain, % 59.67/59.68 (P2(f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42)),x3541,f9(f5(f53(x3542,a1),x3543)))+P1(f5(a1,f3(f5(f53(f53(x3542,a1),a1),a8),f5(f53(x3542,a1),x3543))))), % 59.67/59.68 inference(scs_inference,[],[91,269,104,263,209,274,279,295,217,297,238,203,293,271,261,93,115,121,116,122,200,2,5,137,131,86,133,85,3,84,147,146,143,83,139,136,109,113,110,201,114,128,130])). % 59.67/59.68 cnf(356,plain, % 59.67/59.68 (~E(f5(a1,f3(f5(f53(a1,a1),a6),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42))))),f5(a1,a4))), % 59.67/59.68 inference(scs_inference,[],[293,121])). % 59.67/59.68 cnf(358,plain, % 59.67/59.68 (E(f5(a1,f3(f5(f53(a1,a1),a6),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42))))),f5(a1,a2))), % 59.67/59.68 inference(scs_inference,[],[293,121,115])). % 59.67/59.68 cnf(360,plain, % 59.67/59.68 (P2(a2,x3601,x3601)), % 59.67/59.68 inference(scs_inference,[],[89,293,121,115,200])). % 59.67/59.68 cnf(384,plain, % 59.67/59.68 (P2(f13(f5(f53(x3841,a1),x3842)),f13(f5(f53(x3841,a1),x3842)),f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42)))+P1(f5(a1,f3(f5(f53(f53(x3841,a1),a1),a10),f5(f53(x3841,a1),x3842))))), % 59.67/59.68 inference(scs_inference,[],[91,104,306,269,312,227,221,324,335,316,277,89,215,293,121,115,200,5,125,137,131,133,86,85,3,84,147,143,83,139,136])). % 59.67/59.68 cnf(400,plain, % 59.67/59.68 (P2(f3(f5(f53(a1,a1),a6),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42)))),x4001,x4001)), % 59.67/59.68 inference(scs_inference,[],[293,200])). % 59.67/59.68 cnf(405,plain, % 59.67/59.68 (~P2(a4,f20(f5(x4051,x4052),f5(x4051,x4052)),a2)), % 59.67/59.68 inference(scs_inference,[],[104,269,356,103,293,200,5,125,137])). % 59.67/59.68 cnf(407,plain, % 59.67/59.68 (P2(f20(f5(x4071,x4072),f5(x4071,x4072)),f20(f5(x4073,x4074),f5(x4073,x4074)),a2)), % 59.67/59.68 inference(scs_inference,[],[104,269,356,103,202,293,200,5,125,137,131])). % 59.67/59.68 cnf(415,plain, % 59.67/59.68 (~E(f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a43))),f5(a1,f3(f5(f53(a1,a1),a6),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42))))))), % 59.67/59.68 inference(scs_inference,[],[104,269,358,356,263,103,202,293,221,301,238,200,5,125,137,131,133,86,85,3])). % 59.67/59.68 cnf(421,plain, % 59.67/59.68 (~P1(f5(a1,f3(f5(f53(f53(x4211,a1),a1),a8),f5(f53(x4211,a1),x4212))))+P1(f5(a1,f9(f5(f53(x4211,a1),x4212))))), % 59.67/59.68 inference(scs_inference,[],[104,269,358,356,360,263,103,202,293,221,92,301,238,261,203,200,5,125,137,131,133,86,85,3,84,143,6,83])). % 59.67/59.68 cnf(435,plain, % 59.67/59.68 (P1(f5(a1,f9(f5(f53(x4351,a1),f44(f53(x4351,a1),a8)))))+~P1(f5(a1,f3(f5(f53(f53(x4351,a1),a1),a8),f5(f53(x4351,a1),x4352))))), % 59.67/59.68 inference(scs_inference,[],[91,104,269,358,356,360,263,103,202,293,221,92,301,238,261,203,200,5,125,137,131,133,86,85,3,84,143,6,83,139,136,352,354,166,337,340,164])). % 59.67/59.68 cnf(452,plain, % 59.67/59.68 (~P2(a4,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42)),a2)), % 59.67/59.68 inference(scs_inference,[],[205,103,259,5,137])). % 59.67/59.68 cnf(456,plain, % 59.67/59.68 (P2(f3(f5(f53(a1,a1),a6),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42)))),f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42)),a2)), % 59.67/59.68 inference(scs_inference,[],[104,205,272,103,293,259,5,137,125,131])). % 59.67/59.68 cnf(458,plain, % 59.67/59.68 (P2(f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42)),f5(x4581,x4582),f5(x4581,f3(f5(f53(x4581,x4581),a6),f5(x4581,f3(f5(f53(x4583,x4581),f3(f5(f53(x4581,f53(x4583,x4581)),a35),f5(x4581,x4582))),f5(x4583,x4584))))))), % 59.67/59.68 inference(scs_inference,[],[104,205,272,103,293,225,259,246,5,137,125,131,86])). % 59.67/59.68 cnf(461,plain, % 59.67/59.68 (E(f5(a1,f3(f5(f53(a1,a1),a6),f5(a1,f9(f5(f53(x4611,a1),x4612))))),f5(a1,f3(f5(f53(f53(x4611,a1),a1),a8),f5(f53(x4611,a1),x4612))))), % 59.67/59.68 inference(scs_inference,[],[104,205,272,103,293,271,225,90,259,246,5,137,125,131,86,3])). % 59.67/59.68 cnf(465,plain, % 59.67/59.68 (E(f5(a1,f3(f5(f53(f53(x4651,a1),a1),a8),f5(f53(x4651,a1),x4652))),f5(a1,f3(f5(f53(a1,a1),a6),f5(a1,f9(f5(f53(x4651,a1),x4652))))))), % 59.67/59.68 inference(scs_inference,[],[104,205,400,272,103,293,271,225,90,259,246,215,5,137,125,131,86,3,84,2])). % 59.67/59.68 cnf(469,plain, % 59.67/59.68 (P2(f3(f5(f53(f53(x4691,a1),a1),a10),f5(f53(x4691,a1),x4692)),f3(f5(f53(f53(x4691,a1),a1),a10),f5(f53(x4691,a1),x4692)),f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42)))+P1(f5(a1,f13(f5(f53(x4691,a1),x4692))))), % 59.67/59.68 inference(scs_inference,[],[91,104,205,400,272,103,293,271,225,93,90,259,246,215,5,137,125,131,86,3,84,2,83,139,136])). % 59.67/59.68 cnf(497,plain, % 59.67/59.68 (P2(f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42)),f3(f5(f53(x4971,a1),f3(f5(f53(a1,f53(x4971,a1)),a35),f5(a1,f5(a1,f20(f5(x4972,x4973),f5(x4972,x4973)))))),f5(x4971,x4974)),f5(a1,a2))), % 59.67/59.68 inference(scs_inference,[],[104,269,308,231,293,415,5,131,125,86])). % 59.67/59.68 cnf(502,plain, % 59.67/59.68 (~E(f5(f53(x5021,a1),f3(f5(f53(x5021,f53(x5021,a1)),a21),f5(x5021,x5022))),f5(f53(x5021,a1),f3(f5(f53(a1,f53(x5021,a1)),a35),f5(a1,a4))))), % 59.67/59.68 inference(scs_inference,[],[104,269,308,231,293,217,415,238,5,131,125,86,3,85,6])). % 59.67/59.68 cnf(534,plain, % 59.67/59.68 (~P1(f5(a1,f3(f5(f53(f53(x5341,a1),a1),a8),f5(f53(x5341,a1),x5342))))+P1(f5(a1,f3(f5(f53(a1,a1),a6),f5(a1,f9(f5(f53(x5341,a1),x5342))))))), % 59.67/59.68 inference(scs_inference,[],[205,89,225,90,465,258,458,95,5,131,86,3,83])). % 59.67/59.68 cnf(613,plain, % 59.67/59.68 (~E(f5(f53(a1,f53(a1,a1)),a21),f5(f53(a1,f53(a1,a1)),a35))), % 59.67/59.68 inference(scs_inference,[],[94,502,99,5,3,6])). % 59.67/59.68 cnf(616,plain, % 59.67/59.68 (~E(a21,a35)), % 59.67/59.68 inference(scs_inference,[],[613,5])). % 59.67/59.68 cnf(639,plain, % 59.67/59.68 (~P2(f3(f5(f53(x6391,a1),f3(f5(f53(a1,f53(x6391,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a43))))),f5(x6391,x6392)),x6393,x6393)), % 59.67/59.68 inference(scs_inference,[],[203,243,122,116,201])). % 59.67/59.68 cnf(641,plain, % 59.67/59.68 (E(f5(x6411,x6412),f5(x6411,f3(f5(f53(x6413,x6411),f3(f5(f53(x6411,f53(x6413,x6411)),a35),f5(x6411,x6412))),f5(x6413,x6414))))), % 59.67/59.68 inference(scs_inference,[],[203,94,243,122,116,201,2])). % 59.67/59.68 cnf(643,plain, % 59.67/59.68 (~P2(f3(f5(f53(x6431,a1),f3(f5(f53(a1,f53(x6431,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a43))))),f5(x6431,x6432)),f20(f5(x6433,x6434),f5(x6433,x6434)),a2)), % 59.67/59.68 inference(scs_inference,[],[269,203,94,243,122,116,201,2,5,137])). % 59.67/59.68 cnf(677,plain, % 59.67/59.68 (P2(f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42)),f5(a1,a2),f5(a1,f3(f5(f53(x6771,a1),f3(f5(f53(a1,f53(x6771,a1)),a35),f5(a1,f20(f5(x6772,x6773),f5(x6772,x6773))))),f5(x6771,x6774))))), % 59.67/59.68 inference(scs_inference,[],[269,272,103,246,125,85])). % 59.67/59.68 cnf(679,plain, % 59.67/59.68 (~E(f5(a1,a4),f5(a1,f3(f5(f53(a1,a1),a6),f5(a1,f20(f5(x6791,x6792),f5(x6791,x6792))))))), % 59.67/59.68 inference(scs_inference,[],[269,272,103,90,246,125,85,3])). % 59.67/59.68 cnf(686,plain, % 59.67/59.68 (~P2(f3(f5(f53(x6861,a1),f3(f5(f53(a1,f53(x6861,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a43))))),f5(x6861,x6862)),f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42)),a2)), % 59.67/59.68 inference(scs_inference,[],[205,243,137])). % 59.67/59.68 cnf(697,plain, % 59.67/59.68 (~P1(f5(a1,f13(f5(f53(x6971,a1),f3(f5(f53(a1,f53(x6971,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a43))))))))), % 59.67/59.68 inference(scs_inference,[],[243,166])). % 59.67/59.68 cnf(698,plain, % 59.67/59.68 (~P1(f5(a1,f3(f5(f53(x6981,a1),f3(f5(f53(a1,f53(x6981,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a43))))),f5(x6981,x6982))))), % 59.67/59.68 inference(rename_variables,[],[243])). % 59.67/59.68 cnf(700,plain, % 59.67/59.68 (E(f5(a1,f3(f5(f53(x7001,a1),f3(f5(f53(a1,f53(x7001,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a43))))),f5(x7001,x7002))),f5(a1,a4))), % 59.67/59.68 inference(scs_inference,[],[243,698,166,109])). % 59.67/59.68 cnf(704,plain, % 59.67/59.68 (~P2(f13(f5(f53(x7041,a1),f3(f5(f53(a1,f53(x7041,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a43)))))),x7042,x7042)), % 59.67/59.68 inference(scs_inference,[],[243,698,166,109,113,201])). % 59.67/59.68 cnf(715,plain, % 59.67/59.68 (~P1(f5(a1,f3(f5(f53(f53(x7151,a1),a1),a10),f5(f53(x7151,a1),f3(f5(f53(a1,f53(x7151,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a43))))))))), % 59.67/59.68 inference(scs_inference,[],[91,269,93,243,698,639,166,109,113,201,5,137,128,130,85,83])). % 59.67/59.68 cnf(721,plain, % 59.67/59.68 (~P1(f5(a1,f27(f5(f53(a1,f53(x7211,a1)),a35),f5(f53(f53(x7211,a1),a1),a10))))), % 59.67/59.68 inference(scs_inference,[],[91,269,407,93,243,698,643,639,166,109,113,201,5,137,128,130,85,83,84,136,171])). % 59.67/59.68 cnf(723,plain, % 59.67/59.68 (P1(f5(a1,f29(f5(f53(a1,f53(x7231,a1)),a35),f5(f53(f53(x7231,a1),a1),a10))))), % 59.67/59.68 inference(scs_inference,[],[91,269,407,93,243,698,643,639,166,109,113,201,5,137,128,130,85,83,84,136,171,170])). % 59.67/59.68 cnf(729,plain, % 59.67/59.68 (~E(f5(a1,f29(f5(f53(a1,f53(x7291,a1)),a35),f5(f53(f53(x7291,a1),a1),a10))),f5(a1,a4))), % 59.67/59.68 inference(scs_inference,[],[91,269,407,93,243,698,643,639,166,109,113,201,5,137,128,130,85,83,84,136,171,170,110,115,121])). % 59.67/59.68 cnf(733,plain, % 59.67/59.68 (~E(f5(a1,a4),f5(a1,f29(f5(f53(a1,f53(x7331,a1)),a35),f5(f53(f53(x7331,a1),a1),a10))))), % 59.67/59.68 inference(scs_inference,[],[91,269,407,93,243,698,643,639,166,109,113,201,5,137,128,130,85,83,84,136,171,170,110,115,121,116,122])). % 59.67/59.68 cnf(735,plain, % 59.67/59.68 (P2(f29(f5(f53(a1,f53(x7351,a1)),a35),f5(f53(f53(x7351,a1),a1),a10)),x7352,x7352)), % 59.67/59.68 inference(scs_inference,[],[91,269,407,93,243,698,643,639,166,109,113,201,5,137,128,130,85,83,84,136,171,170,110,115,121,116,122,200])). % 59.67/59.68 cnf(745,plain, % 59.67/59.68 (P2(f29(f5(f53(a1,f53(x7451,a1)),a35),f5(f53(f53(x7451,a1),a1),a10)),f5(a1,f20(f5(x7452,x7453),f5(x7452,x7453))),f5(a1,a2))), % 59.67/59.68 inference(scs_inference,[],[91,269,407,93,221,243,698,643,639,166,109,113,201,5,137,128,130,85,83,84,136,171,170,110,115,121,116,122,200,114,2,133,131,3,86])). % 59.67/59.68 cnf(746,plain, % 59.67/59.68 (~P2(f29(f5(f53(a1,f53(x7461,a1)),a35),f5(f53(f53(x7461,a1),a1),a10)),f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a43)),f29(f5(f53(a1,f53(x7461,a1)),a35),f5(f53(f53(x7461,a1),a1),a10)))), % 59.67/59.68 inference(scs_inference,[],[91,104,269,407,93,221,243,698,643,639,166,109,113,201,5,137,128,130,85,83,84,136,171,170,110,115,121,116,122,200,114,2,133,131,3,86,147])). % 59.67/59.68 cnf(754,plain, % 59.67/59.68 (E(f9(f5(x7541,f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42))))),f9(f5(x7541,f5(a1,a2))))), % 59.67/59.68 inference(scs_inference,[],[205,54,5])). % 59.67/59.68 cnf(759,plain, % 59.67/59.68 (~P2(f3(f5(f53(f53(x7591,a1),a1),a10),f5(f53(x7591,a1),f3(f5(f53(a1,f53(x7591,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a43)))))),x7592,x7592)), % 59.67/59.68 inference(scs_inference,[],[697,715,109,113,201])). % 59.67/59.68 cnf(765,plain, % 59.67/59.68 (P2(x7651,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42)),f13(f5(f53(x7652,a1),f3(f5(f53(a1,f53(x7652,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a43)))))))), % 59.67/59.68 inference(scs_inference,[],[91,205,729,754,697,715,109,113,201,2,5,137,128])). % 59.67/59.68 cnf(767,plain, % 59.67/59.68 (P2(f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42)),x7671,f13(f5(f53(x7672,a1),f3(f5(f53(a1,f53(x7672,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a43)))))))), % 59.67/59.68 inference(scs_inference,[],[91,205,729,754,697,715,109,113,201,2,5,137,128,130])). % 59.67/59.68 cnf(773,plain, % 59.67/59.68 (~P1(f5(a1,f3(f5(f53(f53(f53(x7731,a1),a1),a1),f3(f5(f53(f53(a1,f53(x7731,a1)),f53(f53(f53(x7731,a1),a1),a1)),a26),f5(f53(a1,f53(x7731,a1)),a35))),f5(f53(f53(x7731,a1),a1),a10))))), % 59.67/59.68 inference(scs_inference,[],[91,205,735,729,97,754,746,697,715,721,723,109,113,201,2,5,137,128,130,131,85,83])). % 59.67/59.68 cnf(782,plain, % 59.67/59.68 (E(f3(x7821,f3(f5(a1,f20(f5(x7822,x7823),f5(x7822,x7823))),x7824)),f3(x7821,f3(f5(a1,a2),x7824)))), % 59.67/59.68 inference(scs_inference,[],[269,7,6])). % 59.67/59.68 cnf(785,plain, % 59.67/59.68 (~P2(f3(f5(f53(f53(f53(x7851,a1),a1),a1),f3(f5(f53(f53(a1,f53(x7851,a1)),f53(f53(f53(x7851,a1),a1),a1)),a26),f5(f53(a1,f53(x7851,a1)),a35))),f5(f53(f53(x7851,a1),a1),a10)),x7852,x7852)), % 59.67/59.68 inference(scs_inference,[],[773,721,113,201])). % 59.67/59.68 cnf(798,plain, % 59.67/59.68 (~P2(f13(f5(f53(x7981,a1),f3(f5(f53(a1,f53(x7981,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a43)))))),x7982,x7982)), % 59.67/59.68 inference(rename_variables,[],[704])). % 59.67/59.68 cnf(799,plain, % 59.67/59.68 (P1(f5(a1,f3(f5(f53(x7991,a1),f3(f5(f53(a1,f53(x7991,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42))))),f5(x7991,x7992))))), % 59.67/59.68 inference(scs_inference,[],[91,269,312,733,103,641,782,704,773,721,113,201,2,5,137,125,128,130,85,83])). % 59.67/59.68 cnf(808,plain, % 59.67/59.68 (P1(f5(a1,f9(f5(f53(x8081,a1),f3(f5(f53(a1,f53(x8081,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42))))))))), % 59.67/59.68 inference(scs_inference,[],[91,104,269,314,312,356,765,733,103,217,221,641,452,782,704,798,773,721,113,201,2,5,137,125,128,130,85,83,3,84,86,143,167])). % 59.67/59.68 cnf(810,plain, % 59.67/59.68 (E(f5(a1,f9(f5(f53(x8101,a1),f3(f5(f53(a1,f53(x8101,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42))))))),f5(a1,a2))), % 59.67/59.68 inference(scs_inference,[],[91,104,269,314,312,356,765,733,103,217,221,641,452,782,704,798,773,721,113,201,2,5,137,125,128,130,85,83,3,84,86,143,167,115])). % 59.67/59.68 cnf(812,plain, % 59.67/59.68 (~E(f5(a1,f9(f5(f53(x8121,a1),f3(f5(f53(a1,f53(x8121,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42))))))),f5(a1,a4))), % 59.67/59.68 inference(scs_inference,[],[91,104,269,314,312,356,765,733,103,217,221,641,452,782,704,798,773,721,113,201,2,5,137,125,128,130,85,83,3,84,86,143,167,115,121])). % 59.67/59.68 cnf(814,plain, % 59.67/59.68 (P2(f9(f5(f53(x8141,a1),f3(f5(f53(a1,f53(x8141,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42)))))),x8142,x8142)), % 59.67/59.68 inference(scs_inference,[],[91,104,269,314,312,356,765,733,103,217,221,641,452,782,704,798,773,721,113,201,2,5,137,125,128,130,85,83,3,84,86,143,167,115,121,200])). % 59.67/59.68 cnf(818,plain, % 59.67/59.68 (E(f53(f53(x8181,f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42)))),x8182),f53(f53(x8181,f5(a1,a2)),x8182))), % 59.67/59.68 inference(scs_inference,[],[205,9,10])). % 59.67/59.68 cnf(819,plain, % 59.67/59.68 (E(f5(a1,f3(f5(f53(x8191,a1),f3(f5(f53(a1,f53(x8191,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42))))),f5(x8191,x8192))),f5(a1,a2))), % 59.67/59.68 inference(scs_inference,[],[799,115])). % 59.67/59.68 cnf(823,plain, % 59.67/59.68 (P2(f3(f5(f53(x8231,a1),f3(f5(f53(a1,f53(x8231,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42))))),f5(x8231,x8232)),x8233,x8233)), % 59.67/59.68 inference(scs_inference,[],[799,115,121,200])). % 59.67/59.68 cnf(825,plain, % 59.67/59.68 (~P2(f27(f5(f53(a1,f53(x8251,a1)),a35),f5(f53(f53(x8251,a1),a1),a10)),x8252,x8252)), % 59.67/59.68 inference(scs_inference,[],[799,721,115,121,200,201])). % 59.67/59.68 cnf(831,plain, % 59.67/59.68 (~P2(f3(f5(f53(f53(x8311,a1),a1),a10),f5(f53(x8311,a1),f3(f5(f53(a1,f53(x8311,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a43)))))),f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42)),a2)), % 59.67/59.68 inference(scs_inference,[],[205,812,818,799,715,721,115,121,200,201,2,5,133,137])). % 59.67/59.68 cnf(835,plain, % 59.67/59.68 (P2(f3(f5(f53(x8351,a1),f3(f5(f53(a1,f53(x8351,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42))))),f5(x8351,x8352)),f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42)),a2)), % 59.67/59.68 inference(scs_inference,[],[205,308,812,103,818,799,715,721,115,121,200,201,2,5,133,137,125,131])). % 59.67/59.68 cnf(837,plain, % 59.67/59.68 (P2(f9(f5(f53(x8371,a1),f3(f5(f53(a1,f53(x8371,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42)))))),f5(a1,a2),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42))))), % 59.67/59.68 inference(scs_inference,[],[205,308,814,812,103,818,799,715,721,115,121,200,201,2,5,133,137,125,131,85])). % 59.67/59.68 cnf(838,plain, % 59.67/59.68 (P2(f9(f5(f53(x8381,a1),f3(f5(f53(a1,f53(x8381,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42)))))),x8382,x8382)), % 59.67/59.68 inference(rename_variables,[],[814])). % 59.67/59.68 cnf(839,plain, % 59.67/59.68 (~P1(f5(a1,f3(f5(f53(f53(a34,a1),a1),f3(f5(f53(f53(a33,a34),f53(f53(a34,a1),a1)),a32),f5(f53(a33,a34),a41))),f5(f53(a34,a1),a43))))), % 59.67/59.68 inference(scs_inference,[],[104,205,308,814,812,103,818,799,101,715,721,115,121,200,201,2,5,133,137,125,131,85,83])). % 59.67/59.68 cnf(841,plain, % 59.67/59.68 (~E(f5(a1,f3(f5(f53(x8411,a1),f3(f5(f53(x8411,f53(x8411,a1)),a21),f5(x8411,x8412))),f5(x8411,x8412))),f5(a1,f3(f5(f53(a1,a1),a6),f5(a1,a4))))), % 59.67/59.68 inference(scs_inference,[],[104,205,308,814,812,103,90,818,799,101,715,721,115,121,200,201,2,5,133,137,125,131,85,83,3])). % 59.67/59.68 cnf(844,plain, % 59.67/59.68 (P2(f9(f5(f53(x8441,a1),f3(f5(f53(a1,f53(x8441,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42)))))),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42))),f5(a1,a2))), % 59.67/59.68 inference(scs_inference,[],[104,205,456,308,814,838,812,103,90,818,799,686,101,715,721,115,121,200,201,2,5,133,137,125,131,85,83,3,84,86])). % 59.67/59.68 cnf(853,plain, % 59.67/59.68 (~E(f5(a1,f3(f5(f53(f53(a34,a1),a1),f3(f5(f53(f53(a33,a34),f53(f53(a34,a1),a1)),a32),f5(f53(a33,a34),a41))),f5(f53(a34,a1),a43))),f5(a1,a2))), % 59.67/59.68 inference(scs_inference,[],[91,104,205,456,308,814,838,812,103,221,90,818,799,808,686,101,715,721,115,121,200,201,2,5,133,137,125,131,85,83,3,84,86,143,136,6,109,113])). % 59.67/59.68 cnf(859,plain, % 59.67/59.68 (E(f23(f50(f5(a1,f20(f5(x8591,x8592),f5(x8591,x8592))),x8593,x8594,x8595),x8596),f23(f50(f5(a1,a2),x8593,x8594,x8595),x8596))), % 59.67/59.68 inference(scs_inference,[],[269,15,11])). % 59.67/59.68 cnf(862,plain, % 59.67/59.68 (~E(f5(a1,a2),f5(a1,f3(f5(f53(f53(a34,a1),a1),f3(f5(f53(f53(a33,a34),f53(f53(a34,a1),a1)),a32),f5(f53(a33,a34),a41))),f5(f53(a34,a1),a43))))), % 59.67/59.68 inference(scs_inference,[],[839,110,114])). % 59.67/59.68 cnf(864,plain, % 59.67/59.68 (~P2(f3(f5(f53(f53(a34,a1),a1),f3(f5(f53(f53(a33,a34),f53(f53(a34,a1),a1)),a32),f5(f53(a33,a34),a41))),f5(f53(a34,a1),a43)),x8641,x8641)), % 59.67/59.68 inference(scs_inference,[],[839,110,114,201])). % 59.67/59.68 cnf(866,plain, % 59.67/59.68 (E(f23(f50(f5(a1,a2),x8661,x8662,x8663),x8664),f23(f50(f5(a1,f20(f5(x8665,x8666),f5(x8665,x8666))),x8661,x8662,x8663),x8664))), % 59.67/59.68 inference(scs_inference,[],[859,839,110,114,201,2])). % 59.67/59.68 cnf(897,plain, % 59.67/59.68 (E(f23(x8971,f50(x8972,f5(a1,f20(f5(x8973,x8974),f5(x8973,x8974))),x8975,x8976)),f23(x8971,f50(x8972,f5(a1,a2),x8975,x8976)))), % 59.67/59.68 inference(scs_inference,[],[269,16,12])). % 59.67/59.68 cnf(898,plain, % 59.67/59.68 (E(f23(x8981,f50(x8982,f5(a1,a2),x8983,x8984)),f23(x8981,f50(x8982,f5(a1,f20(f5(x8985,x8986),f5(x8985,x8986))),x8983,x8984)))), % 59.67/59.68 inference(scs_inference,[],[897,2])). % 59.67/59.68 cnf(929,plain, % 59.67/59.68 (E(f19(f50(x9291,x9292,f5(a1,f20(f5(x9293,x9294),f5(x9293,x9294))),x9295),x9296),f19(f50(x9291,x9292,f5(a1,a2),x9295),x9296))), % 59.67/59.68 inference(scs_inference,[],[269,17,13])). % 59.67/59.68 cnf(930,plain, % 59.67/59.68 (E(f19(f50(x9301,x9302,f5(a1,a2),x9303),x9304),f19(f50(x9301,x9302,f5(a1,f20(f5(x9305,x9306),f5(x9305,x9306))),x9303),x9304))), % 59.67/59.68 inference(scs_inference,[],[929,2])). % 59.67/59.68 cnf(936,plain, % 59.67/59.68 (~E(f5(a1,a4),f5(a1,f3(f5(f53(a1,a1),a6),f5(a1,f3(f5(f53(a1,a1),a6),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42))))))))), % 59.67/59.68 inference(scs_inference,[],[269,312,243,90,721,862,929,2,5,125,137,3])). % 59.67/59.68 cnf(942,plain, % 59.67/59.68 (~E(f5(f53(f53(a34,a1),a1),f3(f5(f53(f53(a34,a1),f53(f53(a34,a1),a1)),a21),f5(f53(a34,a1),a43))),f5(f53(f53(a34,a1),a1),f3(f5(f53(f53(a33,a34),f53(f53(a34,a1),a1)),a32),f5(f53(a33,a34),a41))))), % 59.67/59.68 inference(scs_inference,[],[269,314,312,767,243,90,721,864,862,929,256,2,5,125,137,3,84,86,6])). % 59.67/59.68 cnf(950,plain, % 59.67/59.68 (E(f19(x9501,f50(x9502,x9503,x9504,f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42))))),f19(x9501,f50(x9502,x9503,x9504,f5(a1,a2))))), % 59.67/59.68 inference(scs_inference,[],[205,18,14])). % 59.67/59.68 cnf(951,plain, % 59.67/59.68 (E(f19(x9511,f50(x9512,x9513,x9514,f5(a1,a2))),f19(x9511,f50(x9512,x9513,x9514,f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42))))))), % 59.67/59.68 inference(scs_inference,[],[950,2])). % 59.67/59.68 cnf(957,plain, % 59.67/59.68 (~E(f5(a1,f3(f5(f53(a1,a1),a6),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42))))),f5(a1,f3(f5(f53(a1,a1),a6),f5(a1,a4))))), % 59.67/59.68 inference(scs_inference,[],[269,356,103,90,715,950,942,2,5,125,137,3])). % 59.67/59.68 cnf(961,plain, % 59.67/59.68 (P2(f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42)),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42))),f5(a1,a2))), % 59.67/59.68 inference(scs_inference,[],[269,819,360,356,103,90,715,246,950,942,785,2,5,125,137,3,84,86])). % 59.67/59.68 cnf(968,plain, % 59.67/59.68 (E(f7(f7(x9681,f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42)))),x9682),f7(f7(x9681,f5(a1,a2)),x9682))), % 59.67/59.68 inference(scs_inference,[],[205,19,20])). % 59.67/59.68 cnf(973,plain, % 59.67/59.68 (~E(f5(a1,f20(f5(x9731,x9732),f5(x9731,x9732))),f5(a1,f3(f5(f53(a1,a1),a6),f5(a1,a4))))), % 59.67/59.68 inference(scs_inference,[],[274,103,90,968,957,2,5,125,3])). % 59.67/59.68 cnf(979,plain, % 59.67/59.68 (P2(f29(f5(f53(a1,f53(x9791,a1)),a35),f5(f53(f53(x9791,a1),a1),a10)),f5(a1,a2),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42))))), % 59.67/59.68 inference(scs_inference,[],[269,400,207,274,103,90,968,957,745,864,2,5,125,3,84,86,83,85])). % 59.67/59.68 cnf(980,plain, % 59.67/59.68 (E(f29(f29(x9801,f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42)))),x9802),f29(f29(x9801,f5(a1,a2)),x9802))), % 59.67/59.68 inference(scs_inference,[],[205,21,22])). % 59.67/59.68 cnf(985,plain, % 59.67/59.68 (P2(f29(f5(f53(a1,f53(x9851,a1)),a35),f5(f53(f53(x9851,a1),a1),a10)),f5(a1,f3(f5(f53(a1,a1),a6),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42))))),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42))))), % 59.67/59.68 inference(scs_inference,[],[310,272,721,980,979,973,2,5,125,85])). % 59.67/59.68 cnf(991,plain, % 59.67/59.68 (P2(f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42)),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42))),f5(a1,f3(f5(f53(a1,a1),a6),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42))))))), % 59.67/59.68 inference(scs_inference,[],[360,310,272,721,961,980,951,930,979,973,704,2,5,125,85,3,84,86])). % 59.67/59.68 cnf(993,plain, % 59.67/59.68 (E(f25(f51(f5(a1,f20(f5(x9931,x9932),f5(x9931,x9932))),x9933,x9934,x9935),x9936),f25(f51(f5(a1,a2),x9933,x9934,x9935),x9936))), % 59.67/59.68 inference(scs_inference,[],[269,31,23])). % 59.67/59.68 cnf(994,plain, % 59.67/59.68 (E(f25(f51(f5(a1,a2),x9941,x9942,x9943),x9944),f25(f51(f5(a1,f20(f5(x9945,x9946),f5(x9945,x9946))),x9941,x9942,x9943),x9944))), % 59.67/59.68 inference(scs_inference,[],[993,2])). % 59.67/59.68 cnf(996,plain, % 59.67/59.68 (~P2(f3(f5(f53(f53(a34,a1),a1),f3(f5(f53(f53(a33,a34),f53(f53(a34,a1),a1)),a32),f5(f53(a33,a34),a41))),f5(f53(a34,a1),a43)),f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42)),a2)), % 59.67/59.68 inference(scs_inference,[],[205,839,993,936,2,5,137])). % 59.67/59.68 cnf(1006,plain, % 59.67/59.68 (P2(f9(f5(f53(x10061,a1),f3(f5(f53(a1,f53(x10061,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42)))))),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42))),f5(a1,f20(f5(x10062,x10063),f5(x10062,x10063))))), % 59.67/59.68 inference(scs_inference,[],[205,360,265,211,721,839,844,837,993,866,898,936,759,2,5,137,125,85,3,84,86])). % 59.67/59.68 cnf(1008,plain, % 59.67/59.68 (E(f25(x10081,f51(x10082,f5(a1,f20(f5(x10083,x10084),f5(x10083,x10084))),x10085,x10086)),f25(x10081,f51(x10082,f5(a1,a2),x10085,x10086)))), % 59.67/59.68 inference(scs_inference,[],[269,32,24])). % 59.67/59.68 cnf(1011,plain, % 59.67/59.68 (~P2(f3(f5(f53(f53(f53(x10111,a1),a1),a1),f3(f5(f53(f53(a1,f53(x10111,a1)),f53(f53(f53(x10111,a1),a1),a1)),a26),f5(f53(a1,f53(x10111,a1)),a35))),f5(f53(f53(x10111,a1),a1),a10)),f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42)),a2)), % 59.67/59.68 inference(scs_inference,[],[205,773,1008,841,2,5,137])). % 59.67/59.68 cnf(1014,plain, % 59.67/59.68 (E(f25(f51(f5(a1,a2),x10141,x10142,x10143),f51(x10144,f5(a1,f20(f5(x10145,x10146),f5(x10145,x10146))),x10147,x10148)),f25(f51(f5(a1,f20(f5(x10149,x101410),f5(x10149,x101410))),x10141,x10142,x10143),f51(x10144,f5(a1,a2),x10147,x10148)))), % 59.67/59.68 inference(scs_inference,[],[205,773,1008,994,991,841,2,5,137,85,3])). % 59.67/59.68 cnf(1017,plain, % 59.67/59.68 (~E(f3(f5(f53(x10171,a1),f3(f5(f53(a1,f53(x10171,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42))))),f5(x10171,x10172)),f3(f5(f53(f53(a34,a1),a1),f3(f5(f53(f53(a33,a34),f53(f53(a34,a1),a1)),a32),f5(f53(a33,a34),a41))),f5(f53(a34,a1),a43)))), % 59.67/59.68 inference(scs_inference,[],[205,835,773,1008,994,991,841,996,2,5,137,85,3,84])). % 59.67/59.68 cnf(1019,plain, % 59.67/59.68 (~E(f5(f53(a1,a1),f3(f5(f53(a1,f53(a1,a1)),a21),f5(a1,a4))),f5(f53(a1,a1),a6))), % 59.67/59.68 inference(scs_inference,[],[205,835,773,1008,994,985,991,841,996,2,5,137,85,3,84,86,6])). % 59.67/59.68 cnf(1021,plain, % 59.67/59.68 (E(f44(f51(x10211,x10212,f5(a1,f20(f5(x10213,x10214),f5(x10213,x10214))),x10215),x10216),f44(f51(x10211,x10212,f5(a1,a2),x10215),x10216))), % 59.67/59.68 inference(scs_inference,[],[269,37,25])). % 59.67/59.68 cnf(1026,plain, % 59.67/59.68 (P2(f9(f5(f53(x10261,a1),f3(f5(f53(a1,f53(x10261,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42)))))),f5(a1,a2),f5(a1,f20(f5(x10262,x10263),f5(x10262,x10263))))), % 59.67/59.68 inference(scs_inference,[],[205,1019,1021,1017,1006,6,2,5,85])). % 59.67/59.68 cnf(1046,plain, % 59.67/59.68 (E(f16(f47(f5(a1,f20(f5(x10461,x10462),f5(x10461,x10462))),x10463,x10464,x10465),x10466),f16(f47(f5(a1,a2),x10463,x10464,x10465),x10466))), % 59.67/59.68 inference(scs_inference,[],[269,39,27])). % 59.67/59.68 cnf(1047,plain, % 59.67/59.68 (E(f16(f47(f5(a1,a2),x10471,x10472,x10473),x10474),f16(f47(f5(a1,f20(f5(x10475,x10476),f5(x10475,x10476))),x10471,x10472,x10473),x10474))), % 59.67/59.68 inference(scs_inference,[],[1046,2])). % 59.67/59.68 cnf(1101,plain, % 59.67/59.68 (E(f25(f51(f5(a1,f20(f5(x11011,x11012),f5(x11011,x11012))),x11013,x11014,x11015),f51(x11016,f5(a1,a2),x11017,x11018)),f25(f51(f5(a1,a2),x11013,x11014,x11015),f51(x11016,f5(a1,f20(f5(x11019,x110110),f5(x11019,x110110))),x11017,x11018)))), % 59.67/59.68 inference(scs_inference,[],[1014,2])). % 59.67/59.68 cnf(1102,plain, % 59.67/59.68 (E(f19(f50(x11021,x11022,f5(a1,a2),x11023),f50(x11024,x11025,x11026,f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42))))),f19(f50(x11021,x11022,f5(a1,f20(f5(x11027,x11028),f5(x11027,x11028))),x11023),f50(x11024,x11025,x11026,f5(a1,a2))))), % 59.67/59.68 inference(scs_inference,[],[950,930,1014,2,3])). % 59.67/59.68 cnf(1109,plain, % 59.67/59.68 (E(f25(f51(f5(a1,f20(f5(x11091,x11092),f5(x11091,x11092))),x11093,x11094,x11095),f51(x11096,f5(a1,a2),x11097,x11098)),f25(f51(f5(a1,f20(f5(x11099,x110910),f5(x11099,x110910))),x11093,x11094,x11095),f51(x11096,f5(a1,f20(f5(x110911,x110912),f5(x110911,x110912))),x11097,x11098)))), % 59.67/59.68 inference(scs_inference,[],[1102,1101,994,2,3])). % 59.67/59.68 cnf(1116,plain, % 59.67/59.68 (E(f16(x11161,f47(x11162,f5(a1,f20(f5(x11163,x11164),f5(x11163,x11164))),x11165,x11166)),f16(x11161,f47(x11162,f5(a1,a2),x11165,x11166)))), % 59.67/59.68 inference(scs_inference,[],[269,40,28])). % 59.67/59.68 cnf(1117,plain, % 59.67/59.68 (E(f16(x11171,f47(x11172,f5(a1,a2),x11173,x11174)),f16(x11171,f47(x11172,f5(a1,f20(f5(x11175,x11176),f5(x11175,x11176))),x11173,x11174)))), % 59.67/59.68 inference(scs_inference,[],[1116,2])). % 59.67/59.68 cnf(1120,plain, % 59.67/59.68 (E(f16(f47(f5(a1,a2),x11201,x11202,x11203),f47(x11204,f5(a1,f20(f5(x11205,x11206),f5(x11205,x11206))),x11207,x11208)),f16(f47(f5(a1,f20(f5(x11209,x112010),f5(x11209,x112010))),x11201,x11202,x11203),f47(x11204,f5(a1,a2),x11207,x11208)))), % 59.67/59.68 inference(scs_inference,[],[263,1116,1047,825,2,84,3])). % 59.67/59.68 cnf(1126,plain, % 59.67/59.68 (E(f16(f47(f5(a1,f20(f5(x11261,x11262),f5(x11261,x11262))),x11263,x11264,x11265),f47(x11266,f5(a1,a2),x11267,x11268)),f16(f47(f5(a1,a2),x11263,x11264,x11265),f47(x11266,f5(a1,f20(f5(x11269,x112610),f5(x11269,x112610))),x11267,x11268)))), % 59.67/59.68 inference(scs_inference,[],[1120,2])). % 59.67/59.68 cnf(1129,plain, % 59.67/59.68 (E(f16(f47(f5(a1,a2),x11291,x11292,x11293),f47(x11294,f5(a1,f20(f5(x11295,x11296),f5(x11295,x11296))),x11297,x11298)),f16(f47(f5(a1,f20(f5(x11299,x112910),f5(x11299,x112910))),x11291,x11292,x11293),f47(x11294,f5(a1,f20(f5(x112911,x112912),f5(x112911,x112912))),x11297,x11298)))), % 59.67/59.68 inference(scs_inference,[],[814,1117,1120,864,2,84,3])). % 59.67/59.68 cnf(1139,plain, % 59.67/59.68 (~E(f5(f53(x11391,a1),f3(f5(f53(x11391,f53(x11391,a1)),a21),f5(x11391,x11392))),f5(f53(x11391,a1),f3(f5(f53(a1,f53(x11391,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a43))))))), % 59.67/59.68 inference(scs_inference,[],[314,1126,1109,1129,639,2,84,3,6])). % 59.67/59.68 cnf(1376,plain, % 59.67/59.68 (E(f5(a1,f3(f5(f53(a1,a1),a6),f5(a1,f3(f5(f53(f53(x13761,a1),a1),a10),f5(f53(x13761,a1),x13762))))),f5(a1,f13(f5(f53(x13761,a1),x13762))))), % 59.67/59.68 inference(scs_inference,[],[93,90,3])). % 59.67/59.68 cnf(1480,plain, % 59.67/59.68 (E(f20(f37(x14801,x14802,f5(a1,f20(f5(x14803,x14804),f5(x14803,x14804))),x14805),x14806),f20(f37(x14801,x14802,f5(a1,a2),x14805),x14806))), % 59.67/59.68 inference(scs_inference,[],[269,55,35])). % 59.67/59.68 cnf(1481,plain, % 59.67/59.68 (E(f20(f37(x14811,x14812,f5(a1,a2),x14813),x14814),f20(f37(x14811,x14812,f5(a1,f20(f5(x14815,x14816),f5(x14815,x14816))),x14813),x14814))), % 59.67/59.68 inference(scs_inference,[],[1480,2])). % 59.67/59.68 cnf(1500,plain, % 59.67/59.68 (~P1(f5(a1,f7(f5(f53(x15001,x15002),x15003),f5(f53(x15002,a1),f3(f5(f53(x15002,f53(x15002,a1)),a21),f5(x15002,f3(f5(f53(x15001,x15002),x15003),f5(x15001,x15004))))))))), % 59.67/59.68 inference(scs_inference,[],[203,179])). % 59.67/59.68 cnf(1501,plain, % 59.67/59.68 (P1(f5(a1,f3(f5(f53(x15011,a1),f3(f5(f53(x15011,f53(x15011,a1)),a21),f5(x15011,x15012))),f5(x15011,x15012))))), % 59.67/59.68 inference(rename_variables,[],[203])). % 59.67/59.68 cnf(1503,plain, % 59.67/59.68 (P1(f5(a1,f23(f5(f53(x15031,x15032),x15033),f5(f53(x15032,a1),f3(f5(f53(x15032,f53(x15032,a1)),a21),f5(x15032,f3(f5(f53(x15031,x15032),x15033),f5(x15031,x15034))))))))), % 59.67/59.68 inference(scs_inference,[],[203,1501,179,178])). % 59.67/59.68 cnf(1506,plain, % 59.67/59.68 (P1(f5(a1,f23(f5(f53(x15061,x15062),x15063),f5(f53(x15062,a1),f3(f5(f53(a1,f53(x15062,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a43))))))))), % 59.67/59.68 inference(scs_inference,[],[203,1501,243,179,178,180])). % 59.67/59.68 cnf(1507,plain, % 59.67/59.68 (~P1(f5(a1,f3(f5(f53(x15071,a1),f3(f5(f53(a1,f53(x15071,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a43))))),f5(x15071,x15072))))), % 59.67/59.68 inference(rename_variables,[],[243])). % 59.67/59.68 cnf(1509,plain, % 59.67/59.68 (P1(f5(a1,f25(f5(f53(x15091,x15092),x15093),f5(f53(x15092,a1),f3(f5(f53(a1,f53(x15092,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a43))))))))), % 59.67/59.68 inference(scs_inference,[],[203,1501,243,1507,179,178,180,181])). % 59.67/59.68 cnf(1510,plain, % 59.67/59.68 (~P1(f5(a1,f3(f5(f53(x15101,a1),f3(f5(f53(a1,f53(x15101,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a43))))),f5(x15101,x15102))))), % 59.67/59.68 inference(rename_variables,[],[243])). % 59.67/59.68 cnf(1512,plain, % 59.67/59.68 (P1(f5(a1,f29(f5(f53(x15121,x15122),x15123),f5(f53(x15122,a1),f3(f5(f53(a1,f53(x15122,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42))))))))), % 59.67/59.68 inference(scs_inference,[],[203,1501,243,1507,799,179,178,180,181,188])). % 59.67/59.68 cnf(1513,plain, % 59.67/59.68 (P1(f5(a1,f3(f5(f53(x15131,a1),f3(f5(f53(a1,f53(x15131,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42))))),f5(x15131,x15132))))), % 59.67/59.68 inference(rename_variables,[],[799])). % 59.67/59.68 cnf(1515,plain, % 59.67/59.68 (P1(f5(a1,f31(f5(f53(x15151,x15152),x15153),f5(f53(x15152,a1),f3(f5(f53(a1,f53(x15152,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42))))))))), % 59.67/59.68 inference(scs_inference,[],[203,1501,243,1507,799,1513,179,178,180,181,188,189])). % 59.67/59.68 cnf(1516,plain, % 59.67/59.68 (P1(f5(a1,f3(f5(f53(x15161,a1),f3(f5(f53(a1,f53(x15161,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42))))),f5(x15161,x15162))))), % 59.67/59.68 inference(rename_variables,[],[799])). % 59.67/59.68 cnf(1518,plain, % 59.67/59.68 (P1(f5(a1,f27(f5(f53(x15181,x15182),x15183),f5(f53(x15182,a1),f3(f5(f53(a1,f53(x15182,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42))))))))), % 59.67/59.68 inference(scs_inference,[],[203,1501,243,1507,799,1513,1516,179,178,180,181,188,189,194])). % 59.67/59.68 cnf(1519,plain, % 59.67/59.68 (P1(f5(a1,f3(f5(f53(x15191,a1),f3(f5(f53(a1,f53(x15191,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42))))),f5(x15191,x15192))))), % 59.67/59.68 inference(rename_variables,[],[799])). % 59.67/59.68 cnf(1523,plain, % 59.67/59.68 (~P1(f5(a1,f27(f5(f53(x15231,x15232),x15233),f5(f53(x15232,a1),f3(f5(f53(a1,f53(x15232,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a43))))))))), % 59.67/59.68 inference(scs_inference,[],[203,1501,243,1507,1510,799,1513,1516,179,178,180,181,188,189,194,121,171])). % 59.67/59.68 cnf(1524,plain, % 59.67/59.68 (~P1(f5(a1,f3(f5(f53(x15241,a1),f3(f5(f53(a1,f53(x15241,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a43))))),f5(x15241,x15242))))), % 59.67/59.68 inference(rename_variables,[],[243])). % 59.67/59.68 cnf(1528,plain, % 59.67/59.68 (P1(f5(a1,f7(f5(f53(x15281,x15282),x15283),f5(f53(x15282,a1),f3(f5(f53(a1,f53(x15282,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a43))))))))), % 59.67/59.68 inference(scs_inference,[],[203,1501,243,1507,1510,1524,799,1513,1516,179,178,180,181,188,189,194,121,171,200,192])). % 59.67/59.68 cnf(1529,plain, % 59.67/59.68 (~P1(f5(a1,f3(f5(f53(x15291,a1),f3(f5(f53(a1,f53(x15291,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a43))))),f5(x15291,x15292))))), % 59.67/59.68 inference(rename_variables,[],[243])). % 59.67/59.68 cnf(1531,plain, % 59.67/59.68 (P1(f5(a1,f29(f5(f53(x15311,x15312),x15313),f5(f53(x15312,a1),f3(f5(f53(a1,f53(x15312,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a43))))))))), % 59.67/59.68 inference(scs_inference,[],[203,1501,243,1507,1510,1524,1529,799,1513,1516,179,178,180,181,188,189,194,121,171,200,192,170])). % 59.67/59.68 cnf(1532,plain, % 59.67/59.68 (~P1(f5(a1,f3(f5(f53(x15321,a1),f3(f5(f53(a1,f53(x15321,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a43))))),f5(x15321,x15322))))), % 59.67/59.68 inference(rename_variables,[],[243])). % 59.67/59.68 cnf(1541,plain, % 59.67/59.68 (~E(f5(a1,a4),f5(a1,f3(f5(f53(x15411,a1),f3(f5(f53(a1,f53(x15411,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42))))),f5(x15411,x15412))))), % 59.67/59.68 inference(scs_inference,[],[203,1501,715,243,1507,1510,1524,1529,799,1513,1516,1519,179,178,180,181,188,189,194,121,171,200,192,170,5,109,113,116,122])). % 59.67/59.68 cnf(1543,plain, % 59.67/59.68 (~P2(f7(f5(f53(x15431,x15432),x15433),f5(f53(x15432,a1),f3(f5(f53(x15432,f53(x15432,a1)),a21),f5(x15432,f3(f5(f53(x15431,x15432),x15433),f5(x15431,x15434)))))),x15435,x15435)), % 59.67/59.68 inference(scs_inference,[],[203,1501,715,243,1507,1510,1524,1529,799,1513,1516,1519,179,178,180,181,188,189,194,121,171,200,192,170,5,109,113,116,122,201])). % 59.67/59.68 cnf(1556,plain, % 59.67/59.68 (P2(x15561,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42)),f3(f5(f53(f53(x15562,a1),a1),a10),f5(f53(x15562,a1),f3(f5(f53(a1,f53(x15562,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a43)))))))), % 59.67/59.68 inference(scs_inference,[],[91,205,810,203,1501,715,243,1507,1510,1524,1529,1532,799,1513,1516,1519,179,178,180,181,188,189,194,121,171,200,192,170,5,109,113,116,122,201,110,115,114,2,137,131,128])). % 59.67/59.68 cnf(1566,plain, % 59.67/59.68 (P1(f5(a1,f3(f5(f53(f53(x15661,a1),a1),a8),f5(f53(x15661,a1),f3(f5(f53(a1,f53(x15661,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42))))))))), % 59.67/59.68 inference(scs_inference,[],[91,205,810,283,207,203,1501,715,243,1507,1510,1524,1529,1532,799,1513,1516,1519,221,497,808,271,677,831,179,178,180,181,188,189,194,121,171,200,192,170,5,109,113,116,122,201,110,115,114,2,137,131,128,133,130,3,84,85,86,83])). % 59.67/59.68 cnf(1574,plain, % 59.67/59.68 (~P2(f3(f5(f53(x15741,a1),f3(f5(f53(a1,f53(x15741,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42))))),f5(x15741,x15742)),f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a43)),f3(f5(f53(x15741,a1),f3(f5(f53(a1,f53(x15741,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42))))),f5(x15741,x15742)))), % 59.67/59.68 inference(scs_inference,[],[104,91,205,810,283,207,203,1501,715,243,1507,1510,1524,1529,1532,799,1513,1516,1519,221,497,808,271,677,831,179,178,180,181,188,189,194,121,171,200,192,170,5,109,113,116,122,201,110,115,114,2,137,131,128,133,130,3,84,85,86,83,143,136,146,147])). % 59.67/59.68 cnf(1576,plain, % 59.67/59.68 (P1(f5(a1,f9(f5(f53(x15761,a1),f44(f53(x15761,a1),a8)))))), % 59.67/59.68 inference(scs_inference,[],[104,91,205,810,283,207,203,1501,715,243,1507,1510,1524,1529,1532,799,1513,1516,1519,221,497,808,271,677,831,179,178,180,181,188,189,194,121,171,200,192,170,5,109,113,116,122,201,110,115,114,2,137,131,128,133,130,3,84,85,86,83,143,136,146,147,435])). % 59.67/59.68 cnf(1578,plain, % 59.67/59.68 (P1(f5(a1,f3(f5(f53(x15781,a1),f44(f53(x15781,a1),a8)),f5(x15781,x15782))))), % 59.67/59.68 inference(scs_inference,[],[104,91,205,810,283,207,203,1501,715,243,1507,1510,1524,1529,1532,799,1513,1516,1519,221,497,808,271,677,831,179,178,180,181,188,189,194,121,171,200,192,170,5,109,113,116,122,201,110,115,114,2,137,131,128,133,130,3,84,85,86,83,143,136,146,147,435,163])). % 59.67/59.68 cnf(1580,plain, % 59.67/59.68 (E(f20(x15801,f37(x15802,x15803,x15804,f5(a1,f20(f5(x15805,x15806),f5(x15805,x15806))))),f20(x15801,f37(x15802,x15803,x15804,f5(a1,a2))))), % 59.67/59.68 inference(scs_inference,[],[269,56,36])). % 59.67/59.68 cnf(1581,plain, % 59.67/59.68 (P1(f5(a1,f29(f5(f53(x15811,x15812),x15813),f5(f53(x15812,a1),f44(f53(x15812,a1),a8)))))), % 59.67/59.68 inference(scs_inference,[],[1578,188])). % 59.67/59.68 cnf(1582,plain, % 59.67/59.68 (P1(f5(a1,f3(f5(f53(x15821,a1),f44(f53(x15821,a1),a8)),f5(x15821,x15822))))), % 59.67/59.68 inference(rename_variables,[],[1578])). % 59.67/59.68 cnf(1584,plain, % 59.67/59.68 (P1(f5(a1,f31(f5(f53(x15841,x15842),x15843),f5(f53(x15842,a1),f44(f53(x15842,a1),a8)))))), % 59.67/59.68 inference(scs_inference,[],[1578,1582,188,189])). % 59.67/59.68 cnf(1585,plain, % 59.67/59.68 (P1(f5(a1,f3(f5(f53(x15851,a1),f44(f53(x15851,a1),a8)),f5(x15851,x15852))))), % 59.67/59.68 inference(rename_variables,[],[1578])). % 59.67/59.68 cnf(1587,plain, % 59.67/59.68 (P1(f5(a1,f23(f5(f53(x15871,x15872),x15873),f5(f53(x15872,a1),f3(f5(f53(a1,f53(x15872,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42))))))))), % 59.67/59.68 inference(scs_inference,[],[799,1578,1582,188,189,178])). % 59.67/59.68 cnf(1588,plain, % 59.67/59.68 (P1(f5(a1,f3(f5(f53(x15881,a1),f3(f5(f53(a1,f53(x15881,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42))))),f5(x15881,x15882))))), % 59.67/59.68 inference(rename_variables,[],[799])). % 59.67/59.68 cnf(1590,plain, % 59.67/59.68 (~P1(f5(a1,f7(f5(f53(x15901,x15902),x15903),f5(f53(x15902,a1),f3(f5(f53(a1,f53(x15902,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42))))))))), % 59.67/59.68 inference(scs_inference,[],[799,1588,1578,1582,188,189,178,179])). % 59.67/59.68 cnf(1593,plain, % 59.67/59.68 (~E(f5(a1,f23(f5(f53(x15931,x15932),x15933),f5(f53(x15932,a1),f3(f5(f53(a1,f53(x15932,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a43))))))),f5(a1,a4))), % 59.67/59.68 inference(scs_inference,[],[799,1588,1506,1578,1582,188,189,178,179,121])). % 59.67/59.68 cnf(1595,plain, % 59.67/59.68 (P1(f5(a1,f27(f5(f53(x15951,x15952),x15953),f5(f53(x15952,a1),f44(f53(x15952,a1),a8)))))), % 59.67/59.68 inference(scs_inference,[],[799,1588,1506,1578,1582,1585,188,189,178,179,121,194])). % 59.67/59.68 cnf(1596,plain, % 59.67/59.68 (P1(f5(a1,f3(f5(f53(x15961,a1),f44(f53(x15961,a1),a8)),f5(x15961,x15962))))), % 59.67/59.68 inference(rename_variables,[],[1578])). % 59.67/59.68 cnf(1605,plain, % 59.67/59.68 (E(f5(a1,a2),f5(a1,f3(f5(f53(x16051,a1),f44(f53(x16051,a1),a8)),f5(x16051,x16052))))), % 59.67/59.68 inference(scs_inference,[],[1541,1500,799,1588,1506,1578,1582,1585,1596,188,189,178,179,121,194,200,109,5,113,116])). % 59.67/59.68 cnf(1607,plain, % 59.67/59.68 (~E(f5(a1,a4),f5(a1,f9(f5(f53(x16071,a1),f3(f5(f53(a1,f53(x16071,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42))))))))), % 59.67/59.68 inference(scs_inference,[],[1541,1500,799,1588,808,1506,1578,1582,1585,1596,188,189,178,179,121,194,200,109,5,113,116,122])). % 59.67/59.68 cnf(1613,plain, % 59.67/59.68 (~P2(f27(f5(f53(x16131,x16132),x16133),f5(f53(x16132,a1),f3(f5(f53(a1,f53(x16132,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a43)))))),x16134,x16134)), % 59.67/59.68 inference(scs_inference,[],[1541,1500,799,1588,697,808,1506,1523,1578,1582,1585,1596,188,189,178,179,121,194,200,109,5,113,116,122,110,115,201])). % 59.67/59.68 cnf(1617,plain, % 59.67/59.68 (E(f5(a1,f23(f5(f53(x16171,x16172),x16173),f5(f53(x16172,a1),x16174))),f5(a1,f3(f5(f53(f53(x16172,a1),a1),f3(f5(f53(f53(x16171,x16172),f53(f53(x16172,a1),a1)),a14),f5(f53(x16171,x16172),x16173))),f5(f53(x16172,a1),x16174))))), % 59.67/59.68 inference(scs_inference,[],[1541,1500,799,1588,697,808,95,1506,1523,1578,1582,1585,1596,188,189,178,179,121,194,200,109,5,113,116,122,110,115,201,114,2])). % 59.67/59.68 cnf(1622,plain, % 59.67/59.68 (P2(x16221,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42)),f7(f5(f53(x16222,x16223),x16224),f5(f53(x16223,a1),f3(f5(f53(x16223,f53(x16223,a1)),a21),f5(x16223,f3(f5(f53(x16222,x16223),x16224),f5(x16222,x16225)))))))), % 59.67/59.68 inference(scs_inference,[],[91,269,1541,1500,799,1588,697,808,95,1503,1506,1523,1578,1582,1585,1596,188,189,178,179,121,194,200,109,5,113,116,122,110,115,201,114,2,137,131,128])). % 59.67/59.68 cnf(1626,plain, % 59.67/59.68 (P2(f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42)),x16261,f7(f5(f53(x16262,x16263),x16264),f5(f53(x16263,a1),f3(f5(f53(x16263,f53(x16263,a1)),a21),f5(x16263,f3(f5(f53(x16262,x16263),x16264),f5(x16262,x16265)))))))), % 59.67/59.68 inference(scs_inference,[],[91,269,1541,1500,799,1588,697,808,95,1503,1506,1523,1578,1582,1585,1596,188,189,178,179,121,194,200,109,5,113,116,122,110,115,201,114,2,137,131,128,133,130])). % 59.67/59.68 cnf(1636,plain, % 59.67/59.68 (P1(f5(a1,f3(f5(f53(f53(x16361,a1),a1),f3(f5(f53(f53(x16362,x16361),f53(f53(x16361,a1),a1)),a14),f5(f53(x16362,x16361),x16363))),f5(f53(x16361,a1),f3(f5(f53(x16361,f53(x16361,a1)),a21),f5(x16361,f3(f5(f53(x16362,x16361),x16363),f5(x16362,x16364))))))))), % 59.67/59.68 inference(scs_inference,[],[91,269,819,360,823,1556,1541,1500,799,1588,697,221,808,95,1543,1574,1503,1506,1523,1578,1582,1585,1596,188,189,178,179,121,194,200,109,5,113,116,122,110,115,201,114,2,137,131,128,133,130,3,84,85,86,83])). % 59.67/59.68 cnf(1639,plain, % 59.67/59.68 (~P2(f3(f5(f53(x16391,a1),f44(f53(x16391,a1),a8)),f5(x16391,x16392)),f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a43)),f3(f5(f53(x16391,a1),f44(f53(x16391,a1),a8)),f5(x16391,x16392)))), % 59.67/59.68 inference(scs_inference,[],[104,91,269,819,360,823,1556,1541,1500,799,1588,697,221,808,95,1543,1574,1503,1506,1523,1578,1582,1585,1596,188,189,178,179,121,194,200,109,5,113,116,122,110,115,201,114,2,137,131,128,133,130,3,84,85,86,83,143,147])). % 59.67/59.68 cnf(1643,plain, % 59.67/59.68 (E(f45(f48(f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42))),x16431,x16432,x16433),x16434),f45(f48(f5(a1,a2),x16431,x16432,x16433),x16434))), % 59.67/59.68 inference(scs_inference,[],[205,66,46])). % 59.67/59.68 cnf(1644,plain, % 59.67/59.68 (P1(f5(a1,f23(f5(f53(a1,f53(x16441,a1)),a35),f5(f53(f53(x16441,a1),a1),a8))))), % 59.67/59.68 inference(scs_inference,[],[1566,178])). % 59.67/59.68 cnf(1646,plain, % 59.67/59.68 (~P1(f5(a1,f7(f5(f53(a1,f53(x16461,a1)),a35),f5(f53(f53(x16461,a1),a1),a8))))), % 59.67/59.68 inference(scs_inference,[],[1566,178,179])). % 59.67/59.68 cnf(1648,plain, % 59.67/59.68 (P2(f9(f5(f53(x16481,a1),f44(f53(x16481,a1),a8))),x16482,x16482)), % 59.67/59.68 inference(scs_inference,[],[1576,1566,178,179,200])). % 59.67/59.68 cnf(1650,plain, % 59.67/59.68 (~E(f5(a1,f9(f5(f53(x16501,a1),f44(f53(x16501,a1),a8)))),f5(a1,a4))), % 59.67/59.68 inference(scs_inference,[],[1576,1566,178,179,200,121])). % 59.67/59.68 cnf(1657,plain, % 59.67/59.68 (~E(f5(a1,a4),f5(a1,f9(f5(f53(x16571,a1),f44(f53(x16571,a1),a8)))))), % 59.67/59.68 inference(scs_inference,[],[1593,1590,1576,1566,178,179,200,121,5,109,113,122])). % 59.67/59.68 cnf(1661,plain, % 59.67/59.68 (E(f5(a1,f9(f5(f53(x16611,a1),f44(f53(x16611,a1),a8)))),f5(a1,a2))), % 59.67/59.68 inference(scs_inference,[],[1593,1590,1576,1566,178,179,200,121,5,109,113,122,116,115])). % 59.67/59.68 cnf(1665,plain, % 59.67/59.68 (~P2(f7(f5(f53(x16651,x16652),x16653),f5(f53(x16652,a1),f3(f5(f53(a1,f53(x16652,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42)))))),x16654,x16654)), % 59.67/59.68 inference(scs_inference,[],[1593,1590,1576,1566,178,179,200,121,5,109,113,122,116,115,110,201])). % 59.67/59.68 cnf(1676,plain, % 59.67/59.68 (P2(x16761,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42)),f7(f5(f53(x16762,x16763),x16764),f5(f53(x16763,a1),f3(f5(f53(a1,f53(x16763,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42)))))))), % 59.67/59.68 inference(scs_inference,[],[91,205,1593,1605,1590,1576,1566,178,179,200,121,5,109,113,122,116,115,110,201,114,2,137,131,133,128])). % 59.67/59.68 cnf(1678,plain, % 59.67/59.68 (P2(f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42)),x16781,f7(f5(f53(x16782,x16783),x16784),f5(f53(x16783,a1),f3(f5(f53(a1,f53(x16783,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42)))))))), % 59.67/59.68 inference(scs_inference,[],[91,205,1593,1605,1590,1576,1566,178,179,200,121,5,109,113,122,116,115,110,201,114,2,137,131,133,128,130])). % 59.67/59.68 cnf(1683,plain, % 59.67/59.68 (~E(f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42)),f7(f5(f53(x16831,x16832),x16833),f5(f53(x16832,a1),f3(f5(f53(x16832,f53(x16832,a1)),a21),f5(x16832,f3(f5(f53(x16831,x16832),x16833),f5(x16831,x16834)))))))), % 59.67/59.68 inference(scs_inference,[],[91,205,360,1622,1593,1605,1590,1576,1566,1613,178,179,200,121,5,109,113,122,116,115,110,201,114,2,137,131,133,128,130,3,84,85])). % 59.67/59.68 cnf(1684,plain, % 59.67/59.68 (P2(x16841,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42)),f7(f5(f53(x16842,x16843),x16844),f5(f53(x16843,a1),f3(f5(f53(x16843,f53(x16843,a1)),a21),f5(x16843,f3(f5(f53(x16842,x16843),x16844),f5(x16842,x16845)))))))), % 59.67/59.68 inference(rename_variables,[],[1622])). % 59.67/59.68 cnf(1685,plain, % 59.67/59.68 (~P2(f27(f5(f53(x16851,x16852),x16853),f5(f53(x16852,a1),f3(f5(f53(a1,f53(x16852,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a43)))))),x16854,x16854)), % 59.67/59.68 inference(rename_variables,[],[1613])). % 59.67/59.68 cnf(1686,plain, % 59.67/59.68 (~E(f7(f5(f53(x16861,x16862),x16863),f5(f53(x16862,a1),f3(f5(f53(x16862,f53(x16862,a1)),a21),f5(x16862,f3(f5(f53(x16861,x16862),x16863),f5(x16861,x16864)))))),f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42)))), % 59.67/59.68 inference(scs_inference,[],[91,205,360,1622,1684,1593,1605,1590,1576,1566,1613,1685,178,179,200,121,5,109,113,122,116,115,110,201,114,2,137,131,133,128,130,3,84,85,86])). % 59.67/59.68 cnf(1689,plain, % 59.67/59.68 (P1(f5(a1,f3(f5(f53(f53(x16891,a1),a1),f3(f5(f53(f53(x16892,x16891),f53(f53(x16891,a1),a1)),a14),f5(f53(x16892,x16891),x16893))),f5(f53(x16891,a1),f3(f5(f53(a1,f53(x16891,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42))))))))), % 59.67/59.68 inference(scs_inference,[],[91,205,360,1622,1684,1593,1605,1590,1576,1566,1613,1685,1587,1617,178,179,200,121,5,109,113,122,116,115,110,201,114,2,137,131,133,128,130,3,84,85,86,83])). % 59.67/59.68 cnf(1699,plain, % 59.67/59.68 (~P2(f9(f5(f53(x16991,a1),f44(f53(x16991,a1),a8))),f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a43)),f9(f5(f53(x16991,a1),f44(f53(x16991,a1),a8))))), % 59.67/59.68 inference(scs_inference,[],[104,91,205,360,1622,1684,1593,1605,1590,221,1576,1566,1613,1685,1587,1617,178,179,200,121,5,109,113,122,116,115,110,201,114,2,137,131,133,128,130,3,84,85,86,83,143,139,136,146,147])). % 59.67/59.68 cnf(1701,plain, % 59.67/59.68 (E(f45(x17011,f48(x17012,f5(a1,f20(f5(x17013,x17014),f5(x17013,x17014))),x17015,x17016)),f45(x17011,f48(x17012,f5(a1,a2),x17015,x17016)))), % 59.67/59.68 inference(scs_inference,[],[269,67,47])). % 59.67/59.68 cnf(1702,plain, % 59.67/59.68 (P1(f5(a1,f23(f5(f53(x17021,f53(x17021,a1)),a21),f5(f53(f53(x17021,a1),a1),f3(f5(f53(f53(x17022,x17021),f53(f53(x17021,a1),a1)),a14),f5(f53(x17022,x17021),x17023))))))), % 59.67/59.68 inference(scs_inference,[],[1636,178])). % 59.67/59.68 cnf(1706,plain, % 59.67/59.68 (~P1(f5(a1,f7(f5(f53(x17061,f53(x17061,a1)),a21),f5(f53(f53(x17061,a1),a1),f3(f5(f53(f53(x17062,x17061),f53(f53(x17061,a1),a1)),a14),f5(f53(x17062,x17061),x17063))))))), % 59.67/59.68 inference(scs_inference,[],[1509,1636,178,200,179])). % 59.67/59.68 cnf(1708,plain, % 59.67/59.68 (~E(f5(a1,f25(f5(f53(x17081,x17082),x17083),f5(f53(x17082,a1),f3(f5(f53(a1,f53(x17082,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a43))))))),f5(a1,a4))), % 59.67/59.68 inference(scs_inference,[],[1509,1636,178,200,179,121])). % 59.67/59.68 cnf(1717,plain, % 59.67/59.68 (E(f5(a1,a2),f5(a1,f29(f5(f53(x17171,x17172),x17173),f5(f53(x17172,a1),f44(f53(x17172,a1),a8)))))), % 59.67/59.68 inference(scs_inference,[],[1607,1646,1509,1686,1636,1581,178,200,179,121,20,109,113,5,116])). % 59.67/59.68 cnf(1723,plain, % 59.67/59.68 (~P2(f7(f5(f53(a1,f53(x17231,a1)),a35),f5(f53(f53(x17231,a1),a1),a8)),x17232,x17232)), % 59.67/59.68 inference(scs_inference,[],[1607,1646,1509,1686,1636,1581,178,200,179,121,20,109,113,5,116,122,115,201])). % 59.67/59.68 cnf(1725,plain, % 59.67/59.68 (E(f5(a1,f25(f5(f53(x17251,x17252),x17253),f5(f53(x17252,a1),x17254))),f5(a1,f3(f5(f53(f53(x17252,a1),a1),f3(f5(f53(f53(x17251,x17252),f53(f53(x17252,a1),a1)),a24),f5(f53(x17251,x17252),x17253))),f5(f53(x17252,a1),x17254))))), % 59.67/59.68 inference(scs_inference,[],[1607,1646,96,1509,1686,1636,1581,178,200,179,121,20,109,113,5,116,122,115,201,2])). % 59.67/59.68 cnf(1740,plain, % 59.67/59.68 (P2(f9(f5(f53(x17401,a1),f44(f53(x17401,a1),a8))),x17402,x17402)), % 59.67/59.68 inference(rename_variables,[],[1648])). % 59.67/59.68 cnf(1743,plain, % 59.67/59.68 (P1(f5(a1,f3(f5(f53(f53(f53(x17431,a1),a1),a1),f3(f5(f53(f53(a1,f53(x17431,a1)),f53(f53(f53(x17431,a1),a1),a1)),a14),f5(f53(a1,f53(x17431,a1)),a35))),f5(f53(f53(x17431,a1),a1),a8))))), % 59.67/59.68 inference(scs_inference,[],[91,269,1661,360,1648,1740,1607,1646,221,96,1576,1509,1665,1699,1686,1636,1581,1644,1617,178,200,179,121,20,109,113,5,116,122,115,201,2,137,131,128,130,133,3,84,85,86,83])). % 59.67/59.68 cnf(1753,plain, % 59.67/59.68 (E(f11(f48(x17531,x17532,f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42))),x17533),x17534),f11(f48(x17531,x17532,f5(a1,a2),x17533),x17534))), % 59.67/59.68 inference(scs_inference,[],[205,72,48])). % 59.67/59.68 cnf(1754,plain, % 59.67/59.68 (~P1(f5(a1,f7(f5(f53(a1,f53(x17541,a1)),a35),f5(f53(f53(x17541,a1),a1),f3(f5(f53(f53(x17542,x17541),f53(f53(x17541,a1),a1)),a14),f5(f53(x17542,x17541),x17543))))))), % 59.67/59.68 inference(scs_inference,[],[1689,179])). % 59.67/59.68 cnf(1756,plain, % 59.67/59.68 (P1(f5(a1,f23(f5(f53(a1,f53(x17561,a1)),a35),f5(f53(f53(x17561,a1),a1),f3(f5(f53(f53(x17562,x17561),f53(f53(x17561,a1),a1)),a14),f5(f53(x17562,x17561),x17563))))))), % 59.67/59.68 inference(scs_inference,[],[1689,179,178])). % 59.67/59.68 cnf(1758,plain, % 59.67/59.68 (~E(f5(a1,f31(f5(f53(x17581,x17582),x17583),f5(f53(x17582,a1),f3(f5(f53(a1,f53(x17582,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42))))))),f5(a1,a4))), % 59.67/59.68 inference(scs_inference,[],[1515,1689,179,178,121])). % 59.67/59.68 cnf(1768,plain, % 59.67/59.68 (E(f5(a1,a2),f5(a1,f31(f5(f53(x17681,x17682),x17683),f5(f53(x17682,a1),f44(f53(x17682,a1),a8)))))), % 59.67/59.68 inference(scs_inference,[],[1706,1515,1683,1689,1584,179,178,121,200,109,113,20,116])). % 59.67/59.68 cnf(1771,plain, % 59.67/59.68 (~E(f5(a1,a4),f5(a1,f31(f5(f53(x17711,x17712),x17713),f5(f53(x17712,a1),f44(f53(x17712,a1),a8)))))), % 59.67/59.68 inference(scs_inference,[],[1708,1706,1515,1683,1689,1584,179,178,121,200,109,113,20,116,5,122])). % 59.67/59.68 cnf(1773,plain, % 59.67/59.68 (~P2(f7(f5(f53(x17731,f53(x17731,a1)),a21),f5(f53(f53(x17731,a1),a1),f3(f5(f53(f53(x17732,x17731),f53(f53(x17731,a1),a1)),a14),f5(f53(x17732,x17731),x17733)))),x17734,x17734)), % 59.67/59.68 inference(scs_inference,[],[1708,1706,1515,1683,1689,1584,179,178,121,200,109,113,20,116,5,122,201])). % 59.67/59.68 cnf(1784,plain, % 59.67/59.68 (P2(x17841,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42)),f7(f5(f53(x17842,f53(x17842,a1)),a21),f5(f53(f53(x17842,a1),a1),f3(f5(f53(f53(x17843,x17842),f53(f53(x17842,a1),a1)),a14),f5(f53(x17843,x17842),x17844)))))), % 59.67/59.68 inference(scs_inference,[],[91,269,1708,1717,1706,1515,1683,1689,1584,179,178,121,200,109,113,20,116,5,122,201,115,2,137,131,133,128])). % 59.67/59.68 cnf(1786,plain, % 59.67/59.68 (P2(f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42)),x17861,f7(f5(f53(x17862,f53(x17862,a1)),a21),f5(f53(f53(x17862,a1),a1),f3(f5(f53(f53(x17863,x17862),f53(f53(x17862,a1),a1)),a14),f5(f53(x17863,x17862),x17864)))))), % 59.67/59.68 inference(scs_inference,[],[91,269,1708,1717,1706,1515,1683,1689,1584,179,178,121,200,109,113,20,116,5,122,201,115,2,137,131,133,128,130])). % 59.67/59.68 cnf(1791,plain, % 59.67/59.68 (~E(f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42)),f7(f5(f53(x17911,x17912),x17913),f5(f53(x17912,a1),f3(f5(f53(a1,f53(x17912,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42)))))))), % 59.67/59.68 inference(scs_inference,[],[91,269,360,1676,1708,1717,1706,1605,1515,1723,1683,1689,1584,179,178,121,200,109,113,20,116,5,122,201,115,2,137,131,133,128,130,3,84,85])). % 59.67/59.68 cnf(1796,plain, % 59.67/59.68 (P1(f5(a1,f3(f5(f53(f53(x17961,a1),a1),f3(f5(f53(f53(x17962,x17961),f53(f53(x17961,a1),a1)),a24),f5(f53(x17962,x17961),x17963))),f5(f53(x17961,a1),f3(f5(f53(a1,f53(x17961,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a43))))))))), % 59.67/59.68 inference(scs_inference,[],[91,269,360,1626,1676,1708,1717,1706,1605,1515,1509,1723,1683,1725,1689,1584,252,179,178,121,200,109,113,20,116,5,122,201,115,2,137,131,133,128,130,3,84,85,86,83])). % 59.67/59.68 cnf(1804,plain, % 59.67/59.68 (~P2(f31(f5(f53(x18041,x18042),x18043),f5(f53(x18042,a1),f44(f53(x18042,a1),a8))),f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a43)),f31(f5(f53(x18041,x18042),x18043),f5(f53(x18042,a1),f44(f53(x18042,a1),a8))))), % 59.67/59.68 inference(scs_inference,[],[104,91,269,360,1626,1676,1708,1717,1706,1605,221,1515,1509,1723,1683,1725,1689,1584,252,179,178,121,200,109,113,20,116,5,122,201,115,2,137,131,133,128,130,3,84,85,86,83,143,136,146,147])). % 59.67/59.68 cnf(1806,plain, % 59.67/59.68 (E(f11(x18061,f48(x18062,x18063,x18064,f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42))))),f11(x18061,f48(x18062,x18063,x18064,f5(a1,a2))))), % 59.67/59.68 inference(scs_inference,[],[205,73,49])). % 59.67/59.68 cnf(1807,plain, % 59.67/59.68 (~E(f5(a1,f3(f5(f53(f53(x18071,a1),a1),a8),f5(f53(x18071,a1),f3(f5(f53(a1,f53(x18071,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42))))))),f5(a1,a4))), % 59.67/59.68 inference(scs_inference,[],[1566,121])). % 59.67/59.68 cnf(1809,plain, % 59.67/59.68 (~P1(f5(a1,f7(f5(f53(a1,f53(x18091,a1)),a35),f5(f53(f53(x18091,a1),a1),f3(f5(f53(f53(x18092,x18091),f53(f53(x18091,a1),a1)),a24),f5(f53(x18092,x18091),x18093))))))), % 59.67/59.68 inference(scs_inference,[],[1566,1796,121,179])). % 59.67/59.68 cnf(1813,plain, % 59.67/59.68 (P1(f5(a1,f23(f5(f53(a1,f53(x18131,a1)),a35),f5(f53(f53(x18131,a1),a1),f3(f5(f53(f53(x18132,x18131),f53(f53(x18131,a1),a1)),a24),f5(f53(x18132,x18131),x18133))))))), % 59.67/59.68 inference(scs_inference,[],[1566,1796,121,179,200,178])). % 59.67/59.68 cnf(1821,plain, % 59.67/59.68 (E(f5(a1,a2),f5(a1,f27(f5(f53(x18211,x18212),x18213),f5(f53(x18212,a1),f44(f53(x18212,a1),a8)))))), % 59.67/59.68 inference(scs_inference,[],[1754,1566,1791,1796,1595,121,179,200,178,113,109,20,116])). % 59.67/59.68 cnf(1828,plain, % 59.67/59.68 (~P2(f7(f5(f53(a1,f53(x18281,a1)),a35),f5(f53(f53(x18281,a1),a1),f3(f5(f53(f53(x18282,x18281),f53(f53(x18281,a1),a1)),a14),f5(f53(x18282,x18281),x18283)))),x18284,x18284)), % 59.67/59.68 inference(scs_inference,[],[1758,1754,1566,1791,1796,1595,121,179,200,178,113,109,20,116,5,122,115,201])). % 59.67/59.68 cnf(1839,plain, % 59.67/59.68 (P2(x18391,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42)),f7(f5(f53(a1,f53(x18392,a1)),a35),f5(f53(f53(x18392,a1),a1),f3(f5(f53(f53(x18393,x18392),f53(f53(x18392,a1),a1)),a14),f5(f53(x18393,x18392),x18394)))))), % 59.67/59.68 inference(scs_inference,[],[91,205,1758,1768,1754,1566,1791,1796,1595,121,179,200,178,113,109,20,116,5,122,115,201,2,137,131,130,133,128])). % 59.67/59.68 cnf(1841,plain, % 59.67/59.68 (~E(f5(a1,a4),f5(a1,f3(f5(f53(f53(x18411,a1),a1),a8),f5(f53(x18411,a1),f44(f53(x18411,a1),a8)))))), % 59.67/59.68 inference(scs_inference,[],[91,205,1758,1768,1657,1754,92,1566,1791,1796,1595,121,179,200,178,113,109,20,116,5,122,115,201,2,137,131,130,133,128,3])). % 59.67/59.68 cnf(1848,plain, % 59.67/59.68 (~E(f7(f5(f53(x18481,x18482),x18483),f5(f53(x18482,a1),f3(f5(f53(a1,f53(x18482,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42)))))),f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42)))), % 59.67/59.68 inference(scs_inference,[],[91,205,360,1678,1784,1758,1768,1657,1754,92,1566,1773,1791,1796,1595,254,121,179,200,178,113,109,20,116,5,122,115,201,2,137,131,130,133,128,3,84,85,86])). % 59.67/59.68 cnf(1859,plain, % 59.67/59.68 (P1(f5(a1,f15(f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a43))))))), % 59.67/59.68 inference(scs_inference,[],[221,138,115])). % 59.67/59.68 cnf(1860,plain, % 59.67/59.68 (~E(f5(a1,f3(f5(f53(x18601,a1),f44(f53(x18601,a1),a8)),f5(x18601,x18602))),f5(a1,a4))), % 59.67/59.68 inference(scs_inference,[],[1578,121])). % 59.67/59.68 cnf(1862,plain, % 59.67/59.68 (P1(f5(a1,f23(f5(f53(x18621,x18622),x18623),f5(f53(x18622,a1),f44(f53(x18622,a1),a8)))))), % 59.67/59.68 inference(scs_inference,[],[1578,121,178])). % 59.67/59.68 cnf(1863,plain, % 59.67/59.68 (P1(f5(a1,f3(f5(f53(x18631,a1),f44(f53(x18631,a1),a8)),f5(x18631,x18632))))), % 59.67/59.68 inference(rename_variables,[],[1578])). % 59.67/59.69 cnf(1865,plain, % 59.67/59.69 (~P1(f5(a1,f7(f5(f53(x18651,x18652),x18653),f5(f53(x18652,a1),f44(f53(x18652,a1),a8)))))), % 59.67/59.69 inference(scs_inference,[],[1578,1863,121,178,179])). % 59.67/59.69 cnf(1866,plain, % 59.67/59.69 (P1(f5(a1,f3(f5(f53(x18661,a1),f44(f53(x18661,a1),a8)),f5(x18661,x18662))))), % 59.67/59.69 inference(rename_variables,[],[1578])). % 59.67/59.69 cnf(1868,plain, % 59.67/59.69 (P2(f3(f5(f53(x18681,a1),f44(f53(x18681,a1),a8)),f5(x18681,x18682)),x18683,x18683)), % 59.67/59.69 inference(scs_inference,[],[1578,1863,1866,121,178,179,200])). % 59.67/59.69 cnf(1878,plain, % 59.67/59.69 (~E(f5(f53(a34,a1),f3(f5(f53(a1,f53(a34,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42))))),f5(f53(a34,a1),a42))), % 59.67/59.69 inference(scs_inference,[],[1809,1578,1863,1866,1644,1848,121,178,179,200,113,109,116,110,20])). % 59.67/59.69 cnf(1885,plain, % 59.67/59.69 (E(f5(a1,f23(f5(f53(a1,f53(x18851,a1)),a35),f5(f53(f53(x18851,a1),a1),a8))),f5(a1,a2))), % 59.67/59.69 inference(scs_inference,[],[1657,1809,1578,1863,1866,1644,1848,121,178,179,200,113,109,116,110,20,122,5,114,115])). % 59.67/59.69 cnf(1887,plain, % 59.67/59.69 (~P2(f7(f5(f53(a1,f53(x18871,a1)),a35),f5(f53(f53(x18871,a1),a1),f3(f5(f53(f53(x18872,x18871),f53(f53(x18871,a1),a1)),a24),f5(f53(x18872,x18871),x18873)))),x18874,x18874)), % 59.67/59.69 inference(scs_inference,[],[1657,1809,1578,1863,1866,1644,1848,121,178,179,200,113,109,116,110,20,122,5,114,115,201])). % 59.67/59.69 cnf(1909,plain, % 59.67/59.69 (~P2(f7(f5(f53(x19091,x19092),x19093),f5(f53(x19092,a1),f44(f53(x19092,a1),a8))),f7(f5(f53(x19091,x19092),x19093),f5(f53(x19092,a1),f44(f53(x19092,a1),a8))),f7(f5(f53(x19091,x19092),x19093),f5(f53(x19092,a1),f44(f53(x19092,a1),a8))))), % 59.67/59.69 inference(scs_inference,[],[91,269,360,1657,1590,1786,1839,1821,1809,461,1578,1863,1866,1644,1828,1848,1841,252,121,178,179,200,113,109,116,110,20,122,5,114,115,201,2,137,131,130,133,128,3,84,85,86,139])). % 59.67/59.69 cnf(1915,plain, % 59.67/59.69 (~P2(f23(f5(f53(a1,f53(x19151,a1)),a35),f5(f53(f53(x19151,a1),a1),a8)),f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a43)),f23(f5(f53(a1,f53(x19151,a1)),a35),f5(f53(f53(x19151,a1),a1),a8)))), % 59.67/59.69 inference(scs_inference,[],[104,91,269,360,1657,1590,1786,1839,1821,1809,221,461,1578,1863,1866,1644,1828,1848,1841,252,121,178,179,200,113,109,116,110,20,122,5,114,115,201,2,137,131,130,133,128,3,84,85,86,139,143,136,147])). % 59.67/59.69 cnf(1920,plain, % 59.67/59.69 (P1(f5(a1,f19(f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a43))),f5(a1,x19201))))), % 59.67/59.69 inference(scs_inference,[],[1859,149,150])). % 59.67/59.69 cnf(1921,plain, % 59.67/59.69 (~E(f5(a1,f31(f5(f53(x19211,x19212),x19213),f5(f53(x19212,a1),f44(f53(x19212,a1),a8)))),f5(a1,a4))), % 59.67/59.69 inference(scs_inference,[],[1584,121])). % 59.67/59.69 cnf(1923,plain, % 59.67/59.69 (P2(f31(f5(f53(x19231,x19232),x19233),f5(f53(x19232,a1),f44(f53(x19232,a1),a8))),x19234,x19234)), % 59.67/59.69 inference(scs_inference,[],[1584,121,200])). % 59.67/59.69 cnf(1929,plain, % 59.67/59.69 (E(f5(a1,a2),f5(a1,f15(f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a43))))))), % 59.67/59.69 inference(scs_inference,[],[1865,1584,1859,121,200,109,113,116])). % 59.67/59.69 cnf(1934,plain, % 59.67/59.69 (~P2(f7(f5(f53(x19341,x19342),x19343),f5(f53(x19342,a1),f44(f53(x19342,a1),a8))),x19344,x19344)), % 59.67/59.69 inference(scs_inference,[],[1860,1865,1584,1644,1859,121,200,109,113,116,122,5,201])). % 59.67/59.69 cnf(1943,plain, % 59.67/59.69 (P2(f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42)),x19431,f7(f5(f53(x19432,x19433),x19434),f5(f53(x19433,a1),f44(f53(x19433,a1),a8))))), % 59.67/59.69 inference(scs_inference,[],[91,205,1646,1860,1865,99,1578,1584,1644,1743,1859,121,200,109,113,116,122,5,201,115,2,137,131,130])). % 59.67/59.69 cnf(1953,plain, % 59.67/59.69 (P2(f3(f5(f53(x19531,a1),f44(f53(x19531,a1),a8)),f5(x19531,x19532)),x19533,x19533)), % 59.67/59.69 inference(rename_variables,[],[1868])). % 59.67/59.69 cnf(1956,plain, % 59.67/59.69 (P1(f5(a1,f3(f5(f53(f53(x19561,a1),a1),f3(f5(f53(f53(x19562,x19561),f53(f53(x19561,a1),a1)),a30),f5(f53(x19562,x19561),x19563))),f5(f53(x19561,a1),f44(f53(x19561,a1),a8)))))), % 59.67/59.69 inference(scs_inference,[],[91,205,1885,360,1646,1868,1953,1860,1865,221,99,1578,1584,1644,1743,1859,1909,1639,121,200,109,113,116,122,5,201,115,2,137,131,130,133,128,3,84,85,86,83])). % 59.67/59.69 cnf(1963,plain, % 59.67/59.69 (E(f39(f39(x19631,f5(a1,f20(f5(x19632,x19633),f5(x19632,x19633))),x19634,x19635),x19636,x19637,x19638),f39(f39(x19631,f5(a1,a2),x19634,x19635),x19636,x19637,x19638))), % 59.67/59.69 inference(scs_inference,[],[269,50,51])). % 59.67/59.69 cnf(1972,plain, % 59.67/59.69 (E(f5(a1,a2),f5(a1,f23(f5(f53(x19721,x19722),x19723),f5(f53(x19722,a1),f44(f53(x19722,a1),a8)))))), % 59.67/59.69 inference(scs_inference,[],[773,1581,1862,121,200,113,109,116])). % 59.67/59.69 cnf(1974,plain, % 59.67/59.69 (~E(f5(a1,a4),f5(a1,f15(f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a43))))))), % 59.67/59.69 inference(scs_inference,[],[773,1581,1859,1862,121,200,113,109,116,122])). % 59.67/59.69 cnf(1988,plain, % 59.67/59.69 (P2(x19881,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42)),f3(f5(f53(f53(f53(x19882,a1),a1),a1),f3(f5(f53(f53(a1,f53(x19882,a1)),f53(f53(f53(x19882,a1),a1),a1)),a26),f5(f53(a1,f53(x19882,a1)),a35))),f5(f53(f53(x19882,a1),a1),a10)))), % 59.67/59.69 inference(scs_inference,[],[91,205,1706,1929,1921,773,1584,1581,1636,1859,1862,121,200,113,109,116,122,115,5,2,137,131,130,133,128])). % 59.67/59.69 cnf(1995,plain, % 59.67/59.69 (P2(f31(f5(f53(x19951,x19952),x19953),f5(f53(x19952,a1),f44(f53(x19952,a1),a8))),x19954,x19954)), % 59.67/59.69 inference(rename_variables,[],[1923])). % 59.67/59.69 cnf(2004,plain, % 59.67/59.69 (~E(f5(f53(a34,a1),a42),f5(f53(a34,a1),f44(f53(a34,a1),a8)))), % 59.67/59.69 inference(scs_inference,[],[104,91,205,213,1706,1923,1995,1929,1921,1771,773,221,99,1584,1581,1636,1859,1934,1804,1862,121,200,113,109,116,122,115,5,2,137,131,130,133,128,3,84,85,86,143,146,147,20])). % 59.67/59.69 cnf(2007,plain, % 59.67/59.69 (E(f39(x20071,x20072,f39(x20073,x20074,x20075,f5(a1,f20(f5(x20076,x20077),f5(x20076,x20077)))),x20078),f39(x20071,x20072,f39(x20073,x20074,x20075,f5(a1,a2)),x20078))), % 59.67/59.69 inference(scs_inference,[],[269,52,53])). % 59.67/59.69 cnf(2008,plain, % 59.67/59.69 (~E(f5(a1,f27(f5(f53(x20081,x20082),x20083),f5(f53(x20082,a1),f44(f53(x20082,a1),a8)))),f5(a1,a4))), % 59.67/59.69 inference(scs_inference,[],[1595,121])). % 59.67/59.69 cnf(2028,plain, % 59.67/59.69 (P2(f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42)),x20281,f27(f5(f53(x20282,x20283),x20284),f5(f53(x20283,a1),f3(f5(f53(a1,f53(x20283,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a43)))))))), % 59.67/59.69 inference(scs_inference,[],[91,269,1865,1974,1972,1584,1595,1523,1689,1956,1920,121,200,109,113,122,116,115,5,2,137,131,130])). % 59.67/59.69 cnf(2030,plain, % 59.67/59.69 (P2(x20301,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42)),f27(f5(f53(x20302,x20303),x20304),f5(f53(x20303,a1),f3(f5(f53(a1,f53(x20303,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a43)))))))), % 59.67/59.69 inference(scs_inference,[],[91,269,1865,1974,1972,1584,1595,1523,1689,1956,1920,121,200,109,113,122,116,115,5,2,137,131,130,128])). % 59.67/59.69 cnf(2050,plain, % 59.67/59.69 (~E(f5(a1,f3(f5(f53(f53(x20501,a1),a1),f3(f5(f53(f53(x20502,x20501),f53(f53(x20501,a1),a1)),a24),f5(f53(x20502,x20501),x20503))),f5(f53(x20501,a1),f3(f5(f53(a1,f53(x20501,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a43))))))),f5(a1,a4))), % 59.67/59.69 inference(scs_inference,[],[1796,121])). % 59.67/59.69 cnf(2056,plain, % 59.67/59.69 (~E(f5(a1,a4),f5(a1,f23(f5(f53(x20561,x20562),x20563),f5(f53(x20562,a1),f44(f53(x20562,a1),a8)))))), % 59.67/59.69 inference(scs_inference,[],[1796,1920,1862,121,200,116,122])). % 59.67/59.69 cnf(2085,plain, % 59.67/59.69 (~E(f5(a1,f3(f5(f53(f53(x20851,a1),a1),f3(f5(f53(f53(x20852,x20851),f53(f53(x20851,a1),a1)),a14),f5(f53(x20852,x20851),x20853))),f5(f53(x20851,a1),f3(f5(f53(x20851,f53(x20851,a1)),a21),f5(x20851,f3(f5(f53(x20852,x20851),x20853),f5(x20852,x20854))))))),f5(a1,a4))), % 59.67/59.69 inference(scs_inference,[],[1636,121])). % 59.67/59.69 cnf(2089,plain, % 59.67/59.69 (E(f5(a1,f19(f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a43))),f5(a1,x20891))),f5(a1,a2))), % 59.67/59.69 inference(scs_inference,[],[1636,1920,121,200,115])). % 59.67/59.69 cnf(2093,plain, % 59.67/59.69 (~P2(f7(f5(f53(a1,f53(x20931,a1)),a35),f5(f53(f53(x20931,a1),a1),f3(f5(f53(f53(x20932,x20931),f53(f53(x20931,a1),a1)),a24),f5(f53(x20932,x20931),x20933)))),f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42)),a2)), % 59.67/59.69 inference(scs_inference,[],[205,1809,2050,98,1636,1920,121,200,115,5,2,137])). % 59.67/59.69 cnf(2108,plain, % 59.67/59.69 (P1(f5(a1,f3(f5(f53(f53(f53(x21081,a1),a1),a1),f3(f5(f53(f53(a1,f53(x21081,a1)),f53(f53(f53(x21081,a1),a1),a1)),a28),f5(f53(a1,f53(x21081,a1)),a35))),f5(f53(f53(x21081,a1),a1),a10))))), % 59.67/59.69 inference(scs_inference,[],[205,263,1809,2028,2030,2050,2056,723,95,98,1636,1920,1702,1934,254,121,200,115,5,2,137,131,133,3,84,85,86,83])). % 59.67/59.69 cnf(2132,plain, % 59.67/59.69 (~P2(f7(f5(f53(a1,f53(x21321,a1)),a35),f5(f53(f53(x21321,a1),a1),f3(f5(f53(f53(x21322,x21321),f53(f53(x21321,a1),a1)),a24),f5(f53(x21322,x21321),x21323)))),x21324,x21324)), % 59.67/59.69 inference(rename_variables,[],[1887])). % 59.67/59.69 cnf(2138,plain, % 59.67/59.69 (P1(f5(a1,f3(f5(f53(f53(x21381,a1),a1),f3(f5(f53(f53(x21382,x21381),f53(f53(x21381,a1),a1)),a26),f5(f53(x21382,x21381),x21383))),f5(f53(x21381,a1),f44(f53(x21381,a1),a8)))))), % 59.67/59.69 inference(scs_inference,[],[269,2089,229,1754,1943,1988,2085,221,1566,1689,97,1595,1512,1756,1887,2132,256,121,200,115,5,2,137,131,133,3,84,85,86,83])). % 59.67/59.69 cnf(2148,plain, % 59.67/59.69 (E(f52(x21481,x21482,x21483,f38(x21484,x21485,x21486,f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42))),x21487)),f52(x21481,x21482,x21483,f38(x21484,x21485,x21486,f5(a1,a2),x21487)))), % 59.67/59.69 inference(scs_inference,[],[205,65,60])). % 59.67/59.69 cnf(2151,plain, % 59.67/59.69 (P2(f23(f5(f53(a1,f53(x21511,a1)),a35),f5(f53(f53(x21511,a1),a1),a8)),x21512,x21512)), % 59.67/59.69 inference(scs_inference,[],[1644,121,200])). % 59.67/59.69 cnf(2175,plain, % 59.67/59.69 (E(f49(f38(x21751,x21752,x21753,x21754,f5(a1,f20(f5(x21755,x21756),f5(x21755,x21756)))),x21757,x21758,x21759),f49(f38(x21751,x21752,x21753,x21754,f5(a1,a2)),x21757,x21758,x21759))), % 59.67/59.69 inference(scs_inference,[],[269,68,61])). % 59.67/59.69 cnf(2176,plain, % 59.67/59.69 (~E(f5(a1,f3(f5(f53(f53(x21761,a1),a1),f3(f5(f53(f53(x21762,x21761),f53(f53(x21761,a1),a1)),a30),f5(f53(x21762,x21761),x21763))),f5(f53(x21761,a1),f44(f53(x21761,a1),a8)))),f5(a1,a4))), % 59.67/59.69 inference(scs_inference,[],[1956,121])). % 59.67/59.69 cnf(2197,plain, % 59.67/59.69 (P2(f23(f5(f53(a1,f53(x21971,a1)),a35),f5(f53(f53(x21971,a1),a1),a8)),x21972,x21972)), % 59.67/59.69 inference(rename_variables,[],[2151])). % 59.67/59.69 cnf(2200,plain, % 59.67/59.69 (P1(f5(a1,f3(f5(f53(f53(a34,a1),a1),f3(f5(f53(f53(a33,a34),f53(f53(a34,a1),a1)),a32),f5(f53(a33,a34),a41))),f5(f53(a34,a1),a42))))), % 59.67/59.69 inference(scs_inference,[],[91,269,263,356,1646,1809,2151,2197,2008,94,1581,1956,2108,101,1915,1813,1613,121,200,115,5,2,125,137,131,133,3,84,85,86,83])). % 59.67/59.69 cnf(2211,plain, % 59.67/59.69 (E(f49(x22111,f49(x22112,x22113,f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42))),x22114),x22115,x22116),f49(x22111,f49(x22112,x22113,f5(a1,a2),x22114),x22115,x22116))), % 59.67/59.69 inference(scs_inference,[],[205,69,70])). % 59.67/59.69 cnf(2212,plain, % 59.67/59.69 (~E(f5(a1,f19(f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a43))),f5(a1,x22121))),f5(a1,a4))), % 59.67/59.69 inference(scs_inference,[],[1920,121])). % 59.67/59.69 cnf(2236,plain, % 59.67/59.69 (E(f49(x22361,x22362,x22363,f46(f5(a1,f20(f5(x22364,x22365),f5(x22364,x22365))),x22366,x22367,x22368)),f49(x22361,x22362,x22363,f46(f5(a1,a2),x22366,x22367,x22368)))), % 59.67/59.69 inference(scs_inference,[],[269,71,74])). % 59.67/59.69 cnf(2262,plain, % 59.67/59.69 (E(f46(x22621,f46(x22622,x22623,f5(a1,f20(f5(x22624,x22625),f5(x22624,x22625))),x22626),x22627,x22628),f46(x22621,f46(x22622,x22623,f5(a1,a2),x22626),x22627,x22628))), % 59.67/59.69 inference(scs_inference,[],[269,75,76])). % 59.67/59.69 cnf(2263,plain, % 59.67/59.69 (~E(f5(a1,f15(f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a43))))),f5(a1,a4))), % 59.67/59.69 inference(scs_inference,[],[1859,121])). % 59.67/59.69 cnf(2289,plain, % 59.67/59.69 (E(f46(x22891,x22892,x22893,f40(f5(a1,f20(f5(x22894,x22895),f5(x22894,x22895))),x22896,x22897,x22898,x22899)),f46(x22891,x22892,x22893,f40(f5(a1,a2),x22896,x22897,x22898,x22899)))), % 59.67/59.69 inference(scs_inference,[],[269,77,78])). % 59.67/59.69 cnf(2297,plain, % 59.67/59.69 (E(f49(f38(x22971,x22972,x22973,x22974,f5(a1,a2)),x22975,x22976,x22977),f49(f38(x22971,x22972,x22973,x22974,f5(a1,f20(f5(x22978,x22979),f5(x22978,x22979)))),x22975,x22976,x22977))), % 59.67/59.69 inference(scs_inference,[],[2263,2138,1756,2175,121,200,115,5,2])). % 59.67/59.69 cnf(2312,plain, % 59.67/59.69 (~E(f5(a1,f3(f5(f53(f53(a34,a1),a1),f3(f5(f53(f53(a33,a34),f53(f53(a34,a1),a1)),a32),f5(f53(a33,a34),a41))),f5(f53(a34,a1),a42))),f5(a1,a4))), % 59.67/59.69 inference(scs_inference,[],[2200,121])). % 59.67/59.69 cnf(2336,plain, % 59.67/59.69 (P1(f5(a1,f16(f5(a1,x23361),f5(a1,f3(f5(f53(x23362,a1),f3(f5(f53(x23362,f53(x23362,a1)),a21),f5(x23362,x23363))),f5(x23362,x23363))))))), % 59.67/59.69 inference(scs_inference,[],[308,151,109])). % 59.67/59.69 cnf(2344,plain, % 59.67/59.69 (E(f46(x23441,x23442,x23443,f40(f5(a1,a2),x23444,x23445,x23446,x23447)),f46(x23441,x23442,x23443,f40(f5(a1,f20(f5(x23448,x23449),f5(x23448,x23449))),x23444,x23445,x23446,x23447)))), % 59.67/59.69 inference(scs_inference,[],[2312,2336,2289,121,200,115,5,2])). % 59.67/59.69 cnf(2362,plain, % 59.67/59.69 (P1(f5(a1,f16(f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42))),f5(a1,x23621))))), % 59.67/59.69 inference(scs_inference,[],[211,152,110])). % 59.67/59.69 cnf(2363,plain, % 59.67/59.69 (~E(f5(a1,f16(f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42))),f5(a1,x23631))),f5(a1,a4))), % 59.67/59.69 inference(scs_inference,[],[2362,121])). % 59.67/59.69 cnf(2374,plain, % 59.67/59.69 (E(f39(x23741,x23742,f39(x23743,x23744,x23745,f5(a1,a2)),x23746),f39(x23741,x23742,f39(x23743,x23744,x23745,f5(a1,f20(f5(x23747,x23748),f5(x23747,x23748)))),x23746))), % 59.67/59.69 inference(scs_inference,[],[2176,2362,2007,121,122,116,200,115,5,2])). % 59.67/59.69 cnf(2400,plain, % 59.67/59.69 (P1(f5(a1,f19(f5(a1,x24001),f5(a1,f20(f5(x24002,x24003),f5(x24002,x24003))))))), % 59.67/59.69 inference(scs_inference,[],[269,153,113])). % 59.67/59.69 cnf(2412,plain, % 59.67/59.69 (E(f49(x24121,x24122,x24123,f46(f5(a1,a2),x24124,x24125,x24126)),f49(x24121,x24122,x24123,f46(f5(a1,f20(f5(x24127,x24128),f5(x24127,x24128))),x24124,x24125,x24126)))), % 59.67/59.69 inference(scs_inference,[],[2212,2400,2236,121,122,116,200,115,5,2])). % 59.67/59.69 cnf(2439,plain, % 59.67/59.69 (~E(f5(a1,f3(f5(f53(f53(f53(x24391,a1),a1),a1),f3(f5(f53(f53(a1,f53(x24391,a1)),f53(f53(f53(x24391,a1),a1),a1)),a28),f5(f53(a1,f53(x24391,a1)),a35))),f5(f53(f53(x24391,a1),a1),a10))),f5(a1,a4))), % 59.67/59.69 inference(scs_inference,[],[2108,121])). % 59.67/59.69 cnf(2446,plain, % 59.67/59.69 (E(f46(x24461,f46(x24462,x24463,f5(a1,a2),x24464),x24465,x24466),f46(x24461,f46(x24462,x24463,f5(a1,f20(f5(x24467,x24468),f5(x24467,x24468))),x24464),x24465,x24466))), % 59.67/59.69 inference(scs_inference,[],[2363,2108,2262,1587,121,200,115,5,2])). % 59.67/59.69 cnf(2463,plain, % 59.67/59.69 (~E(f5(a1,f3(f5(f53(f53(f53(x24631,a1),a1),a1),f3(f5(f53(f53(a1,f53(x24631,a1)),f53(f53(f53(x24631,a1),a1),a1)),a14),f5(f53(a1,f53(x24631,a1)),a35))),f5(f53(f53(x24631,a1),a1),a8))),f5(a1,a4))), % 59.67/59.69 inference(scs_inference,[],[1743,121])). % 59.67/59.69 cnf(2468,plain, % 59.67/59.69 (E(f20(x24681,f37(x24682,x24683,x24684,f5(a1,a2))),f20(x24681,f37(x24682,x24683,x24684,f5(a1,f20(f5(x24685,x24686),f5(x24685,x24686))))))), % 59.67/59.69 inference(scs_inference,[],[1650,1743,1580,121,200,5,2])). % 59.67/59.69 cnf(2471,plain, % 59.67/59.69 (E(f46(x24711,f46(x24712,x24713,f5(a1,a2),x24714),x24715,f40(f5(a1,a2),x24716,x24717,x24718,x24719)),f46(x24711,f46(x24712,x24713,f5(a1,f20(f5(x247110,x247111),f5(x247110,x247111))),x24714),x24715,f40(f5(a1,f20(f5(x247112,x247113),f5(x247112,x247113))),x24716,x24717,x24718,x24719)))), % 59.67/59.69 inference(scs_inference,[],[205,1650,1920,1743,2344,2446,1580,121,200,5,2,131,3])). % 59.67/59.69 cnf(2484,plain, % 59.67/59.69 (~E(f5(a1,f23(f5(f53(x24841,f53(x24841,a1)),a21),f5(f53(f53(x24841,a1),a1),f3(f5(f53(f53(x24842,x24841),f53(f53(x24841,a1),a1)),a14),f5(f53(x24842,x24841),x24843))))),f5(a1,a4))), % 59.67/59.69 inference(scs_inference,[],[1702,121])). % 59.67/59.69 cnf(2492,plain, % 59.67/59.69 (E(f39(f39(x24921,f5(a1,f20(f5(x24922,x24923),f5(x24922,x24923))),x24924,x24925),x24926,f39(x24927,x24928,x24929,f5(a1,a2)),x249210),f39(f39(x24921,f5(a1,a2),x24924,x24925),x24926,f39(x24927,x24928,x24929,f5(a1,f20(f5(x249211,x249212),f5(x249211,x249212)))),x249210))), % 59.67/59.69 inference(scs_inference,[],[269,2362,1807,1702,2374,2471,1963,121,200,5,2,131,3])). % 59.67/59.69 cnf(2504,plain, % 59.67/59.69 (~E(f5(a1,f23(f5(f53(a1,f53(x25041,a1)),a35),f5(f53(f53(x25041,a1),a1),f3(f5(f53(f53(x25042,x25041),f53(f53(x25041,a1),a1)),a14),f5(f53(x25042,x25041),x25043))))),f5(a1,a4))), % 59.67/59.69 inference(scs_inference,[],[1756,121])). % 59.67/59.69 cnf(2509,plain, % 59.67/59.69 (E(f45(x25091,f48(x25092,f5(a1,a2),x25093,x25094)),f45(x25091,f48(x25092,f5(a1,f20(f5(x25095,x25096),f5(x25095,x25096))),x25093,x25094)))), % 59.67/59.69 inference(scs_inference,[],[2484,1756,1701,121,200,5,2])). % 59.67/59.69 cnf(2512,plain, % 59.67/59.69 (E(f49(x25121,f49(x25122,x25123,f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42))),x25124),x25125,f46(f5(a1,a2),x25126,x25127,x25128)),f49(x25121,f49(x25122,x25123,f5(a1,a2),x25124),x25125,f46(f5(a1,f20(f5(x25129,x251210),f5(x25129,x251210))),x25126,x25127,x25128)))), % 59.67/59.69 inference(scs_inference,[],[205,2484,1862,1756,2412,1701,2211,121,200,5,2,131,3])). % 59.67/59.69 cnf(2532,plain, % 59.67/59.69 (E(f49(x25321,f49(x25322,x25323,f5(a1,a2),x25324),x25325,f46(f5(a1,f20(f5(x25326,x25327),f5(x25326,x25327))),x25328,x25329,x253210)),f49(x25321,f49(x25322,x25323,f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42))),x25324),x25325,f46(f5(a1,a2),x25328,x25329,x253210)))), % 59.67/59.69 inference(scs_inference,[],[2439,1813,2512,121,200,5,2])). % 59.67/59.69 cnf(2535,plain, % 59.67/59.69 (E(f49(f38(x25351,x25352,x25353,x25354,f5(a1,a2)),f49(x25355,x25356,f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42))),x25357),x25358,f46(f5(a1,a2),x25359,x253510,x253511)),f49(f38(x25351,x25352,x25353,x25354,f5(a1,f20(f5(x253512,x253513),f5(x253512,x253513)))),f49(x25355,x25356,f5(a1,a2),x25357),x25358,f46(f5(a1,f20(f5(x253514,x253515),f5(x253514,x253515))),x25359,x253510,x253511)))), % 59.67/59.69 inference(scs_inference,[],[269,2336,2439,1813,2512,2297,121,200,5,2,131,3])). % 59.67/59.69 cnf(2547,plain, % 59.67/59.69 (~E(f5(a1,f29(f5(f53(x25471,x25472),x25473),f5(f53(x25472,a1),f3(f5(f53(a1,f53(x25472,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42))))))),f5(a1,a4))), % 59.67/59.69 inference(scs_inference,[],[1512,121])). % 59.67/59.69 cnf(2555,plain, % 59.67/59.69 (E(f49(f38(x25551,x25552,x25553,x25554,f5(a1,a2)),f49(x25555,x25556,f5(a1,a2),x25557),x25558,f46(f5(a1,f20(f5(x25559,x255510),f5(x25559,x255510))),x255511,x255512,x255513)),f49(f38(x25551,x25552,x25553,x25554,f5(a1,f20(f5(x255514,x255515),f5(x255514,x255515)))),f49(x25555,x25556,f5(a1,a2),x25557),x25558,f46(f5(a1,f20(f5(x255516,x255517),f5(x255516,x255517))),x255511,x255512,x255513)))), % 59.67/59.69 inference(scs_inference,[],[205,2463,2138,1512,2532,2535,121,200,5,2,131,3])). % 59.67/59.69 cnf(2573,plain, % 59.67/59.69 (~E(f5(a1,f27(f5(f53(x25731,x25732),x25733),f5(f53(x25732,a1),f3(f5(f53(a1,f53(x25732,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42))))))),f5(a1,a4))), % 59.67/59.69 inference(scs_inference,[],[1518,121])). % 59.67/59.69 cnf(2581,plain, % 59.67/59.69 (E(f20(f37(x25811,x25812,f5(a1,a2),x25813),f37(x25814,x25815,x25816,f5(a1,a2))),f20(f37(x25811,x25812,f5(a1,f20(f5(x25817,x25818),f5(x25817,x25818))),x25813),f37(x25814,x25815,x25816,f5(a1,f20(f5(x25819,x258110),f5(x25819,x258110))))))), % 59.67/59.69 inference(scs_inference,[],[269,2547,1920,1481,1518,2468,2492,121,200,5,2,131,3])). % 59.67/59.69 cnf(2595,plain, % 59.67/59.69 (~E(f5(a1,f7(f5(f53(x25951,x25952),x25953),f5(f53(x25952,a1),f3(f5(f53(a1,f53(x25952,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a43))))))),f5(a1,a4))), % 59.67/59.69 inference(scs_inference,[],[1528,121])). % 59.67/59.69 cnf(2600,plain, % 59.67/59.69 (E(f49(f38(x26001,x26002,x26003,x26004,f5(a1,f20(f5(x26005,x26006),f5(x26005,x26006)))),f49(x26007,x26008,f5(a1,a2),x26009),x260010,f46(f5(a1,f20(f5(x260011,x260012),f5(x260011,x260012))),x260013,x260014,x260015)),f49(f38(x26001,x26002,x26003,x26004,f5(a1,a2)),f49(x26007,x26008,f5(a1,a2),x26009),x260010,f46(f5(a1,f20(f5(x260016,x260017),f5(x260016,x260017))),x260013,x260014,x260015)))), % 59.67/59.69 inference(scs_inference,[],[2573,1528,2555,121,200,5,2])). % 59.67/59.69 cnf(2620,plain, % 59.67/59.69 (~E(f5(a1,f29(f5(f53(x26201,x26202),x26203),f5(f53(x26202,a1),f3(f5(f53(a1,f53(x26202,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a43))))))),f5(a1,a4))), % 59.67/59.69 inference(scs_inference,[],[1531,121])). % 59.67/59.69 cnf(2628,plain, % 59.67/59.69 (E(f45(f48(f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42))),x26281,x26282,x26283),f48(x26284,f5(a1,a2),x26285,x26286)),f45(f48(f5(a1,a2),x26281,x26282,x26283),f48(x26284,f5(a1,f20(f5(x26287,x26288),f5(x26287,x26288))),x26285,x26286)))), % 59.67/59.69 inference(scs_inference,[],[269,2595,1595,1531,2509,2581,1643,121,200,5,2,131,3])). % 59.67/59.69 cnf(2639,plain, % 59.67/59.69 (~P1(f5(a1,f11(f5(a1,x26391),f5(a1,a4))))), % 59.67/59.69 inference(scs_inference,[],[267,156,116])). % 59.67/59.69 cnf(2648,plain, % 59.67/59.69 (~P2(f11(f5(a1,x26481),f5(a1,a4)),x26482,x26482)), % 59.67/59.69 inference(scs_inference,[],[2639,110,113,109,114,201])). % 59.67/59.69 cnf(2650,plain, % 59.67/59.69 (~E(f5(a1,f23(f5(f53(x26501,x26502),x26503),f5(f53(x26502,a1),f3(f5(f53(a1,f53(x26502,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42))))))),f5(a1,a4))), % 59.67/59.69 inference(scs_inference,[],[1587,2639,110,113,109,114,201,121])). % 59.67/59.69 cnf(2664,plain, % 59.67/59.69 (E(f45(f48(f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42))),x26641,x26642,x26643),f48(x26644,f5(a1,f20(f5(x26645,x26646),f5(x26645,x26646))),x26647,x26648)),f45(f48(f5(a1,a2),x26641,x26642,x26643),f48(x26644,f5(a1,f20(f5(x26649,x266410),f5(x26649,x266410))),x26647,x26648)))), % 59.67/59.69 inference(scs_inference,[],[91,205,2620,2200,1587,2628,2639,1701,110,113,109,114,201,121,200,5,2,137,130,128,131,3])). % 59.67/59.69 cnf(2678,plain, % 59.67/59.69 (E(f45(f48(f5(a1,a2),x26781,x26782,x26783),f48(x26784,f5(a1,f20(f5(x26785,x26786),f5(x26785,x26786))),x26787,x26788)),f45(f48(f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42))),x26781,x26782,x26783),f48(x26784,f5(a1,f20(f5(x26789,x267810),f5(x26789,x267810))),x26787,x26788)))), % 59.67/59.69 inference(scs_inference,[],[2650,2664,5,2])). % 59.67/59.69 cnf(2683,plain, % 59.67/59.69 (E(f49(f38(x26831,x26832,x26833,x26834,f5(a1,f20(f5(x26835,x26836),f5(x26835,x26836)))),f49(x26837,x26838,f5(a1,a2),x26839),x268310,f46(f5(a1,a2),x268311,x268312,x268313)),f49(f38(x26831,x26832,x26833,x26834,f5(a1,a2)),f49(x26837,x26838,f5(a1,a2),x26839),x268310,f46(f5(a1,f20(f5(x268314,x268315),f5(x268314,x268315))),x268311,x268312,x268313)))), % 59.67/59.69 inference(scs_inference,[],[269,2650,1644,2639,2600,2664,2412,5,2,137,131,3])). % 59.67/59.69 cnf(2697,plain, % 59.67/59.69 (E(f49(f38(x26971,x26972,x26973,x26974,f5(a1,a2)),f49(x26975,x26976,f5(a1,a2),x26977),x26978,f46(f5(a1,f20(f5(x26979,x269710),f5(x26979,x269710))),x269711,x269712,x269713)),f49(f38(x26971,x26972,x26973,x26974,f5(a1,f20(f5(x269714,x269715),f5(x269714,x269715)))),f49(x26975,x26976,f5(a1,a2),x26977),x26978,f46(f5(a1,a2),x269711,x269712,x269713)))), % 59.67/59.69 inference(scs_inference,[],[2504,2683,5,2])). % 59.67/59.69 cnf(2703,plain, % 59.67/59.69 (P2(f9(f5(f53(x27031,a1),f3(f5(f53(a1,f53(x27031,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42)))))),f5(a1,f3(f5(f53(a1,a1),a6),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42))))),f5(a1,f20(f5(x27032,x27033),f5(x27032,x27033))))), % 59.67/59.69 inference(scs_inference,[],[205,310,2504,1026,2108,2683,2678,2509,5,2,131,3,85])). % 59.67/59.69 cnf(2806,plain, % 59.67/59.69 (P2(f9(f5(f53(x28061,a1),f3(f5(f53(a1,f53(x28061,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42)))))),f5(a1,f3(f5(f53(a1,a1),a6),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42))))),f5(a1,a2))), % 59.67/59.69 inference(scs_inference,[],[205,269,1500,456,312,274,1756,700,2148,2703,1878,1011,5,2,125,131,3,84,86])). % 59.67/59.69 cnf(2850,plain, % 59.67/59.69 (P1(f5(a1,f3(f5(f53(f53(x28501,a1),a1),a8),f5(f53(x28501,a1),f44(f53(x28501,a1),a8)))))), % 59.67/59.69 inference(scs_inference,[],[269,835,1576,2200,271,1753,1806,2004,2093,1643,5,2,131,3,84,83])). % 59.67/59.69 cnf(2858,plain, % 59.67/59.69 (P1(f5(a1,f3(f5(f53(a1,a1),a6),f5(a1,f9(f5(f53(x28581,a1),f44(f53(x28581,a1),a8)))))))), % 59.67/59.69 inference(scs_inference,[],[104,269,835,1576,221,2200,271,1753,1806,2004,2093,1841,1643,5,2,131,3,84,83,147,146,143,534])). % 59.67/59.69 cnf(2874,plain, % 59.67/59.69 (~E(f5(a1,f3(f5(f53(a1,a1),a6),f5(a1,f9(f5(f53(x28741,a1),f44(f53(x28741,a1),a8)))))),f5(a1,a4))), % 59.67/59.69 inference(scs_inference,[],[2858,116,121])). % 59.67/59.69 cnf(2902,plain, % 59.67/59.69 (E(f49(x29021,f49(x29022,x29023,f5(a1,a2),x29024),x29025,x29026),f49(x29021,f49(x29022,x29023,f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a42))),x29024),x29025,x29026))), % 59.67/59.69 inference(scs_inference,[],[2874,2211,5,2])). % 59.67/59.69 cnf(3124,plain, % 59.67/59.69 (~P1(f5(a1,f3(f5(f53(a1,a1),a6),f5(a1,f3(f5(f53(f53(x31241,a1),a1),a10),f5(f53(x31241,a1),f3(f5(f53(a1,f53(x31241,a1)),a35),f5(a1,f7(f5(f53(a33,a34),a41),f5(f53(a34,a1),a43))))))))))), % 59.67/59.69 inference(scs_inference,[],[814,207,715,697,808,1376,2902,2697,2806,2648,384,469,133,3,84,86,83])). % 59.67/59.69 cnf(3133,plain, % 59.67/59.69 (~P1(f5(a1,f27(f5(f53(f53(x31331,a1),a1),a10),f5(f53(a1,a1),a6))))), % 59.67/59.69 inference(scs_inference,[],[104,91,1590,814,207,1607,715,697,808,1376,2902,2697,2806,2648,384,469,133,3,84,86,83,136,147,146,171])). % 59.67/59.69 cnf(3135,plain, % 59.67/59.69 (P1(f5(a1,f29(f5(f53(f53(x31351,a1),a1),a10),f5(f53(a1,a1),a6))))), % 59.67/59.69 inference(scs_inference,[],[104,91,1590,814,207,1607,715,697,808,1376,2902,2697,2806,2648,384,469,133,3,84,86,83,136,147,146,171,170])). % 59.67/59.69 cnf(3137,plain, % 59.67/59.69 (E(f5(a1,f27(f5(f53(f53(x31371,a1),a1),a10),f5(f53(a1,a1),a6))),f5(a1,a4))), % 59.67/59.69 inference(scs_inference,[],[104,91,1590,814,207,1607,715,697,808,1376,2902,2697,2806,2648,384,469,133,3,84,86,83,136,147,146,171,170,109])). % 59.67/59.69 cnf(3139,plain, % 59.67/59.69 (~E(f5(a1,f27(f5(f53(f53(x31391,a1),a1),a10),f5(f53(a1,a1),a6))),f5(a1,a2))), % 59.67/59.69 inference(scs_inference,[],[104,91,1590,814,207,1607,715,697,808,1376,2902,2697,2806,2648,384,469,133,3,84,86,83,136,147,146,171,170,109,113])). % 59.67/59.69 cnf(3143,plain, % 59.67/59.69 (~P2(f27(f5(f53(f53(x31431,a1),a1),a10),f5(f53(a1,a1),a6)),x31432,x31432)), % 59.67/59.69 inference(scs_inference,[],[104,91,1590,814,207,1607,715,697,808,1376,2902,2697,2806,2648,384,469,133,3,84,86,83,136,147,146,171,170,109,113,110,201])). % 59.67/59.69 cnf(3147,plain, % 59.67/59.69 (~E(f5(a1,a4),f5(a1,f29(f5(f53(f53(x31471,a1),a1),a10),f5(f53(a1,a1),a6))))), % 59.67/59.69 inference(scs_inference,[],[104,91,1590,814,207,1607,715,697,808,1376,2902,2697,2806,2648,384,469,133,3,84,86,83,136,147,146,171,170,109,113,110,201,114,122])). % 59.67/59.69 cnf(3149,plain, % 59.67/59.69 (E(f5(a1,a2),f5(a1,f29(f5(f53(f53(x31491,a1),a1),a10),f5(f53(a1,a1),a6))))), % 59.67/59.69 inference(scs_inference,[],[104,91,1590,814,207,1607,715,697,808,1376,2902,2697,2806,2648,384,469,133,3,84,86,83,136,147,146,171,170,109,113,110,201,114,122,116])). % 59.67/59.69 cnf(3155,plain, % 59.67/59.69 (E(f5(a1,f29(f5(f53(f53(x31551,a1),a1),a10),f5(f53(a1,a1),a6))),f5(a1,a2))), % 59.67/59.69 inference(scs_inference,[],[104,91,1590,814,207,1607,715,697,808,1376,2902,2697,2806,2648,384,469,133,3,84,86,83,136,147,146,171,170,109,113,110,201,114,122,116,121,200,115])). % 59.67/59.69 cnf(3268,plain, % 59.67/59.69 (E(f5(x32681,x32682),f5(x32681,f3(f5(f53(x32681,x32681),a6),f5(x32681,x32682))))), % 59.67/59.69 inference(rename_variables,[],[225])). % 59.67/59.69 cnf(3271,plain, % 59.67/59.69 (E(f5(x32711,x32712),f5(x32711,f3(f5(f53(x32711,x32711),a6),f5(x32711,x32712))))), % 59.67/59.69 inference(rename_variables,[],[225])). % 59.67/59.69 cnf(3337,plain, % 59.67/59.69 ($false), % 59.67/59.69 inference(scs_inference,[],[91,616,317,405,303,3143,3137,3139,3155,3147,3149,3133,3135,3124,1139,679,258,853,2850,839,225,3268,3271,715,90,104,8,41,54,4,9,10,15,16,17,18,19,21,22,31,32,37,38,39,40,42,43,44,45,55,56,66,67,72,73,11,12,13,14,23,24,25,26,27,28,29,30,33,34,35,36,46,47,48,49,50,51,52,53,62,63,64,65,68,69,70,71,74,75,76,77,138,57,58,59,60,61,78,79,80,81,82,150,151,152,153,156,157,154,160,158,162,168,169,187,149,7,163,6,179,164,110,113,20,122,5,2,155,161,190,159,137,130,125,131,85,3,84,86,83,139,136,147,146,143,165,421,192]), % 59.67/59.69 ['proof']). % 59.67/59.69 % SZS output end Proof % 59.67/59.69 % Total time :58.890000s %------------------------------------------------------------------------------