%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LCL491+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n008.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:10:10 PM UTC 2026
% Result : Theorem 0.13s 5.42s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL491+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/5.37 % Computer : n008.cluster.edu
% 0.09/5.37 % Model : x86_64 x86_64
% 0.09/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.37 % Memory : 8046.5625MB
% 0.09/5.37 % OS : Linux 6.8.0-71-generic
% 0.09/5.37 % CPULimit : 300
% 0.09/5.37 % WCLimit : 300
% 0.09/5.37 % DateTime : Mon Sep 21 00:36:45 UTC 2026
% 0.09/5.37 % CPUTime :
% 0.09/5.39 % Drodi V4.1.1
% 0.13/5.42 % Refutation found
% 0.13/5.42 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.13/5.42 % SZS output start CNFRefutation for theBenchmark
% 0.13/5.42 fof(f11,axiom,(
% 0.13/5.42 ( or_2<=> (! [X,Y] : is_a_theorem(implies(Y,or(X,Y))) )) ),
% 0.13/5.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.42 fof(f23,axiom,(
% 0.13/5.42 ( r2<=> (! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) )) ),
% 0.13/5.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.42 fof(f37,axiom,(
% 0.13/5.42 r2 ),
% 0.13/5.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.42 fof(f45,conjecture,(
% 0.13/5.42 or_2 ),
% 0.13/5.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.42 fof(f46,negated_conjecture,(
% 0.13/5.42 ~(or_2 )),
% 0.13/5.42 inference(negated_conjecture,[status(cth)],[f45])).
% 0.13/5.42 fof(f93,plain,(
% 0.13/5.42 (~or_2|(![X,Y]: is_a_theorem(implies(Y,or(X,Y)))))&(or_2|(?[X,Y]: ~is_a_theorem(implies(Y,or(X,Y)))))),
% 0.13/5.42 inference(NNF_transformation,[status(thm)],[f11])).
% 0.13/5.42 fof(f94,plain,(
% 0.13/5.42 (~or_2|(![X,Y]: is_a_theorem(implies(Y,or(X,Y)))))&(or_2|~is_a_theorem(implies(sK22_skl,or(sK21_skl,sK22_skl))))),
% 0.13/5.42 inference(skolemize,[status(esa),new_symbols(skolem,[sK21_skl,sK22_skl]),skolemize(X,sK21_skl),skolemize(Y,sK22_skl)],[f93])).
% 0.13/5.42 fof(f96,plain,(
% 0.13/5.42 or_2|~is_a_theorem(implies(sK22_skl,or(sK21_skl,sK22_skl)))),
% 0.13/5.42 inference(cnf_transformation,[status(thm)],[f94])).
% 0.13/5.42 fof(f141,plain,(
% 0.13/5.42 (~r2|(![P,Q]: is_a_theorem(implies(Q,or(P,Q)))))&(r2|(?[P,Q]: ~is_a_theorem(implies(Q,or(P,Q)))))),
% 0.13/5.42 inference(NNF_transformation,[status(thm)],[f23])).
% 0.13/5.42 fof(f142,plain,(
% 0.13/5.42 (~r2|(![P,Q]: is_a_theorem(implies(Q,or(P,Q)))))&(r2|~is_a_theorem(implies(sK46_skl,or(sK45_skl,sK46_skl))))),
% 0.13/5.42 inference(skolemize,[status(esa),new_symbols(skolem,[sK45_skl,sK46_skl]),skolemize(P,sK45_skl),skolemize(Q,sK46_skl)],[f141])).
% 0.13/5.42 fof(f143,plain,(
% 0.13/5.42 ![X0,X1]: (~r2|is_a_theorem(implies(X0,or(X1,X0))))),
% 0.13/5.42 inference(cnf_transformation,[status(thm)],[f142])).
% 0.13/5.42 fof(f172,plain,(
% 0.13/5.42 r2),
% 0.13/5.42 inference(cnf_transformation,[status(thm)],[f37])).
% 0.13/5.42 fof(f180,plain,(
% 0.13/5.42 ~or_2),
% 0.13/5.42 inference(cnf_transformation,[status(thm)],[f46])).
% 0.13/5.42 fof(f185,plain,(
% 0.13/5.42 ~is_a_theorem(implies(sK22_skl,or(sK21_skl,sK22_skl)))),
% 0.13/5.42 inference(forward_subsumption_resolution,[status(thm)],[f96,f180])).
% 0.13/5.42 fof(f188,plain,(
% 0.13/5.42 ![X0,X1]: (is_a_theorem(implies(X0,or(X1,X0))))),
% 0.13/5.42 inference(forward_subsumption_resolution,[status(thm)],[f143,f172])).
% 0.13/5.42 fof(f189,plain,(
% 0.13/5.42 $false),
% 0.13/5.42 inference(backward_subsumption_resolution,[status(thm)],[f185,f188])).
% 0.13/5.42 % SZS output end CNFRefutation for theBenchmark.p
% 0.13/5.45 % Elapsed time: 0.062679 seconds
% 0.13/5.45 % CPU time: 0.151449 seconds
% 0.13/5.45 % Total memory used: 82.932 MB
% 0.13/5.45 % Net memory used: 82.890 MB
%------------------------------------------------------------------------------