%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : HWV009-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 : 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:07 EDT 2024
% Result : Unsatisfiable 1.37s 1.49s
% Output : CNFRefutation 1.43s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.14 % Problem : HWV009-1 : TPTP v8.2.0. Released v2.5.0.
% 0.12/0.14 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.14/0.36 % Computer : n023.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 300
% 0.14/0.36 % DateTime : Fri Jun 21 03:57:09 EDT 2024
% 0.14/0.36 % CPUTime :
% 0.50/0.56 start to proof:theBenchmark
% 1.37/1.49 %-------------------------------------------
% 1.37/1.49 % File :CSE---1.7
% 1.37/1.49 % Problem :theBenchmark
% 1.37/1.49 % Transform :cnf
% 1.37/1.49 % Format :tptp:raw
% 1.37/1.49 % Command :java -jar mcs_scs.jar %d %s
% 1.37/1.49
% 1.37/1.49 % Result :Theorem 0.870000s
% 1.37/1.49 % Output :CNFRefutation 0.870000s
% 1.37/1.49 %-------------------------------------------
% 1.37/1.49 %--------------------------------------------------------------------------
% 1.37/1.49 % File : HWV009-1 : TPTP v8.2.0. Released v2.5.0.
% 1.37/1.49 % Domain : Hardware Verification
% 1.37/1.49 % Problem : Safelogic VHDL design verification obligation
% 1.37/1.49 % Version : [Mar02] axioms : Especial.
% 1.37/1.49 % English :
% 1.37/1.49
% 1.37/1.49 % Refs : [CHM02] Claessen et al. (2002), Verification of Hardware Systems
% 1.37/1.49 % : [Mar02] Martensson (2002), Email to G. Sutcliffe
% 1.37/1.49 % Source : [Mar02]
% 1.37/1.49 % Names :
% 1.37/1.49
% 1.37/1.49 % Status : Unsatisfiable
% 1.37/1.49 % Rating : 0.05 v8.1.0, 0.00 v7.3.0, 0.08 v7.0.0, 0.13 v6.4.0, 0.07 v6.3.0, 0.18 v6.2.0, 0.10 v6.1.0, 0.07 v6.0.0, 0.10 v5.5.0, 0.25 v5.3.0, 0.17 v5.2.0, 0.12 v5.0.0, 0.07 v4.1.0, 0.15 v4.0.1, 0.18 v3.7.0, 0.10 v3.5.0, 0.09 v3.4.0, 0.08 v3.3.0, 0.14 v3.2.0, 0.08 v3.1.0, 0.18 v2.7.0, 0.08 v2.6.0, 0.12 v2.5.0
% 1.37/1.49 % Syntax : Number of clauses : 92 ( 7 unt; 65 nHn; 83 RR)
% 1.37/1.49 % Number of literals : 373 ( 51 equ; 156 neg)
% 1.37/1.49 % Maximal clause size : 7 ( 4 avg)
% 1.37/1.49 % Maximal term depth : 3 ( 1 avg)
% 1.37/1.49 % Number of predicates : 13 ( 12 usr; 0 prp; 1-3 aty)
% 1.37/1.49 % Number of functors : 11 ( 11 usr; 4 con; 0-2 aty)
% 1.37/1.49 % Number of variables : 139 ( 5 sgn)
% 1.37/1.49 % SPC : CNF_UNS_RFO_SEQ_NHN
% 1.37/1.49
% 1.37/1.49 % Comments :
% 1.37/1.49 %--------------------------------------------------------------------------
% 1.37/1.49 %----Include equality
% 1.37/1.49 %----Include VHDL design axioms
% 1.37/1.49 include('Axioms/HWV003-0.ax').
% 1.37/1.49 %--------------------------------------------------------------------------
% 1.37/1.49 cnf(quest_1,negated_conjecture,
% 1.37/1.49 p_Reset(t_139) ).
% 1.37/1.49
% 1.37/1.49 cnf(quest_2,negated_conjecture,
% 1.37/1.49 ( level(plus(t_139,n1)) != n0
% 1.37/1.49 | p_Wr_error(plus(t_139,n1))
% 1.37/1.49 | p_Rd_error(plus(t_139,n1)) ) ).
% 1.37/1.49
% 1.37/1.49 %--------------------------------------------------------------------------
% 1.37/1.49 %-------------------------------------------
% 1.37/1.49 % Proof found
% 1.37/1.49 % SZS status Theorem for theBenchmark
% 1.37/1.49 % SZS output start Proof
% 1.37/1.49 %ClaNum:120(EqnAxiom:29)
% 1.37/1.49 %VarNum:496(SingletonVarNum:136)
% 1.37/1.49 %MaxLitNum:7
% 1.37/1.49 %MaxfuncDepth:2
% 1.37/1.49 %SharedTerms:13
% 1.37/1.49 %goalClause: 30 85
% 1.37/1.49 %singleGoalClaCount:1
% 1.37/1.49 [30]P1(a1)
% 1.37/1.49 [35]~P2(x351,x351)
% 1.37/1.49 [32]E(f7(a2,x321),x321)
% 1.37/1.49 [33]P2(f7(x331,a6),a2)
% 1.37/1.49 [34]~E(f7(x341,a6),a2)
% 1.37/1.49 [40]P2(x401,a2)+E(x401,a2)
% 1.37/1.49 [36]~P4(x361)+E(f3(x361),a2)
% 1.37/1.49 [37]~P7(x371)+E(f3(x371),a4)
% 1.37/1.49 [38]P7(x381)+~E(f3(x381),a4)
% 1.37/1.49 [39]P4(x391)+~E(f3(x391),a2)
% 1.37/1.49 [55]~P1(x551)+~P12(f7(x551,a6))
% 1.37/1.49 [56]~P1(x561)+~P10(f7(x561,a6))
% 1.37/1.49 [61]~P2(x611,a2)+P2(x611,f5(x611,a6))
% 1.37/1.49 [41]E(x411,a2)+E(f7(f9(x411),a6),x411)
% 1.37/1.49 [44]~P1(x441)+E(f3(f7(x441,a6)),a2)
% 1.37/1.49 [45]~P1(x451)+E(f10(f7(x451,a6)),a2)
% 1.37/1.49 [46]~P1(x461)+E(f8(f7(x461,a6)),a2)
% 1.37/1.49 [42]~P3(x421,x422)+~E(x421,x422)
% 1.37/1.49 [52]~P3(x522,x521)+~P2(x521,x522)
% 1.37/1.49 [48]E(x481,x482)+~E(f7(x481,a6),f7(x482,a6))
% 1.37/1.49 [69]~P1(x691)+~P5(x692,f7(x691,a6))
% 1.37/1.49 [81]~P2(x811,x812)+P2(f7(x811,a6),f7(x812,a6))
% 1.37/1.49 [95]P2(x951,x952)+~P2(f7(x951,a6),f7(x952,a6))
% 1.37/1.49 [102]~P1(x1021)+~P9(x1022,x1023,f7(x1021,a6))
% 1.37/1.49 [85]P10(f7(a1,a6))+P12(f7(a1,a6))+~E(f3(f7(a1,a6)),a2)
% 1.37/1.49 [47]P1(x471)+P11(x471)+E(f10(f7(x471,a6)),f10(x471))
% 1.37/1.49 [43]P2(x432,x431)+P2(x431,x432)+E(x431,x432)
% 1.37/1.49 [75]~P2(x752,x751)+P2(x752,f7(x751,a6))+E(f7(x751,a6),x752)
% 1.37/1.49 [78]P2(x781,x782)+E(x781,x782)+~P2(f7(x781,a6),x782)
% 1.37/1.49 [62]~P2(x621,x623)+P2(x621,x622)+~P2(x623,x622)
% 1.37/1.49 [58]P3(x582,x583)+~E(f5(x583,x582),x581)+E(f7(x581,x582),x583)
% 1.37/1.49 [59]P3(x592,x591)+~E(f7(x593,x592),x591)+E(f5(x591,x592),x593)
% 1.37/1.49 [49]P11(x491)+~P12(x491)+P1(x491)+P12(f7(x491,a6))
% 1.37/1.49 [60]P12(x601)+P11(x601)+P1(x601)+~P12(f7(x601,a6))
% 1.37/1.49 [64]~P11(x641)+~P8(x641)+P1(x641)+~P12(f7(x641,a6))
% 1.37/1.49 [50]P1(x501)+P11(x501)+P8(x501)+E(f3(f7(x501,a6)),f3(x501))
% 1.37/1.49 [51]P1(x511)+P11(x511)+P8(x511)+E(f8(f7(x511,a6)),f8(x511))
% 1.37/1.49 [53]P1(x531)+P8(x531)+~P11(x531)+E(f8(f7(x531,a6)),f8(x531))
% 1.37/1.49 [110]P11(x1101)+~P9(x1102,x1103,x1101)+P1(x1101)+P9(x1102,x1103,f7(x1101,a6))
% 1.37/1.49 [113]P11(x1131)+P1(x1131)+P9(x1132,x1133,x1131)+~P9(x1132,x1133,f7(x1131,a6))
% 1.37/1.49 [54]P11(x541)+P8(x541)+~P10(x541)+P1(x541)+P10(f7(x541,a6))
% 1.37/1.49 [57]P8(x571)+~P10(x571)+~P11(x571)+P1(x571)+P10(f7(x571,a6))
% 1.37/1.49 [63]P10(x631)+P11(x631)+P8(x631)+P1(x631)+~P10(f7(x631,a6))
% 1.37/1.49 [65]P8(x651)+~P11(x651)+P1(x651)+P2(a4,f3(x651))+P12(f7(x651,a6))
% 1.37/1.49 [66]P11(x661)+~P8(x661)+P1(x661)+P2(f3(x661),a2)+P10(f7(x661,a6))
% 1.37/1.49 [67]P10(x671)+P8(x671)+~P11(x671)+P1(x671)+~P10(f7(x671,a6))
% 1.37/1.49 [68]~P11(x681)+~P8(x681)+P1(x681)+P2(f3(x681),a2)+P10(f7(x681,a6))
% 1.37/1.49 [86]P8(x861)+~P11(x861)+P1(x861)+~P2(a4,f3(x861))+~P12(f7(x861,a6))
% 1.37/1.49 [87]P11(x871)+~P8(x871)+P1(x871)+~P2(f3(x871),a2)+~P10(f7(x871,a6))
% 1.37/1.49 [91]~P11(x911)+~P8(x911)+P1(x911)+~P2(f3(x911),a2)+~P10(f7(x911,a6))
% 1.37/1.49 [70]P1(x701)+P8(x701)+~P11(x701)+P2(a4,f3(x701))+E(f3(f7(x701,a6)),f3(x701))
% 1.37/1.49 [71]P1(x711)+P8(x711)+~P11(x711)+P2(a4,f3(x711))+E(f10(f7(x711,a6)),f10(x711))
% 1.37/1.49 [72]P1(x721)+P11(x721)+~P8(x721)+P2(f3(x721),a2)+E(f3(f7(x721,a6)),f3(x721))
% 1.37/1.49 [73]P1(x731)+P11(x731)+~P8(x731)+P2(f3(x731),a2)+E(f8(f7(x731,a6)),f8(x731))
% 1.37/1.49 [74]P1(x741)+~P11(x741)+~P8(x741)+P2(f3(x741),a2)+E(f8(f7(x741,a6)),f8(x741))
% 1.37/1.49 [80]P1(x801)+~P11(x801)+~P8(x801)+~P2(f3(x801),a2)+E(f3(f7(x801,a6)),f3(x801))
% 1.37/1.49 [82]P1(x821)+~P11(x821)+~P8(x821)+P2(f3(x821),a2)+E(f3(f7(x821,a6)),f7(f3(x821),a6))
% 1.37/1.49 [83]P1(x831)+~P11(x831)+~P8(x831)+P2(f5(a4,a6),f10(x831))+E(f10(f7(x831,a6)),a2)
% 1.37/1.49 [89]P1(x891)+P8(x891)+~P11(x891)+~P2(a4,f3(x891))+E(f3(f7(x891,a6)),f7(f3(x891),a6))
% 1.37/1.49 [90]P1(x901)+P11(x901)+~P8(x901)+~P2(f3(x901),a2)+E(f3(f7(x901,a6)),f5(f3(x901),a6))
% 1.37/1.49 [101]P1(x1011)+~P11(x1011)+~P8(x1011)+~P2(f5(a4,a6),f10(x1011))+E(f10(f7(x1011,a6)),f7(f10(x1011),a6))
% 1.37/1.49 [76]P11(x761)+P8(x761)+~P5(x762,x761)+P1(x761)+P5(x762,f7(x761,a6))
% 1.37/1.49 [79]P8(x791)+~P11(x791)+~P5(x792,x791)+P1(x791)+P5(x792,f7(x791,a6))
% 1.37/1.49 [84]P11(x841)+P8(x841)+P1(x841)+P5(x842,x841)+~P5(x842,f7(x841,a6))
% 1.37/1.49 [88]P8(x881)+~P11(x881)+P1(x881)+P5(x882,x881)+~P5(x882,f7(x881,a6))
% 1.37/1.50 [100]~P11(x1001)+~P8(x1001)+~P6(x1002,x1001)+P1(x1001)+P9(f10(x1001),x1002,f7(x1001,a6))
% 1.37/1.50 [107]~P11(x1071)+~P8(x1071)+P1(x1071)+P6(x1072,x1071)+~P9(f10(x1071),x1072,f7(x1071,a6))
% 1.37/1.50 [97]P1(x971)+P8(x971)+~P11(x971)+P2(f5(a4,a6),f10(x971))+~P2(a4,f3(x971))+E(f10(f7(x971,a6)),a2)
% 1.37/1.50 [98]P1(x981)+P11(x981)+~P8(x981)+P2(f5(a4,a6),f8(x981))+~P2(f3(x981),a2)+E(f8(f7(x981,a6)),a2)
% 1.37/1.50 [99]P1(x991)+~P11(x991)+~P8(x991)+P2(f5(a4,a6),f8(x991))+~P2(f3(x991),a2)+E(f8(f7(x991,a6)),a2)
% 1.37/1.50 [104]P1(x1041)+P8(x1041)+~P11(x1041)+~P2(f5(a4,a6),f10(x1041))+~P2(a4,f3(x1041))+E(f10(f7(x1041,a6)),f7(f10(x1041),a6))
% 1.37/1.50 [105]P1(x1051)+P11(x1051)+~P8(x1051)+~P2(f5(a4,a6),f8(x1051))+~P2(f3(x1051),a2)+E(f8(f7(x1051,a6)),f7(f8(x1051),a6))
% 1.37/1.50 [106]P1(x1061)+~P11(x1061)+~P8(x1061)+~P2(f5(a4,a6),f8(x1061))+~P2(f3(x1061),a2)+E(f8(f7(x1061,a6)),f7(f8(x1061),a6))
% 1.37/1.50 [92]P11(x921)+~P8(x921)+~P5(x922,x921)+P1(x921)+P5(x922,f7(x921,a6))+P2(f3(x921),a2)
% 1.37/1.50 [93]~P11(x931)+~P8(x931)+~P5(x932,x931)+P1(x931)+P5(x932,f7(x931,a6))+P2(f3(x931),a2)
% 1.37/1.50 [94]P11(x941)+~P8(x941)+P1(x941)+P5(x942,x941)+~P5(x942,f7(x941,a6))+P2(f3(x941),a2)
% 1.37/1.50 [96]~P11(x961)+~P8(x961)+P1(x961)+P5(x962,x961)+~P5(x962,f7(x961,a6))+P2(f3(x961),a2)
% 1.37/1.50 [103]P8(x1031)+~P11(x1031)+~P6(x1032,x1031)+P1(x1031)+P9(f10(x1031),x1032,f7(x1031,a6))+~P2(a4,f3(x1031))
% 1.37/1.50 [108]P11(x1081)+~P8(x1081)+P1(x1081)+P9(f8(x1081),x1082,x1081)+~P5(x1082,f7(x1081,a6))+~P2(f3(x1081),a2)
% 1.37/1.50 [109]~P11(x1091)+~P8(x1091)+P1(x1091)+P9(f8(x1091),x1092,x1091)+~P5(x1092,f7(x1091,a6))+~P2(f3(x1091),a2)
% 1.37/1.50 [111]P11(x1111)+~P8(x1111)+P1(x1111)+~P9(f8(x1111),x1112,x1111)+P5(x1112,f7(x1111,a6))+~P2(f3(x1111),a2)
% 1.37/1.50 [112]~P11(x1121)+~P8(x1121)+P1(x1121)+~P9(f8(x1121),x1122,x1121)+P5(x1122,f7(x1121,a6))+~P2(f3(x1121),a2)
% 1.37/1.50 [115]P8(x1151)+~P11(x1151)+P1(x1151)+P6(x1152,x1151)+~P9(f10(x1151),x1152,f7(x1151,a6))+~P2(a4,f3(x1151))
% 1.37/1.50 [114]P1(x1142)+~P11(x1142)+~P8(x1142)+~P9(x1141,x1143,x1142)+P9(x1141,x1143,f7(x1142,a6))+E(x1141,f10(x1142))
% 1.37/1.50 [116]P8(x1161)+~P11(x1161)+~P9(x1162,x1163,x1161)+P1(x1161)+P9(x1162,x1163,f7(x1161,a6))+P2(a4,f3(x1161))
% 1.37/1.50 [117]P1(x1172)+~P11(x1172)+~P8(x1172)+P9(x1171,x1173,x1172)+~P9(x1171,x1173,f7(x1172,a6))+E(x1171,f10(x1172))
% 1.37/1.50 [118]P8(x1181)+~P11(x1181)+P1(x1181)+P9(x1182,x1183,x1181)+~P9(x1182,x1183,f7(x1181,a6))+P2(a4,f3(x1181))
% 1.37/1.50 [119]P1(x1192)+P8(x1192)+~P11(x1192)+~P9(x1191,x1193,x1192)+P9(x1191,x1193,f7(x1192,a6))+E(x1191,f10(x1192))+~P2(a4,f3(x1192))
% 1.37/1.50 [120]P1(x1202)+P8(x1202)+~P11(x1202)+P9(x1201,x1203,x1202)+~P9(x1201,x1203,f7(x1202,a6))+E(x1201,f10(x1202))+~P2(a4,f3(x1202))
% 1.37/1.50 %EqnAxiom
% 1.37/1.50 [1]E(x11,x11)
% 1.37/1.50 [2]E(x22,x21)+~E(x21,x22)
% 1.37/1.50 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 1.37/1.50 [4]~E(x41,x42)+E(f7(x41,x43),f7(x42,x43))
% 1.37/1.50 [5]~E(x51,x52)+E(f7(x53,x51),f7(x53,x52))
% 1.37/1.50 [6]~E(x61,x62)+E(f3(x61),f3(x62))
% 1.37/1.50 [7]~E(x71,x72)+E(f10(x71),f10(x72))
% 1.37/1.50 [8]~E(x81,x82)+E(f5(x81,x83),f5(x82,x83))
% 1.37/1.50 [9]~E(x91,x92)+E(f5(x93,x91),f5(x93,x92))
% 1.37/1.50 [10]~E(x101,x102)+E(f8(x101),f8(x102))
% 1.37/1.50 [11]~E(x111,x112)+E(f9(x111),f9(x112))
% 1.37/1.50 [12]~P1(x121)+P1(x122)+~E(x121,x122)
% 1.37/1.50 [13]P2(x132,x133)+~E(x131,x132)+~P2(x131,x133)
% 1.37/1.50 [14]P2(x143,x142)+~E(x141,x142)+~P2(x143,x141)
% 1.37/1.50 [15]P9(x152,x153,x154)+~E(x151,x152)+~P9(x151,x153,x154)
% 1.37/1.50 [16]P9(x163,x162,x164)+~E(x161,x162)+~P9(x163,x161,x164)
% 1.37/1.50 [17]P9(x173,x174,x172)+~E(x171,x172)+~P9(x173,x174,x171)
% 1.37/1.50 [18]~P4(x181)+P4(x182)+~E(x181,x182)
% 1.37/1.50 [19]~P7(x191)+P7(x192)+~E(x191,x192)
% 1.37/1.50 [20]~P11(x201)+P11(x202)+~E(x201,x202)
% 1.37/1.50 [21]~P8(x211)+P8(x212)+~E(x211,x212)
% 1.37/1.50 [22]P5(x222,x223)+~E(x221,x222)+~P5(x221,x223)
% 1.37/1.50 [23]P5(x233,x232)+~E(x231,x232)+~P5(x233,x231)
% 1.37/1.50 [24]P3(x242,x243)+~E(x241,x242)+~P3(x241,x243)
% 1.37/1.50 [25]P3(x253,x252)+~E(x251,x252)+~P3(x253,x251)
% 1.37/1.50 [26]~P10(x261)+P10(x262)+~E(x261,x262)
% 1.37/1.50 [27]~P12(x271)+P12(x272)+~E(x271,x272)
% 1.37/1.50 [28]P6(x282,x283)+~E(x281,x282)+~P6(x281,x283)
% 1.37/1.50 [29]P6(x293,x292)+~E(x291,x292)+~P6(x293,x291)
% 1.37/1.50
% 1.37/1.50 %-------------------------------------------
% 1.37/1.50 cnf(121,plain,
% 1.37/1.50 (~P3(x1211,x1211)),
% 1.37/1.50 inference(equality_inference,[],[42])).
% 1.37/1.50 cnf(123,plain,
% 1.37/1.50 (P3(x1231,x1232)+E(f7(f5(x1232,x1231),x1231),x1232)),
% 1.37/1.50 inference(equality_inference,[],[58])).
% 1.37/1.50 cnf(125,plain,
% 1.37/1.50 (E(x1251,f7(a2,x1251))),
% 1.37/1.50 inference(scs_inference,[],[32,2])).
% 1.37/1.50 cnf(126,plain,
% 1.37/1.50 (~P3(f7(a2,x1261),x1261)),
% 1.37/1.50 inference(scs_inference,[],[32,2,42])).
% 1.37/1.50 cnf(128,plain,
% 1.37/1.50 (~P3(a2,f7(x1281,a6))),
% 1.37/1.50 inference(scs_inference,[],[32,33,2,42,52])).
% 1.37/1.50 cnf(131,plain,
% 1.37/1.50 (~E(f7(x1311,a6),a2)),
% 1.37/1.50 inference(rename_variables,[],[34])).
% 1.37/1.50 cnf(135,plain,
% 1.43/1.50 (~P2(x1351,x1351)),
% 1.43/1.50 inference(rename_variables,[],[35])).
% 1.43/1.50 cnf(142,plain,
% 1.43/1.50 (~E(a6,a2)),
% 1.43/1.50 inference(scs_inference,[],[30,121,35,135,32,33,34,131,2,42,52,123,12,62,75,14,24])).
% 1.43/1.50 cnf(143,plain,
% 1.43/1.50 (~P3(x1431,x1431)),
% 1.43/1.50 inference(rename_variables,[],[121])).
% 1.43/1.50 cnf(146,plain,
% 1.43/1.50 (P2(a6,a2)),
% 1.43/1.50 inference(scs_inference,[],[30,121,143,35,135,32,33,34,131,2,42,52,123,12,62,75,14,24,25,40])).
% 1.43/1.50 cnf(149,plain,
% 1.43/1.50 (E(f7(a2,x1491),x1491)),
% 1.43/1.50 inference(rename_variables,[],[32])).
% 1.43/1.50 cnf(150,plain,
% 1.43/1.50 (~E(f7(x1501,a6),f7(a2,a2))),
% 1.43/1.50 inference(scs_inference,[],[30,121,143,35,135,32,149,33,34,131,2,42,52,123,12,62,75,14,24,25,40,26,3])).
% 1.43/1.50 cnf(151,plain,
% 1.43/1.50 (E(f7(a2,x1511),x1511)),
% 1.43/1.50 inference(rename_variables,[],[32])).
% 1.43/1.50 cnf(152,plain,
% 1.43/1.50 (~P12(f7(a2,x1521))+P12(x1521)),
% 1.43/1.50 inference(scs_inference,[],[30,121,143,35,135,32,149,151,33,34,131,2,42,52,123,12,62,75,14,24,25,40,26,3,27])).
% 1.43/1.50 cnf(153,plain,
% 1.43/1.50 (P3(a6,f7(a2,a2))+~E(f5(f7(a2,a2),a6),x1531)),
% 1.43/1.50 inference(scs_inference,[],[30,121,143,35,135,32,149,151,33,34,131,2,42,52,123,12,62,75,14,24,25,40,26,3,27,58])).
% 1.43/1.50 cnf(158,plain,
% 1.43/1.50 (P3(a6,f7(a2,a2))),
% 1.43/1.50 inference(equality_inference,[],[153])).
% 1.43/1.50 cnf(161,plain,
% 1.43/1.50 (~P3(x1611,f7(a2,x1611))),
% 1.43/1.50 inference(scs_inference,[],[125,146,52,42])).
% 1.43/1.50 cnf(172,plain,
% 1.43/1.50 (P2(f5(a6,a2),a2)),
% 1.43/1.50 inference(scs_inference,[],[125,146,142,126,158,121,32,52,42,24,3,25,21,58,40])).
% 1.43/1.50 cnf(174,plain,
% 1.43/1.50 (~P10(x1741)+P10(f7(a2,x1741))),
% 1.43/1.50 inference(scs_inference,[],[125,146,142,126,158,121,32,52,42,24,3,25,21,58,40,26])).
% 1.43/1.50 cnf(177,plain,
% 1.43/1.50 (~P12(x1771)+P12(f7(a2,x1771))),
% 1.43/1.50 inference(scs_inference,[],[125,146,142,126,158,121,32,52,42,24,3,25,21,58,40,26,18,20,27])).
% 1.43/1.50 cnf(184,plain,
% 1.43/1.50 (E(f7(a2,x1841),x1841)),
% 1.43/1.50 inference(rename_variables,[],[32])).
% 1.43/1.50 cnf(198,plain,
% 1.43/1.50 (~P10(f7(a2,x1981))+P10(x1981)),
% 1.43/1.50 inference(scs_inference,[],[172,150,161,128,158,32,184,52,3,25,41,42,2,12,58,40,26])).
% 1.43/1.50 cnf(278,plain,
% 1.43/1.50 (~P12(f7(a2,f7(a1,a6)))),
% 1.43/1.50 inference(scs_inference,[],[30,152,55])).
% 1.43/1.50 cnf(279,plain,
% 1.43/1.50 (~P12(f7(a1,a6))),
% 1.43/1.50 inference(scs_inference,[],[278,177])).
% 1.43/1.50 cnf(284,plain,
% 1.43/1.50 (P10(f7(a1,a6))+~E(f3(f7(a1,a6)),a2)),
% 1.43/1.50 inference(scs_inference,[],[279,85])).
% 1.43/1.50 cnf(378,plain,
% 1.43/1.50 (~P10(f7(a2,f7(a1,a6)))),
% 1.43/1.50 inference(scs_inference,[],[30,198,56])).
% 1.43/1.50 cnf(379,plain,
% 1.43/1.50 (~P10(f7(a1,a6))),
% 1.43/1.50 inference(scs_inference,[],[378,174])).
% 1.43/1.50 cnf(384,plain,
% 1.43/1.50 (~E(f3(f7(a1,a6)),a2)),
% 1.43/1.50 inference(scs_inference,[],[379,284])).
% 1.43/1.50 cnf(388,plain,
% 1.43/1.50 ($false),
% 1.43/1.50 inference(scs_inference,[],[384,30,36,44]),
% 1.43/1.50 ['proof']).
% 1.43/1.50 % SZS output end Proof
% 1.43/1.50 % Total time :0.870000s
%------------------------------------------------------------------------------