%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : HWV013-1 : TPTP v8.2.0. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n023.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:10 EDT 2024
% Result : Unsatisfiable 0.56s 0.64s
% Output : CNFRefutation 0.56s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13 % Problem : HWV013-1 : TPTP v8.2.0. Released v2.5.0.
% 0.08/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.13/0.34 % Computer : n023.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.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Fri Jun 21 03:56:09 EDT 2024
% 0.13/0.35 % CPUTime :
% 0.22/0.58 start to proof:theBenchmark
% 0.56/0.64 %-------------------------------------------
% 0.56/0.64 % File :CSE---1.7
% 0.56/0.64 % Problem :theBenchmark
% 0.56/0.64 % Transform :cnf
% 0.56/0.64 % Format :tptp:raw
% 0.56/0.64 % Command :java -jar mcs_scs.jar %d %s
% 0.56/0.64
% 0.56/0.64 % Result :Theorem 0.000000s
% 0.56/0.64 % Output :CNFRefutation 0.000000s
% 0.56/0.64 %-------------------------------------------
% 0.56/0.64 %--------------------------------------------------------------------------
% 0.56/0.64 % File : HWV013-1 : TPTP v8.2.0. Released v2.5.0.
% 0.56/0.64 % Domain : Hardware Verification
% 0.56/0.64 % Problem : Safelogic VHDL design verification obligation
% 0.56/0.64 % Version : [Mar02] axioms : Especial.
% 0.56/0.64 % English :
% 0.56/0.64
% 0.56/0.64 % Refs : [CHM02] Claessen et al. (2002), Verification of Hardware Systems
% 0.56/0.64 % : [Mar02] Martensson (2002), Email to G. Sutcliffe
% 0.56/0.64 % Source : [Mar02]
% 0.56/0.64 % Names :
% 0.56/0.64
% 0.56/0.64 % Status : Unsatisfiable
% 0.56/0.64 % Rating : 0.05 v8.1.0, 0.00 v7.0.0, 0.13 v6.3.0, 0.18 v6.2.0, 0.10 v6.1.0, 0.14 v6.0.0, 0.10 v5.5.0, 0.20 v5.3.0, 0.17 v5.2.0, 0.19 v5.1.0, 0.29 v5.0.0, 0.14 v4.1.0, 0.23 v4.0.1, 0.27 v4.0.0, 0.18 v3.7.0, 0.00 v3.3.0, 0.07 v3.2.0, 0.08 v3.1.0, 0.09 v2.7.0, 0.08 v2.6.0, 0.00 v2.5.0
% 0.56/0.64 % Syntax : Number of clauses : 95 ( 11 unt; 64 nHn; 86 RR)
% 0.56/0.64 % Number of literals : 374 ( 51 equ; 158 neg)
% 0.56/0.64 % Maximal clause size : 7 ( 3 avg)
% 0.56/0.64 % Maximal term depth : 3 ( 1 avg)
% 0.56/0.64 % Number of predicates : 13 ( 12 usr; 0 prp; 1-3 aty)
% 0.56/0.64 % Number of functors : 11 ( 11 usr; 4 con; 0-2 aty)
% 0.56/0.64 % Number of variables : 139 ( 5 sgn)
% 0.56/0.64 % SPC : CNF_UNS_RFO_SEQ_NHN
% 0.56/0.64
% 0.56/0.64 % Comments :
% 0.56/0.64 %--------------------------------------------------------------------------
% 0.56/0.64 %----Include equality
% 0.56/0.64 %----Include VHDL design axioms
% 0.56/0.64 include('Axioms/HWV003-0.ax').
% 0.56/0.64 %--------------------------------------------------------------------------
% 0.56/0.64 cnf(quest_1,negated_conjecture,
% 0.56/0.64 ~ p_Reset(x_139) ).
% 0.56/0.64
% 0.56/0.64 cnf(quest_2,negated_conjecture,
% 0.56/0.64 gt(fifo_length,level(x_139)) ).
% 0.56/0.64
% 0.56/0.64 cnf(quest_3,negated_conjecture,
% 0.56/0.64 ~ p_Rd(x_139) ).
% 0.56/0.64
% 0.56/0.64 cnf(quest_4,negated_conjecture,
% 0.56/0.64 p_Wr(x_139) ).
% 0.56/0.64
% 0.56/0.64 cnf(quest_5,negated_conjecture,
% 0.56/0.64 level(plus(x_139,n1)) != plus(level(x_139),n1) ).
% 0.56/0.64
% 0.56/0.64 %--------------------------------------------------------------------------
% 0.56/0.64 %-------------------------------------------
% 0.56/0.64 % Proof found
% 0.56/0.64 % SZS status Theorem for theBenchmark
% 0.56/0.64 % SZS output start Proof
% 0.56/0.65 %ClaNum:123(EqnAxiom:29)
% 0.56/0.65 %VarNum:496(SingletonVarNum:136)
% 0.56/0.65 %MaxLitNum:7
% 0.56/0.65 %MaxfuncDepth:2
% 0.56/0.65 %SharedTerms:16
% 0.56/0.65 %goalClause: 30 33 35 36 39
% 0.56/0.65 %singleGoalClaCount:5
% 0.56/0.65 [30]P1(a1)
% 0.56/0.65 [35]~P4(a1)
% 0.56/0.65 [36]~P5(a1)
% 0.56/0.65 [33]P2(a3,f4(a1))
% 0.56/0.65 [39]~E(f4(f7(a1,a6)),f7(f4(a1),a6))
% 0.56/0.65 [38]~P2(x381,x381)
% 0.56/0.65 [32]E(f7(a2,x321),x321)
% 0.56/0.65 [34]P2(f7(x341,a6),a2)
% 0.56/0.65 [37]~E(f7(x371,a6),a2)
% 0.56/0.65 [44]P2(x441,a2)+E(x441,a2)
% 0.56/0.65 [40]~P6(x401)+E(f4(x401),a2)
% 0.56/0.65 [41]~P9(x411)+E(f4(x411),a3)
% 0.56/0.65 [42]P9(x421)+~E(f4(x421),a3)
% 0.56/0.65 [43]P6(x431)+~E(f4(x431),a2)
% 0.56/0.65 [59]~P4(x591)+~P12(f7(x591,a6))
% 0.56/0.65 [60]~P4(x601)+~P11(f7(x601,a6))
% 0.56/0.65 [65]~P2(x651,a2)+P2(x651,f5(x651,a6))
% 0.56/0.65 [45]E(x451,a2)+E(f7(f10(x451),a6),x451)
% 0.56/0.65 [48]~P4(x481)+E(f4(f7(x481,a6)),a2)
% 0.56/0.65 [49]~P4(x491)+E(f8(f7(x491,a6)),a2)
% 0.56/0.65 [50]~P4(x501)+E(f9(f7(x501,a6)),a2)
% 0.56/0.65 [46]~P3(x461,x462)+~E(x461,x462)
% 0.56/0.65 [56]~P3(x562,x561)+~P2(x561,x562)
% 0.56/0.65 [52]E(x521,x522)+~E(f7(x521,a6),f7(x522,a6))
% 0.56/0.65 [73]~P4(x731)+~P7(x732,f7(x731,a6))
% 0.56/0.65 [85]~P2(x851,x852)+P2(f7(x851,a6),f7(x852,a6))
% 0.56/0.65 [98]P2(x981,x982)+~P2(f7(x981,a6),f7(x982,a6))
% 0.56/0.65 [105]~P4(x1051)+~P10(x1052,x1053,f7(x1051,a6))
% 0.56/0.65 [51]P4(x511)+P1(x511)+E(f8(f7(x511,a6)),f8(x511))
% 0.56/0.65 [47]P2(x472,x471)+P2(x471,x472)+E(x471,x472)
% 0.56/0.65 [79]~P2(x792,x791)+P2(x792,f7(x791,a6))+E(f7(x791,a6),x792)
% 0.56/0.65 [82]P2(x821,x822)+E(x821,x822)+~P2(f7(x821,a6),x822)
% 0.56/0.65 [66]~P2(x661,x663)+P2(x661,x662)+~P2(x663,x662)
% 0.56/0.65 [62]P3(x622,x623)+~E(f5(x623,x622),x621)+E(f7(x621,x622),x623)
% 0.56/0.65 [63]P3(x632,x631)+~E(f7(x633,x632),x631)+E(f5(x631,x632),x633)
% 0.56/0.65 [53]P1(x531)+~P12(x531)+P4(x531)+P12(f7(x531,a6))
% 0.56/0.65 [64]P12(x641)+P1(x641)+P4(x641)+~P12(f7(x641,a6))
% 0.56/0.65 [68]~P1(x681)+~P5(x681)+P4(x681)+~P12(f7(x681,a6))
% 0.56/0.65 [54]P4(x541)+P1(x541)+P5(x541)+E(f4(f7(x541,a6)),f4(x541))
% 0.56/0.65 [55]P4(x551)+P1(x551)+P5(x551)+E(f9(f7(x551,a6)),f9(x551))
% 0.56/0.65 [57]P4(x571)+P5(x571)+~P1(x571)+E(f9(f7(x571,a6)),f9(x571))
% 0.56/0.65 [113]P1(x1131)+~P10(x1132,x1133,x1131)+P4(x1131)+P10(x1132,x1133,f7(x1131,a6))
% 0.56/0.65 [116]P1(x1161)+P4(x1161)+P10(x1162,x1163,x1161)+~P10(x1162,x1163,f7(x1161,a6))
% 0.56/0.65 [58]P1(x581)+P5(x581)+~P11(x581)+P4(x581)+P11(f7(x581,a6))
% 0.56/0.65 [61]P5(x611)+~P11(x611)+~P1(x611)+P4(x611)+P11(f7(x611,a6))
% 0.56/0.65 [67]P11(x671)+P1(x671)+P5(x671)+P4(x671)+~P11(f7(x671,a6))
% 0.56/0.65 [69]P5(x691)+~P1(x691)+P4(x691)+P2(a3,f4(x691))+P12(f7(x691,a6))
% 0.56/0.65 [70]P1(x701)+~P5(x701)+P4(x701)+P2(f4(x701),a2)+P11(f7(x701,a6))
% 0.56/0.65 [71]P11(x711)+P5(x711)+~P1(x711)+P4(x711)+~P11(f7(x711,a6))
% 0.56/0.65 [72]~P1(x721)+~P5(x721)+P4(x721)+P2(f4(x721),a2)+P11(f7(x721,a6))
% 0.56/0.65 [89]P5(x891)+~P1(x891)+P4(x891)+~P2(a3,f4(x891))+~P12(f7(x891,a6))
% 0.56/0.65 [90]P1(x901)+~P5(x901)+P4(x901)+~P2(f4(x901),a2)+~P11(f7(x901,a6))
% 0.56/0.65 [94]~P1(x941)+~P5(x941)+P4(x941)+~P2(f4(x941),a2)+~P11(f7(x941,a6))
% 0.56/0.65 [74]P4(x741)+P5(x741)+~P1(x741)+P2(a3,f4(x741))+E(f4(f7(x741,a6)),f4(x741))
% 0.56/0.65 [75]P4(x751)+P5(x751)+~P1(x751)+P2(a3,f4(x751))+E(f8(f7(x751,a6)),f8(x751))
% 0.56/0.65 [76]P4(x761)+P1(x761)+~P5(x761)+P2(f4(x761),a2)+E(f4(f7(x761,a6)),f4(x761))
% 0.56/0.65 [77]P4(x771)+P1(x771)+~P5(x771)+P2(f4(x771),a2)+E(f9(f7(x771,a6)),f9(x771))
% 0.56/0.65 [78]P4(x781)+~P1(x781)+~P5(x781)+P2(f4(x781),a2)+E(f9(f7(x781,a6)),f9(x781))
% 0.56/0.65 [84]P4(x841)+~P1(x841)+~P5(x841)+~P2(f4(x841),a2)+E(f4(f7(x841,a6)),f4(x841))
% 0.56/0.65 [86]P4(x861)+~P1(x861)+~P5(x861)+P2(f4(x861),a2)+E(f4(f7(x861,a6)),f7(f4(x861),a6))
% 0.56/0.65 [87]P4(x871)+~P1(x871)+~P5(x871)+P2(f5(a3,a6),f8(x871))+E(f8(f7(x871,a6)),a2)
% 0.56/0.65 [92]P4(x921)+P5(x921)+~P1(x921)+~P2(a3,f4(x921))+E(f4(f7(x921,a6)),f7(f4(x921),a6))
% 0.56/0.65 [93]P4(x931)+P1(x931)+~P5(x931)+~P2(f4(x931),a2)+E(f4(f7(x931,a6)),f5(f4(x931),a6))
% 0.56/0.65 [104]P4(x1041)+~P1(x1041)+~P5(x1041)+~P2(f5(a3,a6),f8(x1041))+E(f8(f7(x1041,a6)),f7(f8(x1041),a6))
% 0.56/0.65 [80]P1(x801)+P5(x801)+~P7(x802,x801)+P4(x801)+P7(x802,f7(x801,a6))
% 0.56/0.65 [83]P5(x831)+~P1(x831)+~P7(x832,x831)+P4(x831)+P7(x832,f7(x831,a6))
% 0.56/0.65 [88]P1(x881)+P5(x881)+P4(x881)+P7(x882,x881)+~P7(x882,f7(x881,a6))
% 0.56/0.65 [91]P5(x911)+~P1(x911)+P4(x911)+P7(x912,x911)+~P7(x912,f7(x911,a6))
% 0.56/0.65 [103]~P1(x1031)+~P5(x1031)+~P8(x1032,x1031)+P4(x1031)+P10(f8(x1031),x1032,f7(x1031,a6))
% 0.56/0.65 [110]~P1(x1101)+~P5(x1101)+P4(x1101)+P8(x1102,x1101)+~P10(f8(x1101),x1102,f7(x1101,a6))
% 0.56/0.65 [100]P4(x1001)+P5(x1001)+~P1(x1001)+P2(f5(a3,a6),f8(x1001))+~P2(a3,f4(x1001))+E(f8(f7(x1001,a6)),a2)
% 0.56/0.65 [101]P4(x1011)+P1(x1011)+~P5(x1011)+P2(f5(a3,a6),f9(x1011))+~P2(f4(x1011),a2)+E(f9(f7(x1011,a6)),a2)
% 0.56/0.65 [102]P4(x1021)+~P1(x1021)+~P5(x1021)+P2(f5(a3,a6),f9(x1021))+~P2(f4(x1021),a2)+E(f9(f7(x1021,a6)),a2)
% 0.56/0.65 [107]P4(x1071)+P5(x1071)+~P1(x1071)+~P2(f5(a3,a6),f8(x1071))+~P2(a3,f4(x1071))+E(f8(f7(x1071,a6)),f7(f8(x1071),a6))
% 0.56/0.65 [108]P4(x1081)+P1(x1081)+~P5(x1081)+~P2(f5(a3,a6),f9(x1081))+~P2(f4(x1081),a2)+E(f9(f7(x1081,a6)),f7(f9(x1081),a6))
% 0.56/0.65 [109]P4(x1091)+~P1(x1091)+~P5(x1091)+~P2(f5(a3,a6),f9(x1091))+~P2(f4(x1091),a2)+E(f9(f7(x1091,a6)),f7(f9(x1091),a6))
% 0.56/0.65 [95]P1(x951)+~P5(x951)+~P7(x952,x951)+P4(x951)+P7(x952,f7(x951,a6))+P2(f4(x951),a2)
% 0.56/0.65 [96]~P1(x961)+~P5(x961)+~P7(x962,x961)+P4(x961)+P7(x962,f7(x961,a6))+P2(f4(x961),a2)
% 0.56/0.65 [97]P1(x971)+~P5(x971)+P4(x971)+P7(x972,x971)+~P7(x972,f7(x971,a6))+P2(f4(x971),a2)
% 0.56/0.65 [99]~P1(x991)+~P5(x991)+P4(x991)+P7(x992,x991)+~P7(x992,f7(x991,a6))+P2(f4(x991),a2)
% 0.56/0.65 [106]P5(x1061)+~P1(x1061)+~P8(x1062,x1061)+P4(x1061)+P10(f8(x1061),x1062,f7(x1061,a6))+~P2(a3,f4(x1061))
% 0.56/0.65 [111]P1(x1111)+~P5(x1111)+P4(x1111)+P10(f9(x1111),x1112,x1111)+~P7(x1112,f7(x1111,a6))+~P2(f4(x1111),a2)
% 0.56/0.65 [112]~P1(x1121)+~P5(x1121)+P4(x1121)+P10(f9(x1121),x1122,x1121)+~P7(x1122,f7(x1121,a6))+~P2(f4(x1121),a2)
% 0.56/0.65 [114]P1(x1141)+~P5(x1141)+P4(x1141)+~P10(f9(x1141),x1142,x1141)+P7(x1142,f7(x1141,a6))+~P2(f4(x1141),a2)
% 0.56/0.65 [115]~P1(x1151)+~P5(x1151)+P4(x1151)+~P10(f9(x1151),x1152,x1151)+P7(x1152,f7(x1151,a6))+~P2(f4(x1151),a2)
% 0.56/0.65 [118]P5(x1181)+~P1(x1181)+P4(x1181)+P8(x1182,x1181)+~P10(f8(x1181),x1182,f7(x1181,a6))+~P2(a3,f4(x1181))
% 0.56/0.65 [117]P4(x1172)+~P1(x1172)+~P5(x1172)+~P10(x1171,x1173,x1172)+P10(x1171,x1173,f7(x1172,a6))+E(x1171,f8(x1172))
% 0.56/0.65 [119]P5(x1191)+~P1(x1191)+~P10(x1192,x1193,x1191)+P4(x1191)+P10(x1192,x1193,f7(x1191,a6))+P2(a3,f4(x1191))
% 0.56/0.65 [120]P4(x1202)+~P1(x1202)+~P5(x1202)+P10(x1201,x1203,x1202)+~P10(x1201,x1203,f7(x1202,a6))+E(x1201,f8(x1202))
% 0.56/0.65 [121]P5(x1211)+~P1(x1211)+P4(x1211)+P10(x1212,x1213,x1211)+~P10(x1212,x1213,f7(x1211,a6))+P2(a3,f4(x1211))
% 0.56/0.65 [122]P4(x1222)+P5(x1222)+~P1(x1222)+~P10(x1221,x1223,x1222)+P10(x1221,x1223,f7(x1222,a6))+E(x1221,f8(x1222))+~P2(a3,f4(x1222))
% 0.56/0.65 [123]P4(x1232)+P5(x1232)+~P1(x1232)+P10(x1231,x1233,x1232)+~P10(x1231,x1233,f7(x1232,a6))+E(x1231,f8(x1232))+~P2(a3,f4(x1232))
% 0.56/0.65 %EqnAxiom
% 0.56/0.65 [1]E(x11,x11)
% 0.56/0.65 [2]E(x22,x21)+~E(x21,x22)
% 0.56/0.65 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 0.56/0.65 [4]~E(x41,x42)+E(f7(x41,x43),f7(x42,x43))
% 0.56/0.65 [5]~E(x51,x52)+E(f7(x53,x51),f7(x53,x52))
% 0.56/0.65 [6]~E(x61,x62)+E(f4(x61),f4(x62))
% 0.56/0.65 [7]~E(x71,x72)+E(f5(x71,x73),f5(x72,x73))
% 0.56/0.65 [8]~E(x81,x82)+E(f5(x83,x81),f5(x83,x82))
% 0.56/0.65 [9]~E(x91,x92)+E(f8(x91),f8(x92))
% 0.56/0.65 [10]~E(x101,x102)+E(f9(x101),f9(x102))
% 0.56/0.65 [11]~E(x111,x112)+E(f10(x111),f10(x112))
% 0.56/0.65 [12]~P1(x121)+P1(x122)+~E(x121,x122)
% 0.56/0.65 [13]P2(x132,x133)+~E(x131,x132)+~P2(x131,x133)
% 0.56/0.65 [14]P2(x143,x142)+~E(x141,x142)+~P2(x143,x141)
% 0.56/0.65 [15]P10(x152,x153,x154)+~E(x151,x152)+~P10(x151,x153,x154)
% 0.56/0.65 [16]P10(x163,x162,x164)+~E(x161,x162)+~P10(x163,x161,x164)
% 0.56/0.65 [17]P10(x173,x174,x172)+~E(x171,x172)+~P10(x173,x174,x171)
% 0.56/0.65 [18]~P4(x181)+P4(x182)+~E(x181,x182)
% 0.56/0.65 [19]~P5(x191)+P5(x192)+~E(x191,x192)
% 0.56/0.65 [20]P7(x202,x203)+~E(x201,x202)+~P7(x201,x203)
% 0.56/0.65 [21]P7(x213,x212)+~E(x211,x212)+~P7(x213,x211)
% 0.56/0.65 [22]~P6(x221)+P6(x222)+~E(x221,x222)
% 0.56/0.65 [23]~P9(x231)+P9(x232)+~E(x231,x232)
% 0.56/0.65 [24]~P11(x241)+P11(x242)+~E(x241,x242)
% 0.56/0.65 [25]~P12(x251)+P12(x252)+~E(x251,x252)
% 0.56/0.65 [26]P8(x262,x263)+~E(x261,x262)+~P8(x261,x263)
% 0.56/0.65 [27]P8(x273,x272)+~E(x271,x272)+~P8(x273,x271)
% 0.56/0.65 [28]P3(x282,x283)+~E(x281,x282)+~P3(x281,x283)
% 0.56/0.65 [29]P3(x293,x292)+~E(x291,x292)+~P3(x293,x291)
% 0.56/0.65
% 0.56/0.65 %-------------------------------------------
% 0.56/0.65 cnf(128,plain,
% 0.56/0.65 ($false),
% 0.56/0.65 inference(scs_inference,[],[35,36,30,33,39,92]),
% 0.56/0.65 ['proof']).
% 0.56/0.65 % SZS output end Proof
% 0.56/0.65 % Total time :0.000000s
%------------------------------------------------------------------------------