%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : TOP051-1 : TPTP v9.3.1. Released v8.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n015.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 : Thu Sep 24 03:53:32 PM UTC 2026
% Result : Unsatisfiable 0.06s 0.42s
% Output : CNFRefutation 0.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 40
% Number of leaves : 16
% Syntax : Number of formulae : 169 ( 169 unt; 2 def)
% Number of atoms : 169 ( 168 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 1 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 13 con; 0-10 aty)
% Number of variables : 25 ( 25 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X] : product(X,X) = X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [X,Y] : product(product(X,Y),Y) = X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [X,Y,Z] : product(product(X,Y),Z) = product(product(X,Z),product(Y,Z)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,axiom,
product(a1,a6) = a2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
product(a2,a7) = a3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
product(a3,a1) = a4,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,axiom,
product(a4,a10) = a5,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8,axiom,
product(a5,a9) = a6,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,axiom,
product(a6,a2) = a7,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10,axiom,
product(a7,a3) = a8,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11,axiom,
product(a8,a6) = a9,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12,axiom,
product(a9,a4) = a10,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,axiom,
product(a10,a5) = a11,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f14,negated_conjecture,
tuple(a1,a6,a5,a2,a7,a3,a4,a9,a10,a8) != tuple(a2,a7,a6,a3,a8,a4,a5,a10,a11,a9),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,plain,
! [X0] : product(X0,X0) = X0,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f16,plain,
! [X0,X1] : product(product(X0,X1),X1) = X0,
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f17,plain,
! [X0,X1,X2] : product(product(X0,X1),X2) = product(product(X0,X2),product(X1,X2)),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f18,plain,
product(a1,a6) = a2,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f19,plain,
product(a2,a7) = a3,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f20,plain,
product(a3,a1) = a4,
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f21,plain,
product(a4,a10) = a5,
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f22,plain,
product(a5,a9) = a6,
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f23,plain,
product(a6,a2) = a7,
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f24,plain,
product(a7,a3) = a8,
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f25,plain,
product(a8,a6) = a9,
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f26,plain,
product(a9,a4) = a10,
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f27,plain,
product(a10,a5) = a11,
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f28,plain,
tuple(a1,a6,a5,a2,a7,a3,a4,a9,a10,a8) != tuple(a2,a7,a6,a3,a8,a4,a5,a10,a11,a9),
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f29,definition,
sF0_fnc = tuple(a1,a6,a5,a2,a7,a3,a4,a9,a10,a8),
introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition]) ).
fof(f30,definition,
sF1_fnc = tuple(a2,a7,a6,a3,a8,a4,a5,a10,a11,a9),
introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition]) ).
fof(f31,plain,
sF0_fnc != sF1_fnc,
inference(definition_folding,[],[f28,f30,f29]) ).
fof(f34,plain,
product(a10,a4) = a9,
inference(paramodulation,[status(thm)],[f26,f16]) ).
fof(f35,plain,
product(a9,a6) = a8,
inference(paramodulation,[status(thm)],[f25,f16]) ).
fof(f37,plain,
product(a7,a2) = a6,
inference(paramodulation,[status(thm)],[f23,f16]) ).
fof(f39,plain,
product(a5,a10) = a4,
inference(paramodulation,[status(thm)],[f21,f16]) ).
fof(f41,plain,
product(a3,a7) = a2,
inference(paramodulation,[status(thm)],[f19,f16]) ).
fof(f42,plain,
product(a2,a6) = a1,
inference(paramodulation,[status(thm)],[f18,f16]) ).
fof(f57,plain,
! [X0,X1,X2] : product(product(product(X0,X1),X2),X1) = product(X0,product(X2,X1)),
inference(paramodulation,[status(thm)],[f16,f17]) ).
fof(f67,plain,
! [X0] : product(product(a6,X0),a2) = product(a7,product(X0,a2)),
inference(paramodulation,[status(thm)],[f23,f17]) ).
fof(f69,plain,
! [X0] : product(product(a5,X0),a9) = product(a6,product(X0,a9)),
inference(paramodulation,[status(thm)],[f22,f17]) ).
fof(f73,plain,
! [X0] : product(product(a3,X0),a1) = product(a4,product(X0,a1)),
inference(paramodulation,[status(thm)],[f20,f17]) ).
fof(f76,plain,
! [X0] : product(product(a1,X0),a6) = product(a2,product(X0,a6)),
inference(paramodulation,[status(thm)],[f18,f17]) ).
fof(f77,plain,
! [X0,X1] : product(product(X0,X1),X0) = product(X0,product(X1,X0)),
inference(paramodulation,[status(thm)],[f15,f17]) ).
fof(f80,plain,
! [X0,X1,X2] : product(product(X0,product(X1,X2)),X2) = product(product(X0,X2),X1),
inference(paramodulation,[status(thm)],[f16,f17]) ).
fof(f96,plain,
! [X0] : product(product(X0,a3),a1) = product(product(X0,a1),a4),
inference(paramodulation,[status(thm)],[f20,f17]) ).
fof(f111,plain,
product(a9,a10) = product(a10,product(a4,a10)),
inference(paramodulation,[status(thm)],[f34,f77]) ).
fof(f117,plain,
product(a6,a7) = product(a7,product(a2,a7)),
inference(paramodulation,[status(thm)],[f37,f77]) ).
fof(f120,plain,
product(a7,a6) = product(a6,product(a2,a6)),
inference(paramodulation,[status(thm)],[f23,f77]) ).
fof(f124,plain,
product(a5,a4) = product(a4,product(a10,a4)),
inference(paramodulation,[status(thm)],[f21,f77]) ).
fof(f125,plain,
product(a2,a3) = product(a3,product(a7,a3)),
inference(paramodulation,[status(thm)],[f41,f77]) ).
fof(f127,plain,
product(a1,a2) = product(a2,product(a6,a2)),
inference(paramodulation,[status(thm)],[f42,f77]) ).
fof(f150,plain,
product(a9,a10) = product(a10,a5),
inference(forward_demodulation,[status(thm)],[f21,f111]) ).
fof(f151,plain,
product(a9,a10) = a11,
inference(forward_demodulation,[status(thm)],[f27,f150]) ).
fof(f155,plain,
product(a6,a7) = product(a7,a3),
inference(forward_demodulation,[status(thm)],[f19,f117]) ).
fof(f156,plain,
product(a6,a7) = a8,
inference(forward_demodulation,[status(thm)],[f24,f155]) ).
fof(f160,plain,
product(a7,a6) = product(a6,a1),
inference(forward_demodulation,[status(thm)],[f42,f120]) ).
fof(f162,plain,
product(a5,a4) = product(a4,a9),
inference(forward_demodulation,[status(thm)],[f34,f124]) ).
fof(f163,plain,
product(a2,a3) = product(a3,a8),
inference(forward_demodulation,[status(thm)],[f24,f125]) ).
fof(f164,plain,
product(a1,a2) = product(a2,a7),
inference(forward_demodulation,[status(thm)],[f23,f127]) ).
fof(f165,plain,
product(a1,a2) = a3,
inference(forward_demodulation,[status(thm)],[f19,f164]) ).
fof(f384,plain,
product(a8,a6) = product(a6,product(a7,a6)),
inference(paramodulation,[status(thm)],[f156,f77]) ).
fof(f389,plain,
a9 = product(a6,product(a7,a6)),
inference(forward_demodulation,[status(thm)],[f25,f384]) ).
fof(f425,plain,
product(a3,a1) = product(a1,product(a2,a1)),
inference(paramodulation,[status(thm)],[f165,f77]) ).
fof(f430,plain,
a4 = product(a1,product(a2,a1)),
inference(forward_demodulation,[status(thm)],[f20,f425]) ).
fof(f530,plain,
product(product(a5,a4),a9) = a4,
inference(paramodulation,[status(thm)],[f162,f16]) ).
fof(f576,plain,
product(a4,product(a2,a1)) = a1,
inference(paramodulation,[status(thm)],[f430,f16]) ).
fof(f673,plain,
product(product(a7,a6),a2) = product(a7,product(a1,a2)),
inference(paramodulation,[status(thm)],[f160,f67]) ).
fof(f675,plain,
product(a8,a2) = product(a7,product(a7,a2)),
inference(paramodulation,[status(thm)],[f156,f67]) ).
fof(f690,plain,
product(product(a7,a6),a2) = product(a7,a3),
inference(forward_demodulation,[status(thm)],[f165,f673]) ).
fof(f691,plain,
product(product(a7,a6),a2) = a8,
inference(forward_demodulation,[status(thm)],[f24,f690]) ).
fof(f692,plain,
product(a8,a2) = product(a7,a6),
inference(forward_demodulation,[status(thm)],[f37,f675]) ).
fof(f700,plain,
product(a6,product(a4,a9)) = a4,
inference(backward_demodulation,[status(thm)],[f69,f530]) ).
fof(f715,plain,
product(a6,product(a5,a4)) = a4,
inference(forward_demodulation,[status(thm)],[f162,f700]) ).
fof(f818,plain,
product(a8,a6) = product(a7,product(a2,a6)),
inference(paramodulation,[status(thm)],[f691,f57]) ).
fof(f827,plain,
a9 = product(a7,product(a2,a6)),
inference(forward_demodulation,[status(thm)],[f25,f818]) ).
fof(f828,plain,
a9 = product(a7,a1),
inference(forward_demodulation,[status(thm)],[f42,f827]) ).
fof(f840,plain,
product(a9,a1) = a7,
inference(paramodulation,[status(thm)],[f828,f16]) ).
fof(f854,plain,
a9 = product(a6,product(a8,a2)),
inference(backward_demodulation,[status(thm)],[f692,f389]) ).
fof(f855,plain,
product(a8,a2) = product(a6,a1),
inference(backward_demodulation,[status(thm)],[f692,f160]) ).
fof(f876,plain,
product(a4,product(a5,a4)) = a6,
inference(paramodulation,[status(thm)],[f715,f16]) ).
fof(f930,plain,
product(a3,a6) = product(a2,product(a2,a6)),
inference(paramodulation,[status(thm)],[f165,f76]) ).
fof(f944,plain,
product(a3,a6) = product(a2,a1),
inference(forward_demodulation,[status(thm)],[f42,f930]) ).
fof(f1023,plain,
product(a4,product(a3,a6)) = a1,
inference(backward_demodulation,[status(thm)],[f944,f576]) ).
fof(f1024,plain,
a4 = product(a1,product(a3,a6)),
inference(backward_demodulation,[status(thm)],[f944,f430]) ).
fof(f1032,plain,
product(product(a3,a6),a1) = a2,
inference(paramodulation,[status(thm)],[f944,f16]) ).
fof(f1037,plain,
product(a4,product(a6,a1)) = a2,
inference(forward_demodulation,[status(thm)],[f73,f1032]) ).
fof(f1038,plain,
product(a4,product(a8,a2)) = a2,
inference(forward_demodulation,[status(thm)],[f855,f1037]) ).
fof(f1644,plain,
product(a4,a6) = product(a2,product(product(a3,a6),a6)),
inference(paramodulation,[status(thm)],[f1024,f76]) ).
fof(f1658,plain,
product(a4,a6) = product(a2,a3),
inference(forward_demodulation,[status(thm)],[f16,f1644]) ).
fof(f1659,plain,
product(a4,a6) = product(a3,a8),
inference(forward_demodulation,[status(thm)],[f163,f1658]) ).
fof(f1668,plain,
product(a2,a2) = product(product(a4,a2),a8),
inference(paramodulation,[status(thm)],[f1038,f80]) ).
fof(f1680,plain,
product(a2,product(a8,a2)) = a4,
inference(paramodulation,[status(thm)],[f1038,f16]) ).
fof(f1681,plain,
a2 = product(product(a4,a2),a8),
inference(forward_demodulation,[status(thm)],[f15,f1668]) ).
fof(f1866,plain,
product(product(a4,a6),a8) = a3,
inference(paramodulation,[status(thm)],[f1659,f16]) ).
fof(f2103,plain,
product(a3,a6) = product(a4,product(a8,a6)),
inference(paramodulation,[status(thm)],[f1866,f57]) ).
fof(f2117,plain,
product(a3,a6) = product(a4,a9),
inference(forward_demodulation,[status(thm)],[f25,f2103]) ).
fof(f2118,plain,
product(a3,a6) = product(a5,a4),
inference(forward_demodulation,[status(thm)],[f162,f2117]) ).
fof(f2336,plain,
product(product(a7,a3),a1) = product(a9,a4),
inference(paramodulation,[status(thm)],[f828,f96]) ).
fof(f2361,plain,
product(a8,a1) = product(a9,a4),
inference(forward_demodulation,[status(thm)],[f24,f2336]) ).
fof(f2362,plain,
product(a8,a1) = a10,
inference(forward_demodulation,[status(thm)],[f26,f2361]) ).
fof(f2441,plain,
product(a4,product(a5,a4)) = a1,
inference(backward_demodulation,[status(thm)],[f2118,f1023]) ).
fof(f2456,plain,
a6 = a1,
inference(forward_demodulation,[status(thm)],[f876,f2441]) ).
fof(f2470,plain,
product(a8,a6) = a10,
inference(backward_demodulation,[status(thm)],[f2456,f2362]) ).
fof(f2477,plain,
product(a9,a6) = a7,
inference(backward_demodulation,[status(thm)],[f2456,f840]) ).
fof(f2481,plain,
product(a6,a2) = a3,
inference(backward_demodulation,[status(thm)],[f2456,f165]) ).
fof(f2484,plain,
product(a3,a6) = a4,
inference(backward_demodulation,[status(thm)],[f2456,f20]) ).
fof(f2485,plain,
product(a6,a6) = a2,
inference(backward_demodulation,[status(thm)],[f2456,f18]) ).
fof(f2486,plain,
sF0_fnc = tuple(a6,a6,a5,a2,a7,a3,a4,a9,a10,a8),
inference(backward_demodulation,[status(thm)],[f2456,f29]) ).
fof(f2488,plain,
a9 = a10,
inference(forward_demodulation,[status(thm)],[f25,f2470]) ).
fof(f2493,plain,
a8 = a7,
inference(forward_demodulation,[status(thm)],[f35,f2477]) ).
fof(f2496,plain,
a7 = a3,
inference(forward_demodulation,[status(thm)],[f23,f2481]) ).
fof(f2497,plain,
product(a5,a4) = a4,
inference(forward_demodulation,[status(thm)],[f2118,f2484]) ).
fof(f2498,plain,
a6 = a2,
inference(forward_demodulation,[status(thm)],[f15,f2485]) ).
fof(f2507,plain,
product(a9,a9) = a11,
inference(backward_demodulation,[status(thm)],[f2488,f151]) ).
fof(f2509,plain,
product(a5,a9) = a4,
inference(backward_demodulation,[status(thm)],[f2488,f39]) ).
fof(f2515,plain,
sF1_fnc = tuple(a2,a7,a6,a3,a8,a4,a5,a9,a11,a9),
inference(backward_demodulation,[status(thm)],[f2488,f30]) ).
fof(f2518,plain,
a9 = a11,
inference(forward_demodulation,[status(thm)],[f15,f2507]) ).
fof(f2519,plain,
a6 = a4,
inference(forward_demodulation,[status(thm)],[f22,f2509]) ).
fof(f2523,plain,
product(a4,a4) = a6,
inference(backward_demodulation,[status(thm)],[f2497,f876]) ).
fof(f2536,plain,
product(a4,a4) = a5,
inference(paramodulation,[status(thm)],[f2497,f16]) ).
fof(f2537,plain,
a4 = a6,
inference(forward_demodulation,[status(thm)],[f15,f2523]) ).
fof(f2550,plain,
a4 = a5,
inference(forward_demodulation,[status(thm)],[f15,f2536]) ).
fof(f2554,plain,
product(product(a4,a2),a8) = a3,
inference(backward_demodulation,[status(thm)],[f2498,f1866]) ).
fof(f2563,plain,
a9 = product(a2,product(a8,a2)),
inference(backward_demodulation,[status(thm)],[f2498,f854]) ).
fof(f2580,plain,
a2 = a3,
inference(forward_demodulation,[status(thm)],[f1681,f2554]) ).
fof(f2582,plain,
a9 = a4,
inference(forward_demodulation,[status(thm)],[f1680,f2563]) ).
fof(f2601,plain,
a8 = a3,
inference(forward_demodulation,[status(thm)],[f2493,f2496]) ).
fof(f2602,plain,
a11 = a10,
inference(backward_demodulation,[status(thm)],[f2518,f2488]) ).
fof(f2608,plain,
a6 = a4,
inference(backward_demodulation,[status(thm)],[f2613,f2498]) ).
fof(f2613,plain,
a2 = a4,
inference(forward_demodulation,[status(thm)],[f2498,f2519]) ).
fof(f2620,plain,
a5 = a6,
inference(backward_demodulation,[status(thm)],[f2550,f2537]) ).
fof(f2621,plain,
a2 = a5,
inference(backward_demodulation,[status(thm)],[f2550,f2613]) ).
fof(f2628,plain,
a2 = a8,
inference(forward_demodulation,[status(thm)],[f2601,f2580]) ).
fof(f2629,plain,
a11 = a4,
inference(forward_demodulation,[status(thm)],[f2518,f2582]) ).
fof(f2631,plain,
a11 = a5,
inference(forward_demodulation,[status(thm)],[f2550,f2629]) ).
fof(f2633,plain,
sF0_fnc = tuple(a6,a6,a11,a2,a7,a3,a4,a9,a10,a8),
inference(forward_demodulation,[status(thm)],[f2631,f2486]) ).
fof(f2634,plain,
sF0_fnc = tuple(a6,a6,a11,a8,a7,a3,a4,a9,a10,a8),
inference(forward_demodulation,[status(thm)],[f2628,f2633]) ).
fof(f2635,plain,
sF0_fnc = tuple(a6,a6,a11,a8,a8,a3,a4,a9,a10,a8),
inference(forward_demodulation,[status(thm)],[f2493,f2634]) ).
fof(f2636,plain,
sF0_fnc = tuple(a6,a6,a11,a8,a8,a8,a4,a9,a10,a8),
inference(forward_demodulation,[status(thm)],[f2601,f2635]) ).
fof(f2637,plain,
sF0_fnc = tuple(a6,a6,a11,a8,a8,a8,a4,a11,a10,a8),
inference(forward_demodulation,[status(thm)],[f2518,f2636]) ).
fof(f2638,plain,
sF0_fnc = tuple(a6,a6,a11,a8,a8,a8,a4,a11,a11,a8),
inference(forward_demodulation,[status(thm)],[f2602,f2637]) ).
fof(f2675,plain,
sF1_fnc = tuple(a8,a7,a6,a3,a8,a4,a5,a9,a11,a9),
inference(forward_demodulation,[status(thm)],[f2628,f2515]) ).
fof(f2676,plain,
sF1_fnc = tuple(a8,a8,a6,a3,a8,a4,a5,a9,a11,a9),
inference(forward_demodulation,[status(thm)],[f2493,f2675]) ).
fof(f2677,plain,
sF1_fnc = tuple(a8,a8,a6,a8,a8,a4,a5,a9,a11,a9),
inference(forward_demodulation,[status(thm)],[f2601,f2676]) ).
fof(f2678,plain,
sF1_fnc = tuple(a8,a8,a6,a8,a8,a4,a11,a9,a11,a9),
inference(forward_demodulation,[status(thm)],[f2631,f2677]) ).
fof(f2679,plain,
sF1_fnc = tuple(a8,a8,a6,a8,a8,a4,a11,a11,a11,a9),
inference(forward_demodulation,[status(thm)],[f2518,f2678]) ).
fof(f2680,plain,
sF1_fnc = tuple(a8,a8,a6,a8,a8,a4,a11,a11,a11,a11),
inference(forward_demodulation,[status(thm)],[f2518,f2679]) ).
fof(f2681,plain,
sF1_fnc = tuple(a8,a8,a4,a8,a8,a4,a11,a11,a11,a11),
inference(backward_demodulation,[status(thm)],[f2608,f2680]) ).
fof(f2682,plain,
sF0_fnc = tuple(a6,a4,a11,a8,a8,a8,a4,a11,a11,a8),
inference(backward_demodulation,[status(thm)],[f2608,f2638]) ).
fof(f2683,plain,
sF0_fnc = tuple(a4,a4,a11,a8,a8,a8,a4,a11,a11,a8),
inference(forward_demodulation,[status(thm)],[f2608,f2682]) ).
fof(f2686,plain,
a11 = a6,
inference(forward_demodulation,[status(thm)],[f2631,f2620]) ).
fof(f2687,plain,
sF0_fnc = tuple(a4,a4,a11,a8,a8,a8,a11,a11,a11,a8),
inference(backward_demodulation,[status(thm)],[f2691,f2683]) ).
fof(f2688,plain,
sF1_fnc = tuple(a8,a8,a4,a8,a8,a11,a11,a11,a11,a11),
inference(backward_demodulation,[status(thm)],[f2691,f2681]) ).
fof(f2691,plain,
a11 = a4,
inference(forward_demodulation,[status(thm)],[f2608,f2686]) ).
fof(f2692,plain,
sF0_fnc = tuple(a11,a4,a11,a8,a8,a8,a11,a11,a11,a8),
inference(forward_demodulation,[status(thm)],[f2691,f2687]) ).
fof(f2693,plain,
sF0_fnc = tuple(a11,a11,a11,a8,a8,a8,a11,a11,a11,a8),
inference(forward_demodulation,[status(thm)],[f2691,f2692]) ).
fof(f2694,plain,
sF1_fnc = tuple(a8,a8,a11,a8,a8,a11,a11,a11,a11,a11),
inference(forward_demodulation,[status(thm)],[f2691,f2688]) ).
fof(f2695,plain,
a8 = a5,
inference(forward_demodulation,[status(thm)],[f2628,f2621]) ).
fof(f2700,plain,
a8 = a11,
inference(forward_demodulation,[status(thm)],[f2631,f2695]) ).
fof(f2744,plain,
sF0_fnc = tuple(a11,a11,a11,a11,a8,a8,a11,a11,a11,a8),
inference(forward_demodulation,[status(thm)],[f2700,f2693]) ).
fof(f2745,plain,
sF0_fnc = tuple(a11,a11,a11,a11,a11,a8,a11,a11,a11,a8),
inference(forward_demodulation,[status(thm)],[f2700,f2744]) ).
fof(f2746,plain,
sF0_fnc = tuple(a11,a11,a11,a11,a11,a11,a11,a11,a11,a8),
inference(forward_demodulation,[status(thm)],[f2700,f2745]) ).
fof(f2747,plain,
sF0_fnc = tuple(a11,a11,a11,a11,a11,a11,a11,a11,a11,a11),
inference(forward_demodulation,[status(thm)],[f2700,f2746]) ).
fof(f2748,plain,
sF1_fnc = tuple(a11,a8,a11,a8,a8,a11,a11,a11,a11,a11),
inference(forward_demodulation,[status(thm)],[f2700,f2694]) ).
fof(f2749,plain,
sF1_fnc = tuple(a11,a11,a11,a8,a8,a11,a11,a11,a11,a11),
inference(forward_demodulation,[status(thm)],[f2700,f2748]) ).
fof(f2750,plain,
sF1_fnc = tuple(a11,a11,a11,a11,a8,a11,a11,a11,a11,a11),
inference(forward_demodulation,[status(thm)],[f2700,f2749]) ).
fof(f2751,plain,
sF1_fnc = tuple(a11,a11,a11,a11,a11,a11,a11,a11,a11,a11),
inference(forward_demodulation,[status(thm)],[f2700,f2750]) ).
fof(f2752,plain,
sF1_fnc = sF0_fnc,
inference(forward_demodulation,[status(thm)],[f2747,f2751]) ).
fof(f2753,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f2752,f31]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : TOP051-1 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.06/0.33 % Computer : n015.cluster.edu
% 0.06/0.33 % Model : x86_64 x86_64
% 0.06/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.33 % Memory : 8046.5625MB
% 0.06/0.33 % OS : Linux 6.8.0-71-generic
% 0.06/0.33 % CPULimit : 300
% 0.06/0.33 % WCLimit : 300
% 0.06/0.33 % DateTime : Mon Sep 21 12:51:07 UTC 2026
% 0.06/0.34 % CPUTime :
% 0.06/0.34 % Drodi V4.1.1
% 0.06/0.42 % Refutation found
% 0.06/0.42 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.06/0.42 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.13/0.45 % Elapsed time: 0.102771 seconds
% 0.13/0.45 % CPU time: 0.544035 seconds
% 0.13/0.45 % Total memory used: 21.633 MB
% 0.13/0.45 % Net memory used: 21.384 MB
%------------------------------------------------------------------------------