%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : HWV006-1 : TPTP v8.2.0. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n021.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 07:29:05 EDT 2024
% Result : Unsatisfiable 241.74s 241.75s
% Output : CNFRefutation 242.57s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : HWV006-1 : TPTP v8.2.0. Released v2.1.0.
% 0.06/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n021.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 : Fri Jun 21 01:49:24 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.52/0.56 start to proof:theBenchmark
% 241.68/241.71 %-------------------------------------------
% 241.68/241.71 % File :CSE---1.7
% 241.68/241.71 % Problem :theBenchmark
% 241.68/241.71 % Transform :cnf
% 241.68/241.71 % Format :tptp:raw
% 241.68/241.71 % Command :java -jar mcs_scs.jar %d %s
% 241.68/241.71
% 241.68/241.71 % Result :Theorem 241.060000s
% 241.68/241.71 % Output :CNFRefutation 241.060000s
% 241.68/241.71 %-------------------------------------------
% 241.74/241.75 %--------------------------------------------------------------------------
% 241.74/241.75 % File : HWV006-1 : TPTP v8.2.0. Released v2.1.0.
% 241.74/241.75 % Domain : Hardware Verification
% 241.74/241.75 % Problem : A fulladder built from two halfadders and an or gate
% 241.74/241.75 % Version : [Gei96] axioms.
% 241.74/241.75 % English :
% 241.74/241.75
% 241.74/241.75 % Refs : [Gei96] Geisler (1996), Email to G. Sutcliffe
% 241.74/241.75 % Source : [Gei96]
% 241.74/241.75 % Names :
% 241.74/241.75
% 241.74/241.75 % Status : Unsatisfiable
% 241.74/241.75 % Rating : 0.08 v8.2.0, 0.14 v8.1.0, 0.00 v7.0.0, 0.25 v6.3.0, 0.29 v6.2.0, 0.11 v6.1.0, 0.00 v6.0.0, 0.14 v5.5.0, 0.12 v5.4.0, 0.20 v5.3.0, 0.10 v5.1.0, 0.09 v5.0.0, 0.21 v4.1.0, 0.25 v4.0.1, 0.20 v4.0.0, 0.14 v3.4.0, 0.25 v3.3.0, 0.00 v2.7.0, 0.12 v2.6.0, 0.33 v2.5.0, 0.40 v2.4.0, 0.20 v2.3.0, 0.33 v2.2.1, 0.33 v2.1.0
% 241.74/241.75 % Syntax : Number of clauses : 58 ( 13 unt; 3 nHn; 58 RR)
% 241.74/241.75 % Number of literals : 139 ( 0 equ; 88 neg)
% 241.74/241.75 % Maximal clause size : 5 ( 2 avg)
% 241.74/241.75 % Maximal term depth : 3 ( 1 avg)
% 241.74/241.75 % Number of predicates : 5 ( 5 usr; 0 prp; 2-2 aty)
% 241.74/241.75 % Number of functors : 21 ( 21 usr; 13 con; 0-2 aty)
% 241.74/241.75 % Number of variables : 52 ( 3 sgn)
% 241.74/241.75 % SPC : CNF_UNS_RFO_NEQ_NHN
% 241.74/241.75
% 241.74/241.75 % Comments :
% 241.74/241.75 %--------------------------------------------------------------------------
% 241.74/241.75 %----Include basic diagnosis axioms
% 241.74/241.75 include('Axioms/HWV001-0.ax').
% 241.74/241.75 %----Include model of halfadder
% 241.74/241.75 include('Axioms/HWV001-1.ax').
% 241.74/241.75 %----Include model of fulladder
% 241.74/241.75 include('Axioms/HWV001-2.ax').
% 241.74/241.75 %--------------------------------------------------------------------------
% 241.74/241.75 %----Observations
% 241.74/241.75 cnf(f_isa_fulladder,hypothesis,
% 241.74/241.75 type(f,fulladder) ).
% 241.74/241.75
% 241.74/241.75 cnf(in1_1,hypothesis,
% 241.74/241.75 value(in(n1,f),n1) ).
% 241.74/241.75
% 241.74/241.75 cnf(in2_0,hypothesis,
% 241.74/241.75 value(in(n2,f),n0) ).
% 241.74/241.75
% 241.74/241.75 cnf(inc_1,hypothesis,
% 241.74/241.75 value(in(c,f),n1) ).
% 241.74/241.75
% 241.74/241.75 cnf(outs_1,hypothesis,
% 241.74/241.75 value(out(s,f),n1) ).
% 241.74/241.75
% 241.74/241.75 cnf(outc_0,hypothesis,
% 241.74/241.75 value(out(c,f),n0) ).
% 241.74/241.75
% 241.74/241.75 %----Minimal diagnosis
% 241.74/241.75 cnf(diagnosis_or1_not1h2,negated_conjecture,
% 241.74/241.75 ( ~ mode(or1(f),abnormal)
% 241.74/241.75 | ~ mode(not1(h2(f)),abnormal) ) ).
% 241.74/241.75
% 241.74/241.75 cnf(diagnosis_and2,negated_conjecture,
% 241.74/241.75 ~ mode(and2(h2(f)),abnormal) ).
% 241.74/241.75
% 241.74/241.75 cnf(diagnosis_or1_and1h2,negated_conjecture,
% 241.74/241.75 ( ~ mode(or1(f),abnormal)
% 241.74/241.75 | ~ mode(and1(h2(f)),abnormal) ) ).
% 241.74/241.75
% 241.74/241.75 cnf(diagnosis_or1h1,negated_conjecture,
% 241.74/241.75 ~ mode(or1(h1(f)),abnormal) ).
% 241.74/241.75
% 241.74/241.75 cnf(diagnosis_not1h1,negated_conjecture,
% 241.74/241.75 ~ mode(not1(h1(f)),abnormal) ).
% 241.74/241.75
% 241.74/241.75 cnf(diagnosis_and2h1,negated_conjecture,
% 241.74/241.75 ~ mode(and2(h1(f)),abnormal) ).
% 241.74/241.75
% 241.74/241.75 cnf(diagnosis_and1h1,negated_conjecture,
% 241.74/241.75 ~ mode(and1(h1(f)),abnormal) ).
% 241.74/241.75
% 241.74/241.75 %--------------------------------------------------------------------------
% 241.74/241.75 %-------------------------------------------
% 241.74/241.75 % Proof found
% 241.74/241.75 % SZS status Theorem for theBenchmark
% 241.74/241.75 % SZS output start Proof
% 241.78/241.79 %ClaNum:58(EqnAxiom:0)
% 241.78/241.79 %VarNum:151(SingletonVarNum:52)
% 241.78/241.79 %MaxLitNum:5
% 241.78/241.79 %MaxfuncDepth:2
% 241.78/241.79 %SharedTerms:44
% 241.78/241.79 %goalClause: 9 10 11 12 13 26 27
% 241.78/241.79 %singleGoalClaCount:5
% 241.78/241.79 [1]P1(a1,a7)
% 241.78/241.79 [7]~P2(a13,a8)
% 241.78/241.79 [8]~P2(a8,a13)
% 241.78/241.79 [2]P5(f9(a8,a1),a8)
% 241.78/241.79 [3]P5(f9(a14,a1),a13)
% 241.78/241.79 [4]P5(f9(a2,a1),a8)
% 241.78/241.79 [5]P5(f16(a15,a1),a8)
% 241.78/241.79 [6]P5(f16(a2,a1),a13)
% 241.78/241.79 [9]~P4(f3(f10(a1)),a4)
% 241.78/241.79 [10]~P4(f6(f10(a1)),a4)
% 241.78/241.79 [11]~P4(f6(f11(a1)),a4)
% 241.78/241.79 [12]~P4(f17(f10(a1)),a4)
% 241.78/241.79 [13]~P4(f19(f10(a1)),a4)
% 241.78/241.79 [26]~P4(f19(a1),a4)+~P4(f3(f11(a1)),a4)
% 241.78/241.79 [27]~P4(f19(a1),a4)+~P4(f17(f11(a1)),a4)
% 241.78/241.79 [21]~P4(x211,a4)+~P4(x211,a21)
% 241.78/241.79 [14]~P1(x141,a12)+P1(f3(x141),a5)
% 241.78/241.79 [15]~P1(x151,a12)+P1(f6(x151),a5)
% 241.78/241.79 [16]~P1(x161,a12)+P1(f17(x161),a18)
% 241.78/241.79 [17]~P1(x171,a12)+P1(f19(x171),a20)
% 241.78/241.79 [18]~P1(x181,a7)+P1(f19(x181),a20)
% 241.78/241.79 [19]~P1(x191,a7)+P1(f10(x191),a12)
% 241.78/241.79 [20]~P1(x201,a7)+P1(f11(x201),a12)
% 241.78/241.79 [28]~P1(x281,a12)+P3(f9(a8,x281),f9(a8,f6(x281)))
% 241.78/241.79 [29]~P1(x291,a12)+P3(f9(a8,x291),f9(a8,f19(x291)))
% 241.78/241.79 [30]~P1(x301,a7)+P3(f9(a8,x301),f9(a8,f11(x301)))
% 241.78/241.79 [31]~P1(x311,a7)+P3(f9(a14,x311),f9(a8,f10(x311)))
% 241.78/241.79 [32]~P1(x321,a12)+P3(f9(a14,x321),f9(a14,f6(x321)))
% 241.78/241.79 [33]~P1(x331,a12)+P3(f9(a14,x331),f9(a14,f19(x331)))
% 241.78/241.79 [34]~P1(x341,a7)+P3(f9(a2,x341),f9(a14,f10(x341)))
% 241.78/241.79 [35]~P1(x351,a12)+P3(f16(a15,x351),f16(a8,f3(x351)))
% 241.78/241.79 [36]~P1(x361,a7)+P3(f16(a15,x361),f16(a15,f11(x361)))
% 241.78/241.79 [37]~P1(x371,a12)+P3(f16(a2,x371),f16(a8,f6(x371)))
% 241.78/241.79 [38]~P1(x381,a7)+P3(f16(a2,x381),f16(a8,f19(x381)))
% 241.78/241.79 [39]~P1(x391,a12)+P3(f16(a8,f6(x391)),f9(a8,f17(x391)))
% 241.78/241.79 [40]~P1(x401,a12)+P3(f16(a8,f17(x401)),f9(a14,f3(x401)))
% 241.78/241.79 [41]~P1(x411,a12)+P3(f16(a8,f19(x411)),f9(a8,f3(x411)))
% 241.78/241.79 [42]~P1(x421,a7)+P3(f16(a15,f10(x421)),f9(a14,f11(x421)))
% 241.78/241.79 [43]~P1(x431,a7)+P3(f16(a2,f10(x431)),f9(a14,f19(x431)))
% 241.78/241.79 [44]~P1(x441,a7)+P3(f16(a2,f11(x441)),f9(a8,f19(x441)))
% 241.78/241.79 [22]~P1(x221,x222)+P4(x221,a4)+P4(x221,a21)
% 241.78/241.79 [23]~P5(x233,x232)+P5(x231,x232)+~P3(x233,x231)
% 241.78/241.79 [24]~P5(x243,x242)+P5(x241,x242)+~P3(x241,x243)
% 241.78/241.79 [25]~P5(x253,x251)+P2(x251,x252)+~P5(x253,x252)
% 241.78/241.79 [45]~P4(x451,a21)+~P1(x451,a20)+~P5(f16(a8,x451),a13)+P5(f9(a8,x451),a13)
% 241.78/241.79 [46]~P4(x461,a21)+~P1(x461,a18)+~P5(f16(a8,x461),a8)+P5(f9(a8,x461),a13)
% 241.78/241.79 [47]~P4(x471,a21)+~P1(x471,a5)+~P5(f16(a8,x471),a8)+P5(f9(a8,x471),a8)
% 241.78/241.79 [48]~P4(x481,a21)+~P1(x481,a18)+~P5(f16(a8,x481),a13)+P5(f9(a8,x481),a8)
% 241.78/241.79 [49]~P4(x491,a21)+~P1(x491,a20)+~P5(f16(a8,x491),a13)+P5(f9(a14,x491),a13)
% 241.78/241.79 [50]~P4(x501,a21)+~P1(x501,a5)+~P5(f16(a8,x501),a8)+P5(f9(a14,x501),a8)
% 241.78/241.79 [51]~P4(x511,a21)+~P1(x511,a18)+~P5(f9(a8,x511),a8)+P5(f16(a8,x511),a13)
% 241.78/241.79 [52]~P4(x521,a21)+~P1(x521,a18)+~P5(f9(a8,x521),a13)+P5(f16(a8,x521),a8)
% 241.78/241.79 [53]~P4(x531,a21)+~P1(x531,a5)+~P5(f9(x532,x531),a13)+P5(f16(a8,x531),a13)
% 241.78/241.79 [54]~P4(x541,a21)+~P1(x541,a20)+~P5(f9(x542,x541),a8)+P5(f16(a8,x541),a8)
% 241.78/241.79 [55]~P4(x551,a21)+~P1(x551,a5)+P5(f9(a14,x551),a13)+~P5(f16(a8,x551),a13)+P5(f9(a8,x551),a13)
% 241.78/241.79 [56]~P4(x561,a21)+~P1(x561,a20)+P5(f9(a14,x561),a8)+~P5(f16(a8,x561),a8)+P5(f9(a8,x561),a8)
% 241.78/241.79 [57]~P4(x571,a21)+~P1(x571,a20)+~P5(f9(a8,x571),a13)+~P5(f9(a14,x571),a13)+P5(f16(a8,x571),a13)
% 241.78/241.79 [58]~P4(x581,a21)+~P1(x581,a5)+~P5(f9(a8,x581),a8)+~P5(f9(a14,x581),a8)+P5(f16(a8,x581),a8)
% 241.78/241.79 %EqnAxiom
% 241.78/241.79
% 241.78/241.79 %-------------------------------------------
% 242.18/242.18 cnf(61,plain,
% 242.18/242.18 (~P1(f3(f10(a1)),x611)+P4(f3(f10(a1)),a21)),
% 242.18/242.18 inference(scs_inference,[],[9,2,25,22])).
% 242.18/242.18 cnf(66,plain,
% 242.18/242.18 (~P1(f6(f10(a1)),x661)+P4(f6(f10(a1)),a21)),
% 242.18/242.18 inference(scs_inference,[],[10,3,25,22])).
% 242.18/242.18 cnf(71,plain,
% 242.18/242.18 (~P1(f6(f11(a1)),x711)+P4(f6(f11(a1)),a21)),
% 242.18/242.18 inference(scs_inference,[],[11,4,25,22])).
% 242.18/242.18 cnf(76,plain,
% 242.18/242.18 (~P1(f17(f10(a1)),x761)+P4(f17(f10(a1)),a21)),
% 242.18/242.18 inference(scs_inference,[],[12,5,25,22])).
% 242.18/242.18 cnf(81,plain,
% 242.18/242.18 (~P1(f19(f10(a1)),x811)+P4(f19(f10(a1)),a21)),
% 242.18/242.18 inference(scs_inference,[],[13,6,25,22])).
% 242.18/242.18 cnf(208,plain,
% 242.18/242.18 (P1(f3(f10(a1)),a5)),
% 242.18/242.18 inference(scs_inference,[],[1,14,19])).
% 242.18/242.18 cnf(209,plain,
% 242.18/242.18 (P4(f3(f10(a1)),a21)),
% 242.18/242.18 inference(scs_inference,[],[208,61])).
% 242.18/242.18 cnf(252,plain,
% 242.18/242.18 (P1(f6(f11(a1)),a5)),
% 242.18/242.18 inference(scs_inference,[],[1,15,20])).
% 242.18/242.18 cnf(253,plain,
% 242.18/242.18 (P4(f6(f11(a1)),a21)),
% 242.18/242.18 inference(scs_inference,[],[252,71])).
% 242.18/242.18 cnf(296,plain,
% 242.18/242.18 (P1(f17(f10(a1)),a18)),
% 242.18/242.18 inference(scs_inference,[],[1,16,19])).
% 242.18/242.18 cnf(297,plain,
% 242.18/242.18 (P4(f17(f10(a1)),a21)),
% 242.18/242.18 inference(scs_inference,[],[296,76])).
% 242.18/242.18 cnf(432,plain,
% 242.18/242.18 (~P1(f19(a1),x4321)+P4(f19(a1),a21)+~P4(f3(f11(a1)),a4)),
% 242.18/242.18 inference(scs_inference,[],[26,22])).
% 242.18/242.18 cnf(478,plain,
% 242.18/242.18 (~P1(f19(a1),x4781)+P4(f19(a1),a21)+~P4(f17(f11(a1)),a4)),
% 242.18/242.18 inference(scs_inference,[],[27,22])).
% 242.18/242.18 cnf(524,plain,
% 242.18/242.18 (P4(f6(f10(a1)),a21)+~P1(f10(a1),a12)),
% 242.18/242.18 inference(scs_inference,[],[66,15])).
% 242.18/242.18 cnf(570,plain,
% 242.18/242.18 (P4(f6(f10(a1)),a21)),
% 242.18/242.18 inference(scs_inference,[],[1,524,19])).
% 242.18/242.18 cnf(616,plain,
% 242.18/242.18 (P3(f9(a8,f11(a1)),f9(a8,f6(f11(a1))))),
% 242.18/242.18 inference(scs_inference,[],[1,28,20])).
% 242.18/242.18 cnf(662,plain,
% 242.18/242.18 (P3(f9(a8,f10(a1)),f9(a8,f19(f10(a1))))),
% 242.18/242.18 inference(scs_inference,[],[1,29,19])).
% 242.18/242.18 cnf(708,plain,
% 242.18/242.18 (P5(f9(a8,f11(a1)),a8)),
% 242.18/242.18 inference(scs_inference,[],[1,2,30,23])).
% 242.18/242.18 cnf(754,plain,
% 242.18/242.18 (P5(f9(a8,f10(a1)),a13)),
% 242.18/242.18 inference(scs_inference,[],[1,3,31,23])).
% 242.18/242.18 cnf(800,plain,
% 242.18/242.18 (P3(f9(a14,f11(a1)),f9(a14,f6(f11(a1))))),
% 242.18/242.18 inference(scs_inference,[],[1,32,20])).
% 242.18/242.18 cnf(846,plain,
% 242.18/242.18 (P3(f9(a14,f10(a1)),f9(a14,f19(f10(a1))))),
% 242.18/242.18 inference(scs_inference,[],[1,33,19])).
% 242.18/242.18 cnf(892,plain,
% 242.18/242.18 (P5(f9(a14,f10(a1)),a8)),
% 242.18/242.18 inference(scs_inference,[],[1,4,34,23])).
% 242.18/242.18 cnf(938,plain,
% 242.18/242.18 (P3(f16(a15,f11(a1)),f16(a8,f3(f11(a1))))),
% 242.18/242.18 inference(scs_inference,[],[1,35,20])).
% 242.18/242.18 cnf(984,plain,
% 242.18/242.18 (P5(f16(a15,f11(a1)),a8)),
% 242.18/242.18 inference(scs_inference,[],[1,5,36,23])).
% 242.18/242.18 cnf(1030,plain,
% 242.18/242.18 (P3(f16(a2,f10(a1)),f16(a8,f6(f10(a1))))),
% 242.18/242.18 inference(scs_inference,[],[1,37,19])).
% 242.18/242.18 cnf(1076,plain,
% 242.18/242.18 (P5(f16(a8,f19(a1)),a13)),
% 242.18/242.18 inference(scs_inference,[],[1,6,38,23])).
% 242.18/242.18 cnf(1122,plain,
% 242.18/242.18 (P3(f16(a8,f6(f11(a1))),f9(a8,f17(f11(a1))))),
% 242.18/242.18 inference(scs_inference,[],[1,39,20])).
% 242.18/242.18 cnf(1168,plain,
% 242.18/242.18 (P3(f16(a8,f17(f10(a1))),f9(a14,f3(f10(a1))))),
% 242.18/242.18 inference(scs_inference,[],[1,40,19])).
% 242.18/242.18 cnf(1214,plain,
% 242.18/242.18 (P3(f16(a8,f19(f11(a1))),f9(a8,f3(f11(a1))))),
% 242.18/242.18 inference(scs_inference,[],[1,41,20])).
% 242.18/242.18 cnf(1260,plain,
% 242.18/242.18 (~P5(f9(a14,f11(a1)),x12601)+P5(f16(a15,f10(a1)),x12601)),
% 242.18/242.18 inference(scs_inference,[],[1,42,24])).
% 242.18/242.18 cnf(1306,plain,
% 242.18/242.18 (~P5(f9(a14,f19(a1)),x13061)+P5(f16(a2,f10(a1)),x13061)),
% 242.18/242.18 inference(scs_inference,[],[1,43,24])).
% 242.18/242.18 cnf(1352,plain,
% 242.18/242.18 (~P5(f9(a8,f19(a1)),x13521)+P5(f16(a2,f11(a1)),x13521)),
% 242.18/242.18 inference(scs_inference,[],[1,44,24])).
% 242.18/242.18 cnf(1536,plain,
% 242.18/242.18 (P4(f19(a1),a21)+~P4(f3(f11(a1)),a4)),
% 242.18/242.18 inference(scs_inference,[],[1,432,18])).
% 242.18/242.18 cnf(1628,plain,
% 242.18/242.18 (P4(f19(a1),a21)+~P4(f17(f11(a1)),a4)),
% 242.18/242.18 inference(scs_inference,[],[1,478,18])).
% 242.18/242.18 cnf(2775,plain,
% 242.18/242.18 (~P1(f10(a1),a12)+~P5(f9(x27751,f3(f10(a1))),a13)+P5(f16(a8,f3(f10(a1))),a13)),
% 242.18/242.18 inference(scs_inference,[],[209,14,53])).
% 242.18/242.18 cnf(2821,plain,
% 242.18/242.18 (P5(f16(a8,f3(f10(a1))),a13)+~P5(f9(x28211,f3(f10(a1))),a13)),
% 242.18/242.18 inference(scs_inference,[],[1,2775,19])).
% 242.18/242.18 cnf(2913,plain,
% 242.18/242.18 (P1(f3(f11(a1)),a5)),
% 242.18/242.18 inference(scs_inference,[],[1,14,20])).
% 242.18/242.18 cnf(3648,plain,
% 242.18/242.18 (~P1(f10(a1),a12)+~P5(f9(x36481,f6(f10(a1))),a13)+P5(f16(a8,f6(f10(a1))),a13)),
% 242.18/242.18 inference(scs_inference,[],[570,15,53])).
% 242.18/242.18 cnf(3694,plain,
% 242.18/242.18 (P5(f16(a8,f6(f10(a1))),a13)+~P5(f9(x36941,f6(f10(a1))),a13)),
% 242.18/242.18 inference(scs_inference,[],[1,3648,19])).
% 242.18/242.18 cnf(3969,plain,
% 242.18/242.18 (P1(f17(f11(a1)),a18)),
% 242.18/242.18 inference(scs_inference,[],[1,16,20])).
% 242.18/242.18 cnf(4198,plain,
% 242.18/242.18 (~P1(f10(a1),a12)+~P5(f9(a8,f17(f10(a1))),a13)+P5(f16(a8,f17(f10(a1))),a8)),
% 242.18/242.18 inference(scs_inference,[],[297,16,52])).
% 242.18/242.18 cnf(4244,plain,
% 242.18/242.18 (P5(f16(a8,f17(f10(a1))),a8)+~P5(f9(a8,f17(f10(a1))),a13)),
% 242.18/242.18 inference(scs_inference,[],[1,4198,19])).
% 242.18/242.18 cnf(4426,plain,
% 242.18/242.18 (P4(f19(f10(a1)),a21)+~P1(f10(a1),a12)),
% 242.18/242.18 inference(scs_inference,[],[17,81])).
% 242.18/242.18 cnf(4472,plain,
% 242.18/242.18 (P4(f19(f10(a1)),a21)),
% 242.18/242.18 inference(scs_inference,[],[1,4426,19])).
% 242.18/242.18 cnf(4518,plain,
% 242.18/242.18 (P1(f19(f10(a1)),a20)),
% 242.18/242.18 inference(scs_inference,[],[1,17,19])).
% 242.18/242.18 cnf(154015,plain,
% 242.18/242.18 (P1(f19(a1),a20)),
% 242.18/242.18 inference(scs_inference,[],[1,18])).
% 242.18/242.18 cnf(154017,plain,
% 242.18/242.18 (P1(f10(a1),a12)),
% 242.18/242.18 inference(scs_inference,[],[1,18,19])).
% 242.18/242.18 cnf(154019,plain,
% 242.18/242.18 (P1(f11(a1),a12)),
% 242.18/242.18 inference(scs_inference,[],[1,18,19,20])).
% 242.18/242.18 cnf(154021,plain,
% 242.18/242.18 (P3(f9(a8,f10(a1)),f9(a8,f6(f10(a1))))),
% 242.18/242.18 inference(scs_inference,[],[1,18,19,20,28])).
% 242.18/242.18 cnf(154023,plain,
% 242.18/242.18 (P3(f9(a8,f11(a1)),f9(a8,f19(f11(a1))))),
% 242.18/242.18 inference(scs_inference,[],[1,18,19,20,28,29])).
% 242.18/242.18 cnf(154029,plain,
% 242.18/242.18 (P3(f9(a14,f10(a1)),f9(a14,f6(f10(a1))))),
% 242.18/242.18 inference(scs_inference,[],[1,18,19,20,28,29,30,31,32])).
% 242.18/242.18 cnf(154031,plain,
% 242.18/242.18 (P3(f9(a14,f11(a1)),f9(a14,f19(f11(a1))))),
% 242.18/242.18 inference(scs_inference,[],[1,18,19,20,28,29,30,31,32,33])).
% 242.18/242.18 cnf(154035,plain,
% 242.18/242.18 (P3(f16(a15,f10(a1)),f16(a8,f3(f10(a1))))),
% 242.18/242.18 inference(scs_inference,[],[1,18,19,20,28,29,30,31,32,33,34,35])).
% 242.18/242.18 cnf(154039,plain,
% 242.18/242.18 (P3(f16(a2,f11(a1)),f16(a8,f6(f11(a1))))),
% 242.18/242.18 inference(scs_inference,[],[1,18,19,20,28,29,30,31,32,33,34,35,36,37])).
% 242.18/242.18 cnf(154043,plain,
% 242.18/242.18 (P3(f16(a15,f10(a1)),f9(a14,f11(a1)))),
% 242.18/242.18 inference(scs_inference,[],[1,18,19,20,28,29,30,31,32,33,34,35,36,37,38,42])).
% 242.18/242.18 cnf(154045,plain,
% 242.18/242.18 (P3(f16(a2,f10(a1)),f9(a14,f19(a1)))),
% 242.18/242.18 inference(scs_inference,[],[1,18,19,20,28,29,30,31,32,33,34,35,36,37,38,42,43])).
% 242.18/242.18 cnf(154047,plain,
% 242.18/242.18 (P3(f16(a2,f11(a1)),f9(a8,f19(a1)))),
% 242.18/242.18 inference(scs_inference,[],[1,18,19,20,28,29,30,31,32,33,34,35,36,37,38,42,43,44])).
% 242.18/242.18 cnf(154049,plain,
% 242.18/242.18 (P5(f9(a8,f19(f10(a1))),a13)),
% 242.18/242.18 inference(scs_inference,[],[662,1,754,18,19,20,28,29,30,31,32,33,34,35,36,37,38,42,43,44,23])).
% 242.18/242.18 cnf(154051,plain,
% 242.18/242.18 (~P5(f9(a8,a1),a13)),
% 242.18/242.18 inference(scs_inference,[],[7,662,1,2,754,18,19,20,28,29,30,31,32,33,34,35,36,37,38,42,43,44,23,25])).
% 242.18/242.18 cnf(154066,plain,
% 242.18/242.18 (~P5(f9(a8,f19(f10(a1))),a8)),
% 242.18/242.18 inference(scs_inference,[],[8,154051,154049,23,24,25])).
% 242.18/242.18 cnf(154070,plain,
% 242.18/242.18 (~P5(f9(x1540701,f19(f10(a1))),a8)+P5(f16(a8,f19(f10(a1))),a8)),
% 242.18/242.18 inference(scs_inference,[],[8,154051,154017,154049,4518,4472,23,24,25,22,54])).
% 242.18/242.18 cnf(154076,plain,
% 242.18/242.18 (~P5(f9(a14,a1),a8)),
% 242.18/242.18 inference(scs_inference,[],[8,154051,154049,3,23,24,25])).
% 242.18/242.18 cnf(154111,plain,
% 242.18/242.18 (~P5(f16(a2,a1),a8)),
% 242.18/242.18 inference(scs_inference,[],[8,154076,154051,154049,2,6,23,24,25])).
% 242.18/242.18 cnf(154138,plain,
% 242.18/242.18 (P4(f17(f11(a1)),a21)+P4(f17(f11(a1)),a4)),
% 242.18/242.18 inference(scs_inference,[],[3969,154111,154051,154049,2,24,23,22])).
% 242.18/242.18 cnf(154146,plain,
% 242.18/242.18 (~P5(f9(a2,a1),a13)),
% 242.18/242.18 inference(scs_inference,[],[7,154111,154051,154049,2,4,23,24,25])).
% 242.18/242.18 cnf(154168,plain,
% 242.18/242.18 (P4(f3(f11(a1)),a21)+P4(f3(f11(a1)),a4)),
% 242.18/242.18 inference(scs_inference,[],[2913,154076,154146,154049,2,24,23,22])).
% 242.18/242.18 cnf(154170,plain,
% 242.18/242.18 (P4(f3(f11(a1)),a4)+~P5(f16(a8,f3(f11(a1))),a8)+P5(f9(a14,f3(f11(a1))),a8)),
% 242.18/242.18 inference(scs_inference,[],[2913,154076,154146,154049,2,24,23,22,50])).
% 242.18/242.18 cnf(154175,plain,
% 242.18/242.18 (~P5(f16(a15,a1),a13)),
% 242.18/242.18 inference(scs_inference,[],[7,154111,154146,154049,2,5,23,24,25])).
% 242.18/242.18 cnf(154205,plain,
% 242.18/242.18 (~P5(f9(a8,f10(a1)),a8)),
% 242.18/242.18 inference(scs_inference,[],[8,154076,154146,154049,2,754,23,24,25])).
% 242.18/242.18 cnf(154227,plain,
% 242.18/242.18 (P4(f19(a1),a21)+P4(f19(a1),a4)),
% 242.18/242.18 inference(scs_inference,[],[154015,154205,154175,154049,2,24,23,22])).
% 242.18/242.18 cnf(154229,plain,
% 242.18/242.18 (P4(f19(a1),a4)+P5(f9(a8,f19(a1)),a13)),
% 242.18/242.18 inference(scs_inference,[],[154015,154205,154175,154049,2,1076,24,23,22,45])).
% 242.18/242.18 cnf(154231,plain,
% 242.18/242.18 (P5(f16(a2,f11(a1)),a13)+P4(f19(a1),a4)),
% 242.18/242.18 inference(scs_inference,[],[154015,154205,154175,154049,2,1076,24,23,22,45,1352])).
% 242.18/242.18 cnf(154233,plain,
% 242.18/242.18 (P4(f19(a1),a4)+~P5(f9(x1542331,f19(a1)),a8)+P5(f16(a8,f19(a1)),a8)),
% 242.18/242.18 inference(scs_inference,[],[154015,154205,154175,154049,2,1076,24,23,22,45,1352,54])).
% 242.18/242.18 cnf(154238,plain,
% 242.18/242.18 (~P5(f9(a8,f11(a1)),a13)),
% 242.18/242.18 inference(scs_inference,[],[154205,7,154146,154049,2,708,23,24,25])).
% 242.18/242.18 cnf(154248,plain,
% 242.18/242.18 (~P4(f17(f11(a1)),a21)+P5(f9(a8,f17(f11(a1))),a13)+~P5(f16(a8,f17(f11(a1))),a8)),
% 242.18/242.18 inference(scs_inference,[],[3969,154205,2,24,23,46])).
% 242.18/242.18 cnf(154299,plain,
% 242.18/242.18 (~P5(f16(a15,f11(a1)),a13)),
% 242.18/242.18 inference(scs_inference,[],[7,154146,154111,154049,2,984,23,24,25])).
% 242.18/242.18 cnf(154328,plain,
% 242.18/242.18 (~P5(f16(a8,f19(a1)),a8)),
% 242.18/242.18 inference(scs_inference,[],[8,154076,2,1076,23,24,25])).
% 242.18/242.18 cnf(154332,plain,
% 242.18/242.18 (~P4(f19(a1),a21)+~P5(f9(x1543321,f19(a1)),a8)),
% 242.18/242.18 inference(scs_inference,[],[8,154015,154076,154066,4472,2,1076,23,24,25,48,54])).
% 242.18/242.18 cnf(154334,plain,
% 242.18/242.18 (P4(f19(a1),a4)+~P5(f9(x1543341,f19(a1)),a8)),
% 242.18/242.18 inference(scs_inference,[],[154328,154233])).
% 242.18/242.18 cnf(154815,plain,
% 242.18/242.18 (~P4(f3(f11(a1)),a21)+~P5(f9(x1548151,f3(f11(a1))),a13)+P5(f16(a8,f3(f11(a1))),a13)),
% 242.18/242.18 inference(scs_inference,[],[2913,154146,154111,154049,2,23,24,53])).
% 242.18/242.18 cnf(154914,plain,
% 242.18/242.18 (~P4(f3(f11(a1)),a21)+~P5(f16(a8,f3(f11(a1))),a8)+P5(f9(a8,f3(f11(a1))),a8)),
% 242.18/242.18 inference(scs_inference,[],[154238,2913,154051,154049,3,23,24,47])).
% 242.18/242.18 cnf(154929,plain,
% 242.18/242.18 (~P5(f16(a15,f10(a1)),x1549291)+P5(f9(a14,f11(a1)),x1549291)),
% 242.18/242.18 inference(scs_inference,[],[154043,23])).
% 242.18/242.18 cnf(154968,plain,
% 242.18/242.18 (~P5(f16(a2,f11(a1)),x1549681)+P5(f9(a8,f19(a1)),x1549681)),
% 242.18/242.18 inference(scs_inference,[],[154047,23])).
% 242.18/242.18 cnf(155220,plain,
% 242.18/242.18 (P4(f3(f11(a1)),a21)+~P4(f19(a1),a4)),
% 242.18/242.18 inference(scs_inference,[],[154168,26])).
% 242.18/242.18 cnf(155294,plain,
% 242.18/242.18 (~P4(f19(a1),a4)+P5(f9(a8,f3(f11(a1))),a8)+~P5(f16(a8,f3(f11(a1))),a8)),
% 242.18/242.18 inference(scs_inference,[],[2913,155220,47])).
% 242.18/242.18 cnf(155335,plain,
% 242.18/242.18 (~P4(f17(f11(a1)),a21)+~P5(f9(a8,f17(f11(a1))),a8)+P5(f16(a8,f17(f11(a1))),a13)),
% 242.18/242.18 inference(scs_inference,[],[3969,51])).
% 242.18/242.18 cnf(155356,plain,
% 242.18/242.18 (P5(f9(a8,f19(a1)),a13)+P4(f3(f11(a1)),a21)),
% 242.18/242.18 inference(scs_inference,[],[154229,155220])).
% 242.18/242.18 cnf(155484,plain,
% 242.18/242.18 (~P5(f9(x1554841,f19(a1)),a8)+~P4(f17(f11(a1)),a4)),
% 242.18/242.18 inference(scs_inference,[],[154332,1628])).
% 242.18/242.18 cnf(155550,plain,
% 242.18/242.18 (~P5(f9(x1555501,f19(a1)),a8)+~P4(f3(f11(a1)),a4)),
% 242.18/242.18 inference(scs_inference,[],[154334,26])).
% 242.18/242.18 cnf(155945,plain,
% 242.18/242.18 (P4(f3(f11(a1)),a21)+P5(f16(a2,f11(a1)),a13)),
% 242.18/242.18 inference(scs_inference,[],[155356,1352])).
% 242.18/242.18 cnf(156154,plain,
% 242.18/242.18 (~P5(f16(a2,f11(a1)),a8)+~P4(f3(f11(a1)),a4)),
% 242.18/242.18 inference(scs_inference,[],[155550,154968])).
% 242.18/242.18 cnf(156372,plain,
% 242.18/242.18 (P4(f3(f11(a1)),a21)+~P5(f16(a2,f11(a1)),a8)),
% 242.18/242.18 inference(scs_inference,[],[156154,154168])).
% 242.18/242.18 cnf(157422,plain,
% 242.18/242.18 (~P5(f16(a8,f3(f11(a1))),a8)+P5(f9(a14,f3(f11(a1))),a8)+~P4(f19(a1),a4)),
% 242.18/242.18 inference(scs_inference,[],[154170,26])).
% 242.18/242.18 cnf(157572,plain,
% 242.18/242.18 (P4(f17(f11(a1)),a4)+P5(f9(a8,f17(f11(a1))),a13)+~P5(f16(a8,f17(f11(a1))),a8)),
% 242.18/242.18 inference(scs_inference,[],[154248,154138])).
% 242.18/242.18 cnf(157939,plain,
% 242.18/242.18 (P4(f3(f11(a1)),a4)+P5(f16(a8,f3(f11(a1))),a13)+~P5(f9(x1579391,f3(f11(a1))),a13)),
% 242.18/242.18 inference(scs_inference,[],[154815,154168])).
% 242.18/242.18 cnf(158084,plain,
% 242.18/242.18 (P4(f17(f11(a1)),a4)+P5(f16(a8,f17(f11(a1))),a13)+~P5(f9(a8,f17(f11(a1))),a8)),
% 242.18/242.18 inference(scs_inference,[],[155335,154138])).
% 242.18/242.18 cnf(158310,plain,
% 242.18/242.18 (P5(f9(a8,f17(f11(a1))),a13)+~P5(f16(a8,f17(f11(a1))),a8)+~P4(f19(a1),a4)),
% 242.18/242.18 inference(scs_inference,[],[157572,27])).
% 242.18/242.18 cnf(158795,plain,
% 242.18/242.18 (P4(f19(a1),a21)+P5(f16(a8,f3(f11(a1))),a13)+~P5(f9(x1587951,f3(f11(a1))),a13)),
% 242.18/242.18 inference(scs_inference,[],[157939,1536])).
% 242.18/242.18 cnf(233435,plain,
% 242.18/242.18 (~P5(f9(a8,f6(f11(a1))),a13)),
% 242.18/242.18 inference(scs_inference,[],[616,154238,24])).
% 242.18/242.18 cnf(233437,plain,
% 242.18/242.18 (P5(f9(a14,f19(f10(a1))),a8)),
% 242.18/242.18 inference(scs_inference,[],[616,846,154238,892,24,23])).
% 242.18/242.18 cnf(233439,plain,
% 242.18/242.19 (P5(f16(a8,f19(f10(a1))),a8)),
% 242.18/242.19 inference(scs_inference,[],[616,846,154238,892,24,23,154070])).
% 242.18/242.19 cnf(233445,plain,
% 242.18/242.19 (~P5(f9(a14,f19(f10(a1))),a13)),
% 242.18/242.19 inference(scs_inference,[],[233437,7,25])).
% 242.18/242.19 cnf(233453,plain,
% 242.18/242.19 (~P5(f16(a8,f19(f10(a1))),a13)),
% 242.18/242.19 inference(scs_inference,[],[233437,233439,233435,4518,154111,7,154066,4472,1076,25,24,23,47,49])).
% 242.18/242.19 cnf(233455,plain,
% 242.18/242.19 (P5(f9(a14,f6(f11(a1))),a13)+~P5(f16(a8,f6(f11(a1))),a13)),
% 242.18/242.19 inference(scs_inference,[],[233437,233439,233435,4518,154111,7,252,154066,4472,1076,253,25,24,23,47,49,55])).
% 242.18/242.19 cnf(233467,plain,
% 242.18/242.19 (~P5(f16(a8,f3(f11(a1))),a13)),
% 242.18/242.19 inference(scs_inference,[],[938,154299,24])).
% 242.18/242.19 cnf(233469,plain,
% 242.18/242.19 (P5(f9(a8,f6(f10(a1))),a13)),
% 242.18/242.19 inference(scs_inference,[],[938,154021,154299,754,24,23])).
% 242.18/242.19 cnf(233473,plain,
% 242.18/242.19 (P5(f16(a8,f6(f10(a1))),a13)),
% 242.18/242.19 inference(scs_inference,[],[938,154021,233453,154299,4472,754,154049,24,23,53,3694])).
% 242.18/242.19 cnf(233480,plain,
% 242.18/242.19 (~P4(f3(f11(a1)),a21)+~P5(f9(x2334801,f3(f11(a1))),a13)),
% 242.18/242.19 inference(scs_inference,[],[233467,154815])).
% 242.18/242.19 cnf(233482,plain,
% 242.18/242.19 (P4(f19(a1),a21)+~P5(f9(x2334821,f3(f11(a1))),a13)),
% 242.18/242.19 inference(scs_inference,[],[233467,158795])).
% 242.18/242.19 cnf(233484,plain,
% 242.18/242.19 (~P5(f16(a8,f6(f10(a1))),a8)),
% 242.18/242.19 inference(scs_inference,[],[233473,8,25])).
% 242.18/242.19 cnf(233498,plain,
% 242.18/242.19 (~P5(f9(a8,f6(f10(a1))),a8)),
% 242.18/242.19 inference(scs_inference,[],[233469,8,25])).
% 242.18/242.19 cnf(233510,plain,
% 242.18/242.19 (P5(f16(a2,f10(a1)),a13)),
% 242.18/242.19 inference(scs_inference,[],[1030,233473,24])).
% 242.18/242.19 cnf(233512,plain,
% 242.18/242.19 (~P5(f16(a2,f10(a1)),a8)),
% 242.18/242.19 inference(scs_inference,[],[1030,233484,233473,24,23])).
% 242.18/242.19 cnf(233516,plain,
% 242.18/242.19 (~P5(f9(a14,f19(a1)),a8)),
% 242.18/242.19 inference(scs_inference,[],[1030,233484,233473,233453,4472,154049,24,23,53,1306])).
% 242.18/242.19 cnf(233540,plain,
% 242.18/242.19 (~P5(f9(a8,f19(f11(a1))),a13)),
% 242.18/242.19 inference(scs_inference,[],[154023,154238,24])).
% 242.18/242.19 cnf(233542,plain,
% 242.18/242.19 (P5(f9(a14,f6(f10(a1))),a8)),
% 242.18/242.19 inference(scs_inference,[],[154023,154029,154238,892,24,23])).
% 242.18/242.19 cnf(233552,plain,
% 242.18/242.19 (~P4(f19(a1),a4)+~P5(f9(x2335521,f3(f11(a1))),a13)),
% 242.18/242.19 inference(scs_inference,[],[233482,21])).
% 242.18/242.19 cnf(233553,plain,
% 242.18/242.19 (~P5(f9(a14,f6(f10(a1))),a13)),
% 242.18/242.19 inference(scs_inference,[],[233542,7,25])).
% 242.18/242.19 cnf(233584,plain,
% 242.18/242.19 (P5(f9(a8,f6(f11(a1))),a8)),
% 242.18/242.19 inference(scs_inference,[],[616,708,23])).
% 242.18/242.19 cnf(233590,plain,
% 242.18/242.19 (~P5(f9(a14,f6(f11(a1))),x2335901)+P5(f9(a14,f11(a1)),x2335901)),
% 242.18/242.19 inference(scs_inference,[],[800,616,233553,233473,233453,708,4472,154049,570,23,49,53,24])).
% 242.18/242.19 cnf(233609,plain,
% 242.18/242.19 (~P3(f16(a2,f10(a1)),f16(a8,f19(f10(a1))))),
% 242.18/242.19 inference(scs_inference,[],[233512,233439,24])).
% 242.18/242.19 cnf(233624,plain,
% 242.18/242.19 (P5(f16(a8,f3(f11(a1))),a8)),
% 242.18/242.19 inference(scs_inference,[],[233609,938,984,38,23])).
% 242.18/242.19 cnf(233631,plain,
% 242.18/242.19 (P5(f16(a8,f19(f11(a1))),a8)+~P4(f3(f11(a1)),a21)),
% 242.18/242.19 inference(scs_inference,[],[233609,1214,938,233553,233473,233453,984,4472,154049,570,38,23,49,53,154914,24])).
% 242.18/242.19 cnf(233639,plain,
% 242.18/242.19 (P5(f9(a8,f3(f11(a1))),a8)+~P4(f19(a1),a4)),
% 242.18/242.19 inference(scs_inference,[],[233624,155294])).
% 242.18/242.19 cnf(233642,plain,
% 242.18/242.19 (P5(f9(a14,f3(f11(a1))),a8)+~P4(f19(a1),a4)),
% 242.18/242.19 inference(scs_inference,[],[233624,157422])).
% 242.18/242.19 cnf(233715,plain,
% 242.18/242.19 (P5(f9(a14,f19(a1)),a13)),
% 242.18/242.19 inference(scs_inference,[],[233435,233609,233510,154045,38,24,23])).
% 242.18/242.19 cnf(233732,plain,
% 242.18/242.19 (~P5(f16(a8,f3(f10(a1))),x2337321)+P5(f16(a15,f10(a1)),x2337321)),
% 242.18/242.19 inference(scs_inference,[],[233715,154035,233445,233609,233553,233453,233473,4472,154049,570,38,23,49,53,24])).
% 242.18/242.19 cnf(233766,plain,
% 242.18/242.19 (P5(f16(a8,f6(f11(a1))),a13)+~P5(f9(a8,f19(a1)),a13)),
% 242.18/242.19 inference(scs_inference,[],[154039,233715,233435,233498,233609,233553,233453,233473,4472,154049,570,38,24,49,53,23,48,154231,233552,155945,233639,233642,233631,21,1352])).
% 242.18/242.19 cnf(233777,plain,
% 242.18/242.19 (~P5(f9(a8,f17(f11(a1))),x2337771)+P5(f16(a8,f6(f11(a1))),x2337771)),
% 242.18/242.19 inference(scs_inference,[],[1122,233715,233445,233609,233553,233453,233473,4472,154049,570,38,23,49,53,24])).
% 242.18/242.19 cnf(233805,plain,
% 242.18/242.19 (~P5(f16(a8,f17(f10(a1))),x2338051)+P5(f9(a14,f3(f10(a1))),x2338051)),
% 242.18/242.19 inference(scs_inference,[],[1168,233715,233540,233498,233609,233553,233453,233473,4472,154049,570,38,24,49,53,48,23])).
% 242.18/242.19 cnf(233820,plain,
% 242.18/242.19 (~P5(f16(a8,f6(f11(a1))),x2338201)+P5(f16(a2,f11(a1)),x2338201)),
% 242.18/242.19 inference(scs_inference,[],[2,154039,233516,233498,233609,233553,233453,233473,4472,154049,570,38,23,49,53,48,24])).
% 242.18/242.19 cnf(233939,plain,
% 242.18/242.19 (~P5(f9(a14,f11(a1)),x2339391)+P5(f9(a14,f6(f11(a1))),x2339391)),
% 242.18/242.19 inference(scs_inference,[],[2,800,233512,233609,233553,233453,233473,4472,154049,570,38,49,53,24,23])).
% 242.18/242.19 cnf(233976,plain,
% 242.18/242.19 (~P5(f9(a14,f11(a1)),x2339761)+P5(f9(a14,f19(f11(a1))),x2339761)),
% 242.18/242.19 inference(scs_inference,[],[154031,233469,233484,233609,233553,233453,233473,4472,154049,570,38,49,53,52,23])).
% 242.18/242.19 cnf(234006,plain,
% 242.18/242.19 (~P5(f16(a15,f10(a1)),x2340061)+P5(f16(a8,f3(f10(a1))),x2340061)),
% 242.18/242.19 inference(scs_inference,[],[154035,233609,233553,233453,233473,4472,154049,570,38,49,53,23])).
% 242.18/242.19 cnf(234046,plain,
% 242.18/242.19 (~P5(f16(a8,f6(f11(a1))),x2340461)+P5(f9(a8,f17(f11(a1))),x2340461)),
% 242.18/242.19 inference(scs_inference,[],[3,1122,233540,233469,233484,233609,233553,233453,233473,4472,154049,570,38,49,53,52,24,23])).
% 242.18/242.19 cnf(234050,plain,
% 242.18/242.19 (~P5(f16(a8,f6(f11(a1))),a8)+P4(f17(f11(a1)),a4)+P5(f16(a8,f17(f11(a1))),a13)),
% 242.18/242.19 inference(scs_inference,[],[3,1122,233540,233469,233484,233609,233553,233453,233473,4472,154049,570,38,49,53,52,24,23,233777,158084])).
% 242.18/242.19 cnf(234557,plain,
% 242.18/242.19 (P5(f9(a8,f19(a1)),a13)+~P5(f9(x2345571,f3(f11(a1))),a13)),
% 242.18/242.19 inference(scs_inference,[],[233480,155356])).
% 242.18/242.19 cnf(242438,plain,
% 242.18/242.19 (~P5(f9(a8,f19(a1)),a13)+P5(f9(a14,f6(f11(a1))),a13)),
% 242.18/242.19 inference(scs_inference,[],[233766,233455])).
% 242.18/242.19 cnf(245780,plain,
% 242.18/242.19 (P5(f9(a14,f6(f11(a1))),a13)+~P5(f9(x2457801,f3(f11(a1))),a13)),
% 242.18/242.19 inference(scs_inference,[],[234557,242438])).
% 242.18/242.19 cnf(254221,plain,
% 242.18/242.19 (P5(f9(a14,f11(a1)),a13)+~P5(f9(x2542211,f3(f11(a1))),a13)),
% 242.18/242.19 inference(scs_inference,[],[245780,233590])).
% 242.18/242.19 cnf(254492,plain,
% 242.18/242.19 (P5(f16(a15,f10(a1)),a13)+~P5(f9(x2544921,f3(f11(a1))),a13)),
% 242.18/242.19 inference(scs_inference,[],[254221,1260])).
% 242.18/242.19 cnf(254763,plain,
% 242.18/242.19 (P5(f16(a8,f3(f10(a1))),a13)+~P5(f9(x2547631,f3(f11(a1))),a13)),
% 242.18/242.19 inference(scs_inference,[],[254492,234006])).
% 242.18/242.19 cnf(485142,plain,
% 242.18/242.19 (P3(f16(a8,f6(f10(a1))),f9(a8,f17(f10(a1))))),
% 242.18/242.19 inference(scs_inference,[],[154017,39])).
% 242.18/242.19 cnf(485144,plain,
% 242.18/242.19 (P3(f16(a8,f17(f11(a1))),f9(a14,f3(f11(a1))))),
% 242.18/242.19 inference(scs_inference,[],[154017,154019,39,40])).
% 242.18/242.19 cnf(485146,plain,
% 242.18/242.19 (P3(f16(a8,f19(f10(a1))),f9(a8,f3(f10(a1))))),
% 242.18/242.19 inference(scs_inference,[],[154017,154019,39,40,41])).
% 242.18/242.19 cnf(525235,plain,
% 242.18/242.19 (P5(f9(a8,f17(f10(a1))),a13)),
% 242.18/242.19 inference(scs_inference,[],[485142,233473,23])).
% 242.18/242.19 cnf(525237,plain,
% 242.18/242.19 (~P5(f9(a8,f3(f10(a1))),a13)),
% 242.18/242.19 inference(scs_inference,[],[485142,485146,233453,233473,23,24])).
% 242.18/242.19 cnf(525243,plain,
% 242.18/242.19 (P5(f16(a8,f17(f10(a1))),a8)),
% 242.18/242.19 inference(scs_inference,[],[485142,485146,233553,233453,233498,233473,570,23,24,49,48,4244])).
% 242.18/242.19 cnf(525244,plain,
% 242.18/242.19 (P5(f9(a14,f3(f10(a1))),a8)),
% 242.18/242.19 inference(scs_inference,[],[485142,485146,233553,233453,233498,233473,570,23,24,49,48,4244,233805])).
% 242.18/242.19 cnf(525263,plain,
% 242.18/242.19 (~P5(f9(a8,f17(f10(a1))),a8)),
% 242.18/242.19 inference(scs_inference,[],[525235,525243,525237,233512,7,296,233553,233473,297,570,25,23,24,49,51])).
% 242.18/242.19 cnf(525274,plain,
% 242.18/242.19 (P5(f9(a8,f3(f10(a1))),a8)),
% 242.18/242.19 inference(scs_inference,[],[525244,485146,7,233439,25,23])).
% 242.18/242.19 cnf(525280,plain,
% 242.18/242.19 (~P5(f16(a8,f3(f10(a1))),a13)),
% 242.18/242.19 inference(scs_inference,[],[525244,485146,525237,7,208,233553,233469,209,233484,233473,233439,570,25,23,49,52,55])).
% 242.18/242.19 cnf(525286,plain,
% 242.18/242.19 (P5(f16(a15,f10(a1)),a8)),
% 242.18/242.19 inference(scs_inference,[],[525244,485146,525237,7,208,233553,233469,209,233484,233473,233439,570,25,23,49,52,55,58,2821,254763,233732])).
% 242.18/242.19 cnf(525299,plain,
% 242.18/242.19 (P5(f16(a8,f17(f11(a1))),a8)+~P5(f16(a2,f11(a1)),a8)),
% 242.18/242.19 inference(scs_inference,[],[485144,525244,485146,525237,7,208,233624,233553,2913,233469,209,233484,233473,233439,570,25,23,49,52,55,58,2821,254763,233732,24,46,50,155220,154229,154334,154929,156372])).
% 242.18/242.19 cnf(525312,plain,
% 242.18/242.19 (P5(f9(a14,f11(a1)),a8)),
% 242.18/242.19 inference(scs_inference,[],[525286,154929])).
% 242.18/242.19 cnf(525334,plain,
% 242.18/242.19 (P5(f16(a8,f6(f11(a1))),a8)),
% 242.18/242.19 inference(scs_inference,[],[525286,525274,525280,525263,525243,7,252,233553,233584,233469,209,253,233484,233473,297,570,154929,25,23,24,49,51,47,52,233976,233939,56,58])).
% 242.18/242.19 cnf(525336,plain,
% 242.18/242.19 (P5(f16(a2,f11(a1)),a8)),
% 242.18/242.19 inference(scs_inference,[],[525286,525274,525280,525263,525243,7,252,233553,233584,233469,209,253,233484,233473,297,570,154929,25,23,24,49,51,47,52,233976,233939,56,58,233820])).
% 242.18/242.19 cnf(525338,plain,
% 242.18/242.19 (P5(f9(a8,f17(f11(a1))),a8)),
% 242.18/242.19 inference(scs_inference,[],[525286,525274,525280,525263,525243,7,252,233553,233584,233469,209,253,233484,233473,297,570,154929,25,23,24,49,51,47,52,233976,233939,56,58,233820,234046])).
% 242.18/242.19 cnf(525340,plain,
% 242.18/242.19 (P5(f16(a8,f17(f11(a1))),a8)),
% 242.18/242.19 inference(scs_inference,[],[525286,525274,525280,525263,525243,7,252,233553,233584,233469,209,253,233484,233473,297,570,154929,25,23,24,49,51,47,52,233976,233939,56,58,233820,234046,525299])).
% 242.18/242.19 cnf(525348,plain,
% 242.18/242.19 (P5(f9(a8,f17(f11(a1))),a13)+~P4(f19(a1),a4)),
% 242.18/242.19 inference(scs_inference,[],[525340,158310])).
% 242.18/242.19 cnf(525352,plain,
% 242.18/242.19 (P4(f17(f11(a1)),a4)+P5(f16(a8,f17(f11(a1))),a13)),
% 242.18/242.19 inference(scs_inference,[],[525334,234050])).
% 242.18/242.19 cnf(525354,plain,
% 242.18/242.19 (~P4(f19(a1),a4)),
% 242.18/242.19 inference(scs_inference,[],[7,525338,525348,25])).
% 242.18/242.19 cnf(525356,plain,
% 242.18/242.19 (P4(f19(a1),a21)),
% 242.18/242.19 inference(scs_inference,[],[525354,154227])).
% 242.18/242.19 cnf(525384,plain,
% 242.18/242.19 (~P4(f19(a1),a21)),
% 242.18/242.19 inference(scs_inference,[],[525312,525336,525340,525280,525274,7,154328,3969,154015,233553,209,233498,233473,570,154968,155484,525352,22,25,46,49,51,48,54])).
% 242.18/242.19 cnf(525387,plain,
% 242.18/242.19 ($false),
% 242.18/242.19 inference(scs_inference,[],[525384,525356]),
% 242.18/242.19 ['proof']).
% 242.57/242.48 % SZS output end Proof
% 242.57/242.48 % Total time :241.060000s
%------------------------------------------------------------------------------