%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : COL121-2 : TPTP v8.2.0. Released v3.2.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n011.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 04:45:17 EDT 2024 % Result : Unsatisfiable 266.39s 266.79s % Output : CNFRefutation 266.71s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.11 % Problem : COL121-2 : TPTP v8.2.0. Released v3.2.0. % 0.06/0.11 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.10/0.31 % Computer : n011.cluster.edu % 0.10/0.31 % Model : x86_64 x86_64 % 0.10/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.31 % Memory : 8042.1875MB % 0.10/0.31 % OS : Linux 3.10.0-693.el7.x86_64 % 0.10/0.31 % CPULimit : 300 % 0.10/0.31 % WCLimit : 300 % 0.10/0.31 % DateTime : Tue Jun 18 16:28:54 EDT 2024 % 0.10/0.31 % CPUTime : % 0.49/0.55 start to proof:theBenchmark % 266.30/266.76 %------------------------------------------- % 266.30/266.76 % File :CSE---1.7 % 266.30/266.76 % Problem :theBenchmark % 266.30/266.76 % Transform :cnf % 266.30/266.76 % Format :tptp:raw % 266.30/266.76 % Command :java -jar mcs_scs.jar %d %s % 266.30/266.76 % 266.30/266.76 % Result :Theorem 265.700000s % 266.30/266.76 % Output :CNFRefutation 265.700000s % 266.30/266.76 %------------------------------------------- % 266.30/266.78 %------------------------------------------------------------------------------ % 266.30/266.78 % File : COL121-2 : TPTP v8.2.0. Released v3.2.0. % 266.30/266.78 % Domain : Combinatory Logic % 266.30/266.78 % Problem : Problem about combinators % 266.30/266.78 % Version : [Pau06] axioms : Reduced > Especial. % 266.30/266.78 % English : % 266.30/266.78 % 266.30/266.78 % Refs : [Pau06] Paulson (2006), Email to G. Sutcliffe % 266.30/266.78 % Source : [Pau06] % 266.30/266.78 % Names : % 266.30/266.78 % 266.30/266.78 % Status : Unsatisfiable % 266.39/266.79 % Rating : 0.00 v7.4.0, 0.17 v7.3.0, 0.00 v5.4.0, 0.06 v5.3.0, 0.10 v5.2.0, 0.08 v5.1.0, 0.06 v5.0.0, 0.07 v4.0.1, 0.00 v3.2.0 % 266.39/266.79 % Syntax : Number of clauses : 10 ( 3 unt; 0 nHn; 10 RR) % 266.39/266.79 % Number of literals : 22 ( 0 equ; 13 neg) % 266.39/266.79 % Maximal clause size : 4 ( 2 avg) % 266.39/266.79 % Maximal term depth : 3 ( 1 avg) % 266.39/266.79 % Number of predicates : 2 ( 2 usr; 0 prp; 2-3 aty) % 266.39/266.79 % Number of functors : 11 ( 11 usr; 6 con; 0-4 aty) % 266.39/266.79 % Number of variables : 21 ( 0 sgn) % 266.39/266.79 % SPC : CNF_UNS_RFO_NEQ_HRN % 266.39/266.79 % 266.39/266.79 % Comments : The problems in the [Pau06] collection each have very many axioms, % 266.39/266.79 % of which only a small selection are required for the refutation. % 266.39/266.79 % The mission is to find those few axioms, after which a refutation % 266.39/266.79 % can be quite easily found. This version has only the necessary % 266.39/266.79 % axioms. % 266.39/266.79 %------------------------------------------------------------------------------ % 266.39/266.79 cnf(cls_Comb_Odiamond__strip__lemmaE_0,axiom, % 266.39/266.79 ( ~ c_Comb_Odiamond(V_r,T_a) % 266.39/266.79 | ~ c_in(c_Pair(V_x,V_y_H,T_a,T_a),V_r,tc_prod(T_a,T_a)) % 266.39/266.79 | ~ c_in(c_Pair(V_x,V_y,T_a,T_a),c_Transitive__Closure_Ortrancl(V_r,T_a),tc_prod(T_a,T_a)) % 266.39/266.79 | c_in(c_Pair(V_y_H,c_Comb_Odiamond__strip__lemmaE__1(V_r,V_y,V_y_H,T_a),T_a,T_a),c_Transitive__Closure_Ortrancl(V_r,T_a),tc_prod(T_a,T_a)) ) ). % 266.39/266.79 % 266.39/266.79 cnf(cls_Comb_Odiamond__strip__lemmaE_1,axiom, % 266.39/266.79 ( ~ c_Comb_Odiamond(V_r,T_a) % 266.39/266.79 | ~ c_in(c_Pair(V_x,V_y_H,T_a,T_a),V_r,tc_prod(T_a,T_a)) % 266.39/266.79 | ~ c_in(c_Pair(V_x,V_y,T_a,T_a),c_Transitive__Closure_Ortrancl(V_r,T_a),tc_prod(T_a,T_a)) % 266.39/266.79 | c_in(c_Pair(V_y,c_Comb_Odiamond__strip__lemmaE__1(V_r,V_y,V_y_H,T_a),T_a,T_a),V_r,tc_prod(T_a,T_a)) ) ). % 266.39/266.79 % 266.39/266.79 cnf(cls_Transitive__Closure_Or__into__rtrancl_0,axiom, % 266.39/266.79 ( ~ c_in(V_p,V_r,tc_prod(T_a,T_a)) % 266.39/266.79 | c_in(V_p,c_Transitive__Closure_Ortrancl(V_r,T_a),tc_prod(T_a,T_a)) ) ). % 266.39/266.79 % 266.39/266.79 cnf(cls_Transitive__Closure_Ortrancl__trans_0,axiom, % 266.39/266.79 ( ~ c_in(c_Pair(V_b,V_c,T_a,T_a),c_Transitive__Closure_Ortrancl(V_r,T_a),tc_prod(T_a,T_a)) % 266.39/266.79 | ~ c_in(c_Pair(V_a,V_b,T_a,T_a),c_Transitive__Closure_Ortrancl(V_r,T_a),tc_prod(T_a,T_a)) % 266.39/266.79 | c_in(c_Pair(V_a,V_c,T_a,T_a),c_Transitive__Closure_Ortrancl(V_r,T_a),tc_prod(T_a,T_a)) ) ). % 266.39/266.79 % 266.39/266.79 cnf(cls_conjecture_0,negated_conjecture, % 266.39/266.79 c_Comb_Odiamond(v_r,t_a) ). % 266.39/266.79 % 266.39/266.79 cnf(cls_conjecture_2,negated_conjecture, % 266.39/266.79 c_in(c_Pair(v_ya,v_z,t_a,t_a),v_r,tc_prod(t_a,t_a)) ). % 266.39/266.79 % 266.39/266.79 cnf(cls_conjecture_3,negated_conjecture, % 266.39/266.79 c_in(c_Pair(v_y,v_xaa,t_a,t_a),c_Transitive__Closure_Ortrancl(v_r,t_a),tc_prod(t_a,t_a)) ). % 266.39/266.79 % 266.39/266.79 cnf(cls_conjecture_4,negated_conjecture, % 266.39/266.79 ( c_in(c_Pair(v_ya,v_x(V_U),t_a,t_a),c_Transitive__Closure_Ortrancl(v_r,t_a),tc_prod(t_a,t_a)) % 266.39/266.79 | ~ c_in(c_Pair(v_y,V_U,t_a,t_a),c_Transitive__Closure_Ortrancl(v_r,t_a),tc_prod(t_a,t_a)) ) ). % 266.39/266.79 % 266.39/266.79 cnf(cls_conjecture_5,negated_conjecture, % 266.39/266.79 ( c_in(c_Pair(V_U,v_x(V_U),t_a,t_a),c_Transitive__Closure_Ortrancl(v_r,t_a),tc_prod(t_a,t_a)) % 266.39/266.79 | ~ c_in(c_Pair(v_y,V_U,t_a,t_a),c_Transitive__Closure_Ortrancl(v_r,t_a),tc_prod(t_a,t_a)) ) ). % 266.39/266.79 % 266.39/266.79 cnf(cls_conjecture_6,negated_conjecture, % 266.39/266.79 ( ~ c_in(c_Pair(v_xaa,V_U,t_a,t_a),c_Transitive__Closure_Ortrancl(v_r,t_a),tc_prod(t_a,t_a)) % 266.39/266.79 | ~ c_in(c_Pair(v_z,V_U,t_a,t_a),c_Transitive__Closure_Ortrancl(v_r,t_a),tc_prod(t_a,t_a)) ) ). % 266.39/266.79 % 266.39/266.79 %------------------------------------------------------------------------------ % 266.39/266.79 %------------------------------------------- % 266.39/266.79 % Proof found % 266.39/266.79 % SZS status Theorem for theBenchmark % 266.39/266.79 % SZS output start Proof % 266.41/266.81 %ClaNum:10(EqnAxiom:0) % 266.41/266.81 %VarNum:95(SingletonVarNum:21) % 266.41/266.81 %MaxLitNum:4 % 266.41/266.81 %MaxfuncDepth:2 % 266.41/266.81 %SharedTerms:13 % 266.41/266.81 %goalClause: 1 2 3 5 6 7 % 266.41/266.82 %singleGoalClaCount:3 % 266.41/266.82 [1]P1(a1,a2) % 266.41/266.82 [2]P2(f3(a7,a11,a2,a2),a1,f6(a2,a2)) % 266.41/266.82 [3]P2(f3(a8,a9,a2,a2),f5(a1,a2),f6(a2,a2)) % 266.41/266.82 [7]~P2(f3(a9,x71,a2,a2),f5(a1,a2),f6(a2,a2))+~P2(f3(a11,x71,a2,a2),f5(a1,a2),f6(a2,a2)) % 266.41/266.82 [5]~P2(f3(a8,x51,a2,a2),f5(a1,a2),f6(a2,a2))+P2(f3(a7,f10(x51),a2,a2),f5(a1,a2),f6(a2,a2)) % 266.41/266.82 [6]~P2(f3(a8,x61,a2,a2),f5(a1,a2),f6(a2,a2))+P2(f3(x61,f10(x61),a2,a2),f5(a1,a2),f6(a2,a2)) % 266.41/266.82 [4]~P2(x41,x42,f6(x43,x43))+P2(x41,f5(x42,x43),f6(x43,x43)) % 266.41/266.82 [8]P2(f3(x81,x82,x83,x83),f5(x84,x83),f6(x83,x83))+~P2(f3(x85,x82,x83,x83),f5(x84,x83),f6(x83,x83))+~P2(f3(x81,x85,x83,x83),f5(x84,x83),f6(x83,x83)) % 266.41/266.82 [9]~P1(x92,x94)+~P2(f3(x95,x91,x94,x94),f5(x92,x94),f6(x94,x94))+~P2(f3(x95,x93,x94,x94),x92,f6(x94,x94))+P2(f3(x91,f4(x92,x91,x93,x94),x94,x94),x92,f6(x94,x94)) % 266.41/266.82 [10]~P1(x102,x104)+~P2(f3(x105,x103,x104,x104),f5(x102,x104),f6(x104,x104))+~P2(f3(x105,x101,x104,x104),x102,f6(x104,x104))+P2(f3(x101,f4(x102,x103,x101,x104),x104,x104),f5(x102,x104),f6(x104,x104)) % 266.41/266.82 %EqnAxiom % 266.41/266.82 % 266.41/266.82 %------------------------------------------- % 266.52/266.93 cnf(11,plain, % 266.52/266.93 (P2(f3(a11,f4(a1,a11,a11,a2),a2,a2),a1,f6(a2,a2))), % 266.52/266.93 inference(scs_inference,[],[2,1,4,9])). % 266.52/266.93 cnf(12,plain, % 266.52/266.93 (~P2(f3(a9,f4(a1,a11,a11,a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.93 inference(scs_inference,[],[11,7,4])). % 266.52/266.93 cnf(15,plain, % 266.52/266.93 (~P2(f3(a9,x151,a2,a2),f5(a1,a2),f6(a2,a2))+~P2(f3(x151,f4(a1,a11,a11,a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.93 inference(scs_inference,[],[12,4,8])). % 266.52/266.93 cnf(24,plain, % 266.52/266.93 (~P2(f3(a9,a11,a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.93 inference(scs_inference,[],[11,15,4])). % 266.52/266.93 cnf(27,plain, % 266.52/266.93 (~P2(f3(a9,x271,a2,a2),f5(a1,a2),f6(a2,a2))+~P2(f3(x271,a11,a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.93 inference(scs_inference,[],[24,4,8])). % 266.52/266.93 cnf(41,plain, % 266.52/266.93 (P2(f3(a7,f10(a9),a2,a2),f5(f5(a1,a2),a2),f6(a2,a2))), % 266.52/266.93 inference(scs_inference,[],[3,4,5])). % 266.52/266.93 cnf(44,plain, % 266.52/266.93 (~P2(f3(x441,a11,a2,a2),f5(a1,a2),f6(a2,a2))+~P2(f3(a9,x441,a2,a2),a1,f6(a2,a2))), % 266.52/266.93 inference(scs_inference,[],[4,27])). % 266.52/266.93 cnf(50,plain, % 266.52/266.93 (P2(f3(a9,f10(a9),a2,a2),f5(f5(a1,a2),a2),f6(a2,a2))), % 266.52/266.93 inference(scs_inference,[],[3,4,6])). % 266.52/266.93 cnf(2038,plain, % 266.52/266.93 (~P2(f3(x20381,a9,a2,a2),f5(f5(a1,a2),a2),f6(a2,a2))+P2(f3(x20381,f10(a9),a2,a2),f5(f5(f5(a1,a2),a2),a2),f6(a2,a2))), % 266.52/266.93 inference(scs_inference,[],[50,4,8])). % 266.52/266.93 cnf(18414,plain, % 266.52/266.93 (P2(f3(a9,x184141,a2,a2),f5(f5(f5(a1,a2),a2),a2),f6(a2,a2))+~P2(f3(f10(a9),x184141,a2,a2),f5(f5(a1,a2),a2),f6(a2,a2))), % 266.52/266.93 inference(scs_inference,[],[50,4,8])). % 266.52/266.93 cnf(86493,plain, % 266.52/266.93 (P2(f3(a9,f10(a9),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.93 inference(scs_inference,[],[3,6])). % 266.52/266.93 cnf(86495,plain, % 266.52/266.93 (P2(f3(a7,f10(a9),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.93 inference(scs_inference,[],[3,6,5])). % 266.52/266.93 cnf(86497,plain, % 266.52/266.93 (P2(f3(a11,f4(a1,a11,a11,a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.93 inference(scs_inference,[],[11,3,6,5,4])). % 266.52/266.93 cnf(86499,plain, % 266.52/266.93 (P2(f3(a8,f10(a9),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.93 inference(scs_inference,[],[11,3,6,5,4,8])). % 266.52/266.93 cnf(86506,plain, % 266.52/266.93 (~P2(f3(x865061,a7,a2,a2),f5(a1,a2),f6(a2,a2))+P2(f3(x865061,f10(a9),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.93 inference(scs_inference,[],[86495,3,4,8])). % 266.52/266.93 cnf(86510,plain, % 266.52/266.93 (P2(f3(a7,a11,a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.93 inference(scs_inference,[],[2,4])). % 266.52/266.93 cnf(86512,plain, % 266.52/266.93 (~P2(f3(f10(a9),f4(a1,a11,a11,a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.93 inference(scs_inference,[],[86493,12,2,4,8])). % 266.52/266.93 cnf(86516,plain, % 266.52/266.93 (P2(f3(a7,a11,a2,a2),f5(f5(a1,a2),a2),f6(a2,a2))), % 266.52/266.93 inference(scs_inference,[],[86510,4])). % 266.52/266.93 cnf(86518,plain, % 266.52/266.93 (P2(f3(a7,f4(a1,a11,a11,a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.93 inference(scs_inference,[],[86510,86497,4,8])). % 266.52/266.93 cnf(86520,plain, % 266.52/266.93 (P2(f3(a8,x865201,a2,a2),f5(a1,a2),f6(a2,a2))+~P2(f3(f10(a9),x865201,a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.93 inference(scs_inference,[],[86499,8])). % 266.52/266.93 cnf(86526,plain, % 266.52/266.94 (P2(f3(a7,x865261,a2,a2),f5(a1,a2),f6(a2,a2))+~P2(f3(f4(a1,a11,a11,a2),x865261,a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[86518,8])). % 266.52/266.94 cnf(86536,plain, % 266.52/266.94 (P2(f3(a7,x865361,a2,a2),f5(a1,a2),f6(a2,a2))+~P2(f3(f10(a9),x865361,a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[86495,8])). % 266.52/266.94 cnf(86541,plain, % 266.52/266.94 (P2(f3(x865411,f10(a9),a2,a2),f5(a1,a2),f6(a2,a2))+~P2(f3(x865411,a8,a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[86499,8])). % 266.52/266.94 cnf(86544,plain, % 266.52/266.94 (P2(f3(a11,x865441,a2,a2),f5(a1,a2),f6(a2,a2))+~P2(f3(f4(a1,a11,a11,a2),x865441,a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[86497,8])). % 266.52/266.94 cnf(86546,plain, % 266.52/266.94 (P2(f3(a11,f10(a9),a2,a2),f5(a1,a2),f6(a2,a2))+~P2(f3(f4(a1,a11,a11,a2),a7,a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[86497,8,86506])). % 266.52/266.94 cnf(86553,plain, % 266.52/266.94 (P2(f3(a7,x865531,a2,a2),f5(f5(a1,a2),a2),f6(a2,a2))+~P2(f3(a11,x865531,a2,a2),f5(f5(a1,a2),a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[86516,8])). % 266.52/266.94 cnf(86558,plain, % 266.52/266.94 (P2(f3(a8,f10(f10(a9)),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[86499,86520,6])). % 266.52/266.94 cnf(86560,plain, % 266.52/266.94 (P2(f3(a7,f10(f10(a9)),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[86499,86536,6])). % 266.52/266.94 cnf(86567,plain, % 266.52/266.94 (~P2(f3(a11,a8,a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[86493,86541,7])). % 266.52/266.94 cnf(86568,plain, % 266.52/266.94 (~P2(f3(f4(a1,a11,a11,a2),a8,a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[86567,86544])). % 266.52/266.94 cnf(86575,plain, % 266.52/266.94 (P2(f3(a7,f4(a1,a11,a11,a2),a2,a2),f5(f5(a1,a2),a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[86497,86553,4])). % 266.52/266.94 cnf(86586,plain, % 266.52/266.94 (P2(f3(f10(a9),f10(f10(a9)),a2,a2),f5(f5(a1,a2),a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[86499,4,6])). % 266.52/266.94 cnf(86588,plain, % 266.52/266.94 (P2(f3(a11,f4(a1,a11,a11,a2),a2,a2),f5(f5(a1,a2),a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[1,86510,2,4,10])). % 266.52/266.94 cnf(86591,plain, % 266.52/266.94 (P2(f3(f4(a1,a11,a11,a2),f4(a1,f4(a1,a11,a11,a2),a11,a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[86518,1,2,4,9])). % 266.52/266.94 cnf(86593,plain, % 266.52/266.94 (P2(f3(f10(a9),f4(a1,f10(a9),a11,a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[86495,1,2,4,9])). % 266.52/266.94 cnf(86595,plain, % 266.52/266.94 (P2(f3(f4(a1,a11,a11,a2),f4(a1,f4(a1,a11,a11,a2),f4(a1,a11,a11,a2),a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[11,1,86497,4,9])). % 266.52/266.94 cnf(86603,plain, % 266.52/266.94 (P2(f3(a11,f4(a1,f10(a9),a11,a2),a2,a2),f5(f5(a1,a2),a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[1,86495,2,4,10])). % 266.52/266.94 cnf(86609,plain, % 266.52/266.94 (P2(f3(f4(a1,a11,a11,a2),f4(a1,f4(a1,a11,a11,a2),f4(a1,a11,a11,a2),a2),a2,a2),f5(f5(a1,a2),a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[1,86497,11,4,10])). % 266.52/266.94 cnf(86617,plain, % 266.52/266.94 (P2(f3(a11,f4(a1,f4(a1,a11,a11,a2),a11,a2),a2,a2),f5(f5(a1,a2),a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[1,86518,2,4,10])). % 266.52/266.94 cnf(86632,plain, % 266.52/266.94 (~P2(f3(f10(a9),x866321,a2,a2),f5(a1,a2),f6(a2,a2))+P2(f3(a8,x866321,a2,a2),f5(f5(a1,a2),a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[4,86520])). % 266.52/266.94 cnf(86637,plain, % 266.52/266.94 (~P2(f3(f4(a1,a11,a11,a2),x866371,a2,a2),f5(a1,a2),f6(a2,a2))+P2(f3(a11,x866371,a2,a2),f5(f5(a1,a2),a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[4,86544])). % 266.52/266.94 cnf(86658,plain, % 266.52/266.94 (~P2(f3(f4(a1,a11,a11,a2),x866581,a2,a2),f5(a1,a2),f6(a2,a2))+P2(f3(a7,x866581,a2,a2),f5(f5(a1,a2),a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[4,86526])). % 266.52/266.94 cnf(86688,plain, % 266.52/266.94 (~P2(f3(a11,x866881,a2,a2),f5(f5(a1,a2),a2),f6(a2,a2))+P2(f3(a7,x866881,a2,a2),f5(f5(f5(a1,a2),a2),a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[4,86553])). % 266.52/266.94 cnf(86889,plain, % 266.52/266.94 (~P2(f3(a11,f10(a9),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[86493,7])). % 266.52/266.94 cnf(86892,plain, % 266.52/266.94 (~P2(f3(f4(a1,a11,a11,a2),a7,a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[86889,86546])). % 266.52/266.94 cnf(86896,plain, % 266.52/266.94 (~P2(f3(f4(a1,a11,a11,a2),f10(a9),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[86889,86506,86544])). % 266.52/266.94 cnf(87240,plain, % 266.52/266.94 (~P2(f3(f4(a1,a11,a11,a2),a9,a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[86896,86493,8])). % 266.52/266.94 cnf(87251,plain, % 266.52/266.94 (~P2(f3(f4(a1,a11,a11,a2),x872511,a2,a2),f5(a1,a2),f6(a2,a2))+~P2(f3(x872511,a8,a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[86568,8])). % 266.52/266.94 cnf(87261,plain, % 266.52/266.94 (~P2(f3(f4(a1,a11,a11,a2),x872611,a2,a2),f5(a1,a2),f6(a2,a2))+~P2(f3(x872611,a7,a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[86892,8])). % 266.52/266.94 cnf(87274,plain, % 266.52/266.94 (~P2(f3(a11,a9,a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[86889,86493,8])). % 266.52/266.94 cnf(96902,plain, % 266.52/266.94 (P2(f3(a8,f10(a9),a2,a2),f5(f5(f5(a1,a2),a2),a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[3,4,2038])). % 266.52/266.94 cnf(96903,plain, % 266.52/266.94 (P2(f3(a7,f4(a1,f10(a9),a11,a2),a2,a2),f5(f5(a1,a2),a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[86603,86553])). % 266.52/266.94 cnf(96905,plain, % 266.52/266.94 (P2(f3(a7,f4(a1,a11,a11,a2),a2,a2),f5(f5(f5(a1,a2),a2),a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[86575,86603,86553,4])). % 266.52/266.94 cnf(96909,plain, % 266.52/266.94 (P2(f3(a11,f4(a1,f10(f10(a9)),a11,a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[86512,86575,86560,86593,86603,1,2,86553,4,8,10])). % 266.52/266.94 cnf(96911,plain, % 266.52/266.94 (P2(f3(f10(f10(a9)),f4(a1,f10(f10(a9)),a11,a2),a2,a2),a1,f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[86512,86575,86560,86593,86603,1,2,86553,4,8,10,9])). % 266.52/266.94 cnf(96913,plain, % 266.52/266.94 (P2(f3(a7,f4(a1,f4(a1,a11,a11,a2),a11,a2),a2,a2),f5(f5(a1,a2),a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[86617,86553])). % 266.52/266.94 cnf(96915,plain, % 266.52/266.94 (P2(f3(a11,f4(a1,a11,a11,a2),a2,a2),f5(f5(f5(a1,a2),a2),a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[86588,86617,86553,4])). % 266.52/266.94 cnf(96917,plain, % 266.52/266.94 (P2(f3(a11,f4(a1,f4(a1,a11,a11,a2),f4(a1,a11,a11,a2),a2),a2,a2),f5(f5(a1,a2),a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[86588,86609,86617,86553,4,8])). % 266.52/266.94 cnf(96921,plain, % 266.52/266.94 (~P2(f3(f4(a1,a11,a11,a2),x969211,a2,a2),a1,f6(a2,a2))+P2(f3(x969211,f4(a1,f4(a1,f4(a1,a11,a11,a2),f4(a1,a11,a11,a2),a2),x969211,a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[11,86588,86595,86609,86617,96909,1,86553,4,8,9,10])). % 266.52/266.94 cnf(96931,plain, % 266.52/266.94 (P2(f3(f4(a1,a11,a11,a2),f4(a1,f4(a1,a11,a11,a2),a11,a2),a2,a2),f5(f5(a1,a2),a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[86591,96917,86553,4])). % 266.52/266.94 cnf(96933,plain, % 266.52/266.94 (P2(f3(a7,f4(a1,f4(a1,a11,a11,a2),a11,a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[86591,96917,86518,86553,4,8])). % 266.52/266.94 cnf(96935,plain, % 266.52/266.94 (~P2(f3(f4(a1,a11,a11,a2),x969351,a2,a2),a1,f6(a2,a2))+P2(f3(f4(a1,f4(a1,a11,a11,a2),a11,a2),f4(a1,f4(a1,f4(a1,a11,a11,a2),a11,a2),x969351,a2),a2,a2),a1,f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[86591,96917,1,86518,86553,4,8,9])). % 266.52/266.94 cnf(96941,plain, % 266.52/266.94 (P2(f3(f10(a9),f10(f10(a9)),a2,a2),f5(f5(f5(a1,a2),a2),a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[86586,4])). % 266.52/266.94 cnf(96947,plain, % 266.52/266.94 (P2(f3(a8,f10(f10(a9)),a2,a2),f5(f5(f5(a1,a2),a2),a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[96902,96941,4,8])). % 266.52/266.94 cnf(96949,plain, % 266.52/266.94 (P2(f3(f4(a1,a11,a11,a2),f4(a1,f4(a1,f10(f10(a9)),a11,a2),f4(a1,a11,a11,a2),a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[11,96902,96941,96909,1,4,8,10])). % 266.52/266.94 cnf(96951,plain, % 266.52/266.94 (P2(f3(a7,f4(a1,a11,a11,a2),a2,a2),f5(f5(f5(f5(a1,a2),a2),a2),a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[96905,4])). % 266.52/266.94 cnf(96955,plain, % 266.52/266.94 (P2(f3(f4(a1,f4(a1,a11,a11,a2),a11,a2),f4(a1,f4(a1,f4(a1,a11,a11,a2),a11,a2),a11,a2),a2,a2),a1,f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[96933,96905,96949,86568,1,2,4,8,9])). % 266.52/266.94 cnf(96959,plain, % 266.52/266.94 (P2(f3(a11,f4(a1,a11,a11,a2),a2,a2),f5(f5(f5(f5(a1,a2),a2),a2),a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[96915,4])). % 266.52/266.94 cnf(96965,plain, % 266.52/266.94 (P2(f3(f4(a1,a11,a11,a2),f4(a1,f4(a1,a11,a11,a2),a11,a2),a2,a2),f5(f5(f5(a1,a2),a2),a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[96931,4])). % 266.52/266.94 cnf(96971,plain, % 266.52/266.94 (P2(f3(a7,f4(a1,f4(a1,a11,a11,a2),a11,a2),a2,a2),f5(f5(f5(a1,a2),a2),a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[96913,4])). % 266.52/266.94 cnf(96973,plain, % 266.52/266.94 (~P2(f3(f4(a1,f4(a1,a11,a11,a2),f4(a1,a11,a11,a2),a2),a8,a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[96913,86595,86568,4,8])). % 266.52/266.94 cnf(96981,plain, % 266.52/266.94 (P2(f3(a7,f4(a1,f10(a9),a11,a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[96903,86593,86495,4,8])). % 266.52/266.94 cnf(96998,plain, % 266.52/266.94 (P2(f3(a11,f4(a1,f4(a1,f10(a9),a11,a2),a11,a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[96965,96959,96981,1,2,4,8,10])). % 266.52/266.94 cnf(97000,plain, % 266.52/266.94 (P2(f3(f4(a1,f10(a9),a11,a2),f4(a1,f4(a1,f10(a9),a11,a2),a11,a2),a2,a2),a1,f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[96965,96959,96981,1,2,4,8,10,9])). % 266.52/266.94 cnf(97004,plain, % 266.52/266.94 (P2(f3(a7,f4(a1,f4(a1,f10(a9),a11,a2),a11,a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[96971,96998,86510,4,8])). % 266.52/266.94 cnf(97006,plain, % 266.52/266.94 (P2(f3(f4(a1,a11,a11,a2),f4(a1,f4(a1,f4(a1,f10(a9),a11,a2),a11,a2),f4(a1,a11,a11,a2),a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[96971,96998,11,1,86510,4,8,10])). % 266.52/266.94 cnf(97022,plain, % 266.52/266.94 (P2(f3(a11,f4(a1,f4(a1,f4(a1,f10(a9),a11,a2),a11,a2),f4(a1,a11,a11,a2),a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[96947,97006,86497,4,8])). % 266.52/266.94 cnf(97024,plain, % 266.52/266.94 (~P2(f3(f4(a1,f10(a9),a11,a2),x970241,a2,a2),f5(a1,a2),f6(a2,a2))+P2(f3(x970241,f4(a1,x970241,f4(a1,f4(a1,f10(a9),a11,a2),a11,a2),a2),a2,a2),a1,f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[96947,97000,97006,1,86497,4,8,9])). % 266.52/266.94 cnf(97028,plain, % 266.52/266.94 (P2(f3(a7,f4(a1,f4(a1,f10(a9),a11,a2),a11,a2),a2,a2),f5(f5(a1,a2),a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[97004,4])). % 266.52/266.94 cnf(97032,plain, % 266.52/266.94 (P2(f3(a11,f4(a1,f4(a1,f4(a1,f10(a9),a11,a2),a11,a2),f4(a1,a11,a11,a2),a2),a2,a2),f5(f5(a1,a2),a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[97022,4])). % 266.52/266.94 cnf(97036,plain, % 266.52/266.94 (P2(f3(f4(a1,a11,a11,a2),f4(a1,f4(a1,f4(a1,f4(a1,f10(a9),a11,a2),a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[97022,11,1,86889,4,8,10])). % 266.52/266.94 cnf(97044,plain, % 266.52/266.94 (P2(f3(a11,f4(a1,f4(a1,f4(a1,f4(a1,f10(a9),a11,a2),a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[96951,97036,86497,4,8])). % 266.52/266.94 cnf(97046,plain, % 266.52/266.94 (~P2(f3(f4(a1,a11,a11,a2),x970461,a2,a2),a1,f6(a2,a2))+P2(f3(x970461,f4(a1,f4(a1,f4(a1,f4(a1,f4(a1,f10(a9),a11,a2),a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),x970461,a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[96951,97036,1,86497,4,8,10])). % 266.52/266.94 cnf(97062,plain, % 266.52/266.94 (P2(f3(a7,f4(a1,f4(a1,f4(a1,f4(a1,f10(a9),a11,a2),a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[97028,97044,86510,4,8])). % 266.52/266.94 cnf(97064,plain, % 266.52/266.94 (~P2(f3(f10(f10(a9)),x970641,a2,a2),f5(a1,a2),f6(a2,a2))+P2(f3(x970641,f4(a1,x970641,f4(a1,f10(f10(a9)),a11,a2),a2),a2,a2),a1,f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[97028,96911,97044,1,86510,4,8,9])). % 266.52/266.94 cnf(97071,plain, % 266.52/266.94 (~P2(f3(f4(a1,f4(a1,f10(a9),a11,a2),a11,a2),f10(a9),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[97062,96998,86889,4,8])). % 266.52/266.94 cnf(97075,plain, % 266.52/266.94 (P2(f3(f4(a1,f4(a1,a11,a11,a2),a11,a2),f4(a1,f4(a1,f4(a1,a11,a11,a2),a11,a2),a11,a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[96955,4])). % 266.52/266.94 cnf(97077,plain, % 266.52/266.94 (P2(f3(a7,f4(a1,f4(a1,f4(a1,a11,a11,a2),a11,a2),a11,a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[96955,96933,4,8])). % 266.52/266.94 cnf(97082,plain, % 266.52/266.94 (P2(f3(a11,f4(a1,f4(a1,a11,a11,a2),f4(a1,a11,a11,a2),a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[97077,86595,86497,4,8])). % 266.52/266.94 cnf(97084,plain, % 266.52/266.94 (P2(f3(a11,f4(a1,f4(a1,f4(a1,f4(a1,a11,a11,a2),a11,a2),a11,a2),a11,a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[97077,86595,1,86497,2,4,8,10])). % 266.52/266.94 cnf(97088,plain, % 266.52/266.94 (~P2(f3(f4(a1,f4(a1,a11,a11,a2),f4(a1,a11,a11,a2),a2),f10(a9),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[97082,97075,86889,4,8])). % 266.52/266.94 cnf(97090,plain, % 266.52/266.94 (P2(f3(f4(a1,f4(a1,a11,a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,f4(a1,f4(a1,a11,a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),a2,a2),a1,f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[97082,97075,11,1,86889,4,8,9])). % 266.52/266.94 cnf(97093,plain, % 266.52/266.94 (P2(f3(f4(a1,f4(a1,a11,a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,f4(a1,f4(a1,a11,a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[97090,4])). % 266.52/266.94 cnf(97095,plain, % 266.52/266.94 (~P2(f3(f4(a1,f4(a1,f4(a1,a11,a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),a8,a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[96973,97090,4,8])). % 266.52/266.94 cnf(97097,plain, % 266.52/266.94 (P2(f3(f4(a1,f4(a1,f4(a1,a11,a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,f4(a1,f4(a1,f4(a1,a11,a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,f4(a1,f4(a1,a11,a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[96973,97090,1,4,8,10])). % 266.52/266.94 cnf(97101,plain, % 266.52/266.94 (P2(f3(a11,f4(a1,f4(a1,f4(a1,a11,a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[97093,97082,4,8])). % 266.52/266.94 cnf(97105,plain, % 266.52/266.94 (P2(f3(a11,f4(a1,f4(a1,f4(a1,a11,a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),a2,a2),f5(f5(a1,a2),a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[97101,4])). % 266.52/266.94 cnf(97107,plain, % 266.52/266.94 (~P2(f3(f4(a1,f4(a1,f4(a1,a11,a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),f10(a9),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[97088,97101,97093,4,8])). % 266.52/266.94 cnf(97109,plain, % 266.52/266.94 (P2(f3(a7,f4(a1,f4(a1,f4(a1,a11,a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),a2,a2),f5(f5(a1,a2),a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[97088,97101,97093,4,8,86553])). % 266.52/266.94 cnf(97114,plain, % 266.52/266.94 (P2(f3(a11,f4(a1,f4(a1,f4(a1,a11,a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),a2,a2),f5(f5(f5(a1,a2),a2),a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[97105,4])). % 266.52/266.94 cnf(97116,plain, % 266.52/266.94 (~P2(f3(f4(a1,f4(a1,f4(a1,f4(a1,a11,a11,a2),a11,a2),a11,a2),a11,a2),f10(a9),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[97105,97084,86889,4,8])). % 266.52/266.94 cnf(97120,plain, % 266.52/266.94 (P2(f3(f4(a1,a11,a11,a2),f4(a1,f4(a1,f4(a1,f4(a1,f4(a1,a11,a11,a2),a11,a2),a11,a2),a11,a2),f4(a1,a11,a11,a2),a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[97105,97084,11,1,86889,4,8,86541,10])). % 266.52/266.94 cnf(97122,plain, % 266.52/266.94 (P2(f3(a7,f4(a1,f4(a1,f4(a1,a11,a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),a2,a2),f5(f5(f5(a1,a2),a2),a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[97109,4])). % 266.52/266.94 cnf(97124,plain, % 266.52/266.94 (P2(f3(a11,f4(a1,f4(a1,f4(a1,f4(a1,f4(a1,a11,a11,a2),a11,a2),a11,a2),a11,a2),f4(a1,a11,a11,a2),a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[97109,97120,86497,4,8])). % 266.52/266.94 cnf(97128,plain, % 266.52/266.94 (~P2(f3(f4(a1,f4(a1,f4(a1,f4(a1,f4(a1,a11,a11,a2),a11,a2),a11,a2),a11,a2),f4(a1,a11,a11,a2),a2),f10(a9),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[97122,97124,86889,4,8])). % 266.52/266.94 cnf(97138,plain, % 266.52/266.94 (P2(f3(a11,f4(a1,f4(a1,f4(a1,f4(a1,a11,a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,f4(a1,f4(a1,a11,a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[97114,97097,97101,4,8])). % 266.52/266.94 cnf(97140,plain, % 266.52/266.94 (P2(f3(f4(a1,f4(a1,f4(a1,a11,a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,f4(a1,f4(a1,f4(a1,a11,a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),a2,a2),a1,f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[97114,97097,97101,11,1,4,8,9])). % 266.52/266.94 cnf(97142,plain, % 266.52/266.94 (P2(f3(f4(a1,f4(a1,f4(a1,a11,a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,f4(a1,f4(a1,f4(a1,a11,a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[97140,4])). % 266.52/266.94 cnf(97144,plain, % 266.52/266.94 (~P2(f3(f4(a1,f4(a1,f4(a1,f4(a1,a11,a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,f4(a1,f4(a1,a11,a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),a2),f10(a9),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[97107,97140,97097,4,8])). % 266.52/266.94 cnf(97154,plain, % 266.52/266.94 (P2(f3(f4(a1,a11,a11,a2),f4(a1,f4(a1,f4(a1,f4(a1,f4(a1,a11,a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,f4(a1,f4(a1,a11,a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),a2),f4(a1,a11,a11,a2),a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[97095,97142,97138,11,1,4,8,10])). % 266.52/266.94 cnf(97177,plain, % 266.52/266.94 (P2(f3(a7,f10(a9),a2,a2),f5(f5(f5(a1,a2),a2),a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[41,4])). % 266.52/266.94 cnf(97183,plain, % 266.52/266.94 (P2(f3(a7,f10(a9),a2,a2),f5(f5(f5(f5(a1,a2),a2),a2),a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[97177,4])). % 266.52/266.94 cnf(97185,plain, % 266.52/266.94 (P2(f3(a11,f4(a1,f4(a1,f4(a1,f4(a1,f4(a1,a11,a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,f4(a1,f4(a1,a11,a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),a2),f4(a1,a11,a11,a2),a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[97177,97154,86497,4,8])). % 266.52/266.94 cnf(97187,plain, % 266.52/266.94 (P2(f3(f4(a1,a11,a11,a2),f4(a1,f4(a1,f4(a1,f4(a1,f4(a1,f4(a1,a11,a11,a2),a11,a2),a11,a2),a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[97177,97154,97124,11,1,86497,4,8,10])). % 266.52/266.94 cnf(97191,plain, % 266.52/266.94 (~P2(f3(f4(a1,f4(a1,f4(a1,f4(a1,f4(a1,a11,a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,f4(a1,f4(a1,a11,a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),a2),f4(a1,a11,a11,a2),a2),f10(a9),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[97183,97185,86889,4,8])). % 266.52/266.94 cnf(97193,plain, % 266.52/266.94 (P2(f3(f4(a1,a11,a11,a2),f4(a1,f4(a1,f4(a1,f4(a1,f4(a1,f4(a1,a11,a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,f4(a1,f4(a1,a11,a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[97183,97185,11,1,86889,4,8,10])). % 266.52/266.94 cnf(97203,plain, % 266.52/266.94 (P2(f3(a11,f4(a1,f4(a1,f4(a1,f4(a1,f4(a1,f4(a1,a11,a11,a2),a11,a2),a11,a2),a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[97187,86497,4,8])). % 266.52/266.94 cnf(97205,plain, % 266.52/266.94 (P2(f3(f4(a1,a11,a11,a2),f4(a1,f4(a1,f4(a1,f4(a1,f4(a1,f4(a1,a11,a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,f4(a1,f4(a1,a11,a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),a2,a2),f5(f5(a1,a2),a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[97193,4])). % 266.52/266.94 cnf(97221,plain, % 266.52/266.94 (P2(f3(a11,f4(a1,f4(a1,f4(a1,f10(a9),a11,a2),a11,a2),a11,a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[97205,97032,97004,86575,1,2,4,8,10])). % 266.52/266.94 cnf(97227,plain, % 266.52/266.94 (P2(f3(f4(a1,a11,a11,a2),f4(a1,f4(a1,f4(a1,f4(a1,f10(a9),a11,a2),a11,a2),a11,a2),f4(a1,a11,a11,a2),a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[97221,11,1,86889,4,8,10])). % 266.52/266.94 cnf(97231,plain, % 266.52/266.94 (P2(f3(a7,f4(a1,f4(a1,f4(a1,f10(a9),a11,a2),a11,a2),a11,a2),a2,a2),f5(f5(a1,a2),a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[97221,11,1,86889,4,8,10,86541,86553])). % 266.52/266.94 cnf(97233,plain, % 266.52/266.94 (P2(f3(f4(a1,a11,a11,a2),f4(a1,f4(a1,f4(a1,f4(a1,f10(a9),a11,a2),a11,a2),a11,a2),f4(a1,a11,a11,a2),a2),a2,a2),f5(f5(a1,a2),a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[97227,4])). % 266.52/266.94 cnf(97249,plain, % 266.52/266.94 (P2(f3(a11,f4(a1,f4(a1,a11,a11,a2),a11,a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[87274,86510,86591,86558,44,4,5,86544])). % 266.52/266.94 cnf(97251,plain, % 266.52/266.94 (~P2(f3(f4(a1,f4(a1,a11,a11,a2),f4(a1,a11,a11,a2),a2),a9,a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[87274,87240,86510,86595,86591,86558,44,4,5,86544,8])). % 266.52/266.94 cnf(97253,plain, % 266.52/266.94 (P2(f3(a11,f4(a1,f10(a9),a11,a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[2,87274,87240,86510,1,86495,86595,86591,86558,44,4,5,86544,8,10])). % 266.52/266.94 cnf(97259,plain, % 266.52/266.94 (P2(f3(a11,f4(a1,f4(a1,f10(f10(a9)),a11,a2),f4(a1,a11,a11,a2),a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[87274,86510,96949,44,4,86544])). % 266.52/266.94 cnf(97267,plain, % 266.52/266.94 (P2(f3(a11,f4(a1,f4(a1,f4(a1,f4(a1,f4(a1,f4(a1,a11,a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,f4(a1,f4(a1,a11,a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[86510,97193,44,86544])). % 266.52/266.94 cnf(97273,plain, % 266.52/266.94 (P2(f3(f4(a1,a11,a11,a2),f4(a1,f4(a1,f4(a1,f4(a1,a11,a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[87274,86510,86493,1,11,97101,97193,97144,44,86544,4,8,10])). % 266.52/266.94 cnf(97283,plain, % 266.52/266.94 (P2(f3(f4(a1,a11,a11,a2),f4(a1,f4(a1,f4(a1,f4(a1,f4(a1,f4(a1,f4(a1,a11,a11,a2),a11,a2),a11,a2),a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[87274,86510,86493,1,11,97203,97227,97116,44,4,86544,8,10])). % 266.52/266.94 cnf(97288,plain, % 266.52/266.94 (P2(f3(a11,f4(a1,f4(a1,f4(a1,f4(a1,a11,a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[86510,97273,44,86544])). % 266.52/266.94 cnf(97292,plain, % 266.52/266.94 (~P2(f3(f4(a1,f4(a1,f4(a1,f4(a1,a11,a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),f10(a9),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[87274,86510,97142,97107,97273,44,86544,4,8])). % 266.52/266.94 cnf(97294,plain, % 266.52/266.94 (P2(f3(f4(a1,a11,a11,a2),f4(a1,f4(a1,f4(a1,f4(a1,f4(a1,f10(a9),a11,a2),a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[87274,86510,1,11,97142,97044,97107,97273,44,86544,4,8,10])). % 266.52/266.94 cnf(97304,plain, % 266.52/266.94 (P2(f3(a11,f4(a1,f4(a1,f4(a1,a11,a11,a2),a11,a2),a11,a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[2,87274,86510,86493,1,96933,97191,97283,44,4,86544,8,10])). % 266.52/266.94 cnf(97308,plain, % 266.52/266.94 (P2(f3(a11,f4(a1,f4(a1,f4(a1,f4(a1,f4(a1,f10(a9),a11,a2),a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[86510,97294,44,86544])). % 266.52/266.94 cnf(97332,plain, % 266.52/266.94 (P2(f3(a11,f4(a1,f4(a1,f4(a1,a11,a11,a2),a11,a2),f4(a1,a11,a11,a2),a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[87274,86510,1,11,97093,97251,97249,44,4,8,10,86544])). % 266.52/266.94 cnf(97340,plain, % 266.52/266.94 (P2(f3(f4(a1,a11,a11,a2),f4(a1,f4(a1,f10(a9),a11,a2),f4(a1,a11,a11,a2),a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[87274,86510,86493,1,11,97292,97253,44,4,8,10])). % 266.52/266.94 cnf(97342,plain, % 266.52/266.94 (P2(f3(a11,f4(a1,f4(a1,f10(a9),a11,a2),f4(a1,a11,a11,a2),a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[87274,86510,86493,1,11,97292,97253,44,4,8,10,86544])). % 266.52/266.94 cnf(97358,plain, % 266.52/266.94 (P2(f3(f4(a1,a11,a11,a2),f4(a1,f4(a1,f4(a1,f10(f10(a9)),a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[87274,86510,86493,1,11,97259,97128,44,4,8,10])). % 266.52/266.94 cnf(97368,plain, % 266.52/266.94 (P2(f3(f4(a1,a11,a11,a2),f4(a1,f4(a1,f4(a1,f4(a1,f4(a1,f4(a1,f4(a1,a11,a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,f4(a1,f4(a1,a11,a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[87274,86510,86493,1,11,97267,97071,44,4,8,10])). % 266.52/266.94 cnf(97386,plain, % 266.52/266.94 (P2(f3(f4(a1,a11,a11,a2),f4(a1,f4(a1,f4(a1,f4(a1,f4(a1,a11,a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[87274,86510,1,11,97288,44,4,10])). % 266.52/266.94 cnf(97402,plain, % 266.52/266.94 (P2(f3(a11,f4(a1,f4(a1,f4(a1,f4(a1,f4(a1,f4(a1,f10(a9),a11,a2),a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[87274,86510,1,11,97308,44,4,10,86544])). % 266.52/266.94 cnf(97412,plain, % 266.52/266.94 (P2(f3(f4(a1,a11,a11,a2),f4(a1,f4(a1,f4(a1,f4(a1,a11,a11,a2),a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[87274,86510,1,11,97332,44,4,10])). % 266.52/266.94 cnf(97414,plain, % 266.52/266.94 (P2(f3(a11,f4(a1,f4(a1,f4(a1,f4(a1,a11,a11,a2),a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[87274,86510,1,11,97332,44,4,10,86544])). % 266.52/266.94 cnf(97424,plain, % 266.52/266.94 (P2(f3(f4(a1,a11,a11,a2),f4(a1,f4(a1,f4(a1,f10(a9),a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[87274,86510,1,11,97342,44,4,10])). % 266.52/266.94 cnf(97426,plain, % 266.52/266.94 (P2(f3(a11,f4(a1,f4(a1,f4(a1,f10(a9),a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[87274,86510,1,11,97342,44,4,10,86544])). % 266.52/266.94 cnf(97438,plain, % 266.52/266.94 (P2(f3(a11,f4(a1,f4(a1,f4(a1,f4(a1,a11,a11,a2),a11,a2),a11,a2),f4(a1,a11,a11,a2),a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[87274,86510,1,11,97304,44,4,10,86544])). % 266.52/266.94 cnf(97501,plain, % 266.52/266.94 (P2(f3(f4(a1,a11,a11,a2),f4(a1,f4(a1,f4(a1,f4(a1,f4(a1,f4(a1,f4(a1,f10(a9),a11,a2),a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[87274,86510,1,11,97402,44,4,10])). % 266.52/266.94 cnf(97513,plain, % 266.52/266.94 (P2(f3(f4(a1,a11,a11,a2),f4(a1,f4(a1,f4(a1,f4(a1,f4(a1,a11,a11,a2),a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[87274,86510,1,11,97414,44,4,10])). % 266.52/266.94 cnf(97515,plain, % 266.52/266.94 (P2(f3(a11,f4(a1,f4(a1,f4(a1,f4(a1,f4(a1,a11,a11,a2),a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[87274,86510,1,11,97414,44,4,10,86544])). % 266.52/266.94 cnf(97523,plain, % 266.52/266.94 (P2(f3(f4(a1,a11,a11,a2),f4(a1,f4(a1,f4(a1,f4(a1,f10(a9),a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.94 inference(scs_inference,[],[87274,86510,1,11,97426,4,44,10])). % 266.52/266.94 cnf(97525,plain, % 266.52/266.95 (P2(f3(a11,f4(a1,f4(a1,f4(a1,f4(a1,f10(a9),a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.95 inference(scs_inference,[],[87274,86510,1,11,97426,4,44,10,86544])). % 266.52/266.95 cnf(97545,plain, % 266.52/266.95 (P2(f3(f4(a1,a11,a11,a2),f4(a1,f4(a1,f4(a1,f4(a1,f4(a1,a11,a11,a2),a11,a2),a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.95 inference(scs_inference,[],[87274,86510,1,11,97438,4,44,10])). % 266.52/266.95 cnf(97547,plain, % 266.52/266.95 (P2(f3(a11,f4(a1,f4(a1,f4(a1,f4(a1,f4(a1,a11,a11,a2),a11,a2),a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.95 inference(scs_inference,[],[87274,86510,1,11,97438,4,44,10,86544])). % 266.52/266.95 cnf(97620,plain, % 266.52/266.95 (P2(f3(a11,f4(a1,f4(a1,f4(a1,f4(a1,f4(a1,f4(a1,a11,a11,a2),a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.95 inference(scs_inference,[],[87274,86510,1,11,97515,4,44,10,86544])). % 266.52/266.95 cnf(97630,plain, % 266.52/266.95 (P2(f3(f4(a1,a11,a11,a2),f4(a1,f4(a1,f4(a1,f4(a1,f4(a1,f10(a9),a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.95 inference(scs_inference,[],[87274,86510,1,11,97525,44,4,10])). % 266.52/266.95 cnf(97650,plain, % 266.52/266.95 (P2(f3(f4(a1,a11,a11,a2),f4(a1,f4(a1,f4(a1,f4(a1,f4(a1,f4(a1,a11,a11,a2),a11,a2),a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.95 inference(scs_inference,[],[87274,86510,1,11,97547,44,4,10])). % 266.52/266.95 cnf(97696,plain, % 266.52/266.95 (P2(f3(a11,f4(a1,f4(a1,f4(a1,f4(a1,f4(a1,f4(a1,f4(a1,a11,a11,a2),a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.95 inference(scs_inference,[],[87274,86510,1,11,97620,4,44,10,86544])). % 266.52/266.95 cnf(97744,plain, % 266.52/266.95 (P2(f3(a11,f4(a1,f4(a1,f4(a1,f4(a1,f4(a1,f4(a1,f4(a1,f4(a1,a11,a11,a2),a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.95 inference(scs_inference,[],[87274,86510,1,11,97696,4,44,10,86544])). % 266.52/266.95 cnf(97777,plain, % 266.52/266.95 (P2(f3(a11,f4(a1,f4(a1,f4(a1,f4(a1,f4(a1,f4(a1,f4(a1,f4(a1,f4(a1,a11,a11,a2),a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.95 inference(scs_inference,[],[87274,86510,1,11,97744,4,44,10,86544])). % 266.52/266.95 cnf(97801,plain, % 266.52/266.95 (P2(f3(a11,f4(a1,f4(a1,f4(a1,f4(a1,f4(a1,f4(a1,f4(a1,f4(a1,f4(a1,f4(a1,a11,a11,a2),a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.95 inference(scs_inference,[],[87274,86510,1,11,97777,4,44,10,86544])). % 266.52/266.95 cnf(98806,plain, % 266.52/266.95 (P2(f3(f4(a1,a11,a11,a2),f4(a1,f4(a1,a11,a11,a2),a11,a2),a2,a2),a1,f6(a2,a2))), % 266.52/266.95 inference(scs_inference,[],[2,87274,86510,86518,1,4,44,9])). % 266.52/266.95 cnf(98808,plain, % 266.52/266.95 (P2(f3(f4(a1,f4(a1,a11,a11,a2),a11,a2),f4(a1,f4(a1,f4(a1,a11,a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,f4(a1,a11,a11,a2),a11,a2),a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.95 inference(scs_inference,[],[2,87274,86510,86518,1,4,44,9,96921])). % 266.52/266.95 cnf(98818,plain, % 266.52/266.95 (P2(f3(f4(a1,a11,a11,a2),f4(a1,f4(a1,a11,a11,a2),f4(a1,a11,a11,a2),a2),a2,a2),a1,f6(a2,a2))), % 266.52/266.95 inference(scs_inference,[],[87274,86510,86497,1,11,96949,98806,4,44,10,9])). % 266.52/266.95 cnf(98828,plain, % 266.52/266.95 (P2(f3(f10(a9),f4(a1,f10(a9),a11,a2),a2,a2),a1,f6(a2,a2))), % 266.52/266.95 inference(scs_inference,[],[2,87274,86510,1,86495,86591,98806,4,44,10,9])). % 266.52/266.95 cnf(98834,plain, % 266.52/266.95 (P2(f3(f4(a1,f10(a9),a11,a2),f4(a1,f4(a1,f10(a9),a11,a2),f4(a1,f10(a9),a11,a2),a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.95 inference(scs_inference,[],[87274,86510,1,86593,98828,4,44,10])). % 266.52/266.95 cnf(98903,plain, % 266.52/266.95 (P2(f3(f4(a1,f4(a1,a11,a11,a2),a11,a2),f4(a1,f4(a1,f4(a1,f4(a1,f4(a1,a11,a11,a2),a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,f4(a1,a11,a11,a2),a11,a2),a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.95 inference(scs_inference,[],[87274,86510,1,98806,97412,4,44,10])). % 266.52/266.95 cnf(98929,plain, % 266.52/266.95 (P2(f3(f4(a1,f4(a1,f10(a9),a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,f4(a1,f4(a1,f10(a9),a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),a2,a2),a1,f6(a2,a2))), % 266.52/266.95 inference(scs_inference,[],[87274,86510,1,11,98806,97342,97513,4,44,10,9])). % 266.52/266.95 cnf(98999,plain, % 266.52/266.95 (P2(f3(f4(a1,f4(a1,f10(a9),a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,f4(a1,f4(a1,f10(a9),a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,f4(a1,a11,a11,a2),a11,a2),a2),a2,a2),a1,f6(a2,a2))), % 266.52/266.95 inference(scs_inference,[],[87274,86510,1,98806,97340,4,44,9])). % 266.52/266.95 cnf(105269,plain, % 266.52/266.95 (P2(f3(a7,x1052691,a2,a2),f5(f5(a1,a2),a2),f6(a2,a2))+~P2(f3(f4(a1,a11,a11,a2),x1052691,a2,a2),f5(f5(a1,a2),a2),f6(a2,a2))), % 266.52/266.95 inference(scs_inference,[],[86575,86510,44,8])). % 266.52/266.95 cnf(105279,plain, % 266.52/266.95 (P2(f3(a11,x1052791,a2,a2),f5(f5(a1,a2),a2),f6(a2,a2))+~P2(f3(f4(a1,a11,a11,a2),x1052791,a2,a2),f5(f5(a1,a2),a2),f6(a2,a2))), % 266.52/266.95 inference(scs_inference,[],[86588,86510,44,8])). % 266.52/266.95 cnf(105300,plain, % 266.52/266.95 (P2(f3(a9,x1053001,a2,a2),f5(f5(a1,a2),a2),f6(a2,a2))+~P2(f3(f10(a9),x1053001,a2,a2),f5(f5(a1,a2),a2),f6(a2,a2))), % 266.52/266.95 inference(scs_inference,[],[86510,50,44,8])). % 266.52/266.95 cnf(126213,plain, % 266.52/266.95 (P2(f3(a11,f4(a1,f4(a1,f4(a1,f4(a1,f4(a1,f4(a1,a11,a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,f4(a1,f4(a1,a11,a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),a2,a2),f5(f5(a1,a2),a2),f6(a2,a2))), % 266.52/266.95 inference(scs_inference,[],[97205,86586,105300,105279])). % 266.52/266.95 cnf(126251,plain, % 266.52/266.95 (P2(f3(a7,f10(f4(a1,f10(a9),a11,a2)),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.95 inference(scs_inference,[],[86510,24,86896,86591,86595,86558,86593,96949,96998,98834,97205,86586,97128,97233,98818,105300,105279,105269,97024,96935,87251,87261,86658,86637,86632,86526,18414,86506,7,6,86520,4,44,8,97064,5])). % 266.52/266.95 cnf(126420,plain, % 266.52/266.95 (P2(f3(a11,f4(a1,f4(a1,f4(a1,f4(a1,a11,a11,a2),a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),a2,a2),f5(f5(a1,a2),a2),f6(a2,a2))), % 266.52/266.95 inference(scs_inference,[],[97386,97412,97124,97424,7,87261,86526,87251,86658,86637])). % 266.52/266.95 cnf(126466,plain, % 266.52/266.95 (~P2(f3(a9,f4(a1,f10(a9),a11,a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.95 inference(scs_inference,[],[97253,97523,86658,7])). % 266.52/266.95 cnf(126492,plain, % 266.52/266.95 (P2(f3(a11,f4(a1,f4(a1,f4(a1,f4(a1,f10(a9),a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),a2,a2),f5(f5(a1,a2),a2),f6(a2,a2))), % 266.52/266.95 inference(scs_inference,[],[97513,97523,97259,97358,97368,86526,87251,86658,7,87261,86637])). % 266.52/266.95 cnf(133462,plain, % 266.52/266.95 (P2(f3(a11,f4(a1,f4(a1,f4(a1,f4(a1,f4(a1,f4(a1,f4(a1,f10(a9),a11,a2),a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),a2,a2),f5(f5(a1,a2),a2),f6(a2,a2))), % 266.52/266.95 inference(scs_inference,[],[97501,97525,97545,87261,7,86637])). % 266.52/266.95 cnf(133623,plain, % 266.52/266.95 (P2(f3(a11,f4(a1,f4(a1,f4(a1,f4(a1,f4(a1,f10(a9),a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),a2,a2),f5(f5(a1,a2),a2),f6(a2,a2))), % 266.52/266.95 inference(scs_inference,[],[97630,97650,87261,86637])). % 266.52/266.95 cnf(134152,plain, % 266.52/266.95 (P2(f3(a11,f4(a1,f10(f4(a1,f10(a9),a11,a2)),a11,a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.95 inference(scs_inference,[],[2,97231,98808,126213,126251,97249,1,98806,86688,97046,4,8,10])). % 266.52/266.95 cnf(134244,plain, % 266.52/266.95 (P2(f3(f4(a1,f4(a1,a11,a11,a2),a11,a2),f4(a1,f4(a1,f4(a1,f4(a1,f4(a1,a11,a11,a2),a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,f4(a1,a11,a11,a2),a11,a2),a2),a2,a2),f5(f5(a1,a2),a2),f6(a2,a2))), % 266.52/266.95 inference(scs_inference,[],[98903,126420,86688,4])). % 266.52/266.95 cnf(134284,plain, % 266.52/266.95 (P2(f3(f4(a1,f4(a1,f10(a9),a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,f4(a1,f4(a1,f10(a9),a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.95 inference(scs_inference,[],[98929,126492,86688,4])). % 266.52/266.95 cnf(134370,plain, % 266.52/266.95 (P2(f3(f4(a1,f4(a1,f10(a9),a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,f4(a1,f4(a1,f10(a9),a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,f4(a1,a11,a11,a2),a11,a2),a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.95 inference(scs_inference,[],[98999,133462,86688,4])). % 266.52/266.95 cnf(134374,plain, % 266.52/266.95 (P2(f3(f4(a1,f4(a1,f4(a1,f10(a9),a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,f4(a1,a11,a11,a2),a11,a2),a2),f4(a1,f4(a1,f4(a1,f4(a1,f10(a9),a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,f4(a1,f4(a1,f10(a9),a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,f4(a1,a11,a11,a2),a11,a2),a2),a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.95 inference(scs_inference,[],[98999,133462,134244,134284,96913,1,86688,4,8,10])). % 266.52/266.95 cnf(134453,plain, % 266.52/266.95 (P2(f3(f4(a1,a11,a11,a2),f4(a1,f4(a1,f4(a1,f4(a1,f4(a1,f4(a1,f4(a1,f4(a1,f4(a1,f4(a1,f4(a1,a11,a11,a2),a11,a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),f4(a1,a11,a11,a2),a2),a2,a2),f5(a1,a2),f6(a2,a2))), % 266.52/266.95 inference(scs_inference,[],[11,97801,133623,134370,134374,1,86688,4,8,10])). % 266.52/266.95 cnf(135619,plain, % 266.52/266.95 ($false), % 266.52/266.95 inference(scs_inference,[],[86510,24,86493,86593,134453,134152,126466,86658,86544,86637,7,4,44,8]), % 266.52/266.95 ['proof']). % 266.71/267.08 % SZS output end Proof % 266.71/267.08 % Total time :265.700000s %------------------------------------------------------------------------------