%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : HWV007-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 : n024.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Jun 24 07:29:06 EDT 2024
% Result : Unsatisfiable 241.71s 242.63s
% Output : CNFRefutation 242.12s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.13 % Problem : HWV007-1 : TPTP v8.2.0. Released v2.1.0.
% 0.12/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.13/0.34 % Computer : n024.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Fri Jun 21 01:02:54 EDT 2024
% 0.20/0.34 % CPUTime :
% 0.53/0.57 start to proof:theBenchmark
% 241.66/242.60 %-------------------------------------------
% 241.66/242.60 % File :CSE---1.7
% 241.66/242.60 % Problem :theBenchmark
% 241.66/242.60 % Transform :cnf
% 241.66/242.60 % Format :tptp:raw
% 241.66/242.60 % Command :java -jar mcs_scs.jar %d %s
% 241.66/242.60
% 241.66/242.60 % Result :Theorem 241.000000s
% 241.66/242.60 % Output :CNFRefutation 241.000000s
% 241.66/242.60 %-------------------------------------------
% 241.71/242.62 %--------------------------------------------------------------------------
% 241.71/242.62 % File : HWV007-1 : TPTP v8.2.0. Released v2.1.0.
% 241.71/242.62 % Domain : Hardware Verification
% 241.71/242.62 % Problem : A fulladder built from two halfadders and an or gate
% 241.71/242.62 % Version : [Gei96] axioms.
% 241.71/242.62 % English :
% 241.71/242.62
% 241.71/242.62 % Refs : [Gei96] Geisler (1996), Email to G. Sutcliffe
% 241.71/242.62 % Source : [Gei96]
% 241.71/242.62 % Names :
% 241.71/242.62
% 241.71/242.62 % Status : Unsatisfiable
% 241.71/242.62 % Rating : 0.08 v8.2.0, 0.14 v8.1.0, 0.00 v7.0.0, 0.25 v6.4.0, 0.12 v6.3.0, 0.29 v6.2.0, 0.11 v6.1.0, 0.00 v5.2.0, 0.10 v5.1.0, 0.09 v5.0.0, 0.14 v4.1.0, 0.12 v4.0.1, 0.20 v4.0.0, 0.14 v3.4.0, 0.25 v3.3.0, 0.00 v2.6.0, 0.33 v2.5.0, 0.20 v2.4.0, 0.00 v2.2.1, 0.33 v2.1.0
% 241.71/242.62 % Syntax : Number of clauses : 56 ( 9 unt; 3 nHn; 56 RR)
% 241.71/242.62 % Number of literals : 139 ( 0 equ; 88 neg)
% 241.71/242.62 % Maximal clause size : 5 ( 2 avg)
% 241.71/242.62 % Maximal term depth : 3 ( 1 avg)
% 241.71/242.62 % Number of predicates : 5 ( 5 usr; 0 prp; 2-2 aty)
% 241.71/242.62 % Number of functors : 21 ( 21 usr; 13 con; 0-2 aty)
% 241.71/242.62 % Number of variables : 52 ( 3 sgn)
% 241.71/242.62 % SPC : CNF_UNS_RFO_NEQ_NHN
% 241.71/242.62
% 241.71/242.62 % Comments :
% 241.71/242.62 %--------------------------------------------------------------------------
% 241.71/242.62 %----Include basic diagnosis axioms
% 241.71/242.62 include('Axioms/HWV001-0.ax').
% 241.71/242.62 %----Include model of halfadder
% 241.71/242.62 include('Axioms/HWV001-1.ax').
% 241.71/242.62 %----Include model of fulladder
% 241.71/242.62 include('Axioms/HWV001-2.ax').
% 241.71/242.62 %--------------------------------------------------------------------------
% 241.71/242.62 %----Observations
% 241.71/242.62 cnf(f_isa_fulladder,hypothesis,
% 241.71/242.62 type(f,fulladder) ).
% 241.71/242.62
% 241.71/242.62 cnf(in1_1,hypothesis,
% 241.71/242.62 value(in(n1,f),n0) ).
% 241.71/242.62
% 241.71/242.62 cnf(in2_0,hypothesis,
% 241.71/242.62 value(in(n2,f),n1) ).
% 241.71/242.62
% 241.71/242.62 cnf(inc_1,hypothesis,
% 241.71/242.63 value(in(c,f),n1) ).
% 241.71/242.63
% 241.71/242.63 cnf(outs_1,hypothesis,
% 241.71/242.63 value(out(s,f),n1) ).
% 241.71/242.63
% 241.71/242.63 cnf(outc_0,hypothesis,
% 241.71/242.63 value(out(c,f),n0) ).
% 241.71/242.63
% 241.71/242.63 %----Minimal diagnosis
% 241.71/242.63 cnf(diagnosis_and2h1,negated_conjecture,
% 241.71/242.63 ~ mode(and2(h1(f)),abnormal) ).
% 241.71/242.63
% 241.71/242.63 cnf(diagnosis_or1_and1h1,negated_conjecture,
% 241.71/242.63 ( ~ mode(or1(f),abnormal)
% 241.71/242.63 | ~ mode(and1(h1(f)),abnormal) ) ).
% 241.71/242.63
% 241.71/242.63 cnf(diagnosis_or1_not1h1,negated_conjecture,
% 241.71/242.63 ( ~ mode(or1(f),abnormal)
% 241.71/242.63 | ~ mode(not1(h1(f)),abnormal) ) ).
% 241.71/242.63
% 241.71/242.63 cnf(diagnosis_or1_and1h2,negated_conjecture,
% 241.71/242.63 ( ~ mode(or1(f),abnormal)
% 241.71/242.63 | ~ mode(and1(h2(f)),abnormal) ) ).
% 241.71/242.63
% 241.71/242.63 cnf(diagnosis_or1_or1h2,negated_conjecture,
% 241.71/242.63 ( ~ mode(or1(f),abnormal)
% 241.71/242.63 | ~ mode(or1(h2(f)),abnormal) ) ).
% 241.71/242.63
% 241.71/242.63 %--------------------------------------------------------------------------
% 241.71/242.63 %-------------------------------------------
% 241.71/242.63 % Proof found
% 241.71/242.63 % SZS status Theorem for theBenchmark
% 241.71/242.63 % SZS output start Proof
% 241.71/242.64 %ClaNum:56(EqnAxiom:0)
% 241.71/242.64 %VarNum:151(SingletonVarNum:52)
% 241.71/242.64 %MaxLitNum:5
% 241.71/242.64 %MaxfuncDepth:2
% 241.71/242.64 %SharedTerms:40
% 241.71/242.64 %goalClause: 9 22 23 24 25
% 241.71/242.64 %singleGoalClaCount:1
% 241.71/242.64 [1]P1(a1,a7)
% 241.71/242.64 [7]~P2(a13,a8)
% 241.71/242.64 [8]~P2(a8,a13)
% 241.71/242.64 [2]P5(f9(a8,a1),a13)
% 241.71/242.64 [3]P5(f9(a14,a1),a8)
% 241.71/242.64 [4]P5(f9(a2,a1),a8)
% 241.71/242.64 [5]P5(f16(a15,a1),a8)
% 241.71/242.64 [6]P5(f16(a2,a1),a13)
% 241.71/242.64 [9]~P4(f3(f10(a1)),a4)
% 241.71/242.64 [22]~P4(f19(a1),a4)+~P4(f5(f10(a1)),a4)
% 241.71/242.64 [23]~P4(f19(a1),a4)+~P4(f5(f12(a1)),a4)
% 241.71/242.64 [24]~P4(f19(a1),a4)+~P4(f17(f10(a1)),a4)
% 241.71/242.64 [25]~P4(f19(a1),a4)+~P4(f19(f12(a1)),a4)
% 241.71/242.64 [17]~P4(x171,a4)+~P4(x171,a21)
% 241.71/242.64 [10]~P1(x101,a11)+P1(f5(x101),a6)
% 241.71/242.64 [11]~P1(x111,a11)+P1(f3(x111),a6)
% 241.71/242.64 [12]~P1(x121,a11)+P1(f17(x121),a18)
% 241.71/242.64 [13]~P1(x131,a11)+P1(f19(x131),a20)
% 241.71/242.64 [14]~P1(x141,a7)+P1(f19(x141),a20)
% 241.71/242.64 [15]~P1(x151,a7)+P1(f10(x151),a11)
% 241.71/242.64 [16]~P1(x161,a7)+P1(f12(x161),a11)
% 241.71/242.64 [26]~P1(x261,a11)+P3(f9(a8,x261),f9(a8,f3(x261)))
% 241.71/242.64 [27]~P1(x271,a11)+P3(f9(a8,x271),f9(a8,f19(x271)))
% 241.71/242.64 [28]~P1(x281,a7)+P3(f9(a8,x281),f9(a8,f12(x281)))
% 241.71/242.64 [29]~P1(x291,a7)+P3(f9(a14,x291),f9(a8,f10(x291)))
% 241.71/242.64 [30]~P1(x301,a11)+P3(f9(a14,x301),f9(a14,f3(x301)))
% 241.71/242.64 [31]~P1(x311,a11)+P3(f9(a14,x311),f9(a14,f19(x311)))
% 241.71/242.64 [32]~P1(x321,a7)+P3(f9(a2,x321),f9(a14,f10(x321)))
% 241.71/242.64 [33]~P1(x331,a11)+P3(f16(a15,x331),f16(a8,f5(x331)))
% 241.71/242.64 [34]~P1(x341,a7)+P3(f16(a15,x341),f16(a15,f12(x341)))
% 241.71/242.64 [35]~P1(x351,a11)+P3(f16(a2,x351),f16(a8,f3(x351)))
% 241.71/242.64 [36]~P1(x361,a7)+P3(f16(a2,x361),f16(a8,f19(x361)))
% 241.71/242.64 [37]~P1(x371,a11)+P3(f16(a8,f3(x371)),f9(a8,f17(x371)))
% 241.71/242.64 [38]~P1(x381,a11)+P3(f16(a8,f17(x381)),f9(a14,f5(x381)))
% 241.71/242.64 [39]~P1(x391,a11)+P3(f16(a8,f19(x391)),f9(a8,f5(x391)))
% 241.71/242.64 [40]~P1(x401,a7)+P3(f16(a15,f10(x401)),f9(a14,f12(x401)))
% 241.71/242.64 [41]~P1(x411,a7)+P3(f16(a2,f10(x411)),f9(a14,f19(x411)))
% 241.71/242.64 [42]~P1(x421,a7)+P3(f16(a2,f12(x421)),f9(a8,f19(x421)))
% 241.71/242.64 [18]~P1(x181,x182)+P4(x181,a4)+P4(x181,a21)
% 241.71/242.64 [19]~P5(x193,x192)+P5(x191,x192)+~P3(x193,x191)
% 241.71/242.64 [20]~P5(x203,x202)+P5(x201,x202)+~P3(x201,x203)
% 241.71/242.64 [21]~P5(x213,x211)+P2(x211,x212)+~P5(x213,x212)
% 241.71/242.64 [43]~P4(x431,a21)+~P1(x431,a20)+~P5(f16(a8,x431),a13)+P5(f9(a8,x431),a13)
% 241.71/242.64 [44]~P4(x441,a21)+~P1(x441,a18)+~P5(f16(a8,x441),a8)+P5(f9(a8,x441),a13)
% 241.71/242.64 [45]~P4(x451,a21)+~P1(x451,a6)+~P5(f16(a8,x451),a8)+P5(f9(a8,x451),a8)
% 241.71/242.64 [46]~P4(x461,a21)+~P1(x461,a18)+~P5(f16(a8,x461),a13)+P5(f9(a8,x461),a8)
% 241.71/242.64 [47]~P4(x471,a21)+~P1(x471,a20)+~P5(f16(a8,x471),a13)+P5(f9(a14,x471),a13)
% 241.71/242.64 [48]~P4(x481,a21)+~P1(x481,a6)+~P5(f16(a8,x481),a8)+P5(f9(a14,x481),a8)
% 241.71/242.64 [49]~P4(x491,a21)+~P1(x491,a18)+~P5(f9(a8,x491),a8)+P5(f16(a8,x491),a13)
% 241.71/242.64 [50]~P4(x501,a21)+~P1(x501,a18)+~P5(f9(a8,x501),a13)+P5(f16(a8,x501),a8)
% 241.71/242.64 [51]~P4(x511,a21)+~P1(x511,a6)+~P5(f9(x512,x511),a13)+P5(f16(a8,x511),a13)
% 241.71/242.64 [52]~P4(x521,a21)+~P1(x521,a20)+~P5(f9(x522,x521),a8)+P5(f16(a8,x521),a8)
% 241.71/242.64 [53]~P4(x531,a21)+~P1(x531,a6)+P5(f9(a14,x531),a13)+~P5(f16(a8,x531),a13)+P5(f9(a8,x531),a13)
% 241.71/242.64 [54]~P4(x541,a21)+~P1(x541,a20)+P5(f9(a14,x541),a8)+~P5(f16(a8,x541),a8)+P5(f9(a8,x541),a8)
% 241.71/242.64 [55]~P4(x551,a21)+~P1(x551,a20)+~P5(f9(a8,x551),a13)+~P5(f9(a14,x551),a13)+P5(f16(a8,x551),a13)
% 241.71/242.64 [56]~P4(x561,a21)+~P1(x561,a6)+~P5(f9(a8,x561),a8)+~P5(f9(a14,x561),a8)+P5(f16(a8,x561),a8)
% 241.71/242.64 %EqnAxiom
% 241.71/242.64
% 241.71/242.64 %-------------------------------------------
% 241.92/242.81 cnf(59,plain,
% 241.92/242.81 (~P1(f3(f10(a1)),x591)+P4(f3(f10(a1)),a21)),
% 241.92/242.81 inference(scs_inference,[],[9,2,21,18])).
% 241.92/242.81 cnf(198,plain,
% 241.92/242.81 (P1(f5(f10(a1)),a6)),
% 241.92/242.81 inference(scs_inference,[],[1,10,15])).
% 241.92/242.81 cnf(290,plain,
% 241.92/242.81 (P1(f17(f10(a1)),a18)),
% 241.92/242.81 inference(scs_inference,[],[1,12,15])).
% 241.92/242.81 cnf(336,plain,
% 241.92/242.82 (P1(f19(f12(a1)),a20)),
% 241.92/242.82 inference(scs_inference,[],[1,13,16])).
% 241.92/242.82 cnf(382,plain,
% 241.92/242.82 (P4(f19(a1),a4)+P4(f19(a1),a21)),
% 241.92/242.82 inference(scs_inference,[],[1,14,18])).
% 241.92/242.82 cnf(519,plain,
% 241.92/242.82 (P4(f19(a1),a21)+~P4(f5(f10(a1)),a4)),
% 241.92/242.82 inference(scs_inference,[],[22,382])).
% 241.92/242.82 cnf(565,plain,
% 241.92/242.82 (P4(f19(a1),a21)+~P4(f5(f12(a1)),a4)),
% 241.92/242.82 inference(scs_inference,[],[23,382])).
% 241.92/242.82 cnf(611,plain,
% 241.92/242.82 (P4(f19(a1),a21)+~P4(f17(f10(a1)),a4)),
% 241.92/242.82 inference(scs_inference,[],[24,382])).
% 241.92/242.82 cnf(657,plain,
% 241.92/242.82 (P4(f19(a1),a21)+~P4(f19(f12(a1)),a4)),
% 241.92/242.82 inference(scs_inference,[],[25,382])).
% 241.92/242.82 cnf(703,plain,
% 241.92/242.82 (P4(f5(f10(a1)),a21)+P4(f19(a1),a21)),
% 241.92/242.82 inference(scs_inference,[],[198,519,18])).
% 241.92/242.82 cnf(794,plain,
% 241.92/242.82 (P4(f17(f10(a1)),a21)+P4(f19(a1),a21)),
% 241.92/242.82 inference(scs_inference,[],[290,611,18])).
% 241.92/242.82 cnf(840,plain,
% 241.92/242.82 (P4(f19(f12(a1)),a21)+P4(f19(a1),a21)),
% 241.92/242.82 inference(scs_inference,[],[336,657,18])).
% 241.92/242.82 cnf(1024,plain,
% 241.92/242.82 (P4(f3(f10(a1)),a21)+~P1(f10(a1),a11)),
% 241.92/242.82 inference(scs_inference,[],[59,11])).
% 241.92/242.82 cnf(1070,plain,
% 241.92/242.82 (P4(f3(f10(a1)),a21)),
% 241.92/242.82 inference(scs_inference,[],[1,1024,15])).
% 241.92/242.82 cnf(1116,plain,
% 241.92/242.82 (P3(f9(a8,f12(a1)),f9(a8,f3(f12(a1))))),
% 241.92/242.82 inference(scs_inference,[],[1,26,16])).
% 241.92/242.82 cnf(1162,plain,
% 241.92/242.82 (P3(f9(a8,f10(a1)),f9(a8,f19(f10(a1))))),
% 241.92/242.82 inference(scs_inference,[],[1,27,15])).
% 241.92/242.82 cnf(1208,plain,
% 241.92/242.82 (P5(f9(a8,f12(a1)),a13)),
% 241.92/242.82 inference(scs_inference,[],[1,2,28,19])).
% 241.92/242.82 cnf(1254,plain,
% 241.92/242.82 (P5(f9(a8,f10(a1)),a8)),
% 241.92/242.82 inference(scs_inference,[],[1,3,29,19])).
% 241.92/242.82 cnf(1346,plain,
% 241.92/242.82 (P3(f9(a14,f10(a1)),f9(a14,f19(f10(a1))))),
% 241.92/242.82 inference(scs_inference,[],[1,31,15])).
% 241.92/242.82 cnf(1392,plain,
% 241.92/242.82 (P5(f9(a14,f10(a1)),a8)),
% 241.92/242.82 inference(scs_inference,[],[1,4,32,19])).
% 241.92/242.82 cnf(1438,plain,
% 241.92/242.82 (P3(f16(a15,f12(a1)),f16(a8,f5(f12(a1))))),
% 241.92/242.82 inference(scs_inference,[],[1,33,16])).
% 241.92/242.82 cnf(1484,plain,
% 241.92/242.82 (P5(f16(a15,f12(a1)),a8)),
% 241.92/242.82 inference(scs_inference,[],[1,5,34,19])).
% 241.92/242.82 cnf(1530,plain,
% 241.92/242.82 (P3(f16(a2,f10(a1)),f16(a8,f3(f10(a1))))),
% 241.92/242.82 inference(scs_inference,[],[1,35,15])).
% 241.92/242.82 cnf(1576,plain,
% 241.92/242.82 (P5(f16(a8,f19(a1)),a13)),
% 241.92/242.82 inference(scs_inference,[],[1,6,36,19])).
% 241.92/242.82 cnf(1579,plain,
% 241.92/242.82 (~P1(f19(a1),a20)+~P4(f19(a1),a21)+P5(f9(a14,f19(a1)),a13)),
% 241.92/242.82 inference(scs_inference,[],[4,1576,21,47])).
% 241.92/242.82 cnf(1668,plain,
% 241.92/242.82 (P3(f16(a8,f17(f10(a1))),f9(a14,f5(f10(a1))))),
% 241.92/242.82 inference(scs_inference,[],[1,38,15])).
% 241.92/242.82 cnf(1714,plain,
% 241.92/242.82 (P3(f16(a8,f19(f12(a1))),f9(a8,f5(f12(a1))))),
% 241.92/242.82 inference(scs_inference,[],[1,39,16])).
% 241.92/242.82 cnf(1806,plain,
% 241.92/242.82 (~P5(f9(a14,f19(a1)),x18061)+P5(f16(a2,f10(a1)),x18061)),
% 241.92/242.82 inference(scs_inference,[],[1,41,20])).
% 241.92/242.82 cnf(2036,plain,
% 241.92/242.82 (~P1(f19(a1),a20)+P5(f9(a14,f19(a1)),a13)+P4(f19(a1),a4)),
% 241.92/242.82 inference(scs_inference,[],[1579,382])).
% 241.92/242.82 cnf(2128,plain,
% 241.92/242.82 (P5(f9(a14,f19(a1)),a13)+P4(f19(a1),a4)),
% 241.92/242.82 inference(scs_inference,[],[1,2036,14])).
% 241.92/242.82 cnf(2174,plain,
% 241.92/242.82 (P5(f16(a2,f10(a1)),a13)+P4(f19(a1),a4)),
% 241.92/242.82 inference(scs_inference,[],[2128,1806])).
% 241.92/242.82 cnf(2768,plain,
% 241.92/242.82 (~P4(f19(a1),a4)+P4(f5(f10(a1)),a21)),
% 241.92/242.82 inference(scs_inference,[],[17,703])).
% 241.92/242.82 cnf(2814,plain,
% 241.92/242.82 (P5(f9(a14,f19(a1)),a13)+P4(f5(f10(a1)),a21)),
% 241.92/242.82 inference(scs_inference,[],[2768,2128])).
% 241.92/242.82 cnf(2860,plain,
% 241.92/242.82 (P5(f16(a2,f10(a1)),a13)+P4(f5(f10(a1)),a21)),
% 241.92/242.82 inference(scs_inference,[],[2814,1806])).
% 241.92/242.82 cnf(2952,plain,
% 241.92/242.82 (P5(f16(a2,f10(a1)),a13)+~P4(f19(a1),a21)),
% 241.92/242.82 inference(scs_inference,[],[17,2174])).
% 241.92/242.82 cnf(2998,plain,
% 241.92/242.82 (P5(f16(a2,f10(a1)),a13)+~P4(f5(f10(a1)),a4)),
% 241.92/242.82 inference(scs_inference,[],[2952,519])).
% 241.92/242.82 cnf(3090,plain,
% 241.92/242.82 (~P4(f19(a1),a4)+P4(f17(f10(a1)),a21)),
% 241.92/242.82 inference(scs_inference,[],[17,794])).
% 241.92/242.82 cnf(3136,plain,
% 241.92/242.82 (P5(f9(a14,f19(a1)),a13)+P4(f17(f10(a1)),a21)),
% 241.92/242.82 inference(scs_inference,[],[3090,2128])).
% 241.92/242.82 cnf(3182,plain,
% 241.92/242.82 (P5(f16(a2,f10(a1)),a13)+P4(f17(f10(a1)),a21)),
% 241.92/242.82 inference(scs_inference,[],[3136,1806])).
% 241.92/242.82 cnf(3458,plain,
% 241.92/242.82 (~P4(f19(a1),a4)+P4(f19(f12(a1)),a21)),
% 241.92/242.82 inference(scs_inference,[],[17,840])).
% 241.92/242.82 cnf(3504,plain,
% 241.92/242.82 (P5(f16(a2,f10(a1)),a13)+P4(f19(f12(a1)),a21)),
% 241.92/242.82 inference(scs_inference,[],[3458,2174])).
% 241.92/242.82 cnf(3688,plain,
% 241.92/242.82 (P5(f9(a14,f19(a1)),a13)+~P4(f17(f10(a1)),a4)),
% 241.92/242.82 inference(scs_inference,[],[17,3136])).
% 241.92/242.82 cnf(3734,plain,
% 241.92/242.82 (~P4(f17(f10(a1)),a4)+P5(f16(a2,f10(a1)),a13)),
% 241.92/242.82 inference(scs_inference,[],[3688,1806])).
% 241.92/242.82 cnf(3826,plain,
% 241.92/242.82 (P5(f16(a2,f10(a1)),a13)+~P4(f19(f12(a1)),a4)),
% 241.92/242.82 inference(scs_inference,[],[17,3504])).
% 241.92/242.82 cnf(4560,plain,
% 241.92/242.82 (P1(f5(f12(a1)),a6)),
% 241.92/242.82 inference(scs_inference,[],[1,10,16])).
% 241.92/242.82 cnf(4789,plain,
% 241.92/242.82 (P1(f3(f10(a1)),a6)),
% 241.92/242.82 inference(scs_inference,[],[1,11,15])).
% 241.92/242.82 cnf(5430,plain,
% 241.92/242.82 (P4(f19(x54301),a4)+P4(f19(x54301),a21)+~P1(x54301,a11)),
% 241.92/242.82 inference(scs_inference,[],[13,18])).
% 241.92/242.82 cnf(5476,plain,
% 241.92/242.82 (P4(f19(f10(a1)),a4)+P4(f19(f10(a1)),a21)),
% 241.92/242.82 inference(scs_inference,[],[1,5430,15])).
% 241.92/242.82 cnf(5613,plain,
% 241.92/242.82 (P1(f19(f10(a1)),a20)),
% 241.92/242.82 inference(scs_inference,[],[1,13,15])).
% 241.92/242.82 cnf(106823,plain,
% 241.92/242.82 (P1(f19(a1),a20)),
% 241.92/242.82 inference(scs_inference,[],[1,14])).
% 241.92/242.82 cnf(106825,plain,
% 241.92/242.82 (P1(f10(a1),a11)),
% 241.92/242.82 inference(scs_inference,[],[1,14,15])).
% 241.92/242.82 cnf(106829,plain,
% 241.92/242.82 (P3(f9(a8,f10(a1)),f9(a8,f3(f10(a1))))),
% 241.92/242.82 inference(scs_inference,[],[1,14,15,16,26])).
% 241.92/242.82 cnf(106831,plain,
% 241.92/242.82 (P3(f9(a8,f12(a1)),f9(a8,f19(f12(a1))))),
% 241.92/242.82 inference(scs_inference,[],[1,14,15,16,26,27])).
% 241.92/242.82 cnf(106837,plain,
% 241.92/242.82 (P3(f9(a14,f10(a1)),f9(a14,f3(f10(a1))))),
% 241.92/242.82 inference(scs_inference,[],[1,14,15,16,26,27,28,29,30])).
% 241.92/242.82 cnf(106839,plain,
% 241.92/242.82 (P3(f9(a14,f12(a1)),f9(a14,f19(f12(a1))))),
% 241.92/242.82 inference(scs_inference,[],[1,14,15,16,26,27,28,29,30,31])).
% 241.92/242.82 cnf(106843,plain,
% 241.92/242.82 (P3(f16(a15,f10(a1)),f16(a8,f5(f10(a1))))),
% 241.92/242.82 inference(scs_inference,[],[1,14,15,16,26,27,28,29,30,31,32,33])).
% 241.92/242.82 cnf(106851,plain,
% 241.92/242.82 (P3(f16(a15,f10(a1)),f9(a14,f12(a1)))),
% 241.92/242.82 inference(scs_inference,[],[1,14,15,16,26,27,28,29,30,31,32,33,34,35,36,40])).
% 241.92/242.82 cnf(106857,plain,
% 241.92/242.82 (P5(f9(a8,f3(f12(a1))),a13)),
% 241.92/242.82 inference(scs_inference,[],[1116,1,1208,14,15,16,26,27,28,29,30,31,32,33,34,35,36,40,41,42,19])).
% 241.92/242.82 cnf(106859,plain,
% 241.92/242.82 (~P5(f16(a2,a1),a8)),
% 241.92/242.82 inference(scs_inference,[],[8,1116,1,6,1208,14,15,16,26,27,28,29,30,31,32,33,34,35,36,40,41,42,19,21])).
% 241.92/242.82 cnf(106874,plain,
% 241.92/242.82 (~P5(f9(a2,a1),a13)),
% 241.92/242.82 inference(scs_inference,[],[7,106859,4,20,19,21])).
% 241.92/242.82 cnf(106885,plain,
% 241.92/242.82 (~P5(f9(a8,f3(f12(a1))),a8)),
% 241.92/242.82 inference(scs_inference,[],[106874,8,106857,20,19,21])).
% 241.92/242.82 cnf(106887,plain,
% 241.92/242.82 (P4(f5(f12(a1)),a21)+P4(f5(f12(a1)),a4)),
% 241.92/242.82 inference(scs_inference,[],[106874,4560,8,106857,20,19,21,18])).
% 241.92/242.82 cnf(106895,plain,
% 241.92/242.82 (~P5(f9(a14,a1),a13)),
% 241.92/242.82 inference(scs_inference,[],[106885,7,106874,106857,3,19,20,21])).
% 241.92/242.82 cnf(106904,plain,
% 241.92/242.82 (~P5(f16(a15,a1),a13)),
% 241.92/242.82 inference(scs_inference,[],[106895,7,106857,5,20,19,21])).
% 241.92/242.82 cnf(106928,plain,
% 241.92/242.82 (~P5(f9(a8,f12(a1)),a8)),
% 241.92/242.82 inference(scs_inference,[],[106885,8,106895,6,3,1208,20,19,21])).
% 241.92/242.82 cnf(106953,plain,
% 241.92/242.82 (~P5(f9(a8,a1),a8)),
% 241.92/242.82 inference(scs_inference,[],[106859,8,106874,106857,4,2,20,19,21])).
% 241.92/242.82 cnf(106960,plain,
% 241.92/242.82 (~P4(f19(f10(a1)),a21)+P5(f9(a8,f19(f10(a1))),a13)+~P5(f16(a8,f19(f10(a1))),a13)),
% 241.92/242.82 inference(scs_inference,[],[106953,5613,106904,106857,5,19,20,43])).
% 241.92/242.82 cnf(106977,plain,
% 241.92/242.82 (~P5(f16(a8,f19(a1)),a8)),
% 241.92/242.82 inference(scs_inference,[],[106859,8,106904,106857,5,1576,19,20,21])).
% 241.92/242.82 cnf(107002,plain,
% 241.92/242.82 (~P5(f9(a8,f10(a1)),a13)),
% 241.92/242.82 inference(scs_inference,[],[106977,7,106895,106857,3,1254,19,20,21])).
% 241.92/242.82 cnf(107032,plain,
% 241.92/242.82 (~P4(f5(f12(a1)),a21)+~P5(f9(x1070321,f5(f12(a1))),a13)+P5(f16(a8,f5(f12(a1))),a13)),
% 241.92/242.82 inference(scs_inference,[],[2,4560,107002,7,1392,19,20,21,51])).
% 241.92/242.82 cnf(107053,plain,
% 241.92/242.82 (~P5(f16(a15,f12(a1)),a13)),
% 241.92/242.82 inference(scs_inference,[],[2,106859,107002,7,5,1484,20,19,21])).
% 241.92/242.82 cnf(107493,plain,
% 241.92/242.82 (P4(f5(f12(a1)),a21)+~P4(f5(f12(a1)),a21)),
% 241.92/242.82 inference(scs_inference,[],[106887,17])).
% 241.92/242.82 cnf(108259,plain,
% 241.92/242.82 (~P4(f17(f10(a1)),a21)+P5(f16(a8,f17(f10(a1))),a13)+~P5(f9(a8,f17(f10(a1))),a8)),
% 241.92/242.82 inference(scs_inference,[],[290,106895,106857,19,20,49])).
% 241.92/242.82 cnf(109845,plain,
% 241.92/242.82 (P4(f19(f10(a1)),a4)+~P5(f16(a8,f19(f10(a1))),a13)+P5(f9(a8,f19(f10(a1))),a13)),
% 241.92/242.82 inference(scs_inference,[],[106960,5476])).
% 241.92/242.82 cnf(110225,plain,
% 241.92/242.82 (P4(f5(f12(a1)),a4)+P5(f16(a8,f5(f12(a1))),a13)+~P5(f9(x1102251,f5(f12(a1))),a13)),
% 241.92/242.82 inference(scs_inference,[],[107032,106887])).
% 241.92/242.82 cnf(111431,plain,
% 241.92/242.82 (~P5(f16(a15,f10(a1)),x1114311)+P5(f9(a14,f12(a1)),x1114311)),
% 241.92/242.82 inference(scs_inference,[],[106851,19])).
% 241.92/242.82 cnf(113055,plain,
% 241.92/242.82 (P4(f19(a1),a21)+P5(f16(a8,f5(f12(a1))),a13)+~P5(f9(x1130551,f5(f12(a1))),a13)),
% 241.92/242.82 inference(scs_inference,[],[110225,565])).
% 241.92/242.82 cnf(113099,plain,
% 241.92/242.82 (P5(f16(a8,f5(f12(a1))),a13)+~P5(f9(x1130991,f5(f12(a1))),a13)+P5(f9(a14,f19(a1)),a13)),
% 241.92/242.82 inference(scs_inference,[],[106823,1576,113055,47])).
% 241.92/242.82 cnf(127774,plain,
% 241.92/242.82 (P5(f9(a14,f3(f10(a1))),a8)),
% 241.92/242.82 inference(scs_inference,[],[106837,1392,19])).
% 241.92/242.82 cnf(127779,plain,
% 241.92/242.82 (~P5(f9(a14,f3(f10(a1))),a13)),
% 241.92/242.82 inference(scs_inference,[],[106837,1162,7,1392,107002,19,20,109845,21])).
% 241.92/242.82 cnf(127786,plain,
% 241.92/242.82 (~P5(f16(a8,f5(f12(a1))),a13)),
% 241.92/242.82 inference(scs_inference,[],[1346,1438,1392,107053,19,20])).
% 241.92/242.82 cnf(127794,plain,
% 241.92/242.82 (~P4(f5(f12(a1)),a21)+~P5(f9(x1277941,f5(f12(a1))),a13)),
% 241.92/242.82 inference(scs_inference,[],[127786,107032])).
% 241.92/242.82 cnf(127796,plain,
% 241.92/242.82 (P4(f5(f12(a1)),a4)+~P5(f9(x1277961,f5(f12(a1))),a13)),
% 241.92/242.82 inference(scs_inference,[],[127786,110225])).
% 241.92/242.82 cnf(127797,plain,
% 241.92/242.82 (P4(f19(a1),a21)+~P5(f9(x1277971,f5(f12(a1))),a13)),
% 241.92/242.82 inference(scs_inference,[],[127786,113055])).
% 241.92/242.82 cnf(127798,plain,
% 241.92/242.82 (P5(f9(a14,f19(a1)),a13)+~P5(f9(x1277981,f5(f12(a1))),a13)),
% 241.92/242.82 inference(scs_inference,[],[127786,113099])).
% 241.92/242.82 cnf(127803,plain,
% 241.92/242.82 (P5(f9(a8,f3(f10(a1))),a8)),
% 241.92/242.82 inference(scs_inference,[],[106829,1254,19])).
% 241.92/242.82 cnf(127805,plain,
% 241.92/242.82 (~P5(f9(a8,f19(f12(a1))),a8)),
% 241.92/242.82 inference(scs_inference,[],[106829,106831,1254,106928,19,20])).
% 241.92/242.82 cnf(127807,plain,
% 241.92/242.82 (P5(f16(a8,f3(f10(a1))),a8)),
% 241.92/242.82 inference(scs_inference,[],[106829,106831,127774,4789,1254,1070,106928,19,20,56])).
% 241.92/242.82 cnf(127815,plain,
% 241.92/242.82 (~P5(f16(a8,f3(f10(a1))),a13)),
% 241.92/242.82 inference(scs_inference,[],[127779,106829,106831,127774,4789,7,1254,1070,106928,19,20,56,21,44,43,53])).
% 241.92/242.82 cnf(127817,plain,
% 241.92/242.82 (~P5(f9(x1278171,f3(f10(a1))),a13)),
% 241.92/242.82 inference(scs_inference,[],[127779,106829,106831,127774,4789,7,1254,1070,106928,19,20,56,21,44,43,53,51])).
% 241.92/242.82 cnf(127826,plain,
% 241.92/242.82 (P4(f19(a1),a4)),
% 241.92/242.82 inference(scs_inference,[],[127807,127815,127817,1530,1070,19,20,44,2174])).
% 241.92/242.82 cnf(127827,plain,
% 241.92/242.82 (~P4(f19(a1),a21)),
% 241.92/242.82 inference(scs_inference,[],[127807,127815,127817,1530,1070,19,20,44,2174,2952])).
% 241.92/242.82 cnf(127828,plain,
% 241.92/242.82 (P4(f5(f10(a1)),a21)),
% 241.92/242.82 inference(scs_inference,[],[127807,127815,127817,1530,1070,19,20,44,2174,2952,2860])).
% 241.92/242.82 cnf(127830,plain,
% 241.92/242.82 (P4(f17(f10(a1)),a21)),
% 241.92/242.82 inference(scs_inference,[],[127807,127815,127817,1530,1070,19,20,44,2174,2952,2860,2998,3182])).
% 241.92/242.82 cnf(127831,plain,
% 241.92/242.82 (P4(f19(f12(a1)),a21)),
% 241.92/242.82 inference(scs_inference,[],[127807,127815,127817,1530,1070,19,20,44,2174,2952,2860,2998,3182,3504])).
% 241.92/242.82 cnf(127834,plain,
% 241.92/242.82 (~P5(f9(a14,f19(a1)),a13)),
% 241.92/242.82 inference(scs_inference,[],[127807,127815,127817,1530,1070,19,20,44,2174,2952,2860,2998,3182,3504,3734,3826,1806])).
% 241.92/242.82 cnf(127845,plain,
% 241.92/242.82 (~P4(f5(f12(a1)),a4)),
% 241.92/242.82 inference(scs_inference,[],[127826,23])).
% 241.92/242.82 cnf(127862,plain,
% 241.92/242.82 (~P5(f9(a8,f17(f10(a1))),a8)+P5(f16(a8,f17(f10(a1))),a13)),
% 241.92/242.82 inference(scs_inference,[],[127830,108259])).
% 241.92/242.82 cnf(127892,plain,
% 241.92/242.82 (~P5(f9(x1278921,f5(f12(a1))),a13)),
% 241.92/242.82 inference(scs_inference,[],[127827,127797])).
% 241.92/242.82 cnf(127893,plain,
% 241.92/242.82 (~P5(f9(x1278931,f5(f12(a1))),a13)),
% 241.92/242.82 inference(scs_inference,[],[127834,127798])).
% 241.92/242.82 cnf(127900,plain,
% 241.92/242.82 (~P5(f9(a14,f19(f12(a1))),x1279001)+P5(f9(a14,f12(a1)),x1279001)),
% 241.92/242.82 inference(scs_inference,[],[106839,127817,1162,127807,1254,1070,19,44,20])).
% 241.92/242.82 cnf(127905,plain,
% 241.92/242.82 (P4(f5(f12(a1)),a21)),
% 241.92/242.82 inference(scs_inference,[],[127845,106887])).
% 241.92/242.82 cnf(127908,plain,
% 241.92/242.82 (~P5(f9(x1279081,f5(f12(a1))),a13)),
% 241.92/242.82 inference(scs_inference,[],[127845,127796])).
% 241.92/242.82 cnf(127909,plain,
% 241.92/242.82 (~P5(f16(a8,f19(f12(a1))),a13)),
% 241.92/242.82 inference(scs_inference,[],[127892,1714,19])).
% 241.92/242.82 cnf(127917,plain,
% 241.92/242.82 (P5(f16(a15,f10(a1)),a13)+~P5(f9(x1279171,f5(f10(a1))),a13)),
% 241.92/242.82 inference(scs_inference,[],[127892,106843,1714,127828,127817,127807,1070,198,19,44,20,51])).
% 241.92/242.82 cnf(127922,plain,
% 241.92/242.82 (P4(f5(f12(a1)),a21)),
% 241.92/242.82 inference(scs_inference,[],[127905,107493])).
% 241.92/242.82 cnf(127923,plain,
% 241.92/242.82 (~P5(f9(x1279231,f5(f12(a1))),a13)),
% 241.92/242.82 inference(scs_inference,[],[127905,127794])).
% 241.92/242.82 cnf(127924,plain,
% 241.92/242.82 (P5(f16(a8,f5(f12(a1))),a8)),
% 241.92/242.82 inference(scs_inference,[],[1438,1484,19])).
% 241.92/242.82 cnf(127931,plain,
% 241.92/242.82 (P5(f9(a8,f5(f12(a1))),a8)),
% 241.92/242.82 inference(scs_inference,[],[127905,127803,127893,1438,127815,1484,1070,4560,19,44,49,45])).
% 241.92/242.82 cnf(127944,plain,
% 241.92/242.82 (P5(f9(a8,f19(f12(a1))),a13)),
% 241.92/242.82 inference(scs_inference,[],[127931,106831,1714,1208,20,19])).
% 241.92/242.82 cnf(127957,plain,
% 241.92/242.82 (P5(f9(a14,f12(a1)),a8)),
% 241.92/242.82 inference(scs_inference,[],[127922,127909,127931,127805,127924,127923,106831,1714,127803,127831,127815,336,1070,1208,20,19,51,44,49,54,55,127900])).
% 241.92/242.82 cnf(127963,plain,
% 241.92/242.82 (~P5(f9(x1279631,f5(f10(a1))),a13)),
% 241.92/242.82 inference(scs_inference,[],[127922,127909,127931,127805,127924,127923,106831,1714,127803,127831,127815,7,336,1070,1208,20,19,51,44,49,54,55,127900,21,111431,127917])).
% 241.92/242.82 cnf(127992,plain,
% 241.92/242.82 (~P5(f9(a8,f17(f10(a1))),a8)),
% 241.92/242.82 inference(scs_inference,[],[1668,127963,127908,127957,127944,106851,127922,127924,127909,127803,127815,127831,1070,20,19,51,44,49,127862])).
% 241.92/242.82 cnf(249297,plain,
% 241.92/242.82 (P3(f16(a8,f3(f10(a1))),f9(a8,f17(f10(a1))))),
% 241.92/242.82 inference(scs_inference,[],[106825,37])).
% 241.92/242.82 cnf(277514,plain,
% 241.92/242.82 ($false),
% 241.92/242.82 inference(scs_inference,[],[249297,127807,127992,19]),
% 241.92/242.82 ['proof']).
% 242.12/242.98 % SZS output end Proof
% 242.12/242.98 % Total time :241.000000s
%------------------------------------------------------------------------------