%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : SWV390+1 : TPTP v8.2.0. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n019.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:04 EDT 2024
% Result : Theorem 0.59s 0.80s
% Output : CNFRefutation 0.59s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SWV390+1 : TPTP v8.2.0. Released v3.3.0.
% 0.03/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n019.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 : Thu Jun 20 15:05:24 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.50/0.60 start to proof:theBenchmark
% 0.59/0.80 %-------------------------------------------
% 0.59/0.80 % File :CSE---1.7
% 0.59/0.80 % Problem :theBenchmark
% 0.59/0.80 % Transform :cnf
% 0.59/0.80 % Format :tptp:raw
% 0.59/0.80 % Command :java -jar mcs_scs.jar %d %s
% 0.59/0.80
% 0.59/0.80 % Result :Theorem 0.140000s
% 0.59/0.80 % Output :CNFRefutation 0.140000s
% 0.59/0.80 %-------------------------------------------
% 0.59/0.80 %------------------------------------------------------------------------------
% 0.59/0.80 % File : SWV390+1 : TPTP v8.2.0. Released v3.3.0.
% 0.59/0.80 % Domain : Software Verification
% 0.59/0.80 % Problem : Priority queue checker: tmp_not_check_01
% 0.59/0.80 % Version : [dNP05] axioms.
% 0.59/0.80 % English :
% 0.59/0.80
% 0.59/0.80 % Refs : [Pis06] Piskac (2006), Email to Geoff Sutcliffe
% 0.59/0.80 % : [dNP05] de Nivelle & Piskac (2005), Verification of an Off-Lin
% 0.59/0.80 % Source : [Pis06]
% 0.59/0.80 % Names : cpq_l026 [Pis06]
% 0.59/0.80
% 0.59/0.80 % Status : Theorem
% 0.59/0.80 % Rating : 0.22 v8.2.0, 0.25 v7.5.0, 0.28 v7.4.0, 0.20 v7.3.0, 0.24 v7.2.0, 0.21 v7.1.0, 0.22 v7.0.0, 0.23 v6.4.0, 0.27 v6.3.0, 0.33 v6.2.0, 0.36 v6.1.0, 0.37 v6.0.0, 0.26 v5.5.0, 0.33 v5.4.0, 0.43 v5.3.0, 0.52 v5.2.0, 0.40 v5.1.0, 0.38 v4.1.0, 0.35 v4.0.1, 0.39 v4.0.0, 0.42 v3.7.0, 0.35 v3.5.0, 0.37 v3.4.0, 0.47 v3.3.0
% 0.59/0.80 % Syntax : Number of formulae : 43 ( 16 unt; 0 def)
% 0.59/0.80 % Number of atoms : 87 ( 29 equ)
% 0.59/0.80 % Maximal formula atoms : 4 ( 2 avg)
% 0.59/0.80 % Number of connectives : 59 ( 15 ~; 3 |; 12 &)
% 0.59/0.80 % ( 8 <=>; 21 =>; 0 <=; 0 <~>)
% 0.59/0.80 % Maximal formula depth : 9 ( 5 avg)
% 0.59/0.80 % Maximal term depth : 4 ( 1 avg)
% 0.59/0.80 % Number of predicates : 11 ( 9 usr; 1 prp; 0-3 aty)
% 0.59/0.80 % Number of functors : 18 ( 18 usr; 3 con; 0-3 aty)
% 0.59/0.80 % Number of variables : 126 ( 126 !; 0 ?)
% 0.59/0.80 % SPC : FOF_THM_RFO_SEQ
% 0.59/0.80
% 0.59/0.80 % Comments :
% 0.59/0.80 %------------------------------------------------------------------------------
% 0.59/0.80 %----Include the axioms about priority queues and checked priority queues
% 0.59/0.80 include('Axioms/SWV007+0.ax').
% 0.59/0.80 include('Axioms/SWV007+2.ax').
% 0.59/0.80 include('Axioms/SWV007+3.ax').
% 0.59/0.80 %------------------------------------------------------------------------------
% 0.59/0.80 %----lemma_check_characterization (cpq_l041.p, cpq_l042.p)
% 0.59/0.80 fof(l26_li4142,lemma,
% 0.59/0.80 ! [U,V,W] :
% 0.59/0.80 ( check_cpq(triple(U,V,W))
% 0.59/0.80 <=> ! [X,Y] :
% 0.59/0.80 ( pair_in_list(V,X,Y)
% 0.59/0.80 => less_than(Y,X) ) ) ).
% 0.59/0.80
% 0.59/0.80 %----tmp_not_check_01 (conjecture)
% 0.59/0.80 fof(l26_co,conjecture,
% 0.59/0.80 ! [U,V,W] :
% 0.59/0.80 ( ~ check_cpq(triple(U,V,W))
% 0.59/0.80 => ! [X] : ~ check_cpq(insert_cpq(triple(U,V,W),X)) ) ).
% 0.59/0.80
% 0.59/0.80 %------------------------------------------------------------------------------
% 0.59/0.80 %-------------------------------------------
% 0.59/0.80 % Proof found
% 0.59/0.80 % SZS status Theorem for theBenchmark
% 0.59/0.80 % SZS output start Proof
% 0.59/0.80 %ClaNum:100(EqnAxiom:47)
% 0.59/0.80 %VarNum:322(SingletonVarNum:158)
% 0.59/0.80 %MaxLitNum:4
% 0.59/0.80 %MaxfuncDepth:3
% 0.59/0.80 %SharedTerms:12
% 0.59/0.80 %goalClause: 58 63
% 0.59/0.80 %singleGoalClaCount:2
% 0.59/0.80 [60]~P2(a1)
% 0.59/0.80 [63]~P3(f22(a9,a12,a13))
% 0.59/0.80 [58]P3(f15(f22(a9,a12,a13),a14))
% 0.59/0.80 [49]P1(a2,x491)
% 0.59/0.80 [50]P1(x501,x501)
% 0.59/0.80 [51]P6(x511,x511)
% 0.59/0.80 [61]~P4(a1,x611)
% 0.59/0.80 [48]E(f4(a1,x481),a1)
% 0.59/0.80 [62]~P7(a1,x621,x622)
% 0.59/0.80 [56]P3(f22(x561,a1,x562))
% 0.59/0.80 [64]~P8(f22(x641,x642,a3))
% 0.59/0.80 [55]E(f7(f22(x551,a1,x552)),a2)
% 0.59/0.80 [57]E(f8(f22(x571,a1,x572)),f22(x571,a1,a3))
% 0.59/0.80 [52]P2(f6(x521,f5(x522,x523)))
% 0.59/0.80 [53]E(f19(f6(x531,f5(x532,x533)),x532),x531)
% 0.59/0.80 [54]E(f18(f6(x541,f5(x542,x543)),x542),x543)
% 0.59/0.80 [59]E(f22(f17(x591,x592),f6(x593,f5(x592,a2)),x594),f15(f22(x591,x593,x594),x592))
% 0.59/0.80 [65]P1(x652,x651)+P1(x651,x652)
% 0.59/0.81 [66]~P9(x661,x662)+P1(x661,x662)
% 0.59/0.81 [68]~P9(x682,x681)+~P1(x681,x682)
% 0.59/0.81 [67]~P6(x671,x672)+P6(x671,f8(x672))
% 0.59/0.81 [73]~P6(x731,x732)+P6(x731,f20(f8(x732),f7(x732)))
% 0.59/0.81 [71]~P6(x711,x712)+P6(x711,f15(x712,x713))
% 0.59/0.81 [72]~P6(x721,x722)+P6(x721,f20(x722,x723))
% 0.59/0.81 [75]E(x751,a3)+P8(f22(x752,x753,x751))
% 0.59/0.81 [87]~P1(f10(x871,x872),f11(x871,x872))+P3(f22(x871,x872,x873))
% 0.59/0.81 [88]P7(x882,f11(x881,x882),f10(x881,x882))+P3(f22(x881,x882,x883))
% 0.59/0.81 [77]E(x771,a1)+E(f7(f22(x772,x771,x773)),f16(x772))
% 0.59/0.81 [80]~P4(x802,x804)+P5(f22(x801,x802,x803),x804)
% 0.59/0.81 [86]P4(x861,x862)+~P5(f22(x863,x861,x864),x862)
% 0.59/0.81 [74]~E(x742,x744)+P4(f6(x741,f5(x742,x743)),x744)
% 0.59/0.81 [76]~P4(x761,x764)+P4(f6(x761,f5(x762,x763)),x764)
% 0.59/0.81 [85]P4(x852,x854)+E(f20(f22(x851,x852,x853),x854),f22(x851,x852,a3))
% 0.59/0.81 [82]~P1(x822,x824)+E(f6(f4(x821,x822),f5(x823,x824)),f4(f6(x821,f5(x823,x824)),x822))
% 0.59/0.81 [83]~P9(x833,x834)+E(f4(f6(x831,f5(x832,x833)),x834),f6(f4(x831,x834),f5(x832,x834)))
% 0.59/0.81 [89]~P7(x891,x894,x895)+P7(f6(x891,f5(x892,x893)),x894,x895)
% 0.59/0.81 [98]~P9(x981,x982)+~P3(f22(x983,f6(x984,f5(x981,x982)),x985))
% 0.59/0.81 [69]P9(x692,x691)+~P1(x692,x691)+P1(x691,x692)
% 0.59/0.81 [70]~P1(x701,x703)+P1(x701,x702)+~P1(x703,x702)
% 0.59/0.81 [90]P4(x901,f16(x902))+E(x901,a1)+E(f8(f22(x902,x901,x903)),f22(x902,f4(x901,f16(x902)),a3))
% 0.59/0.81 [81]E(x811,x812)+P4(x813,x812)+~P4(f6(x813,f5(x811,x814)),x812)
% 0.59/0.81 [94]~P4(x942,x944)+~P9(x944,f18(x942,x944))+E(f20(f22(x941,x942,x943),x944),f22(f21(x941,x944),f19(x942,x944),a3))
% 0.59/0.81 [95]~P4(x953,x952)+~P1(f18(x953,x952),x952)+E(f22(f21(x951,x952),f19(x953,x952),x954),f20(f22(x951,x953,x954),x952))
% 0.59/0.81 [78]~P4(x783,x782)+E(x781,x782)+E(f18(f6(x783,f5(x781,x784)),x782),f18(x783,x782))
% 0.59/0.81 [84]~P4(x843,x842)+E(x841,x842)+E(f19(f6(x843,f5(x841,x844)),x842),f6(f19(x843,x842),f5(x841,x844)))
% 0.59/0.81 [93]P1(x931,x932)+~P7(x933,x932,x931)+~P3(f22(x934,x933,x935))
% 0.59/0.81 [79]~E(x793,x795)+~E(x792,x794)+P7(f6(x791,f5(x792,x793)),x794,x795)
% 0.59/0.81 [91]E(x911,x912)+P7(x913,x914,x912)+~P7(f6(x913,f5(x915,x911)),x914,x912)
% 0.59/0.81 [92]E(x921,x922)+P7(x923,x922,x924)+~P7(f6(x923,f5(x921,x925)),x922,x924)
% 0.59/0.81 [99]~P1(x994,x993)+~P3(f22(x991,x992,x995))+P3(f22(x991,f6(x992,f5(x993,x994)),x995))
% 0.59/0.81 [100]~P1(x1004,x1005)+P3(f22(x1001,x1002,x1003))+~P3(f22(x1001,f6(x1002,f5(x1005,x1004)),x1003))
% 0.59/0.81 [96]~P4(x961,f16(x962))+E(x961,a1)+~P9(f16(x962),f18(x961,f16(x962)))+E(f8(f22(x962,x961,x963)),f22(x962,f4(x961,f16(x962)),a3))
% 0.59/0.81 [97]~P4(x971,f16(x972))+E(x971,a1)+~P1(f18(x971,f16(x972)),f16(x972))+E(f22(x972,f4(x971,f16(x972)),x973),f8(f22(x972,x971,x973)))
% 0.59/0.81 %EqnAxiom
% 0.59/0.81 [1]E(x11,x11)
% 0.59/0.81 [2]E(x22,x21)+~E(x21,x22)
% 0.59/0.81 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 0.59/0.81 [4]~E(x41,x42)+E(f4(x41,x43),f4(x42,x43))
% 0.59/0.81 [5]~E(x51,x52)+E(f4(x53,x51),f4(x53,x52))
% 0.59/0.81 [6]~E(x61,x62)+E(f5(x61,x63),f5(x62,x63))
% 0.59/0.81 [7]~E(x71,x72)+E(f5(x73,x71),f5(x73,x72))
% 0.59/0.81 [8]~E(x81,x82)+E(f6(x81,x83),f6(x82,x83))
% 0.59/0.81 [9]~E(x91,x92)+E(f6(x93,x91),f6(x93,x92))
% 0.59/0.81 [10]~E(x101,x102)+E(f22(x101,x103,x104),f22(x102,x103,x104))
% 0.59/0.81 [11]~E(x111,x112)+E(f22(x113,x111,x114),f22(x113,x112,x114))
% 0.59/0.81 [12]~E(x121,x122)+E(f22(x123,x124,x121),f22(x123,x124,x122))
% 0.59/0.81 [13]~E(x131,x132)+E(f8(x131),f8(x132))
% 0.59/0.81 [14]~E(x141,x142)+E(f19(x141,x143),f19(x142,x143))
% 0.59/0.81 [15]~E(x151,x152)+E(f19(x153,x151),f19(x153,x152))
% 0.59/0.81 [16]~E(x161,x162)+E(f16(x161),f16(x162))
% 0.59/0.81 [17]~E(x171,x172)+E(f18(x171,x173),f18(x172,x173))
% 0.59/0.81 [18]~E(x181,x182)+E(f18(x183,x181),f18(x183,x182))
% 0.59/0.81 [19]~E(x191,x192)+E(f20(x191,x193),f20(x192,x193))
% 0.59/0.81 [20]~E(x201,x202)+E(f20(x203,x201),f20(x203,x202))
% 0.59/0.81 [21]~E(x211,x212)+E(f7(x211),f7(x212))
% 0.59/0.81 [22]~E(x221,x222)+E(f15(x221,x223),f15(x222,x223))
% 0.59/0.81 [23]~E(x231,x232)+E(f15(x233,x231),f15(x233,x232))
% 0.59/0.81 [24]~E(x241,x242)+E(f21(x241,x243),f21(x242,x243))
% 0.59/0.81 [25]~E(x251,x252)+E(f21(x253,x251),f21(x253,x252))
% 0.59/0.81 [26]~E(x261,x262)+E(f10(x261,x263),f10(x262,x263))
% 0.59/0.81 [27]~E(x271,x272)+E(f10(x273,x271),f10(x273,x272))
% 0.59/0.81 [28]~E(x281,x282)+E(f17(x281,x283),f17(x282,x283))
% 0.59/0.81 [29]~E(x291,x292)+E(f17(x293,x291),f17(x293,x292))
% 0.59/0.81 [30]~E(x301,x302)+E(f11(x301,x303),f11(x302,x303))
% 0.59/0.81 [31]~E(x311,x312)+E(f11(x313,x311),f11(x313,x312))
% 0.59/0.81 [32]P1(x322,x323)+~E(x321,x322)+~P1(x321,x323)
% 0.59/0.81 [33]P1(x333,x332)+~E(x331,x332)+~P1(x333,x331)
% 0.59/0.81 [34]~P3(x341)+P3(x342)+~E(x341,x342)
% 0.59/0.81 [35]P6(x352,x353)+~E(x351,x352)+~P6(x351,x353)
% 0.59/0.81 [36]P6(x363,x362)+~E(x361,x362)+~P6(x363,x361)
% 0.59/0.81 [37]~P2(x371)+P2(x372)+~E(x371,x372)
% 0.59/0.81 [38]P7(x382,x383,x384)+~E(x381,x382)+~P7(x381,x383,x384)
% 0.59/0.81 [39]P7(x393,x392,x394)+~E(x391,x392)+~P7(x393,x391,x394)
% 0.59/0.81 [40]P7(x403,x404,x402)+~E(x401,x402)+~P7(x403,x404,x401)
% 0.59/0.81 [41]P4(x412,x413)+~E(x411,x412)+~P4(x411,x413)
% 0.59/0.81 [42]P4(x423,x422)+~E(x421,x422)+~P4(x423,x421)
% 0.59/0.81 [43]P9(x432,x433)+~E(x431,x432)+~P9(x431,x433)
% 0.59/0.81 [44]P9(x443,x442)+~E(x441,x442)+~P9(x443,x441)
% 0.59/0.81 [45]P5(x452,x453)+~E(x451,x452)+~P5(x451,x453)
% 0.59/0.81 [46]P5(x463,x462)+~E(x461,x462)+~P5(x463,x461)
% 0.59/0.81 [47]~P8(x471)+P8(x472)+~E(x471,x472)
% 0.59/0.81
% 0.59/0.81 %-------------------------------------------
% 0.59/0.81 cnf(102,plain,
% 0.59/0.81 (~P1(f10(a9,a12),f11(a9,a12))),
% 0.59/0.81 inference(scs_inference,[],[63,87])).
% 0.59/0.81 cnf(104,plain,
% 0.59/0.81 (P7(a12,f11(a9,a12),f10(a9,a12))),
% 0.59/0.81 inference(scs_inference,[],[63,87,88])).
% 0.59/0.81 cnf(114,plain,
% 0.59/0.81 (E(f19(f6(x1141,f5(x1142,x1143)),x1142),x1141)),
% 0.59/0.81 inference(rename_variables,[],[53])).
% 0.59/0.81 cnf(119,plain,
% 0.59/0.81 (~E(f11(a9,a12),f10(a9,a12))),
% 0.59/0.81 inference(scs_inference,[],[63,50,48,53,114,87,88,65,66,2,68,34,69,3,32])).
% 0.59/0.81 cnf(264,plain,
% 0.59/0.81 (E(f15(f22(x2641,x2642,x2643),x2644),f22(f17(x2641,x2644),f6(x2642,f5(x2644,a2)),x2643))),
% 0.59/0.81 inference(scs_inference,[],[59,2])).
% 0.59/0.81 cnf(292,plain,
% 0.59/0.81 (~P7(f6(a12,f5(a14,a2)),f11(a9,a12),f10(a9,a12))),
% 0.59/0.81 inference(scs_inference,[],[58,102,49,53,119,264,55,2,34,3,100,93])).
% 0.59/0.81 cnf(310,plain,
% 0.59/0.81 ($false),
% 0.59/0.81 inference(scs_inference,[],[104,292,89]),
% 0.59/0.81 ['proof']).
% 0.59/0.81 % SZS output end Proof
% 0.59/0.81 % Total time :0.140000s
%------------------------------------------------------------------------------