%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LCL428-1 : TPTP v9.3.1. Bugfixed v5.5.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n001.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:40 PM UTC 2026
% Result : Unsatisfiable 5.12s 1.19s
% Output : CNFRefutation 5.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 6
% Syntax : Number of formulae : 45 ( 19 unt; 0 def)
% Number of atoms : 81 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 85 ( 49 ~; 36 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 13 ( 2 avg)
% Number of predicates : 2 ( 1 usr; 1 prp; 0-1 aty)
% Number of functors : 18 ( 18 usr; 17 con; 0-2 aty)
% Number of variables : 81 ( 81 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,B] :
( is_a_theorem(B)
| ~ is_a_theorem(A)
| ~ is_a_theorem(implies(A,B)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [A,B] : is_a_theorem(implies(A,implies(B,A))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [A,B,C] : is_a_theorem(implies(implies(A,B),implies(implies(B,C),implies(A,C)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [A,B] : is_a_theorem(implies(implies(implies(A,B),B),implies(implies(B,A),A))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [X,Y] : is_a_theorem(implies(implies(implies(X,Y),implies(Y,X)),implies(Y,X))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,negated_conjecture,
~ is_a_theorem(implies(implies(implies(x,implies(y,x)),implies(implies(implies(implies(implies(implies(implies(implies(implies(z,u),implies(implies(v,z),implies(v,u))),implies(implies(w,implies(v6,w)),v7)),v7),implies(implies(implies(implies(v8,v9),v9),implies(implies(v9,v8),v8)),v10)),v10),implies(implies(implies(implies(v11,v12),implies(v12,v11)),implies(v12,v11)),v13)),v13),implies(implies(v14,implies(v15,v14)),v16))),v16)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,plain,
! [B] :
( is_a_theorem(B)
| ! [A] :
( ~ is_a_theorem(A)
| ~ is_a_theorem(implies(A,B)) ) ),
inference(miniscoping,[status(thm)],[f1]) ).
fof(f8,plain,
! [X0,X1] :
( is_a_theorem(X1)
| ~ is_a_theorem(X0)
| ~ is_a_theorem(implies(X0,X1)) ),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f9,plain,
! [X0,X1] : is_a_theorem(implies(X0,implies(X1,X0))),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f10,plain,
! [X0,X1,X2] : is_a_theorem(implies(implies(X0,X1),implies(implies(X1,X2),implies(X0,X2)))),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f11,plain,
! [X0,X1] : is_a_theorem(implies(implies(implies(X0,X1),X1),implies(implies(X1,X0),X0))),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f12,plain,
! [X0,X1] : is_a_theorem(implies(implies(implies(X0,X1),implies(X1,X0)),implies(X1,X0))),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f13,plain,
~ is_a_theorem(implies(implies(implies(x,implies(y,x)),implies(implies(implies(implies(implies(implies(implies(implies(implies(z,u),implies(implies(v,z),implies(v,u))),implies(implies(w,implies(v6,w)),v7)),v7),implies(implies(implies(implies(v8,v9),v9),implies(implies(v9,v8),v8)),v10)),v10),implies(implies(implies(implies(v11,v12),implies(v12,v11)),implies(v12,v11)),v13)),v13),implies(implies(v14,implies(v15,v14)),v16))),v16)),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f14,plain,
! [X0,X1] :
( is_a_theorem(implies(X1,X0))
| ~ is_a_theorem(X0) ),
inference(resolution,[status(thm)],[f8,f9]) ).
fof(f17,plain,
! [X0,X1,X2] :
( is_a_theorem(implies(implies(X1,X2),implies(X0,X2)))
| ~ is_a_theorem(implies(X0,X1)) ),
inference(resolution,[status(thm)],[f10,f8]) ).
fof(f18,plain,
! [X0,X1] :
( is_a_theorem(implies(implies(X1,X0),X0))
| ~ is_a_theorem(implies(implies(X0,X1),X1)) ),
inference(resolution,[status(thm)],[f11,f8]) ).
fof(f20,plain,
! [X0,X1,X2] :
( is_a_theorem(implies(X0,X2))
| ~ is_a_theorem(implies(X1,X2))
| ~ is_a_theorem(implies(X0,X1)) ),
inference(resolution,[status(thm)],[f17,f8]) ).
fof(f22,plain,
! [X0,X1] :
( ~ is_a_theorem(X0)
| is_a_theorem(implies(implies(X0,X1),X1)) ),
inference(resolution,[status(thm)],[f18,f14]) ).
fof(f28,plain,
! [X0,X1,X2] :
( is_a_theorem(implies(X0,implies(implies(X2,X1),X1)))
| ~ is_a_theorem(implies(X0,implies(implies(X1,X2),X2))) ),
inference(resolution,[status(thm)],[f20,f11]) ).
fof(f30,plain,
! [X0,X1,X2,X3] :
( ~ is_a_theorem(implies(X3,X1))
| is_a_theorem(implies(X0,implies(X3,X2)))
| ~ is_a_theorem(implies(X0,implies(X1,X2))) ),
inference(resolution,[status(thm)],[f20,f17]) ).
fof(f31,plain,
! [X0,X1,X2] :
( ~ is_a_theorem(X1)
| is_a_theorem(implies(X0,X2))
| ~ is_a_theorem(implies(X0,implies(X1,X2))) ),
inference(resolution,[status(thm)],[f20,f22]) ).
fof(f32,plain,
! [X0,X1,X2] :
( is_a_theorem(implies(X0,implies(X2,X1)))
| ~ is_a_theorem(implies(X0,X1)) ),
inference(resolution,[status(thm)],[f20,f9]) ).
fof(f37,plain,
! [X0,X1,X2] :
( is_a_theorem(implies(X2,X1))
| ~ is_a_theorem(X0)
| ~ is_a_theorem(implies(X0,X1)) ),
inference(resolution,[status(thm)],[f32,f8]) ).
fof(f59,plain,
! [X0,X1] : is_a_theorem(implies(X0,implies(implies(X0,X1),X1))),
inference(resolution,[status(thm)],[f28,f9]) ).
fof(f76,plain,
! [X0,X1,X2] :
( is_a_theorem(implies(X1,implies(X2,X0)))
| ~ is_a_theorem(X0) ),
inference(resolution,[status(thm)],[f37,f9]) ).
fof(f81,plain,
! [X0,X1,X2] :
( is_a_theorem(implies(implies(implies(X1,X0),X2),X2))
| ~ is_a_theorem(X0) ),
inference(resolution,[status(thm)],[f76,f18]) ).
fof(f100,plain,
! [X0,X1,X2] :
( is_a_theorem(X2)
| ~ is_a_theorem(implies(implies(X1,X0),X2))
| ~ is_a_theorem(X0) ),
inference(resolution,[status(thm)],[f81,f8]) ).
fof(f104,plain,
! [X0,X1,X2] :
( is_a_theorem(implies(implies(X0,X1),implies(X2,X1)))
| ~ is_a_theorem(X0) ),
inference(resolution,[status(thm)],[f100,f10]) ).
fof(f118,plain,
! [X0,X1,X2] :
( is_a_theorem(implies(implies(X0,X1),implies(implies(X1,X2),X2)))
| ~ is_a_theorem(X0) ),
inference(resolution,[status(thm)],[f104,f28]) ).
fof(f128,plain,
! [X0,X1,X2] :
( ~ is_a_theorem(X0)
| ~ is_a_theorem(X1)
| is_a_theorem(implies(implies(X0,implies(X1,X2)),X2)) ),
inference(resolution,[status(thm)],[f31,f22]) ).
fof(f174,plain,
! [X0,X1,X2] :
( ~ is_a_theorem(implies(X1,implies(X0,X2)))
| is_a_theorem(implies(X0,implies(X1,X2))) ),
inference(resolution,[status(thm)],[f30,f59]) ).
fof(f234,plain,
! [X0,X1,X2] :
( ~ is_a_theorem(implies(X1,X2))
| is_a_theorem(implies(implies(X0,X1),X2))
| ~ is_a_theorem(X0) ),
inference(resolution,[status(thm)],[f118,f31]) ).
fof(f313,plain,
! [X0,X1,X2] : is_a_theorem(implies(implies(X0,X1),implies(implies(X2,X0),implies(X2,X1)))),
inference(resolution,[status(thm)],[f174,f10]) ).
fof(f655,plain,
( ~ is_a_theorem(implies(implies(implies(implies(implies(implies(implies(implies(implies(implies(z,u),implies(implies(v,z),implies(v,u))),implies(implies(w,implies(v6,w)),v7)),v7),implies(implies(implies(implies(v8,v9),v9),implies(implies(v9,v8),v8)),v10)),v10),implies(implies(implies(implies(v11,v12),implies(v12,v11)),implies(v12,v11)),v13)),v13),implies(implies(v14,implies(v15,v14)),v16)),v16))
| ~ is_a_theorem(implies(x,implies(y,x))) ),
inference(resolution,[status(thm)],[f234,f13]) ).
fof(f675,plain,
~ is_a_theorem(implies(implies(implies(implies(implies(implies(implies(implies(implies(implies(z,u),implies(implies(v,z),implies(v,u))),implies(implies(w,implies(v6,w)),v7)),v7),implies(implies(implies(implies(v8,v9),v9),implies(implies(v9,v8),v8)),v10)),v10),implies(implies(implies(implies(v11,v12),implies(v12,v11)),implies(v12,v11)),v13)),v13),implies(implies(v14,implies(v15,v14)),v16)),v16)),
inference(forward_subsumption_resolution,[status(thm)],[f655,f9]) ).
fof(f676,plain,
( ~ is_a_theorem(implies(implies(implies(implies(implies(implies(implies(implies(z,u),implies(implies(v,z),implies(v,u))),implies(implies(w,implies(v6,w)),v7)),v7),implies(implies(implies(implies(v8,v9),v9),implies(implies(v9,v8),v8)),v10)),v10),implies(implies(implies(implies(v11,v12),implies(v12,v11)),implies(v12,v11)),v13)),v13))
| ~ is_a_theorem(implies(v14,implies(v15,v14))) ),
inference(resolution,[status(thm)],[f675,f128]) ).
fof(f679,plain,
~ is_a_theorem(implies(implies(implies(implies(implies(implies(implies(implies(z,u),implies(implies(v,z),implies(v,u))),implies(implies(w,implies(v6,w)),v7)),v7),implies(implies(implies(implies(v8,v9),v9),implies(implies(v9,v8),v8)),v10)),v10),implies(implies(implies(implies(v11,v12),implies(v12,v11)),implies(v12,v11)),v13)),v13)),
inference(forward_subsumption_resolution,[status(thm)],[f676,f9]) ).
fof(f680,plain,
( ~ is_a_theorem(implies(implies(implies(implies(implies(implies(z,u),implies(implies(v,z),implies(v,u))),implies(implies(w,implies(v6,w)),v7)),v7),implies(implies(implies(implies(v8,v9),v9),implies(implies(v9,v8),v8)),v10)),v10))
| ~ is_a_theorem(implies(implies(implies(v11,v12),implies(v12,v11)),implies(v12,v11))) ),
inference(resolution,[status(thm)],[f679,f128]) ).
fof(f683,plain,
~ is_a_theorem(implies(implies(implies(implies(implies(implies(z,u),implies(implies(v,z),implies(v,u))),implies(implies(w,implies(v6,w)),v7)),v7),implies(implies(implies(implies(v8,v9),v9),implies(implies(v9,v8),v8)),v10)),v10)),
inference(forward_subsumption_resolution,[status(thm)],[f680,f12]) ).
fof(f1329,plain,
( ~ is_a_theorem(implies(implies(implies(implies(z,u),implies(implies(v,z),implies(v,u))),implies(implies(w,implies(v6,w)),v7)),v7))
| ~ is_a_theorem(implies(implies(implies(v8,v9),v9),implies(implies(v9,v8),v8))) ),
inference(resolution,[status(thm)],[f683,f128]) ).
fof(f1332,plain,
~ is_a_theorem(implies(implies(implies(implies(z,u),implies(implies(v,z),implies(v,u))),implies(implies(w,implies(v6,w)),v7)),v7)),
inference(forward_subsumption_resolution,[status(thm)],[f1329,f11]) ).
fof(f1334,plain,
( ~ is_a_theorem(implies(implies(implies(w,implies(v6,w)),v7),v7))
| ~ is_a_theorem(implies(implies(z,u),implies(implies(v,z),implies(v,u)))) ),
inference(resolution,[status(thm)],[f1332,f234]) ).
fof(f1337,plain,
~ is_a_theorem(implies(implies(implies(w,implies(v6,w)),v7),v7)),
inference(forward_subsumption_resolution,[status(thm)],[f1334,f313]) ).
fof(f1342,plain,
~ is_a_theorem(implies(w,implies(v6,w))),
inference(resolution,[status(thm)],[f1337,f22]) ).
fof(f1345,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f1342,f9]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LCL428-1 : TPTP v9.3.1. Bugfixed v5.5.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.43 % Computer : n001.cluster.edu
% 0.18/0.43 % Model : x86_64 x86_64
% 0.18/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.43 % Memory : 8046.5625MB
% 0.18/0.43 % OS : Linux 6.8.0-71-generic
% 0.18/0.43 % CPULimit : 300
% 0.18/0.43 % WCLimit : 300
% 0.18/0.43 % DateTime : Mon Sep 21 00:37:28 UTC 2026
% 0.18/0.43 % CPUTime :
% 0.18/0.45 % Drodi V4.1.1
% 5.12/1.19 % Refutation found
% 5.12/1.19 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 5.12/1.19 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 1.37/1.22 % Elapsed time: 0.767885 seconds
% 1.37/1.22 % CPU time: 5.751555 seconds
% 1.37/1.22 % Total memory used: 107.628 MB
% 1.37/1.22 % Net memory used: 100.638 MB
%------------------------------------------------------------------------------