%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : HWV021-1 : TPTP v8.2.0. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n024.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:13 EDT 2024
% Result : Unsatisfiable 1.29s 1.36s
% Output : CNFRefutation 1.29s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : HWV021-1 : TPTP v8.2.0. Released v2.5.0.
% 0.07/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.13/0.34 % Computer : n024.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 03:46:09 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.20/0.57 start to proof:theBenchmark
% 1.29/1.35 %-------------------------------------------
% 1.29/1.35 % File :CSE---1.7
% 1.29/1.35 % Problem :theBenchmark
% 1.29/1.35 % Transform :cnf
% 1.29/1.35 % Format :tptp:raw
% 1.29/1.35 % Command :java -jar mcs_scs.jar %d %s
% 1.29/1.35
% 1.29/1.35 % Result :Theorem 0.730000s
% 1.29/1.35 % Output :CNFRefutation 0.730000s
% 1.29/1.35 %-------------------------------------------
% 1.29/1.36 %--------------------------------------------------------------------------
% 1.29/1.36 % File : HWV021-1 : TPTP v8.2.0. Released v2.5.0.
% 1.29/1.36 % Domain : Hardware Verification
% 1.29/1.36 % Problem : Safelogic VHDL design verification obligation
% 1.29/1.36 % Version : [Mar02] axioms : Especial.
% 1.29/1.36 % English :
% 1.29/1.36
% 1.29/1.36 % Refs : [CHM02] Claessen et al. (2002), Verification of Hardware Systems
% 1.29/1.36 % : [Mar02] Martensson (2002), Email to G. Sutcliffe
% 1.29/1.36 % Source : [Mar02]
% 1.29/1.36 % Names :
% 1.29/1.36
% 1.29/1.36 % Status : Unsatisfiable
% 1.29/1.36 % 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.20 v5.3.0, 0.17 v5.2.0, 0.12 v5.1.0, 0.18 v5.0.0, 0.14 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.17 v2.6.0, 0.12 v2.5.0
% 1.29/1.36 % Syntax : Number of clauses : 94 ( 10 unt; 64 nHn; 85 RR)
% 1.29/1.36 % Number of literals : 373 ( 50 equ; 157 neg)
% 1.29/1.36 % Maximal clause size : 7 ( 3 avg)
% 1.29/1.36 % Maximal term depth : 3 ( 1 avg)
% 1.29/1.36 % Number of predicates : 13 ( 12 usr; 0 prp; 1-3 aty)
% 1.29/1.36 % Number of functors : 11 ( 11 usr; 4 con; 0-2 aty)
% 1.29/1.36 % Number of variables : 139 ( 5 sgn)
% 1.29/1.36 % SPC : CNF_UNS_RFO_SEQ_NHN
% 1.29/1.36
% 1.29/1.36 % Comments :
% 1.29/1.36 %--------------------------------------------------------------------------
% 1.29/1.36 %----Include equality
% 1.29/1.36 %----Include VHDL design axioms
% 1.29/1.36 include('Axioms/HWV003-0.ax').
% 1.29/1.36 %--------------------------------------------------------------------------
% 1.29/1.36 cnf(quest_1,negated_conjecture,
% 1.29/1.36 p_Rd_error(plus(t_139,n1)) ).
% 1.29/1.36
% 1.29/1.36 cnf(quest_2,negated_conjecture,
% 1.29/1.36 p_Rd(t_139) ).
% 1.29/1.36
% 1.29/1.36 cnf(quest_3,negated_conjecture,
% 1.29/1.36 ~ p_Reset(t_139) ).
% 1.29/1.36
% 1.29/1.36 cnf(quest_4,negated_conjecture,
% 1.29/1.36 ~ p_Empty(t_139) ).
% 1.29/1.36
% 1.29/1.36 %--------------------------------------------------------------------------
% 1.29/1.36 %-------------------------------------------
% 1.29/1.36 % Proof found
% 1.29/1.36 % SZS status Theorem for theBenchmark
% 1.29/1.36 % SZS output start Proof
% 1.29/1.36 %ClaNum:122(EqnAxiom:29)
% 1.29/1.36 %VarNum:496(SingletonVarNum:136)
% 1.29/1.36 %MaxLitNum:7
% 1.29/1.36 %MaxfuncDepth:2
% 1.29/1.36 %SharedTerms:12
% 1.29/1.36 %goalClause: 30 33 35 36
% 1.29/1.36 %singleGoalClaCount:4
% 1.29/1.36 [30]P1(a1)
% 1.29/1.36 [35]~P4(a1)
% 1.29/1.36 [36]~P10(a1)
% 1.29/1.36 [33]P9(f7(a1,a6))
% 1.29/1.36 [38]~P2(x381,x381)
% 1.29/1.36 [32]E(f7(a2,x321),x321)
% 1.29/1.36 [34]P2(f7(x341,a6),a2)
% 1.29/1.36 [37]~E(f7(x371,a6),a2)
% 1.29/1.36 [43]P2(x431,a2)+E(x431,a2)
% 1.29/1.36 [39]~P4(x391)+E(f3(x391),a2)
% 1.29/1.36 [40]~P7(x401)+E(f3(x401),a4)
% 1.29/1.36 [41]P7(x411)+~E(f3(x411),a4)
% 1.29/1.36 [42]P4(x421)+~E(f3(x421),a2)
% 1.29/1.36 [58]~P10(x581)+~P12(f7(x581,a6))
% 1.29/1.36 [59]~P10(x591)+~P9(f7(x591,a6))
% 1.29/1.36 [64]~P2(x641,a2)+P2(x641,f5(x641,a6))
% 1.29/1.36 [44]E(x441,a2)+E(f7(f9(x441),a6),x441)
% 1.29/1.36 [47]~P10(x471)+E(f3(f7(x471,a6)),a2)
% 1.29/1.36 [48]~P10(x481)+E(f10(f7(x481,a6)),a2)
% 1.29/1.36 [49]~P10(x491)+E(f8(f7(x491,a6)),a2)
% 1.29/1.36 [45]~P3(x451,x452)+~E(x451,x452)
% 1.29/1.36 [55]~P3(x552,x551)+~P2(x551,x552)
% 1.29/1.36 [51]E(x511,x512)+~E(f7(x511,a6),f7(x512,a6))
% 1.29/1.36 [72]~P10(x721)+~P5(x722,f7(x721,a6))
% 1.29/1.36 [84]~P2(x841,x842)+P2(f7(x841,a6),f7(x842,a6))
% 1.29/1.36 [97]P2(x971,x972)+~P2(f7(x971,a6),f7(x972,a6))
% 1.29/1.36 [104]~P10(x1041)+~P8(x1042,x1043,f7(x1041,a6))
% 1.29/1.36 [50]P10(x501)+P11(x501)+E(f10(f7(x501,a6)),f10(x501))
% 1.29/1.36 [46]P2(x462,x461)+P2(x461,x462)+E(x461,x462)
% 1.29/1.36 [78]~P2(x782,x781)+P2(x782,f7(x781,a6))+E(f7(x781,a6),x782)
% 1.29/1.36 [81]P2(x811,x812)+E(x811,x812)+~P2(f7(x811,a6),x812)
% 1.29/1.36 [65]~P2(x651,x653)+P2(x651,x652)+~P2(x653,x652)
% 1.29/1.36 [61]P3(x612,x613)+~E(f5(x613,x612),x611)+E(f7(x611,x612),x613)
% 1.29/1.36 [62]P3(x622,x621)+~E(f7(x623,x622),x621)+E(f5(x621,x622),x623)
% 1.29/1.36 [52]P11(x521)+~P12(x521)+P10(x521)+P12(f7(x521,a6))
% 1.29/1.36 [63]P12(x631)+P11(x631)+P10(x631)+~P12(f7(x631,a6))
% 1.29/1.36 [67]~P11(x671)+~P1(x671)+P10(x671)+~P12(f7(x671,a6))
% 1.29/1.36 [53]P10(x531)+P11(x531)+P1(x531)+E(f3(f7(x531,a6)),f3(x531))
% 1.29/1.36 [54]P10(x541)+P11(x541)+P1(x541)+E(f8(f7(x541,a6)),f8(x541))
% 1.29/1.36 [56]P10(x561)+P1(x561)+~P11(x561)+E(f8(f7(x561,a6)),f8(x561))
% 1.29/1.36 [112]P11(x1121)+~P8(x1122,x1123,x1121)+P10(x1121)+P8(x1122,x1123,f7(x1121,a6))
% 1.29/1.36 [115]P11(x1151)+P10(x1151)+P8(x1152,x1153,x1151)+~P8(x1152,x1153,f7(x1151,a6))
% 1.29/1.36 [57]P11(x571)+P1(x571)+~P9(x571)+P10(x571)+P9(f7(x571,a6))
% 1.29/1.36 [60]P1(x601)+~P9(x601)+~P11(x601)+P10(x601)+P9(f7(x601,a6))
% 1.29/1.36 [66]P9(x661)+P11(x661)+P1(x661)+P10(x661)+~P9(f7(x661,a6))
% 1.29/1.36 [68]P1(x681)+~P11(x681)+P10(x681)+P2(a4,f3(x681))+P12(f7(x681,a6))
% 1.29/1.36 [69]P11(x691)+~P1(x691)+P10(x691)+P2(f3(x691),a2)+P9(f7(x691,a6))
% 1.29/1.36 [70]P9(x701)+P1(x701)+~P11(x701)+P10(x701)+~P9(f7(x701,a6))
% 1.29/1.36 [71]~P11(x711)+~P1(x711)+P10(x711)+P2(f3(x711),a2)+P9(f7(x711,a6))
% 1.29/1.36 [88]P1(x881)+~P11(x881)+P10(x881)+~P2(a4,f3(x881))+~P12(f7(x881,a6))
% 1.29/1.36 [89]P11(x891)+~P1(x891)+P10(x891)+~P2(f3(x891),a2)+~P9(f7(x891,a6))
% 1.29/1.36 [93]~P11(x931)+~P1(x931)+P10(x931)+~P2(f3(x931),a2)+~P9(f7(x931,a6))
% 1.29/1.36 [73]P10(x731)+P1(x731)+~P11(x731)+P2(a4,f3(x731))+E(f3(f7(x731,a6)),f3(x731))
% 1.29/1.36 [74]P10(x741)+P1(x741)+~P11(x741)+P2(a4,f3(x741))+E(f10(f7(x741,a6)),f10(x741))
% 1.29/1.36 [75]P10(x751)+P11(x751)+~P1(x751)+P2(f3(x751),a2)+E(f3(f7(x751,a6)),f3(x751))
% 1.29/1.36 [76]P10(x761)+P11(x761)+~P1(x761)+P2(f3(x761),a2)+E(f8(f7(x761,a6)),f8(x761))
% 1.29/1.36 [77]P10(x771)+~P11(x771)+~P1(x771)+P2(f3(x771),a2)+E(f8(f7(x771,a6)),f8(x771))
% 1.29/1.36 [83]P10(x831)+~P11(x831)+~P1(x831)+~P2(f3(x831),a2)+E(f3(f7(x831,a6)),f3(x831))
% 1.29/1.36 [85]P10(x851)+~P11(x851)+~P1(x851)+P2(f3(x851),a2)+E(f3(f7(x851,a6)),f7(f3(x851),a6))
% 1.29/1.36 [86]P10(x861)+~P11(x861)+~P1(x861)+P2(f5(a4,a6),f10(x861))+E(f10(f7(x861,a6)),a2)
% 1.29/1.36 [91]P10(x911)+P1(x911)+~P11(x911)+~P2(a4,f3(x911))+E(f3(f7(x911,a6)),f7(f3(x911),a6))
% 1.29/1.36 [92]P10(x921)+P11(x921)+~P1(x921)+~P2(f3(x921),a2)+E(f3(f7(x921,a6)),f5(f3(x921),a6))
% 1.29/1.36 [103]P10(x1031)+~P11(x1031)+~P1(x1031)+~P2(f5(a4,a6),f10(x1031))+E(f10(f7(x1031,a6)),f7(f10(x1031),a6))
% 1.29/1.36 [79]P11(x791)+P1(x791)+~P5(x792,x791)+P10(x791)+P5(x792,f7(x791,a6))
% 1.29/1.36 [82]P1(x821)+~P11(x821)+~P5(x822,x821)+P10(x821)+P5(x822,f7(x821,a6))
% 1.29/1.36 [87]P11(x871)+P1(x871)+P10(x871)+P5(x872,x871)+~P5(x872,f7(x871,a6))
% 1.29/1.36 [90]P1(x901)+~P11(x901)+P10(x901)+P5(x902,x901)+~P5(x902,f7(x901,a6))
% 1.29/1.36 [102]~P11(x1021)+~P1(x1021)+~P6(x1022,x1021)+P10(x1021)+P8(f10(x1021),x1022,f7(x1021,a6))
% 1.29/1.36 [109]~P11(x1091)+~P1(x1091)+P10(x1091)+P6(x1092,x1091)+~P8(f10(x1091),x1092,f7(x1091,a6))
% 1.29/1.36 [99]P10(x991)+P1(x991)+~P11(x991)+P2(f5(a4,a6),f10(x991))+~P2(a4,f3(x991))+E(f10(f7(x991,a6)),a2)
% 1.29/1.36 [100]P10(x1001)+P11(x1001)+~P1(x1001)+P2(f5(a4,a6),f8(x1001))+~P2(f3(x1001),a2)+E(f8(f7(x1001,a6)),a2)
% 1.29/1.36 [101]P10(x1011)+~P11(x1011)+~P1(x1011)+P2(f5(a4,a6),f8(x1011))+~P2(f3(x1011),a2)+E(f8(f7(x1011,a6)),a2)
% 1.29/1.36 [106]P10(x1061)+P1(x1061)+~P11(x1061)+~P2(f5(a4,a6),f10(x1061))+~P2(a4,f3(x1061))+E(f10(f7(x1061,a6)),f7(f10(x1061),a6))
% 1.29/1.36 [107]P10(x1071)+P11(x1071)+~P1(x1071)+~P2(f5(a4,a6),f8(x1071))+~P2(f3(x1071),a2)+E(f8(f7(x1071,a6)),f7(f8(x1071),a6))
% 1.29/1.36 [108]P10(x1081)+~P11(x1081)+~P1(x1081)+~P2(f5(a4,a6),f8(x1081))+~P2(f3(x1081),a2)+E(f8(f7(x1081,a6)),f7(f8(x1081),a6))
% 1.29/1.36 [94]P11(x941)+~P1(x941)+~P5(x942,x941)+P10(x941)+P5(x942,f7(x941,a6))+P2(f3(x941),a2)
% 1.29/1.36 [95]~P11(x951)+~P1(x951)+~P5(x952,x951)+P10(x951)+P5(x952,f7(x951,a6))+P2(f3(x951),a2)
% 1.29/1.36 [96]P11(x961)+~P1(x961)+P10(x961)+P5(x962,x961)+~P5(x962,f7(x961,a6))+P2(f3(x961),a2)
% 1.29/1.36 [98]~P11(x981)+~P1(x981)+P10(x981)+P5(x982,x981)+~P5(x982,f7(x981,a6))+P2(f3(x981),a2)
% 1.29/1.36 [105]P1(x1051)+~P11(x1051)+~P6(x1052,x1051)+P10(x1051)+P8(f10(x1051),x1052,f7(x1051,a6))+~P2(a4,f3(x1051))
% 1.29/1.36 [110]P11(x1101)+~P1(x1101)+P10(x1101)+P8(f8(x1101),x1102,x1101)+~P5(x1102,f7(x1101,a6))+~P2(f3(x1101),a2)
% 1.29/1.36 [111]~P11(x1111)+~P1(x1111)+P10(x1111)+P8(f8(x1111),x1112,x1111)+~P5(x1112,f7(x1111,a6))+~P2(f3(x1111),a2)
% 1.29/1.36 [113]P11(x1131)+~P1(x1131)+P10(x1131)+~P8(f8(x1131),x1132,x1131)+P5(x1132,f7(x1131,a6))+~P2(f3(x1131),a2)
% 1.29/1.36 [114]~P11(x1141)+~P1(x1141)+P10(x1141)+~P8(f8(x1141),x1142,x1141)+P5(x1142,f7(x1141,a6))+~P2(f3(x1141),a2)
% 1.29/1.36 [117]P1(x1171)+~P11(x1171)+P10(x1171)+P6(x1172,x1171)+~P8(f10(x1171),x1172,f7(x1171,a6))+~P2(a4,f3(x1171))
% 1.29/1.36 [116]P10(x1162)+~P11(x1162)+~P1(x1162)+~P8(x1161,x1163,x1162)+P8(x1161,x1163,f7(x1162,a6))+E(x1161,f10(x1162))
% 1.29/1.36 [118]P1(x1181)+~P11(x1181)+~P8(x1182,x1183,x1181)+P10(x1181)+P8(x1182,x1183,f7(x1181,a6))+P2(a4,f3(x1181))
% 1.29/1.36 [119]P10(x1192)+~P11(x1192)+~P1(x1192)+P8(x1191,x1193,x1192)+~P8(x1191,x1193,f7(x1192,a6))+E(x1191,f10(x1192))
% 1.29/1.36 [120]P1(x1201)+~P11(x1201)+P10(x1201)+P8(x1202,x1203,x1201)+~P8(x1202,x1203,f7(x1201,a6))+P2(a4,f3(x1201))
% 1.29/1.36 [121]P10(x1212)+P1(x1212)+~P11(x1212)+~P8(x1211,x1213,x1212)+P8(x1211,x1213,f7(x1212,a6))+E(x1211,f10(x1212))+~P2(a4,f3(x1212))
% 1.29/1.36 [122]P10(x1222)+P1(x1222)+~P11(x1222)+P8(x1221,x1223,x1222)+~P8(x1221,x1223,f7(x1222,a6))+E(x1221,f10(x1222))+~P2(a4,f3(x1222))
% 1.29/1.36 %EqnAxiom
% 1.29/1.36 [1]E(x11,x11)
% 1.29/1.36 [2]E(x22,x21)+~E(x21,x22)
% 1.29/1.36 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 1.29/1.36 [4]~E(x41,x42)+E(f7(x41,x43),f7(x42,x43))
% 1.29/1.36 [5]~E(x51,x52)+E(f7(x53,x51),f7(x53,x52))
% 1.29/1.36 [6]~E(x61,x62)+E(f3(x61),f3(x62))
% 1.29/1.36 [7]~E(x71,x72)+E(f10(x71),f10(x72))
% 1.29/1.36 [8]~E(x81,x82)+E(f5(x81,x83),f5(x82,x83))
% 1.29/1.36 [9]~E(x91,x92)+E(f5(x93,x91),f5(x93,x92))
% 1.29/1.36 [10]~E(x101,x102)+E(f8(x101),f8(x102))
% 1.29/1.36 [11]~E(x111,x112)+E(f9(x111),f9(x112))
% 1.29/1.36 [12]~P1(x121)+P1(x122)+~E(x121,x122)
% 1.29/1.36 [13]~P9(x131)+P9(x132)+~E(x131,x132)
% 1.29/1.36 [14]P2(x142,x143)+~E(x141,x142)+~P2(x141,x143)
% 1.29/1.36 [15]P2(x153,x152)+~E(x151,x152)+~P2(x153,x151)
% 1.29/1.36 [16]~P4(x161)+P4(x162)+~E(x161,x162)
% 1.29/1.36 [17]~P10(x171)+P10(x172)+~E(x171,x172)
% 1.29/1.37 [18]P5(x182,x183)+~E(x181,x182)+~P5(x181,x183)
% 1.29/1.37 [19]P5(x193,x192)+~E(x191,x192)+~P5(x193,x191)
% 1.29/1.37 [20]~P11(x201)+P11(x202)+~E(x201,x202)
% 1.29/1.37 [21]~P7(x211)+P7(x212)+~E(x211,x212)
% 1.29/1.37 [22]P3(x222,x223)+~E(x221,x222)+~P3(x221,x223)
% 1.29/1.37 [23]P3(x233,x232)+~E(x231,x232)+~P3(x233,x231)
% 1.29/1.37 [24]P8(x242,x243,x244)+~E(x241,x242)+~P8(x241,x243,x244)
% 1.29/1.37 [25]P8(x253,x252,x254)+~E(x251,x252)+~P8(x253,x251,x254)
% 1.29/1.37 [26]P8(x263,x264,x262)+~E(x261,x262)+~P8(x263,x264,x261)
% 1.29/1.37 [27]~P12(x271)+P12(x272)+~E(x271,x272)
% 1.29/1.37 [28]P6(x282,x283)+~E(x281,x282)+~P6(x281,x283)
% 1.29/1.37 [29]P6(x293,x292)+~E(x291,x292)+~P6(x293,x291)
% 1.29/1.37
% 1.29/1.37 %-------------------------------------------
% 1.29/1.37 cnf(125,plain,
% 1.29/1.37 (P3(x1251,x1252)+E(f7(f5(x1252,x1251),x1251),x1252)),
% 1.29/1.37 inference(equality_inference,[],[61])).
% 1.29/1.37 cnf(132,plain,
% 1.29/1.37 (~E(f7(x1321,a6),a2)),
% 1.29/1.37 inference(rename_variables,[],[37])).
% 1.29/1.37 cnf(137,plain,
% 1.29/1.37 (E(f7(a2,x1371),x1371)),
% 1.29/1.37 inference(rename_variables,[],[32])).
% 1.29/1.37 cnf(143,plain,
% 1.29/1.37 (~P2(a2,x1431)),
% 1.29/1.37 inference(scs_inference,[],[30,35,36,38,32,137,34,37,132,55,45,125,2,12,16,17,65,78])).
% 1.29/1.37 cnf(225,plain,
% 1.29/1.37 (E(f3(a1),a2)+P11(a1)),
% 1.29/1.37 inference(scs_inference,[],[30,33,36,143,89,46])).
% 1.29/1.37 cnf(232,plain,
% 1.29/1.37 (E(f3(a1),a2)+~P11(a1)),
% 1.29/1.37 inference(scs_inference,[],[30,33,36,143,93,46])).
% 1.29/1.37 cnf(418,plain,
% 1.29/1.37 (P11(a1)),
% 1.29/1.37 inference(scs_inference,[],[35,225,42])).
% 1.29/1.37 cnf(420,plain,
% 1.29/1.37 (E(f3(a1),a2)),
% 1.29/1.37 inference(scs_inference,[],[418,232])).
% 1.29/1.37 cnf(426,plain,
% 1.29/1.37 ($false),
% 1.29/1.37 inference(scs_inference,[],[35,420,42]),
% 1.29/1.37 ['proof']).
% 1.29/1.37 % SZS output end Proof
% 1.29/1.37 % Total time :0.730000s
%------------------------------------------------------------------------------