%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SYN176-1 : TPTP v9.3.1. Released v1.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n019.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 03:15:24 PM UTC 2026
% Result : Unsatisfiable 0.12s 0.40s
% Output : CNFRefutation 0.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 12
% Syntax : Number of formulae : 43 ( 17 unt; 0 def)
% Number of atoms : 94 ( 0 equ)
% Maximal formula atoms : 4 ( 2 avg)
% Number of connectives : 112 ( 61 ~; 51 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 10 ( 9 usr; 1 prp; 0-3 aty)
% Number of functors : 4 ( 4 usr; 4 con; 0-0 aty)
% Number of variables : 55 ( 55 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f5,axiom,
s0(b),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f14,axiom,
! [X] : p0(b,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f24,axiom,
l0(c),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f26,axiom,
n0(d,c),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f28,axiom,
k0(e),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f40,axiom,
! [G,H] :
( ~ n0(H,G)
| l1(G,G) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f88,axiom,
! [D,E] :
( ~ p0(b,E)
| ~ l0(D)
| ~ s0(b)
| n1(D,E,D) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f92,axiom,
! [E,F,G] :
( ~ n1(E,F,E)
| ~ l1(G,E)
| ~ l0(G)
| n1(E,F,F) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f123,axiom,
! [B,C] :
( ~ p0(C,B)
| p1(B,B,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f215,axiom,
! [E,F] :
( ~ p1(E,E,E)
| ~ k0(F)
| q2(E,F,F) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f220,axiom,
! [F,G,H] :
( ~ q2(G,H,F)
| ~ n1(G,F,H)
| ~ p1(F,F,H)
| q2(F,G,F) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f369,negated_conjecture,
! [X] : ~ q2(e,c,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f374,plain,
s0(b),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f383,plain,
! [X0] : p0(b,X0),
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f393,plain,
l0(c),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f395,plain,
n0(d,c),
inference(cnf_transformation,[status(thm)],[f26]) ).
fof(f397,plain,
k0(e),
inference(cnf_transformation,[status(thm)],[f28]) ).
fof(f410,plain,
! [G] :
( ! [H] : ~ n0(H,G)
| l1(G,G) ),
inference(miniscoping,[status(thm)],[f40]) ).
fof(f411,plain,
! [X0,X1] :
( ~ n0(X1,X0)
| l1(X0,X0) ),
inference(cnf_transformation,[status(thm)],[f410]) ).
fof(f488,plain,
! [E] :
( ~ p0(b,E)
| ! [D] :
( ~ l0(D)
| ~ s0(b)
| n1(D,E,D) ) ),
inference(miniscoping,[status(thm)],[f88]) ).
fof(f489,plain,
! [X0,X1] :
( ~ p0(b,X1)
| ~ l0(X0)
| ~ s0(b)
| n1(X0,X1,X0) ),
inference(cnf_transformation,[status(thm)],[f488]) ).
fof(f495,plain,
! [E,F] :
( ~ n1(E,F,E)
| ! [G] :
( ~ l1(G,E)
| ~ l0(G)
| n1(E,F,F) ) ),
inference(miniscoping,[status(thm)],[f92]) ).
fof(f496,plain,
! [X0,X1,X2] :
( ~ n1(X0,X1,X0)
| ~ l1(X2,X0)
| ~ l0(X2)
| n1(X0,X1,X1) ),
inference(cnf_transformation,[status(thm)],[f495]) ).
fof(f544,plain,
! [B] :
( ! [C] : ~ p0(C,B)
| p1(B,B,B) ),
inference(miniscoping,[status(thm)],[f123]) ).
fof(f545,plain,
! [X0,X1] :
( ~ p0(X1,X0)
| p1(X0,X0,X0) ),
inference(cnf_transformation,[status(thm)],[f544]) ).
fof(f686,plain,
! [E] :
( ~ p1(E,E,E)
| ! [F] :
( ~ k0(F)
| q2(E,F,F) ) ),
inference(miniscoping,[status(thm)],[f215]) ).
fof(f687,plain,
! [X0,X1] :
( ~ p1(X0,X0,X0)
| ~ k0(X1)
| q2(X0,X1,X1) ),
inference(cnf_transformation,[status(thm)],[f686]) ).
fof(f693,plain,
! [X0,X1,X2] :
( ~ q2(X1,X2,X0)
| ~ n1(X1,X0,X2)
| ~ p1(X0,X0,X2)
| q2(X0,X1,X0) ),
inference(cnf_transformation,[status(thm)],[f220]) ).
fof(f924,plain,
! [X0] : ~ q2(e,c,X0),
inference(cnf_transformation,[status(thm)],[f369]) ).
fof(f969,plain,
! [X0] : p1(X0,X0,X0),
inference(resolution,[status(thm)],[f545,f383]) ).
fof(f976,plain,
! [X0,X1] :
( ~ q2(X1,X0,X0)
| ~ n1(X1,X0,X0)
| q2(X0,X1,X0) ),
inference(resolution,[status(thm)],[f969,f693]) ).
fof(f977,plain,
( ~ q2(c,e,e)
| ~ n1(c,e,e) ),
inference(resolution,[status(thm)],[f976,f924]) ).
fof(f980,plain,
! [X0,X1] :
( ~ p0(b,X1)
| ~ l0(X0)
| n1(X0,X1,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f489,f374]) ).
fof(f981,plain,
! [X0] :
( ~ q2(c,e,e)
| ~ n1(c,e,c)
| ~ l1(X0,c)
| ~ l0(X0) ),
inference(resolution,[status(thm)],[f496,f977]) ).
fof(f1051,plain,
! [X0,X1] :
( ~ k0(X1)
| q2(X0,X1,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f687,f969]) ).
fof(f1053,plain,
! [X0] : q2(X0,e,e),
inference(resolution,[status(thm)],[f1051,f397]) ).
fof(f1057,plain,
! [X0] :
( ~ n1(c,e,c)
| ~ l1(X0,c)
| ~ l0(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f981,f1053]) ).
fof(f1063,plain,
! [X0] :
( ~ n0(X0,c)
| ~ n1(c,e,c)
| ~ l0(c) ),
inference(resolution,[status(thm)],[f1057,f411]) ).
fof(f1064,plain,
! [X0] :
( ~ n0(X0,c)
| ~ n1(c,e,c) ),
inference(forward_subsumption_resolution,[status(thm)],[f1063,f393]) ).
fof(f1065,plain,
~ n1(c,e,c),
inference(resolution,[status(thm)],[f1064,f395]) ).
fof(f1066,plain,
( ~ p0(b,e)
| ~ l0(c) ),
inference(resolution,[status(thm)],[f1065,f980]) ).
fof(f1069,plain,
~ p0(b,e),
inference(forward_subsumption_resolution,[status(thm)],[f1066,f393]) ).
fof(f1070,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f1069,f383]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN176-1 : TPTP v9.3.1. Released v1.1.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n019.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Mon Sep 21 10:45:49 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.09/0.37 % Drodi V4.1.1
% 0.12/0.40 % Refutation found
% 0.12/0.40 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.12/0.40 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.12/0.43 % Elapsed time: 0.073383 seconds
% 0.12/0.43 % CPU time: 0.236079 seconds
% 0.12/0.43 % Total memory used: 70.892 MB
% 0.12/0.43 % Net memory used: 70.678 MB
%------------------------------------------------------------------------------