%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : TOP051-1 : TPTP v9.3.1. Released v8.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n014.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 03:54:48 PM UTC 2026
% Result : Unsatisfiable 6.98s 1.67s
% Output : CNFRefutation 6.98s
% Verified :
% SZS Type : Refutation
% Derivation depth : 57
% Number of leaves : 14
% Syntax : Number of clauses : 260 ( 260 unt; 0 nHn; 240 RR)
% Number of literals : 260 ( 259 equ; 19 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 11 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 12 con; 0-2 aty)
% Number of variables : 32 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t1,axiom,
product(a1,a6) = a2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t75,plain,
product(a1,a6) = a2,
inference(orient,[status(thm)],[t1]) ).
cnf(t11,axiom,
product(product(X1,X2),X2) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t34,plain,
product(product(X1,X2),X2) = X1,
inference(orient,[status(thm)],[t11]) ).
cnf(t12,axiom,
product(product(X1,X2),product(X3,X2)) = product(product(X1,X3),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t83,plain,
product(product(X1,X2),product(X3,X2)) = product(product(X1,X3),X2),
inference(orient,[status(thm)],[t12]) ).
cnf(t0,axiom,
product(X1,X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t33,plain,
product(X1,X1) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t84,plain,
product(product(X1,X2),X1) = product(X1,product(X2,X1)),
inference(cp,[status(thm)],[t83,t33]) ).
cnf(t167,plain,
product(product(X1,X2),X1) = product(X1,product(X2,X1)),
inference(orient,[status(thm)],[t84]) ).
cnf(t76,plain,
a1 = product(a2,a6),
inference(cp,[status(thm)],[t34,t75]) ).
cnf(t140,plain,
product(a2,a6) = a1,
inference(orient,[status(thm)],[t76]) ).
cnf(t183,plain,
product(a2,product(a6,a2)) = product(a1,a2),
inference(cp,[status(thm)],[t167,t140]) ).
cnf(t7,axiom,
product(a6,a2) = a7,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t77,plain,
product(a6,a2) = a7,
inference(orient,[status(thm)],[t7]) ).
cnf(t996,plain,
product(a2,a7) = product(a1,a2),
inference(step,[status(thm)],[t183,t77]) ).
cnf(t3,axiom,
product(a2,a7) = a3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t79,plain,
product(a2,a7) = a3,
inference(orient,[status(thm)],[t3]) ).
cnf(t997,plain,
a3 = product(a1,a2),
inference(step,[status(thm)],[t996,t79]) ).
cnf(t216,plain,
product(a1,a2) = a3,
inference(orient,[status(thm)],[t997]) ).
cnf(t217,plain,
product(a1,product(a2,a1)) = product(a3,a1),
inference(cp,[status(thm)],[t167,t216]) ).
cnf(t4,axiom,
product(a3,a1) = a4,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t99,plain,
product(a3,a1) = a4,
inference(orient,[status(thm)],[t4]) ).
cnf(t1005,plain,
product(a1,product(a2,a1)) = a4,
inference(step,[status(thm)],[t217,t99]) ).
cnf(t248,plain,
product(a1,product(a2,a1)) = a4,
inference(orient,[status(thm)],[t1005]) ).
cnf(t249,plain,
a1 = product(a4,product(a2,a1)),
inference(cp,[status(thm)],[t34,t248]) ).
cnf(t264,plain,
product(a4,product(a2,a1)) = a1,
inference(orient,[status(thm)],[t249]) ).
cnf(t88,plain,
product(product(a1,X1),a6) = product(a2,product(X1,a6)),
inference(cp,[status(thm)],[t83,t75]) ).
cnf(t368,plain,
product(product(a1,X1),a6) = product(a2,product(X1,a6)),
inference(orient,[status(thm)],[t88]) ).
cnf(t371,plain,
product(a2,product(a2,a6)) = product(a3,a6),
inference(cp,[status(thm)],[t368,t216]) ).
cnf(t1022,plain,
product(a2,a1) = product(a3,a6),
inference(step,[status(thm)],[t371,t140]) ).
cnf(t376,plain,
product(a2,a1) = product(a3,a6),
inference(orient,[status(thm)],[t1022]) ).
cnf(t1025,plain,
product(a4,product(a3,a6)) = a1,
inference(step,[status(thm)],[t264,t376]) ).
cnf(t384,plain,
product(a4,product(a3,a6)) = a1,
inference(rw,[status(thm)],[t1025]) ).
cnf(t409,plain,
product(a4,product(a3,a6)) = a1,
inference(orient,[status(thm)],[t384]) ).
cnf(t90,plain,
product(product(product(X1,X2),X3),X2) = product(X1,product(X3,X2)),
inference(cp,[status(thm)],[t83,t34]) ).
cnf(t640,plain,
product(product(product(X1,X2),X3),X2) = product(X1,product(X3,X2)),
inference(orient,[status(thm)],[t90]) ).
cnf(t1026,plain,
product(a1,product(a3,a6)) = a4,
inference(step,[status(thm)],[t248,t376]) ).
cnf(t385,plain,
product(a1,product(a3,a6)) = a4,
inference(rw,[status(thm)],[t1026]) ).
cnf(t414,plain,
product(a1,product(a3,a6)) = a4,
inference(orient,[status(thm)],[t385]) ).
cnf(t415,plain,
product(a2,product(product(a3,a6),a6)) = product(a4,a6),
inference(cp,[status(thm)],[t368,t414]) ).
cnf(t1033,plain,
product(a2,a3) = product(a4,a6),
inference(step,[status(thm)],[t415,t34]) ).
cnf(t80,plain,
a2 = product(a3,a7),
inference(cp,[status(thm)],[t34,t79]) ).
cnf(t146,plain,
product(a3,a7) = a2,
inference(orient,[status(thm)],[t80]) ).
cnf(t179,plain,
product(a3,product(a7,a3)) = product(a2,a3),
inference(cp,[status(thm)],[t167,t146]) ).
cnf(t8,axiom,
product(a7,a3) = a8,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t81,plain,
product(a7,a3) = a8,
inference(orient,[status(thm)],[t8]) ).
cnf(t1000,plain,
product(a3,a8) = product(a2,a3),
inference(step,[status(thm)],[t179,t81]) ).
cnf(t228,plain,
product(a2,a3) = product(a3,a8),
inference(orient,[status(thm)],[t1000]) ).
cnf(t1034,plain,
product(a3,a8) = product(a4,a6),
inference(step,[status(thm)],[t1033,t228]) ).
cnf(t418,plain,
product(a3,a8) = product(a4,a6),
inference(orient,[status(thm)],[t1034]) ).
cnf(t423,plain,
a3 = product(product(a4,a6),a8),
inference(cp,[status(thm)],[t34,t418]) ).
cnf(t439,plain,
product(product(a4,a6),a8) = a3,
inference(orient,[status(thm)],[t423]) ).
cnf(t646,plain,
product(a4,product(a8,a6)) = product(a3,a6),
inference(cp,[status(thm)],[t640,t439]) ).
cnf(t9,axiom,
product(a8,a6) = a9,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t107,plain,
product(a8,a6) = a9,
inference(orient,[status(thm)],[t9]) ).
cnf(t1100,plain,
product(a4,a9) = product(a3,a6),
inference(step,[status(thm)],[t646,t107]) ).
cnf(t5,axiom,
product(a4,a10) = a5,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t103,plain,
product(a4,a10) = a5,
inference(orient,[status(thm)],[t5]) ).
cnf(t176,plain,
product(a4,product(a10,a4)) = product(a5,a4),
inference(cp,[status(thm)],[t167,t103]) ).
cnf(t10,axiom,
product(a9,a4) = a10,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t115,plain,
product(a9,a4) = a10,
inference(orient,[status(thm)],[t10]) ).
cnf(t116,plain,
a9 = product(a10,a4),
inference(cp,[status(thm)],[t34,t115]) ).
cnf(t164,plain,
product(a10,a4) = a9,
inference(orient,[status(thm)],[t116]) ).
cnf(t999,plain,
product(a4,a9) = product(a5,a4),
inference(step,[status(thm)],[t176,t164]) ).
cnf(t224,plain,
product(a4,a9) = product(a5,a4),
inference(orient,[status(thm)],[t999]) ).
cnf(t1101,plain,
product(a5,a4) = product(a3,a6),
inference(step,[status(thm)],[t1100,t224]) ).
cnf(t770,plain,
product(a3,a6) = product(a5,a4),
inference(orient,[status(thm)],[t1101]) ).
cnf(t1111,plain,
product(a4,product(a5,a4)) = a1,
inference(step,[status(thm)],[t409,t770]) ).
cnf(t225,plain,
a4 = product(product(a5,a4),a9),
inference(cp,[status(thm)],[t34,t224]) ).
cnf(t252,plain,
product(product(a5,a4),a9) = a4,
inference(orient,[status(thm)],[t225]) ).
cnf(t6,axiom,
product(a5,a9) = a6,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t73,plain,
product(a5,a9) = a6,
inference(orient,[status(thm)],[t6]) ).
cnf(t89,plain,
product(product(a5,X1),a9) = product(a6,product(X1,a9)),
inference(cp,[status(thm)],[t83,t73]) ).
cnf(t576,plain,
product(product(a5,X1),a9) = product(a6,product(X1,a9)),
inference(orient,[status(thm)],[t89]) ).
cnf(t1077,plain,
product(a6,product(a4,a9)) = a4,
inference(step,[status(thm)],[t252,t576]) ).
cnf(t1078,plain,
product(a6,product(a5,a4)) = a4,
inference(step,[status(thm)],[t1077,t224]) ).
cnf(t585,plain,
product(a6,product(a5,a4)) = a4,
inference(rw,[status(thm)],[t1078]) ).
cnf(t586,plain,
product(a6,product(a5,a4)) = a4,
inference(orient,[status(thm)],[t585]) ).
cnf(t587,plain,
a6 = product(a4,product(a5,a4)),
inference(cp,[status(thm)],[t34,t586]) ).
cnf(t592,plain,
product(a4,product(a5,a4)) = a6,
inference(orient,[status(thm)],[t587]) ).
cnf(t1112,plain,
a6 = a1,
inference(step,[status(thm)],[t1111,t592]) ).
cnf(t785,plain,
a6 = a1,
inference(rw,[status(thm)],[t1112]) ).
cnf(t787,plain,
a1 = a6,
inference(orient,[status(thm)],[t785]) ).
cnf(t1137,plain,
product(a6,a6) = a2,
inference(step,[status(thm)],[t75,t787]) ).
cnf(t1138,plain,
a6 = a2,
inference(step,[status(thm)],[t1137,t33]) ).
cnf(t803,plain,
a6 = a2,
inference(rw,[status(thm)],[t1138]) ).
cnf(t871,plain,
a2 = a6,
inference(orient,[status(thm)],[t803]) ).
cnf(t184,plain,
product(a6,product(a2,a6)) = product(a7,a6),
inference(cp,[status(thm)],[t167,t77]) ).
cnf(t1001,plain,
product(a6,a1) = product(a7,a6),
inference(step,[status(thm)],[t184,t140]) ).
cnf(t232,plain,
product(a6,a1) = product(a7,a6),
inference(orient,[status(thm)],[t1001]) ).
cnf(t233,plain,
a6 = product(product(a7,a6),a1),
inference(cp,[status(thm)],[t34,t232]) ).
cnf(t256,plain,
product(product(a7,a6),a1) = a6,
inference(orient,[status(thm)],[t233]) ).
cnf(t87,plain,
product(product(a6,X1),a2) = product(a7,product(X1,a2)),
inference(cp,[status(thm)],[t83,t77]) ).
cnf(t337,plain,
product(product(a6,X1),a2) = product(a7,product(X1,a2)),
inference(orient,[status(thm)],[t87]) ).
cnf(t78,plain,
a6 = product(a7,a2),
inference(cp,[status(thm)],[t34,t77]) ).
cnf(t143,plain,
product(a7,a2) = a6,
inference(orient,[status(thm)],[t78]) ).
cnf(t181,plain,
product(a7,product(a2,a7)) = product(a6,a7),
inference(cp,[status(thm)],[t167,t143]) ).
cnf(t992,plain,
product(a7,a3) = product(a6,a7),
inference(step,[status(thm)],[t181,t79]) ).
cnf(t993,plain,
a8 = product(a6,a7),
inference(step,[status(thm)],[t992,t81]) ).
cnf(t207,plain,
product(a6,a7) = a8,
inference(orient,[status(thm)],[t993]) ).
cnf(t341,plain,
product(a7,product(a7,a2)) = product(a8,a2),
inference(cp,[status(thm)],[t337,t207]) ).
cnf(t1015,plain,
product(a7,a6) = product(a8,a2),
inference(step,[status(thm)],[t341,t143]) ).
cnf(t347,plain,
product(a7,a6) = product(a8,a2),
inference(orient,[status(thm)],[t1015]) ).
cnf(t1020,plain,
product(product(a8,a2),a1) = a6,
inference(step,[status(thm)],[t256,t347]) ).
cnf(t357,plain,
product(product(a8,a2),a1) = a6,
inference(rw,[status(thm)],[t1020]) ).
cnf(t386,plain,
product(product(a8,a2),a1) = a6,
inference(orient,[status(thm)],[t357]) ).
cnf(t1144,plain,
product(product(a8,a2),a6) = a6,
inference(step,[status(thm)],[t386,t787]) ).
cnf(t350,plain,
a7 = product(product(a8,a2),a6),
inference(cp,[status(thm)],[t34,t347]) ).
cnf(t359,plain,
product(product(a8,a2),a6) = a7,
inference(orient,[status(thm)],[t350]) ).
cnf(t1145,plain,
a7 = a6,
inference(step,[status(thm)],[t1144,t359]) ).
cnf(t807,plain,
a7 = a6,
inference(rw,[status(thm)],[t1145]) ).
cnf(t85,plain,
product(product(a7,X1),a3) = product(a8,product(X1,a3)),
inference(cp,[status(thm)],[t83,t81]) ).
cnf(t311,plain,
product(product(a7,X1),a3) = product(a8,product(X1,a3)),
inference(orient,[status(thm)],[t85]) ).
cnf(t312,plain,
product(a8,product(a2,a3)) = product(a6,a3),
inference(cp,[status(thm)],[t311,t143]) ).
cnf(t1010,plain,
product(a8,product(a3,a8)) = product(a6,a3),
inference(step,[status(thm)],[t312,t228]) ).
cnf(t82,plain,
a7 = product(a8,a3),
inference(cp,[status(thm)],[t34,t81]) ).
cnf(t149,plain,
product(a8,a3) = a7,
inference(orient,[status(thm)],[t82]) ).
cnf(t175,plain,
product(a8,product(a3,a8)) = product(a7,a8),
inference(cp,[status(thm)],[t167,t149]) ).
cnf(t278,plain,
product(a8,product(a3,a8)) = product(a7,a8),
inference(orient,[status(thm)],[t175]) ).
cnf(t1011,plain,
product(a7,a8) = product(a6,a3),
inference(step,[status(thm)],[t1010,t278]) ).
cnf(t317,plain,
product(a6,a3) = product(a7,a8),
inference(orient,[status(thm)],[t1011]) ).
cnf(t338,plain,
product(a7,product(a3,a2)) = product(product(a7,a8),a2),
inference(cp,[status(thm)],[t337,t317]) ).
cnf(t182,plain,
product(a2,product(a7,a2)) = product(a3,a2),
inference(cp,[status(thm)],[t167,t79]) ).
cnf(t994,plain,
product(a2,a6) = product(a3,a2),
inference(step,[status(thm)],[t182,t143]) ).
cnf(t995,plain,
a1 = product(a3,a2),
inference(step,[status(thm)],[t994,t140]) ).
cnf(t211,plain,
product(a3,a2) = a1,
inference(orient,[status(thm)],[t995]) ).
cnf(t1047,plain,
product(a7,a1) = product(product(a7,a8),a2),
inference(step,[status(thm)],[t338,t211]) ).
cnf(t208,plain,
product(a6,product(a7,a6)) = product(a8,a6),
inference(cp,[status(thm)],[t167,t207]) ).
cnf(t1004,plain,
product(a6,product(a7,a6)) = a9,
inference(step,[status(thm)],[t208,t107]) ).
cnf(t244,plain,
product(a6,product(a7,a6)) = a9,
inference(orient,[status(thm)],[t1004]) ).
cnf(t1021,plain,
product(a6,product(a8,a2)) = a9,
inference(step,[status(thm)],[t244,t347]) ).
cnf(t358,plain,
product(a6,product(a8,a2)) = a9,
inference(rw,[status(thm)],[t1021]) ).
cnf(t390,plain,
product(a6,product(a8,a2)) = a9,
inference(orient,[status(thm)],[t358]) ).
cnf(t391,plain,
product(a7,product(product(a8,a2),a2)) = product(a9,a2),
inference(cp,[status(thm)],[t337,t390]) ).
cnf(t1027,plain,
product(a7,a8) = product(a9,a2),
inference(step,[status(thm)],[t391,t34]) ).
cnf(t394,plain,
product(a7,a8) = product(a9,a2),
inference(orient,[status(thm)],[t1027]) ).
cnf(t1048,plain,
product(a7,a1) = product(product(a9,a2),a2),
inference(step,[status(thm)],[t1047,t394]) ).
cnf(t1049,plain,
product(a7,a1) = a9,
inference(step,[status(thm)],[t1048,t34]) ).
cnf(t451,plain,
product(a7,a1) = a9,
inference(orient,[status(thm)],[t1049]) ).
cnf(t452,plain,
a7 = product(a9,a1),
inference(cp,[status(thm)],[t34,t451]) ).
cnf(t457,plain,
product(a9,a1) = a7,
inference(orient,[status(thm)],[t452]) ).
cnf(t1122,plain,
product(a9,a6) = a7,
inference(step,[status(thm)],[t457,t787]) ).
cnf(t108,plain,
a8 = product(a9,a6),
inference(cp,[status(thm)],[t34,t107]) ).
cnf(t158,plain,
product(a9,a6) = a8,
inference(orient,[status(thm)],[t108]) ).
cnf(t1123,plain,
a8 = a7,
inference(step,[status(thm)],[t1122,t158]) ).
cnf(t795,plain,
a8 = a7,
inference(rw,[status(thm)],[t1123]) ).
cnf(t810,plain,
a7 = a8,
inference(orient,[status(thm)],[t795]) ).
cnf(t1252,plain,
a8 = a6,
inference(step,[status(thm)],[t807,t810]) ).
cnf(t882,plain,
a6 = a8,
inference(orient,[status(thm)],[t1252]) ).
cnf(t1267,plain,
a2 = a8,
inference(step,[status(thm)],[t871,t882]) ).
cnf(t897,plain,
a2 = a8,
inference(orient,[status(thm)],[t1267]) ).
cnf(t454,plain,
product(a7,product(a1,a7)) = product(a9,a7),
inference(cp,[status(thm)],[t167,t451]) ).
cnf(t86,plain,
product(product(a2,X1),a7) = product(a3,product(X1,a7)),
inference(cp,[status(thm)],[t83,t79]) ).
cnf(t321,plain,
product(product(a2,X1),a7) = product(a3,product(X1,a7)),
inference(orient,[status(thm)],[t86]) ).
cnf(t323,plain,
product(a3,product(a6,a7)) = product(a1,a7),
inference(cp,[status(thm)],[t321,t140]) ).
cnf(t1012,plain,
product(a3,a8) = product(a1,a7),
inference(step,[status(thm)],[t323,t207]) ).
cnf(t328,plain,
product(a1,a7) = product(a3,a8),
inference(orient,[status(thm)],[t1012]) ).
cnf(t1037,plain,
product(a1,a7) = product(a4,a6),
inference(step,[status(thm)],[t328,t418]) ).
cnf(t421,plain,
product(a1,a7) = product(a4,a6),
inference(orient,[status(thm)],[t1037]) ).
cnf(t1065,plain,
product(a7,product(a4,a6)) = product(a9,a7),
inference(step,[status(thm)],[t454,t421]) ).
cnf(t530,plain,
product(a7,product(a4,a6)) = product(a9,a7),
inference(orient,[status(thm)],[t1065]) ).
cnf(t532,plain,
product(a8,product(product(a4,a6),a3)) = product(product(a9,a7),a3),
inference(cp,[status(thm)],[t311,t530]) ).
cnf(t424,plain,
product(a3,product(a8,a3)) = product(product(a4,a6),a3),
inference(cp,[status(thm)],[t167,t418]) ).
cnf(t1045,plain,
product(a3,a7) = product(product(a4,a6),a3),
inference(step,[status(thm)],[t424,t149]) ).
cnf(t1046,plain,
a2 = product(product(a4,a6),a3),
inference(step,[status(thm)],[t1045,t146]) ).
cnf(t443,plain,
product(product(a4,a6),a3) = a2,
inference(orient,[status(thm)],[t1046]) ).
cnf(t1066,plain,
product(a8,a2) = product(product(a9,a7),a3),
inference(step,[status(thm)],[t532,t443]) ).
cnf(t546,plain,
product(product(a9,a7),a3) = product(a8,a2),
inference(orient,[status(thm)],[t1066]) ).
cnf(t547,plain,
product(a9,a7) = product(product(a8,a2),a3),
inference(cp,[status(thm)],[t34,t546]) ).
cnf(t351,plain,
product(a8,product(a6,a3)) = product(product(a8,a2),a3),
inference(cp,[status(thm)],[t311,t347]) ).
cnf(t1054,plain,
product(a8,product(a7,a8)) = product(product(a8,a2),a3),
inference(step,[status(thm)],[t351,t317]) ).
cnf(t180,plain,
product(a7,product(a3,a7)) = product(a8,a7),
inference(cp,[status(thm)],[t167,t81]) ).
cnf(t990,plain,
product(a7,a2) = product(a8,a7),
inference(step,[status(thm)],[t180,t146]) ).
cnf(t991,plain,
a6 = product(a8,a7),
inference(step,[status(thm)],[t990,t143]) ).
cnf(t202,plain,
product(a8,a7) = a6,
inference(orient,[status(thm)],[t991]) ).
cnf(t204,plain,
product(a8,product(a7,a8)) = product(a6,a8),
inference(cp,[status(thm)],[t167,t202]) ).
cnf(t300,plain,
product(a8,product(a7,a8)) = product(a6,a8),
inference(orient,[status(thm)],[t204]) ).
cnf(t1055,plain,
product(a6,a8) = product(product(a8,a2),a3),
inference(step,[status(thm)],[t1054,t300]) ).
cnf(t482,plain,
product(product(a8,a2),a3) = product(a6,a8),
inference(orient,[status(thm)],[t1055]) ).
cnf(t1067,plain,
product(a9,a7) = product(a6,a8),
inference(step,[status(thm)],[t547,t482]) ).
cnf(t551,plain,
product(a6,a8) = product(a9,a7),
inference(orient,[status(thm)],[t1067]) ).
cnf(t558,plain,
a6 = product(product(a9,a7),a8),
inference(cp,[status(thm)],[t34,t551]) ).
cnf(t564,plain,
product(product(a9,a7),a8) = a6,
inference(orient,[status(thm)],[t558]) ).
cnf(t1189,plain,
product(product(a9,a8),a8) = a6,
inference(step,[status(thm)],[t564,t810]) ).
cnf(t1190,plain,
a9 = a6,
inference(step,[status(thm)],[t1189,t34]) ).
cnf(t845,plain,
a9 = a6,
inference(rw,[status(thm)],[t1190]) ).
cnf(t1288,plain,
a9 = a8,
inference(step,[status(thm)],[t845,t882]) ).
cnf(t914,plain,
a8 = a9,
inference(orient,[status(thm)],[t1288]) ).
cnf(t1311,plain,
a2 = a9,
inference(step,[status(thm)],[t897,t914]) ).
cnf(t933,plain,
a2 = a9,
inference(orient,[status(thm)],[t1311]) ).
cnf(t1307,plain,
a7 = a9,
inference(step,[status(thm)],[t810,t914]) ).
cnf(t929,plain,
a7 = a9,
inference(orient,[status(thm)],[t1307]) ).
cnf(t1313,plain,
a6 = a9,
inference(step,[status(thm)],[t882,t914]) ).
cnf(t935,plain,
a6 = a9,
inference(orient,[status(thm)],[t1313]) ).
cnf(t1132,plain,
product(a6,a2) = a3,
inference(step,[status(thm)],[t216,t787]) ).
cnf(t1133,plain,
a7 = a3,
inference(step,[status(thm)],[t1132,t77]) ).
cnf(t800,plain,
a7 = a3,
inference(rw,[status(thm)],[t1133]) ).
cnf(t1206,plain,
a8 = a3,
inference(step,[status(thm)],[t800,t810]) ).
cnf(t854,plain,
a3 = a8,
inference(orient,[status(thm)],[t1206]) ).
cnf(t1309,plain,
a3 = a9,
inference(step,[status(thm)],[t854,t914]) ).
cnf(t931,plain,
a3 = a9,
inference(orient,[status(thm)],[t1309]) ).
cnf(t1207,plain,
product(product(a4,a6),a8) = a8,
inference(step,[status(thm)],[t439,t854]) ).
cnf(t855,plain,
product(product(a4,a6),a8) = a8,
inference(orient,[status(thm)],[t1207]) ).
cnf(t1286,plain,
product(product(a4,a8),a8) = a8,
inference(step,[status(thm)],[t855,t882]) ).
cnf(t1287,plain,
a4 = a8,
inference(step,[status(thm)],[t1286,t34]) ).
cnf(t913,plain,
a4 = a8,
inference(rw,[status(thm)],[t1287]) ).
cnf(t1335,plain,
a4 = a9,
inference(step,[status(thm)],[t913,t914]) ).
cnf(t952,plain,
a4 = a9,
inference(orient,[status(thm)],[t1335]) ).
cnf(t1243,plain,
product(a6,product(a8,a6)) = a9,
inference(step,[status(thm)],[t390,t871]) ).
cnf(t1244,plain,
product(a6,a9) = a9,
inference(step,[status(thm)],[t1243,t107]) ).
cnf(t74,plain,
a5 = product(a6,a9),
inference(cp,[status(thm)],[t34,t73]) ).
cnf(t137,plain,
product(a6,a9) = a5,
inference(orient,[status(thm)],[t74]) ).
cnf(t1245,plain,
a5 = a9,
inference(step,[status(thm)],[t1244,t137]) ).
cnf(t879,plain,
a5 = a9,
inference(rw,[status(thm)],[t1245]) ).
cnf(t940,plain,
a5 = a9,
inference(orient,[status(thm)],[t879]) ).
cnf(t1321,plain,
product(a4,a9) = product(a9,a4),
inference(step,[status(thm)],[t224,t940]) ).
cnf(t1322,plain,
product(a4,a9) = a10,
inference(step,[status(thm)],[t1321,t115]) ).
cnf(t943,plain,
product(a4,a9) = a10,
inference(orient,[status(thm)],[t1322]) ).
cnf(t1336,plain,
product(a9,a9) = a10,
inference(step,[status(thm)],[t943,t952]) ).
cnf(t1337,plain,
a9 = a10,
inference(step,[status(thm)],[t1336,t33]) ).
cnf(t953,plain,
a9 = a10,
inference(rw,[status(thm)],[t1337]) ).
cnf(t965,plain,
a10 = a9,
inference(orient,[status(thm)],[t953]) ).
cnf(t104,plain,
a4 = product(a5,a10),
inference(cp,[status(thm)],[t34,t103]) ).
cnf(t155,plain,
product(a5,a10) = a4,
inference(orient,[status(thm)],[t104]) ).
cnf(t1327,plain,
product(a9,a10) = a4,
inference(step,[status(thm)],[t155,t940]) ).
cnf(t173,plain,
product(a10,product(a4,a10)) = product(a9,a10),
inference(cp,[status(thm)],[t167,t164]) ).
cnf(t988,plain,
product(a10,a5) = product(a9,a10),
inference(step,[status(thm)],[t173,t103]) ).
cnf(t2,axiom,
product(a10,a5) = a11,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t111,plain,
product(a10,a5) = a11,
inference(orient,[status(thm)],[t2]) ).
cnf(t989,plain,
a11 = product(a9,a10),
inference(step,[status(thm)],[t988,t111]) ).
cnf(t198,plain,
product(a9,a10) = a11,
inference(orient,[status(thm)],[t989]) ).
cnf(t1328,plain,
a11 = a4,
inference(step,[status(thm)],[t1327,t198]) ).
cnf(t947,plain,
a11 = a4,
inference(rw,[status(thm)],[t1328]) ).
cnf(t1345,plain,
a11 = a9,
inference(step,[status(thm)],[t947,t952]) ).
cnf(t959,plain,
a11 = a9,
inference(orient,[status(thm)],[t1345]) ).
cnf(t1265,plain,
a1 = a8,
inference(step,[status(thm)],[t787,t882]) ).
cnf(t895,plain,
a1 = a8,
inference(orient,[status(thm)],[t1265]) ).
cnf(t1305,plain,
a1 = a9,
inference(step,[status(thm)],[t895,t914]) ).
cnf(t927,plain,
a1 = a9,
inference(orient,[status(thm)],[t1305]) ).
cnf(goal_0,negated_conjecture,
ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a2),a7),a6),a3),a8),a4),a5),a10),a11),a9) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a1),a6),a5),a2),a7),a3),a4),a9),a10),a8),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a7),a6),a3),a8),a4),a5),a10),a11),a9) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a1),a6),a5),a2),a7),a3),a4),a9),a10),a8),
inference(rw,[status(thm)],[goal_0,t933]) ).
cnf(g0_1,plain,
ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a6),a3),a8),a4),a5),a10),a11),a9) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a1),a6),a5),a2),a7),a3),a4),a9),a10),a8),
inference(rw,[status(thm)],[g0_0,t929]) ).
cnf(g0_2,plain,
ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a3),a8),a4),a5),a10),a11),a9) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a1),a6),a5),a2),a7),a3),a4),a9),a10),a8),
inference(rw,[status(thm)],[g0_1,t935]) ).
cnf(g0_3,plain,
ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a8),a4),a5),a10),a11),a9) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a1),a6),a5),a2),a7),a3),a4),a9),a10),a8),
inference(rw,[status(thm)],[g0_2,t931]) ).
cnf(g0_4,plain,
ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a4),a5),a10),a11),a9) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a1),a6),a5),a2),a7),a3),a4),a9),a10),a8),
inference(rw,[status(thm)],[g0_3,t914]) ).
cnf(g0_5,plain,
ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a5),a10),a11),a9) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a1),a6),a5),a2),a7),a3),a4),a9),a10),a8),
inference(rw,[status(thm)],[g0_4,t952]) ).
cnf(g0_6,plain,
ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a10),a11),a9) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a1),a6),a5),a2),a7),a3),a4),a9),a10),a8),
inference(rw,[status(thm)],[g0_5,t940]) ).
cnf(g0_7,plain,
ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a11),a9) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a1),a6),a5),a2),a7),a3),a4),a9),a10),a8),
inference(rw,[status(thm)],[g0_6,t965]) ).
cnf(g0_8,plain,
ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a1),a6),a5),a2),a7),a3),a4),a9),a10),a8),
inference(rw,[status(thm)],[g0_7,t959]) ).
cnf(g0_9,plain,
ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a6),a5),a2),a7),a3),a4),a9),a10),a8),
inference(rw,[status(thm)],[g0_8,t927]) ).
cnf(g0_10,plain,
ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a5),a2),a7),a3),a4),a9),a10),a8),
inference(rw,[status(thm)],[g0_9,t935]) ).
cnf(g0_11,plain,
ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a2),a7),a3),a4),a9),a10),a8),
inference(rw,[status(thm)],[g0_10,t940]) ).
cnf(g0_12,plain,
ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a7),a3),a4),a9),a10),a8),
inference(rw,[status(thm)],[g0_11,t933]) ).
cnf(g0_13,plain,
ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a3),a4),a9),a10),a8),
inference(rw,[status(thm)],[g0_12,t929]) ).
cnf(g0_14,plain,
ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a4),a9),a10),a8),
inference(rw,[status(thm)],[g0_13,t931]) ).
cnf(g0_15,plain,
ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a10),a8),
inference(rw,[status(thm)],[g0_14,t952]) ).
cnf(g0_16,plain,
ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a8),
inference(rw,[status(thm)],[g0_15,t965]) ).
cnf(g0_17,plain,
ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),
inference(rw,[status(thm)],[g0_16,t914]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_17]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : TOP051-1 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.36 % Computer : n014.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Fri Sep 25 04:20:02 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 6.98/1.67 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 6.98/1.67 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------