%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : TOP049-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 : n008.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.15s 0.49s
% Output : CNFRefutation 0.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 36
% Number of leaves : 15
% Syntax : Number of formulae : 138 ( 138 unt; 2 def)
% Number of atoms : 138 ( 137 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 : 14 ( 14 usr; 12 con; 0-9 aty)
% Number of variables : 19 ( 19 !; 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,
a1 = product(a9,a7),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
a3 = product(a1,a2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
a2 = product(a3,a4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,axiom,
a5 = product(a2,a10),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,axiom,
a7 = product(a6,a1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10,axiom,
a8 = product(a7,a4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11,axiom,
a10 = product(a8,a9),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12,axiom,
a4 = product(a10,a3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,axiom,
a9 = product(a4,a8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f14,negated_conjecture,
tuple(a1,a9,a8,a6,a7,a2,a3,a4,a5) != tuple(a2,a10,a9,a7,a8,a3,a4,a5,a6),
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,
a1 = product(a9,a7),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f19,plain,
a3 = product(a1,a2),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f20,plain,
a2 = product(a3,a4),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f21,plain,
a5 = product(a2,a10),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f23,plain,
a7 = product(a6,a1),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f24,plain,
a8 = product(a7,a4),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f25,plain,
a10 = product(a8,a9),
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f26,plain,
a4 = product(a10,a3),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f27,plain,
a9 = product(a4,a8),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f28,plain,
tuple(a1,a9,a8,a6,a7,a2,a3,a4,a5) != tuple(a2,a10,a9,a7,a8,a3,a4,a5,a6),
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f29,definition,
sF0_fnc = tuple(a1,a9,a8,a6,a7,a2,a3,a4,a5),
introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition]) ).
fof(f30,definition,
sF1_fnc = tuple(a2,a10,a9,a7,a8,a3,a4,a5,a6),
introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition]) ).
fof(f31,plain,
sF0_fnc != sF1_fnc,
inference(definition_folding,[],[f28,f30,f29]) ).
fof(f33,plain,
product(a9,a8) = a4,
inference(paramodulation,[status(thm)],[f27,f16]) ).
fof(f34,plain,
product(a4,a3) = a10,
inference(paramodulation,[status(thm)],[f26,f16]) ).
fof(f35,plain,
product(a10,a9) = a8,
inference(paramodulation,[status(thm)],[f25,f16]) ).
fof(f36,plain,
product(a8,a4) = a7,
inference(paramodulation,[status(thm)],[f24,f16]) ).
fof(f37,plain,
product(a7,a1) = a6,
inference(paramodulation,[status(thm)],[f23,f16]) ).
fof(f40,plain,
product(a2,a4) = a3,
inference(paramodulation,[status(thm)],[f20,f16]) ).
fof(f41,plain,
product(a3,a2) = a1,
inference(paramodulation,[status(thm)],[f19,f16]) ).
fof(f42,plain,
product(a1,a7) = a9,
inference(paramodulation,[status(thm)],[f18,f16]) ).
fof(f56,plain,
! [X0,X1,X2] : product(product(product(X0,X1),X2),X1) = product(X0,product(X2,X1)),
inference(paramodulation,[status(thm)],[f16,f17]) ).
fof(f58,plain,
! [X0] : product(product(a4,X0),a8) = product(a9,product(X0,a8)),
inference(paramodulation,[status(thm)],[f27,f17]) ).
fof(f64,plain,
! [X0] : product(product(a7,X0),a4) = product(a8,product(X0,a4)),
inference(paramodulation,[status(thm)],[f24,f17]) ).
fof(f77,plain,
! [X0,X1] : product(product(X0,X1),X0) = product(X0,product(X1,X0)),
inference(paramodulation,[status(thm)],[f15,f17]) ).
fof(f109,plain,
product(a10,a4) = product(a4,product(a3,a4)),
inference(paramodulation,[status(thm)],[f34,f77]) ).
fof(f110,plain,
product(a9,a4) = product(a4,product(a8,a4)),
inference(paramodulation,[status(thm)],[f27,f77]) ).
fof(f113,plain,
product(a7,a8) = product(a8,product(a4,a8)),
inference(paramodulation,[status(thm)],[f36,f77]) ).
fof(f114,plain,
product(a10,a8) = product(a8,product(a9,a8)),
inference(paramodulation,[status(thm)],[f25,f77]) ).
fof(f115,plain,
product(a6,a7) = product(a7,product(a1,a7)),
inference(paramodulation,[status(thm)],[f37,f77]) ).
fof(f121,plain,
product(a3,a2) = product(a2,product(a4,a2)),
inference(paramodulation,[status(thm)],[f40,f77]) ).
fof(f140,plain,
product(a10,a4) = product(a4,a2),
inference(forward_demodulation,[status(thm)],[f20,f109]) ).
fof(f141,plain,
product(a9,a4) = product(a4,a7),
inference(forward_demodulation,[status(thm)],[f36,f110]) ).
fof(f142,plain,
product(a7,a8) = product(a8,a9),
inference(forward_demodulation,[status(thm)],[f27,f113]) ).
fof(f143,plain,
product(a7,a8) = a10,
inference(forward_demodulation,[status(thm)],[f25,f142]) ).
fof(f144,plain,
product(a10,a8) = product(a8,a4),
inference(forward_demodulation,[status(thm)],[f33,f114]) ).
fof(f145,plain,
product(a10,a8) = a7,
inference(forward_demodulation,[status(thm)],[f36,f144]) ).
fof(f146,plain,
product(a6,a7) = product(a7,a9),
inference(forward_demodulation,[status(thm)],[f42,f115]) ).
fof(f147,plain,
a1 = product(a2,product(a4,a2)),
inference(forward_demodulation,[status(thm)],[f41,f121]) ).
fof(f179,plain,
product(product(a6,a7),a9) = a7,
inference(paramodulation,[status(thm)],[f146,f16]) ).
fof(f182,plain,
a1 = product(a2,product(a10,a4)),
inference(forward_demodulation,[status(thm)],[f140,f147]) ).
fof(f186,plain,
product(a1,product(a10,a4)) = a2,
inference(paramodulation,[status(thm)],[f182,f16]) ).
fof(f427,plain,
product(product(a9,a4),a8) = product(a9,product(a7,a8)),
inference(paramodulation,[status(thm)],[f141,f58]) ).
fof(f429,plain,
product(a10,a8) = product(a9,product(a3,a8)),
inference(paramodulation,[status(thm)],[f34,f58]) ).
fof(f444,plain,
product(product(a9,a4),a8) = product(a9,a10),
inference(forward_demodulation,[status(thm)],[f143,f427]) ).
fof(f445,plain,
a7 = product(a9,product(a3,a8)),
inference(forward_demodulation,[status(thm)],[f145,f429]) ).
fof(f483,plain,
product(a7,product(a3,a8)) = a9,
inference(paramodulation,[status(thm)],[f445,f16]) ).
fof(f775,plain,
product(a10,a4) = product(a8,product(a8,a4)),
inference(paramodulation,[status(thm)],[f143,f64]) ).
fof(f792,plain,
product(a10,a4) = product(a8,a7),
inference(forward_demodulation,[status(thm)],[f36,f775]) ).
fof(f839,plain,
product(product(a10,a4),a7) = a8,
inference(paramodulation,[status(thm)],[f792,f16]) ).
fof(f917,plain,
product(product(a9,a10),a4) = product(a9,product(a8,a4)),
inference(paramodulation,[status(thm)],[f444,f56]) ).
fof(f926,plain,
product(product(a9,a10),a4) = product(a9,a7),
inference(forward_demodulation,[status(thm)],[f36,f917]) ).
fof(f927,plain,
product(product(a9,a10),a4) = a1,
inference(forward_demodulation,[status(thm)],[f18,f926]) ).
fof(f940,plain,
product(a1,a4) = product(a9,a10),
inference(paramodulation,[status(thm)],[f927,f16]) ).
fof(f952,plain,
product(product(a1,a4),a10) = a9,
inference(paramodulation,[status(thm)],[f940,f16]) ).
fof(f980,plain,
product(a9,a4) = product(a1,product(a10,a4)),
inference(paramodulation,[status(thm)],[f952,f56]) ).
fof(f989,plain,
product(a9,a4) = a2,
inference(forward_demodulation,[status(thm)],[f186,f980]) ).
fof(f999,plain,
product(a2,a4) = a9,
inference(paramodulation,[status(thm)],[f989,f16]) ).
fof(f1002,plain,
a3 = a9,
inference(forward_demodulation,[status(thm)],[f40,f999]) ).
fof(f1008,plain,
product(a7,product(a9,a8)) = a9,
inference(backward_demodulation,[status(thm)],[f1002,f483]) ).
fof(f1009,plain,
a7 = product(a9,product(a9,a8)),
inference(backward_demodulation,[status(thm)],[f1002,f445]) ).
fof(f1014,plain,
a4 = product(a10,a9),
inference(backward_demodulation,[status(thm)],[f1002,f26]) ).
fof(f1017,plain,
sF1_fnc = tuple(a2,a10,a9,a7,a8,a9,a4,a5,a6),
inference(backward_demodulation,[status(thm)],[f1002,f30]) ).
fof(f1018,plain,
sF0_fnc = tuple(a1,a9,a8,a6,a7,a2,a9,a4,a5),
inference(backward_demodulation,[status(thm)],[f1002,f29]) ).
fof(f1026,plain,
product(a7,a4) = a9,
inference(forward_demodulation,[status(thm)],[f33,f1008]) ).
fof(f1027,plain,
a8 = a9,
inference(forward_demodulation,[status(thm)],[f24,f1026]) ).
fof(f1028,plain,
a7 = product(a9,a4),
inference(forward_demodulation,[status(thm)],[f33,f1009]) ).
fof(f1029,plain,
a7 = a2,
inference(forward_demodulation,[status(thm)],[f989,f1028]) ).
fof(f1033,plain,
a4 = a8,
inference(forward_demodulation,[status(thm)],[f35,f1014]) ).
fof(f1040,plain,
product(product(a10,a8),a7) = a8,
inference(backward_demodulation,[status(thm)],[f1033,f839]) ).
fof(f1055,plain,
a8 = product(a7,a8),
inference(backward_demodulation,[status(thm)],[f1033,f24]) ).
fof(f1060,plain,
product(a7,a7) = a8,
inference(forward_demodulation,[status(thm)],[f145,f1040]) ).
fof(f1061,plain,
a7 = a8,
inference(forward_demodulation,[status(thm)],[f15,f1060]) ).
fof(f1074,plain,
a8 = a10,
inference(forward_demodulation,[status(thm)],[f143,f1055]) ).
fof(f1084,plain,
sF1_fnc = tuple(a2,a10,a9,a7,a8,a9,a8,a5,a6),
inference(forward_demodulation,[status(thm)],[f1033,f1017]) ).
fof(f1085,plain,
sF0_fnc = tuple(a1,a9,a8,a6,a7,a2,a9,a8,a5),
inference(forward_demodulation,[status(thm)],[f1033,f1018]) ).
fof(f1086,plain,
sF0_fnc = tuple(a1,a9,a8,a6,a7,a2,a9,a9,a5),
inference(backward_demodulation,[status(thm)],[f1027,f1085]) ).
fof(f1087,plain,
sF1_fnc = tuple(a2,a10,a9,a7,a8,a9,a9,a5,a6),
inference(backward_demodulation,[status(thm)],[f1027,f1084]) ).
fof(f1096,plain,
sF0_fnc = tuple(a1,a9,a9,a6,a7,a2,a9,a9,a5),
inference(forward_demodulation,[status(thm)],[f1027,f1086]) ).
fof(f1097,plain,
sF1_fnc = tuple(a2,a10,a9,a7,a9,a9,a9,a5,a6),
inference(forward_demodulation,[status(thm)],[f1027,f1087]) ).
fof(f1101,plain,
sF1_fnc = tuple(a7,a10,a9,a7,a9,a9,a9,a5,a6),
inference(backward_demodulation,[status(thm)],[f1029,f1097]) ).
fof(f1102,plain,
sF0_fnc = tuple(a1,a9,a9,a6,a7,a7,a9,a9,a5),
inference(backward_demodulation,[status(thm)],[f1029,f1096]) ).
fof(f1107,plain,
a5 = product(a7,a10),
inference(backward_demodulation,[status(thm)],[f1029,f21]) ).
fof(f1110,plain,
sF0_fnc = tuple(a1,a9,a9,a6,a7,a9,a9,a9,a5),
inference(backward_demodulation,[status(thm)],[f1121,f1102]) ).
fof(f1111,plain,
sF1_fnc = tuple(a7,a10,a9,a9,a9,a9,a9,a5,a6),
inference(backward_demodulation,[status(thm)],[f1121,f1101]) ).
fof(f1115,plain,
product(product(a6,a7),a9) = a9,
inference(backward_demodulation,[status(thm)],[f1121,f179]) ).
fof(f1120,plain,
a1 = product(a9,a9),
inference(backward_demodulation,[status(thm)],[f1121,f18]) ).
fof(f1121,plain,
a7 = a9,
inference(forward_demodulation,[status(thm)],[f1027,f1061]) ).
fof(f1122,plain,
sF0_fnc = tuple(a1,a9,a9,a6,a9,a9,a9,a9,a5),
inference(forward_demodulation,[status(thm)],[f1121,f1110]) ).
fof(f1123,plain,
sF1_fnc = tuple(a9,a10,a9,a9,a9,a9,a9,a5,a6),
inference(forward_demodulation,[status(thm)],[f1121,f1111]) ).
fof(f1124,plain,
product(product(a6,a9),a9) = a9,
inference(forward_demodulation,[status(thm)],[f1121,f1115]) ).
fof(f1125,plain,
a6 = a9,
inference(forward_demodulation,[status(thm)],[f16,f1124]) ).
fof(f1129,plain,
a1 = a9,
inference(forward_demodulation,[status(thm)],[f15,f1120]) ).
fof(f1132,plain,
a7 = a10,
inference(backward_demodulation,[status(thm)],[f1136,f1121]) ).
fof(f1136,plain,
a9 = a10,
inference(forward_demodulation,[status(thm)],[f1027,f1074]) ).
fof(f1139,plain,
a6 = a10,
inference(forward_demodulation,[status(thm)],[f1136,f1125]) ).
fof(f1140,plain,
a6 = a1,
inference(backward_demodulation,[status(thm)],[f1144,f1139]) ).
fof(f1143,plain,
a9 = a1,
inference(backward_demodulation,[status(thm)],[f1144,f1136]) ).
fof(f1144,plain,
a1 = a10,
inference(forward_demodulation,[status(thm)],[f1136,f1129]) ).
fof(f1146,plain,
a7 = a1,
inference(forward_demodulation,[status(thm)],[f1144,f1132]) ).
fof(f1155,plain,
a5 = product(a1,a10),
inference(forward_demodulation,[status(thm)],[f1146,f1107]) ).
fof(f1156,plain,
a5 = product(a1,a1),
inference(forward_demodulation,[status(thm)],[f1144,f1155]) ).
fof(f1158,plain,
a5 = a1,
inference(forward_demodulation,[status(thm)],[f15,f1156]) ).
fof(f1193,plain,
sF0_fnc = tuple(a1,a1,a9,a6,a9,a9,a9,a9,a5),
inference(forward_demodulation,[status(thm)],[f1143,f1122]) ).
fof(f1194,plain,
sF0_fnc = tuple(a1,a1,a1,a6,a9,a9,a9,a9,a5),
inference(forward_demodulation,[status(thm)],[f1143,f1193]) ).
fof(f1195,plain,
sF0_fnc = tuple(a1,a1,a1,a1,a9,a9,a9,a9,a5),
inference(forward_demodulation,[status(thm)],[f1140,f1194]) ).
fof(f1196,plain,
sF0_fnc = tuple(a1,a1,a1,a1,a1,a9,a9,a9,a5),
inference(forward_demodulation,[status(thm)],[f1143,f1195]) ).
fof(f1197,plain,
sF0_fnc = tuple(a1,a1,a1,a1,a1,a1,a9,a9,a5),
inference(forward_demodulation,[status(thm)],[f1143,f1196]) ).
fof(f1198,plain,
sF0_fnc = tuple(a1,a1,a1,a1,a1,a1,a1,a9,a5),
inference(forward_demodulation,[status(thm)],[f1143,f1197]) ).
fof(f1199,plain,
sF0_fnc = tuple(a1,a1,a1,a1,a1,a1,a1,a1,a5),
inference(forward_demodulation,[status(thm)],[f1143,f1198]) ).
fof(f1200,plain,
sF0_fnc = tuple(a1,a1,a1,a1,a1,a1,a1,a1,a1),
inference(forward_demodulation,[status(thm)],[f1158,f1199]) ).
fof(f1201,plain,
sF1_fnc = tuple(a1,a10,a9,a9,a9,a9,a9,a5,a6),
inference(forward_demodulation,[status(thm)],[f1143,f1123]) ).
fof(f1202,plain,
sF1_fnc = tuple(a1,a1,a9,a9,a9,a9,a9,a5,a6),
inference(forward_demodulation,[status(thm)],[f1144,f1201]) ).
fof(f1203,plain,
sF1_fnc = tuple(a1,a1,a1,a9,a9,a9,a9,a5,a6),
inference(forward_demodulation,[status(thm)],[f1143,f1202]) ).
fof(f1204,plain,
sF1_fnc = tuple(a1,a1,a1,a1,a9,a9,a9,a5,a6),
inference(forward_demodulation,[status(thm)],[f1143,f1203]) ).
fof(f1205,plain,
sF1_fnc = tuple(a1,a1,a1,a1,a1,a9,a9,a5,a6),
inference(forward_demodulation,[status(thm)],[f1143,f1204]) ).
fof(f1206,plain,
sF1_fnc = tuple(a1,a1,a1,a1,a1,a1,a9,a5,a6),
inference(forward_demodulation,[status(thm)],[f1143,f1205]) ).
fof(f1207,plain,
sF1_fnc = tuple(a1,a1,a1,a1,a1,a1,a1,a5,a6),
inference(forward_demodulation,[status(thm)],[f1143,f1206]) ).
fof(f1208,plain,
sF1_fnc = tuple(a1,a1,a1,a1,a1,a1,a1,a1,a6),
inference(forward_demodulation,[status(thm)],[f1158,f1207]) ).
fof(f1209,plain,
sF1_fnc = tuple(a1,a1,a1,a1,a1,a1,a1,a1,a1),
inference(forward_demodulation,[status(thm)],[f1140,f1208]) ).
fof(f1210,plain,
sF1_fnc = sF0_fnc,
inference(forward_demodulation,[status(thm)],[f1200,f1209]) ).
fof(f1211,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f1210,f31]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : TOP049-1 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.05 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/0.42 % Computer : n008.cluster.edu
% 0.15/0.42 % Model : x86_64 x86_64
% 0.15/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.42 % Memory : 8046.5625MB
% 0.15/0.42 % OS : Linux 6.8.0-71-generic
% 0.15/0.42 % CPULimit : 300
% 0.15/0.42 % WCLimit : 300
% 0.15/0.42 % DateTime : Mon Sep 21 12:48:08 UTC 2026
% 0.15/0.43 % CPUTime :
% 0.15/0.43 % Drodi V4.1.1
% 0.15/0.49 % Refutation found
% 0.15/0.49 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.15/0.49 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.15/0.51 % Elapsed time: 0.077078 seconds
% 0.15/0.51 % CPU time: 0.435912 seconds
% 0.15/0.51 % Total memory used: 17.417 MB
% 0.15/0.51 % Net memory used: 17.226 MB
%------------------------------------------------------------------------------