%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LCL902+1 : TPTP v9.3.1. Released v5.5.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n016.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:11:19 PM UTC 2026
% Result : Theorem 0.15s 0.59s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL902+1 : TPTP v9.3.1. Released v5.5.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.55 % Computer : n016.cluster.edu
% 0.11/0.55 % Model : x86_64 x86_64
% 0.11/0.55 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.55 % Memory : 8046.5625MB
% 0.11/0.55 % OS : Linux 6.8.0-71-generic
% 0.11/0.55 % CPULimit : 300
% 0.11/0.55 % WCLimit : 300
% 0.11/0.55 % DateTime : Mon Sep 21 01:15:38 UTC 2026
% 0.11/0.55 % CPUTime :
% 0.15/0.56 % Drodi V4.1.1
% 0.15/0.59 % Refutation found
% 0.15/0.59 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.15/0.59 % SZS output start CNFRefutation for theBenchmark
% 0.15/0.59 fof(f2,axiom,(
% 0.15/0.59 (! [A,B] : '+'(A,B) = '+'(B,A) )),
% 0.15/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.59 fof(f3,axiom,(
% 0.15/0.59 (! [A] : '+'(A,'0') = A )),
% 0.15/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.59 fof(f4,axiom,(
% 0.15/0.59 (! [A] : '>='(A,A) )),
% 0.15/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.59 fof(f6,axiom,(
% 0.15/0.59 (! [X3,X4] :( ( '>='(X3,X4)& '>='(X4,X3) )=> X3 = X4 ) )),
% 0.15/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.59 fof(f7,axiom,(
% 0.15/0.59 (! [X5,X6,X7] :( '>='('+'(X5,X6),X7)<=> '>='(X6,'==>'(X5,X7)) ) )),
% 0.15/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.59 fof(f8,axiom,(
% 0.15/0.59 (! [A] : '>='(A,'0') )),
% 0.15/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.59 fof(f11,axiom,(
% 0.15/0.59 (! [X14,X15,X16] :( '>='(X14,X15)=> '>='('==>'(X16,X14),'==>'(X16,X15)) ) )),
% 0.15/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.59 fof(f12,axiom,(
% 0.15/0.59 (! [A] : '+'(A,'1') = '1' )),
% 0.15/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.59 fof(f13,axiom,(
% 0.15/0.59 (! [A] : '==>'('==>'('==>'(A,'1'),A),A) = '0' )),
% 0.15/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.59 fof(f14,conjecture,(
% 0.15/0.59 (! [X17] : '==>'('==>'(X17,'1'),'1') = X17 )),
% 0.15/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.59 fof(f15,negated_conjecture,(
% 0.15/0.59 ~((! [X17] : '==>'('==>'(X17,'1'),'1') = X17 ))),
% 0.15/0.59 inference(negated_conjecture,[status(cth)],[f14])).
% 0.15/0.59 fof(f17,plain,(
% 0.15/0.59 ![X0,X1]: ('+'(X0,X1)='+'(X1,X0))),
% 0.15/0.59 inference(cnf_transformation,[status(thm)],[f2])).
% 0.15/0.59 fof(f18,plain,(
% 0.15/0.59 ![X0]: ('+'(X0,'0')=X0)),
% 0.15/0.59 inference(cnf_transformation,[status(thm)],[f3])).
% 0.15/0.59 fof(f19,plain,(
% 0.15/0.59 ![X0]: ('>='(X0,X0))),
% 0.15/0.59 inference(cnf_transformation,[status(thm)],[f4])).
% 0.15/0.59 fof(f23,plain,(
% 0.15/0.59 ![X3,X4]: ((~'>='(X3,X4)|~'>='(X4,X3))|X3=X4)),
% 0.15/0.59 inference(pre_NNF_transformation,[status(thm)],[f6])).
% 0.15/0.59 fof(f24,plain,(
% 0.15/0.59 ![X0,X1]: (~'>='(X0,X1)|~'>='(X1,X0)|X0=X1)),
% 0.15/0.59 inference(cnf_transformation,[status(thm)],[f23])).
% 0.15/0.59 fof(f25,plain,(
% 0.15/0.59 ![X5,X6,X7]: ((~'>='('+'(X5,X6),X7)|'>='(X6,'==>'(X5,X7)))&('>='('+'(X5,X6),X7)|~'>='(X6,'==>'(X5,X7))))),
% 0.15/0.59 inference(NNF_transformation,[status(thm)],[f7])).
% 0.15/0.59 fof(f26,plain,(
% 0.15/0.59 (![X5,X6,X7]: (~'>='('+'(X5,X6),X7)|'>='(X6,'==>'(X5,X7))))&(![X5,X6,X7]: ('>='('+'(X5,X6),X7)|~'>='(X6,'==>'(X5,X7))))),
% 0.15/0.59 inference(miniscoping,[status(thm)],[f25])).
% 0.15/0.59 fof(f27,plain,(
% 0.15/0.59 ![X0,X1,X2]: (~'>='('+'(X0,X1),X2)|'>='(X1,'==>'(X0,X2)))),
% 0.15/0.59 inference(cnf_transformation,[status(thm)],[f26])).
% 0.15/0.59 fof(f28,plain,(
% 0.15/0.59 ![X0,X1,X2]: ('>='('+'(X0,X1),X2)|~'>='(X1,'==>'(X0,X2)))),
% 0.15/0.59 inference(cnf_transformation,[status(thm)],[f26])).
% 0.15/0.59 fof(f29,plain,(
% 0.15/0.59 ![X0]: ('>='(X0,'0'))),
% 0.15/0.59 inference(cnf_transformation,[status(thm)],[f8])).
% 0.15/0.59 fof(f36,plain,(
% 0.15/0.59 ![X14,X15,X16]: (~'>='(X14,X15)|'>='('==>'(X16,X14),'==>'(X16,X15)))),
% 0.15/0.59 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 0.15/0.59 fof(f37,plain,(
% 0.15/0.59 ![X14,X15]: (~'>='(X14,X15)|(![X16]: '>='('==>'(X16,X14),'==>'(X16,X15))))),
% 0.15/0.59 inference(miniscoping,[status(thm)],[f36])).
% 0.15/0.59 fof(f38,plain,(
% 0.15/0.59 ![X0,X1,X2]: (~'>='(X0,X1)|'>='('==>'(X2,X0),'==>'(X2,X1)))),
% 0.15/0.59 inference(cnf_transformation,[status(thm)],[f37])).
% 0.15/0.59 fof(f39,plain,(
% 0.15/0.59 ![X0]: ('+'(X0,'1')='1')),
% 0.15/0.59 inference(cnf_transformation,[status(thm)],[f12])).
% 0.15/0.59 fof(f40,plain,(
% 0.15/0.59 ![X0]: ('==>'('==>'('==>'(X0,'1'),X0),X0)='0')),
% 0.15/0.59 inference(cnf_transformation,[status(thm)],[f13])).
% 0.15/0.59 fof(f41,plain,(
% 0.15/0.59 (?[X17]: ~'==>'('==>'(X17,'1'),'1')=X17)),
% 0.15/0.59 inference(pre_NNF_transformation,[status(thm)],[f15])).
% 0.15/0.59 fof(f42,plain,(
% 0.15/0.59 ~'==>'('==>'(sK0_skl,'1'),'1')=sK0_skl),
% 0.15/0.59 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(X17,sK0_skl)],[f41])).
% 0.15/0.59 fof(f43,plain,(
% 0.15/0.59 ~'==>'('==>'(sK0_skl,'1'),'1')=sK0_skl),
% 0.15/0.59 inference(cnf_transformation,[status(thm)],[f42])).
% 0.15/0.59 fof(f94,plain,(
% 0.15/0.59 ![X0]: (~'>='('0',X0)|'0'=X0)),
% 0.15/0.59 inference(resolution,[status(thm)],[f24,f29])).
% 0.15/0.59 fof(f102,plain,(
% 0.15/0.59 ![X0,X1]: ('>='(X0,'==>'(X1,'+'(X1,X0))))),
% 0.15/0.59 inference(resolution,[status(thm)],[f27,f19])).
% 0.15/0.59 fof(f125,plain,(
% 0.15/0.59 ![X0]: ('0'='==>'(X0,'+'(X0,'0')))),
% 0.15/0.59 inference(resolution,[status(thm)],[f102,f94])).
% 0.15/0.59 fof(f133,plain,(
% 0.15/0.59 ![X0,X1]: ('>='(X0,'==>'(X1,'+'(X0,X1))))),
% 0.15/0.59 inference(paramodulation,[status(thm)],[f17,f102])).
% 0.15/0.59 fof(f136,plain,(
% 0.15/0.59 ![X0]: ('0'='==>'(X0,X0))),
% 0.15/0.59 inference(forward_demodulation,[status(thm)],[f18,f125])).
% 0.15/0.59 fof(f141,plain,(
% 0.15/0.59 ![X0,X1]: ('>='('+'(X0,'==>'(X0,X1)),X1))),
% 0.15/0.59 inference(resolution,[status(thm)],[f28,f19])).
% 0.15/0.59 fof(f148,plain,(
% 0.15/0.59 ![X0,X1]: ('>='('+'(X0,X1),X0)|~'>='(X1,'0'))),
% 0.15/0.59 inference(paramodulation,[status(thm)],[f136,f28])).
% 0.15/0.59 fof(f149,plain,(
% 0.15/0.59 ![X0,X1]: ('>='('+'(X0,X1),X0))),
% 0.15/0.59 inference(forward_subsumption_resolution,[status(thm)],[f148,f29])).
% 0.15/0.59 fof(f157,plain,(
% 0.15/0.59 ![X0]: ('>='('1',X0))),
% 0.15/0.59 inference(paramodulation,[status(thm)],[f39,f149])).
% 0.15/0.59 fof(f159,plain,(
% 0.15/0.59 ![X0,X1]: ('>='('+'(X0,X1),X1))),
% 0.15/0.59 inference(paramodulation,[status(thm)],[f17,f149])).
% 0.15/0.59 fof(f165,plain,(
% 0.15/0.59 ![X0]: (~'>='(X0,'1')|X0='1')),
% 0.15/0.59 inference(resolution,[status(thm)],[f157,f24])).
% 0.15/0.59 fof(f167,plain,(
% 0.15/0.59 ![X0,X1]: ('>='(X0,'==>'(X1,X0)))),
% 0.15/0.59 inference(resolution,[status(thm)],[f159,f27])).
% 0.15/0.59 fof(f262,plain,(
% 0.15/0.59 ![X0]: ('+'(X0,'==>'(X0,'1'))='1')),
% 0.15/0.59 inference(resolution,[status(thm)],[f141,f165])).
% 0.15/0.59 fof(f272,plain,(
% 0.15/0.59 ![X0]: ('>='('+'('==>'('==>'(X0,'1'),X0),'0'),X0))),
% 0.15/0.59 inference(paramodulation,[status(thm)],[f40,f141])).
% 0.15/0.59 fof(f278,plain,(
% 0.15/0.59 ![X0]: ('>='('==>'('==>'(X0,'1'),X0),X0))),
% 0.15/0.59 inference(forward_demodulation,[status(thm)],[f18,f272])).
% 0.15/0.59 fof(f357,plain,(
% 0.15/0.59 ![X0]: ('>='(X0,'==>'('==>'(X0,'1'),'1')))),
% 0.15/0.59 inference(paramodulation,[status(thm)],[f262,f133])).
% 0.15/0.59 fof(f367,plain,(
% 0.15/0.59 ![X0,X1]: ('>='('==>'(X0,'1'),'==>'(X0,X1)))),
% 0.15/0.59 inference(resolution,[status(thm)],[f38,f157])).
% 0.15/0.59 fof(f587,plain,(
% 0.15/0.59 ![X0]: (~'>='(X0,'==>'('==>'(X0,'1'),X0))|X0='==>'('==>'(X0,'1'),X0))),
% 0.15/0.59 inference(resolution,[status(thm)],[f278,f24])).
% 0.15/0.59 fof(f607,plain,(
% 0.15/0.59 ![X0]: (X0='==>'('==>'(X0,'1'),X0))),
% 0.15/0.59 inference(forward_subsumption_resolution,[status(thm)],[f587,f167])).
% 0.15/0.59 fof(f638,plain,(
% 0.15/0.59 ![X0]: ('>='('==>'('==>'(X0,'1'),'1'),X0))),
% 0.15/0.59 inference(paramodulation,[status(thm)],[f607,f367])).
% 0.15/0.59 fof(f676,plain,(
% 0.15/0.59 ![X0]: (~'>='('==>'('==>'(X0,'1'),'1'),X0)|'==>'('==>'(X0,'1'),'1')=X0)),
% 0.15/0.59 inference(resolution,[status(thm)],[f357,f24])).
% 0.15/0.59 fof(f683,plain,(
% 0.15/0.59 ~sK0_skl=sK0_skl),
% 0.15/0.59 inference(backward_demodulation,[status(thm)],[f692,f43])).
% 0.15/0.59 fof(f692,plain,(
% 0.15/0.59 ![X0]: ('==>'('==>'(X0,'1'),'1')=X0)),
% 0.15/0.59 inference(forward_subsumption_resolution,[status(thm)],[f676,f638])).
% 0.15/0.59 fof(f698,plain,(
% 0.15/0.59 $false),
% 0.15/0.59 inference(trivial_equality_resolution,[status(thm)],[f683])).
% 0.15/0.59 % SZS output end CNFRefutation for theBenchmark.p
% 0.15/0.62 % Elapsed time: 0.059292 seconds
% 0.15/0.62 % CPU time: 0.234349 seconds
% 0.15/0.62 % Total memory used: 68.616 MB
% 0.15/0.62 % Net memory used: 68.097 MB
%------------------------------------------------------------------------------