%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LCL144-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n010.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 01:09:26 PM UTC 2026
% Result : Unsatisfiable 5.59s 1.12s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL144-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n010.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 00:07:25 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.38 % Drodi V4.1.1
% 5.59/1.12 % Refutation found
% 5.59/1.12 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 5.59/1.12 % SZS output start CNFRefutation for theBenchmark
% 5.59/1.12 fof(f1,axiom,(
% 5.59/1.12 (![X]: (implies(truth,X) = X ))),
% 5.59/1.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.59/1.12 fof(f2,axiom,(
% 5.59/1.12 (![X,Y,Z]: (implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z))) = truth ))),
% 5.59/1.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.59/1.12 fof(f3,axiom,(
% 5.59/1.12 (![X,Y]: (implies(implies(X,Y),Y) = implies(implies(Y,X),X) ))),
% 5.59/1.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.59/1.12 fof(f5,axiom,(
% 5.59/1.12 (![X,Y]: (big_V(X,Y) = implies(implies(X,Y),Y) ))),
% 5.59/1.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.59/1.12 fof(f7,axiom,(
% 5.59/1.12 (![X,Y]: (( ~ ordered(X,Y)| implies(X,Y) = truth ) ))),
% 5.59/1.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.59/1.12 fof(f8,axiom,(
% 5.59/1.12 (![X,Y]: (( implies(X,Y) != truth| ordered(X,Y) ) ))),
% 5.59/1.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.59/1.12 fof(f9,negated_conjecture,(
% 5.59/1.12 ( ordered(x,implies(y,z))| ordered(y,implies(x,z)) ) ),
% 5.59/1.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.59/1.12 fof(f10,negated_conjecture,(
% 5.59/1.12 ( ~ ordered(x,implies(y,z))| ~ ordered(y,implies(x,z)) ) ),
% 5.59/1.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.59/1.12 fof(f11,plain,(
% 5.59/1.12 ![X0]: (implies(truth,X0)=X0)),
% 5.59/1.12 inference(cnf_transformation,[status(thm)],[f1])).
% 5.59/1.12 fof(f12,plain,(
% 5.59/1.12 ![X0,X1,X2]: (implies(implies(X0,X1),implies(implies(X1,X2),implies(X0,X2)))=truth)),
% 5.59/1.12 inference(cnf_transformation,[status(thm)],[f2])).
% 5.59/1.12 fof(f13,plain,(
% 5.59/1.12 ![X0,X1]: (implies(implies(X0,X1),X1)=implies(implies(X1,X0),X0))),
% 5.59/1.12 inference(cnf_transformation,[status(thm)],[f3])).
% 5.59/1.12 fof(f15,plain,(
% 5.59/1.12 ![X0,X1]: (big_V(X0,X1)=implies(implies(X0,X1),X1))),
% 5.59/1.12 inference(cnf_transformation,[status(thm)],[f5])).
% 5.59/1.12 fof(f17,plain,(
% 5.59/1.12 ![X0,X1]: (~ordered(X0,X1)|implies(X0,X1)=truth)),
% 5.59/1.12 inference(cnf_transformation,[status(thm)],[f7])).
% 5.59/1.12 fof(f18,plain,(
% 5.59/1.12 ![X0,X1]: (~implies(X0,X1)=truth|ordered(X0,X1))),
% 5.59/1.12 inference(cnf_transformation,[status(thm)],[f8])).
% 5.59/1.12 fof(f19,plain,(
% 5.59/1.12 ordered(x,implies(y,z))|ordered(y,implies(x,z))),
% 5.59/1.12 inference(cnf_transformation,[status(thm)],[f9])).
% 5.59/1.12 fof(f20,plain,(
% 5.59/1.12 ~ordered(x,implies(y,z))|~ordered(y,implies(x,z))),
% 5.59/1.12 inference(cnf_transformation,[status(thm)],[f10])).
% 5.59/1.12 fof(f21,definition,(
% 5.59/1.12 sQ0_spl <=> (ordered(x,implies(y,z)))),
% 5.59/1.12 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 5.59/1.12 fof(f22,plain,(
% 5.59/1.12 ordered(x,implies(y,z))|~sQ0_spl),
% 5.59/1.12 inference(component_clause,[status(thm)],[f21])).
% 5.59/1.12 fof(f23,plain,(
% 5.59/1.12 ~ordered(x,implies(y,z))|sQ0_spl),
% 5.59/1.12 inference(component_clause,[status(thm)],[f21])).
% 5.59/1.12 fof(f24,definition,(
% 5.59/1.12 sQ1_spl <=> (ordered(y,implies(x,z)))),
% 5.59/1.12 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 5.59/1.12 fof(f25,plain,(
% 5.59/1.12 ordered(y,implies(x,z))|~sQ1_spl),
% 5.59/1.12 inference(component_clause,[status(thm)],[f24])).
% 5.59/1.12 fof(f26,plain,(
% 5.59/1.12 ~ordered(y,implies(x,z))|sQ1_spl),
% 5.59/1.12 inference(component_clause,[status(thm)],[f24])).
% 5.59/1.12 fof(f27,plain,(
% 5.59/1.12 sQ0_spl|sQ1_spl),
% 5.59/1.12 inference(split_clause,[status(thm)],[f19,f21,f24])).
% 5.59/1.12 fof(f28,plain,(
% 5.59/1.12 ~sQ0_spl|~sQ1_spl),
% 5.59/1.12 inference(split_clause,[status(thm)],[f20,f21,f24])).
% 5.59/1.12 fof(f145,plain,(
% 5.59/1.12 implies(y,implies(x,z))=truth|~sQ1_spl),
% 5.59/1.12 inference(resolution,[status(thm)],[f17,f25])).
% 5.59/1.12 fof(f146,plain,(
% 5.59/1.12 ~implies(x,implies(y,z))=truth|sQ0_spl),
% 5.59/1.12 inference(resolution,[status(thm)],[f18,f23])).
% 5.59/1.12 fof(f151,plain,(
% 5.59/1.12 ![X0,X1]: (implies(implies(X0,X1),X1)=big_V(X1,X0))),
% 5.59/1.12 inference(backward_demodulation,[status(thm)],[f15,f13])).
% 5.59/1.12 fof(f176,plain,(
% 5.59/1.12 ![X0,X1]: (implies(X0,implies(implies(X0,X1),implies(truth,X1)))=truth)),
% 5.59/1.12 inference(paramodulation,[status(thm)],[f11,f12])).
% 5.59/1.12 fof(f186,plain,(
% 5.59/1.12 ![X0,X1,X2]: (implies(implies(X0,implies(X1,X2)),implies(big_V(X1,X2),implies(X0,X2)))=truth)),
% 5.59/1.12 inference(paramodulation,[status(thm)],[f15,f12])).
% 5.59/1.12 fof(f195,plain,(
% 5.59/1.12 ![X0,X1]: (implies(X0,implies(implies(X0,X1),X1))=truth)),
% 5.59/1.12 inference(forward_demodulation,[status(thm)],[f11,f176])).
% 5.59/1.12 fof(f196,plain,(
% 5.59/1.12 ![X0,X1]: (implies(X0,big_V(X0,X1))=truth)),
% 5.59/1.12 inference(forward_demodulation,[status(thm)],[f15,f195])).
% 5.59/1.14 fof(f234,plain,(
% 5.59/1.14 ![X0]: (implies(truth,implies(implies(implies(x,z),X0),implies(y,X0)))=truth|~sQ1_spl)),
% 5.59/1.14 inference(paramodulation,[status(thm)],[f145,f12])).
% 5.59/1.14 fof(f237,plain,(
% 5.59/1.14 ![X0]: (implies(implies(implies(x,z),X0),implies(y,X0))=truth|~sQ1_spl)),
% 5.59/1.14 inference(forward_demodulation,[status(thm)],[f11,f234])).
% 5.59/1.14 fof(f249,plain,(
% 5.59/1.14 ![X0,X1]: (big_V(X0,X1)=big_V(X1,X0))),
% 5.59/1.14 inference(paramodulation,[status(thm)],[f15,f151])).
% 5.59/1.14 fof(f254,plain,(
% 5.59/1.14 ![X0,X1,X2]: (implies(truth,implies(implies(X0,X1),implies(X2,X1)))=big_V(implies(implies(X0,X1),implies(X2,X1)),implies(X2,X0)))),
% 5.59/1.14 inference(paramodulation,[status(thm)],[f12,f151])).
% 5.59/1.14 fof(f268,plain,(
% 5.59/1.14 ![X0,X1,X2]: (implies(implies(X0,X1),implies(X2,X1))=big_V(implies(implies(X0,X1),implies(X2,X1)),implies(X2,X0)))),
% 5.59/1.14 inference(forward_demodulation,[status(thm)],[f11,f254])).
% 5.59/1.14 fof(f422,plain,(
% 5.59/1.14 ![X0]: (big_V(truth,X0)=truth)),
% 5.59/1.14 inference(paramodulation,[status(thm)],[f11,f196])).
% 5.59/1.14 fof(f430,plain,(
% 5.59/1.14 ![X0,X1,X2]: (implies(implies(big_V(X0,X1),X2),implies(X0,X2))=big_V(implies(implies(big_V(X0,X1),X2),implies(X0,X2)),truth))),
% 5.59/1.14 inference(paramodulation,[status(thm)],[f196,f268])).
% 5.59/1.14 fof(f454,plain,(
% 5.59/1.14 ![X0]: (big_V(X0,truth)=truth)),
% 5.59/1.14 inference(paramodulation,[status(thm)],[f249,f422])).
% 5.59/1.14 fof(f1482,plain,(
% 5.59/1.14 implies(big_V(x,z),implies(y,z))=truth|~sQ1_spl),
% 5.59/1.14 inference(paramodulation,[status(thm)],[f15,f237])).
% 5.59/1.14 fof(f17670,plain,(
% 5.59/1.14 ![X0,X1,X2]: (implies(implies(big_V(X0,X1),X2),implies(X0,X2))=truth)),
% 5.59/1.14 inference(forward_demodulation,[status(thm)],[f454,f430])).
% 5.59/1.14 fof(f17672,plain,(
% 5.59/1.14 implies(truth,implies(x,implies(y,z)))=truth|~sQ1_spl),
% 5.59/1.14 inference(paramodulation,[status(thm)],[f1482,f17670])).
% 5.59/1.14 fof(f17882,plain,(
% 5.59/1.14 implies(x,implies(y,z))=truth|~sQ1_spl),
% 5.59/1.14 inference(forward_demodulation,[status(thm)],[f11,f17672])).
% 5.59/1.14 fof(f17883,plain,(
% 5.59/1.14 $false|sQ0_spl|~sQ1_spl),
% 5.59/1.14 inference(forward_subsumption_resolution,[status(thm)],[f17882,f146])).
% 5.59/1.14 fof(f17884,plain,(
% 5.59/1.14 sQ0_spl|~sQ1_spl),
% 5.59/1.14 inference(contradiction_clause,[status(thm)],[f17883])).
% 5.59/1.14 fof(f18040,plain,(
% 5.59/1.14 implies(x,implies(y,z))=truth|~sQ0_spl),
% 5.59/1.14 inference(resolution,[status(thm)],[f22,f17])).
% 5.59/1.14 fof(f18041,plain,(
% 5.59/1.14 ~implies(y,implies(x,z))=truth|sQ1_spl),
% 5.59/1.14 inference(resolution,[status(thm)],[f26,f18])).
% 5.59/1.14 fof(f18048,plain,(
% 5.59/1.14 implies(truth,implies(big_V(y,z),implies(x,z)))=truth|~sQ0_spl),
% 5.59/1.14 inference(paramodulation,[status(thm)],[f18040,f186])).
% 5.59/1.14 fof(f18116,plain,(
% 5.59/1.14 implies(big_V(y,z),implies(x,z))=truth|~sQ0_spl),
% 5.59/1.14 inference(forward_demodulation,[status(thm)],[f11,f18048])).
% 5.59/1.14 fof(f22305,plain,(
% 5.59/1.14 implies(truth,implies(y,implies(x,z)))=truth|~sQ0_spl),
% 5.59/1.14 inference(paramodulation,[status(thm)],[f18116,f17670])).
% 5.59/1.14 fof(f22382,plain,(
% 5.59/1.14 implies(y,implies(x,z))=truth|~sQ0_spl),
% 5.59/1.14 inference(forward_demodulation,[status(thm)],[f11,f22305])).
% 5.59/1.14 fof(f22383,plain,(
% 5.59/1.14 $false|sQ1_spl|~sQ0_spl),
% 5.59/1.14 inference(forward_subsumption_resolution,[status(thm)],[f22382,f18041])).
% 5.59/1.14 fof(f22384,plain,(
% 5.59/1.14 sQ1_spl|~sQ0_spl),
% 5.59/1.14 inference(contradiction_clause,[status(thm)],[f22383])).
% 5.59/1.14 fof(f22385,plain,(
% 5.59/1.14 $false),
% 5.59/1.14 inference(sat_refutation,[status(thm)],[f27,f28,f17884,f22384])).
% 5.59/1.14 % SZS output end CNFRefutation for theBenchmark.p
% 5.59/1.15 % Elapsed time: 0.774703 seconds
% 5.59/1.15 % CPU time: 5.876210 seconds
% 5.59/1.15 % Total memory used: 224.753 MB
% 5.59/1.15 % Net memory used: 219.667 MB
%------------------------------------------------------------------------------