%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GRP775+1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n003.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 : Theorem 1.14s 0.60s
% Output : CNFRefutation 1.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 11
% Syntax : Number of formulae : 85 ( 9 unt; 5 def)
% Number of atoms : 239 ( 101 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 268 ( 114 ~; 119 |; 24 &)
% ( 10 <=>; 0 =>; 0 <=; 1 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 10 ( 8 usr; 6 prp; 0-2 aty)
% Number of functors : 4 ( 4 usr; 2 con; 0-2 aty)
% Number of variables : 90 ( 83 !; 7 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [C,B,A] : product(product(A,B),C) = product(A,product(B,C)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [A] : product(A,A) = A,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [X0,X1] :
( l(X0,X1)
<=> ( product(X1,X0) = X1
& product(X0,X1) = X0 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [X2,X3] :
( r(X2,X3)
<=> ( product(X3,X2) = X2
& product(X2,X3) = X3 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [X4,X5] :
( d(X4,X5)
<=> ? [X6] :
( l(X6,X5)
& r(X4,X6) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,conjecture,
! [X7,X8] :
( d(X7,X8)
<=> ( product(X8,product(X7,X8)) = X8
& product(X7,product(X8,X7)) = X7 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,negated_conjecture,
~ ! [X7,X8] :
( d(X7,X8)
<=> ( product(X8,product(X7,X8)) = X8
& product(X7,product(X8,X7)) = X7 ) ),
inference(negated_conjecture,[status(cth)],[f6]) ).
fof(f8,plain,
! [X0,X1,X2] : product(product(X0,X1),X2) = product(X0,product(X1,X2)),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f9,plain,
! [X0] : product(X0,X0) = X0,
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f10,plain,
! [X0,X1] :
( ( product(X1,X0) != X1
| product(X0,X1) != X0
| l(X0,X1) )
& ( ( product(X1,X0) = X1
& product(X0,X1) = X0 )
| ~ l(X0,X1) ) ),
inference(NNF_transformation,[status(thm)],[f3]) ).
fof(f11,plain,
( ! [X0,X1] :
( product(X1,X0) != X1
| product(X0,X1) != X0
| l(X0,X1) )
& ! [X0,X1] :
( ( product(X1,X0) = X1
& product(X0,X1) = X0 )
| ~ l(X0,X1) ) ),
inference(miniscoping,[status(thm)],[f10]) ).
fof(f12,plain,
! [X0,X1] :
( product(X0,X1) = X0
| ~ l(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f13,plain,
! [X0,X1] :
( product(X1,X0) = X1
| ~ l(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f14,plain,
! [X0,X1] :
( product(X1,X0) != X1
| product(X0,X1) != X0
| l(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f15,plain,
! [X2,X3] :
( ( product(X3,X2) != X2
| product(X2,X3) != X3
| r(X2,X3) )
& ( ( product(X3,X2) = X2
& product(X2,X3) = X3 )
| ~ r(X2,X3) ) ),
inference(NNF_transformation,[status(thm)],[f4]) ).
fof(f16,plain,
( ! [X2,X3] :
( product(X3,X2) != X2
| product(X2,X3) != X3
| r(X2,X3) )
& ! [X2,X3] :
( ( product(X3,X2) = X2
& product(X2,X3) = X3 )
| ~ r(X2,X3) ) ),
inference(miniscoping,[status(thm)],[f15]) ).
fof(f17,plain,
! [X0,X1] :
( product(X0,X1) = X1
| ~ r(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f18,plain,
! [X0,X1] :
( product(X1,X0) = X0
| ~ r(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f19,plain,
! [X0,X1] :
( product(X1,X0) != X0
| product(X0,X1) != X1
| r(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f20,plain,
! [X4,X5] :
( ( ! [X6] :
( ~ l(X6,X5)
| ~ r(X4,X6) )
| d(X4,X5) )
& ( ? [X6] :
( l(X6,X5)
& r(X4,X6) )
| ~ d(X4,X5) ) ),
inference(NNF_transformation,[status(thm)],[f5]) ).
fof(f21,plain,
( ! [X4,X5] :
( ! [X6] :
( ~ l(X6,X5)
| ~ r(X4,X6) )
| d(X4,X5) )
& ! [X4,X5] :
( ? [X6] :
( l(X6,X5)
& r(X4,X6) )
| ~ d(X4,X5) ) ),
inference(miniscoping,[status(thm)],[f20]) ).
fof(f22,plain,
( ! [X4,X5] :
( ! [X6] :
( ~ l(X6,X5)
| ~ r(X4,X6) )
| d(X4,X5) )
& ! [X4,X5] :
( ( l(sK0_skl(X5,X4),X5)
& r(X4,sK0_skl(X5,X4)) )
| ~ d(X4,X5) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(X6,sK0_skl(X5,X4))],[f21]) ).
fof(f23,plain,
! [X0,X1] :
( r(X0,sK0_skl(X1,X0))
| ~ d(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f22]) ).
fof(f24,plain,
! [X0,X1] :
( l(sK0_skl(X1,X0),X1)
| ~ d(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f22]) ).
fof(f25,plain,
! [X0,X1,X2] :
( ~ l(X2,X1)
| ~ r(X0,X2)
| d(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f22]) ).
fof(f26,plain,
? [X7,X8] :
( d(X7,X8)
<~> ( product(X8,product(X7,X8)) = X8
& product(X7,product(X8,X7)) = X7 ) ),
inference(pre_NNF_transformation,[status(thm)],[f7]) ).
fof(f27,plain,
? [X7,X8] :
( ( product(X8,product(X7,X8)) != X8
| product(X7,product(X8,X7)) != X7
| ~ d(X7,X8) )
& ( ( product(X8,product(X7,X8)) = X8
& product(X7,product(X8,X7)) = X7 )
| d(X7,X8) ) ),
inference(NNF_transformation,[status(thm)],[f26]) ).
fof(f28,plain,
( ( product(sK2_skl,product(sK1_skl,sK2_skl)) != sK2_skl
| product(sK1_skl,product(sK2_skl,sK1_skl)) != sK1_skl
| ~ d(sK1_skl,sK2_skl) )
& ( ( product(sK2_skl,product(sK1_skl,sK2_skl)) = sK2_skl
& product(sK1_skl,product(sK2_skl,sK1_skl)) = sK1_skl )
| d(sK1_skl,sK2_skl) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl,sK2_skl]),skolemize(X7,sK1_skl),skolemize(X8,sK2_skl)],[f27]) ).
fof(f29,plain,
( product(sK1_skl,product(sK2_skl,sK1_skl)) = sK1_skl
| d(sK1_skl,sK2_skl) ),
inference(cnf_transformation,[status(thm)],[f28]) ).
fof(f30,plain,
( product(sK2_skl,product(sK1_skl,sK2_skl)) = sK2_skl
| d(sK1_skl,sK2_skl) ),
inference(cnf_transformation,[status(thm)],[f28]) ).
fof(f31,plain,
( product(sK2_skl,product(sK1_skl,sK2_skl)) != sK2_skl
| product(sK1_skl,product(sK2_skl,sK1_skl)) != sK1_skl
| ~ d(sK1_skl,sK2_skl) ),
inference(cnf_transformation,[status(thm)],[f28]) ).
fof(f32,definition,
( sQ0_spl
<=> d(sK1_skl,sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f33,plain,
( ~ sQ0_spl
| d(sK1_skl,sK2_skl) ),
inference(component_clause,[status(thm)],[f32]) ).
fof(f34,plain,
( sQ0_spl
| ~ d(sK1_skl,sK2_skl) ),
inference(component_clause,[status(thm)],[f32]) ).
fof(f35,definition,
( sQ1_spl
<=> product(sK1_skl,product(sK2_skl,sK1_skl)) = sK1_skl ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f36,plain,
( ~ sQ1_spl
| product(sK1_skl,product(sK2_skl,sK1_skl)) = sK1_skl ),
inference(component_clause,[status(thm)],[f35]) ).
fof(f37,plain,
( sQ1_spl
| product(sK1_skl,product(sK2_skl,sK1_skl)) != sK1_skl ),
inference(component_clause,[status(thm)],[f35]) ).
fof(f38,plain,
( sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f29,f32,f35]) ).
fof(f39,definition,
( sQ2_spl
<=> product(sK2_skl,product(sK1_skl,sK2_skl)) = sK2_skl ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f41,plain,
( sQ2_spl
| product(sK2_skl,product(sK1_skl,sK2_skl)) != sK2_skl ),
inference(component_clause,[status(thm)],[f39]) ).
fof(f42,plain,
( sQ2_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f30,f32,f39]) ).
fof(f43,plain,
( ~ sQ2_spl
| ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f31,f32,f35,f39]) ).
fof(f47,plain,
! [X0,X1] : product(X0,product(X1,product(X0,X1))) = product(X0,X1),
inference(paramodulation,[status(thm)],[f8,f9]) ).
fof(f49,plain,
! [X0,X1] : product(X0,X1) = product(X0,product(X0,X1)),
inference(paramodulation,[status(thm)],[f9,f8]) ).
fof(f148,plain,
( ~ sQ0_spl
| r(sK1_skl,sK0_skl(sK2_skl,sK1_skl)) ),
inference(resolution,[status(thm)],[f23,f33]) ).
fof(f149,plain,
( ~ sQ0_spl
| l(sK0_skl(sK2_skl,sK1_skl),sK2_skl) ),
inference(resolution,[status(thm)],[f24,f33]) ).
fof(f150,plain,
! [X0,X1,X2] :
( product(X2,X0) != X0
| product(X0,X2) != X2
| ~ l(X2,X1)
| d(X0,X1) ),
inference(resolution,[status(thm)],[f25,f19]) ).
fof(f152,plain,
( ~ sQ0_spl
| product(sK0_skl(sK2_skl,sK1_skl),sK1_skl) = sK1_skl ),
inference(resolution,[status(thm)],[f148,f18]) ).
fof(f153,plain,
( ~ sQ0_spl
| product(sK1_skl,sK0_skl(sK2_skl,sK1_skl)) = sK0_skl(sK2_skl,sK1_skl) ),
inference(resolution,[status(thm)],[f148,f17]) ).
fof(f154,plain,
( ~ sQ0_spl
| product(sK2_skl,sK0_skl(sK2_skl,sK1_skl)) = sK2_skl ),
inference(resolution,[status(thm)],[f149,f13]) ).
fof(f155,plain,
( ~ sQ0_spl
| product(sK0_skl(sK2_skl,sK1_skl),sK2_skl) = sK0_skl(sK2_skl,sK1_skl) ),
inference(resolution,[status(thm)],[f149,f12]) ).
fof(f161,plain,
! [X0] :
( ~ sQ0_spl
| product(sK1_skl,X0) = product(sK0_skl(sK2_skl,sK1_skl),product(sK1_skl,X0)) ),
inference(paramodulation,[status(thm)],[f152,f8]) ).
fof(f290,plain,
! [X0] :
( ~ sQ0_spl
| product(sK0_skl(sK2_skl,sK1_skl),X0) = product(sK0_skl(sK2_skl,sK1_skl),product(sK2_skl,X0)) ),
inference(paramodulation,[status(thm)],[f155,f8]) ).
fof(f296,plain,
! [X0,X1,X2] :
( product(X1,X2) != X1
| product(X2,X1) != X2
| product(X2,X0) != X0
| product(X0,X2) != X2
| d(X0,X1) ),
inference(resolution,[status(thm)],[f150,f14]) ).
fof(f748,plain,
! [X0] :
( ~ sQ0_spl
| product(sK0_skl(sK2_skl,sK1_skl),product(X0,product(sK2_skl,X0))) = product(sK0_skl(sK2_skl,sK1_skl),product(sK2_skl,X0)) ),
inference(paramodulation,[status(thm)],[f47,f290]) ).
fof(f783,plain,
! [X0] :
( ~ sQ0_spl
| product(sK0_skl(sK2_skl,sK1_skl),product(X0,product(sK2_skl,X0))) = product(sK0_skl(sK2_skl,sK1_skl),X0) ),
inference(forward_demodulation,[status(thm)],[f290,f748]) ).
fof(f816,plain,
( ~ sQ0_spl
| product(sK1_skl,product(sK2_skl,sK1_skl)) = product(sK0_skl(sK2_skl,sK1_skl),sK1_skl) ),
inference(paramodulation,[status(thm)],[f161,f783]) ).
fof(f847,plain,
( ~ sQ0_spl
| product(sK1_skl,product(sK2_skl,sK1_skl)) = sK1_skl ),
inference(forward_demodulation,[status(thm)],[f152,f816]) ).
fof(f848,plain,
( ~ sQ0_spl
| sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f847,f37]) ).
fof(f849,plain,
( ~ sQ0_spl
| sQ1_spl ),
inference(contradiction_clause,[status(thm)],[f848]) ).
fof(f850,plain,
! [X0] :
( sQ0_spl
| product(sK2_skl,X0) != sK2_skl
| product(X0,sK2_skl) != X0
| product(X0,sK1_skl) != sK1_skl
| product(sK1_skl,X0) != X0 ),
inference(resolution,[status(thm)],[f34,f296]) ).
fof(f860,plain,
! [X0] :
( ~ sQ1_spl
| product(sK1_skl,X0) = product(sK1_skl,product(product(sK2_skl,sK1_skl),X0)) ),
inference(paramodulation,[status(thm)],[f36,f8]) ).
fof(f868,plain,
! [X0] :
( ~ sQ1_spl
| product(sK1_skl,X0) = product(sK1_skl,product(sK2_skl,product(sK1_skl,X0))) ),
inference(forward_demodulation,[status(thm)],[f8,f860]) ).
fof(f1321,plain,
! [X0,X1] :
( sQ0_spl
| product(sK2_skl,product(X0,X1)) != sK2_skl
| product(product(X0,X1),sK2_skl) != product(X0,X1)
| product(X0,product(X1,sK1_skl)) != sK1_skl
| product(sK1_skl,product(X0,X1)) != product(X0,X1) ),
inference(paramodulation,[status(thm)],[f8,f850]) ).
fof(f1333,plain,
! [X0,X1] :
( sQ0_spl
| product(sK2_skl,product(X0,X1)) != sK2_skl
| product(X0,product(X1,sK2_skl)) != product(X0,X1)
| product(X0,product(X1,sK1_skl)) != sK1_skl
| product(sK1_skl,product(X0,X1)) != product(X0,X1) ),
inference(forward_demodulation,[status(thm)],[f8,f1321]) ).
fof(f1411,plain,
( ~ sQ0_spl
| ~ sQ1_spl
| product(sK1_skl,sK0_skl(sK2_skl,sK1_skl)) = product(sK1_skl,product(sK2_skl,sK0_skl(sK2_skl,sK1_skl))) ),
inference(paramodulation,[status(thm)],[f153,f868]) ).
fof(f1419,plain,
( ~ sQ0_spl
| ~ sQ1_spl
| sK0_skl(sK2_skl,sK1_skl) = product(sK1_skl,product(sK2_skl,sK0_skl(sK2_skl,sK1_skl))) ),
inference(forward_demodulation,[status(thm)],[f153,f1411]) ).
fof(f1420,plain,
( ~ sQ0_spl
| ~ sQ1_spl
| sK0_skl(sK2_skl,sK1_skl) = product(sK1_skl,sK2_skl) ),
inference(forward_demodulation,[status(thm)],[f154,f1419]) ).
fof(f1440,plain,
( sQ2_spl
| ~ sQ0_spl
| ~ sQ1_spl
| product(sK2_skl,sK0_skl(sK2_skl,sK1_skl)) != sK2_skl ),
inference(backward_demodulation,[status(thm)],[f1420,f41]) ).
fof(f1449,plain,
( sQ2_spl
| ~ sQ0_spl
| ~ sQ1_spl
| sK2_skl != sK2_skl ),
inference(forward_demodulation,[status(thm)],[f154,f1440]) ).
fof(f1450,plain,
( sQ2_spl
| ~ sQ0_spl
| ~ sQ1_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f1449]) ).
fof(f1451,plain,
( sQ2_spl
| ~ sQ0_spl
| ~ sQ1_spl ),
inference(contradiction_clause,[status(thm)],[f1450]) ).
fof(f3473,plain,
( ~ sQ1_spl
| sQ0_spl
| product(sK2_skl,product(sK1_skl,sK2_skl)) != sK2_skl
| product(sK1_skl,product(sK2_skl,sK2_skl)) != product(sK1_skl,sK2_skl)
| product(sK1_skl,product(sK1_skl,sK2_skl)) != product(sK1_skl,sK2_skl) ),
inference(resolution,[status(thm)],[f1333,f36]) ).
fof(f3480,definition,
( sQ7_spl
<=> product(sK1_skl,product(sK1_skl,sK2_skl)) = product(sK1_skl,sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f3482,plain,
( sQ7_spl
| product(sK1_skl,product(sK1_skl,sK2_skl)) != product(sK1_skl,sK2_skl) ),
inference(component_clause,[status(thm)],[f3480]) ).
fof(f3483,definition,
( sQ8_spl
<=> product(sK1_skl,product(sK2_skl,sK2_skl)) = product(sK1_skl,sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f3485,plain,
( sQ8_spl
| product(sK1_skl,product(sK2_skl,sK2_skl)) != product(sK1_skl,sK2_skl) ),
inference(component_clause,[status(thm)],[f3483]) ).
fof(f3486,plain,
( ~ sQ1_spl
| sQ0_spl
| ~ sQ2_spl
| ~ sQ8_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f3473,f3480,f3483,f39,f32,f35]) ).
fof(f3505,plain,
( sQ7_spl
| product(sK1_skl,sK2_skl) != product(sK1_skl,sK2_skl) ),
inference(forward_demodulation,[status(thm)],[f49,f3482]) ).
fof(f3506,plain,
( sQ7_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f3505]) ).
fof(f3507,plain,
sQ7_spl,
inference(contradiction_clause,[status(thm)],[f3506]) ).
fof(f3508,plain,
( sQ8_spl
| product(sK1_skl,sK2_skl) != product(sK1_skl,sK2_skl) ),
inference(forward_demodulation,[status(thm)],[f9,f3485]) ).
fof(f3509,plain,
( sQ8_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f3508]) ).
fof(f3510,plain,
sQ8_spl,
inference(contradiction_clause,[status(thm)],[f3509]) ).
fof(f3511,plain,
$false,
inference(sat_refutation,[status(thm)],[f38,f42,f43,f849,f1451,f3486,f3507,f3510]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP775+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.36 % Computer : n003.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Sun Sep 20 20:41:31 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.38 % Drodi V4.1.1
% 1.14/0.60 % Refutation found
% 1.14/0.60 % SZS status Theorem for theBenchmark: Theorem is valid
% 1.14/0.60 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 1.14/0.63 % Elapsed time: 0.244351 seconds
% 1.14/0.63 % CPU time: 1.637789 seconds
% 1.14/0.63 % Total memory used: 135.095 MB
% 1.14/0.63 % Net memory used: 133.904 MB
%------------------------------------------------------------------------------