%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : TOP053-1 : TPTP v9.3.1. Released v8.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n001.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.17s 0.59s
% Output : CNFRefutation 0.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 53
% Number of leaves : 21
% Syntax : Number of formulae : 191 ( 191 unt; 2 def)
% Number of atoms : 191 ( 190 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 : 19 ( 19 usr; 17 con; 0-14 aty)
% Number of variables : 22 ( 22 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X] : product(X,X) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [X,Y] : product(product(X,Y),Y) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [X,Y,Z] : product(product(X,Y),Z) = product(product(X,Z),product(Y,Z)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
product(a1,a2) = a3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,axiom,
product(a3,a4) = a5,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,axiom,
product(a5,a6) = a7,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
product(a7,a3) = a8,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,axiom,
product(a8,a2) = a9,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,axiom,
product(a9,a1) = a10,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,axiom,
product(a10,a11) = a12,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,axiom,
product(a12,a3) = a13,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,axiom,
product(a13,a8) = a6,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13,axiom,
product(a6,a7) = a2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f14,axiom,
product(a2,a12) = a14,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f15,axiom,
product(a14,a3) = a15,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f16,axiom,
product(a15,a8) = a4,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f17,axiom,
product(a4,a7) = a11,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f18,axiom,
product(a11,a10) = a1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f19,negated_conjecture,
tuple(a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14) != tuple(a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f20,plain,
! [X0] : product(X0,X0) = X0,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f21,plain,
! [X0,X1] : product(product(X0,X1),X1) = X0,
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f22,plain,
! [X0,X1,X2] : product(product(X0,X1),X2) = product(product(X0,X2),product(X1,X2)),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f23,plain,
product(a1,a2) = a3,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f24,plain,
product(a3,a4) = a5,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f25,plain,
product(a5,a6) = a7,
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f26,plain,
product(a7,a3) = a8,
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f27,plain,
product(a8,a2) = a9,
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f28,plain,
product(a9,a1) = a10,
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f29,plain,
product(a10,a11) = a12,
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f30,plain,
product(a12,a3) = a13,
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f31,plain,
product(a13,a8) = a6,
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f32,plain,
product(a6,a7) = a2,
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f33,plain,
product(a2,a12) = a14,
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f34,plain,
product(a14,a3) = a15,
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f35,plain,
product(a15,a8) = a4,
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f36,plain,
product(a4,a7) = a11,
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f37,plain,
product(a11,a10) = a1,
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f38,plain,
tuple(a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14) != tuple(a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15),
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f39,definition,
sF0_fnc = tuple(a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14),
introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition]) ).
fof(f40,definition,
sF1_fnc = tuple(a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15),
introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition]) ).
fof(f41,plain,
sF0_fnc != sF1_fnc,
inference(definition_folding,[],[f38,f40,f39]) ).
fof(f43,plain,
product(a1,a10) = a11,
inference(paramodulation,[status(thm)],[f37,f21]) ).
fof(f44,plain,
product(a11,a7) = a4,
inference(paramodulation,[status(thm)],[f36,f21]) ).
fof(f47,plain,
product(a14,a12) = a2,
inference(paramodulation,[status(thm)],[f33,f21]) ).
fof(f48,plain,
product(a2,a7) = a6,
inference(paramodulation,[status(thm)],[f32,f21]) ).
fof(f52,plain,
product(a10,a1) = a9,
inference(paramodulation,[status(thm)],[f28,f21]) ).
fof(f54,plain,
product(a8,a3) = a7,
inference(paramodulation,[status(thm)],[f26,f21]) ).
fof(f55,plain,
product(a7,a6) = a5,
inference(paramodulation,[status(thm)],[f25,f21]) ).
fof(f57,plain,
product(a3,a2) = a1,
inference(paramodulation,[status(thm)],[f23,f21]) ).
fof(f74,plain,
! [X0,X1,X2] : product(product(product(X0,X1),X2),X1) = product(X0,product(X2,X1)),
inference(paramodulation,[status(thm)],[f21,f22]) ).
fof(f75,plain,
! [X0] : product(product(a11,X0),a7) = product(a4,product(X0,a7)),
inference(paramodulation,[status(thm)],[f44,f22]) ).
fof(f80,plain,
! [X0] : product(product(a15,X0),a8) = product(a4,product(X0,a8)),
inference(paramodulation,[status(thm)],[f35,f22]) ).
fof(f82,plain,
! [X0] : product(product(a14,X0),a3) = product(a15,product(X0,a3)),
inference(paramodulation,[status(thm)],[f34,f22]) ).
fof(f96,plain,
! [X0] : product(product(a8,X0),a2) = product(a9,product(X0,a2)),
inference(paramodulation,[status(thm)],[f27,f22]) ).
fof(f102,plain,
! [X0] : product(product(a1,X0),a2) = product(a3,product(X0,a2)),
inference(paramodulation,[status(thm)],[f23,f22]) ).
fof(f103,plain,
! [X0,X1] : product(product(X0,X1),X0) = product(X0,product(X1,X0)),
inference(paramodulation,[status(thm)],[f20,f22]) ).
fof(f309,plain,
product(a2,a3) = product(a15,product(a12,a3)),
inference(paramodulation,[status(thm)],[f47,f82]) ).
fof(f319,plain,
product(a2,a3) = product(a15,a13),
inference(forward_demodulation,[status(thm)],[f30,f309]) ).
fof(f344,plain,
product(product(a2,a3),a8) = product(a4,product(a13,a8)),
inference(paramodulation,[status(thm)],[f319,f80]) ).
fof(f349,plain,
product(product(a2,a3),a8) = product(a4,a6),
inference(forward_demodulation,[status(thm)],[f31,f344]) ).
fof(f373,plain,
product(a1,a11) = product(a11,product(a10,a11)),
inference(paramodulation,[status(thm)],[f37,f103]) ).
fof(f387,plain,
product(a6,a2) = product(a2,product(a7,a2)),
inference(paramodulation,[status(thm)],[f48,f103]) ).
fof(f401,plain,
product(a5,a7) = product(a7,product(a6,a7)),
inference(paramodulation,[status(thm)],[f55,f103]) ).
fof(f421,plain,
product(a1,a11) = product(a11,a12),
inference(forward_demodulation,[status(thm)],[f29,f373]) ).
fof(f427,plain,
product(a5,a7) = product(a7,a2),
inference(forward_demodulation,[status(thm)],[f32,f401]) ).
fof(f460,plain,
product(product(a5,a7),a2) = a7,
inference(paramodulation,[status(thm)],[f427,f21]) ).
fof(f777,plain,
product(product(a4,a6),a3) = product(a2,product(a8,a3)),
inference(paramodulation,[status(thm)],[f349,f74]) ).
fof(f875,plain,
product(product(a4,a6),a3) = product(a2,a7),
inference(forward_demodulation,[status(thm)],[f54,f777]) ).
fof(f876,plain,
product(product(a4,a6),a3) = a6,
inference(forward_demodulation,[status(thm)],[f48,f875]) ).
fof(f907,plain,
product(a6,a6) = product(a4,product(a3,a6)),
inference(paramodulation,[status(thm)],[f876,f74]) ).
fof(f916,plain,
a6 = product(a4,product(a3,a6)),
inference(forward_demodulation,[status(thm)],[f20,f907]) ).
fof(f927,plain,
product(a6,product(a3,a6)) = a4,
inference(paramodulation,[status(thm)],[f916,f21]) ).
fof(f1150,plain,
product(a6,a2) = product(a2,product(a5,a7)),
inference(forward_demodulation,[status(thm)],[f427,f387]) ).
fof(f1552,plain,
product(a7,a2) = product(a9,product(a3,a2)),
inference(paramodulation,[status(thm)],[f54,f96]) ).
fof(f1569,plain,
product(a5,a7) = product(a9,product(a3,a2)),
inference(forward_demodulation,[status(thm)],[f427,f1552]) ).
fof(f1570,plain,
product(a5,a7) = product(a9,a1),
inference(forward_demodulation,[status(thm)],[f57,f1569]) ).
fof(f1571,plain,
product(a5,a7) = a10,
inference(forward_demodulation,[status(thm)],[f28,f1570]) ).
fof(f1607,plain,
product(a6,a2) = product(a2,a10),
inference(backward_demodulation,[status(thm)],[f1571,f1150]) ).
fof(f1608,plain,
product(a10,a2) = a7,
inference(backward_demodulation,[status(thm)],[f1571,f460]) ).
fof(f1609,plain,
a10 = product(a7,a2),
inference(backward_demodulation,[status(thm)],[f1571,f427]) ).
fof(f1789,plain,
product(a11,a2) = product(a3,product(a10,a2)),
inference(paramodulation,[status(thm)],[f43,f102]) ).
fof(f1806,plain,
product(a11,a2) = product(a3,a7),
inference(forward_demodulation,[status(thm)],[f1608,f1789]) ).
fof(f1815,plain,
product(product(a3,a7),a7) = product(a4,product(a2,a7)),
inference(paramodulation,[status(thm)],[f1806,f75]) ).
fof(f1823,plain,
a3 = product(a4,product(a2,a7)),
inference(forward_demodulation,[status(thm)],[f21,f1815]) ).
fof(f1824,plain,
a3 = product(a4,a6),
inference(forward_demodulation,[status(thm)],[f48,f1823]) ).
fof(f1827,plain,
product(a3,a3) = a6,
inference(backward_demodulation,[status(thm)],[f1824,f876]) ).
fof(f1838,plain,
a3 = a6,
inference(forward_demodulation,[status(thm)],[f20,f1827]) ).
fof(f1847,plain,
product(a3,a2) = product(a2,a10),
inference(backward_demodulation,[status(thm)],[f1838,f1607]) ).
fof(f1853,plain,
product(a6,product(a3,a3)) = a4,
inference(backward_demodulation,[status(thm)],[f1838,f927]) ).
fof(f1859,plain,
product(a7,a3) = a5,
inference(backward_demodulation,[status(thm)],[f1838,f55]) ).
fof(f1863,plain,
product(a13,a8) = a3,
inference(backward_demodulation,[status(thm)],[f1838,f31]) ).
fof(f1864,plain,
product(a5,a3) = a7,
inference(backward_demodulation,[status(thm)],[f1838,f25]) ).
fof(f1865,plain,
sF1_fnc = tuple(a2,a3,a4,a5,a3,a7,a8,a9,a10,a11,a12,a13,a14,a15),
inference(backward_demodulation,[status(thm)],[f1838,f40]) ).
fof(f1866,plain,
sF0_fnc = tuple(a1,a2,a3,a4,a5,a3,a7,a8,a9,a10,a11,a12,a13,a14),
inference(backward_demodulation,[status(thm)],[f1838,f39]) ).
fof(f1868,plain,
a1 = product(a2,a10),
inference(forward_demodulation,[status(thm)],[f57,f1847]) ).
fof(f1874,plain,
product(a3,product(a3,a3)) = a4,
inference(forward_demodulation,[status(thm)],[f1838,f1853]) ).
fof(f1875,plain,
product(a3,a3) = a4,
inference(forward_demodulation,[status(thm)],[f20,f1874]) ).
fof(f1876,plain,
a3 = a4,
inference(forward_demodulation,[status(thm)],[f20,f1875]) ).
fof(f1881,plain,
a8 = a5,
inference(forward_demodulation,[status(thm)],[f26,f1859]) ).
fof(f1900,plain,
product(a3,a7) = a11,
inference(backward_demodulation,[status(thm)],[f1876,f36]) ).
fof(f1902,plain,
product(a3,a3) = a5,
inference(backward_demodulation,[status(thm)],[f1876,f24]) ).
fof(f1915,plain,
a3 = a5,
inference(forward_demodulation,[status(thm)],[f20,f1902]) ).
fof(f1936,plain,
a8 = a3,
inference(backward_demodulation,[status(thm)],[f1915,f1881]) ).
fof(f1950,plain,
product(a1,a10) = a2,
inference(paramodulation,[status(thm)],[f1868,f21]) ).
fof(f1954,plain,
a11 = a2,
inference(forward_demodulation,[status(thm)],[f43,f1950]) ).
fof(f1960,plain,
product(a1,a11) = product(a2,a12),
inference(backward_demodulation,[status(thm)],[f1954,f421]) ).
fof(f1967,plain,
product(a10,a2) = a12,
inference(backward_demodulation,[status(thm)],[f1954,f29]) ).
fof(f1974,plain,
product(a1,a2) = product(a2,a12),
inference(forward_demodulation,[status(thm)],[f1954,f1960]) ).
fof(f1975,plain,
a3 = product(a2,a12),
inference(forward_demodulation,[status(thm)],[f23,f1974]) ).
fof(f1976,plain,
a3 = a14,
inference(forward_demodulation,[status(thm)],[f33,f1975]) ).
fof(f1977,plain,
a7 = a12,
inference(forward_demodulation,[status(thm)],[f1608,f1967]) ).
fof(f1988,plain,
product(a3,a3) = a15,
inference(backward_demodulation,[status(thm)],[f1976,f34]) ).
fof(f1999,plain,
a3 = a15,
inference(forward_demodulation,[status(thm)],[f20,f1988]) ).
fof(f2024,plain,
product(a13,a3) = a3,
inference(forward_demodulation,[status(thm)],[f1936,f1863]) ).
fof(f2031,plain,
product(a3,a3) = a13,
inference(paramodulation,[status(thm)],[f2024,f21]) ).
fof(f2037,plain,
a3 = a13,
inference(forward_demodulation,[status(thm)],[f20,f2031]) ).
fof(f2038,plain,
product(a3,a3) = a7,
inference(forward_demodulation,[status(thm)],[f1915,f1864]) ).
fof(f2040,plain,
a3 = a12,
inference(backward_demodulation,[status(thm)],[f2043,f1977]) ).
fof(f2041,plain,
a10 = product(a3,a2),
inference(backward_demodulation,[status(thm)],[f2043,f1609]) ).
fof(f2043,plain,
a3 = a7,
inference(forward_demodulation,[status(thm)],[f20,f2038]) ).
fof(f2045,plain,
a10 = a1,
inference(forward_demodulation,[status(thm)],[f57,f2041]) ).
fof(f2046,plain,
sF1_fnc = tuple(a2,a3,a3,a5,a3,a7,a8,a9,a10,a11,a12,a13,a14,a15),
inference(forward_demodulation,[status(thm)],[f1876,f1865]) ).
fof(f2047,plain,
sF1_fnc = tuple(a2,a3,a3,a3,a3,a7,a8,a9,a10,a11,a12,a13,a14,a15),
inference(forward_demodulation,[status(thm)],[f1915,f2046]) ).
fof(f2048,plain,
sF1_fnc = tuple(a2,a3,a3,a3,a3,a3,a8,a9,a10,a11,a12,a13,a14,a15),
inference(forward_demodulation,[status(thm)],[f2043,f2047]) ).
fof(f2049,plain,
sF1_fnc = tuple(a2,a3,a3,a3,a3,a3,a3,a9,a10,a11,a12,a13,a14,a15),
inference(forward_demodulation,[status(thm)],[f1936,f2048]) ).
fof(f2050,plain,
sF1_fnc = tuple(a2,a3,a3,a3,a3,a3,a3,a9,a10,a2,a12,a13,a14,a15),
inference(forward_demodulation,[status(thm)],[f1954,f2049]) ).
fof(f2051,plain,
sF1_fnc = tuple(a2,a3,a3,a3,a3,a3,a3,a9,a10,a2,a12,a13,a3,a15),
inference(forward_demodulation,[status(thm)],[f1976,f2050]) ).
fof(f2052,plain,
sF1_fnc = tuple(a2,a3,a3,a3,a3,a3,a3,a9,a10,a2,a12,a13,a3,a3),
inference(forward_demodulation,[status(thm)],[f1999,f2051]) ).
fof(f2053,plain,
sF0_fnc = tuple(a1,a2,a3,a3,a5,a3,a7,a8,a9,a10,a11,a12,a13,a14),
inference(forward_demodulation,[status(thm)],[f1876,f1866]) ).
fof(f2054,plain,
sF0_fnc = tuple(a1,a2,a3,a3,a3,a3,a7,a8,a9,a10,a11,a12,a13,a14),
inference(forward_demodulation,[status(thm)],[f1915,f2053]) ).
fof(f2055,plain,
sF0_fnc = tuple(a1,a2,a3,a3,a3,a3,a3,a8,a9,a10,a11,a12,a13,a14),
inference(forward_demodulation,[status(thm)],[f2043,f2054]) ).
fof(f2056,plain,
sF0_fnc = tuple(a1,a2,a3,a3,a3,a3,a3,a3,a9,a10,a11,a12,a13,a14),
inference(forward_demodulation,[status(thm)],[f1936,f2055]) ).
fof(f2057,plain,
sF0_fnc = tuple(a1,a2,a3,a3,a3,a3,a3,a3,a9,a10,a2,a12,a13,a14),
inference(forward_demodulation,[status(thm)],[f1954,f2056]) ).
fof(f2058,plain,
sF0_fnc = tuple(a1,a2,a3,a3,a3,a3,a3,a3,a9,a10,a2,a12,a13,a3),
inference(forward_demodulation,[status(thm)],[f1976,f2057]) ).
fof(f2059,plain,
sF0_fnc = tuple(a1,a2,a3,a3,a3,a3,a3,a3,a9,a10,a2,a12,a3,a3),
inference(backward_demodulation,[status(thm)],[f2037,f2058]) ).
fof(f2060,plain,
sF1_fnc = tuple(a2,a3,a3,a3,a3,a3,a3,a9,a10,a2,a12,a3,a3,a3),
inference(backward_demodulation,[status(thm)],[f2037,f2052]) ).
fof(f2062,plain,
product(a3,a3) = a11,
inference(forward_demodulation,[status(thm)],[f2043,f1900]) ).
fof(f2063,plain,
a3 = a11,
inference(forward_demodulation,[status(thm)],[f20,f2062]) ).
fof(f2064,plain,
sF1_fnc = tuple(a2,a3,a3,a3,a3,a3,a3,a9,a10,a2,a12,a3,a3,a2),
inference(backward_demodulation,[status(thm)],[f2079,f2060]) ).
fof(f2065,plain,
sF0_fnc = tuple(a1,a2,a3,a3,a3,a3,a3,a3,a9,a10,a2,a12,a3,a2),
inference(backward_demodulation,[status(thm)],[f2079,f2059]) ).
fof(f2077,plain,
product(a2,a2) = a1,
inference(backward_demodulation,[status(thm)],[f2079,f57]) ).
fof(f2079,plain,
a3 = a2,
inference(forward_demodulation,[status(thm)],[f1954,f2063]) ).
fof(f2080,plain,
sF1_fnc = tuple(a2,a2,a3,a3,a3,a3,a3,a9,a10,a2,a12,a3,a3,a2),
inference(forward_demodulation,[status(thm)],[f2079,f2064]) ).
fof(f2081,plain,
sF1_fnc = tuple(a2,a2,a2,a3,a3,a3,a3,a9,a10,a2,a12,a3,a3,a2),
inference(forward_demodulation,[status(thm)],[f2079,f2080]) ).
fof(f2082,plain,
sF1_fnc = tuple(a2,a2,a2,a2,a3,a3,a3,a9,a10,a2,a12,a3,a3,a2),
inference(forward_demodulation,[status(thm)],[f2079,f2081]) ).
fof(f2083,plain,
sF1_fnc = tuple(a2,a2,a2,a2,a2,a3,a3,a9,a10,a2,a12,a3,a3,a2),
inference(forward_demodulation,[status(thm)],[f2079,f2082]) ).
fof(f2084,plain,
sF1_fnc = tuple(a2,a2,a2,a2,a2,a2,a3,a9,a10,a2,a12,a3,a3,a2),
inference(forward_demodulation,[status(thm)],[f2079,f2083]) ).
fof(f2085,plain,
sF1_fnc = tuple(a2,a2,a2,a2,a2,a2,a2,a9,a10,a2,a12,a3,a3,a2),
inference(forward_demodulation,[status(thm)],[f2079,f2084]) ).
fof(f2086,plain,
sF1_fnc = tuple(a2,a2,a2,a2,a2,a2,a2,a9,a10,a2,a12,a2,a3,a2),
inference(forward_demodulation,[status(thm)],[f2079,f2085]) ).
fof(f2087,plain,
sF1_fnc = tuple(a2,a2,a2,a2,a2,a2,a2,a9,a10,a2,a12,a2,a2,a2),
inference(forward_demodulation,[status(thm)],[f2079,f2086]) ).
fof(f2088,plain,
sF0_fnc = tuple(a1,a2,a2,a3,a3,a3,a3,a3,a9,a10,a2,a12,a3,a2),
inference(forward_demodulation,[status(thm)],[f2079,f2065]) ).
fof(f2089,plain,
sF0_fnc = tuple(a1,a2,a2,a2,a3,a3,a3,a3,a9,a10,a2,a12,a3,a2),
inference(forward_demodulation,[status(thm)],[f2079,f2088]) ).
fof(f2090,plain,
sF0_fnc = tuple(a1,a2,a2,a2,a2,a3,a3,a3,a9,a10,a2,a12,a3,a2),
inference(forward_demodulation,[status(thm)],[f2079,f2089]) ).
fof(f2091,plain,
sF0_fnc = tuple(a1,a2,a2,a2,a2,a2,a3,a3,a9,a10,a2,a12,a3,a2),
inference(forward_demodulation,[status(thm)],[f2079,f2090]) ).
fof(f2092,plain,
sF0_fnc = tuple(a1,a2,a2,a2,a2,a2,a2,a3,a9,a10,a2,a12,a3,a2),
inference(forward_demodulation,[status(thm)],[f2079,f2091]) ).
fof(f2093,plain,
sF0_fnc = tuple(a1,a2,a2,a2,a2,a2,a2,a2,a9,a10,a2,a12,a3,a2),
inference(forward_demodulation,[status(thm)],[f2079,f2092]) ).
fof(f2094,plain,
sF0_fnc = tuple(a1,a2,a2,a2,a2,a2,a2,a2,a9,a10,a2,a12,a2,a2),
inference(forward_demodulation,[status(thm)],[f2079,f2093]) ).
fof(f2099,plain,
a2 = a1,
inference(forward_demodulation,[status(thm)],[f20,f2077]) ).
fof(f2100,plain,
a2 = a12,
inference(forward_demodulation,[status(thm)],[f2079,f2040]) ).
fof(f2104,plain,
product(a1,a1) = a9,
inference(backward_demodulation,[status(thm)],[f2045,f52]) ).
fof(f2106,plain,
a1 = a9,
inference(forward_demodulation,[status(thm)],[f20,f2104]) ).
fof(f2121,plain,
a1 = a12,
inference(backward_demodulation,[status(thm)],[f2099,f2100]) ).
fof(f2133,plain,
sF1_fnc = tuple(a1,a2,a2,a2,a2,a2,a2,a9,a10,a2,a12,a2,a2,a2),
inference(forward_demodulation,[status(thm)],[f2099,f2087]) ).
fof(f2134,plain,
sF1_fnc = tuple(a1,a1,a2,a2,a2,a2,a2,a9,a10,a2,a12,a2,a2,a2),
inference(forward_demodulation,[status(thm)],[f2099,f2133]) ).
fof(f2135,plain,
sF1_fnc = tuple(a1,a1,a1,a2,a2,a2,a2,a9,a10,a2,a12,a2,a2,a2),
inference(forward_demodulation,[status(thm)],[f2099,f2134]) ).
fof(f2136,plain,
sF1_fnc = tuple(a1,a1,a1,a1,a2,a2,a2,a9,a10,a2,a12,a2,a2,a2),
inference(forward_demodulation,[status(thm)],[f2099,f2135]) ).
fof(f2137,plain,
sF1_fnc = tuple(a1,a1,a1,a1,a1,a2,a2,a9,a10,a2,a12,a2,a2,a2),
inference(forward_demodulation,[status(thm)],[f2099,f2136]) ).
fof(f2138,plain,
sF1_fnc = tuple(a1,a1,a1,a1,a1,a1,a2,a9,a10,a2,a12,a2,a2,a2),
inference(forward_demodulation,[status(thm)],[f2099,f2137]) ).
fof(f2139,plain,
sF1_fnc = tuple(a1,a1,a1,a1,a1,a1,a1,a9,a10,a2,a12,a2,a2,a2),
inference(forward_demodulation,[status(thm)],[f2099,f2138]) ).
fof(f2140,plain,
sF1_fnc = tuple(a1,a1,a1,a1,a1,a1,a1,a1,a10,a2,a12,a2,a2,a2),
inference(forward_demodulation,[status(thm)],[f2106,f2139]) ).
fof(f2141,plain,
sF1_fnc = tuple(a1,a1,a1,a1,a1,a1,a1,a1,a1,a2,a12,a2,a2,a2),
inference(forward_demodulation,[status(thm)],[f2045,f2140]) ).
fof(f2142,plain,
sF1_fnc = tuple(a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a12,a2,a2,a2),
inference(forward_demodulation,[status(thm)],[f2099,f2141]) ).
fof(f2143,plain,
sF1_fnc = tuple(a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a2,a2,a2),
inference(forward_demodulation,[status(thm)],[f2121,f2142]) ).
fof(f2144,plain,
sF1_fnc = tuple(a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a2,a2),
inference(forward_demodulation,[status(thm)],[f2099,f2143]) ).
fof(f2145,plain,
sF1_fnc = tuple(a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a2),
inference(forward_demodulation,[status(thm)],[f2099,f2144]) ).
fof(f2146,plain,
sF1_fnc = tuple(a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1),
inference(forward_demodulation,[status(thm)],[f2099,f2145]) ).
fof(f2147,plain,
sF0_fnc = tuple(a1,a1,a2,a2,a2,a2,a2,a2,a9,a10,a2,a12,a2,a2),
inference(forward_demodulation,[status(thm)],[f2099,f2094]) ).
fof(f2148,plain,
sF0_fnc = tuple(a1,a1,a1,a2,a2,a2,a2,a2,a9,a10,a2,a12,a2,a2),
inference(forward_demodulation,[status(thm)],[f2099,f2147]) ).
fof(f2149,plain,
sF0_fnc = tuple(a1,a1,a1,a1,a2,a2,a2,a2,a9,a10,a2,a12,a2,a2),
inference(forward_demodulation,[status(thm)],[f2099,f2148]) ).
fof(f2150,plain,
sF0_fnc = tuple(a1,a1,a1,a1,a1,a2,a2,a2,a9,a10,a2,a12,a2,a2),
inference(forward_demodulation,[status(thm)],[f2099,f2149]) ).
fof(f2151,plain,
sF0_fnc = tuple(a1,a1,a1,a1,a1,a1,a2,a2,a9,a10,a2,a12,a2,a2),
inference(forward_demodulation,[status(thm)],[f2099,f2150]) ).
fof(f2152,plain,
sF0_fnc = tuple(a1,a1,a1,a1,a1,a1,a1,a2,a9,a10,a2,a12,a2,a2),
inference(forward_demodulation,[status(thm)],[f2099,f2151]) ).
fof(f2153,plain,
sF0_fnc = tuple(a1,a1,a1,a1,a1,a1,a1,a1,a9,a10,a2,a12,a2,a2),
inference(forward_demodulation,[status(thm)],[f2099,f2152]) ).
fof(f2154,plain,
sF0_fnc = tuple(a1,a1,a1,a1,a1,a1,a1,a1,a1,a10,a2,a12,a2,a2),
inference(forward_demodulation,[status(thm)],[f2106,f2153]) ).
fof(f2155,plain,
sF0_fnc = tuple(a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a2,a12,a2,a2),
inference(forward_demodulation,[status(thm)],[f2045,f2154]) ).
fof(f2156,plain,
sF0_fnc = tuple(a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a12,a2,a2),
inference(forward_demodulation,[status(thm)],[f2099,f2155]) ).
fof(f2157,plain,
sF0_fnc = tuple(a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a2,a2),
inference(forward_demodulation,[status(thm)],[f2121,f2156]) ).
fof(f2158,plain,
sF0_fnc = tuple(a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a2),
inference(forward_demodulation,[status(thm)],[f2099,f2157]) ).
fof(f2159,plain,
sF0_fnc = tuple(a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1,a1),
inference(forward_demodulation,[status(thm)],[f2099,f2158]) ).
fof(f2160,plain,
sF0_fnc = sF1_fnc,
inference(forward_demodulation,[status(thm)],[f2146,f2159]) ).
fof(f2161,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f2160,f41]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : TOP053-1 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.44 % Computer : n001.cluster.edu
% 0.17/0.44 % Model : x86_64 x86_64
% 0.17/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.44 % Memory : 8046.5625MB
% 0.17/0.44 % OS : Linux 6.8.0-71-generic
% 0.17/0.44 % CPULimit : 300
% 0.17/0.44 % WCLimit : 300
% 0.17/0.44 % DateTime : Mon Sep 21 12:53:30 UTC 2026
% 0.17/0.44 % CPUTime :
% 0.17/0.45 % Drodi V4.1.1
% 0.17/0.59 % Refutation found
% 0.17/0.59 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.17/0.59 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.29/0.62 % Elapsed time: 0.157071 seconds
% 0.29/0.62 % CPU time: 1.068201 seconds
% 0.29/0.62 % Total memory used: 41.439 MB
% 0.29/0.62 % Net memory used: 40.940 MB
%------------------------------------------------------------------------------