%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : HWV006-2 : TPTP v8.2.0. Bugfixed v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n019.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.81s 241.97s
% Output : CNFRefutation 242.76s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : HWV006-2 : TPTP v8.2.0. Bugfixed v2.7.0.
% 0.03/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.11/0.33 % Computer : n019.cluster.edu
% 0.11/0.33 % Model : x86_64 x86_64
% 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.33 % Memory : 8042.1875MB
% 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.33 % CPULimit : 300
% 0.11/0.33 % WCLimit : 300
% 0.11/0.33 % DateTime : Fri Jun 21 00:27:24 EDT 2024
% 0.11/0.33 % CPUTime :
% 0.51/0.59 start to proof:theBenchmark
% 241.71/241.93 %-------------------------------------------
% 241.71/241.93 % File :CSE---1.7
% 241.71/241.93 % Problem :theBenchmark
% 241.71/241.93 % Transform :cnf
% 241.71/241.93 % Format :tptp:raw
% 241.71/241.93 % Command :java -jar mcs_scs.jar %d %s
% 241.71/241.93
% 241.71/241.93 % Result :Theorem 241.050000s
% 241.71/241.93 % Output :CNFRefutation 241.050000s
% 241.71/241.93 %-------------------------------------------
% 241.76/241.97 %--------------------------------------------------------------------------
% 241.76/241.97 % File : HWV006-2 : TPTP v8.2.0. Bugfixed v2.7.0.
% 241.76/241.97 % Domain : Hardware Verification
% 241.76/241.97 % Problem : A fulladder built from two halfadders and an or gate
% 241.76/241.97 % Version : [Gei96] axioms.
% 241.76/241.97 % English :
% 241.76/241.97
% 241.76/241.97 % Refs : [Gei96] Geisler (1996), Email to G. Sutcliffe
% 241.76/241.97 % Source : [Gei96]
% 241.76/241.97 % Names :
% 241.76/241.97
% 241.76/241.97 % Status : Unsatisfiable
% 241.76/241.97 % Rating : 0.00 v7.1.0, 0.17 v7.0.0, 0.12 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.10 v5.1.0, 0.09 v5.0.0, 0.14 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
% 241.76/241.97 % Syntax : Number of clauses : 64 ( 11 unt; 5 nHn; 64 RR)
% 241.76/241.97 % Number of literals : 144 ( 0 equ; 86 neg)
% 241.76/241.97 % Maximal clause size : 4 ( 2 avg)
% 241.76/241.97 % Maximal term depth : 3 ( 2 avg)
% 241.76/241.97 % Number of predicates : 12 ( 12 usr; 0 prp; 1-2 aty)
% 241.76/241.97 % Number of functors : 13 ( 13 usr; 1 con; 0-1 aty)
% 241.76/241.97 % Number of variables : 55 ( 0 sgn)
% 241.76/241.97 % SPC : CNF_UNS_RFO_NEQ_NHN
% 241.76/241.97
% 241.76/241.97 % Comments :
% 241.76/241.97 % Bugfixes : v2.7.0 - Bugfix in HWV002-0.ax
% 241.76/241.97 %--------------------------------------------------------------------------
% 241.76/241.97 %----Include basic diagnosis axioms
% 241.76/241.97 include('Axioms/HWV002-0.ax').
% 241.76/241.97 %----Include model of halfadder
% 241.76/241.97 include('Axioms/HWV002-1.ax').
% 241.76/241.97 %----Include model of fulladder
% 241.76/241.97 include('Axioms/HWV002-2.ax').
% 241.76/241.97 %--------------------------------------------------------------------------
% 241.76/241.97 %----Observations
% 241.76/241.97 cnf(f_isa_fulladder,hypothesis,
% 241.76/241.97 fulladder(f) ).
% 241.76/241.97
% 241.76/241.97 cnf(in1_1,hypothesis,
% 241.76/241.97 one(in1(f)) ).
% 241.76/241.97
% 241.76/241.97 cnf(in2_0,hypothesis,
% 241.76/241.97 zero(in2(f)) ).
% 241.76/241.97
% 241.76/241.97 cnf(inc_1,hypothesis,
% 241.76/241.97 one(inc(f)) ).
% 241.76/241.97
% 241.76/241.97 cnf(outs_1,hypothesis,
% 241.76/241.97 one(outs(f)) ).
% 241.76/241.97
% 241.76/241.97 cnf(outc_0,hypothesis,
% 241.76/241.97 zero(outc(f)) ).
% 241.76/241.97
% 241.76/241.97 %----Minimal diagnosis
% 241.76/241.97 cnf(diagnosis_or1_not1h2,negated_conjecture,
% 241.76/241.97 ( ~ abnormal(or1(f))
% 241.76/241.97 | ~ abnormal(not1(h2(f))) ) ).
% 241.76/241.97
% 241.76/241.97 cnf(diagnosis_and2,negated_conjecture,
% 241.76/241.97 ~ abnormal(and2(h2(f))) ).
% 241.76/241.97
% 241.76/241.97 cnf(diagnosis_or1_and1h2,negated_conjecture,
% 241.76/241.97 ( ~ abnormal(or1(f))
% 241.76/241.97 | ~ abnormal(and1(h2(f))) ) ).
% 241.76/241.97
% 241.76/241.97 cnf(diagnosis_or1h1,negated_conjecture,
% 241.76/241.97 ~ abnormal(or1(h1(f))) ).
% 241.76/241.97
% 241.76/241.97 cnf(diagnosis_not1h1,negated_conjecture,
% 241.76/241.97 ~ abnormal(not1(h1(f))) ).
% 241.76/241.97
% 241.76/241.97 cnf(diagnosis_and2h1,negated_conjecture,
% 241.76/241.97 ~ abnormal(and2(h1(f))) ).
% 241.76/241.97
% 241.81/241.97 cnf(diagnosis_and1h1,negated_conjecture,
% 241.81/241.97 ~ abnormal(and1(h1(f))) ).
% 241.81/241.97
% 241.81/241.97 %--------------------------------------------------------------------------
% 241.81/241.97 %-------------------------------------------
% 241.81/241.97 % Proof found
% 241.81/241.97 % SZS status Theorem for theBenchmark
% 241.81/241.97 % SZS output start Proof
% 241.83/242.01 %ClaNum:64(EqnAxiom:0)
% 241.83/242.01 %VarNum:150(SingletonVarNum:55)
% 241.83/242.01 %MaxLitNum:4
% 241.83/242.01 %MaxfuncDepth:2
% 241.83/242.01 %SharedTerms:26
% 241.83/242.01 %goalClause: 7 8 9 10 11 42 43
% 241.83/242.01 %singleGoalClaCount:5
% 241.83/242.01 [1]P1(a1)
% 241.83/242.01 [2]P5(f4(a1))
% 241.83/242.01 [3]P5(f8(a1))
% 241.83/242.01 [4]P6(f5(a1))
% 241.83/242.01 [5]P6(f13(a1))
% 241.83/242.01 [6]P6(f9(a1))
% 241.83/242.01 [7]~P2(f2(f6(a1)))
% 241.83/242.01 [8]~P2(f3(f6(a1)))
% 241.83/242.01 [9]~P2(f3(f7(a1)))
% 241.83/242.01 [10]~P2(f10(f6(a1)))
% 241.83/242.01 [11]~P2(f11(f6(a1)))
% 241.83/242.01 [42]~P2(f11(a1))+~P2(f2(f7(a1)))
% 241.83/242.01 [43]~P2(f10(f7(a1)))+~P2(f11(a1))
% 241.83/242.01 [12]~P6(x121)+~P5(x121)
% 241.83/242.01 [13]~P2(x131)+~P3(x131)
% 241.83/242.01 [14]~P12(x141)+~P2(x141)
% 241.83/242.01 [15]~P7(x151)+~P2(x151)
% 241.83/242.01 [19]~P9(x191)+P8(f2(x191))
% 241.83/242.01 [20]~P9(x201)+P8(f3(x201))
% 241.83/242.01 [21]~P9(x211)+P10(f11(x211))
% 241.83/242.01 [22]~P1(x221)+P10(f11(x221))
% 241.83/242.01 [23]~P9(x231)+P11(f10(x231))
% 241.83/242.01 [24]~P1(x241)+P9(f6(x241))
% 241.83/242.01 [25]~P1(x251)+P9(f7(x251))
% 241.83/242.01 [46]~P9(x461)+P4(f5(x461),f5(f3(x461)))
% 241.83/242.01 [47]~P9(x471)+P4(f5(x471),f5(f11(x471)))
% 241.83/242.01 [48]~P1(x481)+P4(f5(x481),f5(f7(x481)))
% 241.83/242.01 [49]~P1(x491)+P4(f4(x491),f5(f6(x491)))
% 241.83/242.01 [50]~P9(x501)+P4(f4(x501),f4(f3(x501)))
% 241.83/242.01 [51]~P9(x511)+P4(f4(x511),f4(f11(x511)))
% 241.83/242.01 [52]~P9(x521)+P4(f13(x521),f12(f2(x521)))
% 241.83/242.01 [53]~P1(x531)+P4(f13(x531),f13(f7(x531)))
% 241.83/242.01 [54]~P9(x541)+P4(f8(x541),f12(f3(x541)))
% 241.83/242.01 [55]~P1(x551)+P4(f8(x551),f12(f11(x551)))
% 241.83/242.01 [56]~P1(x561)+P4(f9(x561),f4(f6(x561)))
% 241.83/242.01 [59]~P9(x591)+P4(f12(f3(x591)),f5(f10(x591)))
% 241.83/242.01 [60]~P9(x601)+P4(f12(f10(x601)),f4(f2(x601)))
% 241.83/242.01 [61]~P9(x611)+P4(f12(f11(x611)),f5(f2(x611)))
% 241.83/242.01 [62]~P1(x621)+P4(f13(f6(x621)),f4(f7(x621)))
% 241.83/242.01 [63]~P1(x631)+P4(f8(f6(x631)),f4(f11(x631)))
% 241.83/242.01 [64]~P1(x641)+P4(f8(f7(x641)),f5(f11(x641)))
% 241.83/242.01 [16]P2(x161)+~P8(x161)+P3(x161)
% 241.83/242.01 [17]P12(x171)+~P10(x171)+P2(x171)
% 241.83/242.01 [18]P7(x181)+~P11(x181)+P2(x181)
% 241.83/242.01 [30]~P12(x301)+~P5(f12(x301))+P5(f5(x301))
% 241.83/242.01 [31]~P7(x311)+~P6(f12(x311))+P5(f5(x311))
% 241.83/242.01 [32]~P3(x321)+~P5(f5(x321))+P5(f12(x321))
% 241.83/242.01 [33]~P3(x331)+~P5(f4(x331))+P5(f12(x331))
% 241.83/242.01 [34]~P7(x341)+~P6(f5(x341))+P5(f12(x341))
% 241.83/242.01 [35]~P12(x351)+~P5(f12(x351))+P5(f4(x351))
% 241.83/242.01 [36]~P3(x361)+~P6(f12(x361))+P6(f5(x361))
% 241.83/242.01 [37]~P7(x371)+~P5(f12(x371))+P6(f5(x371))
% 241.83/242.01 [38]~P12(x381)+~P6(f5(x381))+P6(f12(x381))
% 241.83/242.02 [39]~P12(x391)+~P6(f4(x391))+P6(f12(x391))
% 241.83/242.02 [40]~P7(x401)+~P5(f5(x401))+P6(f12(x401))
% 241.83/242.02 [41]~P3(x411)+~P6(f12(x411))+P6(f4(x411))
% 241.83/242.02 [26]~P4(x262,x261)+P5(x261)+~P5(x262)
% 241.83/242.02 [27]~P4(x271,x272)+P5(x271)+~P5(x272)
% 241.83/242.02 [28]~P4(x282,x281)+P6(x281)+~P6(x282)
% 241.83/242.02 [29]~P4(x291,x292)+P6(x291)+~P6(x292)
% 241.83/242.02 [44]~P3(x441)+P5(f4(x441))+~P5(f12(x441))+P5(f5(x441))
% 241.83/242.02 [45]~P12(x451)+P6(f4(x451))+~P6(f12(x451))+P6(f5(x451))
% 241.83/242.02 [57]~P12(x571)+~P5(f5(x571))+~P5(f4(x571))+P5(f12(x571))
% 241.83/242.02 [58]~P3(x581)+~P6(f5(x581))+~P6(f4(x581))+P6(f12(x581))
% 241.83/242.02 %EqnAxiom
% 241.83/242.02
% 241.83/242.02 %-------------------------------------------
% 242.27/242.50 cnf(65,plain,
% 242.27/242.50 (~P6(f4(a1))),
% 242.27/242.50 inference(scs_inference,[],[2,12])).
% 242.27/242.50 cnf(74,plain,
% 242.27/242.50 (~P6(f8(a1))),
% 242.27/242.50 inference(scs_inference,[],[3,12])).
% 242.27/242.50 cnf(463,plain,
% 242.27/242.50 (P8(f2(f6(a1)))),
% 242.27/242.50 inference(scs_inference,[],[1,19,24])).
% 242.27/242.50 cnf(464,plain,
% 242.27/242.50 (P3(f2(f6(a1)))),
% 242.27/242.50 inference(scs_inference,[],[7,463,16])).
% 242.27/242.50 cnf(541,plain,
% 242.27/242.50 (P8(f3(f7(a1)))),
% 242.27/242.50 inference(scs_inference,[],[1,20,25])).
% 242.27/242.50 cnf(542,plain,
% 242.27/242.50 (P3(f3(f7(a1)))),
% 242.27/242.50 inference(scs_inference,[],[9,541,16])).
% 242.27/242.50 cnf(619,plain,
% 242.27/242.50 (P10(f11(f6(a1)))),
% 242.27/242.50 inference(scs_inference,[],[1,21,24])).
% 242.27/242.50 cnf(620,plain,
% 242.27/242.50 (P12(f11(f6(a1)))),
% 242.27/242.50 inference(scs_inference,[],[11,619,17])).
% 242.27/242.50 cnf(697,plain,
% 242.27/242.50 (P2(f11(a1))+P12(f11(a1))),
% 242.27/242.50 inference(scs_inference,[],[1,22,17])).
% 242.27/242.50 cnf(773,plain,
% 242.27/242.50 (P11(f10(f7(a1)))),
% 242.27/242.50 inference(scs_inference,[],[1,23,25])).
% 242.27/242.50 cnf(778,plain,
% 242.27/242.50 (P2(f10(f7(a1)))+P7(f10(f7(a1)))),
% 242.27/242.50 inference(scs_inference,[],[773,65,4,28,29,18])).
% 242.27/242.50 cnf(780,plain,
% 242.27/242.50 (~P12(f10(f7(a1)))+P7(f10(f7(a1)))),
% 242.27/242.50 inference(scs_inference,[],[773,65,4,28,29,18,14])).
% 242.27/242.50 cnf(1235,plain,
% 242.27/242.50 (P12(f11(a1))+~P2(f2(f7(a1)))),
% 242.27/242.50 inference(scs_inference,[],[697,42])).
% 242.27/242.50 cnf(1311,plain,
% 242.27/242.50 (P7(f10(f7(a1)))+~P2(f11(a1))),
% 242.27/242.50 inference(scs_inference,[],[43,778])).
% 242.27/242.50 cnf(1387,plain,
% 242.27/242.50 (~P5(f12(f11(a1)))+P5(f5(f11(a1)))+~P2(f2(f7(a1)))),
% 242.27/242.50 inference(scs_inference,[],[1235,30])).
% 242.27/242.50 cnf(1539,plain,
% 242.27/242.50 (P4(f5(f6(a1)),f5(f3(f6(a1))))),
% 242.27/242.50 inference(scs_inference,[],[1,46,24])).
% 242.27/242.50 cnf(1615,plain,
% 242.27/242.50 (P4(f5(f7(a1)),f5(f11(f7(a1))))),
% 242.27/242.50 inference(scs_inference,[],[1,47,25])).
% 242.27/242.50 cnf(1691,plain,
% 242.27/242.50 (P6(f5(f7(a1)))),
% 242.27/242.50 inference(scs_inference,[],[1,4,48,28])).
% 242.27/242.50 cnf(2077,plain,
% 242.27/242.50 (P4(f4(f6(a1)),f4(f3(f6(a1))))),
% 242.27/242.50 inference(scs_inference,[],[1,50,24])).
% 242.27/242.50 cnf(2153,plain,
% 242.27/242.50 (P4(f4(f7(a1)),f4(f11(f7(a1))))),
% 242.27/242.50 inference(scs_inference,[],[1,51,25])).
% 242.27/242.50 cnf(2229,plain,
% 242.27/242.50 (P4(f13(f6(a1)),f12(f2(f6(a1))))),
% 242.27/242.50 inference(scs_inference,[],[1,52,24])).
% 242.27/242.50 cnf(2305,plain,
% 242.27/242.50 (P6(f13(f7(a1)))),
% 242.27/242.50 inference(scs_inference,[],[1,5,53,28])).
% 242.27/242.50 cnf(2381,plain,
% 242.27/242.50 (P4(f8(f7(a1)),f12(f3(f7(a1))))),
% 242.27/242.50 inference(scs_inference,[],[1,54,25])).
% 242.27/242.50 cnf(2457,plain,
% 242.27/242.50 (P5(f12(f11(a1)))),
% 242.27/242.50 inference(scs_inference,[],[1,3,55,26])).
% 242.27/242.50 cnf(2458,plain,
% 242.27/242.50 (P5(f5(f11(a1)))+~P2(f2(f7(a1)))),
% 242.27/242.50 inference(scs_inference,[],[2457,1387])).
% 242.27/242.50 cnf(2459,plain,
% 242.27/242.50 (~P6(f12(f11(a1)))),
% 242.27/242.50 inference(scs_inference,[],[2457,12])).
% 242.27/242.50 cnf(2474,plain,
% 242.27/242.50 (~P12(f11(a1))+P5(f4(f11(a1)))),
% 242.27/242.50 inference(scs_inference,[],[2459,2457,4,28,29,35])).
% 242.27/242.50 cnf(2483,plain,
% 242.27/242.50 (~P12(f11(a1))+P5(f5(f11(a1)))),
% 242.27/242.50 inference(scs_inference,[],[2457,2459,4,29,28,30])).
% 242.27/242.50 cnf(2771,plain,
% 242.36/242.50 (P5(x27711)+~P4(x27711,f4(f11(a1)))+~P12(f11(a1))),
% 242.36/242.50 inference(scs_inference,[],[2474,27])).
% 242.36/242.50 cnf(3227,plain,
% 242.36/242.50 (P6(f4(f6(a1)))),
% 242.36/242.50 inference(scs_inference,[],[1,6,56,28])).
% 242.36/242.50 cnf(3535,plain,
% 242.36/242.50 (~P12(f10(f7(a1)))+~P6(f5(f10(f7(a1))))+P5(f12(f10(f7(a1))))),
% 242.36/242.50 inference(scs_inference,[],[780,34])).
% 242.36/242.50 cnf(3686,plain,
% 242.36/242.50 (P4(f12(f3(f6(a1))),f5(f10(f6(a1))))),
% 242.36/242.50 inference(scs_inference,[],[1,59,24])).
% 242.36/242.50 cnf(3762,plain,
% 242.36/242.50 (P4(f12(f10(f7(a1))),f4(f2(f7(a1))))),
% 242.36/242.50 inference(scs_inference,[],[1,60,25])).
% 242.36/242.50 cnf(3838,plain,
% 242.36/242.50 (P4(f12(f11(f6(a1))),f5(f2(f6(a1))))),
% 242.36/242.50 inference(scs_inference,[],[1,61,24])).
% 242.36/242.50 cnf(16907,plain,
% 242.36/242.51 (~P5(f5(f7(a1)))),
% 242.36/242.51 inference(scs_inference,[],[1691,12])).
% 242.36/242.51 cnf(16919,plain,
% 242.36/242.51 (~P5(f4(f6(a1)))),
% 242.36/242.51 inference(scs_inference,[],[3227,12])).
% 242.36/242.51 cnf(16930,plain,
% 242.36/242.51 (~P5(f13(f7(a1)))),
% 242.36/242.51 inference(scs_inference,[],[2305,12])).
% 242.36/242.51 cnf(16941,plain,
% 242.36/242.51 (~P5(f9(a1))),
% 242.36/242.51 inference(scs_inference,[],[6,12])).
% 242.36/242.51 cnf(16952,plain,
% 242.36/242.51 (~P5(f13(a1))),
% 242.36/242.51 inference(scs_inference,[],[5,12])).
% 242.36/242.51 cnf(49116,plain,
% 242.36/242.51 (P3(f3(f6(a1)))+~P8(f3(f6(a1)))),
% 242.36/242.51 inference(scs_inference,[],[8,2457,65,16952,3227,29,28,27,26,16])).
% 242.36/242.51 cnf(49290,plain,
% 242.36/242.51 (~P8(f3(f6(a1)))+~P5(f5(f3(f6(a1))))+P5(f12(f3(f6(a1))))),
% 242.36/242.51 inference(scs_inference,[],[49116,32])).
% 242.36/242.51 cnf(51350,plain,
% 242.36/242.51 (~P11(f10(f6(a1)))+P7(f10(f6(a1)))),
% 242.36/242.51 inference(scs_inference,[],[10,2457,65,16919,2305,29,28,27,26,18])).
% 242.36/242.51 cnf(51352,plain,
% 242.36/242.51 (~P9(f6(a1))+P7(f10(f6(a1)))),
% 242.36/242.51 inference(scs_inference,[],[10,2457,65,16919,2305,29,28,27,26,18,23])).
% 242.36/242.51 cnf(51446,plain,
% 242.36/242.51 (~P9(f6(a1))+~P6(f12(f10(f6(a1))))+P5(f5(f10(f6(a1))))),
% 242.36/242.51 inference(scs_inference,[],[51352,31])).
% 242.36/242.51 cnf(311828,plain,
% 242.36/242.51 (P9(f7(a1))),
% 242.36/242.51 inference(scs_inference,[],[1,22,25])).
% 242.36/242.51 cnf(311830,plain,
% 242.36/242.51 (P4(f5(f7(a1)),f5(f3(f7(a1))))),
% 242.36/242.51 inference(scs_inference,[],[1,22,25,46])).
% 242.36/242.51 cnf(311836,plain,
% 242.36/242.51 (P4(f4(f7(a1)),f4(f3(f7(a1))))),
% 242.36/242.51 inference(scs_inference,[],[1,22,25,46,48,49,50])).
% 242.36/242.51 cnf(311838,plain,
% 242.36/242.51 (P4(f13(f7(a1)),f12(f2(f7(a1))))),
% 242.36/242.51 inference(scs_inference,[],[1,22,25,46,48,49,50,52])).
% 242.36/242.51 cnf(311846,plain,
% 242.36/242.51 (P4(f13(f6(a1)),f4(f7(a1)))),
% 242.36/242.51 inference(scs_inference,[],[1,22,25,46,48,49,50,52,53,55,56,62])).
% 242.36/242.51 cnf(311848,plain,
% 242.36/242.51 (P4(f8(f6(a1)),f4(f11(a1)))),
% 242.36/242.51 inference(scs_inference,[],[1,22,25,46,48,49,50,52,53,55,56,62,63])).
% 242.36/242.51 cnf(311850,plain,
% 242.36/242.51 (P4(f8(f7(a1)),f5(f11(a1)))),
% 242.36/242.51 inference(scs_inference,[],[1,22,25,46,48,49,50,52,53,55,56,62,63,64])).
% 242.36/242.51 cnf(311852,plain,
% 242.36/242.51 (P9(f6(a1))),
% 242.36/242.51 inference(scs_inference,[],[1,22,25,46,48,49,50,52,53,55,56,62,63,64,24])).
% 242.36/242.51 cnf(311854,plain,
% 242.36/242.51 (P5(f5(f6(a1)))),
% 242.36/242.51 inference(scs_inference,[],[1,2,22,25,46,48,49,50,52,53,55,56,62,63,64,24,26])).
% 242.36/242.51 cnf(311856,plain,
% 242.36/242.51 (~P5(f5(f11(f7(a1))))),
% 242.36/242.51 inference(scs_inference,[],[1615,1,2,16907,22,25,46,48,49,50,52,53,55,56,62,63,64,24,26,27])).
% 242.36/242.51 cnf(311862,plain,
% 242.36/242.51 (P8(f2(f7(a1)))),
% 242.36/242.51 inference(scs_inference,[],[1615,2077,1,2459,2,3227,4,16907,22,25,46,48,49,50,52,53,55,56,62,63,64,24,26,27,29,28,19])).
% 242.36/242.51 cnf(311864,plain,
% 242.36/242.51 (P8(f3(f6(a1)))),
% 242.36/242.51 inference(scs_inference,[],[1615,2077,1,2459,2,3227,4,16907,22,25,46,48,49,50,52,53,55,56,62,63,64,24,26,27,29,28,19,20])).
% 242.36/242.51 cnf(311868,plain,
% 242.36/242.51 (P4(f5(f6(a1)),f5(f11(f6(a1))))),
% 242.36/242.51 inference(scs_inference,[],[1615,2077,1,2459,2,3227,4,16907,22,25,46,48,49,50,52,53,55,56,62,63,64,24,26,27,29,28,19,20,21,47])).
% 242.36/242.51 cnf(311870,plain,
% 242.36/242.51 (P4(f4(f6(a1)),f4(f11(f6(a1))))),
% 242.36/242.51 inference(scs_inference,[],[1615,2077,1,2459,2,3227,4,16907,22,25,46,48,49,50,52,53,55,56,62,63,64,24,26,27,29,28,19,20,21,47,51])).
% 242.36/242.51 cnf(311872,plain,
% 242.36/242.51 (P4(f8(f6(a1)),f12(f3(f6(a1))))),
% 242.36/242.51 inference(scs_inference,[],[1615,2077,1,2459,2,3227,4,16907,22,25,46,48,49,50,52,53,55,56,62,63,64,24,26,27,29,28,19,20,21,47,51,54])).
% 242.36/242.51 cnf(311874,plain,
% 242.36/242.51 (P3(f3(f6(a1)))),
% 242.36/242.51 inference(scs_inference,[],[1615,2077,1,2459,2,3227,4,16907,22,25,46,48,49,50,52,53,55,56,62,63,64,24,26,27,29,28,19,20,21,47,51,54,49116])).
% 242.36/242.51 cnf(311875,plain,
% 242.36/242.51 (P11(f10(f6(a1)))),
% 242.36/242.51 inference(scs_inference,[],[1615,2077,1,2459,2,3227,4,16907,22,25,46,48,49,50,52,53,55,56,62,63,64,24,26,27,29,28,19,20,21,47,51,54,49116,23])).
% 242.36/242.51 cnf(311877,plain,
% 242.36/242.51 (~P5(f4(f3(f6(a1))))),
% 242.36/242.51 inference(scs_inference,[],[1615,2077,1,2459,2,3227,4,16907,22,25,46,48,49,50,52,53,55,56,62,63,64,24,26,27,29,28,19,20,21,47,51,54,49116,23,12])).
% 242.36/242.51 cnf(311886,plain,
% 242.36/242.51 (P5(f12(f3(f6(a1))))+~P5(f5(f3(f6(a1))))),
% 242.36/242.51 inference(scs_inference,[],[311864,49290])).
% 242.36/242.51 cnf(311887,plain,
% 242.36/242.51 (P7(f10(f6(a1)))),
% 242.36/242.51 inference(scs_inference,[],[311875,51350])).
% 242.36/242.51 cnf(311888,plain,
% 242.36/242.51 (P7(f10(f6(a1)))),
% 242.36/242.51 inference(scs_inference,[],[311852,51352])).
% 242.36/242.51 cnf(311889,plain,
% 242.36/242.51 (P5(f5(f10(f6(a1))))+~P6(f12(f10(f6(a1))))),
% 242.36/242.51 inference(scs_inference,[],[311852,51446])).
% 242.36/242.51 cnf(311901,plain,
% 242.36/242.51 (P6(f12(f11(f6(a1))))+~P6(f4(f11(f6(a1))))),
% 242.36/242.51 inference(scs_inference,[],[311877,620,3,16941,2771,27,39])).
% 242.36/242.51 cnf(311905,plain,
% 242.36/242.51 (~P5(f4(f3(f7(a1))))+~P6(f12(f3(f7(a1))))),
% 242.36/242.51 inference(scs_inference,[],[542,41,12])).
% 242.36/242.51 cnf(311920,plain,
% 242.36/242.51 (~P5(f12(f10(f6(a1))))+~P5(f5(f10(f6(a1))))),
% 242.36/242.51 inference(scs_inference,[],[311887,2459,4,40,31,29,12])).
% 242.36/242.51 cnf(311935,plain,
% 242.36/242.51 (P3(f2(f7(a1)))+P2(f2(f7(a1)))),
% 242.36/242.51 inference(scs_inference,[],[311862,311856,3,27,16])).
% 242.36/242.51 cnf(311937,plain,
% 242.36/242.51 (P3(f2(f7(a1)))+~P2(f11(a1))),
% 242.36/242.51 inference(scs_inference,[],[311862,311856,3,27,16,42])).
% 242.36/242.51 cnf(312064,plain,
% 242.36/242.51 (P5(f8(f7(a1)))+~P12(f11(a1))),
% 242.36/242.51 inference(scs_inference,[],[311850,2459,3227,4,29,28,27,2483])).
% 242.36/242.51 cnf(312066,plain,
% 242.36/242.51 (P5(f8(f7(a1)))+P3(f2(f7(a1)))),
% 242.36/242.51 inference(scs_inference,[],[311850,2459,3227,4,29,28,27,2483,2458,311935])).
% 242.36/242.51 cnf(312075,plain,
% 242.36/242.51 (~P6(f13(f6(a1)))+P6(f4(f7(a1)))),
% 242.36/242.51 inference(scs_inference,[],[311846,28])).
% 242.36/242.51 cnf(312089,plain,
% 242.36/242.51 (~P6(f4(f11(a1)))+P6(f8(f6(a1)))),
% 242.36/242.51 inference(scs_inference,[],[311848,29])).
% 242.36/242.51 cnf(312187,plain,
% 242.36/242.51 (P5(f12(f2(f7(a1))))+~P5(f5(f2(f7(a1))))+~P2(f11(a1))),
% 242.36/242.51 inference(scs_inference,[],[311937,32])).
% 242.36/242.51 cnf(312216,plain,
% 242.36/242.51 (~P5(f12(f3(f7(a1))))+P5(f4(f3(f7(a1))))+P5(f5(f3(f7(a1))))),
% 242.36/242.51 inference(scs_inference,[],[542,44])).
% 242.36/242.51 cnf(312430,plain,
% 242.36/242.51 (~P6(f4(f3(f7(a1))))+~P6(f5(f3(f7(a1))))+P6(f12(f3(f7(a1))))),
% 242.36/242.51 inference(scs_inference,[],[542,58])).
% 242.36/242.51 cnf(314461,plain,
% 242.36/242.51 (~P6(f5(f10(f6(a1))))+~P6(f12(f10(f6(a1))))),
% 242.36/242.51 inference(scs_inference,[],[311889,12])).
% 242.36/242.51 cnf(314567,plain,
% 242.36/242.51 (~P5(f12(f11(f6(a1))))+~P6(f4(f11(f6(a1))))),
% 242.36/242.51 inference(scs_inference,[],[311901,12])).
% 242.36/242.51 cnf(343868,plain,
% 242.36/242.51 (P5(f5(f11(f6(a1))))),
% 242.36/242.51 inference(scs_inference,[],[311868,311854,26])).
% 242.36/242.51 cnf(343870,plain,
% 242.36/242.51 (P6(f12(f2(f7(a1))))),
% 242.36/242.51 inference(scs_inference,[],[311838,311868,2305,311854,26,28])).
% 242.36/242.51 cnf(343872,plain,
% 242.36/242.51 (~P5(f12(f2(f7(a1))))),
% 242.36/242.51 inference(scs_inference,[],[311838,311868,2305,16930,311854,26,28,27])).
% 242.36/242.51 cnf(343876,plain,
% 242.36/242.51 (~P6(f5(f11(f6(a1))))),
% 242.36/242.51 inference(scs_inference,[],[311838,311868,74,2305,16930,311854,5,26,28,27,29,12])).
% 242.36/242.51 cnf(343882,plain,
% 242.36/242.51 (~P5(f5(f2(f7(a1))))+~P2(f11(a1))),
% 242.36/242.51 inference(scs_inference,[],[343872,312187])).
% 242.36/242.51 cnf(343886,plain,
% 242.36/242.51 (P5(f5(f3(f6(a1))))),
% 242.36/242.51 inference(scs_inference,[],[1539,311854,26])).
% 242.36/242.51 cnf(343894,plain,
% 242.36/242.51 (P6(f12(f11(f6(a1))))),
% 242.36/242.51 inference(scs_inference,[],[343876,311870,1539,620,3227,16919,311854,4,26,28,27,29,39])).
% 242.36/242.51 cnf(343896,plain,
% 242.36/242.51 (~P5(f12(f11(f6(a1))))),
% 242.36/242.51 inference(scs_inference,[],[343876,311870,1539,620,3227,16919,311854,4,26,28,27,29,39,314567])).
% 242.36/242.51 cnf(343897,plain,
% 242.36/242.51 (~P6(f5(f3(f6(a1))))),
% 242.36/242.51 inference(scs_inference,[],[343876,311870,1539,620,3227,16919,311854,4,26,28,27,29,39,314567,12])).
% 242.36/242.51 cnf(343899,plain,
% 242.36/242.51 (~P3(f11(f6(a1)))),
% 242.36/242.51 inference(scs_inference,[],[343868,343876,311870,1539,620,3227,16919,311854,4,26,28,27,29,39,314567,12,32])).
% 242.36/242.51 cnf(343903,plain,
% 242.36/242.51 (~P6(f12(f3(f6(a1))))),
% 242.36/242.51 inference(scs_inference,[],[343868,343872,343876,311870,1539,311874,620,3227,16919,311854,4,26,28,27,29,39,314567,12,32,33,36])).
% 242.36/242.51 cnf(343910,plain,
% 242.36/242.51 (P2(f2(f7(a1)))+~P5(f4(f2(f7(a1))))),
% 242.36/242.51 inference(scs_inference,[],[343868,343872,343876,311870,1539,311874,620,3227,16919,11,311854,4,26,28,27,29,39,314567,12,32,33,36,16,40,312066,311935])).
% 242.36/242.51 cnf(343916,plain,
% 242.36/242.51 (P5(f12(f3(f6(a1))))),
% 242.36/242.51 inference(scs_inference,[],[343886,311886])).
% 242.36/242.51 cnf(343924,plain,
% 242.36/242.51 (~P6(f8(f6(a1)))),
% 242.36/242.51 inference(scs_inference,[],[343903,343916,311872,3686,26,28])).
% 242.36/242.51 cnf(343932,plain,
% 242.36/242.51 (P6(f12(f10(f6(a1))))),
% 242.36/242.51 inference(scs_inference,[],[343899,343894,343897,343903,343916,311872,3686,311888,11,26,28,27,29,16,40])).
% 242.36/242.51 cnf(343934,plain,
% 242.36/242.51 (~P6(f4(f11(a1)))),
% 242.36/242.51 inference(scs_inference,[],[343899,343894,343897,343903,343916,311872,3686,311888,11,26,28,27,29,16,40,312089])).
% 242.36/242.51 cnf(343935,plain,
% 242.36/242.51 (~P5(f12(f10(f6(a1))))),
% 242.36/242.51 inference(scs_inference,[],[343899,343894,343897,343903,343916,311872,3686,311888,11,26,28,27,29,16,40,312089,311920])).
% 242.36/242.51 cnf(343936,plain,
% 242.36/242.51 (~P6(f5(f10(f6(a1))))),
% 242.36/242.51 inference(scs_inference,[],[343899,343894,343897,343903,343916,311872,3686,311888,11,26,28,27,29,16,40,312089,311920,314461])).
% 242.36/242.51 cnf(343942,plain,
% 242.36/242.51 (~P3(f10(f6(a1)))),
% 242.36/242.51 inference(scs_inference,[],[343932,343936,36])).
% 242.36/242.51 cnf(343944,plain,
% 242.36/242.51 (P6(f5(f3(f7(a1))))),
% 242.36/242.51 inference(scs_inference,[],[343932,343936,311830,1691,36,28])).
% 242.36/242.51 cnf(343952,plain,
% 242.36/242.51 (P5(f4(f3(f7(a1))))+~P5(f12(f3(f7(a1))))),
% 242.36/242.51 inference(scs_inference,[],[343924,343932,343936,311830,343899,1691,11,16907,36,28,27,29,16,312216])).
% 242.36/242.51 cnf(343958,plain,
% 242.36/242.51 (~P6(f4(f3(f7(a1))))+P6(f12(f3(f7(a1))))),
% 242.36/242.51 inference(scs_inference,[],[343944,312430])).
% 242.36/242.51 cnf(343960,plain,
% 242.36/242.51 (P6(f5(f2(f6(a1))))),
% 242.36/242.51 inference(scs_inference,[],[3838,343894,28])).
% 242.36/242.51 cnf(343962,plain,
% 242.36/242.51 (~P5(f5(f2(f6(a1))))),
% 242.36/242.51 inference(scs_inference,[],[3838,343896,343894,28,27])).
% 242.36/242.51 cnf(343973,plain,
% 242.36/242.51 (P6(f5(f11(f7(a1))))),
% 242.36/242.51 inference(scs_inference,[],[1615,1691,28])).
% 242.36/242.51 cnf(343988,plain,
% 242.36/242.51 (~P5(f8(f7(a1)))+P5(f12(f3(f7(a1))))),
% 242.36/242.51 inference(scs_inference,[],[2381,343934,343899,343932,11,29,16,26])).
% 242.36/242.51 cnf(344009,plain,
% 242.36/242.51 (~P5(f12(f10(f7(a1))))+P5(f4(f2(f7(a1))))),
% 242.36/242.51 inference(scs_inference,[],[3762,343936,343899,343932,11,29,16,26])).
% 242.36/242.51 cnf(344020,plain,
% 242.36/242.51 (~P3(f2(f7(a1)))+P6(f5(f2(f7(a1))))),
% 242.36/242.51 inference(scs_inference,[],[2153,343876,343870,343942,343894,10,29,16,28,36])).
% 242.36/242.51 cnf(344031,plain,
% 242.36/242.51 (~P4(f8(f6(a1)),f12(f11(f6(a1))))),
% 242.36/242.51 inference(scs_inference,[],[343924,343894,29])).
% 242.36/242.51 cnf(344048,plain,
% 242.36/242.51 (~P6(f4(f7(a1)))+P6(f4(f3(f7(a1))))),
% 242.36/242.51 inference(scs_inference,[],[344031,343934,311836,343899,343932,11,55,29,16,28])).
% 242.36/242.51 cnf(344078,plain,
% 242.36/242.51 (~P5(f12(f3(f7(a1))))+P5(f8(f7(a1)))),
% 242.36/242.51 inference(scs_inference,[],[343876,2381,344031,343942,343894,10,55,16,29,27])).
% 242.36/242.51 cnf(346450,plain,
% 242.36/242.51 (~P5(f12(f10(f7(a1))))+P2(f2(f7(a1)))),
% 242.36/242.51 inference(scs_inference,[],[343910,344009])).
% 242.36/242.51 cnf(348738,plain,
% 242.36/242.51 (P5(f4(f3(f7(a1))))+~P5(f8(f7(a1)))),
% 242.36/242.51 inference(scs_inference,[],[343988,343952])).
% 242.36/242.51 cnf(351884,plain,
% 242.36/242.51 (P6(f12(f3(f7(a1))))+~P6(f4(f7(a1)))),
% 242.36/242.51 inference(scs_inference,[],[344048,343958])).
% 242.36/242.51 cnf(363324,plain,
% 242.36/242.51 (~P5(f4(f3(f7(a1))))+~P6(f4(f7(a1)))),
% 242.36/242.51 inference(scs_inference,[],[351884,311905])).
% 242.36/242.51 cnf(367080,plain,
% 242.36/242.51 (~P6(f4(f7(a1)))+~P5(f8(f7(a1)))),
% 242.36/242.51 inference(scs_inference,[],[363324,348738])).
% 242.36/242.51 cnf(367366,plain,
% 242.36/242.51 (~P5(f8(f7(a1)))+~P6(f13(f6(a1)))),
% 242.36/242.51 inference(scs_inference,[],[367080,312075])).
% 242.36/242.51 cnf(367652,plain,
% 242.36/242.51 (~P6(f13(f6(a1)))+~P12(f11(a1))),
% 242.36/242.51 inference(scs_inference,[],[367366,312064])).
% 242.36/242.51 cnf(537282,plain,
% 242.36/242.51 (P4(f12(f3(f7(a1))),f5(f10(f7(a1))))),
% 242.36/242.51 inference(scs_inference,[],[311828,59])).
% 242.36/242.51 cnf(537284,plain,
% 242.36/242.51 (P4(f12(f10(f6(a1))),f4(f2(f6(a1))))),
% 242.36/242.51 inference(scs_inference,[],[311828,311852,59,60])).
% 242.36/242.51 cnf(537286,plain,
% 242.36/242.51 (P4(f12(f11(f7(a1))),f5(f2(f7(a1))))),
% 242.36/242.51 inference(scs_inference,[],[311828,311852,59,60,61])).
% 242.36/242.51 cnf(573924,plain,
% 242.36/242.51 (P6(f13(f6(a1)))),
% 242.36/242.51 inference(scs_inference,[],[537282,537284,2229,343935,343932,343962,343960,464,28,27,58,31,26,29])).
% 242.36/242.51 cnf(573926,plain,
% 242.36/242.51 (~P12(f11(a1))),
% 242.36/242.51 inference(scs_inference,[],[537282,537284,2229,343935,343932,343962,343960,464,28,27,58,31,26,29,367652])).
% 242.36/242.51 cnf(573930,plain,
% 242.36/242.51 (P2(f11(a1))),
% 242.36/242.51 inference(scs_inference,[],[573926,697])).
% 242.36/242.51 cnf(573931,plain,
% 242.36/242.51 (~P2(f2(f7(a1)))),
% 242.36/242.51 inference(scs_inference,[],[573926,1235])).
% 242.36/242.51 cnf(573932,plain,
% 242.36/242.51 (P6(f4(f7(a1)))),
% 242.36/242.51 inference(scs_inference,[],[573924,312075])).
% 242.36/242.51 cnf(573939,plain,
% 242.36/242.51 (~P5(f8(f7(a1)))),
% 242.36/242.51 inference(scs_inference,[],[573924,367366])).
% 242.36/242.51 cnf(573943,plain,
% 242.36/242.51 (P7(f10(f7(a1)))),
% 242.36/242.51 inference(scs_inference,[],[573930,1311])).
% 242.36/242.51 cnf(573948,plain,
% 242.36/242.51 (P3(f2(f7(a1)))),
% 242.36/242.51 inference(scs_inference,[],[573931,311935])).
% 242.36/242.51 cnf(573962,plain,
% 242.36/242.51 (~P5(f5(f2(f7(a1))))),
% 242.36/242.51 inference(scs_inference,[],[573930,343882])).
% 242.36/242.51 cnf(573974,plain,
% 242.36/242.51 (~P5(f12(f3(f7(a1))))),
% 242.36/242.51 inference(scs_inference,[],[573939,344078])).
% 242.36/242.51 cnf(573979,plain,
% 242.36/242.51 (~P5(f12(f10(f7(a1))))),
% 242.36/242.51 inference(scs_inference,[],[573931,346450])).
% 242.36/242.51 cnf(573982,plain,
% 242.36/242.51 (P6(f12(f3(f7(a1))))),
% 242.36/242.51 inference(scs_inference,[],[573932,351884])).
% 242.36/242.51 cnf(574005,plain,
% 242.36/242.51 (~P6(f5(f10(f7(a1))))+~P12(f10(f7(a1)))),
% 242.36/242.51 inference(scs_inference,[],[573979,3535])).
% 242.36/242.51 cnf(574031,plain,
% 242.36/242.51 (P6(f5(f2(f7(a1))))),
% 242.36/242.51 inference(scs_inference,[],[573948,344020])).
% 242.36/242.51 cnf(574052,plain,
% 242.36/242.51 (P6(f5(f10(f7(a1))))),
% 242.36/242.51 inference(scs_inference,[],[573982,537282,28])).
% 242.36/242.51 cnf(574061,plain,
% 242.36/242.51 (~P6(f5(f2(f7(a1))))+P6(f12(f11(f7(a1))))),
% 242.36/242.51 inference(scs_inference,[],[573962,573974,573982,537282,537286,343973,28,26,27,574005,34,29])).
% 242.36/242.51 cnf(574083,plain,
% 242.36/242.51 ($false),
% 242.36/242.51 inference(scs_inference,[],[573979,573943,574031,574052,574061,34]),
% 242.36/242.51 ['proof']).
% 242.76/242.92 % SZS output end Proof
% 242.76/242.92 % Total time :241.050000s
%------------------------------------------------------------------------------