%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : HWV008-2.001 : 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 : 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.72s 241.89s
% Output : CNFRefutation 242.76s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : HWV008-2.001 : TPTP v8.2.0. Bugfixed v2.7.0.
% 0.12/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n024.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 02:37:54 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.19/0.56 start to proof:theBenchmark
% 241.72/241.83 %-------------------------------------------
% 241.72/241.83 % File :CSE---1.7
% 241.72/241.83 % Problem :theBenchmark
% 241.72/241.83 % Transform :cnf
% 241.72/241.83 % Format :tptp:raw
% 241.72/241.83 % Command :java -jar mcs_scs.jar %d %s
% 241.72/241.83
% 241.72/241.83 % Result :Theorem 241.040000s
% 241.72/241.83 % Output :CNFRefutation 241.040000s
% 241.72/241.83 %-------------------------------------------
% 241.72/241.89 %--------------------------------------------------------------------------
% 241.72/241.89 % File : HWV008-2.001 : TPTP v8.2.0. Bugfixed v2.7.0.
% 241.72/241.89 % Domain : Hardware Verification
% 241.72/241.89 % Problem : 1 bit ripple carry adder
% 241.72/241.89 % Version : [Gei96] axioms.
% 241.72/241.89 % English :
% 241.72/241.89
% 241.72/241.89 % Refs : [Gei96] Geisler (1996), Email to G. Sutcliffe
% 241.72/241.89 % Source : [Gei96]
% 241.72/241.89 % Names :
% 241.72/241.89
% 241.72/241.89 % Status : Unsatisfiable
% 241.72/241.89 % Rating : 0.00 v7.5.0, 0.17 v7.4.0, 0.00 v6.3.0, 0.14 v6.2.0, 0.00 v3.1.0, 0.17 v2.7.0
% 241.72/241.89 % Syntax : Number of clauses : 66 ( 9 unt; 5 nHn; 66 RR)
% 241.72/241.89 % Number of literals : 150 ( 0 equ; 86 neg)
% 241.72/241.89 % Maximal clause size : 4 ( 2 avg)
% 241.72/241.89 % Maximal term depth : 4 ( 2 avg)
% 241.72/241.89 % Number of predicates : 13 ( 13 usr; 0 prp; 1-2 aty)
% 241.72/241.89 % Number of functors : 16 ( 16 usr; 1 con; 0-1 aty)
% 241.72/241.89 % Number of variables : 61 ( 0 sgn)
% 241.72/241.89 % SPC : CNF_UNS_RFO_NEQ_NHN
% 241.72/241.89
% 241.72/241.89 % Comments :
% 241.72/241.89 % Bugfixes : v2.7.0 - Bugfix in HWV002-0.ax
% 241.72/241.89 %--------------------------------------------------------------------------
% 241.72/241.89 %----Include basic diagnosis axioms
% 241.72/241.89 include('Axioms/HWV002-0.ax').
% 241.72/241.89 %----Include model of halfadder
% 241.72/241.89 include('Axioms/HWV002-1.ax').
% 241.72/241.89 %----Include model of fulladder
% 241.72/241.89 include('Axioms/HWV002-2.ax').
% 241.72/241.89 %--------------------------------------------------------------------------
% 241.72/241.89 %----Composition of 1-bit adder
% 241.72/241.89 cnf(nbit_adder_fulladder1,axiom,
% 241.72/241.89 ( ~ nbit_adder1(X)
% 241.72/241.89 | fulladder(f1(X)) ) ).
% 241.72/241.89
% 241.72/241.89 %----Connections of 1-bit adder
% 241.72/241.89 cnf(nbit_adder_connection_out1_out1f1,axiom,
% 241.72/241.89 ( ~ nbit_adder1(X)
% 241.72/241.89 | connection(out1(X),outs(f1(X))) ) ).
% 241.72/241.89
% 241.72/241.89 cnf(nbit_adder_connection_outc_outcf1,axiom,
% 241.72/241.89 ( ~ nbit_adder1(X)
% 241.72/241.89 | connection(outc(X),outc(f1(X))) ) ).
% 241.72/241.89
% 241.72/241.89 cnf(nbit_adder_connection_ina1_in1f1,axiom,
% 241.72/241.89 ( ~ nbit_adder1(X)
% 241.72/241.89 | connection(ina1(X),in1(f1(X))) ) ).
% 241.72/241.89
% 241.72/241.89 cnf(nbit_adder_connection_inb1_in2f1,axiom,
% 241.72/241.89 ( ~ nbit_adder1(X)
% 241.72/241.89 | connection(inb1(X),in2(f1(X))) ) ).
% 241.72/241.89
% 241.72/241.89 cnf(nbit_adder_connection_inc_incf1,axiom,
% 241.72/241.89 ( ~ nbit_adder1(X)
% 241.72/241.89 | connection(inc(X),inc(f1(X))) ) ).
% 241.72/241.89
% 241.72/241.89 %----Observations
% 241.72/241.89 cnf(a_isa_1bit_adder,hypothesis,
% 241.72/241.89 nbit_adder1(a) ).
% 241.72/241.89
% 241.72/241.89 cnf(ina1_0,hypothesis,
% 241.72/241.89 zero(ina1(a)) ).
% 241.72/241.89
% 241.72/241.89 cnf(inb1_0,hypothesis,
% 241.72/241.89 zero(inb1(a)) ).
% 241.72/241.89
% 241.72/241.89 cnf(inc_0,hypothesis,
% 241.72/241.89 zero(inc(a)) ).
% 241.72/241.89
% 241.72/241.89 cnf(out1_0,hypothesis,
% 241.72/241.89 zero(out1(a)) ).
% 241.72/241.89
% 241.72/241.89 cnf(outc_0,hypothesis,
% 241.72/241.89 one(outc(a)) ).
% 241.72/241.89
% 241.72/241.89 %----Minimal diagnosis
% 241.72/241.89 cnf(diagnosis_or1f1,negated_conjecture,
% 241.72/241.89 ~ abnormal(or1(f1(a))) ).
% 241.72/241.89
% 241.72/241.89 cnf(diagnosis_and2h1f1,negated_conjecture,
% 241.72/241.89 ~ abnormal(and2(h1(f1(a)))) ).
% 241.72/241.89
% 241.72/241.89 cnf(diagnosis_and2h2f1,negated_conjecture,
% 241.72/241.89 ~ abnormal(and2(h2(f1(a)))) ).
% 241.72/241.89
% 241.72/241.89 %--------------------------------------------------------------------------
% 241.72/241.89 %-------------------------------------------
% 241.72/241.89 % Proof found
% 241.72/241.89 % SZS status Theorem for theBenchmark
% 241.72/241.89 % SZS output start Proof
% 241.83/241.95 %ClaNum:66(EqnAxiom:0)
% 241.83/241.95 %VarNum:167(SingletonVarNum:61)
% 241.83/241.95 %MaxLitNum:4
% 241.83/241.95 %MaxfuncDepth:3
% 241.83/241.95 %SharedTerms:21
% 241.83/241.95 %goalClause: 7 8 9
% 241.83/241.95 %singleGoalClaCount:3
% 241.83/241.95 [1]P1(a1)
% 241.83/241.95 [2]P10(f2(a1))
% 241.83/241.95 [3]P10(f3(a1))
% 241.83/241.95 [4]P10(f4(a1))
% 241.83/241.95 [5]P10(f12(a1))
% 241.83/241.95 [6]P11(f15(a1))
% 241.83/241.95 [7]~P2(f13(f5(a1)))
% 241.83/241.95 [8]~P2(f6(f8(f5(a1))))
% 241.83/241.95 [9]~P2(f6(f9(f5(a1))))
% 241.83/241.95 [10]~P11(x101)+~P10(x101)
% 241.83/241.95 [11]~P2(x111)+~P3(x111)
% 241.83/241.95 [12]~P13(x121)+~P2(x121)
% 241.83/241.95 [13]~P12(x131)+~P2(x131)
% 241.83/241.95 [17]~P5(x171)+P4(f7(x171))
% 241.83/241.95 [18]~P5(x181)+P4(f6(x181))
% 241.83/241.95 [19]~P5(x191)+P8(f13(x191))
% 241.83/241.95 [20]~P6(x201)+P8(f13(x201))
% 241.83/241.95 [21]~P5(x211)+P9(f14(x211))
% 241.83/241.95 [22]~P6(x221)+P5(f8(x221))
% 241.83/241.95 [23]~P6(x231)+P5(f9(x231))
% 241.83/241.95 [24]~P1(x241)+P6(f5(x241))
% 241.83/241.95 [43]~P5(x431)+P7(f10(x431),f10(f6(x431)))
% 241.83/241.95 [44]~P5(x441)+P7(f10(x441),f10(f13(x441)))
% 241.83/241.95 [45]~P6(x451)+P7(f10(x451),f10(f9(x451)))
% 241.83/241.95 [46]~P1(x461)+P7(f2(x461),f16(f5(x461)))
% 241.83/241.95 [47]~P6(x471)+P7(f11(x471),f10(f8(x471)))
% 241.83/241.95 [48]~P5(x481)+P7(f11(x481),f11(f6(x481)))
% 241.83/241.95 [49]~P5(x491)+P7(f11(x491),f11(f13(x491)))
% 241.83/241.95 [50]~P5(x501)+P7(f16(x501),f2(f7(x501)))
% 241.83/241.95 [51]~P6(x511)+P7(f16(x511),f16(f9(x511)))
% 241.83/241.95 [52]~P5(x521)+P7(f15(x521),f2(f6(x521)))
% 241.83/241.95 [53]~P6(x531)+P7(f15(x531),f2(f13(x531)))
% 241.83/241.95 [54]~P1(x541)+P7(f15(x541),f15(f5(x541)))
% 241.83/241.95 [55]~P6(x551)+P7(f3(x551),f11(f8(x551)))
% 241.83/241.95 [56]~P1(x561)+P7(f3(x561),f3(f5(x561)))
% 241.83/241.95 [57]~P1(x571)+P7(f4(x571),f10(f5(x571)))
% 241.83/241.95 [58]~P1(x581)+P7(f12(x581),f11(f5(x581)))
% 241.83/241.95 [61]~P5(x611)+P7(f2(f6(x611)),f10(f14(x611)))
% 241.83/241.95 [62]~P5(x621)+P7(f2(f14(x621)),f11(f7(x621)))
% 241.83/241.95 [63]~P5(x631)+P7(f2(f13(x631)),f10(f7(x631)))
% 241.83/241.95 [64]~P6(x641)+P7(f16(f8(x641)),f11(f9(x641)))
% 241.83/241.95 [65]~P6(x651)+P7(f15(f8(x651)),f11(f13(x651)))
% 241.83/241.95 [66]~P6(x661)+P7(f15(f9(x661)),f10(f13(x661)))
% 241.83/241.95 [14]P2(x141)+~P4(x141)+P3(x141)
% 241.83/241.95 [15]P13(x151)+~P8(x151)+P2(x151)
% 241.83/241.95 [16]P12(x161)+~P9(x161)+P2(x161)
% 241.83/241.95 [29]~P13(x291)+~P10(f2(x291))+P10(f10(x291))
% 241.83/241.95 [30]~P12(x301)+~P11(f2(x301))+P10(f10(x301))
% 241.83/241.95 [31]~P3(x311)+~P10(f10(x311))+P10(f2(x311))
% 241.83/241.95 [32]~P3(x321)+~P10(f11(x321))+P10(f2(x321))
% 241.83/241.95 [33]~P12(x331)+~P11(f10(x331))+P10(f2(x331))
% 241.83/241.95 [34]~P13(x341)+~P10(f2(x341))+P10(f11(x341))
% 241.83/241.95 [35]~P3(x351)+~P11(f2(x351))+P11(f10(x351))
% 241.83/241.95 [36]~P12(x361)+~P10(f2(x361))+P11(f10(x361))
% 241.83/241.95 [37]~P13(x371)+~P11(f10(x371))+P11(f2(x371))
% 241.83/241.95 [38]~P13(x381)+~P11(f11(x381))+P11(f2(x381))
% 241.83/241.95 [39]~P12(x391)+~P10(f10(x391))+P11(f2(x391))
% 241.83/241.95 [40]~P3(x401)+~P11(f2(x401))+P11(f11(x401))
% 241.83/241.95 [25]~P7(x252,x251)+P10(x251)+~P10(x252)
% 241.83/241.95 [26]~P7(x261,x262)+P10(x261)+~P10(x262)
% 241.83/241.95 [27]~P7(x272,x271)+P11(x271)+~P11(x272)
% 241.83/241.95 [28]~P7(x281,x282)+P11(x281)+~P11(x282)
% 241.83/241.95 [41]~P3(x411)+P10(f11(x411))+~P10(f2(x411))+P10(f10(x411))
% 241.83/241.95 [42]~P13(x421)+P11(f11(x421))+~P11(f2(x421))+P11(f10(x421))
% 241.83/241.95 [59]~P13(x591)+~P10(f10(x591))+~P10(f11(x591))+P10(f2(x591))
% 241.83/241.95 [60]~P3(x601)+~P11(f10(x601))+~P11(f11(x601))+P11(f2(x601))
% 241.83/241.95 %EqnAxiom
% 241.83/241.95
% 241.83/241.95 %-------------------------------------------
% 242.31/242.41 cnf(67,plain,
% 242.31/242.41 (~P11(f2(a1))),
% 242.31/242.41 inference(scs_inference,[],[2,10])).
% 242.31/242.41 cnf(78,plain,
% 242.31/242.41 (~P11(f3(a1))),
% 242.31/242.41 inference(scs_inference,[],[3,10])).
% 242.31/242.41 cnf(96,plain,
% 242.31/242.41 (~P11(f12(a1))),
% 242.31/242.41 inference(scs_inference,[],[5,10])).
% 242.31/242.41 cnf(394,plain,
% 242.31/242.41 (~P6(x3941)+P4(f7(f8(x3941)))),
% 242.31/242.41 inference(scs_inference,[],[17,22])).
% 242.31/242.41 cnf(455,plain,
% 242.31/242.41 (~P6(x4551)+P4(f6(f9(x4551)))),
% 242.31/242.41 inference(scs_inference,[],[18,23])).
% 242.31/242.41 cnf(516,plain,
% 242.31/242.41 (~P6(x5161)+P8(f13(f8(x5161)))),
% 242.31/242.41 inference(scs_inference,[],[19,22])).
% 242.31/242.41 cnf(577,plain,
% 242.31/242.41 (P8(f13(f5(a1)))),
% 242.31/242.41 inference(scs_inference,[],[1,20,24])).
% 242.31/242.41 cnf(578,plain,
% 242.31/242.41 (P13(f13(f5(a1)))),
% 242.31/242.41 inference(scs_inference,[],[7,577,15])).
% 242.31/242.41 cnf(640,plain,
% 242.31/242.41 (~P6(x6401)+P9(f14(f9(x6401)))),
% 242.31/242.42 inference(scs_inference,[],[21,23])).
% 242.31/242.42 cnf(1128,plain,
% 242.31/242.42 (P3(f6(f9(f5(a1))))+~P6(f5(a1))),
% 242.31/242.42 inference(scs_inference,[],[9,455,14])).
% 242.31/242.42 cnf(1311,plain,
% 242.31/242.42 (~P6(x13111)+P7(f10(f8(x13111)),f10(f6(f8(x13111))))),
% 242.31/242.42 inference(scs_inference,[],[43,22])).
% 242.31/242.42 cnf(1372,plain,
% 242.31/242.42 (~P6(x13721)+P7(f10(f9(x13721)),f10(f13(f9(x13721))))),
% 242.31/242.42 inference(scs_inference,[],[44,23])).
% 242.31/242.42 cnf(1433,plain,
% 242.31/242.42 (P7(f10(f5(a1)),f10(f9(f5(a1))))),
% 242.31/242.42 inference(scs_inference,[],[1,45,24])).
% 242.31/242.42 cnf(1494,plain,
% 242.31/242.42 (P10(f16(f5(a1)))),
% 242.31/242.42 inference(scs_inference,[],[1,2,46,25])).
% 242.31/242.42 cnf(1557,plain,
% 242.31/242.42 (P7(f11(f5(a1)),f10(f8(f5(a1))))),
% 242.31/242.42 inference(scs_inference,[],[1,47,24])).
% 242.31/242.42 cnf(1618,plain,
% 242.31/242.42 (~P6(x16181)+P7(f11(f8(x16181)),f11(f6(f8(x16181))))),
% 242.31/242.42 inference(scs_inference,[],[48,22])).
% 242.31/242.42 cnf(1679,plain,
% 242.31/242.42 (~P6(x16791)+P7(f11(f9(x16791)),f11(f13(f9(x16791))))),
% 242.31/242.42 inference(scs_inference,[],[49,23])).
% 242.31/242.42 cnf(1801,plain,
% 242.31/242.42 (P7(f16(f5(a1)),f16(f9(f5(a1))))),
% 242.31/242.42 inference(scs_inference,[],[1,51,24])).
% 242.31/242.42 cnf(1862,plain,
% 242.31/242.42 (~P6(x18621)+P7(f15(f9(x18621)),f2(f6(f9(x18621))))),
% 242.31/242.42 inference(scs_inference,[],[52,23])).
% 242.31/242.42 cnf(1923,plain,
% 242.31/242.42 (P7(f15(f5(a1)),f2(f13(f5(a1))))),
% 242.31/242.42 inference(scs_inference,[],[1,53,24])).
% 242.31/242.42 cnf(1984,plain,
% 242.31/242.42 (P11(f15(f5(a1)))),
% 242.31/242.42 inference(scs_inference,[],[1,6,54,27])).
% 242.31/242.42 cnf(2045,plain,
% 242.31/242.42 (P7(f3(f5(a1)),f11(f8(f5(a1))))),
% 242.31/242.42 inference(scs_inference,[],[1,55,24])).
% 242.31/242.42 cnf(2106,plain,
% 242.31/242.42 (~P11(f3(f5(a1)))),
% 242.31/242.42 inference(scs_inference,[],[1,78,56,28])).
% 242.31/242.42 cnf(2107,plain,
% 242.31/242.42 (~P11(f11(f8(f5(a1))))),
% 242.31/242.42 inference(scs_inference,[],[2106,2045,28])).
% 242.31/242.42 cnf(2182,plain,
% 242.31/242.42 (P10(f10(f5(a1)))),
% 242.31/242.42 inference(scs_inference,[],[1,4,57,25])).
% 242.31/242.42 cnf(2183,plain,
% 242.31/242.42 (~P11(f10(f5(a1)))),
% 242.31/242.42 inference(scs_inference,[],[2182,10])).
% 242.31/242.42 cnf(2194,plain,
% 242.31/242.42 (~P11(f10(f9(f5(a1))))),
% 242.31/242.42 inference(scs_inference,[],[2183,1433,28])).
% 242.31/242.42 cnf(2198,plain,
% 242.31/242.42 (~P3(f5(a1))+P10(f2(f5(a1)))),
% 242.31/242.42 inference(scs_inference,[],[2183,2182,1984,1433,28,27,31])).
% 242.31/242.42 cnf(2420,plain,
% 242.31/242.42 (P10(x24201)+~P7(f2(f5(a1)),x24201)+~P3(f5(a1))),
% 242.31/242.42 inference(scs_inference,[],[2198,25])).
% 242.31/242.42 cnf(2648,plain,
% 242.31/242.42 (~P11(f11(f5(a1)))),
% 242.31/242.42 inference(scs_inference,[],[1,96,58,28])).
% 242.31/242.42 cnf(2651,plain,
% 242.31/242.42 (~P11(f10(f8(f5(a1))))),
% 242.31/242.42 inference(scs_inference,[],[2648,1984,1557,27,28])).
% 242.31/242.42 cnf(3028,plain,
% 242.31/242.42 (~P6(x30281)+P7(f2(f14(f9(x30281))),f11(f7(f9(x30281))))),
% 242.31/242.42 inference(scs_inference,[],[62,23])).
% 242.31/242.42 cnf(3256,plain,
% 242.31/242.42 (P7(f15(f8(f5(a1))),f11(f13(f5(a1))))),
% 242.31/242.42 inference(scs_inference,[],[1,65,24])).
% 242.31/242.42 cnf(3332,plain,
% 242.31/242.42 (P7(f15(f9(f5(a1))),f10(f13(f5(a1))))),
% 242.31/242.42 inference(scs_inference,[],[1,66,24])).
% 242.31/242.42 cnf(3484,plain,
% 242.31/242.42 (~P11(f10(f6(f8(f5(a1)))))+~P6(f5(a1))),
% 242.31/242.42 inference(scs_inference,[],[2651,1311,28])).
% 242.31/242.42 cnf(3635,plain,
% 242.31/242.42 (~P11(f10(f13(f9(f5(a1)))))+~P6(f5(a1))),
% 242.31/242.42 inference(scs_inference,[],[2194,1372,28])).
% 242.31/242.42 cnf(3786,plain,
% 242.31/242.42 (~P11(f11(f6(f8(f5(a1)))))+~P6(f5(a1))),
% 242.31/242.42 inference(scs_inference,[],[2107,1618,28])).
% 242.31/242.42 cnf(4089,plain,
% 242.31/242.42 (P11(f2(f6(f9(x40891))))+~P11(f15(f9(x40891)))+~P6(x40891)),
% 242.31/242.42 inference(scs_inference,[],[1862,27])).
% 242.31/242.42 cnf(4920,plain,
% 242.31/242.42 (~P6(f5(a1))+~P11(f2(f6(f9(f5(a1)))))+P11(f11(f6(f9(f5(a1)))))),
% 242.31/242.42 inference(scs_inference,[],[40,1128])).
% 242.31/242.42 cnf(6057,plain,
% 242.31/242.42 (P11(f2(f6(f9(f5(a1)))))+~P11(f15(f9(f5(a1))))),
% 242.31/242.42 inference(scs_inference,[],[1,4089,24])).
% 242.31/242.42 cnf(6735,plain,
% 242.31/242.42 (~P10(f2(f13(f5(a1))))),
% 242.31/242.42 inference(scs_inference,[],[1984,1923,10,26])).
% 242.31/242.42 cnf(6736,plain,
% 242.31/242.42 (~P10(f15(f5(a1)))),
% 242.31/242.42 inference(scs_inference,[],[6735,1923,25])).
% 242.31/242.42 cnf(24016,plain,
% 242.31/242.42 (~P10(f15(a1))),
% 242.31/242.42 inference(scs_inference,[],[2651,2,2648,6736,6735,1984,6,28,27,25,26,10])).
% 242.31/242.42 cnf(70327,plain,
% 242.31/242.42 (P3(f6(f9(f5(a1))))+~P4(f6(f9(f5(a1))))),
% 242.31/242.42 inference(scs_inference,[],[6736,9,2182,2107,1984,67,6735,25,28,27,26,16,14])).
% 242.31/242.42 cnf(340084,plain,
% 242.31/242.42 (P6(f5(a1))),
% 242.31/242.42 inference(scs_inference,[],[1,24])).
% 242.31/242.42 cnf(340102,plain,
% 242.31/242.42 (P7(f12(a1),f11(f5(a1)))),
% 242.31/242.42 inference(scs_inference,[],[1,24,394,455,516,640,46,54,56,57,58])).
% 242.31/242.42 cnf(340104,plain,
% 242.31/242.42 (P3(f6(f9(f5(a1))))),
% 242.31/242.42 inference(scs_inference,[],[1,24,394,455,516,640,46,54,56,57,58,70327])).
% 242.31/242.42 cnf(340107,plain,
% 242.31/242.42 (P10(f16(f9(f5(a1))))),
% 242.31/242.42 inference(scs_inference,[],[1801,1,24016,1494,4,24,394,455,516,640,46,54,56,57,58,70327,26,25])).
% 242.31/242.42 cnf(340109,plain,
% 242.31/242.42 (P11(f2(f13(f5(a1))))),
% 242.31/242.42 inference(scs_inference,[],[1801,1923,1,24016,1494,4,1984,24,394,455,516,640,46,54,56,57,58,70327,26,25,27])).
% 242.31/242.42 cnf(340113,plain,
% 242.31/242.42 (P5(f8(f5(a1)))),
% 242.31/242.42 inference(scs_inference,[],[1801,1923,1,24016,2183,6,1494,4,1984,24,394,455,516,640,46,54,56,57,58,70327,26,25,27,28,22])).
% 242.31/242.42 cnf(340115,plain,
% 242.31/242.42 (P5(f9(f5(a1)))),
% 242.31/242.42 inference(scs_inference,[],[1801,1923,1,24016,2183,6,1494,4,1984,24,394,455,516,640,46,54,56,57,58,70327,26,25,27,28,22,23])).
% 242.31/242.42 cnf(340131,plain,
% 242.31/242.42 (~P11(f10(f6(f8(f5(a1)))))),
% 242.31/242.42 inference(scs_inference,[],[340084,3484])).
% 242.31/242.42 cnf(340132,plain,
% 242.31/242.42 (~P11(f10(f13(f9(f5(a1)))))),
% 242.31/242.42 inference(scs_inference,[],[340084,3635])).
% 242.31/242.42 cnf(340133,plain,
% 242.31/242.42 (~P11(f11(f6(f8(f5(a1)))))),
% 242.31/242.42 inference(scs_inference,[],[340084,3786])).
% 242.31/242.42 cnf(340134,plain,
% 242.31/242.42 (P11(f11(f6(f9(f5(a1)))))+~P11(f2(f6(f9(f5(a1)))))),
% 242.31/242.42 inference(scs_inference,[],[340084,4920])).
% 242.31/242.42 cnf(340144,plain,
% 242.31/242.42 (P3(f6(f8(f5(a1))))),
% 242.31/242.42 inference(scs_inference,[],[340113,340115,8,21,17,18,19,14])).
% 242.31/242.42 cnf(340160,plain,
% 242.31/242.42 (P10(f11(f5(a1)))),
% 242.31/242.42 inference(scs_inference,[],[340102,5,25])).
% 242.31/242.42 cnf(340167,plain,
% 242.31/242.42 (P10(f10(f8(f5(a1))))),
% 242.31/242.42 inference(scs_inference,[],[340160,1557,25])).
% 242.31/242.42 cnf(340181,plain,
% 242.31/242.42 (P11(f10(f13(f5(a1))))+P11(f11(f13(f5(a1))))),
% 242.31/242.42 inference(scs_inference,[],[340109,1433,578,24016,2183,2182,4,25,27,26,42])).
% 242.31/242.42 cnf(340183,plain,
% 242.31/242.42 (~P10(f10(f13(f5(a1))))+P11(f11(f13(f5(a1))))),
% 242.31/242.42 inference(scs_inference,[],[340109,1433,578,24016,2183,2182,4,25,27,26,42,10])).
% 242.31/242.42 cnf(340190,plain,
% 242.31/242.42 (~P12(f13(f5(a1)))+~P11(f10(f13(f5(a1))))),
% 242.31/242.42 inference(scs_inference,[],[340107,24016,6735,25,2420,33])).
% 242.31/242.42 cnf(340290,plain,
% 242.31/242.42 (P11(f11(f13(f5(a1))))+~P12(f13(f5(a1)))),
% 242.31/242.42 inference(scs_inference,[],[340190,340181])).
% 242.31/242.42 cnf(361834,plain,
% 242.31/242.42 (~P11(f2(f6(f8(f5(a1)))))),
% 242.31/242.42 inference(scs_inference,[],[340133,340144,40])).
% 242.31/242.42 cnf(361857,plain,
% 242.31/242.42 (~P11(f11(f13(f5(a1))))+P11(f15(f8(f5(a1))))),
% 242.31/242.42 inference(scs_inference,[],[3256,28])).
% 242.31/242.42 cnf(361864,plain,
% 242.31/242.42 (~P11(f10(f13(f5(a1))))+P11(f15(f9(f5(a1))))),
% 242.31/242.42 inference(scs_inference,[],[3332,28])).
% 242.31/242.42 cnf(361890,plain,
% 242.31/242.42 (~P10(f15(f9(f5(a1))))+P10(f10(f13(f5(a1))))),
% 242.31/242.42 inference(scs_inference,[],[3332,25])).
% 242.31/242.42 cnf(361904,plain,
% 242.31/242.42 (P11(f15(f8(f5(a1))))+~P12(f13(f5(a1)))),
% 242.31/242.42 inference(scs_inference,[],[361857,340290])).
% 242.31/242.42 cnf(361952,plain,
% 242.31/242.42 (P7(f10(f8(f5(a1))),f10(f6(f8(f5(a1)))))),
% 242.31/242.42 inference(scs_inference,[],[340113,43])).
% 242.31/242.42 cnf(361954,plain,
% 242.31/242.42 (P7(f10(f8(f5(a1))),f10(f13(f8(f5(a1)))))),
% 242.31/242.42 inference(scs_inference,[],[340113,43,44])).
% 242.31/242.42 cnf(361962,plain,
% 242.31/242.42 (P7(f15(f8(f5(a1))),f2(f6(f8(f5(a1)))))),
% 242.31/242.42 inference(scs_inference,[],[340113,43,44,48,49,50,52])).
% 242.31/242.42 cnf(361974,plain,
% 242.31/242.42 (P7(f11(f9(f5(a1))),f11(f13(f9(f5(a1)))))),
% 242.31/242.42 inference(scs_inference,[],[340084,340113,43,44,48,49,50,52,61,62,63,3028,1372,1679])).
% 242.31/242.42 cnf(361986,plain,
% 242.31/242.42 (P10(f2(f6(f8(f5(a1)))))+~P10(f10(f6(f8(f5(a1)))))),
% 242.31/242.42 inference(scs_inference,[],[5,340144,2651,1984,6735,340084,340113,43,44,48,49,50,52,61,62,63,3028,1372,1679,1862,25,26,28,27,31])).
% 242.31/242.42 cnf(361991,plain,
% 242.31/242.42 (~P12(f6(f8(f5(a1))))+~P10(f10(f6(f8(f5(a1)))))),
% 242.31/242.42 inference(scs_inference,[],[340131,361986,36])).
% 242.31/242.42 cnf(361996,plain,
% 242.31/242.42 (P7(f11(f9(f5(a1))),f11(f6(f9(f5(a1)))))),
% 242.31/242.42 inference(scs_inference,[],[340115,61,50,48])).
% 242.31/242.42 cnf(362000,plain,
% 242.31/242.42 (P7(f10(f9(f5(a1))),f10(f6(f9(f5(a1)))))),
% 242.31/242.42 inference(scs_inference,[],[340115,61,50,48,63,43])).
% 242.31/242.42 cnf(556997,plain,
% 242.31/242.42 (P11(f10(f6(f9(f5(a1)))))+~P11(f2(f6(f9(f5(a1)))))),
% 242.31/242.42 inference(scs_inference,[],[340104,35])).
% 242.31/242.42 cnf(557121,plain,
% 242.31/242.42 (P11(f10(f6(f9(f5(a1)))))+~P11(f15(f9(f5(a1))))),
% 242.31/242.42 inference(scs_inference,[],[556997,6057])).
% 242.31/242.42 cnf(695735,plain,
% 242.31/242.42 (~P3(f13(f5(a1)))),
% 242.31/242.42 inference(scs_inference,[],[361952,361954,361962,340132,340167,361834,2651,340109,27,28,25,361857,361904,361986,340181,340183,361991,35,40])).
% 242.31/242.42 cnf(695741,plain,
% 242.31/242.42 (P11(f15(f9(f5(a1))))),
% 242.31/242.42 inference(scs_inference,[],[361952,361954,361962,340132,340167,361834,2651,7,340109,27,28,25,361857,361904,361986,340181,340183,361991,35,40,14,26,361864])).
% 242.31/242.42 cnf(695743,plain,
% 242.31/242.42 (P11(f10(f6(f9(f5(a1)))))),
% 242.31/242.42 inference(scs_inference,[],[361952,361954,361962,340132,340167,361834,2651,7,340109,27,28,25,361857,361904,361986,340181,340183,361991,35,40,14,26,361864,361890,557121])).
% 242.31/242.42 cnf(695747,plain,
% 242.31/242.42 (P11(f2(f6(f9(f5(a1)))))),
% 242.31/242.42 inference(scs_inference,[],[695741,6057])).
% 242.31/242.42 cnf(695756,plain,
% 242.31/242.42 (P11(f11(f6(f9(f5(a1)))))),
% 242.31/242.42 inference(scs_inference,[],[695747,340134])).
% 242.31/242.42 cnf(695811,plain,
% 242.31/242.42 (P11(f11(f9(f5(a1))))),
% 242.31/242.42 inference(scs_inference,[],[361996,695756,695735,7,14,28])).
% 242.31/242.42 cnf(695832,plain,
% 242.31/242.42 ($false),
% 242.31/242.42 inference(scs_inference,[],[362000,695811,361974,695743,695735,2194,7,14,27,28]),
% 242.31/242.42 ['proof']).
% 242.76/242.83 % SZS output end Proof
% 242.76/242.83 % Total time :241.040000s
%------------------------------------------------------------------------------