%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : TOP049-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:47 PM UTC 2026
% Result : Unsatisfiable 7.46s 1.66s
% Output : CNFRefutation 7.46s
% Verified :
% SZS Type : Refutation
% Derivation depth : 51
% Number of leaves : 14
% Syntax : Number of clauses : 175 ( 175 unt; 0 nHn; 157 RR)
% Number of literals : 175 ( 174 equ; 17 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 11 con; 0-2 aty)
% Number of variables : 30 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t12,axiom,
product(product(X1,X2),product(X3,X2)) = product(product(X1,X3),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t71,plain,
product(product(X1,X2),product(X3,X2)) = product(product(X1,X3),X2),
inference(orient,[status(thm)],[t12]) ).
cnf(t9,axiom,
product(a8,a9) = a10,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t85,plain,
product(a8,a9) = a10,
inference(orient,[status(thm)],[t9]) ).
cnf(t88,plain,
product(product(X1,a8),a9) = product(product(X1,a9),a10),
inference(cp,[status(thm)],[t71,t85]) ).
cnf(t608,plain,
product(product(X1,a8),a9) = product(product(X1,a9),a10),
inference(orient,[status(thm)],[t88]) ).
cnf(t11,axiom,
product(product(X1,X2),X2) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t32,plain,
product(product(X1,X2),X2) = X1,
inference(orient,[status(thm)],[t11]) ).
cnf(t75,plain,
product(product(product(X1,X2),X3),X2) = product(X1,product(X3,X2)),
inference(cp,[status(thm)],[t71,t32]) ).
cnf(t382,plain,
product(product(product(X1,X2),X3),X2) = product(X1,product(X3,X2)),
inference(orient,[status(thm)],[t75]) ).
cnf(t5,axiom,
product(a4,a8) = a9,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t67,plain,
product(a4,a8) = a9,
inference(orient,[status(thm)],[t5]) ).
cnf(t77,plain,
product(product(X1,a4),a8) = product(product(X1,a8),a9),
inference(cp,[status(thm)],[t71,t67]) ).
cnf(t359,plain,
product(product(X1,a4),a8) = product(product(X1,a8),a9),
inference(orient,[status(thm)],[t77]) ).
cnf(t6,axiom,
product(a5,a4) = a6,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t109,plain,
product(a5,a4) = a6,
inference(orient,[status(thm)],[t6]) ).
cnf(t361,plain,
product(product(a5,a8),a9) = product(a6,a8),
inference(cp,[status(thm)],[t359,t109]) ).
cnf(t377,plain,
product(product(a5,a8),a9) = product(a6,a8),
inference(orient,[status(thm)],[t361]) ).
cnf(t940,plain,
product(product(a5,a9),a10) = product(a6,a8),
inference(step,[status(thm)],[t377,t608]) ).
cnf(t623,plain,
product(product(a5,a9),a10) = product(a6,a8),
inference(rw,[status(thm)],[t940]) ).
cnf(t652,plain,
product(product(a5,a9),a10) = product(a6,a8),
inference(orient,[status(thm)],[t623]) ).
cnf(t653,plain,
product(a5,a9) = product(product(a6,a8),a10),
inference(cp,[status(thm)],[t32,t652]) ).
cnf(t679,plain,
product(product(a6,a8),a10) = product(a5,a9),
inference(orient,[status(thm)],[t653]) ).
cnf(t684,plain,
product(a6,product(a10,a8)) = product(product(a5,a9),a8),
inference(cp,[status(thm)],[t382,t679]) ).
cnf(t0,axiom,
product(X1,X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t31,plain,
product(X1,X1) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t72,plain,
product(product(X1,X2),X1) = product(X1,product(X2,X1)),
inference(cp,[status(thm)],[t71,t31]) ).
cnf(t141,plain,
product(product(X1,X2),X1) = product(X1,product(X2,X1)),
inference(orient,[status(thm)],[t72]) ).
cnf(t8,axiom,
product(a7,a4) = a8,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t89,plain,
product(a7,a4) = a8,
inference(orient,[status(thm)],[t8]) ).
cnf(t90,plain,
a7 = product(a8,a4),
inference(cp,[status(thm)],[t32,t89]) ).
cnf(t161,plain,
product(a8,a4) = a7,
inference(orient,[status(thm)],[t90]) ).
cnf(t162,plain,
product(a8,product(a4,a8)) = product(a7,a8),
inference(cp,[status(thm)],[t141,t161]) ).
cnf(t884,plain,
product(a8,a9) = product(a7,a8),
inference(step,[status(thm)],[t162,t67]) ).
cnf(t885,plain,
a10 = product(a7,a8),
inference(step,[status(thm)],[t884,t85]) ).
cnf(t185,plain,
product(a7,a8) = a10,
inference(orient,[status(thm)],[t885]) ).
cnf(t186,plain,
a7 = product(a10,a8),
inference(cp,[status(thm)],[t32,t185]) ).
cnf(t190,plain,
product(a10,a8) = a7,
inference(orient,[status(thm)],[t186]) ).
cnf(t943,plain,
product(a6,a7) = product(product(a5,a9),a8),
inference(step,[status(thm)],[t684,t190]) ).
cnf(t7,axiom,
product(a6,a1) = a7,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t105,plain,
product(a6,a1) = a7,
inference(orient,[status(thm)],[t7]) ).
cnf(t106,plain,
a6 = product(a7,a1),
inference(cp,[status(thm)],[t32,t105]) ).
cnf(t177,plain,
product(a7,a1) = a6,
inference(orient,[status(thm)],[t106]) ).
cnf(t178,plain,
product(a7,product(a1,a7)) = product(a6,a7),
inference(cp,[status(thm)],[t141,t177]) ).
cnf(t10,axiom,
product(a9,a7) = a1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t69,plain,
product(a9,a7) = a1,
inference(orient,[status(thm)],[t10]) ).
cnf(t70,plain,
a9 = product(a1,a7),
inference(cp,[status(thm)],[t32,t69]) ).
cnf(t132,plain,
product(a1,a7) = a9,
inference(orient,[status(thm)],[t70]) ).
cnf(t888,plain,
product(a7,a9) = product(a6,a7),
inference(step,[status(thm)],[t178,t132]) ).
cnf(t202,plain,
product(a6,a7) = product(a7,a9),
inference(orient,[status(thm)],[t888]) ).
cnf(t87,plain,
product(product(a8,X1),a9) = product(a10,product(X1,a9)),
inference(cp,[status(thm)],[t71,t85]) ).
cnf(t573,plain,
product(product(a8,X1),a9) = product(a10,product(X1,a9)),
inference(orient,[status(thm)],[t87]) ).
cnf(t574,plain,
product(a10,product(a4,a9)) = product(a7,a9),
inference(cp,[status(thm)],[t573,t161]) ).
cnf(t68,plain,
a4 = product(a9,a8),
inference(cp,[status(thm)],[t32,t67]) ).
cnf(t129,plain,
product(a9,a8) = a4,
inference(orient,[status(thm)],[t68]) ).
cnf(t155,plain,
product(a9,product(a8,a9)) = product(a4,a9),
inference(cp,[status(thm)],[t141,t129]) ).
cnf(t886,plain,
product(a9,a10) = product(a4,a9),
inference(step,[status(thm)],[t155,t85]) ).
cnf(t194,plain,
product(a4,a9) = product(a9,a10),
inference(orient,[status(thm)],[t886]) ).
cnf(t924,plain,
product(a10,product(a9,a10)) = product(a7,a9),
inference(step,[status(thm)],[t574,t194]) ).
cnf(t86,plain,
a8 = product(a10,a9),
inference(cp,[status(thm)],[t32,t85]) ).
cnf(t138,plain,
product(a10,a9) = a8,
inference(orient,[status(thm)],[t86]) ).
cnf(t148,plain,
product(a10,product(a9,a10)) = product(a8,a10),
inference(cp,[status(thm)],[t141,t138]) ).
cnf(t230,plain,
product(a10,product(a9,a10)) = product(a8,a10),
inference(orient,[status(thm)],[t148]) ).
cnf(t925,plain,
product(a8,a10) = product(a7,a9),
inference(step,[status(thm)],[t924,t230]) ).
cnf(t581,plain,
product(a7,a9) = product(a8,a10),
inference(orient,[status(thm)],[t925]) ).
cnf(t926,plain,
product(a6,a7) = product(a8,a10),
inference(step,[status(thm)],[t202,t581]) ).
cnf(t582,plain,
product(a6,a7) = product(a8,a10),
inference(orient,[status(thm)],[t926]) ).
cnf(t944,plain,
product(a8,a10) = product(product(a5,a9),a8),
inference(step,[status(thm)],[t943,t582]) ).
cnf(t694,plain,
product(product(a5,a9),a8) = product(a8,a10),
inference(orient,[status(thm)],[t944]) ).
cnf(t696,plain,
product(product(product(a5,a9),a9),a10) = product(product(a8,a10),a9),
inference(cp,[status(thm)],[t608,t694]) ).
cnf(t945,plain,
product(a5,a10) = product(product(a8,a10),a9),
inference(step,[status(thm)],[t696,t32]) ).
cnf(t3,axiom,
product(a2,a10) = a5,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t81,plain,
product(a2,a10) = a5,
inference(orient,[status(thm)],[t3]) ).
cnf(t82,plain,
a2 = product(a5,a10),
inference(cp,[status(thm)],[t32,t81]) ).
cnf(t135,plain,
product(a5,a10) = a2,
inference(orient,[status(thm)],[t82]) ).
cnf(t946,plain,
a2 = product(product(a8,a10),a9),
inference(step,[status(thm)],[t945,t135]) ).
cnf(t947,plain,
a2 = product(a10,product(a10,a9)),
inference(step,[status(thm)],[t946,t573]) ).
cnf(t948,plain,
a2 = product(a10,a8),
inference(step,[status(thm)],[t947,t138]) ).
cnf(t949,plain,
a2 = a7,
inference(step,[status(thm)],[t948,t190]) ).
cnf(t702,plain,
a2 = a7,
inference(orient,[status(thm)],[t949]) ).
cnf(t1,axiom,
product(a1,a2) = a3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t93,plain,
product(a1,a2) = a3,
inference(orient,[status(thm)],[t1]) ).
cnf(t975,plain,
product(a1,a7) = a3,
inference(step,[status(thm)],[t93,t702]) ).
cnf(t976,plain,
a9 = a3,
inference(step,[status(thm)],[t975,t132]) ).
cnf(t721,plain,
a9 = a3,
inference(rw,[status(thm)],[t976]) ).
cnf(t4,axiom,
product(a3,a4) = a2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t101,plain,
product(a3,a4) = a2,
inference(orient,[status(thm)],[t4]) ).
cnf(t102,plain,
a3 = product(a2,a4),
inference(cp,[status(thm)],[t32,t101]) ).
cnf(t173,plain,
product(a2,a4) = a3,
inference(orient,[status(thm)],[t102]) ).
cnf(t971,plain,
product(a7,a4) = a3,
inference(step,[status(thm)],[t173,t702]) ).
cnf(t972,plain,
a8 = a3,
inference(step,[status(thm)],[t971,t89]) ).
cnf(t718,plain,
a8 = a3,
inference(rw,[status(thm)],[t972]) ).
cnf(t732,plain,
a3 = a8,
inference(orient,[status(thm)],[t718]) ).
cnf(t1037,plain,
a9 = a8,
inference(step,[status(thm)],[t721,t732]) ).
cnf(t755,plain,
a8 = a9,
inference(orient,[status(thm)],[t1037]) ).
cnf(t1066,plain,
product(a10,a9) = a7,
inference(step,[status(thm)],[t190,t755]) ).
cnf(t1040,plain,
product(a10,a9) = a9,
inference(step,[status(thm)],[t138,t755]) ).
cnf(t758,plain,
product(a10,a9) = a9,
inference(orient,[status(thm)],[t1040]) ).
cnf(t1067,plain,
a9 = a7,
inference(step,[status(thm)],[t1066,t758]) ).
cnf(t782,plain,
a9 = a7,
inference(rw,[status(thm)],[t1067]) ).
cnf(t837,plain,
a7 = a9,
inference(orient,[status(thm)],[t782]) ).
cnf(t1170,plain,
a2 = a9,
inference(step,[status(thm)],[t702,t837]) ).
cnf(t842,plain,
a2 = a9,
inference(orient,[status(thm)],[t1170]) ).
cnf(t2,axiom,
product(a10,a3) = a4,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t97,plain,
product(a10,a3) = a4,
inference(orient,[status(thm)],[t2]) ).
cnf(t98,plain,
a10 = product(a4,a3),
inference(cp,[status(thm)],[t32,t97]) ).
cnf(t169,plain,
product(a4,a3) = a10,
inference(orient,[status(thm)],[t98]) ).
cnf(t1015,plain,
product(a4,a8) = a10,
inference(step,[status(thm)],[t169,t732]) ).
cnf(t1016,plain,
a9 = a10,
inference(step,[status(thm)],[t1015,t67]) ).
cnf(t743,plain,
a9 = a10,
inference(rw,[status(thm)],[t1016]) ).
cnf(t823,plain,
a10 = a9,
inference(orient,[status(thm)],[t743]) ).
cnf(t1064,plain,
a3 = a9,
inference(step,[status(thm)],[t732,t755]) ).
cnf(t780,plain,
a3 = a9,
inference(orient,[status(thm)],[t1064]) ).
cnf(t174,plain,
product(a2,product(a4,a2)) = product(a3,a2),
inference(cp,[status(thm)],[t141,t173]) ).
cnf(t94,plain,
a1 = product(a3,a2),
inference(cp,[status(thm)],[t32,t93]) ).
cnf(t165,plain,
product(a3,a2) = a1,
inference(orient,[status(thm)],[t94]) ).
cnf(t889,plain,
product(a2,product(a4,a2)) = a1,
inference(step,[status(thm)],[t174,t165]) ).
cnf(t206,plain,
product(a2,product(a4,a2)) = a1,
inference(orient,[status(thm)],[t889]) ).
cnf(t207,plain,
a2 = product(a1,product(a4,a2)),
inference(cp,[status(thm)],[t32,t206]) ).
cnf(t210,plain,
product(a1,product(a4,a2)) = a2,
inference(orient,[status(thm)],[t207]) ).
cnf(t993,plain,
product(a1,product(a4,a7)) = a2,
inference(step,[status(thm)],[t210,t702]) ).
cnf(t156,plain,
product(a4,product(a8,a4)) = product(a9,a4),
inference(cp,[status(thm)],[t141,t67]) ).
cnf(t893,plain,
product(a4,a7) = product(a9,a4),
inference(step,[status(thm)],[t156,t161]) ).
cnf(t254,plain,
product(a4,a7) = product(a9,a4),
inference(orient,[status(thm)],[t893]) ).
cnf(t994,plain,
product(a1,product(a9,a4)) = a2,
inference(step,[status(thm)],[t993,t254]) ).
cnf(t255,plain,
a4 = product(product(a9,a4),a7),
inference(cp,[status(thm)],[t32,t254]) ).
cnf(t259,plain,
product(product(a9,a4),a7) = a4,
inference(orient,[status(thm)],[t255]) ).
cnf(t73,plain,
product(product(a9,X1),a7) = product(a1,product(X1,a7)),
inference(cp,[status(thm)],[t71,t69]) ).
cnf(t288,plain,
product(product(a9,X1),a7) = product(a1,product(X1,a7)),
inference(orient,[status(thm)],[t73]) ).
cnf(t897,plain,
product(a1,product(a4,a7)) = a4,
inference(step,[status(thm)],[t259,t288]) ).
cnf(t898,plain,
product(a1,product(a9,a4)) = a4,
inference(step,[status(thm)],[t897,t254]) ).
cnf(t295,plain,
product(a1,product(a9,a4)) = a4,
inference(rw,[status(thm)],[t898]) ).
cnf(t296,plain,
product(a1,product(a9,a4)) = a4,
inference(orient,[status(thm)],[t295]) ).
cnf(t995,plain,
a4 = a2,
inference(step,[status(thm)],[t994,t296]) ).
cnf(t996,plain,
a4 = a7,
inference(step,[status(thm)],[t995,t702]) ).
cnf(t730,plain,
a4 = a7,
inference(rw,[status(thm)],[t996]) ).
cnf(t803,plain,
a4 = a7,
inference(orient,[status(thm)],[t730]) ).
cnf(t1172,plain,
a4 = a9,
inference(step,[status(thm)],[t803,t837]) ).
cnf(t844,plain,
a4 = a9,
inference(orient,[status(thm)],[t1172]) ).
cnf(t977,plain,
product(a7,a10) = a5,
inference(step,[status(thm)],[t81,t702]) ).
cnf(t722,plain,
product(a7,a10) = a5,
inference(rw,[status(thm)],[t977]) ).
cnf(t1204,plain,
product(a9,a10) = a5,
inference(step,[status(thm)],[t722,t837]) ).
cnf(t1205,plain,
product(a9,a9) = a5,
inference(step,[status(thm)],[t1204,t823]) ).
cnf(t1206,plain,
a9 = a5,
inference(step,[status(thm)],[t1205,t31]) ).
cnf(t865,plain,
a5 = a9,
inference(orient,[status(thm)],[t1206]) ).
cnf(t297,plain,
a1 = product(a4,product(a9,a4)),
inference(cp,[status(thm)],[t32,t296]) ).
cnf(t301,plain,
product(a4,product(a9,a4)) = a1,
inference(orient,[status(thm)],[t297]) ).
cnf(t818,plain,
a6 = a1,
inference(rw,[status(thm)],[t301]) ).
cnf(t1114,plain,
product(a7,a7) = product(a9,a4),
inference(step,[status(thm)],[t254,t803]) ).
cnf(t1115,plain,
a7 = product(a9,a4),
inference(step,[status(thm)],[t1114,t31]) ).
cnf(t1116,plain,
a7 = product(a9,a7),
inference(step,[status(thm)],[t1115,t803]) ).
cnf(t1117,plain,
a7 = a1,
inference(step,[status(thm)],[t1116,t69]) ).
cnf(t807,plain,
a7 = a1,
inference(rw,[status(thm)],[t1117]) ).
cnf(t1189,plain,
a9 = a1,
inference(step,[status(thm)],[t807,t837]) ).
cnf(t855,plain,
a1 = a9,
inference(orient,[status(thm)],[t1189]) ).
cnf(t1200,plain,
a6 = a9,
inference(step,[status(thm)],[t818,t855]) ).
cnf(t861,plain,
a6 = a9,
inference(orient,[status(thm)],[t1200]) ).
cnf(goal_0,negated_conjecture,
ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a2),a10),a9),a7),a8),a3),a4),a5),a6) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a1),a9),a8),a6),a7),a2),a3),a4),a5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a10),a9),a7),a8),a3),a4),a5),a6) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a1),a9),a8),a6),a7),a2),a3),a4),a5),
inference(rw,[status(thm)],[goal_0,t842]) ).
cnf(g0_1,plain,
ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a7),a8),a3),a4),a5),a6) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a1),a9),a8),a6),a7),a2),a3),a4),a5),
inference(rw,[status(thm)],[g0_0,t823]) ).
cnf(g0_2,plain,
ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a8),a3),a4),a5),a6) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a1),a9),a8),a6),a7),a2),a3),a4),a5),
inference(rw,[status(thm)],[g0_1,t837]) ).
cnf(g0_3,plain,
ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a3),a4),a5),a6) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a1),a9),a8),a6),a7),a2),a3),a4),a5),
inference(rw,[status(thm)],[g0_2,t755]) ).
cnf(g0_4,plain,
ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a4),a5),a6) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a1),a9),a8),a6),a7),a2),a3),a4),a5),
inference(rw,[status(thm)],[g0_3,t780]) ).
cnf(g0_5,plain,
ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a5),a6) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a1),a9),a8),a6),a7),a2),a3),a4),a5),
inference(rw,[status(thm)],[g0_4,t844]) ).
cnf(g0_6,plain,
ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a6) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a1),a9),a8),a6),a7),a2),a3),a4),a5),
inference(rw,[status(thm)],[g0_5,t865]) ).
cnf(g0_7,plain,
ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a1),a9),a8),a6),a7),a2),a3),a4),a5),
inference(rw,[status(thm)],[g0_6,t861]) ).
cnf(g0_8,plain,
ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a8),a6),a7),a2),a3),a4),a5),
inference(rw,[status(thm)],[g0_7,t855]) ).
cnf(g0_9,plain,
ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a6),a7),a2),a3),a4),a5),
inference(rw,[status(thm)],[g0_8,t755]) ).
cnf(g0_10,plain,
ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a7),a2),a3),a4),a5),
inference(rw,[status(thm)],[g0_9,t861]) ).
cnf(g0_11,plain,
ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a2),a3),a4),a5),
inference(rw,[status(thm)],[g0_10,t837]) ).
cnf(g0_12,plain,
ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a3),a4),a5),
inference(rw,[status(thm)],[g0_11,t842]) ).
cnf(g0_13,plain,
ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a4),a5),
inference(rw,[status(thm)],[g0_12,t780]) ).
cnf(g0_14,plain,
ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a5),
inference(rw,[status(thm)],[g0_13,t844]) ).
cnf(g0_15,plain,
ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9) != ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(tuple,a9),a9),a9),a9),a9),a9),a9),a9),a9),
inference(rw,[status(thm)],[g0_14,t865]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_15]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : TOP049-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 : n017.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:15:16 UTC 2026
% 0.12/0.36 % CPUTime :
% 0.12/0.36 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 7.46/1.66 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.46/1.66 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------