%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEV569+1 : TPTP v9.3.1. Released v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n005.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:33:02 PM UTC 2026
% Result : Theorem 101.47s 18.42s
% Output : CNFRefutation 89.29s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 19
% Syntax : Number of formulae : 101 ( 16 unt; 12 def)
% Number of atoms : 270 ( 71 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 263 ( 94 ~; 140 |; 12 &)
% ( 16 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 16 ( 14 usr; 13 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 1 con; 0-2 aty)
% Number of variables : 97 ( 95 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X,Y] :
( subq(X,Y)
<=> ! [Z] :
( mem(Z,X)
=> mem(Z,Y) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [X] : ~ mem(X,e),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [X,Y] :
( mem(X,s(Y))
<=> X = Y ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [X,Y,Z] :
( mem(X,u(Y,Z))
<=> ( mem(X,Z)
| mem(X,Y) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [X,Y] : a(X,Y) = u(X,s(Y)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [X] : n(X) = a(X,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f26,conjecture,
~ subq(u(a(s(u(n(e),n(s(n(e))))),a(n(e),n(n(e)))),u(a(s(n(e)),n(n(e))),a(s(n(s(n(e)))),n(n(n(e)))))),u(a(s(u(n(e),n(s(n(e))))),a(n(e),n(n(e)))),u(s(n(n(e))),a(s(n(s(n(e)))),n(n(n(e))))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f27,negated_conjecture,
~ ~ subq(u(a(s(u(n(e),n(s(n(e))))),a(n(e),n(n(e)))),u(a(s(n(e)),n(n(e))),a(s(n(s(n(e)))),n(n(n(e)))))),u(a(s(u(n(e),n(s(n(e))))),a(n(e),n(n(e)))),u(s(n(n(e))),a(s(n(s(n(e)))),n(n(n(e))))))),
inference(negated_conjecture,[status(cth)],[f26]) ).
fof(f28,plain,
! [X,Y] :
( subq(X,Y)
<=> ! [Z] :
( mem(Z,Y)
| ~ mem(Z,X) ) ),
inference(pre_NNF_transformation,[status(thm)],[f1]) ).
fof(f29,plain,
! [X,Y] :
( ( ? [Z] :
( ~ mem(Z,Y)
& mem(Z,X) )
| subq(X,Y) )
& ( ! [Z] :
( mem(Z,Y)
| ~ mem(Z,X) )
| ~ subq(X,Y) ) ),
inference(NNF_transformation,[status(thm)],[f28]) ).
fof(f30,plain,
( ! [X,Y] :
( ? [Z] :
( ~ mem(Z,Y)
& mem(Z,X) )
| subq(X,Y) )
& ! [X,Y] :
( ! [Z] :
( mem(Z,Y)
| ~ mem(Z,X) )
| ~ subq(X,Y) ) ),
inference(miniscoping,[status(thm)],[f29]) ).
fof(f31,plain,
( ! [X,Y] :
( ( ~ mem(sK0_skl(Y,X),Y)
& mem(sK0_skl(Y,X),X) )
| subq(X,Y) )
& ! [X,Y] :
( ! [Z] :
( mem(Z,Y)
| ~ mem(Z,X) )
| ~ subq(X,Y) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(Z,sK0_skl(Y,X))],[f30]) ).
fof(f32,plain,
! [X0,X1,X2] :
( ~ mem(X2,X0)
| mem(X2,X1)
| ~ subq(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f31]) ).
fof(f44,plain,
! [X0] : ~ mem(X0,e),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f45,plain,
! [X,Y] :
( ( X != Y
| mem(X,s(Y)) )
& ( X = Y
| ~ mem(X,s(Y)) ) ),
inference(NNF_transformation,[status(thm)],[f5]) ).
fof(f46,plain,
( ! [X,Y] :
( X != Y
| mem(X,s(Y)) )
& ! [X,Y] :
( X = Y
| ~ mem(X,s(Y)) ) ),
inference(miniscoping,[status(thm)],[f45]) ).
fof(f47,plain,
! [X0,X1] :
( X0 = X1
| ~ mem(X0,s(X1)) ),
inference(cnf_transformation,[status(thm)],[f46]) ).
fof(f48,plain,
! [X0,X1] :
( X0 != X1
| mem(X0,s(X1)) ),
inference(cnf_transformation,[status(thm)],[f46]) ).
fof(f49,plain,
! [X,Y,Z] :
( ( ( ~ mem(X,Z)
& ~ mem(X,Y) )
| mem(X,u(Y,Z)) )
& ( mem(X,Z)
| mem(X,Y)
| ~ mem(X,u(Y,Z)) ) ),
inference(NNF_transformation,[status(thm)],[f6]) ).
fof(f50,plain,
( ! [X,Y,Z] :
( ( ~ mem(X,Z)
& ~ mem(X,Y) )
| mem(X,u(Y,Z)) )
& ! [X,Y,Z] :
( mem(X,Z)
| mem(X,Y)
| ~ mem(X,u(Y,Z)) ) ),
inference(miniscoping,[status(thm)],[f49]) ).
fof(f51,plain,
! [X0,X1,X2] :
( ~ mem(X0,u(X2,X1))
| mem(X0,X2)
| mem(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f52,plain,
! [X0,X1,X2] :
( mem(X0,u(X1,X2))
| ~ mem(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f53,plain,
! [X0,X1,X2] :
( ~ mem(X0,X2)
| mem(X0,u(X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f59,plain,
! [X0,X1] : u(X0,s(X1)) = a(X0,X1),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f60,plain,
! [X0] : n(X0) = a(X0,X0),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f169,plain,
subq(u(a(s(u(n(e),n(s(n(e))))),a(n(e),n(n(e)))),u(a(s(n(e)),n(n(e))),a(s(n(s(n(e)))),n(n(n(e)))))),u(a(s(u(n(e),n(s(n(e))))),a(n(e),n(n(e)))),u(s(n(n(e))),a(s(n(s(n(e)))),n(n(n(e))))))),
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f170,plain,
! [X0] : mem(X0,s(X0)),
inference(destructive_equality_resolution,[status(thm)],[f48]) ).
fof(f172,plain,
! [X0,X1,X2] :
( ~ mem(X0,X1)
| mem(X0,a(X1,X2)) ),
inference(paramodulation,[status(thm)],[f59,f52]) ).
fof(f181,plain,
! [X0,X1,X2] :
( ~ mem(X0,s(X2))
| mem(X0,a(X1,X2)) ),
inference(paramodulation,[status(thm)],[f59,f53]) ).
fof(f183,plain,
! [X0,X1] : mem(X0,a(X1,X0)),
inference(resolution,[status(thm)],[f181,f170]) ).
fof(f184,plain,
! [X0] : mem(X0,n(X0)),
inference(paramodulation,[status(thm)],[f60,f183]) ).
fof(f187,plain,
! [X0,X1,X2] :
( mem(X0,s(X2))
| mem(X0,X1)
| ~ mem(X0,a(X1,X2)) ),
inference(paramodulation,[status(thm)],[f59,f51]) ).
fof(f189,plain,
! [X0,X1,X2] :
( mem(X0,X2)
| ~ mem(X0,a(X2,X1))
| X0 = X1 ),
inference(resolution,[status(thm)],[f187,f47]) ).
fof(f192,plain,
! [X0,X1] :
( mem(X1,X0)
| ~ mem(X1,n(X0))
| X0 = X1 ),
inference(paramodulation,[status(thm)],[f60,f189]) ).
fof(f375,plain,
! [X0] :
( mem(X0,u(a(s(u(n(e),n(s(n(e))))),a(n(e),n(n(e)))),u(s(n(n(e))),a(s(n(s(n(e)))),n(n(n(e)))))))
| ~ mem(X0,u(a(s(u(n(e),n(s(n(e))))),a(n(e),n(n(e)))),u(a(s(n(e)),n(n(e))),a(s(n(s(n(e)))),n(n(n(e))))))) ),
inference(resolution,[status(thm)],[f32,f169]) ).
fof(f520,plain,
! [X0] :
( ~ mem(X0,u(a(s(u(n(e),n(s(n(e))))),a(n(e),n(n(e)))),u(a(s(n(e)),n(n(e))),a(s(n(s(n(e)))),n(n(n(e)))))))
| mem(X0,a(s(u(n(e),n(s(n(e))))),a(n(e),n(n(e)))))
| mem(X0,u(s(n(n(e))),a(s(n(s(n(e)))),n(n(n(e)))))) ),
inference(resolution,[status(thm)],[f375,f51]) ).
fof(f525,plain,
! [X0] :
( mem(X0,u(s(n(n(e))),a(s(n(s(n(e)))),n(n(n(e))))))
| ~ mem(X0,u(a(s(u(n(e),n(s(n(e))))),a(n(e),n(n(e)))),u(a(s(n(e)),n(n(e))),a(s(n(s(n(e)))),n(n(n(e)))))))
| X0 = a(n(e),n(n(e)))
| mem(X0,s(u(n(e),n(s(n(e)))))) ),
inference(resolution,[status(thm)],[f520,f189]) ).
fof(f528,plain,
! [X0] :
( mem(X0,s(n(n(e))))
| ~ mem(X0,u(a(s(u(n(e),n(s(n(e))))),a(n(e),n(n(e)))),u(a(s(n(e)),n(n(e))),a(s(n(s(n(e)))),n(n(n(e)))))))
| a(n(e),n(n(e))) = X0
| mem(X0,a(s(n(s(n(e)))),n(n(n(e)))))
| mem(X0,s(u(n(e),n(s(n(e)))))) ),
inference(resolution,[status(thm)],[f525,f51]) ).
fof(f530,plain,
! [X0] :
( X0 = n(n(n(e)))
| mem(X0,s(n(n(e))))
| ~ mem(X0,u(a(s(u(n(e),n(s(n(e))))),a(n(e),n(n(e)))),u(a(s(n(e)),n(n(e))),a(s(n(s(n(e)))),n(n(n(e)))))))
| X0 = a(n(e),n(n(e)))
| mem(X0,s(u(n(e),n(s(n(e))))))
| mem(X0,s(n(s(n(e))))) ),
inference(resolution,[status(thm)],[f528,f189]) ).
fof(f548,plain,
! [X0] :
( mem(X0,s(u(n(e),n(s(n(e))))))
| X0 = n(n(n(e)))
| X0 = a(n(e),n(n(e)))
| mem(X0,s(n(s(n(e)))))
| ~ mem(X0,u(a(s(u(n(e),n(s(n(e))))),a(n(e),n(n(e)))),u(a(s(n(e)),n(n(e))),a(s(n(s(n(e)))),n(n(n(e)))))))
| n(n(e)) = X0 ),
inference(resolution,[status(thm)],[f530,f47]) ).
fof(f551,plain,
! [X0] :
( X0 = n(n(n(e)))
| ~ mem(X0,u(a(s(u(n(e),n(s(n(e))))),a(n(e),n(n(e)))),u(a(s(n(e)),n(n(e))),a(s(n(s(n(e)))),n(n(n(e)))))))
| X0 = n(n(e))
| mem(X0,s(u(n(e),n(s(n(e))))))
| X0 = n(s(n(e)))
| X0 = a(n(e),n(n(e))) ),
inference(resolution,[status(thm)],[f548,f47]) ).
fof(f554,plain,
! [X0] :
( X0 = n(n(e))
| X0 = u(n(e),n(s(n(e))))
| X0 = n(n(n(e)))
| a(n(e),n(n(e))) = X0
| ~ mem(X0,u(a(s(u(n(e),n(s(n(e))))),a(n(e),n(n(e)))),u(a(s(n(e)),n(n(e))),a(s(n(s(n(e)))),n(n(n(e)))))))
| X0 = n(s(n(e))) ),
inference(resolution,[status(thm)],[f551,f47]) ).
fof(f557,plain,
! [X0] :
( X0 = a(n(e),n(n(e)))
| ~ mem(X0,u(a(s(n(e)),n(n(e))),a(s(n(s(n(e)))),n(n(n(e))))))
| n(s(n(e))) = X0
| u(n(e),n(s(n(e)))) = X0
| n(n(n(e))) = X0
| X0 = n(n(e)) ),
inference(resolution,[status(thm)],[f554,f53]) ).
fof(f627,plain,
! [X0] :
( n(n(n(e))) = X0
| X0 = n(n(e))
| X0 = n(s(n(e)))
| ~ mem(X0,a(s(n(e)),n(n(e))))
| X0 = u(n(e),n(s(n(e))))
| a(n(e),n(n(e))) = X0 ),
inference(resolution,[status(thm)],[f557,f52]) ).
fof(f770,plain,
! [X0] :
( n(n(n(e))) = X0
| X0 = u(n(e),n(s(n(e))))
| X0 = a(n(e),n(n(e)))
| ~ mem(X0,s(n(e)))
| X0 = n(n(e))
| X0 = n(s(n(e))) ),
inference(resolution,[status(thm)],[f627,f172]) ).
fof(f1213,plain,
( u(n(e),n(s(n(e)))) = n(e)
| n(e) = n(n(n(e)))
| n(n(e)) = n(e)
| n(e) = a(n(e),n(n(e)))
| n(s(n(e))) = n(e) ),
inference(resolution,[status(thm)],[f770,f170]) ).
fof(f1214,definition,
( sQ96_spl
<=> n(s(n(e))) = n(e) ),
introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition]) ).
fof(f1215,plain,
( ~ sQ96_spl
| n(e) = n(s(n(e))) ),
inference(component_clause,[status(thm)],[f1214]) ).
fof(f1217,definition,
( sQ97_spl
<=> n(e) = a(n(e),n(n(e))) ),
introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition]) ).
fof(f1218,plain,
( ~ sQ97_spl
| a(n(e),n(n(e))) = n(e) ),
inference(component_clause,[status(thm)],[f1217]) ).
fof(f1220,definition,
( sQ98_spl
<=> n(n(e)) = n(e) ),
introduced(definition,[new_symbols(definition,[sQ98_spl])],[split_symbol_definition]) ).
fof(f1221,plain,
( ~ sQ98_spl
| n(e) = n(n(e)) ),
inference(component_clause,[status(thm)],[f1220]) ).
fof(f1223,definition,
( sQ99_spl
<=> n(e) = n(n(n(e))) ),
introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition]) ).
fof(f1224,plain,
( ~ sQ99_spl
| n(e) = n(n(n(e))) ),
inference(component_clause,[status(thm)],[f1223]) ).
fof(f1226,definition,
( sQ100_spl
<=> u(n(e),n(s(n(e)))) = n(e) ),
introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition]) ).
fof(f1227,plain,
( ~ sQ100_spl
| u(n(e),n(s(n(e)))) = n(e) ),
inference(component_clause,[status(thm)],[f1226]) ).
fof(f1229,plain,
( sQ100_spl
| sQ99_spl
| sQ98_spl
| sQ97_spl
| sQ96_spl ),
inference(split_clause,[status(thm)],[f1213,f1214,f1217,f1220,f1223,f1226]) ).
fof(f1246,plain,
( ~ sQ98_spl
| mem(n(e),n(e)) ),
inference(paramodulation,[status(thm)],[f1221,f184]) ).
fof(f1280,plain,
( ~ sQ96_spl
| mem(s(n(e)),n(e)) ),
inference(paramodulation,[status(thm)],[f1215,f184]) ).
fof(f1303,plain,
( ~ sQ99_spl
| mem(n(n(e)),n(e)) ),
inference(paramodulation,[status(thm)],[f1224,f184]) ).
fof(f1399,plain,
( ~ sQ97_spl
| mem(n(n(e)),n(e)) ),
inference(paramodulation,[status(thm)],[f1218,f183]) ).
fof(f1447,plain,
! [X0] :
( ~ sQ100_spl
| ~ mem(X0,n(s(n(e))))
| mem(X0,n(e)) ),
inference(paramodulation,[status(thm)],[f1227,f53]) ).
fof(f1541,definition,
( sQ120_spl
<=> mem(n(n(e)),n(e)) ),
introduced(definition,[new_symbols(definition,[sQ120_spl])],[split_symbol_definition]) ).
fof(f1542,plain,
( ~ sQ120_spl
| mem(n(n(e)),n(e)) ),
inference(component_clause,[status(thm)],[f1541]) ).
fof(f1562,plain,
( ~ sQ98_spl
| mem(n(e),e)
| e = n(e) ),
inference(resolution,[status(thm)],[f1246,f192]) ).
fof(f1563,definition,
( sQ122_spl
<=> e = n(e) ),
introduced(definition,[new_symbols(definition,[sQ122_spl])],[split_symbol_definition]) ).
fof(f1564,plain,
( ~ sQ122_spl
| e = n(e) ),
inference(component_clause,[status(thm)],[f1563]) ).
fof(f1566,definition,
( sQ123_spl
<=> mem(n(e),e) ),
introduced(definition,[new_symbols(definition,[sQ123_spl])],[split_symbol_definition]) ).
fof(f1567,plain,
( ~ sQ123_spl
| mem(n(e),e) ),
inference(component_clause,[status(thm)],[f1566]) ).
fof(f1569,plain,
( ~ sQ98_spl
| sQ123_spl
| sQ122_spl ),
inference(split_clause,[status(thm)],[f1562,f1563,f1566,f1220]) ).
fof(f1570,plain,
( ~ sQ123_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1567,f44]) ).
fof(f1571,plain,
~ sQ123_spl,
inference(contradiction_clause,[status(thm)],[f1570]) ).
fof(f1572,plain,
( ~ sQ98_spl
| ~ sQ122_spl
| mem(n(e),e) ),
inference(backward_demodulation,[status(thm)],[f1564,f1246]) ).
fof(f1640,plain,
( ~ sQ98_spl
| ~ sQ122_spl
| sQ123_spl ),
inference(split_clause,[status(thm)],[f1572,f1566,f1563,f1220]) ).
fof(f2382,plain,
( ~ sQ120_spl
| mem(n(n(e)),e)
| e = n(n(e)) ),
inference(resolution,[status(thm)],[f1542,f192]) ).
fof(f2383,definition,
( sQ125_spl
<=> e = n(n(e)) ),
introduced(definition,[new_symbols(definition,[sQ125_spl])],[split_symbol_definition]) ).
fof(f2384,plain,
( ~ sQ125_spl
| n(n(e)) = e ),
inference(component_clause,[status(thm)],[f2383]) ).
fof(f2386,definition,
( sQ126_spl
<=> mem(n(n(e)),e) ),
introduced(definition,[new_symbols(definition,[sQ126_spl])],[split_symbol_definition]) ).
fof(f2387,plain,
( ~ sQ126_spl
| mem(n(n(e)),e) ),
inference(component_clause,[status(thm)],[f2386]) ).
fof(f2389,plain,
( ~ sQ120_spl
| sQ126_spl
| sQ125_spl ),
inference(split_clause,[status(thm)],[f2382,f2383,f2386,f1541]) ).
fof(f2390,plain,
( ~ sQ126_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2387,f44]) ).
fof(f2391,plain,
~ sQ126_spl,
inference(contradiction_clause,[status(thm)],[f2390]) ).
fof(f2407,plain,
( ~ sQ125_spl
| mem(n(e),e) ),
inference(paramodulation,[status(thm)],[f2384,f184]) ).
fof(f2416,plain,
( ~ sQ125_spl
| sQ123_spl ),
inference(split_clause,[status(thm)],[f2407,f1566,f2383]) ).
fof(f2481,plain,
( ~ sQ97_spl
| sQ120_spl ),
inference(split_clause,[status(thm)],[f1399,f1541,f1217]) ).
fof(f2485,plain,
( ~ sQ96_spl
| mem(s(n(e)),e)
| e = s(n(e)) ),
inference(resolution,[status(thm)],[f1280,f192]) ).
fof(f2486,definition,
( sQ134_spl
<=> e = s(n(e)) ),
introduced(definition,[new_symbols(definition,[sQ134_spl])],[split_symbol_definition]) ).
fof(f2487,plain,
( ~ sQ134_spl
| e = s(n(e)) ),
inference(component_clause,[status(thm)],[f2486]) ).
fof(f2489,definition,
( sQ135_spl
<=> mem(s(n(e)),e) ),
introduced(definition,[new_symbols(definition,[sQ135_spl])],[split_symbol_definition]) ).
fof(f2490,plain,
( ~ sQ135_spl
| mem(s(n(e)),e) ),
inference(component_clause,[status(thm)],[f2489]) ).
fof(f2492,plain,
( ~ sQ96_spl
| sQ135_spl
| sQ134_spl ),
inference(split_clause,[status(thm)],[f2485,f2486,f2489,f1214]) ).
fof(f2494,plain,
( ~ sQ135_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2490,f44]) ).
fof(f2495,plain,
~ sQ135_spl,
inference(contradiction_clause,[status(thm)],[f2494]) ).
fof(f2520,plain,
( ~ sQ134_spl
| mem(n(e),e) ),
inference(paramodulation,[status(thm)],[f2487,f170]) ).
fof(f2566,plain,
( ~ sQ134_spl
| sQ123_spl ),
inference(split_clause,[status(thm)],[f2520,f1566,f2486]) ).
fof(f2590,plain,
( ~ sQ99_spl
| sQ120_spl ),
inference(split_clause,[status(thm)],[f1303,f1541,f1223]) ).
fof(f2801,plain,
! [X0] :
( ~ sQ100_spl
| mem(X0,e)
| e = X0
| ~ mem(X0,n(s(n(e)))) ),
inference(resolution,[status(thm)],[f1447,f192]) ).
fof(f2802,plain,
! [X0] :
( ~ sQ100_spl
| ~ mem(X0,n(s(n(e))))
| e = X0 ),
inference(forward_subsumption_resolution,[status(thm)],[f2801,f44]) ).
fof(f2847,plain,
( ~ sQ100_spl
| e = s(n(e)) ),
inference(resolution,[status(thm)],[f2802,f184]) ).
fof(f2849,plain,
( ~ sQ100_spl
| sQ134_spl ),
inference(split_clause,[status(thm)],[f2847,f2486,f1226]) ).
fof(f2850,plain,
$false,
inference(sat_refutation,[status(thm)],[f1229,f1569,f1571,f1640,f2389,f2391,f2416,f2481,f2492,f2495,f2566,f2590,f2849]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEV569+1 : TPTP v9.3.1. Released v9.1.0.
% 0.00/0.07 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/5.47 % Computer : n005.cluster.edu
% 0.18/5.47 % Model : x86_64 x86_64
% 0.18/5.47 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/5.47 % Memory : 8046.5625MB
% 0.18/5.47 % OS : Linux 6.8.0-71-generic
% 0.18/5.47 % CPULimit : 300
% 0.18/5.47 % WCLimit : 300
% 0.18/5.47 % DateTime : Mon Sep 21 07:27:39 UTC 2026
% 0.18/5.47 % CPUTime :
% 0.18/5.49 % Drodi V4.1.1
% 101.47/18.42 % Refutation found
% 101.47/18.42 % SZS status Theorem for theBenchmark: Theorem is valid
% 101.47/18.42 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 78.54/19.71 % Elapsed time: 14.012667 seconds
% 78.54/19.71 % CPU time: 100.025217 seconds
% 78.54/19.71 % Total memory used: 498.089 MB
% 78.54/19.71 % Net memory used: 461.009 MB
%------------------------------------------------------------------------------