%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SYN644-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n011.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:16:59 PM UTC 2026
% Result : Unsatisfiable 19.27s 3.11s
% Output : CNFRefutation 19.27s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 11
% Syntax : Number of formulae : 40 ( 14 unt; 0 def)
% Number of atoms : 133 ( 0 equ)
% Maximal formula atoms : 9 ( 3 avg)
% Number of connectives : 186 ( 93 ~; 93 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 7 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 6 ( 5 usr; 1 prp; 0-2 aty)
% Number of functors : 18 ( 18 usr; 7 con; 0-5 aty)
% Number of variables : 128 ( 128 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,negated_conjecture,
! [X0] : p12(X0,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,negated_conjecture,
p22(f3(f4(f5(c26))),c27),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,negated_conjecture,
p24(f17(f10(c29,f11(c27,c30)),c28)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10,negated_conjecture,
p23(c28,f8(f10(c29,f11(c27,c30)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f17,negated_conjecture,
! [X1,X2,X0] :
( ~ p12(X0,X2)
| ~ p12(X0,X1)
| p12(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f23,negated_conjecture,
~ p12(c28,f16(f10(c29,f11(c27,c30)),c32,c31)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f25,negated_conjecture,
! [X66,X67,X69,X68] :
( ~ p12(X68,X66)
| ~ p25(X68,X69)
| ~ p12(X69,X67)
| p25(X66,X67) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f33,negated_conjecture,
p12(f13(f14(c31,c28)),f13(f14(c31,f16(f10(c29,f11(c27,c30)),c32,c31)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f37,negated_conjecture,
! [X7,X4,X5,X6,X3] :
( ~ p23(X3,f8(f10(X4,f11(X5,X6))))
| ~ p22(f3(f4(f5(c26))),X5)
| p25(f13(f14(X7,f16(f10(X4,f11(X5,X6)),c32,X7))),f13(f14(X7,X3))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f39,negated_conjecture,
! [X3,X4,X5,X6,X7] :
( ~ p23(X3,f8(f10(X4,f11(X5,X6))))
| ~ p24(f17(f10(X4,f11(X5,X6)),X3))
| ~ p22(f3(f4(f5(c26))),X5)
| p23(f21(X4,X5,X6,X7,X3),f8(f10(X4,f11(X5,X6))))
| p12(X3,f16(f10(X4,f11(X5,X6)),c32,X7)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f40,negated_conjecture,
! [X3,X4,X5,X6,X7] :
( ~ p25(f13(f14(X7,X3)),f13(f14(X7,f21(X4,X5,X6,X7,X3))))
| ~ p23(X3,f8(f10(X4,f11(X5,X6))))
| ~ p24(f17(f10(X4,f11(X5,X6)),X3))
| ~ p22(f3(f4(f5(c26))),X5)
| p12(X3,f16(f10(X4,f11(X5,X6)),c32,X7)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f43,plain,
! [X0] : p12(X0,X0),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f49,plain,
p22(f3(f4(f5(c26))),c27),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f51,plain,
p24(f17(f10(c29,f11(c27,c30)),c28)),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f52,plain,
p23(c28,f8(f10(c29,f11(c27,c30)))),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f59,plain,
! [X2,X0] :
( ~ p12(X0,X2)
| ! [X1] :
( ~ p12(X0,X1)
| p12(X1,X2) ) ),
inference(miniscoping,[status(thm)],[f17]) ).
fof(f60,plain,
! [X0,X1,X2] :
( ~ p12(X2,X1)
| ~ p12(X2,X0)
| p12(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f59]) ).
fof(f71,plain,
~ p12(c28,f16(f10(c29,f11(c27,c30)),c32,c31)),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f74,plain,
! [X66,X68] :
( ~ p12(X68,X66)
| ! [X69] :
( ~ p25(X68,X69)
| ! [X67] :
( ~ p12(X69,X67)
| p25(X66,X67) ) ) ),
inference(miniscoping,[status(thm)],[f25]) ).
fof(f75,plain,
! [X0,X1,X2,X3] :
( ~ p12(X3,X0)
| ~ p25(X3,X2)
| ~ p12(X2,X1)
| p25(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f90,plain,
p12(f13(f14(c31,c28)),f13(f14(c31,f16(f10(c29,f11(c27,c30)),c32,c31)))),
inference(cnf_transformation,[status(thm)],[f33]) ).
fof(f97,plain,
! [X4,X5,X6,X3] :
( ~ p23(X3,f8(f10(X4,f11(X5,X6))))
| ~ p22(f3(f4(f5(c26))),X5)
| ! [X7] : p25(f13(f14(X7,f16(f10(X4,f11(X5,X6)),c32,X7))),f13(f14(X7,X3))) ),
inference(miniscoping,[status(thm)],[f37]) ).
fof(f98,plain,
! [X0,X1,X2,X3,X4] :
( ~ p23(X4,f8(f10(X1,f11(X2,X3))))
| ~ p22(f3(f4(f5(c26))),X2)
| p25(f13(f14(X0,f16(f10(X1,f11(X2,X3)),c32,X0))),f13(f14(X0,X4))) ),
inference(cnf_transformation,[status(thm)],[f97]) ).
fof(f101,plain,
! [X3,X4,X5,X6] :
( ~ p23(X3,f8(f10(X4,f11(X5,X6))))
| ~ p24(f17(f10(X4,f11(X5,X6)),X3))
| ~ p22(f3(f4(f5(c26))),X5)
| ! [X7] :
( p23(f21(X4,X5,X6,X7,X3),f8(f10(X4,f11(X5,X6))))
| p12(X3,f16(f10(X4,f11(X5,X6)),c32,X7)) ) ),
inference(miniscoping,[status(thm)],[f39]) ).
fof(f102,plain,
! [X0,X1,X2,X3,X4] :
( ~ p23(X0,f8(f10(X1,f11(X2,X3))))
| ~ p24(f17(f10(X1,f11(X2,X3)),X0))
| ~ p22(f3(f4(f5(c26))),X2)
| p23(f21(X1,X2,X3,X4,X0),f8(f10(X1,f11(X2,X3))))
| p12(X0,f16(f10(X1,f11(X2,X3)),c32,X4)) ),
inference(cnf_transformation,[status(thm)],[f101]) ).
fof(f103,plain,
! [X0,X1,X2,X3,X4] :
( ~ p25(f13(f14(X4,X0)),f13(f14(X4,f21(X1,X2,X3,X4,X0))))
| ~ p23(X0,f8(f10(X1,f11(X2,X3))))
| ~ p24(f17(f10(X1,f11(X2,X3)),X0))
| ~ p22(f3(f4(f5(c26))),X2)
| p12(X0,f16(f10(X1,f11(X2,X3)),c32,X4)) ),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f125,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ~ p12(f13(f14(X6,f16(f10(X2,f11(X0,X3)),c32,X6))),X4)
| ~ p12(f13(f14(X6,X1)),X5)
| p25(X4,X5)
| ~ p23(X1,f8(f10(X2,f11(X0,X3))))
| ~ p22(f3(f4(f5(c26))),X0) ),
inference(resolution,[status(thm)],[f98,f75]) ).
fof(f159,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ p12(f13(f14(X5,f16(f10(X1,f11(c27,X2)),c32,X5))),X3)
| ~ p12(f13(f14(X5,X0)),X4)
| p25(X3,X4)
| ~ p23(X0,f8(f10(X1,f11(c27,X2)))) ),
inference(resolution,[status(thm)],[f125,f49]) ).
fof(f161,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( ~ p23(X8,f8(f10(X5,f11(X6,X7))))
| ~ p24(f17(f10(X5,f11(X6,X7)),X8))
| ~ p22(f3(f4(f5(c26))),X6)
| p12(X8,f16(f10(X5,f11(X6,X7)),c32,X4))
| ~ p12(f13(f14(X3,f16(f10(X1,f11(c27,X2)),c32,X3))),f13(f14(X4,X8)))
| ~ p12(f13(f14(X3,X0)),f13(f14(X4,f21(X5,X6,X7,X4,X8))))
| ~ p23(X0,f8(f10(X1,f11(c27,X2)))) ),
inference(resolution,[status(thm)],[f159,f103]) ).
fof(f197,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ p23(X7,f8(f10(X5,f11(c27,X6))))
| ~ p24(f17(f10(X5,f11(c27,X6)),X7))
| p12(X7,f16(f10(X5,f11(c27,X6)),c32,X4))
| ~ p12(f13(f14(X3,f16(f10(X1,f11(c27,X2)),c32,X3))),f13(f14(X4,X7)))
| ~ p12(f13(f14(X3,X0)),f13(f14(X4,f21(X5,c27,X6,X4,X7))))
| ~ p23(X0,f8(f10(X1,f11(c27,X2)))) ),
inference(resolution,[status(thm)],[f161,f49]) ).
fof(f251,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( ~ p12(X8,f13(f14(X4,X7)))
| ~ p12(X8,f13(f14(X3,f16(f10(X1,f11(c27,X2)),c32,X3))))
| ~ p23(X7,f8(f10(X5,f11(c27,X6))))
| ~ p24(f17(f10(X5,f11(c27,X6)),X7))
| p12(X7,f16(f10(X5,f11(c27,X6)),c32,X4))
| ~ p12(f13(f14(X3,X0)),f13(f14(X4,f21(X5,c27,X6,X4,X7))))
| ~ p23(X0,f8(f10(X1,f11(c27,X2)))) ),
inference(resolution,[status(thm)],[f197,f60]) ).
fof(f432,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ~ p12(X6,f13(f14(X2,X3)))
| ~ p12(X6,f13(f14(X2,f16(f10(X4,f11(c27,X5)),c32,X2))))
| ~ p23(X3,f8(f10(X0,f11(c27,X1))))
| ~ p24(f17(f10(X0,f11(c27,X1)),X3))
| p12(X3,f16(f10(X0,f11(c27,X1)),c32,X2))
| ~ p23(f21(X0,c27,X1,X2,X3),f8(f10(X4,f11(c27,X5)))) ),
inference(resolution,[status(thm)],[f251,f43]) ).
fof(f963,plain,
! [X0,X1,X2,X3,X4] :
( ~ p23(X0,f8(f10(X1,f11(c27,X2))))
| ~ p24(f17(f10(X1,f11(c27,X2)),X0))
| ~ p22(f3(f4(f5(c26))),c27)
| p12(X0,f16(f10(X1,f11(c27,X2)),c32,X3))
| ~ p12(X4,f13(f14(X3,X0)))
| ~ p12(X4,f13(f14(X3,f16(f10(X1,f11(c27,X2)),c32,X3))))
| ~ p23(X0,f8(f10(X1,f11(c27,X2))))
| ~ p24(f17(f10(X1,f11(c27,X2)),X0))
| p12(X0,f16(f10(X1,f11(c27,X2)),c32,X3)) ),
inference(resolution,[status(thm)],[f432,f102]) ).
fof(f967,plain,
! [X0,X1,X2,X3,X4] :
( ~ p22(f3(f4(f5(c26))),c27)
| ~ p12(X4,f13(f14(X3,X0)))
| ~ p12(X4,f13(f14(X3,f16(f10(X1,f11(c27,X2)),c32,X3))))
| ~ p23(X0,f8(f10(X1,f11(c27,X2))))
| ~ p24(f17(f10(X1,f11(c27,X2)),X0))
| p12(X0,f16(f10(X1,f11(c27,X2)),c32,X3)) ),
inference(duplicate_literals_removal,[status(thm)],[f963]) ).
fof(f968,plain,
! [X0,X1,X2,X3,X4] :
( ~ p12(X4,f13(f14(X3,X0)))
| ~ p12(X4,f13(f14(X3,f16(f10(X1,f11(c27,X2)),c32,X3))))
| ~ p23(X0,f8(f10(X1,f11(c27,X2))))
| ~ p24(f17(f10(X1,f11(c27,X2)),X0))
| p12(X0,f16(f10(X1,f11(c27,X2)),c32,X3)) ),
inference(forward_subsumption_resolution,[status(thm)],[f967,f49]) ).
fof(f972,plain,
! [X0,X1,X2,X3] :
( ~ p12(f13(f14(X3,X0)),f13(f14(X3,f16(f10(X1,f11(c27,X2)),c32,X3))))
| ~ p23(X0,f8(f10(X1,f11(c27,X2))))
| ~ p24(f17(f10(X1,f11(c27,X2)),X0))
| p12(X0,f16(f10(X1,f11(c27,X2)),c32,X3)) ),
inference(resolution,[status(thm)],[f968,f43]) ).
fof(f973,plain,
( ~ p23(c28,f8(f10(c29,f11(c27,c30))))
| ~ p24(f17(f10(c29,f11(c27,c30)),c28))
| p12(c28,f16(f10(c29,f11(c27,c30)),c32,c31)) ),
inference(resolution,[status(thm)],[f972,f90]) ).
fof(f977,plain,
( ~ p23(c28,f8(f10(c29,f11(c27,c30))))
| ~ p24(f17(f10(c29,f11(c27,c30)),c28)) ),
inference(forward_subsumption_resolution,[status(thm)],[f973,f71]) ).
fof(f979,plain,
~ p23(c28,f8(f10(c29,f11(c27,c30)))),
inference(forward_subsumption_resolution,[status(thm)],[f977,f51]) ).
fof(f980,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[f52,f979]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN644-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.55 % Computer : n011.cluster.edu
% 0.09/0.55 % Model : x86_64 x86_64
% 0.09/0.55 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.55 % Memory : 8046.5625MB
% 0.09/0.55 % OS : Linux 6.8.0-71-generic
% 0.09/0.55 % CPULimit : 300
% 0.09/0.55 % WCLimit : 300
% 0.09/0.55 % DateTime : Mon Sep 21 11:11:41 UTC 2026
% 0.09/0.55 % CPUTime :
% 0.15/0.56 % Drodi V4.1.1
% 19.27/3.11 % Refutation found
% 19.27/3.11 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 19.27/3.11 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 19.27/3.15 % Elapsed time: 2.577137 seconds
% 19.27/3.15 % CPU time: 20.258437 seconds
% 19.27/3.15 % Total memory used: 139.602 MB
% 19.27/3.15 % Net memory used: 109.709 MB
%------------------------------------------------------------------------------