%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU411+3 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n013.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:28 PM UTC 2026
% Result : Theorem 20.41s 7.24s
% Output : CNFRefutation 21.37s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 10
% Syntax : Number of formulae : 53 ( 16 unt; 7 def)
% Number of atoms : 225 ( 8 equ)
% Maximal formula atoms : 19 ( 4 avg)
% Number of connectives : 248 ( 76 ~; 68 |; 87 &)
% ( 9 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 22 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 21 ( 19 usr; 8 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 2 con; 0-3 aty)
% Number of variables : 45 ( 41 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f31,axiom,
! [A,B,C] :
( C = k3_xboole_0(A,B)
<=> ! [D] :
( r2_hidden(D,C)
<=> ( r2_hidden(D,B)
& r2_hidden(D,A) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f16772,axiom,
! [A] :
( ( l1_orders_2(A)
& v1_yellow_0(A)
& v4_orders_2(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
& v12_waybel_0(B,A)
& ~ v1_xboole_0(B) )
=> r2_hidden(k3_yellow_0(A),B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19046,conjecture,
! [A] :
( ( l1_orders_2(A)
& v1_lattice3(A)
& v1_yellow_0(A)
& v4_orders_2(A)
& v3_orders_2(A)
& v2_orders_2(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( l1_orders_2(B)
& v1_lattice3(B)
& v1_yellow_0(B)
& v4_orders_2(B)
& v3_orders_2(B)
& v2_orders_2(B)
& ~ v3_struct_0(B) )
=> ( ( m1_subset_1(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)),k1_zfmisc_1(u1_struct_0(B)))
& v12_waybel_0(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)),B)
& v1_waybel_0(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)),B)
& ~ v1_xboole_0(k3_xboole_0(u1_struct_0(A),u1_struct_0(B))) )
=> r2_hidden(k3_yellow_0(B),u1_struct_0(A)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19047,negated_conjecture,
~ ! [A] :
( ( l1_orders_2(A)
& v1_lattice3(A)
& v1_yellow_0(A)
& v4_orders_2(A)
& v3_orders_2(A)
& v2_orders_2(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( l1_orders_2(B)
& v1_lattice3(B)
& v1_yellow_0(B)
& v4_orders_2(B)
& v3_orders_2(B)
& v2_orders_2(B)
& ~ v3_struct_0(B) )
=> ( ( m1_subset_1(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)),k1_zfmisc_1(u1_struct_0(B)))
& v12_waybel_0(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)),B)
& v1_waybel_0(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)),B)
& ~ v1_xboole_0(k3_xboole_0(u1_struct_0(A),u1_struct_0(B))) )
=> r2_hidden(k3_yellow_0(B),u1_struct_0(A)) ) ) ),
inference(negated_conjecture,[status(cth)],[f19046]) ).
fof(f19151,plain,
! [A,B,C] :
( ( ? [D] :
( ( ( r2_hidden(D,B)
& r2_hidden(D,A) )
| r2_hidden(D,C) )
& ( ~ r2_hidden(D,B)
| ~ r2_hidden(D,A)
| ~ r2_hidden(D,C) ) )
| C = k3_xboole_0(A,B) )
& ( ! [D] :
( ( ~ r2_hidden(D,B)
| ~ r2_hidden(D,A)
| r2_hidden(D,C) )
& ( ( r2_hidden(D,B)
& r2_hidden(D,A) )
| ~ r2_hidden(D,C) ) )
| C != k3_xboole_0(A,B) ) ),
inference(NNF_transformation,[status(thm)],[f31]) ).
fof(f19152,plain,
( ! [A,B,C] :
( ? [D] :
( ( ( r2_hidden(D,B)
& r2_hidden(D,A) )
| r2_hidden(D,C) )
& ( ~ r2_hidden(D,B)
| ~ r2_hidden(D,A)
| ~ r2_hidden(D,C) ) )
| C = k3_xboole_0(A,B) )
& ! [A,B,C] :
( ( ! [D] :
( ~ r2_hidden(D,B)
| ~ r2_hidden(D,A)
| r2_hidden(D,C) )
& ! [D] :
( ( r2_hidden(D,B)
& r2_hidden(D,A) )
| ~ r2_hidden(D,C) ) )
| C != k3_xboole_0(A,B) ) ),
inference(miniscoping,[status(thm)],[f19151]) ).
fof(f19153,plain,
( ! [A,B,C] :
( ( ( ( r2_hidden(sK24_skl(C,B,A),B)
& r2_hidden(sK24_skl(C,B,A),A) )
| r2_hidden(sK24_skl(C,B,A),C) )
& ( ~ r2_hidden(sK24_skl(C,B,A),B)
| ~ r2_hidden(sK24_skl(C,B,A),A)
| ~ r2_hidden(sK24_skl(C,B,A),C) ) )
| C = k3_xboole_0(A,B) )
& ! [A,B,C] :
( ( ! [D] :
( ~ r2_hidden(D,B)
| ~ r2_hidden(D,A)
| r2_hidden(D,C) )
& ! [D] :
( ( r2_hidden(D,B)
& r2_hidden(D,A) )
| ~ r2_hidden(D,C) ) )
| C != k3_xboole_0(A,B) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK24_skl]),skolemize(D,sK24_skl(C,B,A))],[f19152]) ).
fof(f19154,plain,
! [X0,X1,X2,X3] :
( r2_hidden(X3,X1)
| ~ r2_hidden(X3,X0)
| X0 != k3_xboole_0(X1,X2) ),
inference(cnf_transformation,[status(thm)],[f19153]) ).
fof(f77335,plain,
! [A] :
( ! [B] :
( r2_hidden(k3_yellow_0(A),B)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ v12_waybel_0(B,A)
| v1_xboole_0(B) )
| ~ l1_orders_2(A)
| ~ v1_yellow_0(A)
| ~ v4_orders_2(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f16772]) ).
fof(f77336,plain,
! [X0,X1] :
( r2_hidden(k3_yellow_0(X0),X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v12_waybel_0(X1,X0)
| v1_xboole_0(X1)
| ~ l1_orders_2(X0)
| ~ v1_yellow_0(X0)
| ~ v4_orders_2(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f77335]) ).
fof(f89112,plain,
? [A] :
( ? [B] :
( ~ r2_hidden(k3_yellow_0(B),u1_struct_0(A))
& m1_subset_1(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)),k1_zfmisc_1(u1_struct_0(B)))
& v12_waybel_0(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)),B)
& v1_waybel_0(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)),B)
& ~ v1_xboole_0(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)))
& l1_orders_2(B)
& v1_lattice3(B)
& v1_yellow_0(B)
& v4_orders_2(B)
& v3_orders_2(B)
& v2_orders_2(B)
& ~ v3_struct_0(B) )
& l1_orders_2(A)
& v1_lattice3(A)
& v1_yellow_0(A)
& v4_orders_2(A)
& v3_orders_2(A)
& v2_orders_2(A)
& ~ v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f19047]) ).
fof(f89113,plain,
( ~ r2_hidden(k3_yellow_0(sK6521_skl),u1_struct_0(sK6520_skl))
& m1_subset_1(k3_xboole_0(u1_struct_0(sK6520_skl),u1_struct_0(sK6521_skl)),k1_zfmisc_1(u1_struct_0(sK6521_skl)))
& v12_waybel_0(k3_xboole_0(u1_struct_0(sK6520_skl),u1_struct_0(sK6521_skl)),sK6521_skl)
& v1_waybel_0(k3_xboole_0(u1_struct_0(sK6520_skl),u1_struct_0(sK6521_skl)),sK6521_skl)
& ~ v1_xboole_0(k3_xboole_0(u1_struct_0(sK6520_skl),u1_struct_0(sK6521_skl)))
& l1_orders_2(sK6521_skl)
& v1_lattice3(sK6521_skl)
& v1_yellow_0(sK6521_skl)
& v4_orders_2(sK6521_skl)
& v3_orders_2(sK6521_skl)
& v2_orders_2(sK6521_skl)
& ~ v3_struct_0(sK6521_skl)
& l1_orders_2(sK6520_skl)
& v1_lattice3(sK6520_skl)
& v1_yellow_0(sK6520_skl)
& v4_orders_2(sK6520_skl)
& v3_orders_2(sK6520_skl)
& v2_orders_2(sK6520_skl)
& ~ v3_struct_0(sK6520_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6520_skl,sK6521_skl]),skolemize(A,sK6520_skl),skolemize(B,sK6521_skl)],[f89112]) ).
fof(f89121,plain,
~ v3_struct_0(sK6521_skl),
inference(cnf_transformation,[status(thm)],[f89113]) ).
fof(f89124,plain,
v4_orders_2(sK6521_skl),
inference(cnf_transformation,[status(thm)],[f89113]) ).
fof(f89125,plain,
v1_yellow_0(sK6521_skl),
inference(cnf_transformation,[status(thm)],[f89113]) ).
fof(f89127,plain,
l1_orders_2(sK6521_skl),
inference(cnf_transformation,[status(thm)],[f89113]) ).
fof(f89128,plain,
~ v1_xboole_0(k3_xboole_0(u1_struct_0(sK6520_skl),u1_struct_0(sK6521_skl))),
inference(cnf_transformation,[status(thm)],[f89113]) ).
fof(f89130,plain,
v12_waybel_0(k3_xboole_0(u1_struct_0(sK6520_skl),u1_struct_0(sK6521_skl)),sK6521_skl),
inference(cnf_transformation,[status(thm)],[f89113]) ).
fof(f89131,plain,
m1_subset_1(k3_xboole_0(u1_struct_0(sK6520_skl),u1_struct_0(sK6521_skl)),k1_zfmisc_1(u1_struct_0(sK6521_skl))),
inference(cnf_transformation,[status(thm)],[f89113]) ).
fof(f89132,plain,
~ r2_hidden(k3_yellow_0(sK6521_skl),u1_struct_0(sK6520_skl)),
inference(cnf_transformation,[status(thm)],[f89113]) ).
fof(f105667,plain,
! [X0,X1,X2] :
( r2_hidden(X0,X1)
| ~ r2_hidden(X0,k3_xboole_0(X1,X2)) ),
inference(destructive_equality_resolution,[status(thm)],[f19154]) ).
fof(f111873,definition,
( sQ2483_spl
<=> v1_xboole_0(k3_xboole_0(u1_struct_0(sK6520_skl),u1_struct_0(sK6521_skl))) ),
introduced(definition,[new_symbols(definition,[sQ2483_spl])],[split_symbol_definition]) ).
fof(f111874,plain,
( ~ sQ2483_spl
| v1_xboole_0(k3_xboole_0(u1_struct_0(sK6520_skl),u1_struct_0(sK6521_skl))) ),
inference(component_clause,[status(thm)],[f111873]) ).
fof(f113808,definition,
( sQ2527_spl
<=> v3_struct_0(sK6521_skl) ),
introduced(definition,[new_symbols(definition,[sQ2527_spl])],[split_symbol_definition]) ).
fof(f113809,plain,
( ~ sQ2527_spl
| v3_struct_0(sK6521_skl) ),
inference(component_clause,[status(thm)],[f113808]) ).
fof(f113811,definition,
( sQ2528_spl
<=> v4_orders_2(sK6521_skl) ),
introduced(definition,[new_symbols(definition,[sQ2528_spl])],[split_symbol_definition]) ).
fof(f113813,plain,
( sQ2528_spl
| ~ v4_orders_2(sK6521_skl) ),
inference(component_clause,[status(thm)],[f113811]) ).
fof(f113814,definition,
( sQ2529_spl
<=> v1_yellow_0(sK6521_skl) ),
introduced(definition,[new_symbols(definition,[sQ2529_spl])],[split_symbol_definition]) ).
fof(f113816,plain,
( sQ2529_spl
| ~ v1_yellow_0(sK6521_skl) ),
inference(component_clause,[status(thm)],[f113814]) ).
fof(f113817,definition,
( sQ2530_spl
<=> l1_orders_2(sK6521_skl) ),
introduced(definition,[new_symbols(definition,[sQ2530_spl])],[split_symbol_definition]) ).
fof(f113819,plain,
( sQ2530_spl
| ~ l1_orders_2(sK6521_skl) ),
inference(component_clause,[status(thm)],[f113817]) ).
fof(f113835,plain,
( sQ2530_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f113819,f89127]) ).
fof(f113836,plain,
sQ2530_spl,
inference(contradiction_clause,[status(thm)],[f113835]) ).
fof(f113837,plain,
( sQ2529_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f113816,f89125]) ).
fof(f113838,plain,
sQ2529_spl,
inference(contradiction_clause,[status(thm)],[f113837]) ).
fof(f113839,plain,
( sQ2528_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f113813,f89124]) ).
fof(f113840,plain,
sQ2528_spl,
inference(contradiction_clause,[status(thm)],[f113839]) ).
fof(f113841,plain,
( ~ sQ2527_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f113809,f89121]) ).
fof(f113842,plain,
~ sQ2527_spl,
inference(contradiction_clause,[status(thm)],[f113841]) ).
fof(f113907,definition,
( sQ2547_spl
<=> v12_waybel_0(k3_xboole_0(u1_struct_0(sK6520_skl),u1_struct_0(sK6521_skl)),sK6521_skl) ),
introduced(definition,[new_symbols(definition,[sQ2547_spl])],[split_symbol_definition]) ).
fof(f113909,plain,
( sQ2547_spl
| ~ v12_waybel_0(k3_xboole_0(u1_struct_0(sK6520_skl),u1_struct_0(sK6521_skl)),sK6521_skl) ),
inference(component_clause,[status(thm)],[f113907]) ).
fof(f113914,plain,
( sQ2547_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f113909,f89130]) ).
fof(f113915,plain,
sQ2547_spl,
inference(contradiction_clause,[status(thm)],[f113914]) ).
fof(f114211,plain,
( ~ sQ2483_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f111874,f89128]) ).
fof(f114212,plain,
~ sQ2483_spl,
inference(contradiction_clause,[status(thm)],[f114211]) ).
fof(f114503,definition,
( sQ2576_spl
<=> r2_hidden(k3_yellow_0(sK6521_skl),k3_xboole_0(u1_struct_0(sK6520_skl),u1_struct_0(sK6521_skl))) ),
introduced(definition,[new_symbols(definition,[sQ2576_spl])],[split_symbol_definition]) ).
fof(f114504,plain,
( ~ sQ2576_spl
| r2_hidden(k3_yellow_0(sK6521_skl),k3_xboole_0(u1_struct_0(sK6520_skl),u1_struct_0(sK6521_skl))) ),
inference(component_clause,[status(thm)],[f114503]) ).
fof(f115109,plain,
( r2_hidden(k3_yellow_0(sK6521_skl),k3_xboole_0(u1_struct_0(sK6520_skl),u1_struct_0(sK6521_skl)))
| ~ v12_waybel_0(k3_xboole_0(u1_struct_0(sK6520_skl),u1_struct_0(sK6521_skl)),sK6521_skl)
| v1_xboole_0(k3_xboole_0(u1_struct_0(sK6520_skl),u1_struct_0(sK6521_skl)))
| ~ l1_orders_2(sK6521_skl)
| ~ v1_yellow_0(sK6521_skl)
| ~ v4_orders_2(sK6521_skl)
| v3_struct_0(sK6521_skl) ),
inference(resolution,[status(thm)],[f77336,f89131]) ).
fof(f115110,plain,
( sQ2576_spl
| ~ sQ2547_spl
| sQ2483_spl
| ~ sQ2530_spl
| ~ sQ2529_spl
| ~ sQ2528_spl
| sQ2527_spl ),
inference(split_clause,[status(thm)],[f115109,f113808,f113811,f113814,f113817,f111873,f113907,f114503]) ).
fof(f115541,plain,
( ~ sQ2576_spl
| r2_hidden(k3_yellow_0(sK6521_skl),u1_struct_0(sK6520_skl)) ),
inference(resolution,[status(thm)],[f114504,f105667]) ).
fof(f115568,plain,
( ~ sQ2576_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f115541,f89132]) ).
fof(f115569,plain,
~ sQ2576_spl,
inference(contradiction_clause,[status(thm)],[f115568]) ).
fof(f115570,plain,
$false,
inference(sat_refutation,[status(thm)],[f113836,f113838,f113840,f113842,f113915,f114212,f115110,f115569]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEU411+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.45 % Computer : n013.cluster.edu
% 0.19/0.45 % Model : x86_64 x86_64
% 0.19/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.45 % Memory : 8046.5625MB
% 0.19/0.45 % OS : Linux 6.8.0-71-generic
% 0.19/0.46 % CPULimit : 300
% 0.19/0.46 % WCLimit : 300
% 0.19/0.46 % DateTime : Mon Sep 21 06:21:53 UTC 2026
% 0.19/0.46 % CPUTime :
% 4.90/5.17 % Drodi V4.1.1
% 20.41/7.24 % Refutation found
% 20.41/7.24 % SZS status Theorem for theBenchmark: Theorem is valid
% 20.41/7.24 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 5.37/7.95 % Elapsed time: 7.398445 seconds
% 5.37/7.95 % CPU time: 21.578652 seconds
% 5.37/7.95 % Total memory used: 5.315 GB
% 5.37/7.95 % Net memory used: 5.281 GB
%------------------------------------------------------------------------------