%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : ALG227+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 : n014.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 11:49:03 AM UTC 2026
% Result : Theorem 229.36s 29.76s
% Output : CNFRefutation 230.07s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 8
% Syntax : Number of formulae : 46 ( 8 unt; 5 def)
% Number of atoms : 159 ( 48 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 182 ( 69 ~; 69 |; 24 &)
% ( 9 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 11 ( 9 usr; 6 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 4 con; 0-3 aty)
% Number of variables : 61 ( 54 !; 7 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f4703,axiom,
! [A,B,C] :
( ( m1_pboole(C,B)
& ~ v1_xboole_0(B) )
=> ( r2_hidden(A,a_2_0_closure3(B,C))
<=> ? [D] :
( k1_funct_1(C,D) != k1_xboole_0
& A = D
& m1_subset_1(D,B) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4728,axiom,
! [A] :
( ~ v1_xboole_0(A)
=> ! [B] :
( m1_pboole(B,A)
=> ! [C] :
( C = k1_closure3(A,B)
<=> C = a_2_0_closure3(A,B) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4731,conjecture,
! [A] :
( ~ v1_xboole_0(A)
=> ! [B] :
( m1_pboole(B,A)
=> ! [C] :
( m1_subset_1(C,A)
=> ( ~ r2_hidden(C,k1_closure3(A,B))
=> k1_funct_1(B,C) = k1_xboole_0 ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4732,negated_conjecture,
~ ! [A] :
( ~ v1_xboole_0(A)
=> ! [B] :
( m1_pboole(B,A)
=> ! [C] :
( m1_subset_1(C,A)
=> ( ~ r2_hidden(C,k1_closure3(A,B))
=> k1_funct_1(B,C) = k1_xboole_0 ) ) ) ),
inference(negated_conjecture,[status(cth)],[f4731]) ).
fof(f19156,plain,
! [A,B,C] :
( ( r2_hidden(A,a_2_0_closure3(B,C))
<=> ? [D] :
( k1_funct_1(C,D) != k1_xboole_0
& A = D
& m1_subset_1(D,B) ) )
| ~ m1_pboole(C,B)
| v1_xboole_0(B) ),
inference(pre_NNF_transformation,[status(thm)],[f4703]) ).
fof(f19157,plain,
! [A,B,C] :
( ( ( ! [D] :
( k1_funct_1(C,D) = k1_xboole_0
| A != D
| ~ m1_subset_1(D,B) )
| r2_hidden(A,a_2_0_closure3(B,C)) )
& ( ? [D] :
( k1_funct_1(C,D) != k1_xboole_0
& A = D
& m1_subset_1(D,B) )
| ~ r2_hidden(A,a_2_0_closure3(B,C)) ) )
| ~ m1_pboole(C,B)
| v1_xboole_0(B) ),
inference(NNF_transformation,[status(thm)],[f19156]) ).
fof(f19158,plain,
! [B,C] :
( ( ! [A] :
( ! [D] :
( k1_funct_1(C,D) = k1_xboole_0
| A != D
| ~ m1_subset_1(D,B) )
| r2_hidden(A,a_2_0_closure3(B,C)) )
& ! [A] :
( ? [D] :
( k1_funct_1(C,D) != k1_xboole_0
& A = D
& m1_subset_1(D,B) )
| ~ r2_hidden(A,a_2_0_closure3(B,C)) ) )
| ~ m1_pboole(C,B)
| v1_xboole_0(B) ),
inference(miniscoping,[status(thm)],[f19157]) ).
fof(f19159,plain,
! [B,C] :
( ( ! [A] :
( ! [D] :
( k1_funct_1(C,D) = k1_xboole_0
| A != D
| ~ m1_subset_1(D,B) )
| r2_hidden(A,a_2_0_closure3(B,C)) )
& ! [A] :
( ( k1_funct_1(C,sK1307_skl(A,C,B)) != k1_xboole_0
& A = sK1307_skl(A,C,B)
& m1_subset_1(sK1307_skl(A,C,B),B) )
| ~ r2_hidden(A,a_2_0_closure3(B,C)) ) )
| ~ m1_pboole(C,B)
| v1_xboole_0(B) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1307_skl]),skolemize(D,sK1307_skl(A,C,B))],[f19158]) ).
fof(f19163,plain,
! [X0,X1,X2,X3] :
( k1_funct_1(X1,X3) = k1_xboole_0
| X2 != X3
| ~ m1_subset_1(X3,X0)
| r2_hidden(X2,a_2_0_closure3(X0,X1))
| ~ m1_pboole(X1,X0)
| v1_xboole_0(X0) ),
inference(cnf_transformation,[status(thm)],[f19159]) ).
fof(f19230,plain,
! [A] :
( ! [B] :
( ! [C] :
( C = k1_closure3(A,B)
<=> C = a_2_0_closure3(A,B) )
| ~ m1_pboole(B,A) )
| v1_xboole_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f4728]) ).
fof(f19231,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( C != a_2_0_closure3(A,B)
| C = k1_closure3(A,B) )
& ( C = a_2_0_closure3(A,B)
| C != k1_closure3(A,B) ) )
| ~ m1_pboole(B,A) )
| v1_xboole_0(A) ),
inference(NNF_transformation,[status(thm)],[f19230]) ).
fof(f19232,plain,
! [A] :
( ! [B] :
( ( ! [C] :
( C != a_2_0_closure3(A,B)
| C = k1_closure3(A,B) )
& ! [C] :
( C = a_2_0_closure3(A,B)
| C != k1_closure3(A,B) ) )
| ~ m1_pboole(B,A) )
| v1_xboole_0(A) ),
inference(miniscoping,[status(thm)],[f19231]) ).
fof(f19233,plain,
! [X0,X1,X2] :
( X2 = a_2_0_closure3(X0,X1)
| X2 != k1_closure3(X0,X1)
| ~ m1_pboole(X1,X0)
| v1_xboole_0(X0) ),
inference(cnf_transformation,[status(thm)],[f19232]) ).
fof(f19239,plain,
? [A] :
( ? [B] :
( ? [C] :
( k1_funct_1(B,C) != k1_xboole_0
& ~ r2_hidden(C,k1_closure3(A,B))
& m1_subset_1(C,A) )
& m1_pboole(B,A) )
& ~ v1_xboole_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f4732]) ).
fof(f19240,plain,
( k1_funct_1(sK1314_skl,sK1315_skl) != k1_xboole_0
& ~ r2_hidden(sK1315_skl,k1_closure3(sK1313_skl,sK1314_skl))
& m1_subset_1(sK1315_skl,sK1313_skl)
& m1_pboole(sK1314_skl,sK1313_skl)
& ~ v1_xboole_0(sK1313_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1313_skl,sK1314_skl,sK1315_skl]),skolemize(A,sK1313_skl),skolemize(B,sK1314_skl),skolemize(C,sK1315_skl)],[f19239]) ).
fof(f19241,plain,
~ v1_xboole_0(sK1313_skl),
inference(cnf_transformation,[status(thm)],[f19240]) ).
fof(f19242,plain,
m1_pboole(sK1314_skl,sK1313_skl),
inference(cnf_transformation,[status(thm)],[f19240]) ).
fof(f19243,plain,
m1_subset_1(sK1315_skl,sK1313_skl),
inference(cnf_transformation,[status(thm)],[f19240]) ).
fof(f19244,plain,
~ r2_hidden(sK1315_skl,k1_closure3(sK1313_skl,sK1314_skl)),
inference(cnf_transformation,[status(thm)],[f19240]) ).
fof(f19245,plain,
k1_funct_1(sK1314_skl,sK1315_skl) != k1_xboole_0,
inference(cnf_transformation,[status(thm)],[f19240]) ).
fof(f23677,plain,
! [X0,X1,X2] :
( k1_funct_1(X1,X2) = k1_xboole_0
| ~ m1_subset_1(X2,X0)
| r2_hidden(X2,a_2_0_closure3(X0,X1))
| ~ m1_pboole(X1,X0)
| v1_xboole_0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f19163]) ).
fof(f23678,plain,
! [X0,X1] :
( k1_closure3(X0,X1) = a_2_0_closure3(X0,X1)
| ~ m1_pboole(X1,X0)
| v1_xboole_0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f19233]) ).
fof(f23834,definition,
( sQ602_spl
<=> v1_xboole_0(sK1313_skl) ),
introduced(definition,[new_symbols(definition,[sQ602_spl])],[split_symbol_definition]) ).
fof(f23835,plain,
( ~ sQ602_spl
| v1_xboole_0(sK1313_skl) ),
inference(component_clause,[status(thm)],[f23834]) ).
fof(f23841,plain,
( ~ sQ602_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f23835,f19241]) ).
fof(f23842,plain,
~ sQ602_spl,
inference(contradiction_clause,[status(thm)],[f23841]) ).
fof(f23849,plain,
( k1_closure3(sK1313_skl,sK1314_skl) = a_2_0_closure3(sK1313_skl,sK1314_skl)
| v1_xboole_0(sK1313_skl) ),
inference(resolution,[status(thm)],[f23678,f19242]) ).
fof(f23850,definition,
( sQ604_spl
<=> k1_closure3(sK1313_skl,sK1314_skl) = a_2_0_closure3(sK1313_skl,sK1314_skl) ),
introduced(definition,[new_symbols(definition,[sQ604_spl])],[split_symbol_definition]) ).
fof(f23851,plain,
( ~ sQ604_spl
| k1_closure3(sK1313_skl,sK1314_skl) = a_2_0_closure3(sK1313_skl,sK1314_skl) ),
inference(component_clause,[status(thm)],[f23850]) ).
fof(f23853,plain,
( sQ604_spl
| sQ602_spl ),
inference(split_clause,[status(thm)],[f23849,f23834,f23850]) ).
fof(f24809,plain,
! [X0] :
( k1_funct_1(sK1314_skl,X0) = k1_xboole_0
| ~ m1_subset_1(X0,sK1313_skl)
| r2_hidden(X0,a_2_0_closure3(sK1313_skl,sK1314_skl))
| v1_xboole_0(sK1313_skl) ),
inference(resolution,[status(thm)],[f23677,f19242]) ).
fof(f24810,definition,
! [X0] :
( sQ693_spl
<=> ( k1_funct_1(sK1314_skl,X0) = k1_xboole_0
| ~ m1_subset_1(X0,sK1313_skl)
| r2_hidden(X0,a_2_0_closure3(sK1313_skl,sK1314_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ693_spl])],[split_symbol_definition]) ).
fof(f24811,plain,
! [X0] :
( ~ sQ693_spl
| k1_funct_1(sK1314_skl,X0) = k1_xboole_0
| ~ m1_subset_1(X0,sK1313_skl)
| r2_hidden(X0,a_2_0_closure3(sK1313_skl,sK1314_skl)) ),
inference(component_clause,[status(thm)],[f24810]) ).
fof(f24813,plain,
( sQ693_spl
| sQ602_spl ),
inference(split_clause,[status(thm)],[f24809,f23834,f24810]) ).
fof(f25103,plain,
( ~ sQ604_spl
| ~ r2_hidden(sK1315_skl,a_2_0_closure3(sK1313_skl,sK1314_skl)) ),
inference(backward_demodulation,[status(thm)],[f23851,f19244]) ).
fof(f25153,plain,
( ~ sQ693_spl
| k1_funct_1(sK1314_skl,sK1315_skl) = k1_xboole_0
| r2_hidden(sK1315_skl,a_2_0_closure3(sK1313_skl,sK1314_skl)) ),
inference(resolution,[status(thm)],[f24811,f19243]) ).
fof(f25171,definition,
( sQ714_spl
<=> r2_hidden(sK1315_skl,a_2_0_closure3(sK1313_skl,sK1314_skl)) ),
introduced(definition,[new_symbols(definition,[sQ714_spl])],[split_symbol_definition]) ).
fof(f25172,plain,
( ~ sQ714_spl
| r2_hidden(sK1315_skl,a_2_0_closure3(sK1313_skl,sK1314_skl)) ),
inference(component_clause,[status(thm)],[f25171]) ).
fof(f25174,definition,
( sQ715_spl
<=> k1_funct_1(sK1314_skl,sK1315_skl) = k1_xboole_0 ),
introduced(definition,[new_symbols(definition,[sQ715_spl])],[split_symbol_definition]) ).
fof(f25175,plain,
( ~ sQ715_spl
| k1_funct_1(sK1314_skl,sK1315_skl) = k1_xboole_0 ),
inference(component_clause,[status(thm)],[f25174]) ).
fof(f25177,plain,
( ~ sQ693_spl
| sQ715_spl
| sQ714_spl ),
inference(split_clause,[status(thm)],[f25153,f25171,f25174,f24810]) ).
fof(f25178,plain,
( ~ sQ714_spl
| ~ sQ604_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f25172,f25103]) ).
fof(f25179,plain,
( ~ sQ714_spl
| ~ sQ604_spl ),
inference(contradiction_clause,[status(thm)],[f25178]) ).
fof(f25180,plain,
( ~ sQ715_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f25175,f19245]) ).
fof(f25181,plain,
~ sQ715_spl,
inference(contradiction_clause,[status(thm)],[f25180]) ).
fof(f25182,plain,
$false,
inference(sat_refutation,[status(thm)],[f23842,f23853,f24813,f25177,f25179,f25181]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ALG227+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n014.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 : Mon Sep 21 13:06:51 UTC 2026
% 0.13/0.35 % CPUTime :
% 0.56/0.81 % Drodi V4.1.1
% 229.36/29.76 % Refutation found
% 229.36/29.76 % SZS status Theorem for theBenchmark: Theorem is valid
% 229.36/29.76 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 44.09/29.95 % Elapsed time: 29.580313 seconds
% 44.09/29.95 % CPU time: 230.269461 seconds
% 44.09/29.95 % Total memory used: 1.153 GB
% 44.09/29.95 % Net memory used: 1.073 GB
%------------------------------------------------------------------------------