%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : HWV007-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 : n026.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.80s 242.25s
% Output : CNFRefutation 242.55s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : HWV007-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.13/0.33 % Computer : n026.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Fri Jun 21 02:07:38 EDT 2024
% 0.13/0.33 % CPUTime :
% 0.52/0.61 start to proof:theBenchmark
% 241.78/242.20 %-------------------------------------------
% 241.78/242.20 % File :CSE---1.7
% 241.78/242.20 % Problem :theBenchmark
% 241.78/242.20 % Transform :cnf
% 241.78/242.20 % Format :tptp:raw
% 241.78/242.20 % Command :java -jar mcs_scs.jar %d %s
% 241.78/242.20
% 241.78/242.20 % Result :Theorem 241.030000s
% 241.78/242.20 % Output :CNFRefutation 241.030000s
% 241.78/242.20 %-------------------------------------------
% 241.80/242.25 %--------------------------------------------------------------------------
% 241.80/242.25 % File : HWV007-2 : TPTP v8.2.0. Bugfixed v2.7.0.
% 241.80/242.25 % Domain : Hardware Verification
% 241.80/242.25 % Problem : A fulladder built from two halfadders and an or gate
% 241.80/242.25 % Version : [Gei96] axioms.
% 241.80/242.25 % English :
% 241.80/242.25
% 241.80/242.25 % Refs : [Gei96] Geisler (1996), Email to G. Sutcliffe
% 241.80/242.25 % Source : [Gei96]
% 241.80/242.25 % Names :
% 241.80/242.25
% 241.80/242.25 % Status : Unsatisfiable
% 241.80/242.25 % Rating : 0.00 v7.1.0, 0.17 v7.0.0, 0.12 v6.3.0, 0.14 v6.2.0, 0.00 v2.7.0
% 241.80/242.25 % Syntax : Number of clauses : 62 ( 7 unt; 5 nHn; 62 RR)
% 241.80/242.25 % Number of literals : 144 ( 0 equ; 86 neg)
% 241.80/242.25 % Maximal clause size : 4 ( 2 avg)
% 241.80/242.25 % Maximal term depth : 3 ( 2 avg)
% 241.80/242.25 % Number of predicates : 12 ( 12 usr; 0 prp; 1-2 aty)
% 241.80/242.25 % Number of functors : 13 ( 13 usr; 1 con; 0-1 aty)
% 241.80/242.25 % Number of variables : 55 ( 0 sgn)
% 241.80/242.25 % SPC : CNF_UNS_RFO_NEQ_NHN
% 241.80/242.25
% 241.80/242.25 % Comments :
% 241.80/242.25 % Bugfixes : v2.7.0 - Bugfix in HWV002-0.ax
% 241.80/242.25 %--------------------------------------------------------------------------
% 241.80/242.25 %----Include basic diagnosis axioms
% 241.80/242.25 include('Axioms/HWV002-0.ax').
% 241.80/242.25 %----Include model of halfadder
% 241.80/242.25 include('Axioms/HWV002-1.ax').
% 241.80/242.25 %----Include model of fulladder
% 241.80/242.25 include('Axioms/HWV002-2.ax').
% 241.80/242.25 %--------------------------------------------------------------------------
% 241.80/242.25 %----Observations
% 241.80/242.25 cnf(f_isa_fulladder,hypothesis,
% 241.80/242.25 fulladder(f) ).
% 241.80/242.25
% 241.80/242.25 cnf(in1_1,hypothesis,
% 241.80/242.25 zero(in1(f)) ).
% 241.80/242.25
% 241.80/242.25 cnf(in2_0,hypothesis,
% 241.80/242.25 one(in2(f)) ).
% 241.80/242.25
% 241.80/242.25 cnf(inc_1,hypothesis,
% 241.80/242.25 one(inc(f)) ).
% 241.80/242.25
% 241.80/242.25 cnf(outs_1,hypothesis,
% 241.80/242.25 one(outs(f)) ).
% 241.80/242.25
% 241.80/242.25 cnf(outc_0,hypothesis,
% 241.80/242.25 zero(outc(f)) ).
% 241.80/242.25
% 241.80/242.25 %----Minimal diagnosis
% 241.80/242.25 cnf(diagnosis_and2h1,negated_conjecture,
% 241.80/242.25 ~ abnormal(and2(h1(f))) ).
% 241.80/242.25
% 241.80/242.25 cnf(diagnosis_or1_and1h1,negated_conjecture,
% 241.80/242.25 ( ~ abnormal(or1(f))
% 241.80/242.25 | ~ abnormal(and1(h1(f))) ) ).
% 241.80/242.25
% 241.80/242.25 cnf(diagnosis_or1_not1h1,negated_conjecture,
% 241.80/242.25 ( ~ abnormal(or1(f))
% 241.80/242.25 | ~ abnormal(not1(h1(f))) ) ).
% 241.80/242.25
% 241.80/242.25 cnf(diagnosis_or1_and1h2,negated_conjecture,
% 241.80/242.25 ( ~ abnormal(or1(f))
% 241.80/242.25 | ~ abnormal(and1(h2(f))) ) ).
% 241.80/242.25
% 241.80/242.25 cnf(diagnosis_or1_or1h2,negated_conjecture,
% 241.80/242.25 ( ~ abnormal(or1(f))
% 241.80/242.25 | ~ abnormal(or1(h2(f))) ) ).
% 241.80/242.25
% 241.80/242.25 %--------------------------------------------------------------------------
% 241.80/242.25 %-------------------------------------------
% 241.80/242.25 % Proof found
% 241.80/242.25 % SZS status Theorem for theBenchmark
% 241.80/242.25 % SZS output start Proof
% 241.80/242.29 %ClaNum:62(EqnAxiom:0)
% 241.80/242.29 %VarNum:150(SingletonVarNum:55)
% 241.80/242.29 %MaxLitNum:4
% 241.80/242.29 %MaxfuncDepth:2
% 241.80/242.29 %SharedTerms:24
% 241.80/242.29 %goalClause: 7 38 39 40 41
% 241.80/242.29 %singleGoalClaCount:1
% 241.80/242.29 [1]P1(a1)
% 241.80/242.29 [2]P5(f4(a1))
% 241.80/242.29 [3]P5(f7(a1))
% 241.80/242.29 [4]P6(f8(a1))
% 241.80/242.29 [5]P6(f13(a1))
% 241.80/242.29 [6]P6(f9(a1))
% 241.80/242.29 [7]~P2(f2(f5(a1)))
% 241.80/242.29 [38]~P2(f10(a1))+~P2(f3(f5(a1)))
% 241.80/242.29 [39]~P2(f3(f6(a1)))+~P2(f10(a1))
% 241.80/242.29 [40]~P2(f11(f5(a1)))+~P2(f10(a1))
% 241.80/242.29 [41]~P2(f10(f6(a1)))+~P2(f10(a1))
% 241.80/242.29 [8]~P6(x81)+~P5(x81)
% 241.80/242.30 [9]~P2(x91)+~P3(x91)
% 241.80/242.30 [10]~P12(x101)+~P2(x101)
% 241.80/242.30 [11]~P7(x111)+~P2(x111)
% 241.80/242.30 [15]~P9(x151)+P8(f3(x151))
% 241.80/242.30 [16]~P9(x161)+P8(f2(x161))
% 241.80/242.30 [17]~P9(x171)+P10(f10(x171))
% 241.80/242.30 [18]~P1(x181)+P10(f10(x181))
% 241.80/242.30 [19]~P9(x191)+P11(f11(x191))
% 241.80/242.30 [20]~P1(x201)+P9(f5(x201))
% 241.80/242.30 [21]~P1(x211)+P9(f6(x211))
% 241.80/242.30 [44]~P9(x441)+P4(f4(x441),f4(f2(x441)))
% 241.80/242.30 [45]~P9(x451)+P4(f4(x451),f4(f10(x451)))
% 241.80/242.30 [46]~P1(x461)+P4(f4(x461),f4(f6(x461)))
% 241.80/242.30 [47]~P1(x471)+P4(f8(x471),f4(f5(x471)))
% 241.80/242.30 [48]~P9(x481)+P4(f8(x481),f8(f2(x481)))
% 241.80/242.30 [49]~P9(x491)+P4(f8(x491),f8(f10(x491)))
% 241.80/242.30 [50]~P9(x501)+P4(f13(x501),f12(f3(x501)))
% 241.80/242.30 [51]~P1(x511)+P4(f13(x511),f13(f6(x511)))
% 241.80/242.30 [52]~P9(x521)+P4(f7(x521),f12(f2(x521)))
% 241.80/242.30 [53]~P1(x531)+P4(f7(x531),f12(f10(x531)))
% 241.80/242.30 [54]~P1(x541)+P4(f9(x541),f8(f5(x541)))
% 241.80/242.30 [57]~P9(x571)+P4(f12(f2(x571)),f4(f11(x571)))
% 241.80/242.30 [58]~P9(x581)+P4(f12(f11(x581)),f8(f3(x581)))
% 241.80/242.30 [59]~P9(x591)+P4(f12(f10(x591)),f4(f3(x591)))
% 241.80/242.30 [60]~P1(x601)+P4(f13(f5(x601)),f8(f6(x601)))
% 241.80/242.30 [61]~P1(x611)+P4(f7(f5(x611)),f8(f10(x611)))
% 241.80/242.30 [62]~P1(x621)+P4(f7(f6(x621)),f4(f10(x621)))
% 241.80/242.30 [12]P2(x121)+~P8(x121)+P3(x121)
% 241.80/242.30 [13]P12(x131)+~P10(x131)+P2(x131)
% 241.80/242.30 [14]P7(x141)+~P11(x141)+P2(x141)
% 241.80/242.30 [26]~P12(x261)+~P5(f12(x261))+P5(f4(x261))
% 241.80/242.30 [27]~P7(x271)+~P6(f12(x271))+P5(f4(x271))
% 241.80/242.30 [28]~P3(x281)+~P5(f4(x281))+P5(f12(x281))
% 241.80/242.30 [29]~P3(x291)+~P5(f8(x291))+P5(f12(x291))
% 241.80/242.30 [30]~P7(x301)+~P6(f4(x301))+P5(f12(x301))
% 241.80/242.30 [31]~P12(x311)+~P5(f12(x311))+P5(f8(x311))
% 241.80/242.30 [32]~P3(x321)+~P6(f12(x321))+P6(f4(x321))
% 241.80/242.30 [33]~P7(x331)+~P5(f12(x331))+P6(f4(x331))
% 241.80/242.30 [34]~P12(x341)+~P6(f4(x341))+P6(f12(x341))
% 241.80/242.30 [35]~P12(x351)+~P6(f8(x351))+P6(f12(x351))
% 241.80/242.30 [36]~P7(x361)+~P5(f4(x361))+P6(f12(x361))
% 241.80/242.30 [37]~P3(x371)+~P6(f12(x371))+P6(f8(x371))
% 241.80/242.30 [22]~P4(x222,x221)+P5(x221)+~P5(x222)
% 241.80/242.30 [23]~P4(x231,x232)+P5(x231)+~P5(x232)
% 241.80/242.30 [24]~P4(x242,x241)+P6(x241)+~P6(x242)
% 241.80/242.30 [25]~P4(x251,x252)+P6(x251)+~P6(x252)
% 241.80/242.30 [42]~P3(x421)+P5(f8(x421))+~P5(f12(x421))+P5(f4(x421))
% 241.80/242.30 [43]~P12(x431)+P6(f8(x431))+~P6(f12(x431))+P6(f4(x431))
% 241.80/242.30 [55]~P12(x551)+~P5(f4(x551))+~P5(f8(x551))+P5(f12(x551))
% 241.80/242.30 [56]~P3(x561)+~P6(f4(x561))+~P6(f8(x561))+P6(f12(x561))
% 241.80/242.30 %EqnAxiom
% 241.80/242.30
% 241.80/242.30 %-------------------------------------------
% 242.22/242.63 cnf(63,plain,
% 242.22/242.63 (~P6(f4(a1))),
% 242.22/242.63 inference(scs_inference,[],[2,8])).
% 242.22/242.63 cnf(74,plain,
% 242.22/242.63 (~P6(f7(a1))),
% 242.22/242.63 inference(scs_inference,[],[3,8])).
% 242.22/242.63 cnf(155,plain,
% 242.22/242.63 (~P3(x1551)+~P8(x1551)+P3(x1551)),
% 242.22/242.63 inference(scs_inference,[],[9,12])).
% 242.22/242.63 cnf(231,plain,
% 242.22/242.63 (~P10(x2311)+~P12(x2311)+P12(x2311)),
% 242.22/242.63 inference(scs_inference,[],[10,13])).
% 242.22/242.63 cnf(459,plain,
% 242.22/242.63 (P8(f3(f5(a1)))),
% 242.22/242.63 inference(scs_inference,[],[1,15,20])).
% 242.22/242.63 cnf(464,plain,
% 242.22/242.63 (P3(f3(f5(a1)))+P2(f3(f5(a1)))),
% 242.22/242.63 inference(scs_inference,[],[459,74,4,24,25,12])).
% 242.22/242.63 cnf(470,plain,
% 242.22/242.63 (P3(f3(f5(a1)))+~P3(f3(f5(a1)))),
% 242.22/242.63 inference(scs_inference,[],[459,74,4,24,25,12,10,11,155])).
% 242.22/242.63 cnf(1627,plain,
% 242.22/242.63 (P4(f4(f5(a1)),f4(f2(f5(a1))))),
% 242.22/242.63 inference(scs_inference,[],[1,44,20])).
% 242.22/242.63 cnf(1703,plain,
% 242.22/242.63 (P4(f4(f6(a1)),f4(f10(f6(a1))))),
% 242.22/242.63 inference(scs_inference,[],[1,45,21])).
% 242.22/242.63 cnf(1779,plain,
% 242.22/242.63 (~P6(f4(f6(a1)))),
% 242.22/242.63 inference(scs_inference,[],[1,63,46,25])).
% 242.22/242.63 cnf(1855,plain,
% 242.22/242.63 (P6(f4(f5(a1)))),
% 242.22/242.63 inference(scs_inference,[],[1,4,47,24])).
% 242.22/242.63 cnf(2319,plain,
% 242.22/242.63 (P4(f8(f5(a1)),f8(f2(f5(a1))))),
% 242.22/242.63 inference(scs_inference,[],[1,48,20])).
% 242.22/242.64 cnf(2395,plain,
% 242.22/242.64 (P4(f8(f6(a1)),f8(f10(f6(a1))))),
% 242.22/242.64 inference(scs_inference,[],[1,49,21])).
% 242.22/242.64 cnf(2471,plain,
% 242.22/242.64 (P4(f13(f5(a1)),f12(f3(f5(a1))))),
% 242.22/242.64 inference(scs_inference,[],[1,50,20])).
% 242.22/242.64 cnf(2547,plain,
% 242.22/242.64 (P6(f13(f6(a1)))),
% 242.22/242.64 inference(scs_inference,[],[1,5,51,24])).
% 242.22/242.64 cnf(2699,plain,
% 242.22/242.64 (~P6(f12(f10(a1)))),
% 242.22/242.64 inference(scs_inference,[],[1,74,53,25])).
% 242.22/242.64 cnf(2775,plain,
% 242.22/242.64 (P6(f8(f5(a1)))),
% 242.22/242.64 inference(scs_inference,[],[1,6,54,24])).
% 242.22/242.64 cnf(4361,plain,
% 242.22/242.64 (P4(f12(f2(f5(a1))),f4(f11(f5(a1))))),
% 242.22/242.64 inference(scs_inference,[],[1,57,20])).
% 242.22/242.64 cnf(4817,plain,
% 242.22/242.64 (P5(f7(f5(a1)))+~P5(f8(f10(a1)))),
% 242.22/242.64 inference(scs_inference,[],[1,61,23])).
% 242.22/242.64 cnf(16914,plain,
% 242.22/242.64 (P3(f2(f5(a1)))+~P8(f2(f5(a1)))),
% 242.22/242.64 inference(scs_inference,[],[7,63,4,25,24,12])).
% 242.22/242.64 cnf(327442,plain,
% 242.22/242.64 (P10(f10(a1))),
% 242.22/242.64 inference(scs_inference,[],[1,18])).
% 242.22/242.64 cnf(327444,plain,
% 242.22/242.64 (P9(f5(a1))),
% 242.22/242.64 inference(scs_inference,[],[1,18,20])).
% 242.22/242.64 cnf(327446,plain,
% 242.22/242.64 (P9(f6(a1))),
% 242.22/242.64 inference(scs_inference,[],[1,18,20,21])).
% 242.22/242.64 cnf(327448,plain,
% 242.22/242.64 (P4(f4(f6(a1)),f4(f2(f6(a1))))),
% 242.22/242.64 inference(scs_inference,[],[1,18,20,21,44])).
% 242.22/242.64 cnf(327450,plain,
% 242.22/242.64 (P4(f4(f5(a1)),f4(f10(f5(a1))))),
% 242.22/242.64 inference(scs_inference,[],[1,18,20,21,44,45])).
% 242.22/242.64 cnf(327452,plain,
% 242.22/242.64 (P4(f4(a1),f4(f6(a1)))),
% 242.22/242.64 inference(scs_inference,[],[1,18,20,21,44,45,46])).
% 242.22/242.64 cnf(327460,plain,
% 242.22/242.64 (P4(f13(f6(a1)),f12(f3(f6(a1))))),
% 242.22/242.64 inference(scs_inference,[],[1,18,20,21,44,45,46,47,48,49,50])).
% 242.22/242.64 cnf(327462,plain,
% 242.22/242.64 (P4(f13(a1),f13(f6(a1)))),
% 242.22/242.64 inference(scs_inference,[],[1,18,20,21,44,45,46,47,48,49,50,51])).
% 242.22/242.64 cnf(327464,plain,
% 242.22/242.64 (P4(f7(f5(a1)),f12(f2(f5(a1))))),
% 242.22/242.64 inference(scs_inference,[],[1,18,20,21,44,45,46,47,48,49,50,51,52])).
% 242.22/242.64 cnf(327468,plain,
% 242.22/242.64 (P4(f9(a1),f8(f5(a1)))),
% 242.22/242.64 inference(scs_inference,[],[1,18,20,21,44,45,46,47,48,49,50,51,52,53,54])).
% 242.22/242.64 cnf(327470,plain,
% 242.22/242.64 (P4(f13(f5(a1)),f8(f6(a1)))),
% 242.22/242.64 inference(scs_inference,[],[1,18,20,21,44,45,46,47,48,49,50,51,52,53,54,60])).
% 242.22/242.64 cnf(327476,plain,
% 242.22/242.64 (~P5(f8(a1))),
% 242.22/242.64 inference(scs_inference,[],[1,4,18,20,21,44,45,46,47,48,49,50,51,52,53,54,60,61,62,8])).
% 242.22/242.64 cnf(327478,plain,
% 242.22/242.64 (P5(f12(f10(a1)))),
% 242.22/242.64 inference(scs_inference,[],[1,4,3,18,20,21,44,45,46,47,48,49,50,51,52,53,54,60,61,62,8,22])).
% 242.22/242.64 cnf(327480,plain,
% 242.22/242.64 (P6(f4(f2(f5(a1))))),
% 242.22/242.64 inference(scs_inference,[],[1627,1,4,1855,3,18,20,21,44,45,46,47,48,49,50,51,52,53,54,60,61,62,8,22,24])).
% 242.22/242.64 cnf(327482,plain,
% 242.22/242.64 (~P5(f4(f5(a1)))),
% 242.22/242.64 inference(scs_inference,[],[1627,1,4,1855,3,18,20,21,44,45,46,47,48,49,50,51,52,53,54,60,61,62,8,22,24,23])).
% 242.22/242.64 cnf(327486,plain,
% 242.22/242.64 (P8(f3(f6(a1)))),
% 242.22/242.64 inference(scs_inference,[],[1627,1,4,2699,1855,3,18,20,21,44,45,46,47,48,49,50,51,52,53,54,60,61,62,8,22,24,23,25,15])).
% 242.22/242.64 cnf(327490,plain,
% 242.22/242.64 (P10(f10(f6(a1)))),
% 242.22/242.64 inference(scs_inference,[],[1627,1,4,2699,1855,3,18,20,21,44,45,46,47,48,49,50,51,52,53,54,60,61,62,8,22,24,23,25,15,16,17])).
% 242.22/242.64 cnf(327492,plain,
% 242.22/242.64 (P11(f11(f5(a1)))),
% 242.22/242.64 inference(scs_inference,[],[1627,1,4,2699,1855,3,18,20,21,44,45,46,47,48,49,50,51,52,53,54,60,61,62,8,22,24,23,25,15,16,17,19])).
% 242.22/242.64 cnf(327494,plain,
% 242.22/242.64 (P3(f2(f5(a1)))),
% 242.22/242.64 inference(scs_inference,[],[1627,1,4,2699,1855,3,18,20,21,44,45,46,47,48,49,50,51,52,53,54,60,61,62,8,22,24,23,25,15,16,17,19,16914])).
% 242.22/242.64 cnf(327509,plain,
% 242.22/242.64 (~P5(f4(f2(f5(a1))))),
% 242.22/242.64 inference(scs_inference,[],[327480,8])).
% 242.22/242.64 cnf(327511,plain,
% 242.22/242.64 (P5(f4(f6(a1)))),
% 242.22/242.64 inference(scs_inference,[],[327452,327480,2,8,22])).
% 242.22/242.64 cnf(327517,plain,
% 242.22/242.64 (~P5(f8(f5(a1)))),
% 242.22/242.64 inference(scs_inference,[],[2775,8])).
% 242.22/242.64 cnf(327526,plain,
% 242.22/242.64 (~P5(f13(a1))),
% 242.22/242.64 inference(scs_inference,[],[5,8])).
% 242.22/242.64 cnf(327530,plain,
% 242.22/242.64 (~P5(f13(f6(a1)))),
% 242.22/242.64 inference(scs_inference,[],[327517,327462,327468,5,8,22,23])).
% 242.22/242.64 cnf(327534,plain,
% 242.22/242.64 (P3(f3(f6(a1)))+P2(f3(f6(a1)))),
% 242.22/242.64 inference(scs_inference,[],[327486,327517,327462,327468,327476,5,8,22,23,31,12])).
% 242.22/242.64 cnf(327538,plain,
% 242.22/242.64 (P2(f10(f6(a1)))+P12(f10(f6(a1)))),
% 242.22/242.64 inference(scs_inference,[],[327526,327490,327511,22,13])).
% 242.22/242.64 cnf(327567,plain,
% 242.22/242.64 (P2(f11(f5(a1)))+P7(f11(f5(a1)))),
% 242.22/242.64 inference(scs_inference,[],[327492,4,2699,1855,24,25,14])).
% 242.22/242.64 cnf(327617,plain,
% 242.22/242.64 (~P6(f8(f6(a1)))+P6(f13(f5(a1)))),
% 242.22/242.64 inference(scs_inference,[],[327470,2699,1855,24,25])).
% 242.22/242.64 cnf(327624,plain,
% 242.22/242.64 (P12(f10(f6(a1)))+~P12(f10(f6(a1)))),
% 242.22/242.64 inference(scs_inference,[],[327490,4,2699,25,231])).
% 242.22/242.64 cnf(356917,plain,
% 242.22/242.64 (P5(f4(f10(f6(a1))))),
% 242.22/242.64 inference(scs_inference,[],[1703,2319,2699,327517,6,327511,25,23,22])).
% 242.22/242.64 cnf(356918,plain,
% 242.22/242.64 (~P4(x3569181,x3569182)+~P5(x3569181)+P5(x3569182)),
% 242.22/242.64 inference(rename_variables,[],[22])).
% 242.22/242.64 cnf(356921,plain,
% 242.22/242.64 (~P5(f12(f2(f5(a1))))),
% 242.22/242.64 inference(scs_inference,[],[1703,2319,327494,2699,2775,327509,327517,6,327511,25,23,22,24,42])).
% 242.22/242.64 cnf(356923,plain,
% 242.22/242.64 (P6(f12(f2(f5(a1))))),
% 242.22/242.64 inference(scs_inference,[],[1703,2319,327494,2699,2775,327509,327517,327480,6,327511,25,23,22,24,42,56])).
% 242.22/242.64 cnf(356925,plain,
% 242.22/242.64 (~P7(f2(f5(a1)))),
% 242.22/242.64 inference(scs_inference,[],[1703,2319,327494,2699,2775,327509,327517,327480,6,327511,25,23,22,24,42,56,27])).
% 242.22/242.64 cnf(356934,plain,
% 242.22/242.64 (P2(f10(a1))),
% 242.22/242.64 inference(scs_inference,[],[327464,1703,2319,327442,327494,2699,327478,2775,327509,327517,327480,6,327511,25,23,22,24,42,56,27,356918,36,4817,31,13])).
% 242.22/242.64 cnf(356936,plain,
% 242.22/242.64 (~P2(f3(f5(a1)))),
% 242.22/242.64 inference(scs_inference,[],[356934,38])).
% 242.22/242.64 cnf(356937,plain,
% 242.22/242.64 (~P2(f3(f6(a1)))),
% 242.22/242.64 inference(scs_inference,[],[356934,39])).
% 242.22/242.64 cnf(356938,plain,
% 242.22/242.64 (~P2(f11(f5(a1)))),
% 242.22/242.64 inference(scs_inference,[],[356934,40])).
% 242.22/242.64 cnf(356939,plain,
% 242.22/242.64 (~P2(f10(f6(a1)))),
% 242.22/242.64 inference(scs_inference,[],[356934,41])).
% 242.22/242.64 cnf(356945,plain,
% 242.22/242.64 (P3(f3(f5(a1)))),
% 242.22/242.64 inference(scs_inference,[],[356936,464])).
% 242.22/242.64 cnf(356948,plain,
% 242.22/242.64 (P3(f3(f6(a1)))),
% 242.22/242.64 inference(scs_inference,[],[356937,327534])).
% 242.22/242.64 cnf(356949,plain,
% 242.22/242.64 (P12(f10(f6(a1)))),
% 242.22/242.64 inference(scs_inference,[],[356939,327538])).
% 242.22/242.64 cnf(356951,plain,
% 242.22/242.64 (P7(f11(f5(a1)))),
% 242.22/242.64 inference(scs_inference,[],[356938,327567])).
% 242.22/242.64 cnf(356956,plain,
% 242.22/242.64 (P6(f7(f5(a1)))),
% 242.22/242.64 inference(scs_inference,[],[327464,356934,356923,11,25])).
% 242.22/242.64 cnf(356960,plain,
% 242.22/242.64 (P5(f4(f2(f6(a1))))),
% 242.22/242.64 inference(scs_inference,[],[327464,356934,356923,327448,327450,327482,327511,11,25,23,22])).
% 242.22/242.64 cnf(356971,plain,
% 242.22/242.64 (P3(f3(f5(a1)))),
% 242.22/242.64 inference(scs_inference,[],[356945,470])).
% 242.22/242.64 cnf(356979,plain,
% 242.22/242.64 (P12(f10(f6(a1)))),
% 242.22/242.64 inference(scs_inference,[],[356949,327624])).
% 242.22/242.64 cnf(356998,plain,
% 242.22/242.64 (~P5(f4(f3(f6(a1))))),
% 242.22/242.64 inference(scs_inference,[],[327460,356948,356956,2699,327530,25,23,28])).
% 242.22/242.64 cnf(357000,plain,
% 242.22/242.64 (P6(f12(f3(f6(a1))))),
% 242.22/242.64 inference(scs_inference,[],[327460,356948,356956,2699,2547,327530,25,23,28,24])).
% 242.22/242.64 cnf(357009,plain,
% 242.22/242.64 (P6(f4(f11(f5(a1))))),
% 242.22/242.64 inference(scs_inference,[],[4361,356923,24])).
% 242.22/242.64 cnf(357013,plain,
% 242.22/242.64 (~P5(f4(f11(f5(a1))))),
% 242.22/242.64 inference(scs_inference,[],[4361,356921,356923,356956,1779,24,25,23])).
% 242.22/242.64 cnf(357279,plain,
% 242.22/242.64 (~P6(f4(f2(f6(a1))))),
% 242.22/242.64 inference(scs_inference,[],[356960,8])).
% 242.22/242.64 cnf(357287,plain,
% 242.22/242.64 (P6(f4(f3(f6(a1))))),
% 242.22/242.64 inference(scs_inference,[],[7,5,1779,356948,356934,356960,356925,357000,8,9,14,25,32])).
% 242.22/242.64 cnf(357289,plain,
% 242.22/242.64 (P5(f12(f11(f5(a1))))),
% 242.22/242.64 inference(scs_inference,[],[7,5,1779,357009,356948,356934,356960,356951,356925,357000,8,9,14,25,32,30])).
% 242.22/242.64 cnf(357299,plain,
% 242.22/242.64 (~P6(f12(f11(f5(a1))))),
% 242.22/242.64 inference(scs_inference,[],[7,63,327511,5,327476,1779,357013,357009,356948,356934,356960,356951,356925,357000,8,9,14,25,32,30,22,23,37,24,27])).
% 242.22/242.64 cnf(357311,plain,
% 242.22/242.64 (~P6(f4(f10(f6(a1))))),
% 242.22/242.64 inference(scs_inference,[],[356917,8])).
% 242.22/242.64 cnf(458726,plain,
% 242.22/242.64 (~P5(f8(f3(f5(a1))))+~P6(f12(f3(f5(a1))))),
% 242.22/242.64 inference(scs_inference,[],[5,357279,356971,25,37,8])).
% 242.22/242.64 cnf(461542,plain,
% 242.22/242.64 (~P6(f8(f10(f6(a1))))+P6(f8(f6(a1)))),
% 242.22/242.64 inference(scs_inference,[],[2395,25])).
% 242.22/242.64 cnf(497636,plain,
% 242.22/242.64 (P4(f12(f2(f6(a1))),f4(f11(f6(a1))))),
% 242.22/242.64 inference(scs_inference,[],[327446,57])).
% 242.22/242.64 cnf(497638,plain,
% 242.22/242.64 (P4(f12(f11(f5(a1))),f8(f3(f5(a1))))),
% 242.22/242.64 inference(scs_inference,[],[327444,327446,57,58])).
% 242.22/242.64 cnf(497640,plain,
% 242.22/242.64 (P4(f12(f10(f6(a1))),f4(f3(f6(a1))))),
% 242.22/242.64 inference(scs_inference,[],[327444,327446,57,58,59])).
% 242.22/242.64 cnf(533088,plain,
% 242.22/242.64 (~P6(f8(f6(a1)))),
% 242.22/242.64 inference(scs_inference,[],[497636,497638,2471,357299,357289,25,22,458726,23,24,327617])).
% 242.22/242.64 cnf(533097,plain,
% 242.22/242.64 (~P6(f8(f10(f6(a1))))),
% 242.22/242.64 inference(scs_inference,[],[533088,461542])).
% 242.22/242.64 cnf(533109,plain,
% 242.22/242.64 (P6(f8(f10(f6(a1))))),
% 242.22/242.64 inference(scs_inference,[],[497640,356979,356998,357287,356917,357311,25,22,28,43])).
% 242.22/242.64 cnf(533128,plain,
% 242.22/242.64 ($false),
% 242.22/242.64 inference(scs_inference,[],[533097,533109]),
% 242.22/242.64 ['proof']).
% 242.55/242.93 % SZS output end Proof
% 242.55/242.93 % Total time :241.030000s
%------------------------------------------------------------------------------