%------------------------------------------------------------------------------
% File : SNARK---20120808r022
% Problem : ALG113+1 : TPTP v8.1.0. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run-snark %s %d
% 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 : 600s
% DateTime : Thu Jul 14 17:59:55 EDT 2022
% Result : Theorem 2.98s 3.16s
% Output : Refutation 2.98s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 73
% Syntax : Number of clauses : 160 ( 108 unt; 42 nHn; 160 RR)
% Number of literals : 343 ( 342 equ; 149 neg)
% Maximal clause size : 20 ( 2 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 20 ( 20 usr; 8 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(21,axiom,
( op1(e10,e10) = e12
| op1(e10,e11) = e12
| op1(e10,e12) = e12
| op1(e10,e13) = e12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2) ).
cnf(23,axiom,
( op1(e10,e10) = e13
| op1(e10,e11) = e13
| op1(e10,e12) = e13
| op1(e10,e13) = e13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2) ).
cnf(25,axiom,
( op1(e11,e10) = e10
| op1(e11,e11) = e10
| op1(e11,e12) = e10
| op1(e11,e13) = e10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2) ).
cnf(31,axiom,
( op1(e11,e10) = e13
| op1(e11,e11) = e13
| op1(e11,e12) = e13
| op1(e11,e13) = e13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2) ).
cnf(35,axiom,
( op1(e12,e10) = e11
| op1(e12,e11) = e11
| op1(e12,e12) = e11
| op1(e12,e13) = e11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2) ).
cnf(39,axiom,
( op1(e12,e10) = e13
| op1(e12,e11) = e13
| op1(e12,e12) = e13
| op1(e12,e13) = e13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2) ).
cnf(41,axiom,
( op1(e13,e10) = e10
| op1(e13,e11) = e10
| op1(e13,e12) = e10
| op1(e13,e13) = e10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2) ).
cnf(43,axiom,
( op1(e13,e10) = e11
| op1(e13,e11) = e11
| op1(e13,e12) = e11
| op1(e13,e13) = e11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2) ).
cnf(45,axiom,
( op1(e13,e10) = e12
| op1(e13,e11) = e12
| op1(e13,e12) = e12
| op1(e13,e13) = e12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2) ).
cnf(46,axiom,
( op1(e10,e13) = e12
| op1(e11,e13) = e12
| op1(e12,e13) = e12
| op1(e13,e13) = e12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2) ).
cnf(69,axiom,
( op2(e20,e20) = e22
| op2(e20,e21) = e22
| op2(e20,e22) = e22
| op2(e20,e23) = e22 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax4) ).
cnf(71,axiom,
( op2(e20,e20) = e23
| op2(e20,e21) = e23
| op2(e20,e22) = e23
| op2(e20,e23) = e23 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax4) ).
cnf(73,axiom,
( op2(e21,e20) = e20
| op2(e21,e21) = e20
| op2(e21,e22) = e20
| op2(e21,e23) = e20 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax4) ).
cnf(79,axiom,
( op2(e21,e20) = e23
| op2(e21,e21) = e23
| op2(e21,e22) = e23
| op2(e21,e23) = e23 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax4) ).
cnf(83,axiom,
( op2(e22,e20) = e21
| op2(e22,e21) = e21
| op2(e22,e22) = e21
| op2(e22,e23) = e21 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax4) ).
cnf(87,axiom,
( op2(e22,e20) = e23
| op2(e22,e21) = e23
| op2(e22,e22) = e23
| op2(e22,e23) = e23 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax4) ).
cnf(89,axiom,
( op2(e23,e20) = e20
| op2(e23,e21) = e20
| op2(e23,e22) = e20
| op2(e23,e23) = e20 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax4) ).
cnf(91,axiom,
( op2(e23,e20) = e21
| op2(e23,e21) = e21
| op2(e23,e22) = e21
| op2(e23,e23) = e21 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax4) ).
cnf(93,axiom,
( op2(e23,e20) = e22
| op2(e23,e21) = e22
| op2(e23,e22) = e22
| op2(e23,e23) = e22 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax4) ).
cnf(94,axiom,
( op2(e20,e23) = e22
| op2(e21,e23) = e22
| op2(e22,e23) = e22
| op2(e23,e23) = e22 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax4) ).
cnf(102,axiom,
op1(e12,e10) != op1(e13,e10),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
cnf(105,axiom,
op1(e10,e11) != op1(e13,e11),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
cnf(106,axiom,
op1(e11,e11) != op1(e12,e11),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
cnf(107,axiom,
op1(e11,e11) != op1(e13,e11),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
cnf(109,axiom,
op1(e10,e12) != op1(e11,e12),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
cnf(110,axiom,
op1(e10,e12) != op1(e12,e12),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
cnf(114,axiom,
op1(e12,e12) != op1(e13,e12),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
cnf(150,axiom,
op2(e22,e20) != op2(e23,e20),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
cnf(153,axiom,
op2(e20,e21) != op2(e23,e21),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
cnf(154,axiom,
op2(e21,e21) != op2(e22,e21),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
cnf(155,axiom,
op2(e21,e21) != op2(e23,e21),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
cnf(157,axiom,
op2(e20,e22) != op2(e21,e22),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
cnf(158,axiom,
op2(e20,e22) != op2(e22,e22),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
cnf(162,axiom,
op2(e22,e22) != op2(e23,e22),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
cnf(193,axiom,
e10 != e11,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax7) ).
cnf(194,axiom,
e10 != e12,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax7) ).
cnf(195,axiom,
e10 != e13,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax7) ).
cnf(196,axiom,
e11 != e12,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax7) ).
cnf(197,axiom,
e11 != e13,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax7) ).
cnf(198,axiom,
e12 != e13,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax7) ).
cnf(199,axiom,
e20 != e21,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
cnf(200,axiom,
e20 != e22,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
cnf(201,axiom,
e20 != e23,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
cnf(202,axiom,
e21 != e22,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
cnf(203,axiom,
e21 != e23,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
cnf(204,axiom,
e22 != e23,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
cnf(221,axiom,
op1(e10,e10) = e10,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax10) ).
cnf(222,axiom,
op1(e11,e11) = e11,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax10) ).
cnf(223,axiom,
op1(e12,e12) = e12,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax10) ).
cnf(224,axiom,
op1(e13,e13) = e13,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax10) ).
cnf(225,axiom,
op2(e20,e20) = e20,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax11) ).
cnf(226,axiom,
op2(e21,e21) = e21,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax11) ).
cnf(227,axiom,
op2(e22,e22) = e22,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax11) ).
cnf(228,axiom,
op2(e23,e23) = e23,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax11) ).
cnf(229,axiom,
op1(e12,e13) = e10,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax12) ).
cnf(230,axiom,
e11 = op1(op1(e12,e13),e13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax12) ).
cnf(231,plain,
op1(e10,e13) = e11,
inference('REWRITE',[status(thm)],[230,229,theory(equality)]) ).
cnf(232,axiom,
op2(e22,e23) = e20,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax13) ).
cnf(233,axiom,
e21 = op2(op2(e22,e23),e23),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax13) ).
cnf(234,plain,
op2(e20,e23) = e21,
inference('REWRITE',[status(thm)],[233,232,theory(equality)]) ).
cnf(237,axiom,
h1(e10) = op2(e20,e21),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax14) ).
cnf(242,axiom,
h2(e10) = op2(e20,e22),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax15) ).
cnf(249,axiom,
h3(e11) = op2(op2(e20,e23),e23),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax16) ).
cnf(250,plain,
h3(e11) = op2(e21,e23),
inference('REWRITE',[status(thm)],[249,234,theory(equality)]) ).
cnf(253,axiom,
h4(e10) = op2(e21,e20),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax17) ).
cnf(256,axiom,
h5(e12) = e21,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax18) ).
cnf(257,axiom,
h5(e13) = e22,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax18) ).
cnf(258,axiom,
h5(e10) = op2(e21,e22),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax18) ).
cnf(259,axiom,
h5(e11) = op2(op2(e21,e22),e22),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax18) ).
cnf(260,plain,
h5(e11) = op2(h5(e10),e22),
inference('REWRITE',[status(thm)],[259,258,theory(equality)]) ).
cnf(269,axiom,
h7(e10) = op2(e22,e20),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax20) ).
cnf(274,axiom,
h8(e10) = op2(e22,e21),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax21) ).
cnf(285,axiom,
h10(e10) = op2(e23,e20),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax23) ).
cnf(290,axiom,
h11(e10) = op2(e23,e21),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax24) ).
cnf(295,axiom,
h12(e10) = op2(e23,e22),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax25) ).
cnf(296,axiom,
h12(e11) = op2(op2(e23,e22),e22),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax25) ).
cnf(297,plain,
h12(e11) = op2(h12(e10),e22),
inference('REWRITE',[status(thm)],[296,295,theory(equality)]) ).
cnf(560,negated_conjecture,
( h5(op1(e10,e10)) != op2(h5(e10),h5(e10))
| h5(op1(e10,e11)) != op2(h5(e10),h5(e11))
| h5(op1(e10,e12)) != op2(h5(e10),h5(e12))
| h5(op1(e10,e13)) != op2(h5(e10),h5(e13))
| h5(op1(e11,e10)) != op2(h5(e11),h5(e10))
| h5(op1(e11,e11)) != op2(h5(e11),h5(e11))
| h5(op1(e11,e12)) != op2(h5(e11),h5(e12))
| h5(op1(e11,e13)) != op2(h5(e11),h5(e13))
| h5(op1(e12,e10)) != op2(h5(e12),h5(e10))
| h5(op1(e12,e11)) != op2(h5(e12),h5(e11))
| h5(op1(e12,e12)) != op2(h5(e12),h5(e12))
| h5(op1(e12,e13)) != op2(h5(e12),h5(e13))
| h5(op1(e13,e10)) != op2(h5(e13),h5(e10))
| h5(op1(e13,e11)) != op2(h5(e13),h5(e11))
| h5(op1(e13,e12)) != op2(h5(e13),h5(e12))
| h5(op1(e13,e13)) != op2(h5(e13),h5(e13))
| h5(e10) != e20
| h5(e12) != e21
| h5(e13) != e22
| h5(e11) != e23 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1) ).
cnf(561,plain,
( h5(e10) != op2(h5(e10),h5(e10))
| h5(op1(e10,e11)) != op2(h5(e10),h5(e11))
| h5(op1(e10,e12)) != op2(h5(e10),e21)
| h5(op1(e11,e10)) != op2(h5(e11),h5(e10))
| h5(e11) != op2(h5(e11),h5(e11))
| h5(op1(e11,e12)) != op2(h5(e11),e21)
| h5(op1(e11,e13)) != op2(h5(e11),e22)
| h5(op1(e12,e10)) != op2(e21,h5(e10))
| h5(op1(e12,e11)) != op2(e21,h5(e11))
| h5(op1(e13,e10)) != op2(e22,h5(e10))
| h5(op1(e13,e11)) != op2(e22,h5(e11))
| h5(op1(e13,e12)) != h8(e10)
| h5(e10) != e20
| h5(e11) != e23 ),
inference('REWRITE',[status(thm)],[560,227,224,274,258,229,226,223,222,260,257,231,256,221,theory(equality)]) ).
cnf(1041,plain,
h7(e10) != h10(e10),
inference('REWRITE',[status(thm)],[150,285,269,theory(equality)]) ).
cnf(1053,plain,
h2(e10) != h5(e10),
inference('REWRITE',[status(thm)],[157,258,242,theory(equality)]) ).
cnf(1057,plain,
h1(e10) != h11(e10),
inference('REWRITE',[status(thm)],[153,290,237,theory(equality)]) ).
cnf(1083,plain,
( h10(e10) = e20
| h11(e10) = e20
| h12(e10) = e20 ),
inference('REWRITE',[status(thm)],[89,201,295,290,285,228,theory(equality)]) ).
cnf(1084,plain,
( h10(e10) = e21
| h11(e10) = e21
| h12(e10) = e21 ),
inference('REWRITE',[status(thm)],[91,203,295,290,285,228,theory(equality)]) ).
cnf(1085,plain,
( h10(e10) = e22
| h11(e10) = e22
| h12(e10) = e22 ),
inference('REWRITE',[status(thm)],[93,204,295,290,285,228,theory(equality)]) ).
cnf(1086,plain,
h3(e11) = e22,
inference('REWRITE',[status(thm)],[94,204,200,232,250,202,234,228,theory(equality)]) ).
cnf(1087,plain,
op2(e21,e23) = e22,
inference('REWRITE',[status(thm)],[250,1086,theory(equality)]) ).
cnf(1108,plain,
( h7(e10) = e21
| h8(e10) = e21 ),
inference('REWRITE',[status(thm)],[83,199,232,202,274,269,227,theory(equality)]) ).
cnf(1110,plain,
( h7(e10) = e23
| h8(e10) = e23 ),
inference('REWRITE',[status(thm)],[87,201,232,204,274,269,227,theory(equality)]) ).
cnf(1112,plain,
h2(e10) != e22,
inference('REWRITE',[status(thm)],[158,242,227,theory(equality)]) ).
cnf(1114,plain,
h12(e10) != e22,
inference('REWRITE',[status(thm)],[162,295,227,theory(equality)]) ).
cnf(1115,plain,
( h10(e10) = e22
| h11(e10) = e22 ),
inference('REWRITE',[status(thm)],[1085,1114]) ).
cnf(1121,plain,
( h4(e10) = e20
| h5(e10) = e20 ),
inference('REWRITE',[status(thm)],[73,200,1087,258,199,253,226,theory(equality)]) ).
cnf(1124,plain,
( h4(e10) = e23
| h5(e10) = e23 ),
inference('REWRITE',[status(thm)],[79,204,1087,258,203,253,226,theory(equality)]) ).
cnf(1126,plain,
h8(e10) != e21,
inference('REWRITE',[status(thm)],[154,274,226,theory(equality)]) ).
cnf(1127,plain,
h7(e10) = e21,
inference('REWRITE',[status(thm)],[1108,1126]) ).
cnf(1128,plain,
op2(e22,e20) = e21,
inference('REWRITE',[status(thm)],[269,1127,theory(equality)]) ).
cnf(1133,plain,
h10(e10) != e21,
inference('REWRITE',[status(thm)],[1041,1127,theory(equality)]) ).
cnf(1134,plain,
( h11(e10) = e21
| h12(e10) = e21 ),
inference('REWRITE',[status(thm)],[1084,1133]) ).
cnf(1141,plain,
h8(e10) = e23,
inference('REWRITE',[status(thm)],[1110,203,1127,theory(equality)]) ).
cnf(1145,plain,
( h5(e10) != op2(h5(e10),h5(e10))
| h5(op1(e10,e11)) != op2(h5(e10),h5(e11))
| h5(op1(e10,e12)) != op2(h5(e10),e21)
| h5(op1(e11,e10)) != op2(h5(e11),h5(e10))
| h5(e11) != op2(h5(e11),h5(e11))
| h5(op1(e11,e12)) != op2(h5(e11),e21)
| h5(op1(e11,e13)) != op2(h5(e11),e22)
| h5(op1(e12,e10)) != op2(e21,h5(e10))
| h5(op1(e12,e11)) != op2(e21,h5(e11))
| h5(op1(e13,e10)) != op2(e22,h5(e10))
| h5(op1(e13,e11)) != op2(e22,h5(e11))
| h5(op1(e13,e12)) != e23
| h5(e10) != e20
| h5(e11) != e23 ),
inference('REWRITE',[status(thm)],[561,1141,theory(equality)]) ).
cnf(1155,plain,
h11(e10) != e21,
inference('REWRITE',[status(thm)],[155,290,226,theory(equality)]) ).
cnf(1157,plain,
h12(e10) = e21,
inference('REWRITE',[status(thm)],[1134,1155]) ).
cnf(1158,plain,
op2(e23,e22) = e21,
inference('REWRITE',[status(thm)],[295,1157,theory(equality)]) ).
cnf(1159,plain,
h12(e11) = h5(e10),
inference('REWRITE',[status(thm)],[297,258,1157,theory(equality)]) ).
cnf(1161,plain,
h5(e11) = op2(h12(e11),e22),
inference('REWRITE',[status(thm)],[260,1159,theory(equality)]) ).
cnf(1163,plain,
h2(e10) != h12(e11),
inference('REWRITE',[status(thm)],[1053,1159,theory(equality)]) ).
cnf(1167,plain,
( h4(e10) = e20
| h12(e11) = e20 ),
inference('REWRITE',[status(thm)],[1121,1159,theory(equality)]) ).
cnf(1168,plain,
( h4(e10) = e23
| h12(e11) = e23 ),
inference('REWRITE',[status(thm)],[1124,1159,theory(equality)]) ).
cnf(1170,plain,
( h12(e11) != op2(h12(e11),h12(e11))
| h5(op1(e10,e11)) != op2(h12(e11),h5(e11))
| h5(op1(e10,e12)) != op2(h12(e11),e21)
| h5(op1(e11,e10)) != op2(h5(e11),h12(e11))
| h5(e11) != op2(h5(e11),h5(e11))
| h5(op1(e11,e12)) != op2(h5(e11),e21)
| h5(op1(e11,e13)) != op2(h5(e11),e22)
| h5(op1(e12,e10)) != op2(e21,h12(e11))
| h5(op1(e12,e11)) != op2(e21,h5(e11))
| h5(op1(e13,e10)) != op2(e22,h12(e11))
| h5(op1(e13,e11)) != op2(e22,h5(e11))
| h5(op1(e13,e12)) != e23
| h12(e11) != e20
| h5(e11) != e23 ),
inference('REWRITE',[status(thm)],[1145,1159,theory(equality)]) ).
cnf(1177,plain,
( h10(e10) = e20
| h11(e10) = e20 ),
inference('REWRITE',[status(thm)],[1083,199,1157,theory(equality)]) ).
cnf(1183,plain,
h1(e10) = e22,
inference('REWRITE',[status(thm)],[69,202,234,1112,242,237,200,225,theory(equality)]) ).
cnf(1184,plain,
op2(e20,e21) = e22,
inference('REWRITE',[status(thm)],[237,1183,theory(equality)]) ).
cnf(1189,plain,
h11(e10) != e22,
inference('REWRITE',[status(thm)],[1057,1183,theory(equality)]) ).
cnf(1190,plain,
h10(e10) = e22,
inference('REWRITE',[status(thm)],[1115,1189]) ).
cnf(1191,plain,
op2(e23,e20) = e22,
inference('REWRITE',[status(thm)],[285,1190,theory(equality)]) ).
cnf(1194,plain,
h11(e10) = e20,
inference('REWRITE',[status(thm)],[1177,200,1190,theory(equality)]) ).
cnf(1195,plain,
op2(e23,e21) = e20,
inference('REWRITE',[status(thm)],[290,1194,theory(equality)]) ).
cnf(1207,plain,
h2(e10) = e23,
inference('REWRITE',[status(thm)],[71,203,234,242,204,1184,201,225,theory(equality)]) ).
cnf(1208,plain,
op2(e20,e22) = e23,
inference('REWRITE',[status(thm)],[242,1207,theory(equality)]) ).
cnf(1211,plain,
h12(e11) != e23,
inference('REWRITE',[status(thm)],[1163,1207,theory(equality)]) ).
cnf(1212,plain,
h4(e10) = e23,
inference('REWRITE',[status(thm)],[1168,1211]) ).
cnf(1213,plain,
op2(e21,e20) = e23,
inference('REWRITE',[status(thm)],[253,1212,theory(equality)]) ).
cnf(1216,plain,
h12(e11) = e20,
inference('REWRITE',[status(thm)],[1167,201,1212,theory(equality)]) ).
cnf(1217,plain,
h5(e10) = e20,
inference('REWRITE',[status(thm)],[1159,1216,theory(equality)]) ).
cnf(1219,plain,
h5(e11) = e23,
inference('REWRITE',[status(thm)],[1161,1208,1216,theory(equality)]) ).
cnf(1220,plain,
( h5(op1(e10,e11)) != e21
| h5(op1(e10,e12)) != e22
| h5(op1(e11,e10)) != e22
| h5(op1(e11,e12)) != e20
| h5(op1(e11,e13)) != e21
| h5(op1(e12,e10)) != e23
| h5(op1(e12,e11)) != e22
| h5(op1(e13,e10)) != e21
| h5(op1(e13,e11)) != e20
| h5(op1(e13,e12)) != e23 ),
inference('REWRITE',[status(thm)],[1170,232,1128,1087,1213,1158,1195,228,1191,1184,234,1219,225,1216,theory(equality)]) ).
cnf(1232,plain,
( op1(e13,e10) = e10
| op1(e13,e11) = e10
| op1(e13,e12) = e10 ),
inference('REWRITE',[status(thm)],[41,195,224,theory(equality)]) ).
cnf(1233,plain,
( op1(e13,e10) = e11
| op1(e13,e11) = e11
| op1(e13,e12) = e11 ),
inference('REWRITE',[status(thm)],[43,197,224,theory(equality)]) ).
cnf(1234,plain,
( op1(e13,e10) = e12
| op1(e13,e11) = e12
| op1(e13,e12) = e12 ),
inference('REWRITE',[status(thm)],[45,198,224,theory(equality)]) ).
cnf(1235,plain,
op1(e11,e13) = e12,
inference('REWRITE',[status(thm)],[46,198,194,229,196,231,224,theory(equality)]) ).
cnf(1240,plain,
( h5(op1(e10,e11)) != e21
| h5(op1(e10,e12)) != e22
| h5(op1(e11,e10)) != e22
| h5(op1(e11,e12)) != e20
| h5(op1(e12,e10)) != e23
| h5(op1(e12,e11)) != e22
| h5(op1(e13,e10)) != e21
| h5(op1(e13,e11)) != e20
| h5(op1(e13,e12)) != e23 ),
inference('REWRITE',[status(thm)],[1220,256,1235,theory(equality)]) ).
cnf(1259,plain,
( op1(e12,e10) = e11
| op1(e12,e11) = e11 ),
inference('REWRITE',[status(thm)],[35,193,229,196,223,theory(equality)]) ).
cnf(1261,plain,
( op1(e12,e10) = e13
| op1(e12,e11) = e13 ),
inference('REWRITE',[status(thm)],[39,195,229,198,223,theory(equality)]) ).
cnf(1263,plain,
op1(e10,e12) != e12,
inference('REWRITE',[status(thm)],[110,223,theory(equality)]) ).
cnf(1265,plain,
op1(e13,e12) != e12,
inference('REWRITE',[status(thm)],[114,223,theory(equality)]) ).
cnf(1266,plain,
( op1(e13,e10) = e12
| op1(e13,e11) = e12 ),
inference('REWRITE',[status(thm)],[1234,1265]) ).
cnf(1272,plain,
( op1(e11,e10) = e10
| op1(e11,e12) = e10 ),
inference('REWRITE',[status(thm)],[25,194,1235,193,222,theory(equality)]) ).
cnf(1275,plain,
( op1(e11,e10) = e13
| op1(e11,e12) = e13 ),
inference('REWRITE',[status(thm)],[31,198,1235,197,222,theory(equality)]) ).
cnf(1277,plain,
op1(e12,e11) != e11,
inference('REWRITE',[status(thm)],[106,222,theory(equality)]) ).
cnf(1278,plain,
op1(e12,e10) = e11,
inference('REWRITE',[status(thm)],[1259,1277]) ).
cnf(1281,plain,
op1(e13,e10) != e11,
inference('REWRITE',[status(thm)],[102,1278,theory(equality)]) ).
cnf(1282,plain,
( op1(e13,e11) = e11
| op1(e13,e12) = e11 ),
inference('REWRITE',[status(thm)],[1233,1281]) ).
cnf(1284,plain,
( h5(op1(e10,e11)) != e21
| h5(op1(e10,e12)) != e22
| h5(op1(e11,e10)) != e22
| h5(op1(e11,e12)) != e20
| h5(op1(e12,e11)) != e22
| h5(op1(e13,e10)) != e21
| h5(op1(e13,e11)) != e20
| h5(op1(e13,e12)) != e23 ),
inference('REWRITE',[status(thm)],[1240,1219,1278,theory(equality)]) ).
cnf(1296,plain,
op1(e12,e11) = e13,
inference('REWRITE',[status(thm)],[1261,197,1278,theory(equality)]) ).
cnf(1299,plain,
( h5(op1(e10,e11)) != e21
| h5(op1(e10,e12)) != e22
| h5(op1(e11,e10)) != e22
| h5(op1(e11,e12)) != e20
| h5(op1(e13,e10)) != e21
| h5(op1(e13,e11)) != e20
| h5(op1(e13,e12)) != e23 ),
inference('REWRITE',[status(thm)],[1284,257,1296,theory(equality)]) ).
cnf(1311,plain,
op1(e13,e11) != e11,
inference('REWRITE',[status(thm)],[107,222,theory(equality)]) ).
cnf(1313,plain,
op1(e13,e12) = e11,
inference('REWRITE',[status(thm)],[1282,1311]) ).
cnf(1316,plain,
( op1(e13,e10) = e10
| op1(e13,e11) = e10 ),
inference('REWRITE',[status(thm)],[1232,193,1313,theory(equality)]) ).
cnf(1318,plain,
( h5(op1(e10,e11)) != e21
| h5(op1(e10,e12)) != e22
| h5(op1(e11,e10)) != e22
| h5(op1(e11,e12)) != e20
| h5(op1(e13,e10)) != e21
| h5(op1(e13,e11)) != e20 ),
inference('REWRITE',[status(thm)],[1299,1219,1313,theory(equality)]) ).
cnf(1330,plain,
op1(e10,e11) = e12,
inference('REWRITE',[status(thm)],[21,196,231,1263,194,221,theory(equality)]) ).
cnf(1331,plain,
op1(e13,e11) != e12,
inference('REWRITE',[status(thm)],[105,1330,theory(equality)]) ).
cnf(1332,plain,
op1(e13,e10) = e12,
inference('REWRITE',[status(thm)],[1266,1331]) ).
cnf(1333,plain,
op1(e13,e11) = e10,
inference('REWRITE',[status(thm)],[1316,194,1332,theory(equality)]) ).
cnf(1334,plain,
( h5(op1(e10,e12)) != e22
| h5(op1(e11,e10)) != e22
| h5(op1(e11,e12)) != e20 ),
inference('REWRITE',[status(thm)],[1318,1217,1333,1332,256,1330,theory(equality)]) ).
cnf(1346,plain,
op1(e10,e12) = e13,
inference('REWRITE',[status(thm)],[23,197,231,198,1330,195,221,theory(equality)]) ).
cnf(1347,plain,
op1(e11,e12) != e13,
inference('REWRITE',[status(thm)],[109,1346,theory(equality)]) ).
cnf(1348,plain,
op1(e11,e10) = e13,
inference('REWRITE',[status(thm)],[1275,1347]) ).
cnf(1349,plain,
op1(e11,e12) = e10,
inference('REWRITE',[status(thm)],[1272,195,1348,theory(equality)]) ).
cnf(1350,plain,
$false,
inference('REWRITE',[status(thm)],[1334,1217,1349,1348,257,1346,theory(equality)]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : ALG113+1 : TPTP v8.1.0. Released v2.7.0.
% 0.03/0.13 % Command : run-snark %s %d
% 0.12/0.33 % Computer : n024.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 600
% 0.12/0.33 % DateTime : Wed Jun 8 05:29:34 EDT 2022
% 0.12/0.34 % CPUTime :
% 0.19/0.45 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.46 *
% 0.19/0.46 *
% 0.19/0.46 #<PACKAGE "SNARK-USER">
% 0.19/0.46 *
% 0.19/0.46 SNARK-TPTP-OPTIONS
% 0.19/0.46 *
% 0.19/0.46 ((AGENDA-LENGTH-LIMIT NIL) (AGENDA-LENGTH-BEFORE-SIMPLIFICATION-LIMIT NIL)
% 0.19/0.46 (USE-HYPERRESOLUTION T) (USE-UR-RESOLUTION T) (USE-PARAMODULATION T)
% 0.19/0.46 (USE-FACTORING :POS)
% 0.19/0.46 (USE-LITERAL-ORDERING-WITH-HYPERRESOLUTION 'LITERAL-ORDERING-P)
% 0.19/0.46 (USE-LITERAL-ORDERING-WITH-PARAMODULATION 'LITERAL-ORDERING-P)
% 0.19/0.46 (ORDERING-FUNCTIONS>CONSTANTS T) (ASSERT-CONTEXT :CURRENT)
% 0.19/0.46 (RUN-TIME-LIMIT 300) (LISTEN-FOR-COMMANDS NIL)
% 0.19/0.46 (USE-CLOSURE-WHEN-SATISFIABLE T) (PRINT-ROWS-WHEN-GIVEN NIL)
% 0.19/0.46 (PRINT-ROWS-WHEN-DERIVED NIL) (PRINT-UNORIENTABLE-ROWS NIL)
% 0.19/0.46 (PRINT-ROW-WFFS-PRETTILY NIL) (PRINT-FINAL-ROWS :TPTP)
% 0.19/0.46 (PRINT-OPTIONS-WHEN-STARTING NIL) (USE-VARIABLE-NAME-SORTS NIL)
% 0.19/0.46 (USE-PURITY-TEST T) (USE-RELEVANCE-TEST T) (DECLARE-TPTP-SYMBOLS1)
% 0.19/0.46 (DECLARE-TPTP-SYMBOLS2))
% 0.19/0.46 *
% 0.19/0.46 "."
% 0.19/0.46 *
% 0.19/0.46 ; Begin refute-file /export/starexec/sandbox2/benchmark/theBenchmark.p 2022-06-08T05:29:35
% 0.19/0.46 ; Running SNARK from /davis/home/graph/tptp/Systems/SNARK---20120808r022/Source/snark-system.lisp in SBCL 1.0.12 on n024.cluster.edu at 2022-06-08T05:29:35
% 2.98/3.16
% 2.98/3.16
% 2.98/3.16 #||
% 2.98/3.16 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 2.98/3.16 % SZS output start Refutation
% See solution above
% 2.98/3.18 ||#
% 2.98/3.18
% 2.98/3.18 ; Summary of computation:
% 2.98/3.18 ; 4254 formulas have been input or derived (from 1 formulas).
% 2.98/3.18 ; 1350 (32%) were retained. Of these,
% 2.98/3.18 ; 1241 (92%) were simplified or subsumed later,
% 2.98/3.18 ; 109 ( 8%) are still being kept.
% 2.98/3.18 ;
% 2.98/3.18 ; Run time in seconds excluding printing time:
% 2.98/3.18 ; 0.065 2% Read assertion file (1 call)
% 2.98/3.18 ; 1.137 42% Assert (26 calls)
% 2.98/3.18 ; 0.171 6% Process new row (3,850 calls)
% 2.98/3.18 ; 0.002 0% Condensing (673 calls)
% 2.98/3.18 ; 0.086 3% Forward subsumption (673 calls)
% 2.98/3.18 ; 0.088 3% Backward subsumption (667 calls)
% 2.98/3.18 ; 0.053 2% Clause clause subsumption (1,018 calls)
% 2.98/3.18 ; 1.026 38% Forward simplification (3,850 calls)
% 2.98/3.18 ; 0.036 1% Backward simplification (964 calls)
% 2.98/3.18 ; 0.000 0% Ordering (106 calls)
% 2.98/3.18 ; 0.000 0% Sortal reasoning (32 calls)
% 2.98/3.18 ; 0.010 0% Purity testing (1 call)
% 2.98/3.18 ; 0.025 1% Other
% 2.98/3.18 ; 2.699 Total
% 2.98/3.18 ; 2.714 Real time
% 2.98/3.18 ;
% 2.98/3.18 ; Term-hash-array has 1,051 terms in all.
% 2.98/3.18 ; Feature-vector-row-index has 0 entries (96 at peak, 667 added, 667 deleted).
% 2.98/3.18 ; Feature-vector-row-index has 1 node (868 at peak, 9,737 added, 9,736 deleted).
% 2.98/3.18 ; Retrieved 438 possibly forward subsuming rows in 673 calls.
% 2.98/3.18 ; Retrieved 593 possibly backward subsumed rows in 667 calls.
% 2.98/3.18 ; Path-index has 196 entries (692 at peak, 3,227 added, 3,031 deleted).
% 2.98/3.18 ; Path-index has 298 nodes (570 at peak, 2,248 added, 1,950 deleted).
% 2.98/3.18 ; Trie-index has 196 entries (692 at peak, 3,227 added, 3,031 deleted).
% 2.98/3.18 ; Trie-index has 329 nodes (1,601 at peak, 6,968 added, 6,639 deleted).
% 2.98/3.18 ; Retrieved 109,696 generalization terms in 309,744 calls.
% 2.98/3.18 ; Retrieved 296 instance terms in 296 calls.
% 2.98/3.18 ;
% 2.98/3.18 ; The agenda of backward simplifiable rows to process has 18 entries:
% 2.98/3.18 ; 18 with value 0
% 2.98/3.18 ; The agenda of input rows to give has 108 entries:
% 2.98/3.18 ; 28 with value 4 48 with value 6 32 with value 7
% 2.98/3.18 Evaluation took:
% 2.98/3.18 2.714 seconds of real time
% 2.98/3.18 2.678334 seconds of user run time
% 2.98/3.18 0.035185 seconds of system run time
% 2.98/3.18 [Run times include 0.04 seconds GC run time.]
% 2.98/3.18 0 calls to %EVAL
% 2.98/3.18 0 page faults and
% 2.98/3.18 158,635,416 bytes consed.
% 2.98/3.18 :PROOF-FOUND
% 2.98/3.18 ; End refute-file /export/starexec/sandbox2/benchmark/theBenchmark.p 2022-06-08T05:29:37
% 2.98/3.18 :PROOF-FOUND
% 2.98/3.18 *
%------------------------------------------------------------------------------