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