%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWX063+1 : TPTP v9.3.1. Released v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/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:36 PM UTC 2026
% Result : Theorem 2.14s 0.99s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWX063+1 : TPTP v9.3.1. Released v9.1.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.42 % Computer : n005.cluster.edu
% 0.08/0.42 % Model : x86_64 x86_64
% 0.08/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.42 % Memory : 8046.5625MB
% 0.08/0.42 % OS : Linux 6.8.0-71-generic
% 0.08/0.42 % CPULimit : 300
% 0.08/0.42 % WCLimit : 300
% 0.08/0.42 % DateTime : Mon Sep 21 10:25:18 UTC 2026
% 0.08/0.43 % CPUTime :
% 0.13/0.46 % Drodi V4.1.1
% 2.14/0.99 % Refutation found
% 2.14/0.99 % SZS status Theorem for theBenchmark: Theorem is valid
% 2.14/0.99 % SZS output start CNFRefutation for theBenchmark
% 2.14/0.99 fof(f342,axiom,(
% 2.14/0.99 rev(nil) = nil ),
% 2.14/0.99 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.14/0.99 fof(f343,axiom,(
% 2.14/0.99 (! [Xl] :( list_succeeds(Xl)=> list_succeeds(rev(Xl)) ) )),
% 2.14/0.99 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.14/0.99 fof(f344,axiom,(
% 2.14/0.99 (! [Xx,Xl] :( list_succeeds(Xl)=> rev(cons(Xx,Xl)) = '**'(rev(Xl),cons(Xx,nil)) ) )),
% 2.14/0.99 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.14/0.99 fof(f353,axiom,(
% 2.14/0.99 (! [Xl,Xy] :( list_succeeds(Xl)=> rev('**'(Xl,cons(Xy,nil))) = cons(Xy,rev(Xl)) ) )),
% 2.14/0.99 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.14/0.99 fof(f354,axiom,(
% 2.14/0.99 ( (! [Xl] :( ( (? [Xx2,Xx3] :( Xl = cons(Xx2,Xx3)& list_succeeds(Xx3)& rev(rev(Xx3)) = Xx3 ))| Xl = nil )=> rev(rev(Xl)) = Xl ))=> (! [Xl] :( list_succeeds(Xl)=> rev(rev(Xl)) = Xl ) )) ),
% 2.14/0.99 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.14/0.99 fof(f355,conjecture,(
% 2.14/0.99 (! [Xl] :( list_succeeds(Xl)=> rev(rev(Xl)) = Xl ) )),
% 2.14/0.99 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.14/0.99 fof(f356,negated_conjecture,(
% 2.14/0.99 ~((! [Xl] :( list_succeeds(Xl)=> rev(rev(Xl)) = Xl ) ))),
% 2.14/0.99 inference(negated_conjecture,[status(cth)],[f355])).
% 2.14/0.99 fof(f1537,plain,(
% 2.14/0.99 rev(nil)=nil),
% 2.14/0.99 inference(cnf_transformation,[status(thm)],[f342])).
% 2.14/0.99 fof(f1538,plain,(
% 2.14/0.99 ![Xl]: (~list_succeeds(Xl)|list_succeeds(rev(Xl)))),
% 2.14/0.99 inference(pre_NNF_transformation,[status(thm)],[f343])).
% 2.14/0.99 fof(f1539,plain,(
% 2.14/0.99 ![X0]: (~list_succeeds(X0)|list_succeeds(rev(X0)))),
% 2.14/0.99 inference(cnf_transformation,[status(thm)],[f1538])).
% 2.14/0.99 fof(f1540,plain,(
% 2.14/0.99 ![Xx,Xl]: (~list_succeeds(Xl)|rev(cons(Xx,Xl))='**'(rev(Xl),cons(Xx,nil)))),
% 2.14/0.99 inference(pre_NNF_transformation,[status(thm)],[f344])).
% 2.14/0.99 fof(f1541,plain,(
% 2.14/0.99 ![Xl]: (~list_succeeds(Xl)|(![Xx]: rev(cons(Xx,Xl))='**'(rev(Xl),cons(Xx,nil))))),
% 2.14/0.99 inference(miniscoping,[status(thm)],[f1540])).
% 2.14/0.99 fof(f1542,plain,(
% 2.14/0.99 ![X0,X1]: (~list_succeeds(X0)|rev(cons(X1,X0))='**'(rev(X0),cons(X1,nil)))),
% 2.14/0.99 inference(cnf_transformation,[status(thm)],[f1541])).
% 2.14/0.99 fof(f1562,plain,(
% 2.14/0.99 ![Xl,Xy]: (~list_succeeds(Xl)|rev('**'(Xl,cons(Xy,nil)))=cons(Xy,rev(Xl)))),
% 2.14/0.99 inference(pre_NNF_transformation,[status(thm)],[f353])).
% 2.14/0.99 fof(f1563,plain,(
% 2.14/0.99 ![Xl]: (~list_succeeds(Xl)|(![Xy]: rev('**'(Xl,cons(Xy,nil)))=cons(Xy,rev(Xl))))),
% 2.14/0.99 inference(miniscoping,[status(thm)],[f1562])).
% 2.14/0.99 fof(f1564,plain,(
% 2.14/0.99 ![X0,X1]: (~list_succeeds(X0)|rev('**'(X0,cons(X1,nil)))=cons(X1,rev(X0)))),
% 2.14/0.99 inference(cnf_transformation,[status(thm)],[f1563])).
% 2.14/0.99 fof(f1565,plain,(
% 2.14/0.99 (?[Xl]: (((?[Xx2,Xx3]: ((Xl=cons(Xx2,Xx3)&list_succeeds(Xx3))&rev(rev(Xx3))=Xx3))|Xl=nil)&~rev(rev(Xl))=Xl))|(![Xl]: (~list_succeeds(Xl)|rev(rev(Xl))=Xl))),
% 2.14/0.99 inference(pre_NNF_transformation,[status(thm)],[f354])).
% 2.14/0.99 fof(f1566,plain,(
% 2.14/0.99 (?[Xl]: (((?[Xx3]: (((?[Xx2]: Xl=cons(Xx2,Xx3))&list_succeeds(Xx3))&rev(rev(Xx3))=Xx3))|Xl=nil)&~rev(rev(Xl))=Xl))|(![Xl]: (~list_succeeds(Xl)|rev(rev(Xl))=Xl))),
% 2.14/0.99 inference(miniscoping,[status(thm)],[f1565])).
% 2.14/0.99 fof(f1567,plain,(
% 2.14/0.99 ((((sK144_skl=cons(sK146_skl,sK145_skl)&list_succeeds(sK145_skl))&rev(rev(sK145_skl))=sK145_skl)|sK144_skl=nil)&~rev(rev(sK144_skl))=sK144_skl)|(![Xl]: (~list_succeeds(Xl)|rev(rev(Xl))=Xl))),
% 2.14/0.99 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])).
% 2.14/0.99 fof(f1568,plain,(
% 2.14/0.99 ![X0]: (sK144_skl=cons(sK146_skl,sK145_skl)|sK144_skl=nil|~list_succeeds(X0)|rev(rev(X0))=X0)),
% 2.14/0.99 inference(cnf_transformation,[status(thm)],[f1567])).
% 2.14/0.99 fof(f1569,plain,(
% 2.14/0.99 ![X0]: (list_succeeds(sK145_skl)|sK144_skl=nil|~list_succeeds(X0)|rev(rev(X0))=X0)),
% 2.14/0.99 inference(cnf_transformation,[status(thm)],[f1567])).
% 2.14/0.99 fof(f1570,plain,(
% 2.14/0.99 ![X0]: (rev(rev(sK145_skl))=sK145_skl|sK144_skl=nil|~list_succeeds(X0)|rev(rev(X0))=X0)),
% 2.14/0.99 inference(cnf_transformation,[status(thm)],[f1567])).
% 2.14/0.99 fof(f1571,plain,(
% 2.14/0.99 ![X0]: (~rev(rev(sK144_skl))=sK144_skl|~list_succeeds(X0)|rev(rev(X0))=X0)),
% 2.14/0.99 inference(cnf_transformation,[status(thm)],[f1567])).
% 2.14/0.99 fof(f1572,plain,(
% 2.14/0.99 (?[Xl]: (list_succeeds(Xl)&~rev(rev(Xl))=Xl))),
% 2.14/0.99 inference(pre_NNF_transformation,[status(thm)],[f356])).
% 2.14/0.99 fof(f1573,plain,(
% 2.14/0.99 (list_succeeds(sK147_skl)&~rev(rev(sK147_skl))=sK147_skl)),
% 2.14/0.99 inference(skolemize,[status(esa),new_symbols(skolem,[sK147_skl]),skolemize(Xl,sK147_skl)],[f1572])).
% 2.14/0.99 fof(f1574,plain,(
% 2.14/0.99 list_succeeds(sK147_skl)),
% 2.14/0.99 inference(cnf_transformation,[status(thm)],[f1573])).
% 2.14/0.99 fof(f1575,plain,(
% 2.14/0.99 ~rev(rev(sK147_skl))=sK147_skl),
% 2.14/0.99 inference(cnf_transformation,[status(thm)],[f1573])).
% 2.14/0.99 fof(f1692,definition,(
% 2.14/0.99 sQ0_spl <=> (sK144_skl=cons(sK146_skl,sK145_skl))),
% 2.14/0.99 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 2.14/0.99 fof(f1693,plain,(
% 2.14/0.99 sK144_skl=cons(sK146_skl,sK145_skl)|~sQ0_spl),
% 2.14/0.99 inference(component_clause,[status(thm)],[f1692])).
% 2.14/0.99 fof(f1695,definition,(
% 2.14/0.99 sQ1_spl <=> (sK144_skl=nil)),
% 2.14/0.99 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 2.14/0.99 fof(f1696,plain,(
% 2.14/0.99 sK144_skl=nil|~sQ1_spl),
% 2.14/0.99 inference(component_clause,[status(thm)],[f1695])).
% 2.14/0.99 fof(f1698,definition,(
% 2.14/0.99 ![X0]: (sQ2_spl <=> (~list_succeeds(X0)|rev(rev(X0))=X0))),
% 2.14/0.99 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 2.14/0.99 fof(f1699,plain,(
% 2.14/0.99 ![X0]: (~list_succeeds(X0)|rev(rev(X0))=X0|~sQ2_spl)),
% 2.14/0.99 inference(component_clause,[status(thm)],[f1698])).
% 2.14/0.99 fof(f1701,plain,(
% 2.14/0.99 sQ0_spl|sQ1_spl|sQ2_spl),
% 2.14/0.99 inference(split_clause,[status(thm)],[f1568,f1692,f1695,f1698])).
% 2.14/0.99 fof(f1702,definition,(
% 2.14/0.99 sQ3_spl <=> (list_succeeds(sK145_skl))),
% 2.14/0.99 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 2.14/0.99 fof(f1703,plain,(
% 2.14/0.99 list_succeeds(sK145_skl)|~sQ3_spl),
% 2.14/0.99 inference(component_clause,[status(thm)],[f1702])).
% 2.14/0.99 fof(f1705,plain,(
% 2.14/0.99 sQ3_spl|sQ1_spl|sQ2_spl),
% 2.14/0.99 inference(split_clause,[status(thm)],[f1569,f1702,f1695,f1698])).
% 2.14/0.99 fof(f1706,definition,(
% 2.14/0.99 sQ4_spl <=> (rev(rev(sK145_skl))=sK145_skl)),
% 2.14/0.99 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 2.14/0.99 fof(f1707,plain,(
% 2.14/0.99 rev(rev(sK145_skl))=sK145_skl|~sQ4_spl),
% 2.14/0.99 inference(component_clause,[status(thm)],[f1706])).
% 2.14/0.99 fof(f1709,plain,(
% 2.14/0.99 sQ4_spl|sQ1_spl|sQ2_spl),
% 2.14/0.99 inference(split_clause,[status(thm)],[f1570,f1706,f1695,f1698])).
% 2.14/0.99 fof(f1710,definition,(
% 2.14/0.99 sQ5_spl <=> (rev(rev(sK144_skl))=sK144_skl)),
% 2.14/0.99 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 2.14/0.99 fof(f1712,plain,(
% 2.14/0.99 ~rev(rev(sK144_skl))=sK144_skl|sQ5_spl),
% 2.14/0.99 inference(component_clause,[status(thm)],[f1710])).
% 2.14/0.99 fof(f1713,plain,(
% 2.14/0.99 ~sQ5_spl|sQ2_spl),
% 2.14/0.99 inference(split_clause,[status(thm)],[f1571,f1710,f1698])).
% 2.14/0.99 fof(f1820,plain,(
% 2.14/0.99 ![X0,X1]: (rev('**'(rev(X0),cons(X1,nil)))=cons(X1,rev(rev(X0)))|~list_succeeds(X0))),
% 2.14/0.99 inference(resolution,[status(thm)],[f1564,f1539])).
% 2.14/0.99 fof(f4306,plain,(
% 2.14/0.99 rev(rev(sK147_skl))=sK147_skl|~sQ2_spl),
% 2.14/0.99 inference(resolution,[status(thm)],[f1699,f1574])).
% 2.14/0.99 fof(f4311,plain,(
% 2.14/0.99 $false|~sQ2_spl),
% 2.14/0.99 inference(forward_subsumption_resolution,[status(thm)],[f4306,f1575])).
% 2.14/0.99 fof(f4312,plain,(
% 2.14/0.99 ~sQ2_spl),
% 2.14/0.99 inference(contradiction_clause,[status(thm)],[f4311])).
% 2.14/0.99 fof(f4313,plain,(
% 2.14/0.99 ~rev(rev(nil))=sK144_skl|~sQ1_spl|sQ5_spl),
% 2.14/0.99 inference(forward_demodulation,[status(thm)],[f1696,f1712])).
% 2.14/0.99 fof(f4314,plain,(
% 2.14/0.99 ~rev(nil)=sK144_skl|~sQ1_spl|sQ5_spl),
% 2.14/0.99 inference(forward_demodulation,[status(thm)],[f1537,f4313])).
% 2.14/0.99 fof(f4315,plain,(
% 2.14/0.99 ~nil=sK144_skl|~sQ1_spl|sQ5_spl),
% 2.14/0.99 inference(forward_demodulation,[status(thm)],[f1537,f4314])).
% 2.14/0.99 fof(f4316,plain,(
% 2.14/0.99 ~nil=nil|~sQ1_spl|sQ5_spl),
% 2.14/0.99 inference(forward_demodulation,[status(thm)],[f1696,f4315])).
% 2.14/0.99 fof(f4317,plain,(
% 2.14/0.99 $false|~sQ1_spl|sQ5_spl),
% 2.14/0.99 inference(trivial_equality_resolution,[status(thm)],[f4316])).
% 2.14/0.99 fof(f4318,plain,(
% 2.14/0.99 ~sQ1_spl|sQ5_spl),
% 2.14/0.99 inference(contradiction_clause,[status(thm)],[f4317])).
% 2.14/0.99 fof(f4347,plain,(
% 2.14/0.99 ![X0]: (rev('**'(rev(sK145_skl),cons(X0,nil)))=cons(X0,rev(rev(sK145_skl)))|~sQ3_spl)),
% 2.14/0.99 inference(resolution,[status(thm)],[f1703,f1820])).
% 2.14/0.99 fof(f4351,plain,(
% 2.14/0.99 ![X0]: (rev(cons(X0,sK145_skl))='**'(rev(sK145_skl),cons(X0,nil))|~sQ3_spl)),
% 2.14/0.99 inference(resolution,[status(thm)],[f1703,f1542])).
% 2.14/0.99 fof(f6387,plain,(
% 2.14/0.99 ![X0]: (rev(rev(cons(X0,sK145_skl)))=cons(X0,rev(rev(sK145_skl)))|~sQ3_spl)),
% 2.14/1.01 inference(forward_demodulation,[status(thm)],[f4351,f4347])).
% 2.14/1.01 fof(f6388,plain,(
% 2.14/1.01 ![X0]: (rev(rev(cons(X0,sK145_skl)))=cons(X0,sK145_skl)|~sQ4_spl|~sQ3_spl)),
% 2.14/1.01 inference(forward_demodulation,[status(thm)],[f1707,f6387])).
% 2.14/1.01 fof(f6389,plain,(
% 2.14/1.01 rev(rev(sK144_skl))=cons(sK146_skl,sK145_skl)|~sQ4_spl|~sQ3_spl|~sQ0_spl),
% 2.14/1.01 inference(paramodulation,[status(thm)],[f1693,f6388])).
% 2.14/1.01 fof(f6394,plain,(
% 2.14/1.01 rev(rev(sK144_skl))=sK144_skl|~sQ4_spl|~sQ3_spl|~sQ0_spl),
% 2.14/1.01 inference(forward_demodulation,[status(thm)],[f1693,f6389])).
% 2.14/1.01 fof(f6395,plain,(
% 2.14/1.01 $false|sQ5_spl|~sQ4_spl|~sQ3_spl|~sQ0_spl),
% 2.14/1.01 inference(forward_subsumption_resolution,[status(thm)],[f6394,f1712])).
% 2.14/1.01 fof(f6396,plain,(
% 2.14/1.01 sQ5_spl|~sQ4_spl|~sQ3_spl|~sQ0_spl),
% 2.14/1.01 inference(contradiction_clause,[status(thm)],[f6395])).
% 2.14/1.01 fof(f6397,plain,(
% 2.14/1.01 $false),
% 2.14/1.01 inference(sat_refutation,[status(thm)],[f1701,f1705,f1709,f1713,f4312,f4318,f6396])).
% 2.14/1.01 % SZS output end CNFRefutation for theBenchmark.p
% 1.67/1.02 % Elapsed time: 0.589373 seconds
% 1.67/1.02 % CPU time: 4.177734 seconds
% 1.67/1.02 % Total memory used: 199.292 MB
% 1.67/1.02 % Net memory used: 193.267 MB
%------------------------------------------------------------------------------