%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU418+2 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n002.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 02:20:30 PM UTC 2026
% Result : Theorem 1.00s 1.93s
% Output : CNFRefutation 1.00s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 13
% Syntax : Number of formulae : 56 ( 16 unt; 7 def)
% Number of atoms : 130 ( 2 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 123 ( 49 ~; 47 |; 7 &)
% ( 7 <=>; 13 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 11 ( 9 usr; 8 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 3 con; 0-2 aty)
% Number of variables : 48 ( 45 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f57,axiom,
! [A,B] : k3_xboole_0(A,B) = k3_xboole_0(B,A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f86,axiom,
! [A,B] : r1_tarski(k3_xboole_0(A,B),A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f88,axiom,
! [A,B,C] :
( ( r1_tarski(A,C)
& r1_tarski(A,B) )
=> r1_tarski(A,k3_xboole_0(B,C)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f563,axiom,
! [A,B] :
( v1_relat_1(B)
=> ( r1_tarski(A,B)
=> v1_relat_1(A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f616,axiom,
! [A] :
( v1_relat_1(A)
=> ! [B] :
( v1_relat_1(B)
=> ! [C] :
( v1_relat_1(C)
=> ( r1_tarski(A,B)
=> r1_tarski(k5_relat_1(A,C),k5_relat_1(B,C)) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4476,conjecture,
! [A] :
( v1_relat_1(A)
=> ! [B] :
( v1_relat_1(B)
=> ! [C] :
( v1_relat_1(C)
=> r1_tarski(k5_relat_1(k3_xboole_0(A,B),C),k3_xboole_0(k5_relat_1(A,C),k5_relat_1(B,C))) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4477,negated_conjecture,
~ ! [A] :
( v1_relat_1(A)
=> ! [B] :
( v1_relat_1(B)
=> ! [C] :
( v1_relat_1(C)
=> r1_tarski(k5_relat_1(k3_xboole_0(A,B),C),k3_xboole_0(k5_relat_1(A,C),k5_relat_1(B,C))) ) ) ),
inference(negated_conjecture,[status(cth)],[f4476]) ).
fof(f4686,plain,
! [X0,X1] : k3_xboole_0(X0,X1) = k3_xboole_0(X1,X0),
inference(cnf_transformation,[status(thm)],[f57]) ).
fof(f4737,plain,
! [X0,X1] : r1_tarski(k3_xboole_0(X0,X1),X0),
inference(cnf_transformation,[status(thm)],[f86]) ).
fof(f4741,plain,
! [A,B,C] :
( r1_tarski(A,k3_xboole_0(B,C))
| ~ r1_tarski(A,C)
| ~ r1_tarski(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f88]) ).
fof(f4742,plain,
! [X0,X1,X2] :
( r1_tarski(X0,k3_xboole_0(X1,X2))
| ~ r1_tarski(X0,X2)
| ~ r1_tarski(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f4741]) ).
fof(f5870,plain,
! [A,B] :
( v1_relat_1(A)
| ~ r1_tarski(A,B)
| ~ v1_relat_1(B) ),
inference(pre_NNF_transformation,[status(thm)],[f563]) ).
fof(f5871,plain,
! [B] :
( ! [A] :
( v1_relat_1(A)
| ~ r1_tarski(A,B) )
| ~ v1_relat_1(B) ),
inference(miniscoping,[status(thm)],[f5870]) ).
fof(f5872,plain,
! [X0,X1] :
( v1_relat_1(X1)
| ~ r1_tarski(X1,X0)
| ~ v1_relat_1(X0) ),
inference(cnf_transformation,[status(thm)],[f5871]) ).
fof(f6008,plain,
! [A] :
( ! [B] :
( ! [C] :
( r1_tarski(k5_relat_1(A,C),k5_relat_1(B,C))
| ~ r1_tarski(A,B)
| ~ v1_relat_1(C) )
| ~ v1_relat_1(B) )
| ~ v1_relat_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f616]) ).
fof(f6009,plain,
! [X0,X1,X2] :
( r1_tarski(k5_relat_1(X0,X2),k5_relat_1(X1,X2))
| ~ r1_tarski(X0,X1)
| ~ v1_relat_1(X2)
| ~ v1_relat_1(X1)
| ~ v1_relat_1(X0) ),
inference(cnf_transformation,[status(thm)],[f6008]) ).
fof(f17494,plain,
? [A] :
( ? [B] :
( ? [C] :
( ~ r1_tarski(k5_relat_1(k3_xboole_0(A,B),C),k3_xboole_0(k5_relat_1(A,C),k5_relat_1(B,C)))
& v1_relat_1(C) )
& v1_relat_1(B) )
& v1_relat_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f4477]) ).
fof(f17495,plain,
( ~ r1_tarski(k5_relat_1(k3_xboole_0(sK1204_skl,sK1205_skl),sK1206_skl),k3_xboole_0(k5_relat_1(sK1204_skl,sK1206_skl),k5_relat_1(sK1205_skl,sK1206_skl)))
& v1_relat_1(sK1206_skl)
& v1_relat_1(sK1205_skl)
& v1_relat_1(sK1204_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1204_skl,sK1205_skl,sK1206_skl]),skolemize(A,sK1204_skl),skolemize(B,sK1205_skl),skolemize(C,sK1206_skl)],[f17494]) ).
fof(f17496,plain,
v1_relat_1(sK1204_skl),
inference(cnf_transformation,[status(thm)],[f17495]) ).
fof(f17497,plain,
v1_relat_1(sK1205_skl),
inference(cnf_transformation,[status(thm)],[f17495]) ).
fof(f17498,plain,
v1_relat_1(sK1206_skl),
inference(cnf_transformation,[status(thm)],[f17495]) ).
fof(f17499,plain,
~ r1_tarski(k5_relat_1(k3_xboole_0(sK1204_skl,sK1205_skl),sK1206_skl),k3_xboole_0(k5_relat_1(sK1204_skl,sK1206_skl),k5_relat_1(sK1205_skl,sK1206_skl))),
inference(cnf_transformation,[status(thm)],[f17495]) ).
fof(f21993,plain,
~ r1_tarski(k5_relat_1(k3_xboole_0(sK1204_skl,sK1205_skl),sK1206_skl),k3_xboole_0(k5_relat_1(sK1205_skl,sK1206_skl),k5_relat_1(sK1204_skl,sK1206_skl))),
inference(paramodulation,[status(thm)],[f4686,f17499]) ).
fof(f21996,plain,
! [X0,X1] : r1_tarski(k3_xboole_0(X0,X1),X1),
inference(paramodulation,[status(thm)],[f4686,f4737]) ).
fof(f22191,plain,
( ~ r1_tarski(k5_relat_1(k3_xboole_0(sK1204_skl,sK1205_skl),sK1206_skl),k5_relat_1(sK1204_skl,sK1206_skl))
| ~ r1_tarski(k5_relat_1(k3_xboole_0(sK1204_skl,sK1205_skl),sK1206_skl),k5_relat_1(sK1205_skl,sK1206_skl)) ),
inference(resolution,[status(thm)],[f4742,f21993]) ).
fof(f22211,definition,
( sQ584_spl
<=> r1_tarski(k5_relat_1(k3_xboole_0(sK1204_skl,sK1205_skl),sK1206_skl),k5_relat_1(sK1205_skl,sK1206_skl)) ),
introduced(definition,[new_symbols(definition,[sQ584_spl])],[split_symbol_definition]) ).
fof(f22213,plain,
( sQ584_spl
| ~ r1_tarski(k5_relat_1(k3_xboole_0(sK1204_skl,sK1205_skl),sK1206_skl),k5_relat_1(sK1205_skl,sK1206_skl)) ),
inference(component_clause,[status(thm)],[f22211]) ).
fof(f22214,definition,
( sQ585_spl
<=> r1_tarski(k5_relat_1(k3_xboole_0(sK1204_skl,sK1205_skl),sK1206_skl),k5_relat_1(sK1204_skl,sK1206_skl)) ),
introduced(definition,[new_symbols(definition,[sQ585_spl])],[split_symbol_definition]) ).
fof(f22216,plain,
( sQ585_spl
| ~ r1_tarski(k5_relat_1(k3_xboole_0(sK1204_skl,sK1205_skl),sK1206_skl),k5_relat_1(sK1204_skl,sK1206_skl)) ),
inference(component_clause,[status(thm)],[f22214]) ).
fof(f22217,plain,
( ~ sQ585_spl
| ~ sQ584_spl ),
inference(split_clause,[status(thm)],[f22191,f22211,f22214]) ).
fof(f24682,plain,
! [X0,X1,X2] :
( r1_tarski(k5_relat_1(X2,X1),k5_relat_1(X0,X1))
| ~ r1_tarski(X2,X0)
| ~ v1_relat_1(X1)
| ~ v1_relat_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f6009,f5872]) ).
fof(f24685,plain,
( sQ585_spl
| ~ r1_tarski(k3_xboole_0(sK1204_skl,sK1205_skl),sK1204_skl)
| ~ v1_relat_1(sK1206_skl)
| ~ v1_relat_1(sK1204_skl) ),
inference(resolution,[status(thm)],[f24682,f22216]) ).
fof(f24686,plain,
( sQ584_spl
| ~ r1_tarski(k3_xboole_0(sK1204_skl,sK1205_skl),sK1205_skl)
| ~ v1_relat_1(sK1206_skl)
| ~ v1_relat_1(sK1205_skl) ),
inference(resolution,[status(thm)],[f24682,f22213]) ).
fof(f24690,definition,
( sQ619_spl
<=> v1_relat_1(sK1204_skl) ),
introduced(definition,[new_symbols(definition,[sQ619_spl])],[split_symbol_definition]) ).
fof(f24692,plain,
( sQ619_spl
| ~ v1_relat_1(sK1204_skl) ),
inference(component_clause,[status(thm)],[f24690]) ).
fof(f24693,definition,
( sQ620_spl
<=> v1_relat_1(sK1206_skl) ),
introduced(definition,[new_symbols(definition,[sQ620_spl])],[split_symbol_definition]) ).
fof(f24695,plain,
( sQ620_spl
| ~ v1_relat_1(sK1206_skl) ),
inference(component_clause,[status(thm)],[f24693]) ).
fof(f24700,definition,
( sQ622_spl
<=> v1_relat_1(sK1205_skl) ),
introduced(definition,[new_symbols(definition,[sQ622_spl])],[split_symbol_definition]) ).
fof(f24702,plain,
( sQ622_spl
| ~ v1_relat_1(sK1205_skl) ),
inference(component_clause,[status(thm)],[f24700]) ).
fof(f24707,definition,
( sQ624_spl
<=> r1_tarski(k3_xboole_0(sK1204_skl,sK1205_skl),sK1204_skl) ),
introduced(definition,[new_symbols(definition,[sQ624_spl])],[split_symbol_definition]) ).
fof(f24709,plain,
( sQ624_spl
| ~ r1_tarski(k3_xboole_0(sK1204_skl,sK1205_skl),sK1204_skl) ),
inference(component_clause,[status(thm)],[f24707]) ).
fof(f24710,plain,
( sQ585_spl
| ~ sQ624_spl
| ~ sQ620_spl
| ~ sQ619_spl ),
inference(split_clause,[status(thm)],[f24685,f24690,f24693,f24707,f22214]) ).
fof(f24711,definition,
( sQ625_spl
<=> r1_tarski(k3_xboole_0(sK1204_skl,sK1205_skl),sK1205_skl) ),
introduced(definition,[new_symbols(definition,[sQ625_spl])],[split_symbol_definition]) ).
fof(f24713,plain,
( sQ625_spl
| ~ r1_tarski(k3_xboole_0(sK1204_skl,sK1205_skl),sK1205_skl) ),
inference(component_clause,[status(thm)],[f24711]) ).
fof(f24714,plain,
( sQ584_spl
| ~ sQ625_spl
| ~ sQ620_spl
| ~ sQ622_spl ),
inference(split_clause,[status(thm)],[f24686,f24700,f24693,f24711,f22211]) ).
fof(f24716,plain,
( sQ620_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f24695,f17498]) ).
fof(f24717,plain,
sQ620_spl,
inference(contradiction_clause,[status(thm)],[f24716]) ).
fof(f24718,plain,
( sQ622_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f24702,f17497]) ).
fof(f24719,plain,
sQ622_spl,
inference(contradiction_clause,[status(thm)],[f24718]) ).
fof(f24720,plain,
( sQ619_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f24692,f17496]) ).
fof(f24721,plain,
sQ619_spl,
inference(contradiction_clause,[status(thm)],[f24720]) ).
fof(f24722,plain,
( sQ625_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f24713,f21996]) ).
fof(f24723,plain,
sQ625_spl,
inference(contradiction_clause,[status(thm)],[f24722]) ).
fof(f24724,plain,
( sQ624_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f24709,f4737]) ).
fof(f24725,plain,
sQ624_spl,
inference(contradiction_clause,[status(thm)],[f24724]) ).
fof(f24726,plain,
$false,
inference(sat_refutation,[status(thm)],[f22217,f24710,f24714,f24717,f24719,f24721,f24723,f24725]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SEU418+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.42 % Computer : n002.cluster.edu
% 0.17/0.42 % Model : x86_64 x86_64
% 0.17/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.42 % Memory : 8046.5625MB
% 0.17/0.42 % OS : Linux 6.8.0-71-generic
% 0.17/0.42 % CPULimit : 300
% 0.17/0.42 % WCLimit : 300
% 0.17/0.42 % DateTime : Mon Sep 21 06:27:17 UTC 2026
% 0.17/0.43 % CPUTime :
% 0.66/1.04 % Drodi V4.1.1
% 1.00/1.93 % Refutation found
% 1.00/1.93 % SZS status Theorem for theBenchmark: Theorem is valid
% 1.00/1.93 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 1.00/2.06 % Elapsed time: 1.606585 seconds
% 1.00/2.06 % CPU time: 7.802074 seconds
% 1.00/2.06 % Total memory used: 767.268 MB
% 1.00/2.06 % Net memory used: 754.738 MB
%------------------------------------------------------------------------------