%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : SWV399+1 : TPTP v8.2.0. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n022.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 16:47:06 EDT 2024
% Result : Theorem 16.22s 16.31s
% Output : CNFRefutation 16.27s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.09/0.10 % Problem : SWV399+1 : TPTP v8.2.0. Released v3.3.0.
% 0.09/0.10 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.10/0.31 % Computer : n022.cluster.edu
% 0.10/0.31 % Model : x86_64 x86_64
% 0.10/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.31 % Memory : 8042.1875MB
% 0.10/0.31 % OS : Linux 3.10.0-693.el7.x86_64
% 0.10/0.31 % CPULimit : 300
% 0.10/0.31 % WCLimit : 300
% 0.10/0.31 % DateTime : Thu Jun 20 19:04:53 EDT 2024
% 0.15/0.31 % CPUTime :
% 0.17/0.55 start to proof:theBenchmark
% 16.22/16.30 %-------------------------------------------
% 16.22/16.30 % File :CSE---1.7
% 16.22/16.30 % Problem :theBenchmark
% 16.22/16.30 % Transform :cnf
% 16.22/16.30 % Format :tptp:raw
% 16.22/16.30 % Command :java -jar mcs_scs.jar %d %s
% 16.22/16.30
% 16.22/16.30 % Result :Theorem 15.700000s
% 16.22/16.30 % Output :CNFRefutation 15.700000s
% 16.22/16.30 %-------------------------------------------
% 16.22/16.31 %------------------------------------------------------------------------------
% 16.22/16.31 % File : SWV399+1 : TPTP v8.2.0. Released v3.3.0.
% 16.22/16.31 % Domain : Software Verification
% 16.22/16.31 % Problem : Priority queue checker: tmp_not_check_03_1
% 16.22/16.31 % Version : [dNP05] axioms.
% 16.22/16.31 % English :
% 16.22/16.31
% 16.22/16.31 % Refs : [Pis06] Piskac (2006), Email to Geoff Sutcliffe
% 16.22/16.31 % : [dNP05] de Nivelle & Piskac (2005), Verification of an Off-Lin
% 16.22/16.31 % Source : [Pis06]
% 16.22/16.31 % Names : cpq_l035 [Pis06]
% 16.22/16.31
% 16.22/16.31 % Status : Theorem
% 16.22/16.31 % Rating : 0.17 v8.1.0, 0.14 v7.5.0, 0.12 v7.4.0, 0.17 v7.2.0, 0.14 v7.1.0, 0.13 v6.4.0, 0.19 v6.3.0, 0.12 v6.2.0, 0.16 v6.1.0, 0.10 v6.0.0, 0.09 v5.5.0, 0.07 v5.4.0, 0.11 v5.3.0, 0.19 v5.2.0, 0.10 v5.0.0, 0.12 v4.1.0, 0.17 v4.0.1, 0.13 v4.0.0, 0.12 v3.7.0, 0.10 v3.5.0, 0.11 v3.4.0, 0.21 v3.3.0
% 16.22/16.31 % Syntax : Number of formulae : 21 ( 9 unt; 0 def)
% 16.22/16.31 % Number of atoms : 44 ( 12 equ)
% 16.22/16.31 % Maximal formula atoms : 4 ( 2 avg)
% 16.22/16.31 % Number of connectives : 29 ( 6 ~; 3 |; 9 &)
% 16.22/16.31 % ( 3 <=>; 8 =>; 0 <=; 0 <~>)
% 16.22/16.31 % Maximal formula depth : 9 ( 5 avg)
% 16.22/16.31 % Maximal term depth : 4 ( 1 avg)
% 16.22/16.31 % Number of predicates : 6 ( 5 usr; 0 prp; 1-3 aty)
% 16.22/16.31 % Number of functors : 7 ( 7 usr; 2 con; 0-2 aty)
% 16.22/16.31 % Number of variables : 61 ( 57 !; 4 ?)
% 16.22/16.31 % SPC : FOF_THM_RFO_SEQ
% 16.22/16.31
% 16.22/16.31 % Comments :
% 16.22/16.31 %------------------------------------------------------------------------------
% 16.22/16.31 %----Include the axioms about priority queues and checked priority queues
% 16.22/16.31 include('Axioms/SWV007+0.ax').
% 16.22/16.31 include('Axioms/SWV007+2.ax').
% 16.22/16.31 %------------------------------------------------------------------------------
% 16.22/16.31 %----tmp_not_check_03_2 (cpq_l036.p, cpq_l037.p)
% 16.22/16.31 fof(l35_li3637,lemma,
% 16.22/16.31 ! [U,V,W,X] :
% 16.22/16.31 ( ( pair_in_list(U,V,W)
% 16.22/16.31 & less_than(X,W) )
% 16.22/16.31 => pair_in_list(update_slb(U,X),V,W) ) ).
% 16.22/16.31
% 16.22/16.31 %----tmp_not_check_03_3 (cpq_l038.p, cpq_l039.p)
% 16.22/16.31 fof(l35_li3839,lemma,
% 16.22/16.31 ! [U,V,W,X] :
% 16.22/16.31 ( ( pair_in_list(U,V,W)
% 16.22/16.31 & strictly_less_than(W,X) )
% 16.22/16.31 => pair_in_list(update_slb(U,X),V,X) ) ).
% 16.22/16.31
% 16.22/16.31 %----tmp_not_check_03_1 (conjecture)
% 16.22/16.31 fof(l35_co,conjecture,
% 16.22/16.31 ! [U] :
% 16.22/16.31 ( ? [V,W] :
% 16.22/16.31 ( pair_in_list(U,V,W)
% 16.22/16.31 & strictly_less_than(V,W) )
% 16.22/16.31 => ! [X] :
% 16.22/16.31 ? [Y,Z] :
% 16.22/16.31 ( pair_in_list(update_slb(U,X),Y,Z)
% 16.22/16.31 & strictly_less_than(Y,Z) ) ) ).
% 16.22/16.31
% 16.22/16.31 %------------------------------------------------------------------------------
% 16.22/16.31 %-------------------------------------------
% 16.22/16.31 % Proof found
% 16.22/16.31 % SZS status Theorem for theBenchmark
% 16.22/16.31 % SZS output start Proof
% 16.22/16.32 %ClaNum:53(EqnAxiom:23)
% 16.22/16.32 %VarNum:165(SingletonVarNum:84)
% 16.22/16.32 %MaxLitNum:3
% 16.22/16.32 %MaxfuncDepth:3
% 16.22/16.32 %SharedTerms:10
% 16.22/16.32 %goalClause: 24 28 44
% 16.22/16.32 %singleGoalClaCount:2
% 16.22/16.32 [24]P1(a1,a5)
% 16.22/16.32 [28]P5(a4,a1,a5)
% 16.22/16.32 [32]~P3(a2)
% 16.22/16.32 [26]P2(a3,x261)
% 16.22/16.32 [27]P2(x271,x271)
% 16.22/16.32 [33]~P4(a2,x331)
% 16.22/16.32 [25]E(f6(a2,x251),a2)
% 16.22/16.32 [34]~P5(a2,x341,x342)
% 16.22/16.32 [29]P3(f8(x291,f7(x292,x293)))
% 16.22/16.32 [30]E(f11(f8(x301,f7(x302,x303)),x302),x301)
% 16.22/16.32 [31]E(f10(f8(x311,f7(x312,x313)),x312),x313)
% 16.22/16.32 [35]P2(x352,x351)+P2(x351,x352)
% 16.22/16.32 [36]~P1(x361,x362)+P2(x361,x362)
% 16.22/16.32 [37]~P1(x372,x371)+~P2(x371,x372)
% 16.22/16.32 [44]~P1(x441,x442)+~P5(f6(a4,a9),x441,x442)
% 16.22/16.32 [40]~E(x402,x404)+P4(f8(x401,f7(x402,x403)),x404)
% 16.22/16.32 [41]~P4(x411,x414)+P4(f8(x411,f7(x412,x413)),x414)
% 16.22/16.32 [46]~P2(x462,x464)+E(f8(f6(x461,x462),f7(x463,x464)),f6(f8(x461,f7(x463,x464)),x462))
% 16.22/16.32 [47]~P1(x473,x474)+E(f6(f8(x471,f7(x472,x473)),x474),f8(f6(x471,x474),f7(x472,x474)))
% 16.22/16.32 [51]~P5(x511,x514,x515)+P5(f8(x511,f7(x512,x513)),x514,x515)
% 16.22/16.32 [38]P1(x382,x381)+~P2(x382,x381)+P2(x381,x382)
% 16.22/16.32 [39]~P2(x391,x393)+P2(x391,x392)+~P2(x393,x392)
% 16.22/16.32 [49]~P5(x491,x493,x494)+~P1(x494,x492)+P5(f6(x491,x492),x493,x492)
% 16.22/16.32 [50]~P2(x502,x504)+~P5(x501,x503,x504)+P5(f6(x501,x502),x503,x504)
% 16.22/16.32 [45]E(x451,x452)+P4(x453,x452)+~P4(f8(x453,f7(x451,x454)),x452)
% 16.22/16.32 [42]~P4(x423,x422)+E(x421,x422)+E(f10(f8(x423,f7(x421,x424)),x422),f10(x423,x422))
% 16.22/16.32 [48]~P4(x483,x482)+E(x481,x482)+E(f11(f8(x483,f7(x481,x484)),x482),f8(f11(x483,x482),f7(x481,x484)))
% 16.22/16.32 [43]~E(x433,x435)+~E(x432,x434)+P5(f8(x431,f7(x432,x433)),x434,x435)
% 16.22/16.32 [52]E(x521,x522)+P5(x523,x524,x522)+~P5(f8(x523,f7(x525,x521)),x524,x522)
% 16.22/16.32 [53]E(x531,x532)+P5(x533,x532,x534)+~P5(f8(x533,f7(x531,x535)),x532,x534)
% 16.22/16.32 %EqnAxiom
% 16.22/16.32 [1]E(x11,x11)
% 16.22/16.32 [2]E(x22,x21)+~E(x21,x22)
% 16.22/16.32 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 16.22/16.32 [4]~E(x41,x42)+E(f6(x41,x43),f6(x42,x43))
% 16.22/16.32 [5]~E(x51,x52)+E(f6(x53,x51),f6(x53,x52))
% 16.22/16.32 [6]~E(x61,x62)+E(f7(x61,x63),f7(x62,x63))
% 16.22/16.32 [7]~E(x71,x72)+E(f7(x73,x71),f7(x73,x72))
% 16.22/16.32 [8]~E(x81,x82)+E(f8(x81,x83),f8(x82,x83))
% 16.22/16.32 [9]~E(x91,x92)+E(f8(x93,x91),f8(x93,x92))
% 16.22/16.32 [10]~E(x101,x102)+E(f10(x101,x103),f10(x102,x103))
% 16.22/16.32 [11]~E(x111,x112)+E(f10(x113,x111),f10(x113,x112))
% 16.22/16.32 [12]~E(x121,x122)+E(f11(x121,x123),f11(x122,x123))
% 16.22/16.32 [13]~E(x131,x132)+E(f11(x133,x131),f11(x133,x132))
% 16.22/16.32 [14]P1(x142,x143)+~E(x141,x142)+~P1(x141,x143)
% 16.22/16.32 [15]P1(x153,x152)+~E(x151,x152)+~P1(x153,x151)
% 16.22/16.32 [16]P2(x162,x163)+~E(x161,x162)+~P2(x161,x163)
% 16.22/16.32 [17]P2(x173,x172)+~E(x171,x172)+~P2(x173,x171)
% 16.22/16.32 [18]P5(x182,x183,x184)+~E(x181,x182)+~P5(x181,x183,x184)
% 16.22/16.32 [19]P5(x193,x192,x194)+~E(x191,x192)+~P5(x193,x191,x194)
% 16.22/16.32 [20]P5(x203,x204,x202)+~E(x201,x202)+~P5(x203,x204,x201)
% 16.22/16.32 [21]P4(x212,x213)+~E(x211,x212)+~P4(x211,x213)
% 16.22/16.32 [22]P4(x223,x222)+~E(x221,x222)+~P4(x223,x221)
% 16.22/16.32 [23]~P3(x231)+P3(x232)+~E(x231,x232)
% 16.22/16.32
% 16.22/16.32 %-------------------------------------------
% 16.25/16.32 cnf(54,plain,
% 16.25/16.32 (P4(f8(x542,f7(x541,x543)),x541)),
% 16.25/16.32 inference(equality_inference,[],[40])).
% 16.25/16.32 cnf(55,plain,
% 16.25/16.32 (~P1(x551,x551)),
% 16.25/16.32 inference(scs_inference,[],[27,37])).
% 16.25/16.32 cnf(57,plain,
% 16.25/16.32 (E(a2,f6(a2,x571))),
% 16.25/16.32 inference(scs_inference,[],[27,25,37,2])).
% 16.25/16.32 cnf(58,plain,
% 16.25/16.32 (~E(a1,a5)),
% 16.25/16.32 inference(scs_inference,[],[24,27,25,37,2,14])).
% 16.25/16.32 cnf(59,plain,
% 16.25/16.32 (~E(a4,a2)),
% 16.25/16.32 inference(scs_inference,[],[24,28,27,34,25,37,2,14,18])).
% 16.25/16.32 cnf(63,plain,
% 16.25/16.32 (P4(f8(x631,f7(x632,x633)),x632)),
% 16.25/16.32 inference(rename_variables,[],[54])).
% 16.25/16.32 cnf(64,plain,
% 16.25/16.32 (P4(f8(x641,f7(f6(a2,x642),x643)),a2)),
% 16.25/16.32 inference(scs_inference,[],[24,28,27,54,63,34,33,25,37,2,14,18,3,21,22])).
% 16.25/16.32 cnf(66,plain,
% 16.25/16.32 (~P3(f6(a2,x661))),
% 16.25/16.32 inference(scs_inference,[],[24,28,27,54,63,34,33,32,25,37,2,14,18,3,21,22,23])).
% 16.25/16.32 cnf(74,plain,
% 16.25/16.32 (~P1(x741,a3)),
% 16.25/16.32 inference(scs_inference,[],[26,37])).
% 16.25/16.32 cnf(76,plain,
% 16.25/16.32 (E(x761,f11(f8(x761,f7(x762,x763)),x762))),
% 16.25/16.32 inference(scs_inference,[],[26,30,37,2])).
% 16.25/16.32 cnf(77,plain,
% 16.25/16.32 (P2(f11(f8(a3,f7(x771,x772)),x771),x773)),
% 16.25/16.32 inference(scs_inference,[],[26,30,37,2,16])).
% 16.25/16.32 cnf(78,plain,
% 16.25/16.32 (P4(f8(x781,f7(f6(a2,x782),x783)),f6(a2,x784))),
% 16.25/16.32 inference(scs_inference,[],[26,64,57,30,37,2,16,22])).
% 16.25/16.32 cnf(83,plain,
% 16.25/16.32 (P2(a2,f6(a2,x831))),
% 16.25/16.33 inference(scs_inference,[],[24,55,58,26,64,57,27,30,31,37,2,16,22,15,3,17])).
% 16.25/16.33 cnf(92,plain,
% 16.25/16.33 (P5(a4,x921,a5)+~E(a1,x921)),
% 16.25/16.33 inference(scs_inference,[],[24,28,55,58,26,64,57,27,30,31,33,37,2,16,22,15,3,17,45,38,23,19])).
% 16.25/16.33 cnf(98,plain,
% 16.25/16.33 (E(x981,f10(f8(x982,f7(x983,x981)),x983))),
% 16.25/16.33 inference(scs_inference,[],[77,31,37,2])).
% 16.25/16.33 cnf(100,plain,
% 16.25/16.33 (E(x1001,f11(f8(x1001,f7(x1002,x1003)),x1002))),
% 16.25/16.33 inference(rename_variables,[],[76])).
% 16.25/16.33 cnf(102,plain,
% 16.25/16.33 (P4(f8(x1021,f7(a2,x1022)),f6(a2,x1023))),
% 16.25/16.33 inference(scs_inference,[],[54,57,76,77,83,29,31,37,2,23,16,22])).
% 16.25/16.33 cnf(105,plain,
% 16.25/16.33 (E(x1051,f11(f8(x1051,f7(x1052,x1053)),x1052))),
% 16.25/16.33 inference(rename_variables,[],[76])).
% 16.25/16.33 cnf(106,plain,
% 16.25/16.33 (E(a2,f11(f8(f6(a2,x1061),f7(x1062,x1063)),x1062))),
% 16.25/16.33 inference(scs_inference,[],[28,54,57,76,100,105,77,83,29,31,37,2,23,16,22,19,3])).
% 16.25/16.33 cnf(107,plain,
% 16.25/16.33 (E(x1071,f11(f8(x1071,f7(x1072,x1073)),x1072))),
% 16.25/16.33 inference(rename_variables,[],[76])).
% 16.25/16.33 cnf(110,plain,
% 16.25/16.33 (P2(a2,f11(f8(f6(a2,x1101),f7(x1102,x1103)),x1102))),
% 16.25/16.33 inference(scs_inference,[],[24,28,74,54,57,76,100,105,107,77,83,29,31,37,2,23,16,22,19,3,15,17])).
% 16.25/16.33 cnf(118,plain,
% 16.25/16.33 (E(f11(f8(f6(a2,x1181),f7(x1182,x1183)),x1182),a2)),
% 16.25/16.33 inference(scs_inference,[],[83,106,37,2])).
% 16.25/16.33 cnf(120,plain,
% 16.25/16.33 (E(f6(a2,x1201),f11(f8(f6(a2,x1202),f7(x1203,x1204)),x1203))),
% 16.25/16.33 inference(scs_inference,[],[83,106,25,32,37,2,23,3])).
% 16.25/16.33 cnf(121,plain,
% 16.25/16.33 (P5(a4,f10(f8(x1211,f7(x1212,a1)),x1212),a5)),
% 16.25/16.33 inference(scs_inference,[],[28,83,98,106,25,32,37,2,23,3,19])).
% 16.25/16.33 cnf(160,plain,
% 16.25/16.33 (P2(a1,a5)),
% 16.25/16.33 inference(scs_inference,[],[24,35,37])).
% 16.25/16.33 cnf(163,plain,
% 16.25/16.33 (P2(a1,f11(f8(a5,f7(x1631,x1632)),x1631))),
% 16.25/16.33 inference(scs_inference,[],[160,76,37,17])).
% 16.25/16.33 cnf(164,plain,
% 16.25/16.33 (E(x1641,f11(f8(x1641,f7(x1642,x1643)),x1642))),
% 16.25/16.33 inference(rename_variables,[],[76])).
% 16.25/16.33 cnf(165,plain,
% 16.25/16.33 (P2(f11(f8(a1,f7(x1651,x1652)),x1651),a5)),
% 16.25/16.33 inference(scs_inference,[],[160,76,164,37,17,16])).
% 16.25/16.33 cnf(169,plain,
% 16.25/16.33 (E(f8(f6(x1691,a1),f7(x1692,a5)),f6(f8(x1691,f7(x1692,a5)),a1))),
% 16.25/16.33 inference(scs_inference,[],[24,36,46])).
% 16.25/16.33 cnf(177,plain,
% 16.25/16.33 (E(x1771,f10(f8(x1772,f7(x1773,x1771)),x1773))),
% 16.25/16.33 inference(rename_variables,[],[98])).
% 16.25/16.33 cnf(178,plain,
% 16.25/16.33 (P2(f10(f8(x1781,f7(x1782,a1)),x1782),a5)),
% 16.25/16.33 inference(scs_inference,[],[98,177,160,169,163,29,2,37,23,17,16])).
% 16.25/16.33 cnf(190,plain,
% 16.25/16.33 (P2(a5,f10(f8(x1901,f7(x1902,a1)),x1902))+P1(f10(f8(x1901,f7(x1902,a1)),x1902),a5)),
% 16.25/16.33 inference(scs_inference,[],[178,37,38])).
% 16.27/16.33 cnf(194,plain,
% 16.27/16.33 (E(f6(f6(a2,x1941),x1942),f6(a2,x1942))),
% 16.27/16.33 inference(scs_inference,[],[57,4,2])).
% 16.27/16.33 cnf(195,plain,
% 16.27/16.33 (E(f6(a2,x1951),f6(f6(a2,x1952),x1951))),
% 16.27/16.33 inference(scs_inference,[],[194,2])).
% 16.27/16.33 cnf(198,plain,
% 16.27/16.33 (~P3(f6(f6(a2,x1981),x1982))),
% 16.27/16.33 inference(scs_inference,[],[165,194,66,2,37,23])).
% 16.27/16.33 cnf(202,plain,
% 16.27/16.33 (E(f6(x2021,f7(a2,x2022)),f6(x2021,f7(f6(a2,x2023),x2022)))),
% 16.27/16.33 inference(scs_inference,[],[57,5,6])).
% 16.27/16.33 cnf(203,plain,
% 16.27/16.33 (E(f6(x2031,f7(f6(a2,x2032),x2033)),f6(x2031,f7(a2,x2033)))),
% 16.27/16.33 inference(scs_inference,[],[202,2])).
% 16.27/16.33 cnf(237,plain,
% 16.27/16.33 (P5(f8(a4,f7(x2371,x2372)),f10(f8(x2373,f7(x2374,a1)),x2374),a5)),
% 16.27/16.33 inference(scs_inference,[],[98,51,92])).
% 16.27/16.33 cnf(240,plain,
% 16.27/16.33 (P2(f11(f8(x2401,f7(x2402,x2403)),x2402),x2401)),
% 16.27/16.33 inference(scs_inference,[],[30,27,17])).
% 16.27/16.33 cnf(241,plain,
% 16.27/16.33 (P2(x2411,x2411)),
% 16.27/16.33 inference(rename_variables,[],[27])).
% 16.27/16.33 cnf(242,plain,
% 16.27/16.33 (P2(x2421,f11(f8(x2421,f7(x2422,x2423)),x2422))),
% 16.27/16.33 inference(scs_inference,[],[30,27,241,17,16])).
% 16.27/16.33 cnf(255,plain,
% 16.27/16.33 (E(f10(f8(x2551,f7(x2552,x2553)),x2552),x2553)),
% 16.27/16.33 inference(rename_variables,[],[31])).
% 16.27/16.33 cnf(256,plain,
% 16.27/16.33 (P2(f10(f8(x2561,f7(x2562,x2563)),x2562),x2563)),
% 16.27/16.33 inference(scs_inference,[],[31,255,237,27,19,17])).
% 16.27/16.33 cnf(276,plain,
% 16.27/16.33 (~P5(f6(a4,a9),f10(f8(x2761,f7(x2762,a1)),x2762),a5)+P2(a5,f10(f8(x2761,f7(x2762,a1)),x2762))),
% 16.27/16.33 inference(scs_inference,[],[190,44])).
% 16.27/16.33 cnf(307,plain,
% 16.27/16.33 (P2(f6(a2,x3071),f11(f8(a2,f7(x3072,x3073)),x3072))),
% 16.27/16.33 inference(scs_inference,[],[57,240,242,17,16])).
% 16.27/16.33 cnf(316,plain,
% 16.27/16.33 (P2(f10(f8(x3161,f7(x3162,a2)),x3162),f6(a2,x3163))),
% 16.27/16.33 inference(scs_inference,[],[57,59,307,256,30,37,3,17])).
% 16.27/16.33 cnf(471,plain,
% 16.27/16.33 (E(f6(f6(a2,x4711),x4712),f6(f6(f6(a2,x4713),x4711),x4712))),
% 16.27/16.33 inference(scs_inference,[],[194,2,4])).
% 16.27/16.33 cnf(472,plain,
% 16.27/16.33 (E(f6(f6(f6(a2,x4721),x4722),x4723),f6(f6(a2,x4722),x4723))),
% 16.27/16.33 inference(scs_inference,[],[471,2])).
% 16.27/16.33 cnf(475,plain,
% 16.27/16.33 (P2(x4751,x4751)),
% 16.27/16.33 inference(rename_variables,[],[27])).
% 16.27/16.33 cnf(476,plain,
% 16.27/16.33 (P2(f6(a2,x4761),f6(f6(a2,x4762),x4761))),
% 16.27/16.33 inference(scs_inference,[],[194,27,475,471,198,2,23,17,16])).
% 16.27/16.33 cnf(478,plain,
% 16.27/16.33 (E(f6(f6(a2,x4781),f7(f6(a2,x4782),x4783)),f6(f6(f6(a2,x4784),x4781),f7(a2,x4783)))),
% 16.27/16.33 inference(scs_inference,[],[194,27,475,203,471,198,2,23,17,16,3])).
% 16.27/16.33 cnf(481,plain,
% 16.27/16.33 (~P1(f6(a2,x4811),f6(f6(a2,x4812),x4811))),
% 16.27/16.33 inference(scs_inference,[],[194,27,475,203,471,198,2,23,17,16,3,37])).
% 16.27/16.33 cnf(483,plain,
% 16.27/16.33 (P2(a2,f6(f6(a2,x4831),x4832))),
% 16.27/16.33 inference(scs_inference,[],[194,83,27,475,203,471,198,2,23,17,16,3,37,39])).
% 16.27/16.33 cnf(485,plain,
% 16.27/16.33 (P2(f6(f6(a2,x4851),x4852),a2)+P1(a2,f6(f6(a2,x4851),x4852))),
% 16.27/16.33 inference(scs_inference,[],[194,83,27,475,203,471,198,2,23,17,16,3,37,39,38])).
% 16.27/16.33 cnf(487,plain,
% 16.27/16.33 (P2(f6(f6(a2,x4871),x4872),a2)),
% 16.27/16.33 inference(scs_inference,[],[481,57,485,14])).
% 16.27/16.33 cnf(488,plain,
% 16.27/16.33 (E(f6(f6(f6(a2,x4881),x4882),f7(a2,x4883)),f6(f6(a2,x4882),f7(f6(a2,x4884),x4883)))),
% 16.27/16.33 inference(scs_inference,[],[478,2])).
% 16.27/16.33 cnf(495,plain,
% 16.27/16.33 (P2(f11(f8(f6(f6(a2,x4951),x4952),f7(x4953,x4954)),x4953),f6(a2,x4952))),
% 16.27/16.33 inference(scs_inference,[],[194,487,83,240,242,478,2,37,39,16,17])).
% 16.27/16.33 cnf(506,plain,
% 16.27/16.33 (P2(f11(f8(f6(a2,x5061),f7(x5062,x5063)),x5062),f6(f6(a2,x5064),x5065))),
% 16.27/16.33 inference(scs_inference,[],[487,110,120,495,476,37,39,16])).
% 16.27/16.33 cnf(523,plain,
% 16.27/16.33 (P2(f6(f6(a2,x5231),x5232),f6(f6(a2,x5233),x5234))),
% 16.27/16.33 inference(scs_inference,[],[487,506,483,37,39])).
% 16.27/16.33 cnf(560,plain,
% 16.27/16.33 (P4(f8(x5601,f7(a2,x5602)),f6(f6(a2,x5603),x5604))),
% 16.27/16.33 inference(scs_inference,[],[195,102,22])).
% 16.27/16.33 cnf(579,plain,
% 16.27/16.33 (E(f6(f6(a2,x5791),x5792),f6(a2,x5793))),
% 16.27/16.33 inference(scs_inference,[],[195,78,316,33,22,17,37,45,2])).
% 16.27/16.33 cnf(641,plain,
% 16.27/16.33 (P1(f10(f8(x6411,f7(x6412,a1)),x6412),a5)),
% 16.27/16.33 inference(scs_inference,[],[24,98,14])).
% 16.27/16.33 cnf(733,plain,
% 16.27/16.33 (P2(a5,x7331)+P5(f6(a4,x7331),a1,a5)),
% 16.27/16.33 inference(scs_inference,[],[28,35,50])).
% 16.27/16.33 cnf(734,plain,
% 16.27/16.33 (P5(f6(a4,a1),a1,a5)),
% 16.27/16.33 inference(scs_inference,[],[24,733,37])).
% 16.27/16.33 cnf(735,plain,
% 16.27/16.33 (~E(f6(a4,a1),a2)),
% 16.27/16.33 inference(scs_inference,[],[734,34,18])).
% 16.27/16.33 cnf(737,plain,
% 16.27/16.33 (P5(f6(a4,a1),f10(f8(x7371,f7(x7372,a1)),x7372),a5)),
% 16.27/16.33 inference(scs_inference,[],[734,98,34,18,19])).
% 16.27/16.33 cnf(741,plain,
% 16.27/16.33 (~E(f6(a4,a1),f11(f8(f6(a2,x7411),f7(x7412,x7413)),x7412))),
% 16.27/16.33 inference(scs_inference,[],[735,118,3])).
% 16.27/16.33 cnf(742,plain,
% 16.27/16.33 (~E(f6(a4,a1),f6(a2,x7421))),
% 16.27/16.33 inference(scs_inference,[],[120,741,3])).
% 16.27/16.33 cnf(744,plain,
% 16.27/16.33 (~P5(f6(a4,a9),f10(f8(x7441,f7(x7442,a1)),x7442),a5)),
% 16.27/16.33 inference(scs_inference,[],[641,37,276])).
% 16.27/16.33 cnf(745,plain,
% 16.27/16.33 (~P2(a9,a5)),
% 16.27/16.33 inference(scs_inference,[],[744,121,50])).
% 16.27/16.33 cnf(746,plain,
% 16.27/16.33 (~P5(f6(a4,a9),f10(f8(x7461,f7(x7462,a1)),x7462),a5)),
% 16.27/16.33 inference(rename_variables,[],[744])).
% 16.27/16.33 cnf(750,plain,
% 16.27/16.33 (~E(f6(a4,a1),f6(f6(a2,x7501),x7502))),
% 16.27/16.33 inference(scs_inference,[],[744,746,237,121,579,742,50,18,3])).
% 16.27/16.33 cnf(752,plain,
% 16.27/16.33 (~P1(a9,a5)),
% 16.27/16.33 inference(scs_inference,[],[744,746,237,121,579,742,50,18,3,36])).
% 16.27/16.33 cnf(754,plain,
% 16.27/16.33 (P2(a5,a9)),
% 16.27/16.33 inference(scs_inference,[],[744,746,237,121,579,742,50,18,3,36,35])).
% 16.27/16.33 cnf(756,plain,
% 16.27/16.33 (P2(a1,a9)),
% 16.27/16.33 inference(scs_inference,[],[744,746,237,121,160,579,742,50,18,3,36,35,39])).
% 16.27/16.33 cnf(758,plain,
% 16.27/16.33 (P1(a5,a9)),
% 16.27/16.33 inference(scs_inference,[],[744,746,237,121,160,579,742,50,18,3,36,35,39,38])).
% 16.27/16.33 cnf(761,plain,
% 16.27/16.33 (E(x7611,f10(f8(x7612,f7(x7613,x7611)),x7613))),
% 16.27/16.33 inference(rename_variables,[],[98])).
% 16.27/16.33 cnf(762,plain,
% 16.27/16.33 (P2(f10(f8(x7621,f7(x7622,a5)),x7622),a9)),
% 16.27/16.33 inference(scs_inference,[],[744,746,237,121,160,98,761,579,742,50,18,3,36,35,39,38,15,16])).
% 16.27/16.33 cnf(763,plain,
% 16.27/16.33 (E(x7631,f10(f8(x7632,f7(x7633,x7631)),x7633))),
% 16.27/16.33 inference(rename_variables,[],[98])).
% 16.27/16.33 cnf(764,plain,
% 16.27/16.33 (P2(a5,f10(f8(x7641,f7(x7642,a9)),x7642))),
% 16.27/16.33 inference(scs_inference,[],[744,746,237,121,160,98,761,763,579,742,50,18,3,36,35,39,38,15,16,17])).
% 16.27/16.33 cnf(776,plain,
% 16.27/16.33 (P2(a1,f10(f8(x7761,f7(x7762,a9)),x7762))),
% 16.27/16.33 inference(scs_inference,[],[24,752,744,121,160,762,764,37,18,14,39])).
% 16.27/16.33 cnf(781,plain,
% 16.27/16.33 (P2(f10(f8(x7811,f7(x7812,a1)),x7812),a9)),
% 16.27/16.33 inference(scs_inference,[],[24,752,744,121,160,98,488,750,762,764,756,37,18,14,39,3,16])).
% 16.27/16.33 cnf(792,plain,
% 16.27/16.33 (E(x7921,f11(f8(x7921,f7(x7922,x7923)),x7922))),
% 16.27/16.33 inference(rename_variables,[],[76])).
% 16.27/16.33 cnf(794,plain,
% 16.27/16.33 (E(x7941,f11(f8(x7941,f7(x7942,x7943)),x7942))),
% 16.27/16.33 inference(rename_variables,[],[76])).
% 16.27/16.33 cnf(796,plain,
% 16.27/16.33 (E(x7961,f11(f8(x7961,f7(x7962,x7963)),x7962))),
% 16.27/16.33 inference(rename_variables,[],[76])).
% 16.27/16.33 cnf(798,plain,
% 16.27/16.33 (E(x7981,f11(f8(x7981,f7(x7982,x7983)),x7982))),
% 16.27/16.33 inference(rename_variables,[],[76])).
% 16.27/16.33 cnf(802,plain,
% 16.27/16.33 (E(x8021,f11(f8(x8021,f7(x8022,x8023)),x8022))),
% 16.27/16.33 inference(rename_variables,[],[76])).
% 16.27/16.33 cnf(803,plain,
% 16.27/16.33 (P2(f11(f8(f6(f6(a2,x8031),x8032),f7(x8033,x8034)),x8033),f6(f6(a2,x8035),x8036))),
% 16.27/16.33 inference(scs_inference,[],[24,744,752,734,737,641,76,792,794,796,798,802,472,523,560,754,776,750,37,18,14,19,20,15,22,3,17,16])).
% 16.27/16.33 cnf(810,plain,
% 16.27/16.33 (P2(a9,a1)+P1(a1,a9)),
% 16.27/16.33 inference(scs_inference,[],[24,744,752,734,737,641,160,76,792,794,796,798,802,472,523,560,754,756,776,750,33,37,18,14,19,20,15,22,3,17,16,45,39,38])).
% 16.27/16.33 cnf(812,plain,
% 16.27/16.33 (E(f11(f8(f6(f6(a2,x8121),x8122),f7(x8123,x8124)),x8123),a2)),
% 16.27/16.33 inference(scs_inference,[],[24,744,752,734,737,641,160,76,792,794,796,798,802,472,523,560,754,756,776,750,33,37,18,14,19,20,15,22,3,17,16,45,39,38,2])).
% 16.27/16.33 cnf(813,plain,
% 16.27/16.33 (P1(a1,a9)),
% 16.27/16.33 inference(scs_inference,[],[160,745,810,39])).
% 16.27/16.33 cnf(819,plain,
% 16.27/16.33 (P2(a9,f10(f8(x8191,f7(x8192,a1)),x8192))+P1(f10(f8(x8191,f7(x8192,a1)),x8192),a9)),
% 16.27/16.33 inference(scs_inference,[],[813,735,98,803,812,781,37,15,3,38])).
% 16.27/16.33 cnf(821,plain,
% 16.27/16.33 (~P5(f6(a4,a9),f10(f8(x8211,f7(x8212,a1)),x8212),a9)+P2(a9,f10(f8(x8211,f7(x8212,a1)),x8212))),
% 16.27/16.33 inference(scs_inference,[],[819,44])).
% 16.27/16.33 cnf(858,plain,
% 16.27/16.33 (~P5(f6(a4,a9),f10(f8(x8581,f7(x8582,a1)),x8582),a9)),
% 16.27/16.33 inference(scs_inference,[],[178,745,821,39])).
% 16.27/16.33 cnf(859,plain,
% 16.27/16.33 ($false),
% 16.27/16.33 inference(scs_inference,[],[858,121,758,49]),
% 16.27/16.33 ['proof']).
% 16.27/16.33 % SZS output end Proof
% 16.27/16.33 % Total time :15.700000s
%------------------------------------------------------------------------------