%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LCL239-10 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n020.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:07:16 PM UTC 2026
% Result : Unsatisfiable 0.17s 5.96s
% Output : CNFRefutation 0.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 14
% Syntax : Number of formulae : 96 ( 96 unt; 4 def)
% Number of atoms : 96 ( 95 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 3 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 6 con; 0-4 aty)
% Number of variables : 157 ( 157 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,B,C] : ifeq(A,A,B,C) = B,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [A] : axiom(implies(or(A,A),A)) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [A,B] : axiom(implies(A,or(B,A))) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [A,B] : axiom(implies(or(A,B),or(B,A))) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [A,B,C] : axiom(implies(or(A,or(B,C)),or(B,or(A,C)))) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [X,Y] : implies(X,Y) = or(not(X),Y),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [X] : ifeq(axiom(X),true,theorem(X),true) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [Y,X] : ifeq(theorem(implies(Y,X)),true,ifeq(theorem(Y),true,theorem(X),true),true) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [P,Q] : and(P,Q) = not(or(not(P),not(Q))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11,negated_conjecture,
theorem(not(and(p,not(p)))) != true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12,plain,
! [X0,X1,X2] : ifeq(X0,X0,X1,X2) = X1,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f13,plain,
! [X0] : axiom(implies(or(X0,X0),X0)) = true,
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f14,plain,
! [X0,X1] : axiom(implies(X0,or(X1,X0))) = true,
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f15,plain,
! [X0,X1] : axiom(implies(or(X0,X1),or(X1,X0))) = true,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f16,plain,
! [X0,X1,X2] : axiom(implies(or(X0,or(X1,X2)),or(X1,or(X0,X2)))) = true,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f18,plain,
! [X0,X1] : implies(X0,X1) = or(not(X0),X1),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f19,plain,
! [X0] : ifeq(axiom(X0),true,theorem(X0),true) = true,
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f20,plain,
! [X0,X1] : ifeq(theorem(implies(X0,X1)),true,ifeq(theorem(X0),true,theorem(X1),true),true) = true,
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f21,plain,
! [X0,X1] : and(X0,X1) = not(or(not(X0),not(X1))),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f22,plain,
theorem(not(and(p,not(p)))) != true,
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f23,definition,
sF3_fnc = not(p),
introduced(definition,[new_symbols(definition,[sF3_fnc])],[function_definition]) ).
fof(f24,definition,
sF2_fnc = and(p,sF3_fnc),
introduced(definition,[new_symbols(definition,[sF2_fnc])],[function_definition]) ).
fof(f25,definition,
sF1_fnc = not(sF2_fnc),
introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition]) ).
fof(f26,definition,
sF0_fnc = theorem(sF1_fnc),
introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition]) ).
fof(f27,plain,
sF0_fnc != true,
inference(definition_folding,[],[f22,f26,f25,f24,f23]) ).
fof(f28,plain,
! [X0] : implies(sF2_fnc,X0) = or(sF1_fnc,X0),
inference(paramodulation,[status(thm)],[f25,f18]) ).
fof(f29,plain,
! [X0] : implies(p,X0) = or(sF3_fnc,X0),
inference(paramodulation,[status(thm)],[f23,f18]) ).
fof(f30,plain,
! [X0,X1] : and(X0,X1) = not(implies(X0,not(X1))),
inference(forward_demodulation,[status(thm)],[f18,f21]) ).
fof(f34,plain,
! [X0,X1,X2] : implies(implies(X0,not(X1)),X2) = or(and(X0,X1),X2),
inference(paramodulation,[status(thm)],[f30,f18]) ).
fof(f79,plain,
! [X0,X1] : axiom(implies(implies(X0,X1),or(X1,not(X0)))) = true,
inference(paramodulation,[status(thm)],[f18,f15]) ).
fof(f85,plain,
! [X0,X1] : ifeq(true,true,theorem(implies(or(X0,X1),or(X1,X0))),true) = true,
inference(paramodulation,[status(thm)],[f15,f19]) ).
fof(f86,plain,
! [X0] : ifeq(true,true,theorem(implies(or(X0,X0),X0)),true) = true,
inference(paramodulation,[status(thm)],[f13,f19]) ).
fof(f88,plain,
! [X0,X1] : ifeq(true,true,theorem(implies(X0,or(X1,X0))),true) = true,
inference(paramodulation,[status(thm)],[f14,f19]) ).
fof(f91,plain,
! [X0,X1] : theorem(implies(or(X0,X1),or(X1,X0))) = true,
inference(forward_demodulation,[status(thm)],[f12,f85]) ).
fof(f92,plain,
! [X0] : theorem(implies(or(X0,X0),X0)) = true,
inference(forward_demodulation,[status(thm)],[f12,f86]) ).
fof(f94,plain,
! [X0,X1] : theorem(implies(X0,or(X1,X0))) = true,
inference(forward_demodulation,[status(thm)],[f12,f88]) ).
fof(f129,plain,
! [X0,X1,X2] : ifeq(true,true,theorem(implies(or(X0,or(X1,X2)),or(X1,or(X0,X2)))),true) = true,
inference(paramodulation,[status(thm)],[f16,f19]) ).
fof(f146,plain,
! [X0,X1,X2] : theorem(implies(or(X0,or(X1,X2)),or(X1,or(X0,X2)))) = true,
inference(forward_demodulation,[status(thm)],[f12,f129]) ).
fof(f167,plain,
! [X0] : ifeq(true,true,ifeq(theorem(or(X0,X0)),true,theorem(X0),true),true) = true,
inference(paramodulation,[status(thm)],[f92,f20]) ).
fof(f168,plain,
! [X0,X1] : ifeq(true,true,ifeq(theorem(X0),true,theorem(or(X1,X0)),true),true) = true,
inference(paramodulation,[status(thm)],[f94,f20]) ).
fof(f172,plain,
! [X0,X1,X2] : ifeq(theorem(implies(implies(X0,or(X1,X0)),X2)),true,ifeq(true,true,theorem(X2),true),true) = true,
inference(paramodulation,[status(thm)],[f94,f20]) ).
fof(f178,plain,
! [X0] : ifeq(theorem(implies(X0,sF1_fnc)),true,ifeq(theorem(X0),true,sF0_fnc,true),true) = true,
inference(paramodulation,[status(thm)],[f26,f20]) ).
fof(f179,plain,
! [X0] : ifeq(theorem(or(X0,X0)),true,theorem(X0),true) = true,
inference(forward_demodulation,[status(thm)],[f12,f167]) ).
fof(f180,plain,
! [X0,X1] : ifeq(theorem(X0),true,theorem(or(X1,X0)),true) = true,
inference(forward_demodulation,[status(thm)],[f12,f168]) ).
fof(f183,plain,
! [X0,X1,X2] : ifeq(theorem(implies(implies(X0,or(X1,X0)),X2)),true,theorem(X2),true) = true,
inference(forward_demodulation,[status(thm)],[f12,f172]) ).
fof(f232,plain,
! [X0,X1] : ifeq(true,true,theorem(implies(implies(X0,X1),or(X1,not(X0)))),true) = true,
inference(paramodulation,[status(thm)],[f79,f19]) ).
fof(f237,plain,
! [X0,X1] : theorem(implies(implies(X0,X1),or(X1,not(X0)))) = true,
inference(forward_demodulation,[status(thm)],[f12,f232]) ).
fof(f259,plain,
! [X0] : theorem(implies(implies(sF2_fnc,X0),or(X0,sF1_fnc))) = true,
inference(paramodulation,[status(thm)],[f28,f91]) ).
fof(f265,plain,
! [X0,X1] : ifeq(true,true,ifeq(theorem(or(X0,X1)),true,theorem(or(X1,X0)),true),true) = true,
inference(paramodulation,[status(thm)],[f91,f20]) ).
fof(f269,plain,
! [X0,X1] : ifeq(theorem(or(X0,X1)),true,theorem(or(X1,X0)),true) = true,
inference(forward_demodulation,[status(thm)],[f12,f265]) ).
fof(f586,plain,
! [X0,X1,X2] : ifeq(true,true,ifeq(theorem(or(X0,or(X1,X2))),true,theorem(or(X1,or(X0,X2))),true),true) = true,
inference(paramodulation,[status(thm)],[f146,f20]) ).
fof(f611,plain,
! [X0,X1,X2] : ifeq(theorem(or(X0,or(X1,X2))),true,theorem(or(X1,or(X0,X2))),true) = true,
inference(forward_demodulation,[status(thm)],[f12,f586]) ).
fof(f648,plain,
! [X0,X1] : ifeq(theorem(or(and(X0,X1),sF1_fnc)),true,ifeq(theorem(implies(X0,not(X1))),true,sF0_fnc,true),true) = true,
inference(paramodulation,[status(thm)],[f34,f178]) ).
fof(f3611,plain,
! [X0] : ifeq(true,true,theorem(or(or(X0,sF2_fnc),sF1_fnc)),true) = true,
inference(paramodulation,[status(thm)],[f259,f183]) ).
fof(f3614,plain,
! [X0,X1] : ifeq(true,true,theorem(or(or(X0,X1),not(X1))),true) = true,
inference(paramodulation,[status(thm)],[f237,f183]) ).
fof(f3699,plain,
! [X0] : theorem(or(or(X0,sF2_fnc),sF1_fnc)) = true,
inference(forward_demodulation,[status(thm)],[f12,f3611]) ).
fof(f3702,plain,
! [X0,X1] : theorem(or(or(X0,X1),not(X1))) = true,
inference(forward_demodulation,[status(thm)],[f12,f3614]) ).
fof(f3733,plain,
! [X0,X1] : ifeq(true,true,theorem(or(X0,or(or(X1,sF2_fnc),sF1_fnc))),true) = true,
inference(paramodulation,[status(thm)],[f3699,f180]) ).
fof(f3743,plain,
! [X0,X1] : theorem(or(X0,or(or(X1,sF2_fnc),sF1_fnc))) = true,
inference(forward_demodulation,[status(thm)],[f12,f3733]) ).
fof(f3992,plain,
! [X0,X1,X2] : ifeq(true,true,theorem(or(X0,or(or(X1,X2),not(X2)))),true) = true,
inference(paramodulation,[status(thm)],[f3702,f180]) ).
fof(f4002,plain,
! [X0,X1,X2] : theorem(or(X0,or(or(X1,X2),not(X2)))) = true,
inference(forward_demodulation,[status(thm)],[f12,f3992]) ).
fof(f11552,plain,
! [X0,X1] : ifeq(true,true,theorem(or(or(X0,sF2_fnc),or(X1,sF1_fnc))),true) = true,
inference(paramodulation,[status(thm)],[f3743,f611]) ).
fof(f11553,plain,
! [X0,X1,X2] : ifeq(true,true,theorem(or(or(X0,X1),or(X2,not(X1)))),true) = true,
inference(paramodulation,[status(thm)],[f4002,f611]) ).
fof(f11678,plain,
! [X0,X1] : theorem(or(or(X0,sF2_fnc),or(X1,sF1_fnc))) = true,
inference(forward_demodulation,[status(thm)],[f12,f11552]) ).
fof(f11679,plain,
! [X0,X1,X2] : theorem(or(or(X0,X1),or(X2,not(X1)))) = true,
inference(forward_demodulation,[status(thm)],[f12,f11553]) ).
fof(f11921,plain,
! [X0,X1] : ifeq(true,true,theorem(or(or(X0,sF1_fnc),or(X1,sF2_fnc))),true) = true,
inference(paramodulation,[status(thm)],[f11678,f269]) ).
fof(f11940,plain,
! [X0,X1] : theorem(or(or(X0,sF1_fnc),or(X1,sF2_fnc))) = true,
inference(forward_demodulation,[status(thm)],[f12,f11921]) ).
fof(f12110,plain,
! [X0,X1,X2] : ifeq(true,true,theorem(or(or(X0,not(X1)),or(X2,X1))),true) = true,
inference(paramodulation,[status(thm)],[f11679,f269]) ).
fof(f12129,plain,
! [X0,X1,X2] : theorem(or(or(X0,not(X1)),or(X2,X1))) = true,
inference(forward_demodulation,[status(thm)],[f12,f12110]) ).
fof(f13123,plain,
! [X0,X1] : ifeq(true,true,theorem(or(X0,or(or(X1,sF1_fnc),sF2_fnc))),true) = true,
inference(paramodulation,[status(thm)],[f11940,f611]) ).
fof(f13143,plain,
! [X0,X1] : theorem(or(X0,or(or(X1,sF1_fnc),sF2_fnc))) = true,
inference(forward_demodulation,[status(thm)],[f12,f13123]) ).
fof(f13899,plain,
! [X0,X1,X2] : ifeq(true,true,theorem(or(X0,or(or(X1,not(X2)),X2))),true) = true,
inference(paramodulation,[status(thm)],[f12129,f611]) ).
fof(f13920,plain,
! [X0,X1,X2] : theorem(or(X0,or(or(X1,not(X2)),X2))) = true,
inference(forward_demodulation,[status(thm)],[f12,f13899]) ).
fof(f15427,plain,
! [X0] : ifeq(true,true,theorem(or(or(X0,sF1_fnc),sF2_fnc)),true) = true,
inference(paramodulation,[status(thm)],[f13143,f179]) ).
fof(f15448,plain,
! [X0] : theorem(or(or(X0,sF1_fnc),sF2_fnc)) = true,
inference(forward_demodulation,[status(thm)],[f12,f15427]) ).
fof(f15474,plain,
! [X0] : ifeq(true,true,theorem(or(sF2_fnc,or(X0,sF1_fnc))),true) = true,
inference(paramodulation,[status(thm)],[f15448,f269]) ).
fof(f15493,plain,
! [X0] : theorem(or(sF2_fnc,or(X0,sF1_fnc))) = true,
inference(forward_demodulation,[status(thm)],[f12,f15474]) ).
fof(f15562,plain,
! [X0] : ifeq(true,true,theorem(or(X0,or(sF2_fnc,sF1_fnc))),true) = true,
inference(paramodulation,[status(thm)],[f15493,f611]) ).
fof(f15583,plain,
! [X0] : theorem(or(X0,or(sF2_fnc,sF1_fnc))) = true,
inference(forward_demodulation,[status(thm)],[f12,f15562]) ).
fof(f15835,plain,
ifeq(true,true,theorem(or(sF2_fnc,sF1_fnc)),true) = true,
inference(paramodulation,[status(thm)],[f15583,f179]) ).
fof(f15856,plain,
theorem(or(sF2_fnc,sF1_fnc)) = true,
inference(forward_demodulation,[status(thm)],[f12,f15835]) ).
fof(f17107,plain,
! [X0,X1] : ifeq(true,true,theorem(or(or(X0,not(X1)),X1)),true) = true,
inference(paramodulation,[status(thm)],[f13920,f179]) ).
fof(f17129,plain,
! [X0,X1] : theorem(or(or(X0,not(X1)),X1)) = true,
inference(forward_demodulation,[status(thm)],[f12,f17107]) ).
fof(f17237,plain,
! [X0,X1] : ifeq(true,true,theorem(or(X0,or(X1,not(X0)))),true) = true,
inference(paramodulation,[status(thm)],[f17129,f269]) ).
fof(f17258,plain,
! [X0,X1] : theorem(or(X0,or(X1,not(X0)))) = true,
inference(forward_demodulation,[status(thm)],[f12,f17237]) ).
fof(f17486,plain,
! [X0,X1] : ifeq(true,true,theorem(or(X0,or(X1,not(X1)))),true) = true,
inference(paramodulation,[status(thm)],[f17258,f611]) ).
fof(f17509,plain,
! [X0,X1] : theorem(or(X0,or(X1,not(X1)))) = true,
inference(forward_demodulation,[status(thm)],[f12,f17486]) ).
fof(f17758,plain,
! [X0] : ifeq(true,true,theorem(or(X0,not(X0))),true) = true,
inference(paramodulation,[status(thm)],[f17509,f179]) ).
fof(f17780,plain,
! [X0] : theorem(or(X0,not(X0))) = true,
inference(forward_demodulation,[status(thm)],[f12,f17758]) ).
fof(f17825,plain,
theorem(implies(p,not(sF3_fnc))) = true,
inference(paramodulation,[status(thm)],[f29,f17780]) ).
fof(f17901,plain,
ifeq(theorem(or(and(p,sF3_fnc),sF1_fnc)),true,ifeq(true,true,sF0_fnc,true),true) = true,
inference(paramodulation,[status(thm)],[f17825,f648]) ).
fof(f17924,plain,
ifeq(theorem(or(sF2_fnc,sF1_fnc)),true,ifeq(true,true,sF0_fnc,true),true) = true,
inference(forward_demodulation,[status(thm)],[f24,f17901]) ).
fof(f17925,plain,
ifeq(true,true,ifeq(true,true,sF0_fnc,true),true) = true,
inference(forward_demodulation,[status(thm)],[f15856,f17924]) ).
fof(f17926,plain,
ifeq(true,true,sF0_fnc,true) = true,
inference(forward_demodulation,[status(thm)],[f12,f17925]) ).
fof(f17927,plain,
sF0_fnc = true,
inference(forward_demodulation,[status(thm)],[f12,f17926]) ).
fof(f17928,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f17927,f27]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL239-10 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.13/5.55 % Computer : n020.cluster.edu
% 0.13/5.55 % Model : x86_64 x86_64
% 0.13/5.55 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/5.55 % Memory : 8046.5625MB
% 0.13/5.55 % OS : Linux 6.8.0-71-generic
% 0.13/5.55 % CPULimit : 300
% 0.13/5.55 % WCLimit : 300
% 0.13/5.55 % DateTime : Mon Sep 21 00:14:53 UTC 2026
% 0.13/5.55 % CPUTime :
% 0.13/5.56 % Drodi V4.1.1
% 0.17/5.96 % Refutation found
% 0.17/5.96 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.17/5.96 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.17/6.03 % Elapsed time: 0.456946 seconds
% 0.17/6.03 % CPU time: 3.227797 seconds
% 0.17/6.03 % Total memory used: 97.060 MB
% 0.17/6.03 % Net memory used: 95.993 MB
%------------------------------------------------------------------------------