%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : TOP053-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 : n017.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 7.39s 16.89s
% Output : CNFRefutation 7.39s
% Verified :
% SZS Type : Refutation
% Derivation depth : 79
% Number of leaves : 19
% Syntax : Number of clauses : 276 ( 276 unt; 0 nHn; 252 RR)
% Number of literals : 276 ( 275 equ; 27 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 15 ( 3 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 18 ( 18 usr; 16 con; 0-2 aty)
% Number of variables : 32 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t17,axiom,
product(product(X1,X2),product(X3,X2)) = product(product(X1,X3),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t54,plain,
product(product(X1,X2),product(X3,X2)) = product(product(X1,X3),X2),
inference(orient,[status(thm)],[t17]) ).
cnf(t14,axiom,
product(a8,a2) = a9,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t32,plain,
product(a8,a2) = a9,
inference(orient,[status(thm)],[t14]) ).
cnf(t82,plain,
product(product(a8,X1),a2) = product(a9,product(X1,a2)),
inference(cp,[status(thm)],[t54,t32]) ).
cnf(t590,plain,
product(product(a8,X1),a2) = product(a9,product(X1,a2)),
inference(orient,[status(thm)],[t82]) ).
cnf(t0,axiom,
product(X1,X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t18,plain,
product(X1,X1) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t55,plain,
product(product(X1,X2),X1) = product(X1,product(X2,X1)),
inference(cp,[status(thm)],[t54,t18]) ).
cnf(t131,plain,
product(product(X1,X2),X1) = product(X1,product(X2,X1)),
inference(orient,[status(thm)],[t55]) ).
cnf(t16,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)],[t16]) ).
cnf(t11,axiom,
product(a5,a6) = a7,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t29,plain,
product(a5,a6) = a7,
inference(orient,[status(thm)],[t11]) ).
cnf(t45,plain,
a5 = product(a7,a6),
inference(cp,[status(thm)],[t34,t29]) ).
cnf(t116,plain,
product(a7,a6) = a5,
inference(orient,[status(thm)],[t45]) ).
cnf(t159,plain,
product(a7,product(a6,a7)) = product(a5,a7),
inference(cp,[status(thm)],[t131,t116]) ).
cnf(t12,axiom,
product(a6,a7) = a2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t30,plain,
product(a6,a7) = a2,
inference(orient,[status(thm)],[t12]) ).
cnf(t791,plain,
product(a7,a2) = product(a5,a7),
inference(step,[status(thm)],[t159,t30]) ).
cnf(t183,plain,
product(a5,a7) = product(a7,a2),
inference(orient,[status(thm)],[t791]) ).
cnf(t1,axiom,
product(a1,a2) = a3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t19,plain,
product(a1,a2) = a3,
inference(orient,[status(thm)],[t1]) ).
cnf(t57,plain,
product(product(X1,a1),a2) = product(product(X1,a2),a3),
inference(cp,[status(thm)],[t54,t19]) ).
cnf(t199,plain,
product(product(X1,a1),a2) = product(product(X1,a2),a3),
inference(orient,[status(thm)],[t57]) ).
cnf(t15,axiom,
product(a9,a1) = a10,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t33,plain,
product(a9,a1) = a10,
inference(orient,[status(thm)],[t15]) ).
cnf(t200,plain,
product(product(a9,a2),a3) = product(a10,a2),
inference(cp,[status(thm)],[t199,t33]) ).
cnf(t48,plain,
a8 = product(a9,a2),
inference(cp,[status(thm)],[t34,t32]) ).
cnf(t125,plain,
product(a9,a2) = a8,
inference(orient,[status(thm)],[t48]) ).
cnf(t794,plain,
product(a8,a3) = product(a10,a2),
inference(step,[status(thm)],[t200,t125]) ).
cnf(t13,axiom,
product(a7,a3) = a8,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t31,plain,
product(a7,a3) = a8,
inference(orient,[status(thm)],[t13]) ).
cnf(t47,plain,
a7 = product(a8,a3),
inference(cp,[status(thm)],[t34,t31]) ).
cnf(t122,plain,
product(a8,a3) = a7,
inference(orient,[status(thm)],[t47]) ).
cnf(t795,plain,
a7 = product(a10,a2),
inference(step,[status(thm)],[t794,t122]) ).
cnf(t206,plain,
product(a10,a2) = a7,
inference(orient,[status(thm)],[t795]) ).
cnf(t207,plain,
a10 = product(a7,a2),
inference(cp,[status(thm)],[t34,t206]) ).
cnf(t218,plain,
product(a7,a2) = a10,
inference(orient,[status(thm)],[t207]) ).
cnf(t796,plain,
product(a5,a7) = a10,
inference(step,[status(thm)],[t183,t218]) ).
cnf(t219,plain,
product(a5,a7) = a10,
inference(orient,[status(thm)],[t796]) ).
cnf(t376,plain,
product(a7,a6) = a8,
inference(rw,[status(thm)],[t31]) ).
cnf(t826,plain,
a5 = a8,
inference(step,[status(thm)],[t376,t116]) ).
cnf(t415,plain,
a5 = a8,
inference(orient,[status(thm)],[t826]) ).
cnf(t831,plain,
product(a8,a7) = a10,
inference(step,[status(thm)],[t219,t415]) ).
cnf(t422,plain,
product(a8,a7) = a10,
inference(rw,[status(thm)],[t831]) ).
cnf(t485,plain,
product(a8,a7) = a10,
inference(orient,[status(thm)],[t422]) ).
cnf(t593,plain,
product(a9,product(a7,a2)) = product(a10,a2),
inference(cp,[status(thm)],[t590,t485]) ).
cnf(t908,plain,
product(a9,a10) = product(a10,a2),
inference(step,[status(thm)],[t593,t218]) ).
cnf(t49,plain,
a9 = product(a10,a1),
inference(cp,[status(thm)],[t34,t33]) ).
cnf(t128,plain,
product(a10,a1) = a9,
inference(orient,[status(thm)],[t49]) ).
cnf(t163,plain,
product(a10,product(a1,a10)) = product(a9,a10),
inference(cp,[status(thm)],[t131,t128]) ).
cnf(t3,axiom,
product(a11,a10) = a1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t21,plain,
product(a11,a10) = a1,
inference(orient,[status(thm)],[t3]) ).
cnf(t37,plain,
a11 = product(a1,a10),
inference(cp,[status(thm)],[t34,t21]) ).
cnf(t52,plain,
product(a1,a10) = a11,
inference(orient,[status(thm)],[t37]) ).
cnf(t792,plain,
product(a10,a11) = product(a9,a10),
inference(step,[status(thm)],[t163,t52]) ).
cnf(t2,axiom,
product(a10,a11) = a12,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t20,plain,
product(a10,a11) = a12,
inference(orient,[status(thm)],[t2]) ).
cnf(t793,plain,
a12 = product(a9,a10),
inference(step,[status(thm)],[t792,t20]) ).
cnf(t187,plain,
product(a9,a10) = a12,
inference(orient,[status(thm)],[t793]) ).
cnf(t10,axiom,
product(a4,a7) = a11,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t28,plain,
product(a4,a7) = a11,
inference(orient,[status(thm)],[t10]) ).
cnf(t75,plain,
product(product(X1,a4),a7) = product(product(X1,a7),a11),
inference(cp,[status(thm)],[t54,t28]) ).
cnf(t343,plain,
product(product(X1,a4),a7) = product(product(X1,a7),a11),
inference(orient,[status(thm)],[t75]) ).
cnf(t9,axiom,
product(a3,a4) = a5,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t27,plain,
product(a3,a4) = a5,
inference(orient,[status(thm)],[t9]) ).
cnf(t43,plain,
a3 = product(a5,a4),
inference(cp,[status(thm)],[t34,t27]) ).
cnf(t110,plain,
product(a5,a4) = a3,
inference(orient,[status(thm)],[t43]) ).
cnf(t345,plain,
product(product(a5,a7),a11) = product(a3,a7),
inference(cp,[status(thm)],[t343,t110]) ).
cnf(t801,plain,
product(a10,a11) = product(a3,a7),
inference(step,[status(thm)],[t345,t219]) ).
cnf(t802,plain,
a12 = product(a3,a7),
inference(step,[status(thm)],[t801,t20]) ).
cnf(t352,plain,
product(a3,a7) = a12,
inference(orient,[status(thm)],[t802]) ).
cnf(t395,plain,
product(a6,a7) = a12,
inference(rw,[status(thm)],[t352]) ).
cnf(t839,plain,
a2 = a12,
inference(step,[status(thm)],[t395,t30]) ).
cnf(t455,plain,
a12 = a2,
inference(orient,[status(thm)],[t839]) ).
cnf(t847,plain,
product(a9,a10) = a2,
inference(step,[status(thm)],[t187,t455]) ).
cnf(t464,plain,
product(a9,a10) = a2,
inference(orient,[status(thm)],[t847]) ).
cnf(t909,plain,
a2 = product(a10,a2),
inference(step,[status(thm)],[t908,t464]) ).
cnf(t910,plain,
a2 = a7,
inference(step,[status(thm)],[t909,t206]) ).
cnf(t598,plain,
a2 = a7,
inference(orient,[status(thm)],[t910]) ).
cnf(t539,plain,
product(a8,a7) = a2,
inference(rw,[status(thm)],[t30]) ).
cnf(t56,plain,
product(product(a1,X1),a2) = product(a3,product(X1,a2)),
inference(cp,[status(thm)],[t54,t19]) ).
cnf(t191,plain,
product(product(a1,X1),a2) = product(a3,product(X1,a2)),
inference(orient,[status(thm)],[t56]) ).
cnf(t4,axiom,
product(a12,a3) = a13,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t22,plain,
product(a12,a3) = a13,
inference(orient,[status(thm)],[t4]) ).
cnf(t62,plain,
product(product(a12,X1),a3) = product(a13,product(X1,a3)),
inference(cp,[status(thm)],[t54,t22]) ).
cnf(t249,plain,
product(product(a12,X1),a3) = product(a13,product(X1,a3)),
inference(orient,[status(thm)],[t62]) ).
cnf(t353,plain,
a3 = product(a12,a7),
inference(cp,[status(thm)],[t34,t352]) ).
cnf(t365,plain,
product(a12,a7) = a3,
inference(orient,[status(thm)],[t353]) ).
cnf(t369,plain,
product(a13,product(a7,a3)) = product(a3,a3),
inference(cp,[status(thm)],[t249,t365]) ).
cnf(t803,plain,
product(a13,a8) = product(a3,a3),
inference(step,[status(thm)],[t369,t31]) ).
cnf(t5,axiom,
product(a13,a8) = a6,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t23,plain,
product(a13,a8) = a6,
inference(orient,[status(thm)],[t5]) ).
cnf(t804,plain,
a6 = product(a3,a3),
inference(step,[status(thm)],[t803,t23]) ).
cnf(t805,plain,
a6 = a3,
inference(step,[status(thm)],[t804,t18]) ).
cnf(t370,plain,
a3 = a6,
inference(orient,[status(thm)],[t805]) ).
cnf(t817,plain,
product(product(a1,X1),a2) = product(a6,product(X1,a2)),
inference(step,[status(thm)],[t191,t370]) ).
cnf(t383,plain,
product(product(a1,X1),a2) = product(a6,product(X1,a2)),
inference(orient,[status(thm)],[t817]) ).
cnf(t78,plain,
product(product(a6,X1),a7) = product(a2,product(X1,a7)),
inference(cp,[status(thm)],[t54,t30]) ).
cnf(t444,plain,
product(product(a6,X1),a7) = product(a2,product(X1,a7)),
inference(orient,[status(thm)],[t78]) ).
cnf(t35,plain,
a1 = product(a3,a2),
inference(cp,[status(thm)],[t34,t19]) ).
cnf(t50,plain,
product(a3,a2) = a1,
inference(orient,[status(thm)],[t35]) ).
cnf(t811,plain,
product(a6,a2) = a1,
inference(step,[status(thm)],[t50,t370]) ).
cnf(t377,plain,
product(a6,a2) = a1,
inference(rw,[status(thm)],[t811]) ).
cnf(t430,plain,
product(a6,a2) = a1,
inference(orient,[status(thm)],[t377]) ).
cnf(t447,plain,
product(a2,product(a2,a7)) = product(a1,a7),
inference(cp,[status(thm)],[t444,t430]) ).
cnf(t46,plain,
a6 = product(a2,a7),
inference(cp,[status(thm)],[t34,t30]) ).
cnf(t119,plain,
product(a2,a7) = a6,
inference(orient,[status(thm)],[t46]) ).
cnf(t862,plain,
product(a2,a6) = product(a1,a7),
inference(step,[status(thm)],[t447,t119]) ).
cnf(t143,plain,
product(a6,product(a7,a6)) = product(a2,a6),
inference(cp,[status(thm)],[t131,t30]) ).
cnf(t789,plain,
product(a6,a5) = product(a2,a6),
inference(step,[status(thm)],[t143,t116]) ).
cnf(t175,plain,
product(a2,a6) = product(a6,a5),
inference(orient,[status(thm)],[t789]) ).
cnf(t420,plain,
product(a2,a6) = product(a6,a8),
inference(orient,[status(thm)],[t175]) ).
cnf(t863,plain,
product(a6,a8) = product(a1,a7),
inference(step,[status(thm)],[t862,t420]) ).
cnf(t39,plain,
a13 = product(a6,a8),
inference(cp,[status(thm)],[t34,t23]) ).
cnf(t98,plain,
product(a6,a8) = a13,
inference(orient,[status(thm)],[t39]) ).
cnf(t864,plain,
a13 = product(a1,a7),
inference(step,[status(thm)],[t863,t98]) ).
cnf(t512,plain,
product(a1,a7) = a13,
inference(orient,[status(thm)],[t864]) ).
cnf(t517,plain,
product(a6,product(a7,a2)) = product(a13,a2),
inference(cp,[status(thm)],[t383,t512]) ).
cnf(t935,plain,
product(a6,a10) = product(a13,a2),
inference(step,[status(thm)],[t517,t218]) ).
cnf(t133,plain,
product(a10,product(a11,a10)) = product(a12,a10),
inference(cp,[status(thm)],[t131,t20]) ).
cnf(t786,plain,
product(a10,a1) = product(a12,a10),
inference(step,[status(thm)],[t133,t21]) ).
cnf(t787,plain,
a9 = product(a12,a10),
inference(step,[status(thm)],[t786,t128]) ).
cnf(t167,plain,
product(a12,a10) = a9,
inference(orient,[status(thm)],[t787]) ).
cnf(t844,plain,
product(a2,a10) = a9,
inference(step,[status(thm)],[t167,t455]) ).
cnf(t461,plain,
product(a2,a10) = a9,
inference(rw,[status(thm)],[t844]) ).
cnf(t529,plain,
product(a2,a10) = a9,
inference(orient,[status(thm)],[t461]) ).
cnf(t532,plain,
product(a2,product(a10,a2)) = product(a9,a2),
inference(cp,[status(thm)],[t131,t529]) ).
cnf(t871,plain,
product(a2,a7) = product(a9,a2),
inference(step,[status(thm)],[t532,t206]) ).
cnf(t872,plain,
a6 = product(a9,a2),
inference(step,[status(thm)],[t871,t119]) ).
cnf(t873,plain,
a6 = a8,
inference(step,[status(thm)],[t872,t125]) ).
cnf(t534,plain,
a6 = a8,
inference(orient,[status(thm)],[t873]) ).
cnf(t936,plain,
product(a8,a10) = product(a13,a2),
inference(step,[status(thm)],[t935,t534]) ).
cnf(t808,plain,
product(a12,a6) = a13,
inference(step,[status(thm)],[t22,t370]) ).
cnf(t373,plain,
product(a12,a6) = a13,
inference(rw,[status(thm)],[t808]) ).
cnf(t404,plain,
product(a12,a6) = a13,
inference(orient,[status(thm)],[t373]) ).
cnf(t473,plain,
product(a2,a6) = a13,
inference(rw,[status(thm)],[t404]) ).
cnf(t895,plain,
product(a2,a8) = a13,
inference(step,[status(thm)],[t473,t534]) ).
cnf(t64,plain,
product(product(a13,X1),a8) = product(a6,product(X1,a8)),
inference(cp,[status(thm)],[t54,t23]) ).
cnf(t267,plain,
product(product(a13,X1),a8) = product(a6,product(X1,a8)),
inference(orient,[status(thm)],[t64]) ).
cnf(t38,plain,
a12 = product(a13,a3),
inference(cp,[status(thm)],[t34,t22]) ).
cnf(t53,plain,
product(a13,a3) = a12,
inference(orient,[status(thm)],[t38]) ).
cnf(t812,plain,
product(a13,a6) = a12,
inference(step,[status(thm)],[t53,t370]) ).
cnf(t378,plain,
product(a13,a6) = a12,
inference(rw,[status(thm)],[t812]) ).
cnf(t434,plain,
product(a13,a6) = a12,
inference(orient,[status(thm)],[t378]) ).
cnf(t438,plain,
product(a6,product(a6,a8)) = product(a12,a8),
inference(cp,[status(thm)],[t267,t434]) ).
cnf(t859,plain,
product(a6,a13) = product(a12,a8),
inference(step,[status(thm)],[t438,t98]) ).
cnf(t860,plain,
product(a6,a13) = product(a2,a8),
inference(step,[status(thm)],[t859,t455]) ).
cnf(t494,plain,
product(a2,a8) = product(a6,a13),
inference(orient,[status(thm)],[t860]) ).
cnf(t892,plain,
product(a2,a8) = product(a8,a13),
inference(step,[status(thm)],[t494,t534]) ).
cnf(t567,plain,
product(a2,a8) = product(a8,a13),
inference(orient,[status(thm)],[t892]) ).
cnf(t896,plain,
product(a8,a13) = a13,
inference(step,[status(thm)],[t895,t567]) ).
cnf(t570,plain,
product(a8,a13) = a13,
inference(orient,[status(thm)],[t896]) ).
cnf(t575,plain,
a8 = product(a13,a13),
inference(cp,[status(thm)],[t34,t570]) ).
cnf(t901,plain,
a8 = a13,
inference(step,[status(thm)],[t575,t18]) ).
cnf(t578,plain,
a13 = a8,
inference(orient,[status(thm)],[t901]) ).
cnf(t937,plain,
product(a8,a10) = product(a8,a2),
inference(step,[status(thm)],[t936,t578]) ).
cnf(t938,plain,
product(a8,a10) = product(a8,a7),
inference(step,[status(thm)],[t937,t598]) ).
cnf(t939,plain,
product(a8,a10) = a10,
inference(step,[status(thm)],[t938,t485]) ).
cnf(t640,plain,
product(a8,a10) = a10,
inference(orient,[status(thm)],[t939]) ).
cnf(t641,plain,
a8 = product(a10,a10),
inference(cp,[status(thm)],[t34,t640]) ).
cnf(t940,plain,
a8 = a10,
inference(step,[status(thm)],[t641,t18]) ).
cnf(t646,plain,
a10 = a8,
inference(orient,[status(thm)],[t940]) ).
cnf(t945,plain,
product(a8,a7) = a8,
inference(step,[status(thm)],[t485,t646]) ).
cnf(t654,plain,
product(a8,a7) = a8,
inference(orient,[status(thm)],[t945]) ).
cnf(t954,plain,
a8 = a2,
inference(step,[status(thm)],[t539,t654]) ).
cnf(t955,plain,
a8 = a7,
inference(step,[status(thm)],[t954,t598]) ).
cnf(t666,plain,
a7 = a8,
inference(orient,[status(thm)],[t955]) ).
cnf(t961,plain,
a2 = a8,
inference(step,[status(thm)],[t598,t666]) ).
cnf(t677,plain,
a2 = a8,
inference(orient,[status(thm)],[t961]) ).
cnf(t602,plain,
product(a8,a7) = a9,
inference(rw,[status(thm)],[t32]) ).
cnf(t963,plain,
product(a8,a8) = a9,
inference(step,[status(thm)],[t602,t666]) ).
cnf(t964,plain,
a8 = a9,
inference(step,[status(thm)],[t963,t18]) ).
cnf(t701,plain,
a8 = a9,
inference(orient,[status(thm)],[t964]) ).
cnf(t977,plain,
a2 = a9,
inference(step,[status(thm)],[t677,t701]) ).
cnf(t716,plain,
a2 = a9,
inference(orient,[status(thm)],[t977]) ).
cnf(t886,plain,
a3 = a8,
inference(step,[status(thm)],[t370,t534]) ).
cnf(t555,plain,
a3 = a8,
inference(orient,[status(thm)],[t886]) ).
cnf(t965,plain,
a3 = a9,
inference(step,[status(thm)],[t555,t701]) ).
cnf(t703,plain,
a3 = a9,
inference(orient,[status(thm)],[t965]) ).
cnf(t7,axiom,
product(a15,a8) = a4,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t25,plain,
product(a15,a8) = a4,
inference(orient,[status(thm)],[t7]) ).
cnf(t660,plain,
product(a8,a8) = a4,
inference(rw,[status(thm)],[t25]) ).
cnf(t991,plain,
a8 = a4,
inference(step,[status(thm)],[t660,t18]) ).
cnf(t992,plain,
a9 = a4,
inference(step,[status(thm)],[t991,t701]) ).
cnf(t785,plain,
a4 = a9,
inference(orient,[status(thm)],[t992]) ).
cnf(t967,plain,
a5 = a9,
inference(step,[status(thm)],[t415,t701]) ).
cnf(t705,plain,
a5 = a9,
inference(orient,[status(thm)],[t967]) ).
cnf(t973,plain,
a6 = a9,
inference(step,[status(thm)],[t534,t701]) ).
cnf(t712,plain,
a6 = a9,
inference(orient,[status(thm)],[t973]) ).
cnf(t985,plain,
a7 = a9,
inference(step,[status(thm)],[t666,t701]) ).
cnf(t724,plain,
a7 = a9,
inference(orient,[status(thm)],[t985]) ).
cnf(t981,plain,
a10 = a9,
inference(step,[status(thm)],[t646,t701]) ).
cnf(t720,plain,
a10 = a9,
inference(orient,[status(thm)],[t981]) ).
cnf(t632,plain,
product(a10,a10) = a11,
inference(rw,[status(thm)],[t52]) ).
cnf(t989,plain,
a10 = a11,
inference(step,[status(thm)],[t632,t18]) ).
cnf(t990,plain,
a9 = a11,
inference(step,[status(thm)],[t989,t720]) ).
cnf(t754,plain,
a11 = a9,
inference(orient,[status(thm)],[t990]) ).
cnf(t920,plain,
a12 = a7,
inference(step,[status(thm)],[t455,t598]) ).
cnf(t617,plain,
a12 = a7,
inference(orient,[status(thm)],[t920]) ).
cnf(t957,plain,
a12 = a8,
inference(step,[status(thm)],[t617,t666]) ).
cnf(t671,plain,
a12 = a8,
inference(orient,[status(thm)],[t957]) ).
cnf(t969,plain,
a12 = a9,
inference(step,[status(thm)],[t671,t701]) ).
cnf(t707,plain,
a12 = a9,
inference(orient,[status(thm)],[t969]) ).
cnf(t975,plain,
a13 = a9,
inference(step,[status(thm)],[t578,t701]) ).
cnf(t714,plain,
a13 = a9,
inference(orient,[status(thm)],[t975]) ).
cnf(t8,axiom,
product(a2,a12) = a14,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t26,plain,
product(a2,a12) = a14,
inference(orient,[status(thm)],[t8]) ).
cnf(t458,plain,
product(a2,a2) = a14,
inference(rw,[status(thm)],[t26]) ).
cnf(t868,plain,
a2 = a14,
inference(step,[status(thm)],[t458,t18]) ).
cnf(t524,plain,
a14 = a2,
inference(orient,[status(thm)],[t868]) ).
cnf(t923,plain,
a14 = a7,
inference(step,[status(thm)],[t524,t598]) ).
cnf(t621,plain,
a14 = a7,
inference(orient,[status(thm)],[t923]) ).
cnf(t959,plain,
a14 = a8,
inference(step,[status(thm)],[t621,t666]) ).
cnf(t675,plain,
a14 = a8,
inference(orient,[status(thm)],[t959]) ).
cnf(t971,plain,
a14 = a9,
inference(step,[status(thm)],[t675,t701]) ).
cnf(t710,plain,
a14 = a9,
inference(orient,[status(thm)],[t971]) ).
cnf(t6,axiom,
product(a14,a3) = a15,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t24,plain,
product(a14,a3) = a15,
inference(orient,[status(thm)],[t6]) ).
cnf(t809,plain,
product(a14,a6) = a15,
inference(step,[status(thm)],[t24,t370]) ).
cnf(t374,plain,
product(a14,a6) = a15,
inference(rw,[status(thm)],[t809]) ).
cnf(t408,plain,
product(a14,a6) = a15,
inference(orient,[status(thm)],[t374]) ).
cnf(t525,plain,
product(a2,a6) = a15,
inference(rw,[status(thm)],[t408]) ).
cnf(t949,plain,
product(a7,a6) = a15,
inference(step,[status(thm)],[t525,t598]) ).
cnf(t950,plain,
product(a7,a8) = a15,
inference(step,[status(thm)],[t949,t534]) ).
cnf(t816,plain,
product(a8,a6) = a7,
inference(step,[status(thm)],[t122,t370]) ).
cnf(t382,plain,
product(a8,a6) = a7,
inference(rw,[status(thm)],[t816]) ).
cnf(t452,plain,
product(a8,a6) = a7,
inference(orient,[status(thm)],[t382]) ).
cnf(t454,plain,
product(a8,product(a6,a8)) = product(a7,a8),
inference(cp,[status(thm)],[t131,t452]) ).
cnf(t865,plain,
product(a8,a13) = product(a7,a8),
inference(step,[status(thm)],[t454,t98]) ).
cnf(t518,plain,
product(a7,a8) = product(a8,a13),
inference(orient,[status(thm)],[t865]) ).
cnf(t899,plain,
product(a7,a8) = a13,
inference(step,[status(thm)],[t518,t570]) ).
cnf(t573,plain,
product(a7,a8) = a13,
inference(orient,[status(thm)],[t899]) ).
cnf(t906,plain,
product(a7,a8) = a8,
inference(step,[status(thm)],[t573,t578]) ).
cnf(t587,plain,
product(a7,a8) = a8,
inference(orient,[status(thm)],[t906]) ).
cnf(t951,plain,
a8 = a15,
inference(step,[status(thm)],[t950,t587]) ).
cnf(t659,plain,
a15 = a8,
inference(orient,[status(thm)],[t951]) ).
cnf(t983,plain,
a15 = a9,
inference(step,[status(thm)],[t659,t701]) ).
cnf(t722,plain,
a15 = a9,
inference(orient,[status(thm)],[t983]) ).
cnf(t513,plain,
a1 = product(a13,a7),
inference(cp,[status(thm)],[t34,t512]) ).
cnf(t929,plain,
a1 = product(a8,a7),
inference(step,[status(thm)],[t513,t578]) ).
cnf(t930,plain,
a1 = a10,
inference(step,[status(thm)],[t929,t485]) ).
cnf(t628,plain,
a1 = a10,
inference(orient,[status(thm)],[t930]) ).
cnf(t947,plain,
a1 = a8,
inference(step,[status(thm)],[t628,t646]) ).
cnf(t656,plain,
a1 = a8,
inference(orient,[status(thm)],[t947]) ).
cnf(t979,plain,
a1 = a9,
inference(step,[status(thm)],[t656,t701]) ).
cnf(t718,plain,
a1 = a9,
inference(orient,[status(thm)],[t979]) ).
cnf(goal_0,negated_conjecture,
ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a2),a3),a4),a5),a6),a7),a8),a9),a10),a11),a12),a13),a14),a15) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a1),a2),a3),a4),a5),a6),a7),a8),a9),a10),a11),a12),a13),a14),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a3),a4),a5),a6),a7),a8),a9),a10),a11),a12),a13),a14),a15) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a1),a2),a3),a4),a5),a6),a7),a8),a9),a10),a11),a12),a13),a14),
inference(rw,[status(thm)],[goal_0,t716]) ).
cnf(g0_1,plain,
ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a4),a5),a6),a7),a8),a9),a10),a11),a12),a13),a14),a15) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a1),a2),a3),a4),a5),a6),a7),a8),a9),a10),a11),a12),a13),a14),
inference(rw,[status(thm)],[g0_0,t703]) ).
cnf(g0_2,plain,
ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a5),a6),a7),a8),a9),a10),a11),a12),a13),a14),a15) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a1),a2),a3),a4),a5),a6),a7),a8),a9),a10),a11),a12),a13),a14),
inference(rw,[status(thm)],[g0_1,t785]) ).
cnf(g0_3,plain,
ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a6),a7),a8),a9),a10),a11),a12),a13),a14),a15) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a1),a2),a3),a4),a5),a6),a7),a8),a9),a10),a11),a12),a13),a14),
inference(rw,[status(thm)],[g0_2,t705]) ).
cnf(g0_4,plain,
ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a7),a8),a9),a10),a11),a12),a13),a14),a15) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a1),a2),a3),a4),a5),a6),a7),a8),a9),a10),a11),a12),a13),a14),
inference(rw,[status(thm)],[g0_3,t712]) ).
cnf(g0_5,plain,
ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a8),a9),a10),a11),a12),a13),a14),a15) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a1),a2),a3),a4),a5),a6),a7),a8),a9),a10),a11),a12),a13),a14),
inference(rw,[status(thm)],[g0_4,t724]) ).
cnf(g0_6,plain,
ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a10),a11),a12),a13),a14),a15) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a1),a2),a3),a4),a5),a6),a7),a8),a9),a10),a11),a12),a13),a14),
inference(rw,[status(thm)],[g0_5,t701]) ).
cnf(g0_7,plain,
ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a11),a12),a13),a14),a15) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a1),a2),a3),a4),a5),a6),a7),a8),a9),a10),a11),a12),a13),a14),
inference(rw,[status(thm)],[g0_6,t720]) ).
cnf(g0_8,plain,
ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a12),a13),a14),a15) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a1),a2),a3),a4),a5),a6),a7),a8),a9),a10),a11),a12),a13),a14),
inference(rw,[status(thm)],[g0_7,t754]) ).
cnf(g0_9,plain,
ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a13),a14),a15) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a1),a2),a3),a4),a5),a6),a7),a8),a9),a10),a11),a12),a13),a14),
inference(rw,[status(thm)],[g0_8,t707]) ).
cnf(g0_10,plain,
ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a14),a15) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a1),a2),a3),a4),a5),a6),a7),a8),a9),a10),a11),a12),a13),a14),
inference(rw,[status(thm)],[g0_9,t714]) ).
cnf(g0_11,plain,
ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a15) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a1),a2),a3),a4),a5),a6),a7),a8),a9),a10),a11),a12),a13),a14),
inference(rw,[status(thm)],[g0_10,t710]) ).
cnf(g0_12,plain,
ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a1),a2),a3),a4),a5),a6),a7),a8),a9),a10),a11),a12),a13),a14),
inference(rw,[status(thm)],[g0_11,t722]) ).
cnf(g0_13,plain,
ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a2),a3),a4),a5),a6),a7),a8),a9),a10),a11),a12),a13),a14),
inference(rw,[status(thm)],[g0_12,t718]) ).
cnf(g0_14,plain,
ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a3),a4),a5),a6),a7),a8),a9),a10),a11),a12),a13),a14),
inference(rw,[status(thm)],[g0_13,t716]) ).
cnf(g0_15,plain,
ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a4),a5),a6),a7),a8),a9),a10),a11),a12),a13),a14),
inference(rw,[status(thm)],[g0_14,t703]) ).
cnf(g0_16,plain,
ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a5),a6),a7),a8),a9),a10),a11),a12),a13),a14),
inference(rw,[status(thm)],[g0_15,t785]) ).
cnf(g0_17,plain,
ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a6),a7),a8),a9),a10),a11),a12),a13),a14),
inference(rw,[status(thm)],[g0_16,t705]) ).
cnf(g0_18,plain,
ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a7),a8),a9),a10),a11),a12),a13),a14),
inference(rw,[status(thm)],[g0_17,t712]) ).
cnf(g0_19,plain,
ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a8),a9),a10),a11),a12),a13),a14),
inference(rw,[status(thm)],[g0_18,t724]) ).
cnf(g0_20,plain,
ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a10),a11),a12),a13),a14),
inference(rw,[status(thm)],[g0_19,t701]) ).
cnf(g0_21,plain,
ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a11),a12),a13),a14),
inference(rw,[status(thm)],[g0_20,t720]) ).
cnf(g0_22,plain,
ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a12),a13),a14),
inference(rw,[status(thm)],[g0_21,t754]) ).
cnf(g0_23,plain,
ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a13),a14),
inference(rw,[status(thm)],[g0_22,t707]) ).
cnf(g0_24,plain,
ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a14),
inference(rw,[status(thm)],[g0_23,t714]) ).
cnf(g0_25,plain,
ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),a9),
inference(rw,[status(thm)],[g0_24,t710]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_25]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : TOP053-1 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.11/15.39 % Computer : n017.cluster.edu
% 0.11/15.39 % Model : x86_64 x86_64
% 0.11/15.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/15.39 % Memory : 8046.5625MB
% 0.11/15.39 % OS : Linux 6.8.0-71-generic
% 0.11/15.39 % CPULimit : 300
% 0.11/15.39 % WCLimit : 300
% 0.11/15.39 % DateTime : Fri Sep 25 04:16:02 UTC 2026
% 0.11/15.39 % CPUTime :
% 0.11/15.39 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 7.39/16.89 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.39/16.89 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------