%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : SWV405+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 : n021.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:07 EDT 2024
% Result : Theorem 0.20s 0.59s
% Output : CNFRefutation 0.20s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : SWV405+1 : TPTP v8.2.0. Released v3.3.0.
% 0.06/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.11/0.32 % Computer : n021.cluster.edu
% 0.11/0.32 % Model : x86_64 x86_64
% 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.32 % Memory : 8042.1875MB
% 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.32 % CPULimit : 300
% 0.11/0.32 % WCLimit : 300
% 0.11/0.32 % DateTime : Thu Jun 20 17:50:39 EDT 2024
% 0.11/0.33 % CPUTime :
% 0.20/0.54 start to proof:theBenchmark
% 0.20/0.58 %-------------------------------------------
% 0.20/0.58 % File :CSE---1.7
% 0.20/0.58 % Problem :theBenchmark
% 0.20/0.58 % Transform :cnf
% 0.20/0.58 % Format :tptp:raw
% 0.20/0.58 % Command :java -jar mcs_scs.jar %d %s
% 0.20/0.58
% 0.20/0.58 % Result :Theorem 0.000000s
% 0.20/0.58 % Output :CNFRefutation 0.000000s
% 0.20/0.58 %-------------------------------------------
% 0.20/0.59 %------------------------------------------------------------------------------
% 0.20/0.59 % File : SWV405+1 : TPTP v8.2.0. Released v3.3.0.
% 0.20/0.59 % Domain : Software Verification
% 0.20/0.59 % Problem : Priority queue checker: lemma_check_characterization base
% 0.20/0.59 % Version : [dNP05] axioms.
% 0.20/0.59 % English :
% 0.20/0.59
% 0.20/0.59 % Refs : [Pis06] Piskac (2006), Email to Geoff Sutcliffe
% 0.20/0.59 % : [dNP05] de Nivelle & Piskac (2005), Verification of an Off-Lin
% 0.20/0.59 % Source : [Pis06]
% 0.20/0.59 % Names : cpq_l041 [Pis06]
% 0.20/0.59
% 0.20/0.59 % Status : Theorem
% 0.20/0.59 % Rating : 0.06 v7.4.0, 0.07 v7.1.0, 0.09 v7.0.0, 0.07 v6.4.0, 0.08 v6.2.0, 0.16 v6.1.0, 0.07 v6.0.0, 0.04 v5.3.0, 0.11 v5.2.0, 0.10 v5.0.0, 0.08 v4.1.0, 0.09 v4.0.1, 0.13 v4.0.0, 0.17 v3.7.0, 0.15 v3.5.0, 0.16 v3.3.0
% 0.20/0.59 % Syntax : Number of formulae : 42 ( 16 unt; 0 def)
% 0.20/0.59 % Number of atoms : 85 ( 29 equ)
% 0.20/0.59 % Maximal formula atoms : 4 ( 2 avg)
% 0.20/0.59 % Number of connectives : 56 ( 13 ~; 3 |; 12 &)
% 0.20/0.59 % ( 8 <=>; 20 =>; 0 <=; 0 <~>)
% 0.20/0.59 % Maximal formula depth : 9 ( 5 avg)
% 0.20/0.59 % Maximal term depth : 4 ( 1 avg)
% 0.20/0.59 % Number of predicates : 11 ( 9 usr; 1 prp; 0-3 aty)
% 0.20/0.59 % Number of functors : 18 ( 18 usr; 3 con; 0-3 aty)
% 0.20/0.59 % Number of variables : 121 ( 121 !; 0 ?)
% 0.20/0.59 % SPC : FOF_THM_RFO_SEQ
% 0.20/0.59
% 0.20/0.59 % Comments :
% 0.20/0.59 %------------------------------------------------------------------------------
% 0.20/0.59 %----Include the axioms about priority queues and checked priority queues
% 0.20/0.59 include('Axioms/SWV007+0.ax').
% 0.20/0.59 include('Axioms/SWV007+2.ax').
% 0.20/0.59 include('Axioms/SWV007+3.ax').
% 0.20/0.59 %------------------------------------------------------------------------------
% 0.20/0.59 %----goal: fof(l26_li4142, lemma, (! [U,V,W] : (check_cpq(triple(U,V,W)) <=>
% 0.20/0.59 %---- ! [X,Y] : (pair_in_list(V,X,Y) => less_than(Y,X))))).
% 0.20/0.59
% 0.20/0.59 %----lemma_check_characterization::base (conjecture)
% 0.20/0.59 fof(l41_co,conjecture,
% 0.20/0.59 ! [U,V] :
% 0.20/0.59 ( check_cpq(triple(U,create_slb,V))
% 0.20/0.59 <=> ! [W,X] :
% 0.20/0.59 ( pair_in_list(create_slb,W,X)
% 0.20/0.59 => less_than(X,W) ) ) ).
% 0.20/0.59
% 0.20/0.59 %------------------------------------------------------------------------------
% 0.20/0.59 %-------------------------------------------
% 0.20/0.59 % Proof found
% 0.20/0.59 % SZS status Theorem for theBenchmark
% 0.20/0.59 % SZS output start Proof
% 0.20/0.59 %ClaNum:94(EqnAxiom:43)
% 0.20/0.59 %VarNum:299(SingletonVarNum:147)
% 0.20/0.59 %MaxLitNum:4
% 0.20/0.59 %MaxfuncDepth:3
% 0.20/0.59 %SharedTerms:13
% 0.20/0.59 %goalClause: 76 83
% 0.20/0.59 [55]~P2(a1)
% 0.20/0.59 [45]P1(a2,x451)
% 0.20/0.59 [46]P1(x461,x461)
% 0.20/0.59 [47]P6(x471,x471)
% 0.20/0.59 [56]~P4(a1,x561)
% 0.20/0.59 [44]E(f4(a1,x441),a1)
% 0.20/0.59 [57]~P7(a1,x571,x572)
% 0.20/0.59 [52]P3(f20(x521,a1,x522))
% 0.20/0.59 [58]~P8(f20(x581,x582,a3))
% 0.20/0.59 [51]E(f7(f20(x511,a1,x512)),a2)
% 0.20/0.59 [53]E(f8(f20(x531,a1,x532)),f20(x531,a1,a3))
% 0.20/0.59 [48]P2(f6(x481,f5(x482,x483)))
% 0.20/0.59 [49]E(f17(f6(x491,f5(x492,x493)),x492),x491)
% 0.20/0.59 [50]E(f16(f6(x501,f5(x502,x503)),x502),x503)
% 0.20/0.59 [54]E(f20(f13(x541,x542),f6(x543,f5(x542,a2)),x544),f14(f20(x541,x543,x544),x542))
% 0.20/0.59 [76]~P1(a9,a10)+~P3(f20(a11,a1,a12))
% 0.20/0.59 [83]P7(a1,a10,a9)+~P3(f20(a11,a1,a12))
% 0.20/0.59 [59]P1(x592,x591)+P1(x591,x592)
% 0.20/0.59 [60]~P9(x601,x602)+P1(x601,x602)
% 0.20/0.59 [62]~P9(x622,x621)+~P1(x621,x622)
% 0.20/0.59 [61]~P6(x611,x612)+P6(x611,f8(x612))
% 0.20/0.59 [67]~P6(x671,x672)+P6(x671,f18(f8(x672),f7(x672)))
% 0.20/0.59 [65]~P6(x651,x652)+P6(x651,f14(x652,x653))
% 0.20/0.59 [66]~P6(x661,x662)+P6(x661,f18(x662,x663))
% 0.20/0.59 [69]E(x691,a3)+P8(f20(x692,x693,x691))
% 0.20/0.59 [71]E(x711,a1)+E(f7(f20(x712,x711,x713)),f15(x712))
% 0.20/0.59 [74]~P4(x742,x744)+P5(f20(x741,x742,x743),x744)
% 0.20/0.59 [82]P4(x821,x822)+~P5(f20(x823,x821,x824),x822)
% 0.20/0.59 [68]~E(x682,x684)+P4(f6(x681,f5(x682,x683)),x684)
% 0.20/0.59 [70]~P4(x701,x704)+P4(f6(x701,f5(x702,x703)),x704)
% 0.20/0.59 [80]P4(x802,x804)+E(f18(f20(x801,x802,x803),x804),f20(x801,x802,a3))
% 0.20/0.59 [77]~P1(x772,x774)+E(f6(f4(x771,x772),f5(x773,x774)),f4(f6(x771,f5(x773,x774)),x772))
% 0.20/0.59 [78]~P9(x783,x784)+E(f4(f6(x781,f5(x782,x783)),x784),f6(f4(x781,x784),f5(x782,x784)))
% 0.20/0.59 [84]~P7(x841,x844,x845)+P7(f6(x841,f5(x842,x843)),x844,x845)
% 0.20/0.59 [92]~P9(x921,x922)+~P3(f20(x923,f6(x924,f5(x921,x922)),x925))
% 0.20/0.59 [63]P9(x632,x631)+~P1(x632,x631)+P1(x631,x632)
% 0.20/0.59 [64]~P1(x641,x643)+P1(x641,x642)+~P1(x643,x642)
% 0.20/0.59 [85]P4(x851,f15(x852))+E(x851,a1)+E(f8(f20(x852,x851,x853)),f20(x852,f4(x851,f15(x852)),a3))
% 0.20/0.59 [75]E(x751,x752)+P4(x753,x752)+~P4(f6(x753,f5(x751,x754)),x752)
% 0.20/0.59 [88]~P4(x882,x884)+~P9(x884,f16(x882,x884))+E(f18(f20(x881,x882,x883),x884),f20(f19(x881,x884),f17(x882,x884),a3))
% 0.20/0.59 [89]~P4(x893,x892)+~P1(f16(x893,x892),x892)+E(f20(f19(x891,x892),f17(x893,x892),x894),f18(f20(x891,x893,x894),x892))
% 0.20/0.59 [72]~P4(x723,x722)+E(x721,x722)+E(f16(f6(x723,f5(x721,x724)),x722),f16(x723,x722))
% 0.20/0.59 [79]~P4(x793,x792)+E(x791,x792)+E(f17(f6(x793,f5(x791,x794)),x792),f6(f17(x793,x792),f5(x791,x794)))
% 0.20/0.59 [73]~E(x733,x735)+~E(x732,x734)+P7(f6(x731,f5(x732,x733)),x734,x735)
% 0.20/0.59 [86]E(x861,x862)+P7(x863,x864,x862)+~P7(f6(x863,f5(x865,x861)),x864,x862)
% 0.20/0.59 [87]E(x871,x872)+P7(x873,x872,x874)+~P7(f6(x873,f5(x871,x875)),x872,x874)
% 0.20/0.59 [93]~P1(x934,x933)+~P3(f20(x931,x932,x935))+P3(f20(x931,f6(x932,f5(x933,x934)),x935))
% 0.20/0.59 [94]~P1(x944,x945)+P3(f20(x941,x942,x943))+~P3(f20(x941,f6(x942,f5(x945,x944)),x943))
% 0.20/0.59 [90]~P4(x901,f15(x902))+E(x901,a1)+~P9(f15(x902),f16(x901,f15(x902)))+E(f8(f20(x902,x901,x903)),f20(x902,f4(x901,f15(x902)),a3))
% 0.20/0.59 [91]~P4(x911,f15(x912))+E(x911,a1)+~P1(f16(x911,f15(x912)),f15(x912))+E(f20(x912,f4(x911,f15(x912)),x913),f8(f20(x912,x911,x913)))
% 0.20/0.59 %EqnAxiom
% 0.20/0.59 [1]E(x11,x11)
% 0.20/0.59 [2]E(x22,x21)+~E(x21,x22)
% 0.20/0.59 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 0.20/0.59 [4]~E(x41,x42)+E(f4(x41,x43),f4(x42,x43))
% 0.20/0.59 [5]~E(x51,x52)+E(f4(x53,x51),f4(x53,x52))
% 0.20/0.59 [6]~E(x61,x62)+E(f5(x61,x63),f5(x62,x63))
% 0.20/0.59 [7]~E(x71,x72)+E(f5(x73,x71),f5(x73,x72))
% 0.20/0.59 [8]~E(x81,x82)+E(f6(x81,x83),f6(x82,x83))
% 0.20/0.59 [9]~E(x91,x92)+E(f6(x93,x91),f6(x93,x92))
% 0.20/0.59 [10]~E(x101,x102)+E(f20(x101,x103,x104),f20(x102,x103,x104))
% 0.20/0.59 [11]~E(x111,x112)+E(f20(x113,x111,x114),f20(x113,x112,x114))
% 0.20/0.59 [12]~E(x121,x122)+E(f20(x123,x124,x121),f20(x123,x124,x122))
% 0.20/0.59 [13]~E(x131,x132)+E(f8(x131),f8(x132))
% 0.20/0.59 [14]~E(x141,x142)+E(f17(x141,x143),f17(x142,x143))
% 0.20/0.59 [15]~E(x151,x152)+E(f17(x153,x151),f17(x153,x152))
% 0.20/0.59 [16]~E(x161,x162)+E(f15(x161),f15(x162))
% 0.20/0.59 [17]~E(x171,x172)+E(f16(x171,x173),f16(x172,x173))
% 0.20/0.59 [18]~E(x181,x182)+E(f16(x183,x181),f16(x183,x182))
% 0.20/0.59 [19]~E(x191,x192)+E(f7(x191),f7(x192))
% 0.20/0.59 [20]~E(x201,x202)+E(f19(x201,x203),f19(x202,x203))
% 0.20/0.59 [21]~E(x211,x212)+E(f19(x213,x211),f19(x213,x212))
% 0.20/0.59 [22]~E(x221,x222)+E(f14(x221,x223),f14(x222,x223))
% 0.20/0.59 [23]~E(x231,x232)+E(f14(x233,x231),f14(x233,x232))
% 0.20/0.59 [24]~E(x241,x242)+E(f18(x241,x243),f18(x242,x243))
% 0.20/0.59 [25]~E(x251,x252)+E(f18(x253,x251),f18(x253,x252))
% 0.20/0.59 [26]~E(x261,x262)+E(f13(x261,x263),f13(x262,x263))
% 0.20/0.59 [27]~E(x271,x272)+E(f13(x273,x271),f13(x273,x272))
% 0.20/0.59 [28]P1(x282,x283)+~E(x281,x282)+~P1(x281,x283)
% 0.20/0.59 [29]P1(x293,x292)+~E(x291,x292)+~P1(x293,x291)
% 0.20/0.59 [30]~P3(x301)+P3(x302)+~E(x301,x302)
% 0.20/0.59 [31]P6(x312,x313)+~E(x311,x312)+~P6(x311,x313)
% 0.20/0.59 [32]P6(x323,x322)+~E(x321,x322)+~P6(x323,x321)
% 0.20/0.59 [33]~P2(x331)+P2(x332)+~E(x331,x332)
% 0.20/0.59 [34]P7(x342,x343,x344)+~E(x341,x342)+~P7(x341,x343,x344)
% 0.20/0.59 [35]P7(x353,x352,x354)+~E(x351,x352)+~P7(x353,x351,x354)
% 0.20/0.59 [36]P7(x363,x364,x362)+~E(x361,x362)+~P7(x363,x364,x361)
% 0.20/0.59 [37]P4(x372,x373)+~E(x371,x372)+~P4(x371,x373)
% 0.20/0.59 [38]P4(x383,x382)+~E(x381,x382)+~P4(x383,x381)
% 0.20/0.59 [39]~P8(x391)+P8(x392)+~E(x391,x392)
% 0.20/0.59 [40]P9(x402,x403)+~E(x401,x402)+~P9(x401,x403)
% 0.20/0.59 [41]P9(x413,x412)+~E(x411,x412)+~P9(x413,x411)
% 0.20/0.60 [42]P5(x422,x423)+~E(x421,x422)+~P5(x421,x423)
% 0.20/0.60 [43]P5(x433,x432)+~E(x431,x432)+~P5(x433,x431)
% 0.20/0.60
% 0.20/0.60 %-------------------------------------------
% 0.20/0.60 cnf(96,plain,
% 0.20/0.60 ($false),
% 0.20/0.60 inference(scs_inference,[],[57,52,83]),
% 0.20/0.60 ['proof']).
% 0.20/0.60 % SZS output end Proof
% 0.20/0.60 % Total time :0.000000s
%------------------------------------------------------------------------------