%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU444+2 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n019.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:38 PM UTC 2026
% Result : Theorem 0.87s 1.23s
% Output : CNFRefutation 0.87s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 4
% Syntax : Number of formulae : 23 ( 6 unt; 2 def)
% Number of atoms : 46 ( 23 equ)
% Maximal formula atoms : 3 ( 2 avg)
% Number of connectives : 38 ( 15 ~; 12 |; 6 &)
% ( 2 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 3 prp; 0-3 aty)
% Number of functors : 7 ( 7 usr; 3 con; 0-4 aty)
% Number of variables : 21 ( 18 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f4523,axiom,
! [A,B,C] :
( m2_relset_1(C,B,A)
=> ( k2_funct_5(C) = k10_relset_1(B,A,C,B)
& k1_funct_5(C) = k10_relset_1(A,B,k6_relset_1(B,A,C),A) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4528,conjecture,
! [A,B,C] :
( m2_relset_1(C,B,A)
=> ( k10_relset_1(A,B,k6_relset_1(B,A,C),k10_relset_1(B,A,C,B)) = k10_relset_1(A,B,k6_relset_1(B,A,C),k2_funct_5(C))
& k1_funct_5(C) = k10_relset_1(A,B,k6_relset_1(B,A,C),A) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4529,negated_conjecture,
~ ! [A,B,C] :
( m2_relset_1(C,B,A)
=> ( k10_relset_1(A,B,k6_relset_1(B,A,C),k10_relset_1(B,A,C,B)) = k10_relset_1(A,B,k6_relset_1(B,A,C),k2_funct_5(C))
& k1_funct_5(C) = k10_relset_1(A,B,k6_relset_1(B,A,C),A) ) ),
inference(negated_conjecture,[status(cth)],[f4528]) ).
fof(f17711,plain,
! [A,B,C] :
( ( k2_funct_5(C) = k10_relset_1(B,A,C,B)
& k1_funct_5(C) = k10_relset_1(A,B,k6_relset_1(B,A,C),A) )
| ~ m2_relset_1(C,B,A) ),
inference(pre_NNF_transformation,[status(thm)],[f4523]) ).
fof(f17712,plain,
! [X0,X1,X2] :
( k1_funct_5(X0) = k10_relset_1(X2,X1,k6_relset_1(X1,X2,X0),X2)
| ~ m2_relset_1(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f17711]) ).
fof(f17713,plain,
! [X0,X1,X2] :
( k2_funct_5(X0) = k10_relset_1(X1,X2,X0,X1)
| ~ m2_relset_1(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f17711]) ).
fof(f17732,plain,
? [A,B,C] :
( ( k10_relset_1(A,B,k6_relset_1(B,A,C),k10_relset_1(B,A,C,B)) != k10_relset_1(A,B,k6_relset_1(B,A,C),k2_funct_5(C))
| k1_funct_5(C) != k10_relset_1(A,B,k6_relset_1(B,A,C),A) )
& m2_relset_1(C,B,A) ),
inference(pre_NNF_transformation,[status(thm)],[f4529]) ).
fof(f17733,plain,
( ( k10_relset_1(sK1211_skl,sK1212_skl,k6_relset_1(sK1212_skl,sK1211_skl,sK1213_skl),k10_relset_1(sK1212_skl,sK1211_skl,sK1213_skl,sK1212_skl)) != k10_relset_1(sK1211_skl,sK1212_skl,k6_relset_1(sK1212_skl,sK1211_skl,sK1213_skl),k2_funct_5(sK1213_skl))
| k1_funct_5(sK1213_skl) != k10_relset_1(sK1211_skl,sK1212_skl,k6_relset_1(sK1212_skl,sK1211_skl,sK1213_skl),sK1211_skl) )
& m2_relset_1(sK1213_skl,sK1212_skl,sK1211_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1211_skl,sK1212_skl,sK1213_skl]),skolemize(A,sK1211_skl),skolemize(B,sK1212_skl),skolemize(C,sK1213_skl)],[f17732]) ).
fof(f17734,plain,
m2_relset_1(sK1213_skl,sK1212_skl,sK1211_skl),
inference(cnf_transformation,[status(thm)],[f17733]) ).
fof(f17735,plain,
( k10_relset_1(sK1211_skl,sK1212_skl,k6_relset_1(sK1212_skl,sK1211_skl,sK1213_skl),k10_relset_1(sK1212_skl,sK1211_skl,sK1213_skl,sK1212_skl)) != k10_relset_1(sK1211_skl,sK1212_skl,k6_relset_1(sK1212_skl,sK1211_skl,sK1213_skl),k2_funct_5(sK1213_skl))
| k1_funct_5(sK1213_skl) != k10_relset_1(sK1211_skl,sK1212_skl,k6_relset_1(sK1212_skl,sK1211_skl,sK1213_skl),sK1211_skl) ),
inference(cnf_transformation,[status(thm)],[f17733]) ).
fof(f20564,definition,
( sQ419_spl
<=> k1_funct_5(sK1213_skl) = k10_relset_1(sK1211_skl,sK1212_skl,k6_relset_1(sK1212_skl,sK1211_skl,sK1213_skl),sK1211_skl) ),
introduced(definition,[new_symbols(definition,[sQ419_spl])],[split_symbol_definition]) ).
fof(f20566,plain,
( sQ419_spl
| k1_funct_5(sK1213_skl) != k10_relset_1(sK1211_skl,sK1212_skl,k6_relset_1(sK1212_skl,sK1211_skl,sK1213_skl),sK1211_skl) ),
inference(component_clause,[status(thm)],[f20564]) ).
fof(f20567,definition,
( sQ420_spl
<=> k10_relset_1(sK1211_skl,sK1212_skl,k6_relset_1(sK1212_skl,sK1211_skl,sK1213_skl),k10_relset_1(sK1212_skl,sK1211_skl,sK1213_skl,sK1212_skl)) = k10_relset_1(sK1211_skl,sK1212_skl,k6_relset_1(sK1212_skl,sK1211_skl,sK1213_skl),k2_funct_5(sK1213_skl)) ),
introduced(definition,[new_symbols(definition,[sQ420_spl])],[split_symbol_definition]) ).
fof(f20569,plain,
( sQ420_spl
| k10_relset_1(sK1211_skl,sK1212_skl,k6_relset_1(sK1212_skl,sK1211_skl,sK1213_skl),k10_relset_1(sK1212_skl,sK1211_skl,sK1213_skl,sK1212_skl)) != k10_relset_1(sK1211_skl,sK1212_skl,k6_relset_1(sK1212_skl,sK1211_skl,sK1213_skl),k2_funct_5(sK1213_skl)) ),
inference(component_clause,[status(thm)],[f20567]) ).
fof(f20570,plain,
( ~ sQ420_spl
| ~ sQ419_spl ),
inference(split_clause,[status(thm)],[f17735,f20564,f20567]) ).
fof(f22792,plain,
k1_funct_5(sK1213_skl) = k10_relset_1(sK1211_skl,sK1212_skl,k6_relset_1(sK1212_skl,sK1211_skl,sK1213_skl),sK1211_skl),
inference(resolution,[status(thm)],[f17712,f17734]) ).
fof(f22794,plain,
( sQ419_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f22792,f20566]) ).
fof(f22795,plain,
sQ419_spl,
inference(contradiction_clause,[status(thm)],[f22794]) ).
fof(f22797,plain,
k2_funct_5(sK1213_skl) = k10_relset_1(sK1212_skl,sK1211_skl,sK1213_skl,sK1212_skl),
inference(resolution,[status(thm)],[f17713,f17734]) ).
fof(f22861,plain,
( sQ420_spl
| k10_relset_1(sK1211_skl,sK1212_skl,k6_relset_1(sK1212_skl,sK1211_skl,sK1213_skl),k2_funct_5(sK1213_skl)) != k10_relset_1(sK1211_skl,sK1212_skl,k6_relset_1(sK1212_skl,sK1211_skl,sK1213_skl),k2_funct_5(sK1213_skl)) ),
inference(forward_demodulation,[status(thm)],[f22797,f20569]) ).
fof(f22862,plain,
( sQ420_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f22861]) ).
fof(f22863,plain,
sQ420_spl,
inference(contradiction_clause,[status(thm)],[f22862]) ).
fof(f22864,plain,
$false,
inference(sat_refutation,[status(thm)],[f20570,f22795,f22863]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEU444+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.43 % Computer : n019.cluster.edu
% 0.17/0.43 % Model : x86_64 x86_64
% 0.17/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.43 % Memory : 8046.5625MB
% 0.17/0.43 % 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 06:33:36 UTC 2026
% 0.17/0.44 % CPUTime :
% 0.81/1.07 % Drodi V4.1.1
% 0.87/1.23 % Refutation found
% 0.87/1.23 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.87/1.23 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.90/1.53 % Elapsed time: 1.078562 seconds
% 0.90/1.53 % CPU time: 2.278161 seconds
% 0.90/1.53 % Total memory used: 737.527 MB
% 0.90/1.53 % Net memory used: 732.426 MB
%------------------------------------------------------------------------------