%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWX063+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 03:13:14 PM UTC 2026
% Result : Theorem 0.09s 0.69s
% Output : CNFRefutation 1.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 25
% Syntax : Number of formulae : 123 ( 19 unt; 15 def)
% Number of atoms : 282 ( 82 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 261 ( 102 ~; 114 |; 18 &)
% ( 15 <=>; 12 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 19 ( 17 usr; 16 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 5 con; 0-3 aty)
% Number of variables : 76 ( 63 !; 13 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f7,axiom,
! [Xx12,Xx13] : nil != cons(Xx12,Xx13),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f332,axiom,
! [Xl1,Xl2] :
( n_reverse_succeeds(Xl1,Xl2)
=> ( list_succeeds(Xl2)
& list_succeeds(Xl1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f338,axiom,
! [Xl1] :
( list_succeeds(Xl1)
=> ? [Xl2] : n_reverse_succeeds(Xl1,Xl2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f340,axiom,
! [Xl1] :
( list_succeeds(Xl1)
=> ? [Xl2] :
( ! [Xl3] :
( n_reverse_succeeds(Xl1,Xl3)
=> Xl2 = Xl3 )
& n_reverse_succeeds(Xl1,Xl2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f342,axiom,
rev(nil) = nil,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f343,axiom,
! [Xl] :
( list_succeeds(Xl)
=> list_succeeds(rev(Xl)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f344,axiom,
! [Xx,Xl] :
( list_succeeds(Xl)
=> rev(cons(Xx,Xl)) = '**'(rev(Xl),cons(Xx,nil)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f353,axiom,
! [Xl,Xy] :
( list_succeeds(Xl)
=> rev('**'(Xl,cons(Xy,nil))) = cons(Xy,rev(Xl)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f354,axiom,
( ! [Xl] :
( ( Xl = nil
| ? [Xx2,Xx3] :
( rev(rev(Xx3)) = Xx3
& list_succeeds(Xx3)
& Xl = cons(Xx2,Xx3) ) )
=> rev(rev(Xl)) = Xl )
=> ! [Xl] :
( list_succeeds(Xl)
=> rev(rev(Xl)) = Xl ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f355,conjecture,
! [Xl] :
( list_succeeds(Xl)
=> rev(rev(Xl)) = Xl ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f356,negated_conjecture,
~ ! [Xl] :
( list_succeeds(Xl)
=> rev(rev(Xl)) = Xl ),
inference(negated_conjecture,[status(cth)],[f355]) ).
fof(f364,plain,
! [X0,X1] : nil != cons(X0,X1),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f1506,plain,
! [Xl1,Xl2] :
( ( list_succeeds(Xl2)
& list_succeeds(Xl1) )
| ~ n_reverse_succeeds(Xl1,Xl2) ),
inference(pre_NNF_transformation,[status(thm)],[f332]) ).
fof(f1508,plain,
! [X0,X1] :
( list_succeeds(X1)
| ~ n_reverse_succeeds(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f1506]) ).
fof(f1524,plain,
! [Xl1] :
( ? [Xl2] : n_reverse_succeeds(Xl1,Xl2)
| ~ list_succeeds(Xl1) ),
inference(pre_NNF_transformation,[status(thm)],[f338]) ).
fof(f1525,plain,
! [Xl1] :
( n_reverse_succeeds(Xl1,sK142_skl(Xl1))
| ~ list_succeeds(Xl1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK142_skl]),skolemize(Xl2,sK142_skl(Xl1))],[f1524]) ).
fof(f1526,plain,
! [X0] :
( n_reverse_succeeds(X0,sK142_skl(X0))
| ~ list_succeeds(X0) ),
inference(cnf_transformation,[status(thm)],[f1525]) ).
fof(f1530,plain,
! [Xl1] :
( ? [Xl2] :
( ! [Xl3] :
( Xl2 = Xl3
| ~ n_reverse_succeeds(Xl1,Xl3) )
& n_reverse_succeeds(Xl1,Xl2) )
| ~ list_succeeds(Xl1) ),
inference(pre_NNF_transformation,[status(thm)],[f340]) ).
fof(f1531,plain,
! [Xl1] :
( ( ! [Xl3] :
( sK143_skl(Xl1) = Xl3
| ~ n_reverse_succeeds(Xl1,Xl3) )
& n_reverse_succeeds(Xl1,sK143_skl(Xl1)) )
| ~ list_succeeds(Xl1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK143_skl]),skolemize(Xl2,sK143_skl(Xl1))],[f1530]) ).
fof(f1532,plain,
! [X0] :
( n_reverse_succeeds(X0,sK143_skl(X0))
| ~ list_succeeds(X0) ),
inference(cnf_transformation,[status(thm)],[f1531]) ).
fof(f1537,plain,
rev(nil) = nil,
inference(cnf_transformation,[status(thm)],[f342]) ).
fof(f1538,plain,
! [Xl] :
( list_succeeds(rev(Xl))
| ~ list_succeeds(Xl) ),
inference(pre_NNF_transformation,[status(thm)],[f343]) ).
fof(f1539,plain,
! [X0] :
( list_succeeds(rev(X0))
| ~ list_succeeds(X0) ),
inference(cnf_transformation,[status(thm)],[f1538]) ).
fof(f1540,plain,
! [Xx,Xl] :
( rev(cons(Xx,Xl)) = '**'(rev(Xl),cons(Xx,nil))
| ~ list_succeeds(Xl) ),
inference(pre_NNF_transformation,[status(thm)],[f344]) ).
fof(f1541,plain,
! [Xl] :
( ! [Xx] : rev(cons(Xx,Xl)) = '**'(rev(Xl),cons(Xx,nil))
| ~ list_succeeds(Xl) ),
inference(miniscoping,[status(thm)],[f1540]) ).
fof(f1542,plain,
! [X0,X1] :
( rev(cons(X1,X0)) = '**'(rev(X0),cons(X1,nil))
| ~ list_succeeds(X0) ),
inference(cnf_transformation,[status(thm)],[f1541]) ).
fof(f1562,plain,
! [Xl,Xy] :
( rev('**'(Xl,cons(Xy,nil))) = cons(Xy,rev(Xl))
| ~ list_succeeds(Xl) ),
inference(pre_NNF_transformation,[status(thm)],[f353]) ).
fof(f1563,plain,
! [Xl] :
( ! [Xy] : rev('**'(Xl,cons(Xy,nil))) = cons(Xy,rev(Xl))
| ~ list_succeeds(Xl) ),
inference(miniscoping,[status(thm)],[f1562]) ).
fof(f1564,plain,
! [X0,X1] :
( rev('**'(X0,cons(X1,nil))) = cons(X1,rev(X0))
| ~ list_succeeds(X0) ),
inference(cnf_transformation,[status(thm)],[f1563]) ).
fof(f1565,plain,
( ! [Xl] :
( rev(rev(Xl)) = Xl
| ~ list_succeeds(Xl) )
| ? [Xl] :
( rev(rev(Xl)) != Xl
& ( Xl = nil
| ? [Xx2,Xx3] :
( rev(rev(Xx3)) = Xx3
& list_succeeds(Xx3)
& Xl = cons(Xx2,Xx3) ) ) ) ),
inference(pre_NNF_transformation,[status(thm)],[f354]) ).
fof(f1566,plain,
( ! [Xl] :
( rev(rev(Xl)) = Xl
| ~ list_succeeds(Xl) )
| ? [Xl] :
( rev(rev(Xl)) != Xl
& ( Xl = nil
| ? [Xx3] :
( rev(rev(Xx3)) = Xx3
& list_succeeds(Xx3)
& ? [Xx2] : Xl = cons(Xx2,Xx3) ) ) ) ),
inference(miniscoping,[status(thm)],[f1565]) ).
fof(f1567,plain,
( ! [Xl] :
( rev(rev(Xl)) = Xl
| ~ list_succeeds(Xl) )
| ( rev(rev(sK144_skl)) != sK144_skl
& ( sK144_skl = nil
| ( rev(rev(sK145_skl)) = sK145_skl
& list_succeeds(sK145_skl)
& sK144_skl = cons(sK146_skl,sK145_skl) ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK144_skl,sK145_skl,sK146_skl]),skolemize(Xl,sK144_skl),skolemize(Xx3,sK145_skl),skolemize(Xx2,sK146_skl)],[f1566]) ).
fof(f1568,plain,
! [X0] :
( rev(rev(X0)) = X0
| ~ list_succeeds(X0)
| sK144_skl = nil
| sK144_skl = cons(sK146_skl,sK145_skl) ),
inference(cnf_transformation,[status(thm)],[f1567]) ).
fof(f1569,plain,
! [X0] :
( rev(rev(X0)) = X0
| ~ list_succeeds(X0)
| sK144_skl = nil
| list_succeeds(sK145_skl) ),
inference(cnf_transformation,[status(thm)],[f1567]) ).
fof(f1570,plain,
! [X0] :
( rev(rev(X0)) = X0
| ~ list_succeeds(X0)
| sK144_skl = nil
| rev(rev(sK145_skl)) = sK145_skl ),
inference(cnf_transformation,[status(thm)],[f1567]) ).
fof(f1571,plain,
! [X0] :
( rev(rev(X0)) = X0
| ~ list_succeeds(X0)
| rev(rev(sK144_skl)) != sK144_skl ),
inference(cnf_transformation,[status(thm)],[f1567]) ).
fof(f1572,plain,
? [Xl] :
( rev(rev(Xl)) != Xl
& list_succeeds(Xl) ),
inference(pre_NNF_transformation,[status(thm)],[f356]) ).
fof(f1573,plain,
( rev(rev(sK147_skl)) != sK147_skl
& list_succeeds(sK147_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK147_skl]),skolemize(Xl,sK147_skl)],[f1572]) ).
fof(f1574,plain,
list_succeeds(sK147_skl),
inference(cnf_transformation,[status(thm)],[f1573]) ).
fof(f1575,plain,
rev(rev(sK147_skl)) != sK147_skl,
inference(cnf_transformation,[status(thm)],[f1573]) ).
fof(f1692,definition,
( sQ0_spl
<=> sK144_skl = cons(sK146_skl,sK145_skl) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f1693,plain,
( ~ sQ0_spl
| sK144_skl = cons(sK146_skl,sK145_skl) ),
inference(component_clause,[status(thm)],[f1692]) ).
fof(f1695,definition,
( sQ1_spl
<=> sK144_skl = nil ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f1696,plain,
( ~ sQ1_spl
| sK144_skl = nil ),
inference(component_clause,[status(thm)],[f1695]) ).
fof(f1698,definition,
! [X0] :
( sQ2_spl
<=> ( rev(rev(X0)) = X0
| ~ list_succeeds(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f1699,plain,
! [X0] :
( ~ sQ2_spl
| rev(rev(X0)) = X0
| ~ list_succeeds(X0) ),
inference(component_clause,[status(thm)],[f1698]) ).
fof(f1701,plain,
( sQ2_spl
| sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f1568,f1692,f1695,f1698]) ).
fof(f1702,definition,
( sQ3_spl
<=> list_succeeds(sK145_skl) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f1703,plain,
( ~ sQ3_spl
| list_succeeds(sK145_skl) ),
inference(component_clause,[status(thm)],[f1702]) ).
fof(f1705,plain,
( sQ2_spl
| sQ1_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f1569,f1702,f1695,f1698]) ).
fof(f1706,definition,
( sQ4_spl
<=> rev(rev(sK145_skl)) = sK145_skl ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f1707,plain,
( ~ sQ4_spl
| rev(rev(sK145_skl)) = sK145_skl ),
inference(component_clause,[status(thm)],[f1706]) ).
fof(f1709,plain,
( sQ2_spl
| sQ1_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f1570,f1706,f1695,f1698]) ).
fof(f1710,definition,
( sQ5_spl
<=> rev(rev(sK144_skl)) = sK144_skl ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f1712,plain,
( sQ5_spl
| rev(rev(sK144_skl)) != sK144_skl ),
inference(component_clause,[status(thm)],[f1710]) ).
fof(f1713,plain,
( sQ2_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f1571,f1710,f1698]) ).
fof(f1820,plain,
! [X0,X1] :
( ~ list_succeeds(X0)
| rev('**'(rev(X0),cons(X1,nil))) = cons(X1,rev(rev(X0))) ),
inference(resolution,[status(thm)],[f1564,f1539]) ).
fof(f1927,definition,
( sQ11_spl
<=> list_succeeds(rev(rev(sK147_skl))) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f1929,plain,
( sQ11_spl
| ~ list_succeeds(rev(rev(sK147_skl))) ),
inference(component_clause,[status(thm)],[f1927]) ).
fof(f2911,plain,
! [X0] :
( list_succeeds(sK142_skl(X0))
| ~ list_succeeds(X0) ),
inference(resolution,[status(thm)],[f1526,f1508]) ).
fof(f2922,plain,
list_succeeds(sK142_skl(sK147_skl)),
inference(resolution,[status(thm)],[f2911,f1574]) ).
fof(f2997,plain,
! [X0] :
( list_succeeds(sK143_skl(X0))
| ~ list_succeeds(X0) ),
inference(resolution,[status(thm)],[f1532,f1508]) ).
fof(f3012,plain,
list_succeeds(sK143_skl(sK147_skl)),
inference(resolution,[status(thm)],[f2997,f1574]) ).
fof(f3372,plain,
( ~ sQ2_spl
| rev(rev(sK147_skl)) = sK147_skl ),
inference(resolution,[status(thm)],[f1699,f1574]) ).
fof(f3378,plain,
( ~ sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3372,f1575]) ).
fof(f3379,plain,
~ sQ2_spl,
inference(contradiction_clause,[status(thm)],[f3378]) ).
fof(f3380,plain,
( sQ5_spl
| ~ sQ1_spl
| rev(rev(nil)) != sK144_skl ),
inference(forward_demodulation,[status(thm)],[f1696,f1712]) ).
fof(f3381,plain,
( sQ5_spl
| ~ sQ1_spl
| rev(nil) != sK144_skl ),
inference(forward_demodulation,[status(thm)],[f1537,f3380]) ).
fof(f3382,plain,
( sQ5_spl
| ~ sQ1_spl
| nil != sK144_skl ),
inference(forward_demodulation,[status(thm)],[f1537,f3381]) ).
fof(f3383,plain,
( sQ5_spl
| ~ sQ1_spl
| nil != nil ),
inference(forward_demodulation,[status(thm)],[f1696,f3382]) ).
fof(f3384,plain,
( sQ5_spl
| ~ sQ1_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f3383]) ).
fof(f3385,plain,
( sQ5_spl
| ~ sQ1_spl ),
inference(contradiction_clause,[status(thm)],[f3384]) ).
fof(f3402,plain,
! [X0] :
( ~ sQ3_spl
| rev('**'(rev(sK145_skl),cons(X0,nil))) = cons(X0,rev(rev(sK145_skl))) ),
inference(resolution,[status(thm)],[f1703,f1820]) ).
fof(f3538,plain,
( sQ11_spl
| ~ list_succeeds(rev(sK147_skl)) ),
inference(resolution,[status(thm)],[f1929,f1539]) ).
fof(f3541,plain,
( sQ11_spl
| ~ list_succeeds(sK147_skl) ),
inference(resolution,[status(thm)],[f3538,f1539]) ).
fof(f3543,plain,
( sQ11_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3541,f1574]) ).
fof(f3544,plain,
sQ11_spl,
inference(contradiction_clause,[status(thm)],[f3543]) ).
fof(f3852,definition,
! [X0] :
( sQ65_spl
<=> nil = cons(sK2_skl(X0,X0,nil),sK3_skl(X0,X0,nil)) ),
introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition]) ).
fof(f3853,plain,
! [X0] :
( ~ sQ65_spl
| nil = cons(sK2_skl(X0,X0,nil),sK3_skl(X0,X0,nil)) ),
inference(component_clause,[status(thm)],[f3852]) ).
fof(f3856,plain,
( ~ sQ65_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3853,f364]) ).
fof(f3857,plain,
~ sQ65_spl,
inference(contradiction_clause,[status(thm)],[f3856]) ).
fof(f4979,definition,
( sQ75_spl
<=> sK144_skl = sK144_skl ),
introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition]) ).
fof(f4981,plain,
( sQ75_spl
| sK144_skl != sK144_skl ),
inference(component_clause,[status(thm)],[f4979]) ).
fof(f4986,plain,
( sQ75_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f4981]) ).
fof(f4987,plain,
sQ75_spl,
inference(contradiction_clause,[status(thm)],[f4986]) ).
fof(f5037,definition,
( sQ82_spl
<=> list_succeeds(rev(sK147_skl)) ),
introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition]) ).
fof(f5039,plain,
( sQ82_spl
| ~ list_succeeds(rev(sK147_skl)) ),
inference(component_clause,[status(thm)],[f5037]) ).
fof(f5049,plain,
( sQ82_spl
| ~ list_succeeds(sK147_skl) ),
inference(resolution,[status(thm)],[f5039,f1539]) ).
fof(f5051,plain,
( sQ82_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5049,f1574]) ).
fof(f5052,plain,
sQ82_spl,
inference(contradiction_clause,[status(thm)],[f5051]) ).
fof(f5372,plain,
! [X0] :
( ~ sQ3_spl
| rev(cons(X0,sK145_skl)) = '**'(rev(sK145_skl),cons(X0,nil)) ),
inference(resolution,[status(thm)],[f1703,f1542]) ).
fof(f6745,definition,
( sQ121_spl
<=> list_succeeds(sK147_skl) ),
introduced(definition,[new_symbols(definition,[sQ121_spl])],[split_symbol_definition]) ).
fof(f6747,plain,
( sQ121_spl
| ~ list_succeeds(sK147_skl) ),
inference(component_clause,[status(thm)],[f6745]) ).
fof(f6759,definition,
( sQ124_spl
<=> list_succeeds(rev(sK142_skl(sK147_skl))) ),
introduced(definition,[new_symbols(definition,[sQ124_spl])],[split_symbol_definition]) ).
fof(f6761,plain,
( sQ124_spl
| ~ list_succeeds(rev(sK142_skl(sK147_skl))) ),
inference(component_clause,[status(thm)],[f6759]) ).
fof(f6784,plain,
( sQ121_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6747,f1574]) ).
fof(f6785,plain,
sQ121_spl,
inference(contradiction_clause,[status(thm)],[f6784]) ).
fof(f6786,plain,
( sQ124_spl
| ~ list_succeeds(sK142_skl(sK147_skl)) ),
inference(resolution,[status(thm)],[f6761,f1539]) ).
fof(f6788,plain,
( sQ124_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6786,f2922]) ).
fof(f6789,plain,
sQ124_spl,
inference(contradiction_clause,[status(thm)],[f6788]) ).
fof(f6882,definition,
( sQ139_spl
<=> list_succeeds(sK142_skl(sK147_skl)) ),
introduced(definition,[new_symbols(definition,[sQ139_spl])],[split_symbol_definition]) ).
fof(f6884,plain,
( sQ139_spl
| ~ list_succeeds(sK142_skl(sK147_skl)) ),
inference(component_clause,[status(thm)],[f6882]) ).
fof(f6893,plain,
( sQ139_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6884,f2922]) ).
fof(f6894,plain,
sQ139_spl,
inference(contradiction_clause,[status(thm)],[f6893]) ).
fof(f6897,definition,
( sQ142_spl
<=> list_succeeds(sK143_skl(sK147_skl)) ),
introduced(definition,[new_symbols(definition,[sQ142_spl])],[split_symbol_definition]) ).
fof(f6899,plain,
( sQ142_spl
| ~ list_succeeds(sK143_skl(sK147_skl)) ),
inference(component_clause,[status(thm)],[f6897]) ).
fof(f6908,plain,
( sQ142_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6899,f3012]) ).
fof(f6909,plain,
sQ142_spl,
inference(contradiction_clause,[status(thm)],[f6908]) ).
fof(f7843,definition,
( sQ183_spl
<=> sK147_skl = nil ),
introduced(definition,[new_symbols(definition,[sQ183_spl])],[split_symbol_definition]) ).
fof(f7844,plain,
( ~ sQ183_spl
| sK147_skl = nil ),
inference(component_clause,[status(thm)],[f7843]) ).
fof(f7881,plain,
( ~ sQ183_spl
| rev(rev(sK147_skl)) != nil ),
inference(backward_demodulation,[status(thm)],[f7844,f1575]) ).
fof(f7997,plain,
( ~ sQ183_spl
| rev(rev(nil)) != nil ),
inference(forward_demodulation,[status(thm)],[f7844,f7881]) ).
fof(f7998,plain,
( ~ sQ183_spl
| rev(nil) != nil ),
inference(forward_demodulation,[status(thm)],[f1537,f7997]) ).
fof(f7999,plain,
( ~ sQ183_spl
| nil != nil ),
inference(forward_demodulation,[status(thm)],[f1537,f7998]) ).
fof(f8000,plain,
( ~ sQ183_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f7999]) ).
fof(f8001,plain,
~ sQ183_spl,
inference(contradiction_clause,[status(thm)],[f8000]) ).
fof(f8770,plain,
! [X0] :
( ~ sQ3_spl
| rev(rev(cons(X0,sK145_skl))) = cons(X0,rev(rev(sK145_skl))) ),
inference(forward_demodulation,[status(thm)],[f5372,f3402]) ).
fof(f8771,plain,
! [X0] :
( ~ sQ3_spl
| ~ sQ4_spl
| rev(rev(cons(X0,sK145_skl))) = cons(X0,sK145_skl) ),
inference(forward_demodulation,[status(thm)],[f1707,f8770]) ).
fof(f8772,plain,
( ~ sQ0_spl
| ~ sQ3_spl
| ~ sQ4_spl
| rev(rev(sK144_skl)) = cons(sK146_skl,sK145_skl) ),
inference(paramodulation,[status(thm)],[f1693,f8771]) ).
fof(f8778,plain,
( ~ sQ0_spl
| ~ sQ3_spl
| ~ sQ4_spl
| rev(rev(sK144_skl)) = sK144_skl ),
inference(forward_demodulation,[status(thm)],[f1693,f8772]) ).
fof(f8779,plain,
( ~ sQ0_spl
| ~ sQ3_spl
| ~ sQ4_spl
| sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8778,f1712]) ).
fof(f8780,plain,
( ~ sQ0_spl
| ~ sQ3_spl
| ~ sQ4_spl
| sQ5_spl ),
inference(contradiction_clause,[status(thm)],[f8779]) ).
fof(f8781,plain,
$false,
inference(sat_refutation,[status(thm)],[f1701,f1705,f1709,f1713,f3379,f3385,f3544,f3857,f4987,f5052,f6785,f6789,f6894,f6909,f8001,f8780]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWX063+1 : TPTP v9.3.1. Released v9.1.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n005.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 10:25:18 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.40 % Drodi V4.1.1
% 0.09/0.69 % Refutation found
% 0.09/0.69 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.09/0.69 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 1.15/0.73 % Elapsed time: 0.345221 seconds
% 1.15/0.73 % CPU time: 2.271331 seconds
% 1.15/0.73 % Total memory used: 163.243 MB
% 1.15/0.73 % Net memory used: 160.754 MB
%------------------------------------------------------------------------------