%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LCL250-3 : TPTP v9.3.1. Released v2.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/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 01:07:18 PM UTC 2026
% Result : Unsatisfiable 140.25s 18.20s
% Output : CNFRefutation 140.97s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 12
% Syntax : Number of formulae : 110 ( 53 unt; 2 def)
% Number of atoms : 181 ( 6 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 149 ( 78 ~; 69 |; 0 &)
% ( 2 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 4 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 6 ( 4 usr; 3 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 3 con; 0-2 aty)
% Number of variables : 214 ( 214 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A] : axiom(implies(or(A,A),A)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [A,B] : axiom(implies(A,or(B,A))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [A,B] : axiom(implies(or(A,B),or(B,A))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [A,B,C] : axiom(implies(or(A,or(B,C)),or(B,or(A,C)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [A,B,C] : axiom(implies(implies(A,B),implies(or(C,A),or(C,B)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [X,Y] : implies(X,Y) = or(not(X),Y),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [X] :
( ~ axiom(X)
| theorem(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [X,Y] :
( ~ theorem(Y)
| ~ theorem(implies(Y,X))
| theorem(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [P,Q] : and(P,Q) = not(or(not(P),not(Q))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10,negated_conjecture,
~ theorem(implies(implies(q,r),implies(and(p,q),r))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11,plain,
! [X0] : axiom(implies(or(X0,X0),X0)),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f12,plain,
! [X0,X1] : axiom(implies(X0,or(X1,X0))),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f13,plain,
! [X0,X1] : axiom(implies(or(X0,X1),or(X1,X0))),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f14,plain,
! [X0,X1,X2] : axiom(implies(or(X0,or(X1,X2)),or(X1,or(X0,X2)))),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f15,plain,
! [X0,X1,X2] : axiom(implies(implies(X0,X1),implies(or(X2,X0),or(X2,X1)))),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f16,plain,
! [X0,X1] : implies(X0,X1) = or(not(X0),X1),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f17,plain,
! [X0] :
( ~ axiom(X0)
| theorem(X0) ),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f18,plain,
! [Y] :
( ~ theorem(Y)
| ! [X] :
( ~ theorem(implies(Y,X))
| theorem(X) ) ),
inference(miniscoping,[status(thm)],[f8]) ).
fof(f19,plain,
! [X0,X1] :
( ~ theorem(X1)
| ~ theorem(implies(X1,X0))
| theorem(X0) ),
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f20,plain,
! [X0,X1] : and(X0,X1) = not(or(not(X0),not(X1))),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f21,plain,
~ theorem(implies(implies(q,r),implies(and(p,q),r))),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f36,plain,
! [X0] : theorem(implies(or(X0,X0),X0)),
inference(resolution,[status(thm)],[f11,f17]) ).
fof(f37,plain,
! [X0] :
( ~ theorem(or(X0,X0))
| theorem(X0) ),
inference(resolution,[status(thm)],[f36,f19]) ).
fof(f38,plain,
! [X0,X1] : theorem(implies(X0,or(X1,X0))),
inference(resolution,[status(thm)],[f12,f17]) ).
fof(f39,plain,
! [X0,X1] :
( ~ theorem(X1)
| theorem(or(X0,X1)) ),
inference(resolution,[status(thm)],[f38,f19]) ).
fof(f43,plain,
! [X0,X1] : and(X0,X1) = not(implies(X0,not(X1))),
inference(backward_demodulation,[status(thm)],[f16,f20]) ).
fof(f44,plain,
! [X0,X1] :
( ~ theorem(X1)
| theorem(implies(X0,X1)) ),
inference(paramodulation,[status(thm)],[f16,f39]) ).
fof(f56,definition,
! [X1] :
( sQ1_spl
<=> ~ theorem(X1) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f57,plain,
! [X0] :
( ~ sQ1_spl
| ~ theorem(X0) ),
inference(component_clause,[status(thm)],[f56]) ).
fof(f62,plain,
! [X0,X1,X2] : implies(implies(X0,not(X1)),X2) = or(and(X0,X1),X2),
inference(paramodulation,[status(thm)],[f43,f16]) ).
fof(f76,plain,
! [X0,X1] : theorem(implies(or(X0,X1),or(X1,X0))),
inference(resolution,[status(thm)],[f13,f17]) ).
fof(f79,plain,
! [X0,X1] :
( ~ theorem(or(X1,X0))
| theorem(or(X0,X1)) ),
inference(resolution,[status(thm)],[f76,f19]) ).
fof(f80,plain,
! [X0,X1] : theorem(implies(implies(X0,X1),or(X1,not(X0)))),
inference(paramodulation,[status(thm)],[f16,f76]) ).
fof(f81,plain,
! [X0,X1] : theorem(implies(or(X0,not(X1)),implies(X1,X0))),
inference(paramodulation,[status(thm)],[f16,f76]) ).
fof(f82,plain,
! [X0,X1] :
( ~ theorem(X0)
| theorem(or(X0,X1)) ),
inference(resolution,[status(thm)],[f79,f39]) ).
fof(f83,plain,
! [X0,X1] :
( ~ theorem(implies(X1,X0))
| theorem(or(X0,not(X1))) ),
inference(paramodulation,[status(thm)],[f16,f79]) ).
fof(f86,plain,
! [X0,X1] :
( ~ theorem(not(X0))
| theorem(implies(X0,X1)) ),
inference(paramodulation,[status(thm)],[f16,f82]) ).
fof(f124,plain,
! [X0,X1] :
( ~ theorem(or(X1,not(X0)))
| theorem(implies(X0,X1)) ),
inference(resolution,[status(thm)],[f81,f19]) ).
fof(f138,plain,
! [X0,X1,X2] : theorem(implies(or(X0,or(X1,X2)),or(X1,or(X0,X2)))),
inference(resolution,[status(thm)],[f14,f17]) ).
fof(f139,plain,
! [X0,X1,X2] : axiom(implies(implies(X0,or(X1,X2)),or(X1,or(not(X0),X2)))),
inference(paramodulation,[status(thm)],[f16,f14]) ).
fof(f143,plain,
! [X0,X1,X2] : axiom(implies(implies(X0,or(X1,X2)),or(X1,implies(X0,X2)))),
inference(forward_demodulation,[status(thm)],[f16,f139]) ).
fof(f147,plain,
! [X0,X1,X2] : theorem(implies(implies(X0,X1),implies(or(X2,X0),or(X2,X1)))),
inference(resolution,[status(thm)],[f15,f17]) ).
fof(f148,plain,
! [X0,X1,X2] : axiom(implies(implies(X0,X1),implies(implies(X2,X0),or(not(X2),X1)))),
inference(paramodulation,[status(thm)],[f16,f15]) ).
fof(f150,plain,
! [X0,X1,X2] : axiom(implies(implies(X0,X1),implies(implies(X2,X0),implies(X2,X1)))),
inference(forward_demodulation,[status(thm)],[f16,f148]) ).
fof(f200,plain,
! [X0,X1,X2] : theorem(or(implies(X0,or(X1,X0)),X2)),
inference(resolution,[status(thm)],[f38,f82]) ).
fof(f206,plain,
! [X0,X1] :
( ~ axiom(implies(X1,X0))
| ~ theorem(X1)
| theorem(X0) ),
inference(resolution,[status(thm)],[f19,f17]) ).
fof(f219,plain,
! [X0,X1,X2] :
( ~ theorem(implies(X1,not(X2)))
| ~ theorem(or(and(X1,X2),X0))
| theorem(X0) ),
inference(paramodulation,[status(thm)],[f62,f19]) ).
fof(f229,plain,
! [X0,X1] : theorem(implies(X0,implies(or(X1,X1),X1))),
inference(resolution,[status(thm)],[f44,f36]) ).
fof(f232,plain,
! [X0,X1] :
( ~ axiom(X1)
| theorem(implies(X0,X1)) ),
inference(resolution,[status(thm)],[f44,f17]) ).
fof(f247,plain,
! [X0,X1] :
( ~ theorem(X1)
| theorem(X0)
| ~ axiom(X0) ),
inference(resolution,[status(thm)],[f232,f19]) ).
fof(f253,definition,
! [X0] :
( sQ4_spl
<=> ( theorem(X0)
| ~ axiom(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f254,plain,
! [X0] :
( ~ sQ4_spl
| theorem(X0)
| ~ axiom(X0) ),
inference(component_clause,[status(thm)],[f253]) ).
fof(f256,plain,
( sQ1_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f247,f253,f56]) ).
fof(f260,plain,
( ~ sQ1_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f36,f57]) ).
fof(f265,plain,
~ sQ1_spl,
inference(contradiction_clause,[status(thm)],[f260]) ).
fof(f294,plain,
! [X0,X1,X2] : theorem(implies(implies(X0,or(X1,X2)),or(X1,or(not(X0),X2)))),
inference(paramodulation,[status(thm)],[f16,f138]) ).
fof(f298,plain,
! [X0,X1,X2] : theorem(implies(implies(X0,or(X1,X2)),or(X1,implies(X0,X2)))),
inference(forward_demodulation,[status(thm)],[f16,f294]) ).
fof(f338,plain,
! [X0,X1,X2] :
( ~ theorem(implies(X1,X2))
| theorem(implies(or(X0,X1),or(X0,X2))) ),
inference(resolution,[status(thm)],[f147,f19]) ).
fof(f342,plain,
! [X0,X1,X2] : theorem(implies(implies(X0,X1),implies(implies(X2,X0),or(not(X2),X1)))),
inference(paramodulation,[status(thm)],[f16,f147]) ).
fof(f344,plain,
! [X0,X1,X2] : theorem(implies(implies(X0,X1),implies(implies(X2,X0),implies(X2,X1)))),
inference(forward_demodulation,[status(thm)],[f16,f342]) ).
fof(f452,plain,
! [X0,X1,X2] :
( ~ theorem(implies(X1,or(X0,X2)))
| theorem(or(X0,implies(X1,X2))) ),
inference(resolution,[status(thm)],[f206,f143]) ).
fof(f558,plain,
! [X0,X1,X2] :
( ~ theorem(implies(X1,X2))
| theorem(implies(implies(X0,X1),implies(X0,X2))) ),
inference(resolution,[status(thm)],[f150,f206]) ).
fof(f559,plain,
! [X0,X1,X2] : axiom(or(and(X0,X1),implies(implies(X2,X0),implies(X2,not(X1))))),
inference(paramodulation,[status(thm)],[f62,f150]) ).
fof(f932,plain,
! [X0,X1] : theorem(or(and(X0,X1),or(not(X1),not(X0)))),
inference(paramodulation,[status(thm)],[f62,f80]) ).
fof(f940,plain,
! [X0,X1] : theorem(or(and(X0,X1),implies(X1,not(X0)))),
inference(forward_demodulation,[status(thm)],[f16,f932]) ).
fof(f1551,plain,
! [X0,X1] :
( ~ theorem(or(and(or(not(X1),not(X1)),X1),X0))
| theorem(X0) ),
inference(resolution,[status(thm)],[f219,f36]) ).
fof(f1564,plain,
! [X0,X1] :
( ~ theorem(or(and(implies(X1,not(X1)),X1),X0))
| theorem(X0) ),
inference(forward_demodulation,[status(thm)],[f16,f1551]) ).
fof(f1720,plain,
! [X0,X1,X2] : theorem(implies(implies(X0,implies(X1,X2)),or(not(X1),implies(X0,X2)))),
inference(paramodulation,[status(thm)],[f16,f298]) ).
fof(f1728,plain,
! [X0,X1,X2] : theorem(implies(implies(X0,implies(X1,X2)),implies(X1,implies(X0,X2)))),
inference(forward_demodulation,[status(thm)],[f16,f1720]) ).
fof(f1892,plain,
! [X0,X1,X2] :
( ~ theorem(or(X2,X0))
| theorem(or(X2,X1))
| ~ theorem(implies(X0,X1)) ),
inference(resolution,[status(thm)],[f338,f19]) ).
fof(f2333,plain,
! [X0,X1] :
( theorem(implies(X0,X1))
| ~ theorem(implies(X0,or(implies(X0,X1),X1))) ),
inference(resolution,[status(thm)],[f452,f37]) ).
fof(f2379,plain,
! [X0,X1,X2] :
( ~ theorem(implies(X2,X0))
| theorem(implies(X2,X1))
| ~ theorem(implies(X0,X1)) ),
inference(resolution,[status(thm)],[f558,f19]) ).
fof(f2870,plain,
! [X0,X1,X2] :
( theorem(X1)
| ~ theorem(or(and(implies(X2,not(X2)),X2),X0))
| ~ theorem(implies(X0,X1)) ),
inference(resolution,[status(thm)],[f1892,f1564]) ).
fof(f2880,plain,
! [X0,X1] :
( theorem(X1)
| ~ theorem(or(X1,X0))
| ~ theorem(implies(X0,X1)) ),
inference(resolution,[status(thm)],[f1892,f37]) ).
fof(f4373,plain,
! [X0] : theorem(implies(X0,X0)),
inference(resolution,[status(thm)],[f2333,f38]) ).
fof(f4401,plain,
! [X0,X1] :
( ~ theorem(or(and(not(X1),X1),X0))
| theorem(X0) ),
inference(resolution,[status(thm)],[f4373,f219]) ).
fof(f5598,plain,
! [X0] : theorem(implies(X0,not(not(X0)))),
inference(resolution,[status(thm)],[f4401,f940]) ).
fof(f5643,plain,
! [X0,X1] :
( ~ theorem(or(and(X1,not(X1)),X0))
| theorem(X0) ),
inference(resolution,[status(thm)],[f5598,f219]) ).
fof(f5645,plain,
! [X0] :
( theorem(not(not(X0)))
| ~ theorem(or(not(not(X0)),X0)) ),
inference(resolution,[status(thm)],[f5598,f2880]) ).
fof(f5659,plain,
! [X0] :
( theorem(not(not(X0)))
| ~ theorem(implies(not(X0),X0)) ),
inference(forward_demodulation,[status(thm)],[f16,f5645]) ).
fof(f6340,plain,
! [X0,X1] :
( ~ sQ4_spl
| ~ axiom(or(and(X1,not(X1)),X0))
| theorem(X0) ),
inference(resolution,[status(thm)],[f5643,f254]) ).
fof(f8227,plain,
! [X0,X1] :
( ~ sQ4_spl
| theorem(implies(implies(X0,X1),implies(X0,not(not(X1))))) ),
inference(resolution,[status(thm)],[f6340,f559]) ).
fof(f10066,plain,
! [X0,X1] :
( theorem(implies(not(X0),X1))
| ~ theorem(implies(not(X0),X0)) ),
inference(resolution,[status(thm)],[f5659,f86]) ).
fof(f15140,plain,
! [X0,X1] : theorem(implies(not(implies(or(X0,X0),X0)),X1)),
inference(resolution,[status(thm)],[f10066,f229]) ).
fof(f15223,plain,
! [X0,X1] :
( theorem(X0)
| ~ theorem(or(X0,not(implies(or(X1,X1),X1)))) ),
inference(resolution,[status(thm)],[f15140,f2880]) ).
fof(f36327,plain,
! [X0,X1] :
( ~ theorem(implies(implies(or(X1,X1),X1),X0))
| theorem(X0) ),
inference(resolution,[status(thm)],[f15223,f83]) ).
fof(f36772,plain,
! [X0,X1] :
( ~ theorem(implies(X0,X1))
| theorem(implies(or(X0,X0),X1)) ),
inference(resolution,[status(thm)],[f36327,f558]) ).
fof(f38490,plain,
! [X0,X1] :
( ~ theorem(or(X0,X0))
| theorem(X1)
| ~ theorem(implies(X0,X1)) ),
inference(resolution,[status(thm)],[f36772,f19]) ).
fof(f41487,plain,
! [X0,X1,X2] :
( theorem(X2)
| ~ theorem(implies(implies(X0,or(X1,X0)),X2)) ),
inference(resolution,[status(thm)],[f38490,f200]) ).
fof(f43293,plain,
! [X0,X1] : theorem(or(X0,implies(X1,X1))),
inference(resolution,[status(thm)],[f41487,f298]) ).
fof(f43295,plain,
! [X0,X1,X2] : theorem(implies(implies(X0,X1),implies(X0,or(X2,X1)))),
inference(resolution,[status(thm)],[f41487,f344]) ).
fof(f43297,plain,
! [X0,X1] :
( ~ sQ4_spl
| theorem(implies(X0,not(not(or(X1,X0))))) ),
inference(resolution,[status(thm)],[f41487,f8227]) ).
fof(f43365,plain,
! [X0,X1] :
( theorem(X1)
| ~ theorem(implies(implies(X0,X0),X1)) ),
inference(resolution,[status(thm)],[f43293,f38490]) ).
fof(f44210,plain,
! [X0,X1] : theorem(implies(X0,implies(implies(X0,X1),X1))),
inference(resolution,[status(thm)],[f43365,f1728]) ).
fof(f44883,plain,
! [X0,X1] :
( ~ theorem(X0)
| theorem(implies(implies(X0,X1),X1)) ),
inference(resolution,[status(thm)],[f44210,f19]) ).
fof(f45294,plain,
! [X0,X1] :
( ~ sQ4_spl
| theorem(implies(X0,not(not(implies(X1,X0))))) ),
inference(paramodulation,[status(thm)],[f16,f43297]) ).
fof(f46244,plain,
! [X0,X1] :
( ~ sQ4_spl
| theorem(implies(not(X0),not(and(X1,X0)))) ),
inference(paramodulation,[status(thm)],[f43,f45294]) ).
fof(f54056,plain,
! [X0,X1,X2] :
( ~ theorem(implies(X0,X2))
| theorem(implies(X0,or(X1,X2))) ),
inference(resolution,[status(thm)],[f43295,f19]) ).
fof(f57291,plain,
! [X0] :
( ~ theorem(implies(implies(q,r),X0))
| ~ theorem(implies(X0,implies(and(p,q),r))) ),
inference(resolution,[status(thm)],[f2379,f21]) ).
fof(f58226,plain,
! [X0] : ~ theorem(implies(implies(implies(X0,q),implies(X0,r)),implies(and(p,q),r))),
inference(resolution,[status(thm)],[f57291,f344]) ).
fof(f63436,plain,
~ theorem(implies(and(p,q),q)),
inference(resolution,[status(thm)],[f58226,f44883]) ).
fof(f63484,plain,
~ theorem(or(q,not(and(p,q)))),
inference(resolution,[status(thm)],[f63436,f124]) ).
fof(f65442,plain,
! [X0,X1,X2] :
( theorem(or(X2,X1))
| ~ theorem(implies(implies(X0,X0),X1)) ),
inference(resolution,[status(thm)],[f54056,f43365]) ).
fof(f95717,plain,
! [X0,X1] : theorem(or(X0,or(X1,not(X1)))),
inference(resolution,[status(thm)],[f65442,f80]) ).
fof(f95841,plain,
! [X0,X1] :
( theorem(X1)
| ~ theorem(implies(or(X0,not(X0)),X1)) ),
inference(resolution,[status(thm)],[f95717,f2870]) ).
fof(f99278,plain,
! [X0,X1] :
( ~ theorem(implies(not(X0),X1))
| theorem(or(X0,X1)) ),
inference(resolution,[status(thm)],[f95841,f338]) ).
fof(f106077,plain,
! [X0,X1] :
( ~ sQ4_spl
| theorem(or(X0,not(and(X1,X0)))) ),
inference(resolution,[status(thm)],[f99278,f46244]) ).
fof(f106228,plain,
( ~ sQ4_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f63484,f106077]) ).
fof(f106282,plain,
~ sQ4_spl,
inference(contradiction_clause,[status(thm)],[f106228]) ).
fof(f106283,plain,
$false,
inference(sat_refutation,[status(thm)],[f256,f265,f106282]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL250-3 : TPTP v9.3.1. Released v2.3.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.37 % Computer : n009.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Mon Sep 21 00:15:27 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.38 % Drodi V4.1.1
% 140.25/18.20 % Refutation found
% 140.25/18.20 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 140.25/18.20 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 110.73/19.44 % Elapsed time: 18.853070 seconds
% 110.73/19.44 % CPU time: 139.503354 seconds
% 110.73/19.44 % Total memory used: 793.740 MB
% 110.73/19.44 % Net memory used: 755.490 MB
%------------------------------------------------------------------------------