%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : HWV008-2.002 : 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 : n025.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:07 EDT 2024
% Result : Unsatisfiable 116.60s 117.79s
% Output : CNFRefutation 117.10s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : HWV008-2.002 : TPTP v8.2.0. Bugfixed v2.7.0.
% 0.03/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.13/0.34 % Computer : n025.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:51:39 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.51/0.58 start to proof:theBenchmark
% 116.55/117.76 %-------------------------------------------
% 116.55/117.76 % File :CSE---1.7
% 116.55/117.76 % Problem :theBenchmark
% 116.55/117.76 % Transform :cnf
% 116.55/117.76 % Format :tptp:raw
% 116.55/117.76 % Command :java -jar mcs_scs.jar %d %s
% 116.55/117.76
% 116.55/117.76 % Result :Theorem 115.910000s
% 116.55/117.76 % Output :CNFRefutation 115.910000s
% 116.55/117.76 %-------------------------------------------
% 116.60/117.79 %--------------------------------------------------------------------------
% 116.60/117.79 % File : HWV008-2.002 : TPTP v8.2.0. Bugfixed v2.7.0.
% 116.60/117.79 % Domain : Hardware Verification
% 116.60/117.79 % Problem : 2 bit ripple carry adder
% 116.60/117.79 % Version : [Gei96] axioms.
% 116.60/117.79 % English :
% 116.60/117.79
% 116.60/117.79 % Refs : [Gei96] Geisler (1996), Email to G. Sutcliffe
% 116.60/117.79 % Source : [Gei96]
% 116.60/117.79 % Names :
% 116.60/117.79
% 116.60/117.79 % Status : Unsatisfiable
% 116.60/117.79 % Rating : 0.00 v7.5.0, 0.17 v7.4.0, 0.00 v7.0.0, 0.12 v6.3.0, 0.14 v6.2.0, 0.00 v3.1.0, 0.17 v2.7.0
% 116.60/117.79 % Syntax : Number of clauses : 74 ( 12 unt; 5 nHn; 74 RR)
% 116.60/117.79 % Number of literals : 163 ( 0 equ; 91 neg)
% 116.60/117.79 % Maximal clause size : 4 ( 2 avg)
% 116.60/117.79 % Maximal term depth : 4 ( 2 avg)
% 116.60/117.79 % Number of predicates : 13 ( 13 usr; 0 prp; 1-2 aty)
% 116.60/117.79 % Number of functors : 20 ( 20 usr; 1 con; 0-1 aty)
% 116.60/117.79 % Number of variables : 66 ( 0 sgn)
% 116.60/117.79 % SPC : CNF_UNS_RFO_NEQ_NHN
% 116.60/117.79
% 116.60/117.79 % Comments :
% 116.60/117.79 % Bugfixes : v2.2.0 - Missing conjecture clauses added.
% 116.60/117.79 % : v2.7.0 - Bugfix in HWV002-0.ax
% 116.60/117.79 %--------------------------------------------------------------------------
% 116.60/117.79 %----Include basic diagnosis axioms
% 116.60/117.79 include('Axioms/HWV002-0.ax').
% 116.60/117.79 %----Include model of halfadder
% 116.60/117.79 include('Axioms/HWV002-1.ax').
% 116.60/117.79 %----Include model of fulladder
% 116.60/117.79 include('Axioms/HWV002-2.ax').
% 116.60/117.79 %--------------------------------------------------------------------------
% 116.60/117.79 %----Composition of 2-bit adder
% 116.60/117.79 cnf(nbit_adder_fulladder1,axiom,
% 116.60/117.79 ( ~ nbit_adder2(X)
% 116.60/117.79 | fulladder(f1(X)) ) ).
% 116.60/117.79
% 116.60/117.79 cnf(nbit_adder_fulladder2,axiom,
% 116.60/117.79 ( ~ nbit_adder2(X)
% 116.60/117.79 | fulladder(f2(X)) ) ).
% 116.60/117.79
% 116.60/117.79 %----Connections of 2-bit adder
% 116.60/117.79 cnf(nbit_adder_connection_out1_out1f1,axiom,
% 116.60/117.79 ( ~ nbit_adder2(X)
% 116.60/117.79 | connection(out1(X),out1(f1(X))) ) ).
% 116.60/117.79
% 116.60/117.79 cnf(nbit_adder_connection_out2_out1f2,axiom,
% 116.60/117.79 ( ~ nbit_adder2(X)
% 116.60/117.79 | connection(out2(X),out1(f2(X))) ) ).
% 116.60/117.79
% 116.60/117.79 cnf(nbit_adder_connection_outc_outcf1,axiom,
% 116.60/117.79 ( ~ nbit_adder2(X)
% 116.60/117.79 | connection(outc(X),outc(f2(X))) ) ).
% 116.60/117.79
% 116.60/117.79 cnf(nbit_adder_connection_ina1_in1f1,axiom,
% 116.60/117.79 ( ~ nbit_adder2(X)
% 116.60/117.79 | connection(ina1(X),in1(f1(X))) ) ).
% 116.60/117.79
% 116.60/117.79 cnf(nbit_adder_connection_inb1_in2f1,axiom,
% 116.60/117.79 ( ~ nbit_adder2(X)
% 116.60/117.79 | connection(inb1(X),in2(f1(X))) ) ).
% 116.60/117.79
% 116.60/117.79 cnf(nbit_adder_connection_ina2_in1f2,axiom,
% 116.60/117.79 ( ~ nbit_adder2(X)
% 116.60/117.79 | connection(ina2(X),in1(f2(X))) ) ).
% 116.60/117.79
% 116.60/117.79 cnf(nbit_adder_connection_inb2_in2f2,axiom,
% 116.60/117.79 ( ~ nbit_adder2(X)
% 116.60/117.79 | connection(inb2(X),in2(f2(X))) ) ).
% 116.60/117.79
% 116.60/117.79 cnf(nbit_adder_connection_inc_incf1,axiom,
% 116.60/117.79 ( ~ nbit_adder2(X)
% 116.60/117.79 | connection(outc(f1(X)),inc(f2(X))) ) ).
% 116.60/117.79
% 116.60/117.79 cnf(nbit_adder_connection_inc_incf2,axiom,
% 116.60/117.79 ( ~ nbit_adder2(X)
% 116.60/117.79 | connection(inc(X),inc(f1(X))) ) ).
% 116.60/117.79
% 116.60/117.79 %----Observations
% 116.60/117.79 cnf(a_isa_2bit_adder,hypothesis,
% 116.60/117.79 nbit_adder2(a) ).
% 116.60/117.79
% 116.60/117.79 cnf(ina1_0,hypothesis,
% 116.60/117.79 zero(ina1(a)) ).
% 116.60/117.79
% 116.60/117.79 cnf(ina2_0,hypothesis,
% 116.60/117.79 zero(ina2(a)) ).
% 116.60/117.79
% 116.60/117.79 cnf(inb1_0,hypothesis,
% 116.60/117.79 zero(inb1(a)) ).
% 116.60/117.79
% 116.60/117.79 cnf(inb2_0,hypothesis,
% 116.60/117.79 zero(inb2(a)) ).
% 116.60/117.79
% 116.60/117.79 cnf(inc_0,hypothesis,
% 116.60/117.79 zero(inc(a)) ).
% 116.60/117.79
% 116.60/117.79 cnf(out1_0,hypothesis,
% 116.60/117.79 zero(out1(a)) ).
% 116.60/117.79
% 116.60/117.79 cnf(out2_0,hypothesis,
% 116.60/117.79 zero(out2(a)) ).
% 116.60/117.79
% 116.60/117.79 cnf(outc_1,hypothesis,
% 116.60/117.79 one(outc(a)) ).
% 116.60/117.79
% 116.60/117.79 %----Minimal diagnosis
% 116.60/117.79 cnf(diagnosis_or1f2a,negated_conjecture,
% 116.60/117.79 ~ abnormal(or1(f2(a))) ).
% 116.60/117.79
% 116.60/117.79 cnf(diagnosis_and2h1f2a,negated_conjecture,
% 116.60/117.79 ~ abnormal(and2(h1(f2(a)))) ).
% 116.60/117.79
% 116.60/117.79 cnf(diagnosis_and2h2f2a,negated_conjecture,
% 116.60/117.79 ~ abnormal(and2(h2(f2(a)))) ).
% 116.60/117.79
% 116.60/117.79 %--------------------------------------------------------------------------
% 116.60/117.79 %-------------------------------------------
% 116.60/117.79 % Proof found
% 116.60/117.79 % SZS status Theorem for theBenchmark
% 116.60/117.79 % SZS output start Proof
% 116.60/117.81 %ClaNum:74(EqnAxiom:0)
% 116.60/117.81 %VarNum:181(SingletonVarNum:66)
% 116.60/117.81 %MaxLitNum:4
% 116.60/117.82 %MaxfuncDepth:3
% 116.60/117.82 %SharedTerms:27
% 116.60/117.82 %goalClause: 10 11 12
% 116.60/117.82 %singleGoalClaCount:3
% 116.60/117.82 [1]P1(a1)
% 116.60/117.82 [2]P10(f2(a1))
% 116.60/117.82 [3]P10(f3(a1))
% 116.60/117.82 [4]P10(f18(a1))
% 116.60/117.82 [5]P10(f4(a1))
% 116.60/117.82 [6]P10(f13(a1))
% 116.60/117.82 [7]P10(f14(a1))
% 116.60/117.82 [8]P10(f15(a1))
% 116.60/117.82 [9]P11(f19(a1))
% 116.60/117.82 [10]~P2(f16(f5(a1)))
% 116.60/117.82 [11]~P2(f6(f9(f5(a1))))
% 116.60/117.82 [12]~P2(f6(f10(f5(a1))))
% 116.60/117.82 [13]~P11(x131)+~P10(x131)
% 116.60/117.82 [14]~P2(x141)+~P3(x141)
% 116.60/117.82 [15]~P13(x151)+~P2(x151)
% 116.60/117.82 [16]~P12(x161)+~P2(x161)
% 116.60/117.82 [20]~P5(x201)+P4(f7(x201))
% 116.60/117.82 [21]~P5(x211)+P4(f6(x211))
% 116.60/117.82 [22]~P5(x221)+P8(f16(x221))
% 116.60/117.82 [23]~P6(x231)+P8(f16(x231))
% 116.60/117.82 [24]~P5(x241)+P9(f17(x241))
% 116.60/117.82 [25]~P6(x251)+P5(f9(x251))
% 116.60/117.82 [26]~P6(x261)+P5(f10(x261))
% 116.60/117.82 [27]~P1(x271)+P6(f8(x271))
% 116.60/117.82 [28]~P1(x281)+P6(f5(x281))
% 116.60/117.82 [47]~P5(x471)+P7(f11(x471),f11(f6(x471)))
% 116.60/117.82 [48]~P5(x481)+P7(f11(x481),f11(f16(x481)))
% 116.60/117.82 [49]~P6(x491)+P7(f11(x491),f11(f10(x491)))
% 116.60/117.82 [50]~P1(x501)+P7(f2(x501),f2(f8(x501)))
% 116.60/117.82 [51]~P6(x511)+P7(f12(x511),f11(f9(x511)))
% 116.60/117.82 [52]~P5(x521)+P7(f12(x521),f12(f6(x521)))
% 116.60/117.82 [53]~P5(x531)+P7(f12(x531),f12(f16(x531)))
% 116.60/117.82 [54]~P5(x541)+P7(f20(x541),f2(f7(x541)))
% 116.60/117.82 [55]~P6(x551)+P7(f20(x551),f20(f10(x551)))
% 116.60/117.82 [56]~P5(x561)+P7(f19(x561),f2(f6(x561)))
% 116.60/117.82 [57]~P6(x571)+P7(f19(x571),f2(f16(x571)))
% 116.60/117.82 [58]~P1(x581)+P7(f19(x581),f19(f5(x581)))
% 116.60/117.82 [59]~P6(x591)+P7(f3(x591),f12(f9(x591)))
% 116.60/117.82 [60]~P1(x601)+P7(f3(x601),f3(f8(x601)))
% 116.60/117.82 [61]~P1(x611)+P7(f18(x611),f2(f5(x611)))
% 116.60/117.82 [62]~P1(x621)+P7(f4(x621),f11(f8(x621)))
% 116.60/117.82 [63]~P1(x631)+P7(f13(x631),f12(f8(x631)))
% 116.60/117.82 [64]~P1(x641)+P7(f14(x641),f11(f5(x641)))
% 116.60/117.82 [65]~P1(x651)+P7(f15(x651),f12(f5(x651)))
% 116.60/117.82 [68]~P5(x681)+P7(f2(f6(x681)),f11(f17(x681)))
% 116.60/117.82 [69]~P5(x691)+P7(f2(f17(x691)),f12(f7(x691)))
% 116.60/117.82 [70]~P5(x701)+P7(f2(f16(x701)),f11(f7(x701)))
% 116.60/117.82 [71]~P6(x711)+P7(f20(f9(x711)),f12(f10(x711)))
% 116.60/117.82 [72]~P6(x721)+P7(f19(f9(x721)),f12(f16(x721)))
% 116.60/117.82 [73]~P6(x731)+P7(f19(f10(x731)),f11(f16(x731)))
% 116.60/117.82 [74]~P1(x741)+P7(f19(f8(x741)),f3(f5(x741)))
% 116.60/117.82 [17]P2(x171)+~P4(x171)+P3(x171)
% 116.60/117.82 [18]P13(x181)+~P8(x181)+P2(x181)
% 116.60/117.82 [19]P12(x191)+~P9(x191)+P2(x191)
% 116.60/117.82 [33]~P13(x331)+~P10(f2(x331))+P10(f11(x331))
% 116.60/117.82 [34]~P12(x341)+~P11(f2(x341))+P10(f11(x341))
% 116.60/117.82 [35]~P3(x351)+~P10(f11(x351))+P10(f2(x351))
% 116.60/117.82 [36]~P3(x361)+~P10(f12(x361))+P10(f2(x361))
% 116.60/117.82 [37]~P12(x371)+~P11(f11(x371))+P10(f2(x371))
% 116.60/117.82 [38]~P13(x381)+~P10(f2(x381))+P10(f12(x381))
% 116.60/117.82 [39]~P3(x391)+~P11(f2(x391))+P11(f11(x391))
% 116.60/117.82 [40]~P12(x401)+~P10(f2(x401))+P11(f11(x401))
% 116.60/117.82 [41]~P13(x411)+~P11(f11(x411))+P11(f2(x411))
% 116.60/117.82 [42]~P13(x421)+~P11(f12(x421))+P11(f2(x421))
% 116.60/117.82 [43]~P12(x431)+~P10(f11(x431))+P11(f2(x431))
% 116.60/117.82 [44]~P3(x441)+~P11(f2(x441))+P11(f12(x441))
% 116.60/117.82 [29]~P7(x292,x291)+P10(x291)+~P10(x292)
% 116.60/117.82 [30]~P7(x301,x302)+P10(x301)+~P10(x302)
% 116.60/117.82 [31]~P7(x312,x311)+P11(x311)+~P11(x312)
% 116.60/117.82 [32]~P7(x321,x322)+P11(x321)+~P11(x322)
% 116.60/117.82 [45]~P3(x451)+P10(f12(x451))+~P10(f2(x451))+P10(f11(x451))
% 116.60/117.82 [46]~P13(x461)+P11(f12(x461))+~P11(f2(x461))+P11(f11(x461))
% 116.60/117.82 [66]~P13(x661)+~P10(f11(x661))+~P10(f12(x661))+P10(f2(x661))
% 116.60/117.82 [67]~P3(x671)+~P11(f11(x671))+~P11(f12(x671))+P11(f2(x671))
% 116.60/117.82 %EqnAxiom
% 116.60/117.82
% 116.60/117.82 %-------------------------------------------
% 116.92/118.10 cnf(109,plain,
% 116.92/118.10 (~P11(f13(a1))),
% 116.92/118.10 inference(scs_inference,[],[6,13])).
% 116.92/118.10 cnf(121,plain,
% 116.92/118.10 (~P11(f15(a1))),
% 116.92/118.10 inference(scs_inference,[],[8,13])).
% 116.92/118.10 cnf(407,plain,
% 116.92/118.10 (~P6(x4071)+P4(f7(f9(x4071)))),
% 116.92/118.10 inference(scs_inference,[],[20,25])).
% 116.92/118.10 cnf(468,plain,
% 116.92/118.10 (~P6(x4681)+P4(f6(f10(x4681)))),
% 116.92/118.10 inference(scs_inference,[],[21,26])).
% 116.92/118.10 cnf(529,plain,
% 116.92/118.10 (~P6(x5291)+P8(f16(f9(x5291)))),
% 116.92/118.10 inference(scs_inference,[],[22,25])).
% 116.92/118.10 cnf(658,plain,
% 116.92/118.10 (~P6(x6581)+P9(f17(f10(x6581)))),
% 116.92/118.10 inference(scs_inference,[],[24,26])).
% 116.92/118.10 cnf(719,plain,
% 116.92/118.10 (P7(f11(f5(a1)),f11(f10(f5(a1))))),
% 116.92/118.10 inference(scs_inference,[],[1,28,49])).
% 116.92/118.10 cnf(1207,plain,
% 116.92/118.10 (P3(f6(f10(f5(a1))))+~P6(f5(a1))),
% 116.92/118.10 inference(scs_inference,[],[12,468,17])).
% 116.92/118.10 cnf(1390,plain,
% 116.92/118.10 (~P6(x13901)+P7(f11(f9(x13901)),f11(f6(f9(x13901))))),
% 116.92/118.10 inference(scs_inference,[],[47,25])).
% 116.92/118.10 cnf(1451,plain,
% 116.92/118.10 (~P6(x14511)+P7(f11(f10(x14511)),f11(f16(f10(x14511))))),
% 116.92/118.10 inference(scs_inference,[],[48,26])).
% 116.92/118.10 cnf(2012,plain,
% 116.92/118.10 (P7(f12(f8(a1)),f11(f9(f8(a1))))),
% 116.92/118.10 inference(scs_inference,[],[1,51,27])).
% 116.92/118.10 cnf(2073,plain,
% 116.92/118.10 (~P6(x20731)+P7(f12(f9(x20731)),f12(f6(f9(x20731))))),
% 116.92/118.10 inference(scs_inference,[],[52,25])).
% 116.92/118.10 cnf(2134,plain,
% 116.92/118.10 (~P6(x21341)+P7(f12(f10(x21341)),f12(f16(f10(x21341))))),
% 116.92/118.10 inference(scs_inference,[],[53,26])).
% 116.92/118.10 cnf(2195,plain,
% 116.92/118.10 (~P6(x21951)+P7(f20(f9(x21951)),f2(f7(f9(x21951))))),
% 116.92/118.10 inference(scs_inference,[],[54,25])).
% 116.92/118.10 cnf(2317,plain,
% 116.92/118.10 (~P6(x23171)+P7(f19(f10(x23171)),f2(f6(f10(x23171))))),
% 116.92/118.10 inference(scs_inference,[],[56,26])).
% 116.92/118.10 cnf(2439,plain,
% 116.92/118.10 (P11(f19(f5(a1)))),
% 116.92/118.10 inference(scs_inference,[],[1,9,58,31])).
% 116.92/118.10 cnf(2561,plain,
% 116.92/118.10 (P10(f3(f8(a1)))),
% 116.92/118.10 inference(scs_inference,[],[1,3,60,29])).
% 116.92/118.10 cnf(2562,plain,
% 116.92/118.10 (~P11(f3(f8(a1)))),
% 116.92/118.10 inference(scs_inference,[],[2561,13])).
% 116.92/118.10 cnf(2685,plain,
% 116.92/118.10 (P10(f11(f8(a1)))),
% 116.92/118.10 inference(scs_inference,[],[1,5,62,29])).
% 116.92/118.10 cnf(2755,plain,
% 116.92/118.10 (~P11(f12(f8(a1)))),
% 116.92/118.10 inference(scs_inference,[],[1,109,63,32])).
% 116.92/118.10 cnf(2758,plain,
% 116.92/118.10 (~P11(f11(f9(f8(a1))))),
% 116.92/118.10 inference(scs_inference,[],[2755,2439,2012,31,32])).
% 116.92/118.10 cnf(2831,plain,
% 116.92/118.10 (P10(f11(f5(a1)))),
% 116.92/118.10 inference(scs_inference,[],[1,7,64,29])).
% 116.92/118.10 cnf(2832,plain,
% 116.92/118.10 (~P11(f11(f5(a1)))),
% 116.92/118.10 inference(scs_inference,[],[2831,13])).
% 116.92/118.10 cnf(2845,plain,
% 116.92/118.10 (~P11(f11(f10(f5(a1))))),
% 116.92/118.10 inference(scs_inference,[],[2755,2832,2439,719,31,32])).
% 116.92/118.10 cnf(2989,plain,
% 116.92/118.10 (~P11(f12(f5(a1)))),
% 116.92/118.10 inference(scs_inference,[],[1,121,65,32])).
% 116.92/118.10 cnf(3292,plain,
% 116.92/118.10 (~P6(f5(a1))+~P10(f11(f6(f10(f5(a1)))))+P10(f2(f6(f10(f5(a1)))))),
% 116.92/118.10 inference(scs_inference,[],[1207,35])).
% 116.92/118.10 cnf(3444,plain,
% 116.92/118.10 (~P6(x34441)+P7(f2(f6(f9(x34441))),f11(f17(f9(x34441))))),
% 116.92/118.10 inference(scs_inference,[],[68,25])).
% 116.92/118.11 cnf(3520,plain,
% 116.92/118.11 (~P6(x35201)+P7(f2(f17(f10(x35201))),f12(f7(f10(x35201))))),
% 116.92/118.11 inference(scs_inference,[],[69,26])).
% 116.92/118.11 cnf(3748,plain,
% 116.92/118.11 (P7(f19(f9(f5(a1))),f12(f16(f5(a1))))),
% 116.92/118.11 inference(scs_inference,[],[1,72,28])).
% 116.92/118.11 cnf(4128,plain,
% 116.92/118.11 (~P11(f11(f6(f9(f8(a1)))))+~P6(f8(a1))),
% 116.92/118.11 inference(scs_inference,[],[2758,1390,32])).
% 116.92/118.11 cnf(4279,plain,
% 116.92/118.11 (~P11(f11(f16(f10(f5(a1)))))+~P6(f5(a1))),
% 116.92/118.11 inference(scs_inference,[],[2845,1451,32])).
% 116.92/118.11 cnf(4430,plain,
% 116.92/118.11 (P10(f12(f6(f9(x44301))))+~P10(f12(f9(x44301)))+~P6(x44301)),
% 116.92/118.11 inference(scs_inference,[],[2073,29])).
% 116.92/118.11 cnf(16227,plain,
% 116.92/118.11 (~P10(f19(f5(a1)))),
% 116.92/118.11 inference(scs_inference,[],[2439,13])).
% 116.92/118.11 cnf(16238,plain,
% 116.92/118.11 (~P10(f19(a1))),
% 116.92/118.11 inference(scs_inference,[],[9,13])).
% 116.92/118.11 cnf(16433,plain,
% 116.92/118.11 (~P8(f16(f5(a1)))+P13(f16(f5(a1)))),
% 116.92/118.11 inference(scs_inference,[],[2562,10,2,2439,16227,30,29,31,32,18])).
% 116.92/118.11 cnf(42225,plain,
% 116.92/118.11 (P3(f6(f9(f5(a1))))+~P5(f9(f5(a1)))),
% 116.92/118.11 inference(scs_inference,[],[11,2831,2758,2989,2439,16227,30,32,31,29,17,21])).
% 116.92/118.11 cnf(42227,plain,
% 116.92/118.11 (P3(f6(f9(f5(a1))))+~P6(f5(a1))),
% 116.92/118.11 inference(scs_inference,[],[11,2831,2758,2989,2439,16227,30,32,31,29,17,21,25])).
% 116.92/118.11 cnf(42425,plain,
% 116.92/118.11 (~P6(f5(a1))+~P10(f11(f6(f9(f5(a1)))))+P10(f2(f6(f9(f5(a1)))))),
% 116.92/118.11 inference(scs_inference,[],[42227,35])).
% 116.92/118.11 cnf(42651,plain,
% 116.92/118.11 (~P5(f9(f5(a1)))+~P10(f11(f6(f9(f5(a1)))))+P10(f2(f6(f9(f5(a1)))))),
% 116.92/118.11 inference(scs_inference,[],[42225,35])).
% 116.92/118.11 cnf(43907,plain,
% 116.92/118.11 (~P4(f6(f10(f5(a1))))+P3(f6(f10(f5(a1))))),
% 116.92/118.11 inference(scs_inference,[],[12,2989,2685,2439,16227,30,31,29,32,17])).
% 116.92/118.11 cnf(188968,plain,
% 116.92/118.11 (P6(f8(a1))),
% 116.92/118.11 inference(scs_inference,[],[1,27])).
% 116.92/118.11 cnf(188994,plain,
% 116.92/118.11 (P7(f13(a1),f12(f8(a1)))),
% 116.92/118.11 inference(scs_inference,[],[1,27,407,468,529,658,49,50,55,58,59,60,61,62,63])).
% 116.92/118.11 cnf(188998,plain,
% 116.92/118.11 (P7(f15(a1),f12(f5(a1)))),
% 116.92/118.11 inference(scs_inference,[],[1,27,407,468,529,658,49,50,55,58,59,60,61,62,63,64,65])).
% 116.92/118.11 cnf(189004,plain,
% 116.92/118.11 (P5(f9(f8(a1)))),
% 116.92/118.11 inference(scs_inference,[],[1,27,407,468,529,658,49,50,55,58,59,60,61,62,63,64,65,72,74,25])).
% 116.92/118.11 cnf(189006,plain,
% 116.92/118.11 (P6(f5(a1))),
% 116.92/118.11 inference(scs_inference,[],[1,27,407,468,529,658,49,50,55,58,59,60,61,62,63,64,65,72,74,25,28])).
% 116.92/118.11 cnf(189014,plain,
% 116.92/118.11 (P10(f12(f9(f8(a1))))),
% 116.92/118.11 inference(scs_inference,[],[2755,1,2,2561,16238,2439,27,407,468,529,658,49,50,55,58,59,60,61,62,63,64,65,72,74,25,28,21,30,31,29])).
% 116.92/118.11 cnf(189020,plain,
% 116.92/118.11 (P5(f10(f8(a1)))),
% 116.92/118.11 inference(scs_inference,[],[2755,1,2,2561,16238,9,2439,27,407,468,529,658,49,50,55,58,59,60,61,62,63,64,65,72,74,25,28,21,30,31,29,32,24,26])).
% 116.92/118.11 cnf(189022,plain,
% 116.92/118.11 (P7(f12(f5(a1)),f11(f9(f5(a1))))),
% 116.92/118.11 inference(scs_inference,[],[2755,1,2,2561,16238,9,2439,27,407,468,529,658,49,50,55,58,59,60,61,62,63,64,65,72,74,25,28,21,30,31,29,32,24,26,51])).
% 116.92/118.11 cnf(189024,plain,
% 116.92/118.11 (P7(f19(f5(a1)),f2(f16(f5(a1))))),
% 116.92/118.11 inference(scs_inference,[],[2755,1,2,2561,16238,9,2439,27,407,468,529,658,49,50,55,58,59,60,61,62,63,64,65,72,74,25,28,21,30,31,29,32,24,26,51,57])).
% 116.92/118.11 cnf(189028,plain,
% 116.92/118.11 (P7(f19(f10(f5(a1))),f11(f16(f5(a1))))),
% 116.92/118.11 inference(scs_inference,[],[2755,1,2,2561,16238,9,2439,27,407,468,529,658,49,50,55,58,59,60,61,62,63,64,65,72,74,25,28,21,30,31,29,32,24,26,51,57,71,73])).
% 116.92/118.11 cnf(189032,plain,
% 116.92/118.11 (P8(f16(f5(a1)))),
% 116.92/118.11 inference(scs_inference,[],[2755,1,2,2561,16238,9,2439,27,407,468,529,658,49,50,55,58,59,60,61,62,63,64,65,72,74,25,28,21,30,31,29,32,24,26,51,57,71,73,22,23])).
% 116.92/118.11 cnf(189042,plain,
% 116.92/118.11 (P10(f2(f6(f10(f5(a1)))))+~P10(f11(f6(f10(f5(a1)))))),
% 116.92/118.11 inference(scs_inference,[],[189006,3292])).
% 116.92/118.11 cnf(189043,plain,
% 116.92/118.11 (~P11(f11(f6(f9(f8(a1)))))),
% 116.92/118.11 inference(scs_inference,[],[188968,4128])).
% 116.92/118.11 cnf(189044,plain,
% 116.92/118.11 (~P11(f11(f16(f10(f5(a1)))))),
% 116.92/118.11 inference(scs_inference,[],[189006,4279])).
% 116.92/118.11 cnf(189049,plain,
% 116.92/118.11 (P13(f16(f5(a1)))),
% 116.92/118.11 inference(scs_inference,[],[189032,16433])).
% 116.92/118.11 cnf(189052,plain,
% 116.92/118.11 (P3(f6(f9(f5(a1))))),
% 116.92/118.11 inference(scs_inference,[],[189006,42227])).
% 116.92/118.11 cnf(189053,plain,
% 116.92/118.11 (P10(f2(f6(f9(f5(a1)))))+~P10(f11(f6(f9(f5(a1)))))),
% 116.92/118.11 inference(scs_inference,[],[189006,42425])).
% 116.92/118.11 cnf(189054,plain,
% 116.92/118.11 (P5(f10(f5(a1)))),
% 116.92/118.11 inference(scs_inference,[],[189006,26])).
% 116.92/118.11 cnf(189056,plain,
% 116.92/118.11 (P5(f9(f5(a1)))),
% 116.92/118.11 inference(scs_inference,[],[189006,26,25])).
% 116.92/118.11 cnf(189060,plain,
% 116.92/118.11 (P4(f6(f10(f5(a1))))),
% 116.92/118.11 inference(scs_inference,[],[189006,26,25,24,468])).
% 116.92/118.11 cnf(189072,plain,
% 116.92/118.11 (~P10(f2(f16(f5(a1))))),
% 116.92/118.11 inference(scs_inference,[],[189006,189020,189024,16227,26,25,24,468,20,529,22,407,21,30])).
% 116.92/118.11 cnf(189074,plain,
% 116.92/118.11 (P11(f2(f16(f5(a1))))),
% 116.92/118.11 inference(scs_inference,[],[189006,189020,189024,16227,2439,26,25,24,468,20,529,22,407,21,30,31])).
% 116.92/118.11 cnf(189086,plain,
% 116.92/118.11 (~P10(f11(f6(f9(f5(a1)))))+P10(f2(f6(f9(f5(a1)))))),
% 116.92/118.11 inference(scs_inference,[],[189056,42651])).
% 116.92/118.11 cnf(189088,plain,
% 116.92/118.11 (P3(f6(f10(f5(a1))))),
% 116.92/118.11 inference(scs_inference,[],[189060,43907])).
% 116.92/118.11 cnf(189106,plain,
% 116.92/118.11 (P10(f12(f8(a1)))),
% 116.92/118.11 inference(scs_inference,[],[188994,6,29])).
% 116.92/118.11 cnf(189116,plain,
% 116.92/118.11 (P10(f11(f9(f8(a1))))),
% 116.92/118.11 inference(scs_inference,[],[189106,2012,189072,2,30,29])).
% 116.92/118.11 cnf(189125,plain,
% 116.92/118.11 (P10(f12(f5(a1)))),
% 116.92/118.11 inference(scs_inference,[],[188998,8,29])).
% 116.92/118.11 cnf(189127,plain,
% 116.92/118.11 (~P11(f11(f9(f5(a1))))),
% 116.92/118.11 inference(scs_inference,[],[189022,188998,2989,8,29,32])).
% 116.92/118.11 cnf(189135,plain,
% 116.92/118.11 (P10(f11(f9(f5(a1))))),
% 116.92/118.11 inference(scs_inference,[],[189125,189022,189072,2,30,29])).
% 116.92/118.11 cnf(189143,plain,
% 116.92/118.11 (P10(f11(f10(f5(a1))))),
% 116.92/118.11 inference(scs_inference,[],[719,2831,29])).
% 116.92/118.11 cnf(200918,plain,
% 116.92/118.11 (~P3(f16(f5(a1)))+P11(f12(f16(f5(a1))))),
% 116.92/118.11 inference(scs_inference,[],[189135,3,2562,16227,189074,31,29,30,44])).
% 116.92/118.11 cnf(202250,plain,
% 116.92/118.11 (P7(f12(f9(f8(a1))),f12(f16(f9(f8(a1)))))),
% 116.92/118.11 inference(scs_inference,[],[189004,47,48,52,53])).
% 116.92/118.11 cnf(202252,plain,
% 116.92/118.11 (P7(f20(f9(f8(a1))),f2(f7(f9(f8(a1)))))),
% 116.92/118.11 inference(scs_inference,[],[189004,47,48,52,53,54])).
% 116.92/118.11 cnf(202262,plain,
% 116.92/118.11 (P7(f11(f9(f5(a1))),f11(f6(f9(f5(a1)))))),
% 116.92/118.11 inference(scs_inference,[],[189004,189006,47,48,52,53,54,56,68,69,70,1390])).
% 116.92/118.11 cnf(202282,plain,
% 116.92/118.11 (P7(f2(f6(f9(f5(a1)))),f11(f17(f9(f5(a1)))))),
% 116.92/118.11 inference(scs_inference,[],[189043,189004,188968,189006,189116,2758,189074,47,48,52,53,54,56,68,69,70,1390,2134,3520,29,31,32,1451,2073,2195,2317,3444])).
% 116.92/118.11 cnf(202303,plain,
% 116.92/118.11 (P10(f11(f6(f9(f5(a1)))))),
% 116.92/118.11 inference(scs_inference,[],[202262,189135,29])).
% 116.92/118.11 cnf(202311,plain,
% 116.92/118.11 (~P11(f2(f6(f9(f5(a1)))))),
% 116.92/118.11 inference(scs_inference,[],[189044,202262,189006,189135,189127,189052,189074,29,31,32,4430,39])).
% 116.92/118.11 cnf(202319,plain,
% 116.92/118.11 (P10(f2(f6(f9(f5(a1)))))),
% 116.92/118.11 inference(scs_inference,[],[202303,189053])).
% 116.92/118.11 cnf(202320,plain,
% 116.92/118.11 (P10(f2(f6(f9(f5(a1)))))),
% 116.92/118.11 inference(scs_inference,[],[202303,189086])).
% 116.92/118.11 cnf(202344,plain,
% 116.92/118.11 (P7(f19(f10(f5(a1))),f2(f6(f10(f5(a1)))))),
% 116.92/118.11 inference(scs_inference,[],[202319,202282,189020,189054,202311,189006,29,32,53,47,3520,56])).
% 116.92/118.11 cnf(202397,plain,
% 116.92/118.11 (P7(f11(f10(f5(a1))),f11(f6(f10(f5(a1)))))),
% 116.92/118.11 inference(scs_inference,[],[202250,189054,189014,29,47])).
% 116.92/118.11 cnf(202401,plain,
% 116.92/118.11 (P7(f19(f9(f5(a1))),f2(f6(f9(f5(a1)))))),
% 116.92/118.11 inference(scs_inference,[],[202250,189054,189056,189014,29,47,53,56])).
% 116.92/118.11 cnf(202409,plain,
% 116.92/118.11 (P7(f2(f6(f10(f5(a1)))),f11(f17(f10(f5(a1)))))),
% 116.92/118.11 inference(scs_inference,[],[202250,189054,189056,189014,29,47,53,56,70,54,52,68])).
% 116.92/118.11 cnf(202413,plain,
% 116.92/118.11 (~P11(f19(f9(f5(a1))))),
% 116.92/118.11 inference(scs_inference,[],[202252,202250,202311,189054,189056,189014,29,47,53,56,70,54,52,68,30,31])).
% 116.92/118.11 cnf(202415,plain,
% 116.92/118.11 (~P11(f12(f16(f5(a1))))),
% 116.92/118.11 inference(scs_inference,[],[202252,202250,3748,202311,189054,189056,189014,29,47,53,56,70,54,52,68,30,31,32])).
% 116.92/118.11 cnf(202417,plain,
% 116.92/118.11 (P11(f11(f16(f5(a1))))),
% 116.92/118.11 inference(scs_inference,[],[202252,202250,3748,202311,189054,189056,189049,189014,189074,29,47,53,56,70,54,52,68,30,31,32,46])).
% 116.92/118.11 cnf(202423,plain,
% 116.92/118.11 (~P3(f16(f5(a1)))),
% 116.92/118.11 inference(scs_inference,[],[202415,200918])).
% 116.92/118.11 cnf(202435,plain,
% 116.92/118.11 (P10(f2(f6(f10(f5(a1)))))),
% 116.92/118.11 inference(scs_inference,[],[202423,202413,202417,202397,202401,202320,10,189143,2845,32,29,17,30,31,189042])).
% 116.92/118.11 cnf(202438,plain,
% 116.92/118.11 (~P11(f2(f6(f10(f5(a1)))))),
% 116.92/118.11 inference(scs_inference,[],[202423,202413,202417,202397,202401,202320,10,189143,2845,189088,32,29,17,30,31,189042,40,39])).
% 116.92/118.11 cnf(202449,plain,
% 116.92/118.11 (~P11(f19(f10(f5(a1))))),
% 116.92/118.11 inference(scs_inference,[],[202435,202438,202344,202409,32,29,30,31])).
% 116.92/118.11 cnf(202454,plain,
% 116.92/118.11 ($false),
% 116.92/118.11 inference(scs_inference,[],[202449,189028,202417,32]),
% 116.92/118.11 ['proof']).
% 117.10/118.26 % SZS output end Proof
% 117.10/118.26 % Total time :115.910000s
%------------------------------------------------------------------------------