%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : HWV008-1.002 : TPTP v8.2.0. Bugfixed v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n027.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 116.39s 116.41s
% Output : CNFRefutation 116.58s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.13 % Problem : HWV008-1.002 : TPTP v8.2.0. Bugfixed v2.2.0.
% 0.12/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.12/0.34 % Computer : n027.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Fri Jun 21 00:37:09 EDT 2024
% 0.12/0.35 % CPUTime :
% 0.56/0.60 start to proof:theBenchmark
% 116.39/116.39 %-------------------------------------------
% 116.39/116.39 % File :CSE---1.7
% 116.39/116.39 % Problem :theBenchmark
% 116.39/116.39 % Transform :cnf
% 116.39/116.39 % Format :tptp:raw
% 116.39/116.39 % Command :java -jar mcs_scs.jar %d %s
% 116.39/116.39
% 116.39/116.39 % Result :Theorem 115.720000s
% 116.39/116.39 % Output :CNFRefutation 115.720000s
% 116.39/116.39 %-------------------------------------------
% 116.39/116.40 %--------------------------------------------------------------------------
% 116.39/116.40 % File : HWV008-1.002 : TPTP v8.2.0. Bugfixed v2.2.0.
% 116.39/116.40 % Domain : Hardware Verification
% 116.39/116.40 % Problem : 2 bit ripple carry adder
% 116.39/116.40 % Version : [Gei96] axioms.
% 116.39/116.40 % English :
% 116.39/116.40
% 116.39/116.40 % Refs : [Gei96] Geisler (1996), Email to G. Sutcliffe
% 116.39/116.40 % Source : [Gei96]
% 116.39/116.40 % Names :
% 116.39/116.40
% 116.39/116.40 % Status : Unsatisfiable
% 116.39/116.40 % Rating : 0.08 v8.2.0, 0.14 v8.1.0, 0.00 v7.5.0, 0.17 v7.4.0, 0.00 v7.0.0, 0.25 v6.3.0, 0.29 v6.2.0, 0.11 v6.1.0, 0.00 v5.0.0, 0.14 v4.1.0, 0.12 v4.0.1, 0.20 v4.0.0, 0.14 v3.4.0, 0.25 v3.3.0, 0.00 v3.1.0, 0.17 v2.7.0, 0.12 v2.6.0, 0.00 v2.2.1
% 116.39/116.40 % Syntax : Number of clauses : 68 ( 14 unt; 3 nHn; 68 RR)
% 116.39/116.40 % Number of literals : 158 ( 0 equ; 93 neg)
% 116.39/116.40 % Maximal clause size : 5 ( 2 avg)
% 116.39/116.40 % Maximal term depth : 4 ( 1 avg)
% 116.39/116.40 % Number of predicates : 5 ( 5 usr; 0 prp; 2-2 aty)
% 116.39/116.40 % Number of functors : 27 ( 27 usr; 17 con; 0-2 aty)
% 116.39/116.40 % Number of variables : 63 ( 3 sgn)
% 116.39/116.40 % SPC : CNF_UNS_RFO_NEQ_NHN
% 116.39/116.40
% 116.39/116.40 % Comments :
% 116.39/116.40 % Bugfixes : v2.2.0 - Missing conjecture clauses added.
% 116.39/116.40 %--------------------------------------------------------------------------
% 116.39/116.40 %----Include basic diagnosis axioms
% 116.39/116.41 include('Axioms/HWV001-0.ax').
% 116.39/116.41 %----Include model of halfadder
% 116.39/116.41 include('Axioms/HWV001-1.ax').
% 116.39/116.41 %----Include model of fulladder
% 116.39/116.41 include('Axioms/HWV001-2.ax').
% 116.39/116.41 %--------------------------------------------------------------------------
% 116.39/116.41 %----Composition of 2-bit adder
% 116.39/116.41 cnf(nbit_adder_fulladder1,axiom,
% 116.39/116.41 ( ~ type(X,nbit_adder(n2))
% 116.39/116.41 | type(f(n1,X),fulladder) ) ).
% 116.39/116.41
% 116.39/116.41 cnf(nbit_adder_fulladder2,axiom,
% 116.39/116.41 ( ~ type(X,nbit_adder(n2))
% 116.39/116.41 | type(f(n2,X),fulladder) ) ).
% 116.39/116.41
% 116.39/116.41 %----Connections of 2-bit adder
% 116.39/116.41 cnf(nbit_adder_connection_out1_out1f1,axiom,
% 116.39/116.41 ( ~ type(X,nbit_adder(n2))
% 116.39/116.41 | connection(out(n1,X),out(n1,f(n1,X))) ) ).
% 116.39/116.41
% 116.39/116.41 cnf(nbit_adder_connection_out2_out1f2,axiom,
% 116.39/116.41 ( ~ type(X,nbit_adder(n2))
% 116.39/116.41 | connection(out(n2,X),out(n1,f(n2,X))) ) ).
% 116.39/116.41
% 116.39/116.41 cnf(nbit_adder_connection_outc_outcf1,axiom,
% 116.39/116.41 ( ~ type(X,nbit_adder(n2))
% 116.39/116.41 | connection(out(c,X),out(c,f(n2,X))) ) ).
% 116.39/116.41
% 116.39/116.41 cnf(nbit_adder_connection_ina1_in1f1,axiom,
% 116.39/116.41 ( ~ type(X,nbit_adder(n2))
% 116.39/116.41 | connection(in(a1,X),in(n1,f(n1,X))) ) ).
% 116.39/116.41
% 116.39/116.41 cnf(nbit_adder_connection_inb1_in2f1,axiom,
% 116.39/116.41 ( ~ type(X,nbit_adder(n2))
% 116.39/116.41 | connection(in(b1,X),in(n2,f(n1,X))) ) ).
% 116.39/116.41
% 116.39/116.41 cnf(nbit_adder_connection_ina2_in1f2,axiom,
% 116.39/116.41 ( ~ type(X,nbit_adder(n2))
% 116.39/116.41 | connection(in(a2,X),in(n1,f(n2,X))) ) ).
% 116.39/116.41
% 116.39/116.41 cnf(nbit_adder_connection_inb2_in2f2,axiom,
% 116.39/116.41 ( ~ type(X,nbit_adder(n2))
% 116.39/116.41 | connection(in(b2,X),in(n2,f(n2,X))) ) ).
% 116.39/116.41
% 116.39/116.41 cnf(nbit_adder_connection_inc_incf1,axiom,
% 116.39/116.41 ( ~ type(X,nbit_adder(n2))
% 116.39/116.41 | connection(out(c,f(n1,X)),in(c,f(n2,X))) ) ).
% 116.39/116.41
% 116.39/116.41 cnf(nbit_adder_connection_inc_incf2,axiom,
% 116.39/116.41 ( ~ type(X,nbit_adder(n2))
% 116.39/116.41 | connection(in(c,X),in(c,f(n1,X))) ) ).
% 116.39/116.41
% 116.39/116.41 %----Observations
% 116.39/116.41 cnf(a_isa_2bit_adder,hypothesis,
% 116.39/116.41 type(a,nbit_adder(n2)) ).
% 116.39/116.41
% 116.39/116.41 cnf(ina1_0,hypothesis,
% 116.39/116.41 value(in(a1,a),n0) ).
% 116.39/116.41
% 116.39/116.41 cnf(ina2_0,hypothesis,
% 116.39/116.41 value(in(a2,a),n0) ).
% 116.39/116.41
% 116.39/116.41 cnf(inb1_0,hypothesis,
% 116.39/116.41 value(in(b1,a),n0) ).
% 116.39/116.41
% 116.39/116.41 cnf(inb2_0,hypothesis,
% 116.39/116.41 value(in(b2,a),n0) ).
% 116.39/116.41
% 116.39/116.41 cnf(inc_0,hypothesis,
% 116.39/116.41 value(in(c,a),n0) ).
% 116.39/116.41
% 116.39/116.41 cnf(out1_0,hypothesis,
% 116.39/116.41 value(out(n1,a),n0) ).
% 116.39/116.41
% 116.39/116.41 cnf(out2_0,hypothesis,
% 116.39/116.41 value(out(n2,a),n0) ).
% 116.39/116.41
% 116.39/116.41 cnf(outc_1,hypothesis,
% 116.39/116.41 value(out(c,a),n1) ).
% 116.39/116.41
% 116.39/116.41 %----Minimal diagnosis
% 116.39/116.41 cnf(diagnosis_or1f2a,negated_conjecture,
% 116.39/116.41 ~ mode(or1(f(n2,a)),abnormal) ).
% 116.39/116.41
% 116.39/116.41 cnf(diagnosis_and2h2f2a,negated_conjecture,
% 116.39/116.41 ~ mode(and2(h1(f(n2,a))),abnormal) ).
% 116.39/116.41
% 116.39/116.41 cnf(diagnosis_and2h1f2a,negated_conjecture,
% 116.39/116.41 ~ mode(and2(h2(f(n2,a))),abnormal) ).
% 116.39/116.41
% 116.39/116.41 %--------------------------------------------------------------------------
% 116.39/116.41 %-------------------------------------------
% 116.39/116.41 % Proof found
% 116.39/116.41 % SZS status Theorem for theBenchmark
% 116.39/116.41 % SZS output start Proof
% 116.39/116.41 %ClaNum:68(EqnAxiom:0)
% 116.39/116.41 %VarNum:182(SingletonVarNum:63)
% 116.39/116.41 %MaxLitNum:5
% 116.39/116.41 %MaxfuncDepth:3
% 116.39/116.41 %SharedTerms:46
% 116.39/116.41 %goalClause: 12 13 14
% 116.39/116.41 %singleGoalClaCount:3
% 116.39/116.41 [10]~P2(a18,a19)
% 116.39/116.41 [11]~P2(a19,a18)
% 116.39/116.41 [1]P1(a1,f20(a2))
% 116.39/116.41 [2]P5(f12(a3,a1),a18)
% 116.39/116.41 [3]P5(f12(a4,a1),a18)
% 116.39/116.41 [4]P5(f12(a5,a1),a18)
% 116.39/116.41 [5]P5(f12(a6,a1),a18)
% 116.39/116.41 [6]P5(f12(a11,a1),a18)
% 116.39/116.41 [7]P5(f21(a19,a1),a18)
% 116.39/116.41 [8]P5(f21(a2,a1),a18)
% 116.39/116.41 [9]P5(f21(a3,a1),a19)
% 116.39/116.41 [12]~P4(f22(f13(a2,a1)),a7)
% 116.39/116.41 [13]~P4(f8(f14(f13(a2,a1))),a7)
% 116.39/116.41 [14]~P4(f8(f16(f13(a2,a1))),a7)
% 116.39/116.41 [22]~P4(x221,a7)+~P4(x221,a26)
% 116.39/116.41 [15]~P1(x151,a17)+P1(f9(x151),a10)
% 116.39/116.41 [16]~P1(x161,a17)+P1(f8(x161),a10)
% 116.39/116.42 [17]~P1(x171,a17)+P1(f23(x171),a24)
% 116.39/116.42 [18]~P1(x181,a17)+P1(f22(x181),a25)
% 116.39/116.42 [19]~P1(x191,a15)+P1(f22(x191),a25)
% 116.39/116.42 [20]~P1(x201,a15)+P1(f14(x201),a17)
% 116.39/116.42 [21]~P1(x211,a15)+P1(f16(x211),a17)
% 116.39/116.42 [27]~P1(x271,f20(a2))+P1(f13(a19,x271),a15)
% 116.39/116.42 [28]~P1(x281,f20(a2))+P1(f13(a2,x281),a15)
% 116.39/116.42 [29]~P1(x291,a17)+P3(f12(a19,x291),f12(a19,f8(x291)))
% 116.39/116.42 [30]~P1(x301,a17)+P3(f12(a19,x301),f12(a19,f22(x301)))
% 116.39/116.42 [31]~P1(x311,a15)+P3(f12(a19,x311),f12(a19,f16(x311)))
% 116.39/116.42 [32]~P1(x321,a15)+P3(f12(a2,x321),f12(a19,f14(x321)))
% 116.39/116.42 [33]~P1(x331,a17)+P3(f12(a2,x331),f12(a2,f8(x331)))
% 116.39/116.42 [34]~P1(x341,a17)+P3(f12(a2,x341),f12(a2,f22(x341)))
% 116.39/116.42 [35]~P1(x351,a15)+P3(f12(a3,x351),f12(a2,f14(x351)))
% 116.39/116.42 [36]~P1(x361,a17)+P3(f21(a27,x361),f21(a19,f9(x361)))
% 116.39/116.42 [37]~P1(x371,a15)+P3(f21(a27,x371),f21(a27,f16(x371)))
% 116.39/116.42 [38]~P1(x381,a17)+P3(f21(a3,x381),f21(a19,f8(x381)))
% 116.39/116.42 [39]~P1(x391,a15)+P3(f21(a3,x391),f21(a19,f22(x391)))
% 116.39/116.42 [40]~P1(x401,a17)+P3(f21(a19,f8(x401)),f12(a19,f23(x401)))
% 116.39/116.42 [41]~P1(x411,a17)+P3(f21(a19,f23(x411)),f12(a2,f9(x411)))
% 116.39/116.42 [42]~P1(x421,a17)+P3(f21(a19,f22(x421)),f12(a19,f9(x421)))
% 116.39/116.42 [43]~P1(x431,a15)+P3(f21(a27,f14(x431)),f12(a2,f16(x431)))
% 116.39/116.42 [44]~P1(x441,a15)+P3(f21(a3,f14(x441)),f12(a2,f22(x441)))
% 116.39/116.42 [45]~P1(x451,a15)+P3(f21(a3,f16(x451)),f12(a19,f22(x451)))
% 116.39/116.42 [54]~P1(x541,f20(a2))+P3(f12(a3,x541),f12(a3,f13(a19,x541)))
% 116.39/116.42 [55]~P1(x551,f20(a2))+P3(f12(a4,x551),f12(a19,f13(a19,x551)))
% 116.39/116.42 [56]~P1(x561,f20(a2))+P3(f12(a5,x561),f12(a2,f13(a19,x561)))
% 116.39/116.42 [57]~P1(x571,f20(a2))+P3(f12(a6,x571),f12(a19,f13(a2,x571)))
% 116.39/116.42 [58]~P1(x581,f20(a2))+P3(f12(a11,x581),f12(a2,f13(a2,x581)))
% 116.39/116.42 [59]~P1(x591,f20(a2))+P3(f21(a19,x591),f21(a19,f13(a19,x591)))
% 116.39/116.42 [60]~P1(x601,f20(a2))+P3(f21(a2,x601),f21(a19,f13(a2,x601)))
% 116.39/116.42 [61]~P1(x611,f20(a2))+P3(f21(a3,x611),f21(a3,f13(a2,x611)))
% 116.39/116.42 [66]~P1(x661,f20(a2))+P3(f21(a3,f13(a19,x661)),f12(a3,f13(a2,x661)))
% 116.39/116.42 [23]~P1(x231,x232)+P4(x231,a7)+P4(x231,a26)
% 116.39/116.42 [24]~P5(x243,x242)+P5(x241,x242)+~P3(x243,x241)
% 116.39/116.42 [25]~P5(x253,x252)+P5(x251,x252)+~P3(x251,x253)
% 116.39/116.42 [26]~P5(x263,x261)+P2(x261,x262)+~P5(x263,x262)
% 116.39/116.42 [46]~P4(x461,a26)+~P1(x461,a25)+~P5(f21(a19,x461),a18)+P5(f12(a19,x461),a18)
% 116.39/116.42 [47]~P4(x471,a26)+~P1(x471,a24)+~P5(f21(a19,x471),a19)+P5(f12(a19,x471),a18)
% 116.39/116.42 [48]~P4(x481,a26)+~P1(x481,a10)+~P5(f21(a19,x481),a19)+P5(f12(a19,x481),a19)
% 116.39/116.42 [49]~P4(x491,a26)+~P1(x491,a24)+~P5(f21(a19,x491),a18)+P5(f12(a19,x491),a19)
% 116.39/116.42 [50]~P4(x501,a26)+~P1(x501,a25)+~P5(f21(a19,x501),a18)+P5(f12(a2,x501),a18)
% 116.39/116.42 [51]~P4(x511,a26)+~P1(x511,a10)+~P5(f21(a19,x511),a19)+P5(f12(a2,x511),a19)
% 116.39/116.42 [52]~P4(x521,a26)+~P1(x521,a24)+~P5(f12(a19,x521),a19)+P5(f21(a19,x521),a18)
% 116.39/116.42 [53]~P4(x531,a26)+~P1(x531,a24)+~P5(f12(a19,x531),a18)+P5(f21(a19,x531),a19)
% 116.39/116.42 [62]~P4(x621,a26)+~P1(x621,a10)+~P5(f12(x622,x621),a18)+P5(f21(a19,x621),a18)
% 116.39/116.42 [63]~P4(x631,a26)+~P1(x631,a25)+~P5(f12(x632,x631),a19)+P5(f21(a19,x631),a19)
% 116.39/116.42 [64]~P4(x641,a26)+~P1(x641,a10)+P5(f12(a2,x641),a18)+~P5(f21(a19,x641),a18)+P5(f12(a19,x641),a18)
% 116.39/116.42 [65]~P4(x651,a26)+~P1(x651,a25)+P5(f12(a2,x651),a19)+~P5(f21(a19,x651),a19)+P5(f12(a19,x651),a19)
% 116.39/116.42 [67]~P4(x671,a26)+~P1(x671,a25)+~P5(f12(a19,x671),a18)+~P5(f12(a2,x671),a18)+P5(f21(a19,x671),a18)
% 116.39/116.42 [68]~P4(x681,a26)+~P1(x681,a10)+~P5(f12(a19,x681),a19)+~P5(f12(a2,x681),a19)+P5(f21(a19,x681),a19)
% 116.39/116.42 %EqnAxiom
% 116.39/116.42
% 116.39/116.42 %-------------------------------------------
% 116.51/116.49 cnf(71,plain,
% 116.51/116.49 (~P1(f22(f13(a2,a1)),x711)+P4(f22(f13(a2,a1)),a26)),
% 116.51/116.49 inference(scs_inference,[],[12,7,26,23])).
% 116.51/116.49 cnf(76,plain,
% 116.51/116.49 (~P1(f8(f16(f13(a2,a1))),x761)+P4(f8(f16(f13(a2,a1))),a26)),
% 116.51/116.49 inference(scs_inference,[],[14,7,26,23])).
% 116.51/116.49 cnf(81,plain,
% 116.51/116.49 (~P1(f8(f14(f13(a2,a1))),x811)+P4(f8(f14(f13(a2,a1))),a26)),
% 116.51/116.49 inference(scs_inference,[],[13,7,26,23])).
% 116.51/116.49 cnf(214,plain,
% 116.51/116.49 (~P1(x2141,a15)+P1(f9(f14(x2141)),a10)),
% 116.51/116.49 inference(scs_inference,[],[15,20])).
% 116.51/116.49 cnf(260,plain,
% 116.51/116.49 (~P1(x2601,a15)+P1(f8(f16(x2601)),a10)),
% 116.51/116.49 inference(scs_inference,[],[16,21])).
% 116.51/116.49 cnf(306,plain,
% 116.51/116.49 (~P1(x3061,a15)+P1(f23(f14(x3061)),a24)),
% 116.51/116.49 inference(scs_inference,[],[17,20])).
% 116.51/116.49 cnf(352,plain,
% 116.51/116.49 (~P1(x3521,a15)+P1(f22(f16(x3521)),a25)),
% 116.51/116.49 inference(scs_inference,[],[18,21])).
% 116.51/116.49 cnf(490,plain,
% 116.51/116.49 (P4(f8(f16(f13(a2,a1))),a26)+~P1(f13(a2,a1),a15)),
% 116.51/116.49 inference(scs_inference,[],[260,76])).
% 116.51/116.49 cnf(628,plain,
% 116.51/116.49 (P3(f12(a19,f13(a2,a1)),f12(a19,f16(f13(a2,a1))))),
% 116.51/116.49 inference(scs_inference,[],[1,28,31])).
% 116.51/116.49 cnf(682,plain,
% 116.51/116.49 (~P1(x6821,a15)+P3(f12(a19,f14(x6821)),f12(a19,f8(f14(x6821))))),
% 116.51/116.49 inference(scs_inference,[],[29,20])).
% 116.51/116.49 cnf(728,plain,
% 116.51/116.49 (~P1(x7281,a15)+P3(f12(a19,f16(x7281)),f12(a19,f22(f16(x7281))))),
% 116.51/116.49 inference(scs_inference,[],[30,21])).
% 116.51/116.49 cnf(774,plain,
% 116.51/116.49 (P3(f12(a2,f13(a19,a1)),f12(a19,f14(f13(a19,a1))))),
% 116.51/116.49 inference(scs_inference,[],[1,32,27])).
% 116.51/116.49 cnf(777,plain,
% 116.51/116.49 (~P5(f12(a2,f13(a19,a1)),x7771)+P5(f12(a19,f14(f13(a19,a1))),x7771)),
% 116.51/116.49 inference(scs_inference,[],[774,7,26,24])).
% 116.51/116.49 cnf(828,plain,
% 116.51/116.49 (~P1(x8281,a15)+P3(f12(a2,f14(x8281)),f12(a2,f8(f14(x8281))))),
% 116.51/116.49 inference(scs_inference,[],[33,20])).
% 116.51/116.49 cnf(874,plain,
% 116.51/116.49 (~P1(x8741,a15)+P3(f12(a2,f16(x8741)),f12(a2,f22(f16(x8741))))),
% 116.51/116.49 inference(scs_inference,[],[34,21])).
% 116.51/116.49 cnf(974,plain,
% 116.51/116.49 (~P1(x9741,a15)+P3(f21(a27,f14(x9741)),f21(a19,f9(f14(x9741))))),
% 116.51/116.49 inference(scs_inference,[],[36,20])).
% 116.51/116.49 cnf(1074,plain,
% 116.51/116.49 (~P1(x10741,a15)+P3(f21(a3,f16(x10741)),f21(a19,f8(f16(x10741))))),
% 116.51/116.49 inference(scs_inference,[],[38,21])).
% 116.51/116.49 cnf(1120,plain,
% 116.51/116.49 (P3(f21(a3,f13(a2,a1)),f21(a19,f22(f13(a2,a1))))),
% 116.51/116.49 inference(scs_inference,[],[1,39,28])).
% 116.51/116.49 cnf(1130,plain,
% 116.51/116.49 (~P5(f21(a19,f22(f13(a2,a1))),x11301)+P5(f21(a3,f13(a2,a1)),x11301)),
% 116.51/116.49 inference(scs_inference,[],[1120,7,26,25])).
% 116.51/116.49 cnf(1174,plain,
% 116.51/116.49 (~P1(x11741,a15)+P3(f21(a19,f8(f14(x11741))),f12(a19,f23(f14(x11741))))),
% 116.51/116.49 inference(scs_inference,[],[40,20])).
% 116.51/116.49 cnf(1220,plain,
% 116.51/116.50 (~P1(x12201,a15)+P3(f21(a19,f23(f16(x12201))),f12(a2,f9(f16(x12201))))),
% 116.51/116.50 inference(scs_inference,[],[41,21])).
% 116.51/116.50 cnf(1266,plain,
% 116.51/116.50 (~P1(x12661,a15)+P3(f21(a19,f22(f14(x12661))),f12(a19,f9(f14(x12661))))),
% 116.51/116.50 inference(scs_inference,[],[42,20])).
% 116.51/116.50 cnf(1358,plain,
% 116.51/116.50 (P3(f21(a3,f14(f13(a2,a1))),f12(a2,f22(f13(a2,a1))))),
% 116.51/116.50 inference(scs_inference,[],[1,44,28])).
% 116.51/116.50 cnf(1496,plain,
% 116.51/116.50 (P4(f8(f16(f13(a2,a1))),a26)),
% 116.51/116.50 inference(scs_inference,[],[1,490,28])).
% 116.51/116.50 cnf(1588,plain,
% 116.51/116.50 (P5(f12(a19,f13(a19,a1)),a18)),
% 116.51/116.50 inference(scs_inference,[],[1,3,55,24])).
% 116.51/116.50 cnf(1634,plain,
% 116.51/116.50 (P5(f12(a2,f13(a19,a1)),a18)),
% 116.51/116.50 inference(scs_inference,[],[1,4,56,24])).
% 116.51/116.50 cnf(1635,plain,
% 116.51/116.50 (P5(f12(a19,f14(f13(a19,a1))),a18)),
% 116.51/116.50 inference(scs_inference,[],[1634,777])).
% 116.51/116.50 cnf(1682,plain,
% 116.51/116.50 (P5(f12(a19,f13(a2,a1)),a18)),
% 116.51/116.50 inference(scs_inference,[],[1,5,57,24])).
% 116.51/116.50 cnf(1683,plain,
% 116.51/116.50 (P5(f12(a19,f16(f13(a2,a1))),a18)),
% 116.51/116.50 inference(scs_inference,[],[628,1682,24])).
% 116.51/116.50 cnf(1730,plain,
% 116.51/116.50 (P5(f12(a2,f13(a2,a1)),a18)),
% 116.51/116.50 inference(scs_inference,[],[1,6,58,24])).
% 116.51/116.50 cnf(1776,plain,
% 116.51/116.50 (P5(f21(a19,f13(a19,a1)),a18)),
% 116.51/116.50 inference(scs_inference,[],[1,7,59,24])).
% 116.51/116.50 cnf(1868,plain,
% 116.51/116.50 (P5(f21(a3,f13(a2,a1)),a19)),
% 116.51/116.50 inference(scs_inference,[],[1,9,61,24])).
% 116.51/116.50 cnf(1869,plain,
% 116.51/116.50 (P5(f21(a19,f22(f13(a2,a1))),a19)),
% 116.51/116.50 inference(scs_inference,[],[1120,1868,24])).
% 116.51/116.50 cnf(1916,plain,
% 116.51/116.50 (P5(f12(a19,f8(f14(f13(a19,a1)))),a18)+~P1(f13(a19,a1),a15)),
% 116.51/116.50 inference(scs_inference,[],[1635,682,24])).
% 116.51/116.50 cnf(1962,plain,
% 116.51/116.50 (P5(f12(a19,f22(f16(f13(a2,a1)))),a18)+~P1(f13(a2,a1),a15)),
% 116.51/116.50 inference(scs_inference,[],[1683,728,24])).
% 116.51/116.50 cnf(2146,plain,
% 116.51/116.50 (~P5(f21(a19,f8(f16(x21461))),x21462)+P5(f21(a3,f16(x21461)),x21462)+~P1(x21461,a15)),
% 116.51/116.50 inference(scs_inference,[],[1074,25])).
% 116.51/116.50 cnf(2192,plain,
% 116.51/116.50 (P4(f8(f14(f13(a2,a1))),a26)+~P1(f14(f13(a2,a1)),a17)),
% 116.51/116.50 inference(scs_inference,[],[81,16])).
% 116.51/116.50 cnf(2238,plain,
% 116.52/116.50 (P4(f8(f14(f13(a2,a1))),a26)+~P1(f13(a2,a1),a15)),
% 116.52/116.50 inference(scs_inference,[],[2192,20])).
% 116.52/116.50 cnf(2284,plain,
% 116.52/116.50 (P4(f8(f14(f13(a2,a1))),a26)),
% 116.52/116.50 inference(scs_inference,[],[1,2238,28])).
% 116.52/116.50 cnf(4152,plain,
% 116.52/116.50 (~P5(f21(a3,f16(x41521)),a18)+~P5(f21(a19,f8(f16(x41521))),a19)+~P1(x41521,a15)),
% 116.52/116.50 inference(scs_inference,[],[11,2146,26])).
% 116.52/116.50 cnf(6201,plain,
% 116.52/116.50 (~P1(x62011,a15)+P1(f8(f14(x62011)),a10)),
% 116.52/116.50 inference(scs_inference,[],[16,20])).
% 116.52/116.50 cnf(7159,plain,
% 116.52/116.50 (~P1(x71591,a15)+P1(f22(f14(x71591)),a25)),
% 116.52/116.50 inference(scs_inference,[],[18,20])).
% 116.52/116.50 cnf(74726,plain,
% 116.52/116.50 (P1(f13(a19,a1),a15)),
% 116.52/116.50 inference(scs_inference,[],[1,27])).
% 116.52/116.50 cnf(74728,plain,
% 116.52/116.50 (P1(f13(a2,a1),a15)),
% 116.52/116.50 inference(scs_inference,[],[1,27,28])).
% 116.52/116.50 cnf(74732,plain,
% 116.52/116.50 (P3(f12(a2,f13(a2,a1)),f12(a19,f14(f13(a2,a1))))),
% 116.52/116.50 inference(scs_inference,[],[1,27,28,31,32])).
% 116.52/116.50 cnf(74744,plain,
% 116.52/116.50 (P3(f21(a3,f16(f13(a2,a1))),f12(a19,f22(f13(a2,a1))))),
% 116.52/116.50 inference(scs_inference,[],[1,27,28,31,32,35,37,39,43,44,45])).
% 116.52/116.50 cnf(74765,plain,
% 116.52/116.50 (P5(f12(a19,f22(f16(f13(a2,a1)))),a18)),
% 116.52/116.50 inference(scs_inference,[],[1,27,28,31,32,35,37,39,43,44,45,54,55,56,57,58,59,60,61,66,1916,1962])).
% 116.52/116.50 cnf(74766,plain,
% 116.52/116.50 (P5(f12(a19,f16(f13(a19,a1))),a18)),
% 116.52/116.50 inference(scs_inference,[],[1,1588,27,28,31,32,35,37,39,43,44,45,54,55,56,57,58,59,60,61,66,1916,1962,24])).
% 116.52/116.50 cnf(74768,plain,
% 116.52/116.50 (~P5(f21(a2,a1),a19)),
% 116.52/116.50 inference(scs_inference,[],[11,1,8,1588,27,28,31,32,35,37,39,43,44,45,54,55,56,57,58,59,60,61,66,1916,1962,24,26])).
% 116.52/116.50 cnf(74770,plain,
% 116.52/116.50 (P1(f22(f13(a2,a1)),a25)),
% 116.52/116.50 inference(scs_inference,[],[11,1,8,1588,27,28,31,32,35,37,39,43,44,45,54,55,56,57,58,59,60,61,66,1916,1962,24,26,19])).
% 116.52/116.50 cnf(74772,plain,
% 116.52/116.50 (P1(f14(f13(a19,a1)),a17)),
% 116.52/116.50 inference(scs_inference,[],[11,1,8,1588,27,28,31,32,35,37,39,43,44,45,54,55,56,57,58,59,60,61,66,1916,1962,24,26,19,20])).
% 116.52/116.50 cnf(74774,plain,
% 116.52/116.50 (P1(f16(f13(a19,a1)),a17)),
% 116.52/116.50 inference(scs_inference,[],[11,1,8,1588,27,28,31,32,35,37,39,43,44,45,54,55,56,57,58,59,60,61,66,1916,1962,24,26,19,20,21])).
% 116.52/116.50 cnf(74797,plain,
% 116.52/116.50 (P4(f22(f13(a2,a1)),a26)),
% 116.52/116.50 inference(scs_inference,[],[74770,71])).
% 116.52/116.50 cnf(74799,plain,
% 116.52/116.50 (P1(f8(f14(f13(a2,a1))),a10)),
% 116.52/116.50 inference(scs_inference,[],[74728,6201])).
% 116.52/116.50 cnf(74803,plain,
% 116.52/116.50 (P1(f16(f13(a2,a1)),a17)),
% 116.52/116.50 inference(scs_inference,[],[74728,6201,7159,21])).
% 116.52/116.50 cnf(74811,plain,
% 116.52/116.50 (P1(f14(f13(a2,a1)),a17)),
% 116.52/116.50 inference(scs_inference,[],[74728,6201,7159,21,214,306,352,20])).
% 116.52/116.50 cnf(74813,plain,
% 116.52/116.50 (P1(f8(f16(f13(a2,a1))),a10)),
% 116.52/116.50 inference(scs_inference,[],[74728,6201,7159,21,214,306,352,20,260])).
% 116.52/116.50 cnf(74819,plain,
% 116.52/116.50 (~P5(f21(a3,a1),a18)),
% 116.52/116.50 inference(scs_inference,[],[74728,74768,10,9,6201,7159,21,214,306,352,20,260,25,24,26])).
% 116.52/116.50 cnf(74833,plain,
% 116.52/116.50 (~P5(f12(a19,f16(f13(a19,a1))),a19)),
% 116.52/116.50 inference(scs_inference,[],[74819,74766,11,24,25,26])).
% 116.52/116.50 cnf(74865,plain,
% 116.52/116.50 (~P5(f12(a11,a1),a19)),
% 116.52/116.50 inference(scs_inference,[],[74770,74797,74768,11,74819,74766,6,9,1869,24,25,65,26])).
% 116.52/116.50 cnf(74892,plain,
% 116.52/116.50 (~P5(f12(a6,a1),a19)),
% 116.52/116.50 inference(scs_inference,[],[74865,11,74819,74766,9,5,24,25,26])).
% 116.52/116.50 cnf(74917,plain,
% 116.52/116.50 (~P5(f12(a3,a1),a19)),
% 116.52/116.50 inference(scs_inference,[],[74892,11,74819,74766,9,2,24,25,26])).
% 116.52/116.50 cnf(74943,plain,
% 116.52/116.50 (~P5(f12(a4,a1),a19)),
% 116.52/116.50 inference(scs_inference,[],[74917,11,74819,74766,9,3,24,25,26])).
% 116.52/116.50 cnf(74969,plain,
% 116.52/116.50 (~P5(f12(a5,a1),a19)),
% 116.52/116.50 inference(scs_inference,[],[74943,11,74819,74766,9,4,24,25,26])).
% 116.52/116.50 cnf(74994,plain,
% 116.52/116.50 (~P5(f12(a19,f13(a2,a1)),a19)),
% 116.52/116.50 inference(scs_inference,[],[74969,11,74819,74766,9,1682,24,25,26])).
% 116.52/116.50 cnf(75019,plain,
% 116.52/116.50 (~P5(f12(a19,f14(f13(a19,a1))),a19)),
% 116.52/116.50 inference(scs_inference,[],[74994,11,74819,74766,9,1635,24,25,26])).
% 116.52/116.50 cnf(75050,plain,
% 116.52/116.50 (~P5(f12(a19,f16(f13(a2,a1))),a19)),
% 116.52/116.50 inference(scs_inference,[],[75019,11,74819,74766,9,1683,24,25,26])).
% 116.52/116.50 cnf(75074,plain,
% 116.52/116.50 (~P5(f12(a19,f13(a19,a1)),a19)),
% 116.52/116.50 inference(scs_inference,[],[75050,11,74819,74766,9,1588,24,25,26])).
% 116.52/116.50 cnf(75103,plain,
% 116.52/116.50 (~P5(f12(a2,f13(a2,a1)),a19)),
% 116.52/116.50 inference(scs_inference,[],[75019,11,74819,74766,9,1730,24,25,26])).
% 116.52/116.50 cnf(75157,plain,
% 116.52/116.50 (~P5(f21(a19,f22(f13(a2,a1))),a18)),
% 116.52/116.50 inference(scs_inference,[],[75103,75074,10,74819,74766,9,1868,1776,24,25,26,49,1130])).
% 116.52/116.50 cnf(75173,plain,
% 116.52/116.50 (~P5(f12(a2,f22(f13(a2,a1))),a18)+~P5(f12(a19,f22(f13(a2,a1))),a18)),
% 116.52/116.50 inference(scs_inference,[],[74833,75157,74770,74797,8,9,24,25,67])).
% 116.52/116.50 cnf(79128,plain,
% 116.52/116.50 (P5(f12(a19,f14(f13(a2,a1))),a18)),
% 116.52/116.50 inference(scs_inference,[],[74732,1730,24])).
% 116.52/116.50 cnf(97245,plain,
% 116.52/116.50 (P3(f21(a3,f16(f13(a2,a1))),f21(a19,f8(f16(f13(a2,a1)))))),
% 116.52/116.50 inference(scs_inference,[],[74803,29,30,33,34,36,38])).
% 116.52/116.50 cnf(97247,plain,
% 116.52/116.50 (P3(f21(a19,f8(f16(f13(a2,a1)))),f12(a19,f23(f16(f13(a2,a1)))))),
% 116.52/116.50 inference(scs_inference,[],[74803,29,30,33,34,36,38,40])).
% 116.52/116.50 cnf(97259,plain,
% 116.52/116.50 (P5(f12(a19,f8(f16(f13(a2,a1)))),a18)),
% 116.52/116.50 inference(scs_inference,[],[74803,74728,74726,1683,29,30,33,34,36,38,40,41,42,728,828,1220,24])).
% 116.52/116.50 cnf(97260,plain,
% 116.52/116.50 (~P3(x972601,x972602)+P5(x972602,x972603)+~P5(x972601,x972603)),
% 116.52/116.50 inference(rename_variables,[],[24])).
% 116.52/116.50 cnf(97265,plain,
% 116.52/116.50 (P5(f21(a19,f8(f16(f13(a2,a1)))),a18)),
% 116.52/116.50 inference(scs_inference,[],[74765,74803,74813,11,74833,1496,74728,74726,1683,29,30,33,34,36,38,40,41,42,728,828,1220,24,25,26,62])).
% 116.52/116.50 cnf(97267,plain,
% 116.52/116.50 (P3(f12(a19,f14(f13(a2,a1))),f12(a19,f8(f14(f13(a2,a1)))))),
% 116.52/116.50 inference(scs_inference,[],[74765,74803,74813,11,74833,1496,74728,74726,1683,29,30,33,34,36,38,40,41,42,728,828,1220,24,25,26,62,682])).
% 116.52/116.50 cnf(97275,plain,
% 116.52/116.50 (P3(f21(a19,f8(f14(f13(a2,a1)))),f12(a19,f23(f14(f13(a2,a1)))))),
% 116.52/116.50 inference(scs_inference,[],[74765,74803,74813,11,74833,1496,74728,74726,1683,29,30,33,34,36,38,40,41,42,728,828,1220,24,25,26,62,682,874,974,1074,1174])).
% 116.52/116.50 cnf(97279,plain,
% 116.52/116.50 (~P5(f21(a3,f16(f13(a2,a1))),x972791)+P5(f12(a19,f22(f13(a2,a1))),x972791)),
% 116.52/116.50 inference(scs_inference,[],[74744,74765,74803,74813,11,74833,1496,74728,74726,1683,29,30,33,34,36,38,40,41,42,728,828,1220,24,25,26,62,682,874,974,1074,1174,1266,97260])).
% 116.52/116.50 cnf(97291,plain,
% 116.52/116.50 (P5(f12(a19,f8(f14(f13(a2,a1)))),a18)),
% 116.52/116.50 inference(scs_inference,[],[97267,79128,24])).
% 116.52/116.50 cnf(97295,plain,
% 116.52/116.50 (~P5(f21(a19,f8(f16(f13(a2,a1)))),a19)),
% 116.52/116.50 inference(scs_inference,[],[97265,97245,97267,79128,74728,24,25,4152])).
% 116.52/116.50 cnf(97297,plain,
% 116.52/116.50 (~P5(f12(a19,f8(f16(f13(a2,a1)))),a19)),
% 116.52/116.50 inference(scs_inference,[],[97265,97259,97245,97267,11,79128,74728,24,25,4152,26])).
% 116.52/116.50 cnf(97301,plain,
% 116.52/116.50 (P5(f21(a19,f8(f14(f13(a2,a1)))),a18)),
% 116.52/116.50 inference(scs_inference,[],[97265,97259,97245,97267,74799,11,79128,2284,1496,74728,24,25,4152,26,53,62])).
% 116.52/116.50 cnf(97303,plain,
% 116.52/116.50 (P5(f12(a19,f22(f13(a2,a1))),a18)),
% 116.52/116.50 inference(scs_inference,[],[97265,97259,97245,97267,74799,11,79128,2284,1496,74728,24,25,4152,26,53,62,97279])).
% 116.52/116.50 cnf(97305,plain,
% 116.52/116.50 (~P5(f12(a2,f22(f13(a2,a1))),a18)),
% 116.52/116.50 inference(scs_inference,[],[97265,97259,97245,97267,74799,11,79128,2284,1496,74728,24,25,4152,26,53,62,97279,75173])).
% 116.52/116.50 cnf(97310,plain,
% 116.52/116.50 (~P5(f21(a3,f14(f13(a2,a1))),a18)),
% 116.52/116.50 inference(scs_inference,[],[97305,1358,24])).
% 116.52/116.50 cnf(97320,plain,
% 116.52/116.50 (P5(f12(a2,f22(f13(a2,a1))),a19)),
% 116.52/116.50 inference(scs_inference,[],[97303,97305,1358,97295,97247,97259,11,74770,74797,1496,1869,24,25,26,53,48,65])).
% 116.52/116.50 cnf(97333,plain,
% 116.52/116.50 (~P5(f21(a19,f8(f14(f13(a2,a1)))),a19)),
% 116.52/116.50 inference(scs_inference,[],[97320,97301,97275,1358,11,24,25,26])).
% 116.52/116.50 cnf(97361,plain,
% 116.52/116.50 (P3(f12(a19,f14(f13(a2,a1))),f12(a19,f22(f14(f13(a2,a1)))))),
% 116.52/116.50 inference(scs_inference,[],[97333,97291,97297,97303,97265,74811,74772,74774,75157,74797,2284,1496,74726,53,49,62,29,34,974,1266,42,41,30])).
% 116.52/116.50 cnf(97369,plain,
% 116.52/116.50 (P3(f21(a3,f14(f13(a2,a1))),f21(a19,f8(f14(f13(a2,a1)))))),
% 116.52/116.50 inference(scs_inference,[],[97333,97291,97297,97303,97265,74811,74772,74774,75157,74797,2284,1496,74726,53,49,62,29,34,974,1266,42,41,30,36,828,1174,38])).
% 116.52/116.50 cnf(97385,plain,
% 116.52/116.50 ($false),
% 116.52/116.50 inference(scs_inference,[],[97310,97361,97369,97301,79128,24,25]),
% 116.52/116.50 ['proof']).
% 116.58/116.58 % SZS output end Proof
% 116.58/116.58 % Total time :115.720000s
%------------------------------------------------------------------------------