%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWC357-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n009.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:42:15 PM UTC 2026
% Result : Unsatisfiable 2.51s 0.79s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWC357-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n009.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 08:18:12 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.12/0.37 % Drodi V4.1.1
% 2.51/0.79 % Refutation found
% 2.51/0.79 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 2.51/0.79 % SZS output start CNFRefutation for theBenchmark
% 2.51/0.79 fof(f8,axiom,(
% 2.51/0.79 ssList(nil) ),
% 2.51/0.79 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.51/0.79 fof(f51,axiom,(
% 2.51/0.79 (![U,V]: (ssList(skaf45(U,V)) ))),
% 2.51/0.79 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.51/0.79 fof(f56,axiom,(
% 2.51/0.79 (![U]: (( ~ ssList(U)| segmentP(U,nil) ) ))),
% 2.51/0.79 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.51/0.79 fof(f74,axiom,(
% 2.51/0.79 (![U]: (( ~ ssList(U)| app(nil,U) = U ) ))),
% 2.51/0.79 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.51/0.79 fof(f85,axiom,(
% 2.51/0.79 (![U,V]: (( ~ ssList(U)| ~ ssList(V)| ssList(app(V,U)) ) ))),
% 2.51/0.79 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.51/0.79 fof(f132,axiom,(
% 2.51/0.79 (![U,V]: (( ~ frontsegP(U,V)| ~ ssList(V)| ~ ssList(U)| app(V,skaf45(U,V)) = U ) ))),
% 2.51/0.79 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.51/0.79 fof(f173,axiom,(
% 2.51/0.79 (![U,V,W,X]: (( app(app(U,V),W) != X| ~ ssList(W)| ~ ssList(U)| ~ ssList(V)| ~ ssList(X)| segmentP(X,V) ) ))),
% 2.51/0.79 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.51/0.79 fof(f186,negated_conjecture,(
% 2.51/0.79 ssList(sk1) ),
% 2.51/0.79 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.51/0.79 fof(f187,negated_conjecture,(
% 2.51/0.79 ssList(sk2) ),
% 2.51/0.79 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.51/0.79 fof(f190,negated_conjecture,(
% 2.51/0.79 sk2 = sk4 ),
% 2.51/0.79 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.51/0.79 fof(f191,negated_conjecture,(
% 2.51/0.79 sk1 = sk3 ),
% 2.51/0.79 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.51/0.79 fof(f193,negated_conjecture,(
% 2.51/0.79 ~ segmentP(sk2,sk1) ),
% 2.51/0.79 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.51/0.79 fof(f195,negated_conjecture,(
% 2.51/0.79 ( nil = sk4| frontsegP(sk4,sk3) ) ),
% 2.51/0.79 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.51/0.79 fof(f197,negated_conjecture,(
% 2.51/0.79 ( nil = sk3| frontsegP(sk4,sk3) ) ),
% 2.51/0.79 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.51/0.79 fof(f205,plain,(
% 2.51/0.79 ssList(nil)),
% 2.51/0.79 inference(cnf_transformation,[status(thm)],[f8])).
% 2.51/0.79 fof(f248,plain,(
% 2.51/0.79 ![X0,X1]: (ssList(skaf45(X0,X1)))),
% 2.51/0.79 inference(cnf_transformation,[status(thm)],[f51])).
% 2.51/0.79 fof(f253,plain,(
% 2.51/0.79 ![X0]: (~ssList(X0)|segmentP(X0,nil))),
% 2.51/0.79 inference(cnf_transformation,[status(thm)],[f56])).
% 2.51/0.79 fof(f272,plain,(
% 2.51/0.79 ![X0]: (~ssList(X0)|app(nil,X0)=X0)),
% 2.51/0.79 inference(cnf_transformation,[status(thm)],[f74])).
% 2.51/0.79 fof(f283,plain,(
% 2.51/0.79 ![X0,X1]: (~ssList(X0)|~ssList(X1)|ssList(app(X1,X0)))),
% 2.51/0.79 inference(cnf_transformation,[status(thm)],[f85])).
% 2.51/0.79 fof(f342,plain,(
% 2.51/0.79 ![X0,X1]: (~frontsegP(X0,X1)|~ssList(X1)|~ssList(X0)|app(X1,skaf45(X0,X1))=X0)),
% 2.51/0.79 inference(cnf_transformation,[status(thm)],[f132])).
% 2.51/0.79 fof(f403,plain,(
% 2.51/0.79 ![V,X]: ((((![U]: ((![W]: (~app(app(U,V),W)=X|~ssList(W)))|~ssList(U)))|~ssList(V))|~ssList(X))|segmentP(X,V))),
% 2.51/0.79 inference(miniscoping,[status(thm)],[f173])).
% 2.51/0.79 fof(f404,plain,(
% 2.51/0.79 ![X0,X1,X2,X3]: (~app(app(X0,X1),X2)=X3|~ssList(X2)|~ssList(X0)|~ssList(X1)|~ssList(X3)|segmentP(X3,X1))),
% 2.51/0.79 inference(cnf_transformation,[status(thm)],[f403])).
% 2.51/0.79 fof(f428,plain,(
% 2.51/0.79 ssList(sk1)),
% 2.51/0.79 inference(cnf_transformation,[status(thm)],[f186])).
% 2.51/0.79 fof(f429,plain,(
% 2.51/0.79 ssList(sk2)),
% 2.51/0.79 inference(cnf_transformation,[status(thm)],[f187])).
% 2.51/0.79 fof(f432,plain,(
% 2.51/0.79 sk2=sk4),
% 2.51/0.79 inference(cnf_transformation,[status(thm)],[f190])).
% 2.51/0.79 fof(f433,plain,(
% 2.51/0.79 sk1=sk3),
% 2.51/0.79 inference(cnf_transformation,[status(thm)],[f191])).
% 2.51/0.79 fof(f435,plain,(
% 2.51/0.79 ~segmentP(sk2,sk1)),
% 2.51/0.79 inference(cnf_transformation,[status(thm)],[f193])).
% 2.51/0.79 fof(f437,plain,(
% 2.51/0.79 nil=sk4|frontsegP(sk4,sk3)),
% 2.51/0.79 inference(cnf_transformation,[status(thm)],[f195])).
% 2.51/0.79 fof(f439,plain,(
% 2.51/0.79 nil=sk3|frontsegP(sk4,sk3)),
% 2.51/0.79 inference(cnf_transformation,[status(thm)],[f197])).
% 2.51/0.79 fof(f447,definition,(
% 2.51/0.79 sQ2_spl <=> (nil=sk4)),
% 2.51/0.79 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 2.51/0.79 fof(f448,plain,(
% 2.51/0.79 nil=sk4|~sQ2_spl),
% 2.51/0.79 inference(component_clause,[status(thm)],[f447])).
% 2.51/0.79 fof(f454,definition,(
% 2.51/0.79 sQ4_spl <=> (frontsegP(sk4,sk3))),
% 2.51/0.79 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 2.51/0.79 fof(f455,plain,(
% 2.51/0.79 frontsegP(sk4,sk3)|~sQ4_spl),
% 2.51/0.79 inference(component_clause,[status(thm)],[f454])).
% 2.51/0.79 fof(f457,plain,(
% 2.51/0.79 sQ2_spl|sQ4_spl),
% 2.51/0.79 inference(split_clause,[status(thm)],[f437,f447,f454])).
% 2.51/0.79 fof(f458,definition,(
% 2.51/0.79 sQ5_spl <=> (nil=sk3)),
% 2.51/0.79 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 2.51/0.79 fof(f459,plain,(
% 2.51/0.79 nil=sk3|~sQ5_spl),
% 2.51/0.79 inference(component_clause,[status(thm)],[f458])).
% 2.51/0.79 fof(f462,plain,(
% 2.51/0.79 sQ5_spl|sQ4_spl),
% 2.51/0.79 inference(split_clause,[status(thm)],[f439,f458,f454])).
% 2.51/0.79 fof(f481,plain,(
% 2.51/0.79 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(app(app(X1,X2),X0))|segmentP(app(app(X1,X2),X0),X2))),
% 2.51/0.79 inference(destructive_equality_resolution,[status(thm)],[f404])).
% 2.51/0.79 fof(f495,plain,(
% 2.51/0.79 nil=sk1|~sQ5_spl),
% 2.51/0.79 inference(forward_demodulation,[status(thm)],[f433,f459])).
% 2.51/0.79 fof(f496,plain,(
% 2.51/0.79 sk2=sk1|~sQ5_spl|~sQ2_spl),
% 2.51/0.79 inference(backward_demodulation,[status(thm)],[f497,f432])).
% 2.51/0.79 fof(f497,plain,(
% 2.51/0.79 sk1=sk4|~sQ5_spl|~sQ2_spl),
% 2.51/0.79 inference(forward_demodulation,[status(thm)],[f495,f448])).
% 2.51/0.79 fof(f499,plain,(
% 2.51/0.79 ![X0]: (~ssList(X0)|segmentP(X0,sk1)|~sQ5_spl)),
% 2.51/0.79 inference(forward_demodulation,[status(thm)],[f495,f253])).
% 2.51/0.79 fof(f510,plain,(
% 2.51/0.79 ~segmentP(sk1,sk1)|~sQ5_spl|~sQ2_spl),
% 2.51/0.79 inference(forward_demodulation,[status(thm)],[f496,f435])).
% 2.51/0.79 fof(f511,plain,(
% 2.51/0.79 ~ssList(sk1)|~sQ2_spl|~sQ5_spl),
% 2.51/0.79 inference(resolution,[status(thm)],[f510,f499])).
% 2.51/0.79 fof(f513,plain,(
% 2.51/0.79 $false|~sQ2_spl|~sQ5_spl),
% 2.51/0.79 inference(forward_subsumption_resolution,[status(thm)],[f511,f428])).
% 2.51/0.79 fof(f514,plain,(
% 2.51/0.79 ~sQ2_spl|~sQ5_spl),
% 2.51/0.79 inference(contradiction_clause,[status(thm)],[f513])).
% 2.51/0.79 fof(f516,plain,(
% 2.51/0.79 frontsegP(sk4,sk1)|~sQ4_spl),
% 2.51/0.79 inference(forward_demodulation,[status(thm)],[f433,f455])).
% 2.51/0.79 fof(f518,plain,(
% 2.51/0.79 frontsegP(sk2,sk1)|~sQ4_spl),
% 2.51/0.79 inference(forward_demodulation,[status(thm)],[f432,f516])).
% 2.51/0.79 fof(f521,definition,(
% 2.51/0.79 sQ6_spl <=> (ssList(nil))),
% 2.51/0.79 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 2.51/0.79 fof(f523,plain,(
% 2.51/0.79 ~ssList(nil)|sQ6_spl),
% 2.51/0.79 inference(component_clause,[status(thm)],[f521])).
% 2.51/0.79 fof(f529,plain,(
% 2.51/0.79 $false|sQ6_spl),
% 2.51/0.79 inference(forward_subsumption_resolution,[status(thm)],[f523,f205])).
% 2.51/0.79 fof(f530,plain,(
% 2.51/0.79 sQ6_spl),
% 2.51/0.79 inference(contradiction_clause,[status(thm)],[f529])).
% 2.51/0.79 fof(f574,definition,(
% 2.51/0.79 sQ10_spl <=> (ssList(sk1))),
% 2.51/0.79 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 2.51/0.79 fof(f576,plain,(
% 2.51/0.79 ~ssList(sk1)|sQ10_spl),
% 2.51/0.79 inference(component_clause,[status(thm)],[f574])).
% 2.51/0.79 fof(f577,definition,(
% 2.51/0.79 sQ11_spl <=> (ssList(sk2))),
% 2.51/0.79 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 2.51/0.79 fof(f579,plain,(
% 2.51/0.79 ~ssList(sk2)|sQ11_spl),
% 2.51/0.79 inference(component_clause,[status(thm)],[f577])).
% 2.51/0.79 fof(f631,plain,(
% 2.51/0.79 $false|sQ11_spl),
% 2.51/0.79 inference(forward_subsumption_resolution,[status(thm)],[f429,f579])).
% 2.51/0.79 fof(f632,plain,(
% 2.51/0.79 sQ11_spl),
% 2.51/0.79 inference(contradiction_clause,[status(thm)],[f631])).
% 2.51/0.79 fof(f643,plain,(
% 2.51/0.79 $false|sQ10_spl),
% 2.51/0.79 inference(forward_subsumption_resolution,[status(thm)],[f576,f428])).
% 2.51/0.79 fof(f644,plain,(
% 2.51/0.79 sQ10_spl),
% 2.51/0.79 inference(contradiction_clause,[status(thm)],[f643])).
% 2.51/0.79 fof(f1174,plain,(
% 2.51/0.79 app(nil,sk1)=sk1),
% 2.51/0.79 inference(resolution,[status(thm)],[f272,f428])).
% 2.51/0.79 fof(f1262,plain,(
% 2.51/0.79 ![X0]: (~ssList(X0)|~ssList(nil)|~ssList(sk1)|~ssList(app(sk1,X0))|segmentP(app(app(nil,sk1),X0),sk1))),
% 2.51/0.79 inference(paramodulation,[status(thm)],[f1174,f481])).
% 2.51/0.79 fof(f1266,definition,(
% 2.51/0.79 ![X0]: (sQ62_spl <=> (~ssList(X0)|~ssList(app(sk1,X0))|segmentP(app(app(nil,sk1),X0),sk1)))),
% 2.51/0.79 introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition])).
% 2.51/0.79 fof(f1267,plain,(
% 2.51/0.79 ![X0]: (~ssList(X0)|~ssList(app(sk1,X0))|segmentP(app(app(nil,sk1),X0),sk1)|~sQ62_spl)),
% 2.51/0.79 inference(component_clause,[status(thm)],[f1266])).
% 2.51/0.79 fof(f1269,plain,(
% 2.51/0.79 sQ62_spl|~sQ6_spl|~sQ10_spl),
% 2.51/0.79 inference(split_clause,[status(thm)],[f1262,f1266,f521,f574])).
% 2.51/0.79 fof(f1282,plain,(
% 2.51/0.79 ![X0]: (~ssList(X0)|~ssList(app(sk1,X0))|segmentP(app(sk1,X0),sk1)|~sQ62_spl)),
% 2.51/0.79 inference(forward_demodulation,[status(thm)],[f1174,f1267])).
% 2.51/0.79 fof(f2667,plain,(
% 2.51/0.79 ![X0]: (~ssList(X0)|segmentP(app(sk1,X0),sk1)|~ssList(X0)|~ssList(sk1)|~sQ62_spl)),
% 2.51/0.79 inference(resolution,[status(thm)],[f1282,f283])).
% 2.51/0.81 fof(f2669,definition,(
% 2.51/0.81 ![X0]: (sQ169_spl <=> (~ssList(X0)|segmentP(app(sk1,X0),sk1)|~ssList(X0)))),
% 2.51/0.81 introduced(definition,[new_symbols(definition,[sQ169_spl])],[split_symbol_definition])).
% 2.51/0.81 fof(f2670,plain,(
% 2.51/0.81 ![X0]: (~ssList(X0)|segmentP(app(sk1,X0),sk1)|~ssList(X0)|~sQ169_spl)),
% 2.51/0.81 inference(component_clause,[status(thm)],[f2669])).
% 2.51/0.81 fof(f2672,plain,(
% 2.51/0.81 sQ169_spl|~sQ10_spl|~sQ62_spl),
% 2.51/0.81 inference(split_clause,[status(thm)],[f2667,f2669,f574,f1266])).
% 2.51/0.81 fof(f2677,plain,(
% 2.51/0.81 ![X0]: (~ssList(X0)|segmentP(app(sk1,X0),sk1)|~sQ169_spl)),
% 2.51/0.81 inference(duplicate_literals_removal,[status(thm)],[f2670])).
% 2.51/0.81 fof(f3583,plain,(
% 2.51/0.81 ~ssList(sk1)|~ssList(sk2)|app(sk1,skaf45(sk2,sk1))=sk2|~sQ4_spl),
% 2.51/0.81 inference(resolution,[status(thm)],[f342,f518])).
% 2.51/0.81 fof(f3610,definition,(
% 2.51/0.81 sQ222_spl <=> (app(sk1,skaf45(sk2,sk1))=sk2)),
% 2.51/0.81 introduced(definition,[new_symbols(definition,[sQ222_spl])],[split_symbol_definition])).
% 2.51/0.81 fof(f3611,plain,(
% 2.51/0.81 app(sk1,skaf45(sk2,sk1))=sk2|~sQ222_spl),
% 2.51/0.81 inference(component_clause,[status(thm)],[f3610])).
% 2.51/0.81 fof(f3613,plain,(
% 2.51/0.81 ~sQ10_spl|~sQ11_spl|sQ222_spl|~sQ4_spl),
% 2.51/0.81 inference(split_clause,[status(thm)],[f3583,f574,f577,f3610,f454])).
% 2.51/0.81 fof(f5328,plain,(
% 2.51/0.81 ~ssList(skaf45(sk2,sk1))|segmentP(sk2,sk1)|~sQ169_spl|~sQ222_spl),
% 2.51/0.81 inference(paramodulation,[status(thm)],[f3611,f2677])).
% 2.51/0.81 fof(f5340,definition,(
% 2.51/0.81 sQ400_spl <=> (ssList(skaf45(sk2,sk1)))),
% 2.51/0.81 introduced(definition,[new_symbols(definition,[sQ400_spl])],[split_symbol_definition])).
% 2.51/0.81 fof(f5342,plain,(
% 2.51/0.81 ~ssList(skaf45(sk2,sk1))|sQ400_spl),
% 2.51/0.81 inference(component_clause,[status(thm)],[f5340])).
% 2.51/0.81 fof(f5343,definition,(
% 2.51/0.81 sQ401_spl <=> (segmentP(sk2,sk1))),
% 2.51/0.81 introduced(definition,[new_symbols(definition,[sQ401_spl])],[split_symbol_definition])).
% 2.51/0.81 fof(f5344,plain,(
% 2.51/0.81 segmentP(sk2,sk1)|~sQ401_spl),
% 2.51/0.81 inference(component_clause,[status(thm)],[f5343])).
% 2.51/0.81 fof(f5346,plain,(
% 2.51/0.81 ~sQ400_spl|sQ401_spl|~sQ169_spl|~sQ222_spl),
% 2.51/0.81 inference(split_clause,[status(thm)],[f5328,f5340,f5343,f2669,f3610])).
% 2.51/0.81 fof(f5385,plain,(
% 2.51/0.81 $false|sQ400_spl),
% 2.51/0.81 inference(forward_subsumption_resolution,[status(thm)],[f5342,f248])).
% 2.51/0.81 fof(f5386,plain,(
% 2.51/0.81 sQ400_spl),
% 2.51/0.81 inference(contradiction_clause,[status(thm)],[f5385])).
% 2.51/0.81 fof(f5387,plain,(
% 2.51/0.81 $false|~sQ401_spl),
% 2.51/0.81 inference(forward_subsumption_resolution,[status(thm)],[f5344,f435])).
% 2.51/0.81 fof(f5388,plain,(
% 2.51/0.81 ~sQ401_spl),
% 2.51/0.81 inference(contradiction_clause,[status(thm)],[f5387])).
% 2.51/0.81 fof(f5389,plain,(
% 2.51/0.81 $false),
% 2.51/0.81 inference(sat_refutation,[status(thm)],[f457,f462,f514,f530,f632,f644,f1269,f2672,f3613,f5346,f5386,f5388])).
% 2.51/0.81 % SZS output end CNFRefutation for theBenchmark.p
% 2.51/0.81 % Elapsed time: 0.439450 seconds
% 2.51/0.81 % CPU time: 3.138089 seconds
% 2.51/0.81 % Total memory used: 170.422 MB
% 2.51/0.81 % Net memory used: 167.208 MB
%------------------------------------------------------------------------------