%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GRP777-10 : TPTP v9.3.1. Released v8.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n007.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 12:35:19 PM UTC 2026
% Result : Unsatisfiable 260.09s 33.39s
% Output : CNFRefutation 21.44s
% Verified :
% SZS Type : Refutation
% Derivation depth : 41
% Number of leaves : 12
% Syntax : Number of formulae : 160 ( 160 unt; 2 def)
% Number of atoms : 160 ( 159 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 3 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 6 con; 0-3 aty)
% Number of variables : 316 ( 316 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,B] : difference(A,product(A,B)) = B,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [A,B] : product(A,difference(A,B)) = B,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [A,B] : quotient(product(A,B),B) = A,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [A,B] : product(quotient(A,B),B) = A,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [A,B,C,D] : product(product(A,B),product(C,D)) = product(product(A,C),product(B,D)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [A] : product(A,A) = A,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [A,B] : product(product(product(A,B),B),product(B,product(B,A))) = B,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [A,B,C] : bigC(A,B,C) = product(product(A,B),product(C,A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,axiom,
product(product(a,c),product(c,b)) = product(a,b),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,negated_conjecture,
bigC(a,b,x0) != bigC(c,c,x0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,plain,
! [X0,X1] : difference(X0,product(X0,X1)) = X1,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f12,plain,
! [X0,X1] : product(X0,difference(X0,X1)) = X1,
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f13,plain,
! [X0,X1] : quotient(product(X0,X1),X1) = X0,
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f14,plain,
! [X0,X1] : product(quotient(X0,X1),X1) = X0,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f15,plain,
! [X0,X1,X2,X3] : product(product(X0,X1),product(X2,X3)) = product(product(X0,X2),product(X1,X3)),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f16,plain,
! [X0] : product(X0,X0) = X0,
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f17,plain,
! [X0,X1] : product(product(product(X0,X1),X1),product(X1,product(X1,X0))) = X1,
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f18,plain,
! [X0,X1,X2] : bigC(X0,X1,X2) = product(product(X0,X1),product(X2,X0)),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f19,plain,
product(product(a,c),product(c,b)) = product(a,b),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f20,plain,
bigC(a,b,x0) != bigC(c,c,x0),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f21,definition,
sF0_fnc = bigC(a,b,x0),
introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition]) ).
fof(f22,definition,
sF1_fnc = bigC(c,c,x0),
introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition]) ).
fof(f23,plain,
sF0_fnc != sF1_fnc,
inference(definition_folding,[],[f20,f22,f21]) ).
fof(f28,plain,
! [X0,X1] : bigC(X0,X1,X0) = product(product(X0,X1),X0),
inference(paramodulation,[status(thm)],[f16,f18]) ).
fof(f29,plain,
! [X0,X1] : bigC(X0,X0,X1) = product(X0,product(X1,X0)),
inference(paramodulation,[status(thm)],[f16,f18]) ).
fof(f32,plain,
! [X0,X1,X2] : difference(product(X0,X1),bigC(X0,X1,X2)) = product(X2,X0),
inference(paramodulation,[status(thm)],[f18,f11]) ).
fof(f34,plain,
! [X0,X1,X2] : quotient(bigC(X0,X1,X2),product(X2,X0)) = product(X0,X1),
inference(paramodulation,[status(thm)],[f18,f13]) ).
fof(f39,plain,
! [X0,X1] : difference(quotient(X0,X1),X0) = X1,
inference(paramodulation,[status(thm)],[f14,f11]) ).
fof(f40,plain,
! [X0,X1,X2] : bigC(X0,X1,quotient(X2,X0)) = product(product(X0,X1),X2),
inference(paramodulation,[status(thm)],[f14,f18]) ).
fof(f41,plain,
! [X0,X1,X2] : bigC(quotient(X0,X1),X1,X2) = product(X0,product(X2,quotient(X0,X1))),
inference(paramodulation,[status(thm)],[f14,f18]) ).
fof(f47,plain,
! [X0,X1] : quotient(X0,difference(X1,X0)) = X1,
inference(paramodulation,[status(thm)],[f12,f13]) ).
fof(f49,plain,
! [X0,X1,X2] : bigC(difference(X0,X1),X2,X0) = product(product(difference(X0,X1),X2),X1),
inference(paramodulation,[status(thm)],[f12,f18]) ).
fof(f50,plain,
! [X0,X1,X2] : bigC(X0,difference(X0,X1),X2) = product(X1,product(X2,X0)),
inference(paramodulation,[status(thm)],[f12,f18]) ).
fof(f62,plain,
! [X0,X1] : difference(X0,bigC(X0,X0,X1)) = product(X1,X0),
inference(paramodulation,[status(thm)],[f29,f11]) ).
fof(f69,plain,
difference(c,sF1_fnc) = product(x0,c),
inference(paramodulation,[status(thm)],[f22,f62]) ).
fof(f93,plain,
! [X0,X1] : quotient(X0,product(X0,product(X0,X1))) = product(product(X1,X0),X0),
inference(paramodulation,[status(thm)],[f17,f13]) ).
fof(f130,plain,
! [X0,X1] : quotient(bigC(X0,X1,X0),X0) = product(X0,X1),
inference(paramodulation,[status(thm)],[f28,f13]) ).
fof(f177,plain,
difference(product(a,b),sF0_fnc) = product(x0,a),
inference(paramodulation,[status(thm)],[f21,f32]) ).
fof(f209,plain,
! [X0,X1,X2] : quotient(bigC(difference(X0,X1),X2,X0),X1) = product(difference(X0,X1),X2),
inference(paramodulation,[status(thm)],[f12,f34]) ).
fof(f307,plain,
difference(product(a,c),product(a,b)) = product(c,b),
inference(paramodulation,[status(thm)],[f19,f11]) ).
fof(f323,plain,
! [X0,X1] : quotient(X0,product(X0,X1)) = product(product(difference(X0,X1),X0),X0),
inference(paramodulation,[status(thm)],[f12,f93]) ).
fof(f341,plain,
! [X0,X1,X2] : bigC(X0,X1,X2) = product(product(X0,X2),product(X1,X0)),
inference(paramodulation,[status(thm)],[f18,f15]) ).
fof(f353,plain,
! [X0,X1,X2,X3] : product(X0,product(X1,X2)) = product(product(X3,X1),product(difference(X3,X0),X2)),
inference(paramodulation,[status(thm)],[f12,f15]) ).
fof(f354,plain,
! [X0,X1,X2] : product(X0,product(X1,X2)) = product(product(X0,X1),product(X0,X2)),
inference(paramodulation,[status(thm)],[f16,f15]) ).
fof(f364,plain,
! [X0,X1,X2] : product(product(X0,X1),X2) = product(product(X0,X2),product(X1,X2)),
inference(paramodulation,[status(thm)],[f16,f15]) ).
fof(f504,plain,
! [X0,X1,X2] : bigC(X0,X1,X2) = bigC(X0,X2,X1),
inference(paramodulation,[status(thm)],[f18,f341]) ).
fof(f506,plain,
! [X0,X1,X2] : bigC(quotient(X0,X1),X2,X1) = product(X0,product(X2,quotient(X0,X1))),
inference(paramodulation,[status(thm)],[f14,f341]) ).
fof(f515,plain,
! [X0,X1,X2] : bigC(X0,X1,difference(X0,X2)) = product(X2,product(X1,X0)),
inference(paramodulation,[status(thm)],[f12,f341]) ).
fof(f517,plain,
! [X0,X1,X2] : bigC(X0,quotient(X1,X0),X2) = product(product(X0,X2),X1),
inference(paramodulation,[status(thm)],[f14,f341]) ).
fof(f550,plain,
! [X0,X1,X2] : quotient(bigC(X0,X1,X2),product(X1,X0)) = product(X0,X2),
inference(paramodulation,[status(thm)],[f341,f13]) ).
fof(f551,plain,
! [X0,X1,X2] : difference(product(X0,X1),bigC(X0,X2,X1)) = product(X2,X0),
inference(paramodulation,[status(thm)],[f341,f11]) ).
fof(f600,plain,
! [X0,X1] : quotient(bigC(X0,X0,X1),X0) = product(X0,X1),
inference(paramodulation,[status(thm)],[f504,f130]) ).
fof(f601,plain,
! [X0,X1] : difference(X0,bigC(X0,X1,X0)) = product(X1,X0),
inference(paramodulation,[status(thm)],[f504,f62]) ).
fof(f611,plain,
! [X0,X1] : difference(X0,product(X1,product(X0,X0))) = product(difference(X0,X1),X0),
inference(paramodulation,[status(thm)],[f50,f601]) ).
fof(f621,plain,
! [X0,X1] : difference(X0,product(X1,X0)) = product(difference(X0,X1),X0),
inference(forward_demodulation,[status(thm)],[f16,f611]) ).
fof(f624,plain,
quotient(sF1_fnc,c) = product(c,x0),
inference(paramodulation,[status(thm)],[f22,f600]) ).
fof(f626,plain,
! [X0,X1] : quotient(product(product(X0,X0),X1),X0) = product(X0,quotient(X1,X0)),
inference(paramodulation,[status(thm)],[f40,f600]) ).
fof(f636,plain,
! [X0,X1] : quotient(product(X0,X1),X0) = product(X0,quotient(X1,X0)),
inference(forward_demodulation,[status(thm)],[f16,f626]) ).
fof(f738,plain,
! [X0,X1] : difference(X0,X1) = product(difference(X0,quotient(X1,X0)),X0),
inference(paramodulation,[status(thm)],[f14,f621]) ).
fof(f741,plain,
! [X0,X1,X2] : difference(product(X0,X1),bigC(X1,X0,X2)) = product(difference(product(X0,X1),product(X1,X2)),product(X0,X1)),
inference(paramodulation,[status(thm)],[f341,f621]) ).
fof(f743,plain,
! [X0,X1,X2,X3] : difference(product(X0,X1),product(product(X2,X0),product(X3,X1))) = product(difference(product(X0,X1),product(X2,X3)),product(X0,X1)),
inference(paramodulation,[status(thm)],[f15,f621]) ).
fof(f744,plain,
! [X0,X1,X2] : difference(product(X0,X1),bigC(X1,X2,X0)) = product(difference(product(X0,X1),product(X1,X2)),product(X0,X1)),
inference(paramodulation,[status(thm)],[f18,f621]) ).
fof(f751,plain,
! [X0,X1,X2] : bigC(X0,product(difference(X0,X1),X0),X2) = product(product(X1,X0),product(X2,X0)),
inference(paramodulation,[status(thm)],[f621,f50]) ).
fof(f754,plain,
! [X0,X1,X2] : bigC(X0,product(difference(X0,X1),X0),X2) = product(product(X1,X2),X0),
inference(forward_demodulation,[status(thm)],[f364,f751]) ).
fof(f856,plain,
! [X0,X1,X2] : quotient(bigC(X0,X1,X2),product(X0,X1)) = product(product(X0,X1),quotient(product(X2,X0),product(X0,X1))),
inference(paramodulation,[status(thm)],[f18,f636]) ).
fof(f860,plain,
! [X0,X1] : quotient(X0,X1) = product(X1,quotient(difference(X1,X0),X1)),
inference(paramodulation,[status(thm)],[f12,f636]) ).
fof(f1258,plain,
! [X0,X1] : bigC(difference(X0,quotient(X1,X0)),X0,X0) = product(difference(X0,X1),quotient(X1,X0)),
inference(paramodulation,[status(thm)],[f738,f49]) ).
fof(f1282,plain,
! [X0,X1] : quotient(difference(X0,X1),X0) = difference(X0,quotient(X1,X0)),
inference(paramodulation,[status(thm)],[f738,f13]) ).
fof(f1326,plain,
! [X0,X1] : bigC(quotient(difference(X0,X1),X0),X0,X0) = product(difference(X0,X1),quotient(X1,X0)),
inference(backward_demodulation,[status(thm)],[f1282,f1258]) ).
fof(f1362,plain,
! [X0,X1] : quotient(quotient(X0,X1),quotient(difference(X1,X0),X1)) = X1,
inference(paramodulation,[status(thm)],[f1282,f47]) ).
fof(f2232,plain,
quotient(sF0_fnc,product(b,a)) = product(a,x0),
inference(paramodulation,[status(thm)],[f21,f550]) ).
fof(f2309,plain,
difference(product(a,x0),sF0_fnc) = product(b,a),
inference(paramodulation,[status(thm)],[f2232,f39]) ).
fof(f2314,plain,
quotient(sF0_fnc,product(a,x0)) = product(product(a,x0),quotient(product(b,a),product(a,x0))),
inference(paramodulation,[status(thm)],[f2309,f860]) ).
fof(f2323,plain,
quotient(sF0_fnc,product(a,x0)) = quotient(bigC(a,x0,b),product(a,x0)),
inference(forward_demodulation,[status(thm)],[f856,f2314]) ).
fof(f2403,plain,
! [X0,X1,X2] : difference(X0,bigC(quotient(X0,X1),X2,X1)) = product(X2,quotient(X0,X1)),
inference(paramodulation,[status(thm)],[f14,f551]) ).
fof(f2585,plain,
! [X0,X1] : difference(X0,quotient(X0,product(X0,X1))) = product(difference(X0,product(difference(X0,X1),X0)),X0),
inference(paramodulation,[status(thm)],[f323,f621]) ).
fof(f2586,plain,
! [X0,X1,X2] : bigC(X0,product(difference(X0,X1),X0),X2) = product(product(X0,X2),quotient(X0,product(X0,X1))),
inference(paramodulation,[status(thm)],[f323,f341]) ).
fof(f2638,plain,
! [X0,X1] : difference(X0,quotient(X0,product(X0,X1))) = product(product(difference(X0,difference(X0,X1)),X0),X0),
inference(forward_demodulation,[status(thm)],[f621,f2585]) ).
fof(f2639,plain,
! [X0,X1] : difference(X0,quotient(X0,product(X0,X1))) = quotient(X0,product(X0,difference(X0,X1))),
inference(forward_demodulation,[status(thm)],[f323,f2638]) ).
fof(f2640,plain,
! [X0,X1] : difference(X0,quotient(X0,product(X0,X1))) = quotient(X0,X1),
inference(forward_demodulation,[status(thm)],[f12,f2639]) ).
fof(f2682,plain,
! [X0,X1,X2] : product(product(X0,X1),X2) = product(product(X2,X1),quotient(X2,product(X2,X0))),
inference(forward_demodulation,[status(thm)],[f754,f2586]) ).
fof(f2747,plain,
! [X0,X1] : difference(X0,quotient(X0,X1)) = quotient(X0,difference(X0,X1)),
inference(paramodulation,[status(thm)],[f12,f2640]) ).
fof(f2757,plain,
! [X0,X1] : product(X0,quotient(X0,X1)) = quotient(X0,product(X0,X1)),
inference(paramodulation,[status(thm)],[f2640,f12]) ).
fof(f2792,plain,
! [X0,X1,X2] : product(product(X0,X1),X2) = product(product(X2,X1),product(X2,quotient(X2,X0))),
inference(backward_demodulation,[status(thm)],[f2757,f2682]) ).
fof(f2830,plain,
! [X0,X1,X2] : bigC(quotient(X0,X1),X1,X2) = product(product(X1,X2),X0),
inference(backward_demodulation,[status(thm)],[f2836,f41]) ).
fof(f2835,plain,
! [X0,X1,X2] : bigC(quotient(X0,X1),X2,X1) = product(product(X1,X2),X0),
inference(backward_demodulation,[status(thm)],[f2836,f506]) ).
fof(f2836,plain,
! [X0,X1,X2] : product(product(X0,X1),X2) = product(X2,product(X1,quotient(X2,X0))),
inference(forward_demodulation,[status(thm)],[f354,f2792]) ).
fof(f2870,plain,
! [X0,X1] : product(product(X0,X0),difference(X0,X1)) = product(difference(X0,X1),quotient(X1,X0)),
inference(backward_demodulation,[status(thm)],[f2830,f1326]) ).
fof(f2918,plain,
! [X0,X1,X2] : difference(X0,product(product(X1,X2),X0)) = product(X2,quotient(X0,X1)),
inference(backward_demodulation,[status(thm)],[f2835,f2403]) ).
fof(f2922,plain,
! [X0,X1,X2] : difference(product(X0,X1),bigC(X1,X2,X0)) = product(X2,quotient(product(X0,X1),X1)),
inference(backward_demodulation,[status(thm)],[f2927,f744]) ).
fof(f2923,plain,
! [X0,X1,X2] : difference(product(X0,X1),bigC(X1,X0,X2)) = product(X2,quotient(product(X0,X1),X1)),
inference(backward_demodulation,[status(thm)],[f2927,f741]) ).
fof(f2924,plain,
! [X0,X1,X2,X3] : difference(product(X0,X1),product(product(X2,X0),product(X3,X1))) = product(X3,quotient(product(X0,X1),X2)),
inference(backward_demodulation,[status(thm)],[f2927,f743]) ).
fof(f2927,plain,
! [X0,X1,X2] : product(difference(X0,product(X1,X2)),X0) = product(X2,quotient(X0,X1)),
inference(forward_demodulation,[status(thm)],[f621,f2918]) ).
fof(f2933,plain,
! [X0,X1] : product(X0,difference(X0,X1)) = product(difference(X0,X1),quotient(X1,X0)),
inference(forward_demodulation,[status(thm)],[f16,f2870]) ).
fof(f2934,plain,
! [X0,X1] : X0 = product(difference(X1,X0),quotient(X0,X1)),
inference(forward_demodulation,[status(thm)],[f12,f2933]) ).
fof(f2941,plain,
! [X0,X1,X2] : difference(product(X0,X1),bigC(X1,X0,X2)) = product(X2,X0),
inference(forward_demodulation,[status(thm)],[f13,f2923]) ).
fof(f2947,plain,
! [X0,X1,X2] : difference(product(X0,X1),bigC(X1,X2,X0)) = product(X2,X0),
inference(forward_demodulation,[status(thm)],[f13,f2922]) ).
fof(f3664,plain,
! [X0,X1] : difference(X0,X1) = quotient(X0,difference(X0,difference(X1,X0))),
inference(paramodulation,[status(thm)],[f47,f2747]) ).
fof(f3721,plain,
! [X0,X1] : product(difference(X0,X1),difference(X0,difference(X1,X0))) = X0,
inference(paramodulation,[status(thm)],[f3664,f14]) ).
fof(f4975,plain,
sF0_fnc = product(product(b,a),quotient(sF0_fnc,product(a,x0))),
inference(paramodulation,[status(thm)],[f2309,f2934]) ).
fof(f4976,plain,
sF0_fnc = product(product(x0,a),quotient(sF0_fnc,product(a,b))),
inference(paramodulation,[status(thm)],[f177,f2934]) ).
fof(f4978,plain,
! [X0,X1,X2] : bigC(X0,X1,X2) = product(product(X1,X0),quotient(bigC(X0,X1,X2),product(X0,X2))),
inference(paramodulation,[status(thm)],[f551,f2934]) ).
fof(f4987,plain,
! [X0,X1] : bigC(X0,X1,X0) = product(product(X1,X0),quotient(bigC(X0,X1,X0),X0)),
inference(paramodulation,[status(thm)],[f601,f2934]) ).
fof(f4988,plain,
! [X0,X1] : bigC(X0,X0,X1) = product(product(X1,X0),quotient(bigC(X0,X0,X1),X0)),
inference(paramodulation,[status(thm)],[f62,f2934]) ).
fof(f5001,plain,
sF1_fnc = product(difference(c,sF1_fnc),product(c,x0)),
inference(paramodulation,[status(thm)],[f624,f2934]) ).
fof(f5056,plain,
! [X0,X1] : quotient(X0,quotient(X0,X1)) = difference(X1,X0),
inference(paramodulation,[status(thm)],[f2934,f13]) ).
fof(f5080,plain,
! [X0,X1] : bigC(X0,X1,X0) = product(product(X1,X0),product(X0,X1)),
inference(forward_demodulation,[status(thm)],[f130,f4987]) ).
fof(f5081,plain,
! [X0,X1] : bigC(X0,X1,X0) = bigC(X1,X0,X0),
inference(forward_demodulation,[status(thm)],[f341,f5080]) ).
fof(f5085,plain,
! [X0,X1] : bigC(X0,X0,X1) = product(product(X1,X0),product(X0,X1)),
inference(forward_demodulation,[status(thm)],[f600,f4988]) ).
fof(f5086,plain,
! [X0,X1] : bigC(X0,X0,X1) = bigC(X1,X0,X0),
inference(forward_demodulation,[status(thm)],[f341,f5085]) ).
fof(f5112,plain,
sF1_fnc = product(product(x0,c),product(c,x0)),
inference(forward_demodulation,[status(thm)],[f69,f5001]) ).
fof(f5113,plain,
sF1_fnc = bigC(x0,c,c),
inference(forward_demodulation,[status(thm)],[f341,f5112]) ).
fof(f6351,plain,
! [X0,X1,X2] : quotient(bigC(X0,X1,X2),product(X0,X2)) = difference(product(X1,X0),bigC(X0,X1,X2)),
inference(paramodulation,[status(thm)],[f550,f5056]) ).
fof(f6352,plain,
! [X0,X1,X2] : quotient(bigC(X0,X1,X2),product(X0,X1)) = difference(product(X2,X0),bigC(X0,X1,X2)),
inference(paramodulation,[status(thm)],[f34,f5056]) ).
fof(f6360,plain,
! [X0,X1] : quotient(product(X0,X1),X0) = difference(X1,product(X0,X1)),
inference(paramodulation,[status(thm)],[f13,f5056]) ).
fof(f6410,plain,
quotient(sF0_fnc,product(a,x0)) = product(x0,b),
inference(backward_demodulation,[status(thm)],[f6416,f2323]) ).
fof(f6416,plain,
! [X0,X1,X2] : quotient(bigC(X0,X1,X2),product(X0,X1)) = product(X1,X2),
inference(forward_demodulation,[status(thm)],[f2947,f6352]) ).
fof(f6417,plain,
! [X0,X1,X2] : bigC(X0,X1,X2) = product(product(X1,X0),product(X2,X1)),
inference(backward_demodulation,[status(thm)],[f6421,f4978]) ).
fof(f6421,plain,
! [X0,X1,X2] : quotient(bigC(X0,X1,X2),product(X0,X2)) = product(X2,X1),
inference(forward_demodulation,[status(thm)],[f2941,f6351]) ).
fof(f6465,plain,
sF0_fnc = product(product(b,a),product(x0,b)),
inference(backward_demodulation,[status(thm)],[f6410,f4975]) ).
fof(f6470,plain,
sF0_fnc = bigC(b,x0,a),
inference(forward_demodulation,[status(thm)],[f341,f6465]) ).
fof(f6479,plain,
quotient(sF0_fnc,product(a,b)) = product(b,x0),
inference(paramodulation,[status(thm)],[f6470,f34]) ).
fof(f6483,plain,
sF0_fnc = product(product(x0,a),product(b,x0)),
inference(backward_demodulation,[status(thm)],[f6479,f4976]) ).
fof(f6485,plain,
sF0_fnc = bigC(x0,b,a),
inference(forward_demodulation,[status(thm)],[f341,f6483]) ).
fof(f6619,plain,
! [X0,X1] : difference(X0,bigC(X1,X0,X0)) = product(X1,X0),
inference(paramodulation,[status(thm)],[f5081,f601]) ).
fof(f6769,plain,
! [X0,X1] : product(X0,product(X1,X0)) = bigC(X1,X0,X0),
inference(paramodulation,[status(thm)],[f6619,f12]) ).
fof(f6805,plain,
! [X0,X1] : product(product(difference(X0,X1),difference(X0,X1)),X1) = bigC(X0,difference(X0,X1),difference(X0,X1)),
inference(paramodulation,[status(thm)],[f49,f5086]) ).
fof(f6849,plain,
! [X0,X1] : product(difference(X0,X1),X1) = bigC(X0,difference(X0,X1),difference(X0,X1)),
inference(forward_demodulation,[status(thm)],[f16,f6805]) ).
fof(f6854,plain,
! [X0,X1] : product(difference(X0,X1),X1) = product(X1,product(difference(X0,X1),X0)),
inference(forward_demodulation,[status(thm)],[f50,f6849]) ).
fof(f9627,plain,
! [X0,X1,X2,X3] : quotient(product(product(X0,X1),product(X2,X3)),product(X0,X1)) = difference(product(X2,X3),product(product(X0,X2),product(X1,X3))),
inference(paramodulation,[status(thm)],[f15,f6360]) ).
fof(f9671,plain,
! [X0,X1] : quotient(quotient(product(X0,X1),X1),quotient(quotient(product(X0,X1),X0),X1)) = X1,
inference(paramodulation,[status(thm)],[f6360,f1362]) ).
fof(f9790,plain,
! [X0,X1,X2,X3] : product(product(X0,X1),quotient(product(X2,X3),product(X0,X1))) = difference(product(X2,X3),product(product(X0,X2),product(X1,X3))),
inference(forward_demodulation,[status(thm)],[f636,f9627]) ).
fof(f9802,plain,
! [X0,X1,X2,X3] : product(product(X0,X1),quotient(product(X2,X3),product(X0,X1))) = product(X1,quotient(product(X2,X3),X0)),
inference(forward_demodulation,[status(thm)],[f2924,f9790]) ).
fof(f9859,plain,
! [X0,X1] : quotient(X0,quotient(quotient(product(X0,X1),X0),X1)) = X1,
inference(forward_demodulation,[status(thm)],[f13,f9671]) ).
fof(f9860,plain,
! [X0,X1] : quotient(X0,quotient(product(X0,quotient(X1,X0)),X1)) = X1,
inference(forward_demodulation,[status(thm)],[f636,f9859]) ).
fof(f10614,plain,
! [X0,X1,X2] : bigC(quotient(product(X0,quotient(X1,X0)),X1),X1,X2) = product(product(quotient(product(X0,quotient(X1,X0)),X1),X2),X0),
inference(paramodulation,[status(thm)],[f9860,f517]) ).
fof(f10617,plain,
! [X0,X1] : difference(X0,X1) = quotient(product(X1,quotient(X0,X1)),X0),
inference(paramodulation,[status(thm)],[f9860,f39]) ).
fof(f10692,plain,
! [X0,X1,X2] : product(product(X0,X1),product(X2,quotient(X0,X2))) = product(product(quotient(product(X2,quotient(X0,X2)),X0),X1),X2),
inference(forward_demodulation,[status(thm)],[f2830,f10614]) ).
fof(f10694,plain,
! [X0,X1,X2] : product(product(X0,X1),product(X2,quotient(X0,X2))) = product(product(difference(X0,X2),X1),X2),
inference(forward_demodulation,[status(thm)],[f10617,f10692]) ).
fof(f10963,plain,
! [X0,X1,X2] : bigC(X0,difference(X0,X1),X2) = product(product(X0,X2),product(X1,quotient(X0,X1))),
inference(paramodulation,[status(thm)],[f10617,f517]) ).
fof(f11009,plain,
! [X0,X1,X2] : product(X0,product(X1,X2)) = product(product(difference(X2,X0),X1),X0),
inference(backward_demodulation,[status(thm)],[f11010,f10694]) ).
fof(f11010,plain,
! [X0,X1,X2] : product(X0,product(X1,X2)) = product(product(X2,X1),product(X0,quotient(X2,X0))),
inference(forward_demodulation,[status(thm)],[f50,f10963]) ).
fof(f11064,plain,
! [X0,X1,X2] : bigC(difference(X0,X1),X2,X0) = product(X1,product(X2,X0)),
inference(backward_demodulation,[status(thm)],[f11009,f49]) ).
fof(f11165,plain,
! [X0,X1,X2] : quotient(product(X0,product(X1,X2)),X0) = product(difference(X2,X0),X1),
inference(backward_demodulation,[status(thm)],[f11064,f209]) ).
fof(f11213,plain,
! [X0,X1,X2,X3] : product(difference(X0,product(X1,X2)),X3) = product(X2,quotient(product(X3,X0),X1)),
inference(backward_demodulation,[status(thm)],[f11215,f9802]) ).
fof(f11215,plain,
! [X0,X1,X2] : product(X0,quotient(product(X1,X2),X0)) = product(difference(X2,X0),X1),
inference(forward_demodulation,[status(thm)],[f636,f11165]) ).
fof(f11838,plain,
! [X0,X1,X2] : difference(product(X0,X1),product(X2,product(X0,X1))) = product(difference(X1,X2),X0),
inference(paramodulation,[status(thm)],[f515,f2941]) ).
fof(f11902,plain,
! [X0,X1,X2] : product(difference(product(X0,X1),X2),product(X0,X1)) = product(difference(X1,X2),X0),
inference(forward_demodulation,[status(thm)],[f621,f11838]) ).
fof(f14826,plain,
product(difference(product(a,b),product(a,c)),difference(product(a,b),product(c,b))) = product(a,b),
inference(paramodulation,[status(thm)],[f307,f3721]) ).
fof(f14877,plain,
product(c,quotient(product(difference(product(a,b),product(c,b)),product(a,b)),a)) = product(a,b),
inference(forward_demodulation,[status(thm)],[f11213,f14826]) ).
fof(f14878,plain,
product(c,quotient(product(difference(b,product(c,b)),a),a)) = product(a,b),
inference(forward_demodulation,[status(thm)],[f11902,f14877]) ).
fof(f14879,plain,
product(c,difference(b,product(c,b))) = product(a,b),
inference(forward_demodulation,[status(thm)],[f13,f14878]) ).
fof(f14880,plain,
product(c,product(difference(b,c),b)) = product(a,b),
inference(forward_demodulation,[status(thm)],[f621,f14879]) ).
fof(f14881,plain,
product(difference(b,c),c) = product(a,b),
inference(forward_demodulation,[status(thm)],[f6854,f14880]) ).
fof(f33881,plain,
! [X0] : product(c,product(X0,c)) = product(product(b,X0),product(a,b)),
inference(paramodulation,[status(thm)],[f14881,f353]) ).
fof(f34185,plain,
! [X0] : bigC(X0,c,c) = product(product(b,X0),product(a,b)),
inference(forward_demodulation,[status(thm)],[f6769,f33881]) ).
fof(f34186,plain,
sF0_fnc = bigC(x0,c,c),
inference(backward_demodulation,[status(thm)],[f34189,f6485]) ).
fof(f34189,plain,
! [X0] : bigC(X0,c,c) = bigC(X0,b,a),
inference(forward_demodulation,[status(thm)],[f6417,f34185]) ).
fof(f34191,plain,
sF0_fnc = sF1_fnc,
inference(forward_demodulation,[status(thm)],[f5113,f34186]) ).
fof(f34192,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f34191,f23]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP777-10 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n007.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sun Sep 20 20:37:35 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 % Drodi V4.1.1
% 260.09/33.39 % Refutation found
% 260.09/33.39 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 260.09/33.39 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 21.44/34.59 % Elapsed time: 34.230293 seconds
% 246.21/34.81 % CPU time: 249.963617 seconds
% 246.21/34.81 % Total memory used: 1.007 GB
% 246.21/34.81 % Net memory used: 970.576 MB
%------------------------------------------------------------------------------