%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : HWV032-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 : 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 07:29:17 EDT 2024
% Result : Unsatisfiable 0.59s 0.64s
% Output : CNFRefutation 0.59s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : HWV032-1 : TPTP v8.2.0. Released v2.5.0.
% 0.07/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.13/0.34 % Computer : n019.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.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Fri Jun 21 04:04:54 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.21/0.57 start to proof:theBenchmark
% 0.58/0.63 %-------------------------------------------
% 0.58/0.63 % File :CSE---1.7
% 0.58/0.63 % Problem :theBenchmark
% 0.58/0.63 % Transform :cnf
% 0.58/0.63 % Format :tptp:raw
% 0.58/0.63 % Command :java -jar mcs_scs.jar %d %s
% 0.58/0.63
% 0.58/0.63 % Result :Theorem 0.010000s
% 0.58/0.64 % Output :CNFRefutation 0.010000s
% 0.58/0.64 %-------------------------------------------
% 0.58/0.64 %--------------------------------------------------------------------------
% 0.58/0.64 % File : HWV032-1 : TPTP v8.2.0. Released v2.5.0.
% 0.58/0.64 % Domain : Hardware Verification
% 0.58/0.64 % Problem : Safelogic VHDL design verification obligation
% 0.58/0.64 % Version : [Mar02] axioms : Especial.
% 0.59/0.64 % English :
% 0.59/0.64
% 0.59/0.64 % Refs : [CHM02] Claessen et al. (2002), Verification of Hardware Systems
% 0.59/0.64 % : [Mar02] Martensson (2002), Email to G. Sutcliffe
% 0.59/0.64 % Source : [Mar02]
% 0.59/0.64 % Names :
% 0.59/0.64
% 0.59/0.64 % Status : Unsatisfiable
% 0.59/0.64 % Rating : 0.05 v8.1.0, 0.00 v7.5.0, 0.05 v7.4.0, 0.06 v7.3.0, 0.08 v7.1.0, 0.00 v7.0.0, 0.07 v6.4.0, 0.00 v6.1.0, 0.07 v6.0.0, 0.00 v5.5.0, 0.15 v5.3.0, 0.06 v5.0.0, 0.00 v4.1.0, 0.08 v4.0.1, 0.09 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.59/0.64 % Syntax : Number of clauses : 93 ( 9 unt; 64 nHn; 84 RR)
% 0.59/0.64 % Number of literals : 372 ( 50 equ; 156 neg)
% 0.59/0.64 % Maximal clause size : 7 ( 4 avg)
% 0.59/0.64 % Maximal term depth : 3 ( 1 avg)
% 0.59/0.64 % Number of predicates : 13 ( 12 usr; 0 prp; 1-3 aty)
% 0.59/0.64 % Number of functors : 11 ( 11 usr; 4 con; 0-2 aty)
% 0.59/0.64 % Number of variables : 139 ( 5 sgn)
% 0.59/0.64 % SPC : CNF_UNS_RFO_SEQ_NHN
% 0.59/0.64
% 0.59/0.64 % Comments :
% 0.59/0.64 %--------------------------------------------------------------------------
% 0.59/0.64 %----Include equality
% 0.59/0.64 %----Include VHDL design axioms
% 0.59/0.64 include('Axioms/HWV003-0.ax').
% 0.59/0.64 %--------------------------------------------------------------------------
% 0.59/0.64 cnf(quest_1,negated_conjecture,
% 0.59/0.64 p_Reset(t_139) ).
% 0.59/0.64
% 0.59/0.64 cnf(quest_2,negated_conjecture,
% 0.59/0.64 ~ gt(fifo_length,rd_level(plus(t_139,n1))) ).
% 0.59/0.64
% 0.59/0.64 cnf(quest_3,negated_conjecture,
% 0.59/0.64 gt(fifo_length,n0) ).
% 0.59/0.64
% 0.59/0.64 %--------------------------------------------------------------------------
% 0.59/0.64 %-------------------------------------------
% 0.59/0.64 % Proof found
% 0.59/0.64 % SZS status Theorem for theBenchmark
% 0.59/0.64 % SZS output start Proof
% 0.59/0.64 %ClaNum:121(EqnAxiom:29)
% 0.59/0.64 %VarNum:496(SingletonVarNum:136)
% 0.59/0.64 %MaxLitNum:7
% 0.59/0.64 %MaxfuncDepth:2
% 0.59/0.64 %SharedTerms:12
% 0.59/0.64 %goalClause: 30 32 37
% 0.59/0.64 %singleGoalClaCount:3
% 0.59/0.64 [30]P1(a1)
% 0.59/0.64 [32]P2(a3,a2)
% 0.59/0.64 [37]~P2(a3,f8(f7(a1,a6)))
% 0.59/0.64 [36]~P2(x361,x361)
% 0.59/0.64 [33]E(f7(a2,x331),x331)
% 0.59/0.64 [34]P2(f7(x341,a6),a2)
% 0.59/0.64 [35]~E(f7(x351,a6),a2)
% 0.59/0.64 [42]P2(x421,a2)+E(x421,a2)
% 0.59/0.64 [38]~P4(x381)+E(f4(x381),a2)
% 0.59/0.64 [39]~P7(x391)+E(f4(x391),a3)
% 0.59/0.64 [40]P7(x401)+~E(f4(x401),a3)
% 0.59/0.64 [41]P4(x411)+~E(f4(x411),a2)
% 0.59/0.64 [57]~P1(x571)+~P12(f7(x571,a6))
% 0.59/0.64 [58]~P1(x581)+~P10(f7(x581,a6))
% 0.59/0.64 [63]~P2(x631,a2)+P2(x631,f5(x631,a6))
% 0.59/0.64 [43]E(x431,a2)+E(f7(f9(x431),a6),x431)
% 0.59/0.64 [46]~P1(x461)+E(f4(f7(x461,a6)),a2)
% 0.59/0.64 [47]~P1(x471)+E(f10(f7(x471,a6)),a2)
% 0.59/0.64 [48]~P1(x481)+E(f8(f7(x481,a6)),a2)
% 0.59/0.64 [44]~P3(x441,x442)+~E(x441,x442)
% 0.59/0.64 [54]~P3(x542,x541)+~P2(x541,x542)
% 0.59/0.64 [50]E(x501,x502)+~E(f7(x501,a6),f7(x502,a6))
% 0.59/0.64 [71]~P1(x711)+~P5(x712,f7(x711,a6))
% 0.59/0.64 [83]~P2(x831,x832)+P2(f7(x831,a6),f7(x832,a6))
% 0.59/0.64 [96]P2(x961,x962)+~P2(f7(x961,a6),f7(x962,a6))
% 0.59/0.64 [103]~P1(x1031)+~P9(x1032,x1033,f7(x1031,a6))
% 0.59/0.64 [49]P1(x491)+P11(x491)+E(f10(f7(x491,a6)),f10(x491))
% 0.59/0.64 [45]P2(x452,x451)+P2(x451,x452)+E(x451,x452)
% 0.59/0.64 [77]~P2(x772,x771)+P2(x772,f7(x771,a6))+E(f7(x771,a6),x772)
% 0.59/0.64 [80]P2(x801,x802)+E(x801,x802)+~P2(f7(x801,a6),x802)
% 0.59/0.64 [64]~P2(x641,x643)+P2(x641,x642)+~P2(x643,x642)
% 0.59/0.64 [60]P3(x602,x603)+~E(f5(x603,x602),x601)+E(f7(x601,x602),x603)
% 0.59/0.64 [61]P3(x612,x611)+~E(f7(x613,x612),x611)+E(f5(x611,x612),x613)
% 0.59/0.64 [51]P11(x511)+~P12(x511)+P1(x511)+P12(f7(x511,a6))
% 0.59/0.64 [62]P12(x621)+P11(x621)+P1(x621)+~P12(f7(x621,a6))
% 0.59/0.64 [66]~P11(x661)+~P8(x661)+P1(x661)+~P12(f7(x661,a6))
% 0.59/0.64 [52]P1(x521)+P11(x521)+P8(x521)+E(f4(f7(x521,a6)),f4(x521))
% 0.59/0.64 [53]P1(x531)+P11(x531)+P8(x531)+E(f8(f7(x531,a6)),f8(x531))
% 0.59/0.64 [55]P1(x551)+P8(x551)+~P11(x551)+E(f8(f7(x551,a6)),f8(x551))
% 0.59/0.64 [111]P11(x1111)+~P9(x1112,x1113,x1111)+P1(x1111)+P9(x1112,x1113,f7(x1111,a6))
% 0.59/0.64 [114]P11(x1141)+P1(x1141)+P9(x1142,x1143,x1141)+~P9(x1142,x1143,f7(x1141,a6))
% 0.59/0.64 [56]P11(x561)+P8(x561)+~P10(x561)+P1(x561)+P10(f7(x561,a6))
% 0.59/0.64 [59]P8(x591)+~P10(x591)+~P11(x591)+P1(x591)+P10(f7(x591,a6))
% 0.59/0.64 [65]P10(x651)+P11(x651)+P8(x651)+P1(x651)+~P10(f7(x651,a6))
% 0.59/0.64 [67]P8(x671)+~P11(x671)+P1(x671)+P2(a3,f4(x671))+P12(f7(x671,a6))
% 0.59/0.64 [68]P11(x681)+~P8(x681)+P1(x681)+P2(f4(x681),a2)+P10(f7(x681,a6))
% 0.59/0.64 [69]P10(x691)+P8(x691)+~P11(x691)+P1(x691)+~P10(f7(x691,a6))
% 0.59/0.64 [70]~P11(x701)+~P8(x701)+P1(x701)+P2(f4(x701),a2)+P10(f7(x701,a6))
% 0.59/0.64 [87]P8(x871)+~P11(x871)+P1(x871)+~P2(a3,f4(x871))+~P12(f7(x871,a6))
% 0.59/0.65 [88]P11(x881)+~P8(x881)+P1(x881)+~P2(f4(x881),a2)+~P10(f7(x881,a6))
% 0.59/0.65 [92]~P11(x921)+~P8(x921)+P1(x921)+~P2(f4(x921),a2)+~P10(f7(x921,a6))
% 0.59/0.65 [72]P1(x721)+P8(x721)+~P11(x721)+P2(a3,f4(x721))+E(f4(f7(x721,a6)),f4(x721))
% 0.59/0.65 [73]P1(x731)+P8(x731)+~P11(x731)+P2(a3,f4(x731))+E(f10(f7(x731,a6)),f10(x731))
% 0.59/0.65 [74]P1(x741)+P11(x741)+~P8(x741)+P2(f4(x741),a2)+E(f4(f7(x741,a6)),f4(x741))
% 0.59/0.65 [75]P1(x751)+P11(x751)+~P8(x751)+P2(f4(x751),a2)+E(f8(f7(x751,a6)),f8(x751))
% 0.59/0.65 [76]P1(x761)+~P11(x761)+~P8(x761)+P2(f4(x761),a2)+E(f8(f7(x761,a6)),f8(x761))
% 0.59/0.65 [82]P1(x821)+~P11(x821)+~P8(x821)+~P2(f4(x821),a2)+E(f4(f7(x821,a6)),f4(x821))
% 0.59/0.65 [84]P1(x841)+~P11(x841)+~P8(x841)+P2(f4(x841),a2)+E(f4(f7(x841,a6)),f7(f4(x841),a6))
% 0.59/0.65 [85]P1(x851)+~P11(x851)+~P8(x851)+P2(f5(a3,a6),f10(x851))+E(f10(f7(x851,a6)),a2)
% 0.59/0.65 [90]P1(x901)+P8(x901)+~P11(x901)+~P2(a3,f4(x901))+E(f4(f7(x901,a6)),f7(f4(x901),a6))
% 0.59/0.65 [91]P1(x911)+P11(x911)+~P8(x911)+~P2(f4(x911),a2)+E(f4(f7(x911,a6)),f5(f4(x911),a6))
% 0.59/0.65 [102]P1(x1021)+~P11(x1021)+~P8(x1021)+~P2(f5(a3,a6),f10(x1021))+E(f10(f7(x1021,a6)),f7(f10(x1021),a6))
% 0.59/0.65 [78]P11(x781)+P8(x781)+~P5(x782,x781)+P1(x781)+P5(x782,f7(x781,a6))
% 0.59/0.65 [81]P8(x811)+~P11(x811)+~P5(x812,x811)+P1(x811)+P5(x812,f7(x811,a6))
% 0.59/0.65 [86]P11(x861)+P8(x861)+P1(x861)+P5(x862,x861)+~P5(x862,f7(x861,a6))
% 0.59/0.65 [89]P8(x891)+~P11(x891)+P1(x891)+P5(x892,x891)+~P5(x892,f7(x891,a6))
% 0.59/0.65 [101]~P11(x1011)+~P8(x1011)+~P6(x1012,x1011)+P1(x1011)+P9(f10(x1011),x1012,f7(x1011,a6))
% 0.59/0.65 [108]~P11(x1081)+~P8(x1081)+P1(x1081)+P6(x1082,x1081)+~P9(f10(x1081),x1082,f7(x1081,a6))
% 0.59/0.65 [98]P1(x981)+P8(x981)+~P11(x981)+P2(f5(a3,a6),f10(x981))+~P2(a3,f4(x981))+E(f10(f7(x981,a6)),a2)
% 0.59/0.65 [99]P1(x991)+P11(x991)+~P8(x991)+P2(f5(a3,a6),f8(x991))+~P2(f4(x991),a2)+E(f8(f7(x991,a6)),a2)
% 0.59/0.65 [100]P1(x1001)+~P11(x1001)+~P8(x1001)+P2(f5(a3,a6),f8(x1001))+~P2(f4(x1001),a2)+E(f8(f7(x1001,a6)),a2)
% 0.59/0.65 [105]P1(x1051)+P8(x1051)+~P11(x1051)+~P2(f5(a3,a6),f10(x1051))+~P2(a3,f4(x1051))+E(f10(f7(x1051,a6)),f7(f10(x1051),a6))
% 0.59/0.65 [106]P1(x1061)+P11(x1061)+~P8(x1061)+~P2(f5(a3,a6),f8(x1061))+~P2(f4(x1061),a2)+E(f8(f7(x1061,a6)),f7(f8(x1061),a6))
% 0.59/0.65 [107]P1(x1071)+~P11(x1071)+~P8(x1071)+~P2(f5(a3,a6),f8(x1071))+~P2(f4(x1071),a2)+E(f8(f7(x1071,a6)),f7(f8(x1071),a6))
% 0.59/0.65 [93]P11(x931)+~P8(x931)+~P5(x932,x931)+P1(x931)+P5(x932,f7(x931,a6))+P2(f4(x931),a2)
% 0.59/0.65 [94]~P11(x941)+~P8(x941)+~P5(x942,x941)+P1(x941)+P5(x942,f7(x941,a6))+P2(f4(x941),a2)
% 0.59/0.65 [95]P11(x951)+~P8(x951)+P1(x951)+P5(x952,x951)+~P5(x952,f7(x951,a6))+P2(f4(x951),a2)
% 0.59/0.65 [97]~P11(x971)+~P8(x971)+P1(x971)+P5(x972,x971)+~P5(x972,f7(x971,a6))+P2(f4(x971),a2)
% 0.59/0.65 [104]P8(x1041)+~P11(x1041)+~P6(x1042,x1041)+P1(x1041)+P9(f10(x1041),x1042,f7(x1041,a6))+~P2(a3,f4(x1041))
% 0.59/0.65 [109]P11(x1091)+~P8(x1091)+P1(x1091)+P9(f8(x1091),x1092,x1091)+~P5(x1092,f7(x1091,a6))+~P2(f4(x1091),a2)
% 0.59/0.65 [110]~P11(x1101)+~P8(x1101)+P1(x1101)+P9(f8(x1101),x1102,x1101)+~P5(x1102,f7(x1101,a6))+~P2(f4(x1101),a2)
% 0.59/0.65 [112]P11(x1121)+~P8(x1121)+P1(x1121)+~P9(f8(x1121),x1122,x1121)+P5(x1122,f7(x1121,a6))+~P2(f4(x1121),a2)
% 0.59/0.65 [113]~P11(x1131)+~P8(x1131)+P1(x1131)+~P9(f8(x1131),x1132,x1131)+P5(x1132,f7(x1131,a6))+~P2(f4(x1131),a2)
% 0.59/0.65 [116]P8(x1161)+~P11(x1161)+P1(x1161)+P6(x1162,x1161)+~P9(f10(x1161),x1162,f7(x1161,a6))+~P2(a3,f4(x1161))
% 0.59/0.65 [115]P1(x1152)+~P11(x1152)+~P8(x1152)+~P9(x1151,x1153,x1152)+P9(x1151,x1153,f7(x1152,a6))+E(x1151,f10(x1152))
% 0.59/0.65 [117]P8(x1171)+~P11(x1171)+~P9(x1172,x1173,x1171)+P1(x1171)+P9(x1172,x1173,f7(x1171,a6))+P2(a3,f4(x1171))
% 0.59/0.65 [118]P1(x1182)+~P11(x1182)+~P8(x1182)+P9(x1181,x1183,x1182)+~P9(x1181,x1183,f7(x1182,a6))+E(x1181,f10(x1182))
% 0.59/0.65 [119]P8(x1191)+~P11(x1191)+P1(x1191)+P9(x1192,x1193,x1191)+~P9(x1192,x1193,f7(x1191,a6))+P2(a3,f4(x1191))
% 0.59/0.65 [120]P1(x1202)+P8(x1202)+~P11(x1202)+~P9(x1201,x1203,x1202)+P9(x1201,x1203,f7(x1202,a6))+E(x1201,f10(x1202))+~P2(a3,f4(x1202))
% 0.59/0.65 [121]P1(x1212)+P8(x1212)+~P11(x1212)+P9(x1211,x1213,x1212)+~P9(x1211,x1213,f7(x1212,a6))+E(x1211,f10(x1212))+~P2(a3,f4(x1212))
% 0.59/0.65 %EqnAxiom
% 0.59/0.65 [1]E(x11,x11)
% 0.59/0.65 [2]E(x22,x21)+~E(x21,x22)
% 0.59/0.65 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 0.59/0.65 [4]~E(x41,x42)+E(f7(x41,x43),f7(x42,x43))
% 0.59/0.65 [5]~E(x51,x52)+E(f7(x53,x51),f7(x53,x52))
% 0.59/0.65 [6]~E(x61,x62)+E(f4(x61),f4(x62))
% 0.59/0.65 [7]~E(x71,x72)+E(f10(x71),f10(x72))
% 0.59/0.65 [8]~E(x81,x82)+E(f5(x81,x83),f5(x82,x83))
% 0.59/0.65 [9]~E(x91,x92)+E(f5(x93,x91),f5(x93,x92))
% 0.59/0.65 [10]~E(x101,x102)+E(f8(x101),f8(x102))
% 0.59/0.65 [11]~E(x111,x112)+E(f9(x111),f9(x112))
% 0.59/0.65 [12]~P1(x121)+P1(x122)+~E(x121,x122)
% 0.59/0.65 [13]P2(x132,x133)+~E(x131,x132)+~P2(x131,x133)
% 0.59/0.65 [14]P2(x143,x142)+~E(x141,x142)+~P2(x143,x141)
% 0.59/0.65 [15]P9(x152,x153,x154)+~E(x151,x152)+~P9(x151,x153,x154)
% 0.59/0.65 [16]P9(x163,x162,x164)+~E(x161,x162)+~P9(x163,x161,x164)
% 0.59/0.65 [17]P9(x173,x174,x172)+~E(x171,x172)+~P9(x173,x174,x171)
% 0.59/0.65 [18]P5(x182,x183)+~E(x181,x182)+~P5(x181,x183)
% 0.59/0.65 [19]P5(x193,x192)+~E(x191,x192)+~P5(x193,x191)
% 0.59/0.65 [20]~P8(x201)+P8(x202)+~E(x201,x202)
% 0.59/0.65 [21]~P4(x211)+P4(x212)+~E(x211,x212)
% 0.59/0.65 [22]~P7(x221)+P7(x222)+~E(x221,x222)
% 0.59/0.65 [23]~P11(x231)+P11(x232)+~E(x231,x232)
% 0.59/0.65 [24]P6(x242,x243)+~E(x241,x242)+~P6(x241,x243)
% 0.59/0.65 [25]P6(x253,x252)+~E(x251,x252)+~P6(x253,x251)
% 0.59/0.65 [26]~P10(x261)+P10(x262)+~E(x261,x262)
% 0.59/0.65 [27]P3(x272,x273)+~E(x271,x272)+~P3(x271,x273)
% 0.59/0.65 [28]P3(x283,x282)+~E(x281,x282)+~P3(x283,x281)
% 0.59/0.65 [29]~P12(x291)+P12(x292)+~E(x291,x292)
% 0.59/0.65
% 0.59/0.65 %-------------------------------------------
% 0.59/0.65 cnf(124,plain,
% 0.59/0.65 (P3(x1241,x1242)+E(f7(f5(x1242,x1241),x1241),x1242)),
% 0.59/0.65 inference(equality_inference,[],[60])).
% 0.59/0.65 cnf(128,plain,
% 0.59/0.65 (~P3(f7(a2,x1281),x1281)),
% 0.59/0.65 inference(scs_inference,[],[32,33,54,44])).
% 0.59/0.65 cnf(130,plain,
% 0.59/0.65 (P3(a6,a2)),
% 0.59/0.65 inference(scs_inference,[],[32,33,35,54,44,124])).
% 0.59/0.65 cnf(133,plain,
% 0.59/0.65 (E(x1331,f7(a2,x1331))),
% 0.59/0.65 inference(scs_inference,[],[32,33,35,54,44,124,2])).
% 0.59/0.65 cnf(135,plain,
% 0.59/0.65 (~P2(x1351,x1351)),
% 0.59/0.65 inference(rename_variables,[],[36])).
% 0.59/0.65 cnf(140,plain,
% 0.59/0.65 (~E(a2,f8(f7(a1,a6)))),
% 0.59/0.65 inference(scs_inference,[],[30,32,37,36,135,33,35,54,44,124,2,64,12,13,14])).
% 0.59/0.65 cnf(159,plain,
% 0.59/0.65 (~P2(x1591,x1591)),
% 0.59/0.65 inference(rename_variables,[],[36])).
% 0.59/0.65 cnf(162,plain,
% 0.59/0.65 (~P2(x1621,x1621)),
% 0.59/0.65 inference(rename_variables,[],[36])).
% 0.59/0.65 cnf(172,plain,
% 0.59/0.65 (~E(f8(f7(a1,a6)),a2)),
% 0.59/0.65 inference(scs_inference,[],[140,34,128,133,130,36,159,162,35,33,44,54,64,14,3,27,77,26,45,13])).
% 0.59/0.65 cnf(180,plain,
% 0.59/0.65 ($false),
% 0.59/0.65 inference(scs_inference,[],[30,172,48]),
% 0.59/0.65 ['proof']).
% 0.59/0.65 % SZS output end Proof
% 0.59/0.65 % Total time :0.010000s
%------------------------------------------------------------------------------