%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SYO634-1 : TPTP v9.3.1. Released v7.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n016.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:42:51 PM UTC 2026
% Result : Unsatisfiable 0.16s 5.41s
% Output : CNFRefutation 0.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 6
% Number of leaves : 32
% Syntax : Number of formulae : 113 ( 9 unt; 20 def)
% Number of atoms : 446 ( 0 equ)
% Maximal formula atoms : 11 ( 3 avg)
% Number of connectives : 622 ( 289 ~; 313 |; 0 &)
% ( 20 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 25 ( 7 avg)
% Maximal term depth : 14 ( 4 avg)
% Number of predicates : 22 ( 21 usr; 21 prp; 0-2 aty)
% Number of functors : 4 ( 4 usr; 1 con; 0-2 aty)
% Number of variables : 348 ( 348 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [E,A_0,B_0] :
( 'E'(f(B_0),s(s(s(s(s(s(s(s('0')))))))))
| ~ 'E'(f(B_0),s(s(s(s(s(s(s(s(s(s('0')))))))))))
| ~ 'E'(f(A_0),s(s(s(s(s(s(s(s(s('0')))))))))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [E,B] : 'E'(f(B),s(s(s(s(s(s(s(s(s(s('0'))))))))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [E,A_0,B_0,A_1,A_2] :
( 'E'(f(B_0),s(s(s(s(s(s('0')))))))
| ~ 'E'(f(A_2),s(s(s(s(s(s(s('0'))))))))
| ~ 'E'(f(A_1),s(s(s(s(s(s(s(s('0')))))))))
| ~ 'E'(f(B_0),s(s(s(s(s(s(s(s(s(s('0')))))))))))
| ~ 'E'(f(A_0),s(s(s(s(s(s(s(s(s('0')))))))))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [E,B_0] : 'E'(f(B_0),s(s(s(s(s(s(s(s(s('0')))))))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [E,A_1,A_4,B_0,A_5,A_7,A_2,A_6,A_0,A_3,AP,K] :
( 'E'(f('AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),K)),s('0'))
| ~ 'E'(f(A_3),s(s(s(s(s(s('0')))))))
| ~ 'E'(f(A_0),s(s(s(s(s(s(s(s(s('0'))))))))))
| ~ 'E'(f(A_6),s(s(s('0'))))
| ~ 'E'(f(A_2),s(s(s(s(s(s(s('0'))))))))
| ~ 'E'(f(A_7),s(s('0')))
| ~ 'E'(f(A_5),s(s(s(s('0')))))
| ~ 'E'(f(B_0),s(s(s(s(s(s(s(s(s(s('0')))))))))))
| ~ 'E'(f(A_4),s(s(s(s(s('0'))))))
| ~ 'E'(f(A_1),s(s(s(s(s(s(s(s('0'))))))))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [E,A_1,A_4,B_0,A_2,A_0,A_3,AP,K] :
( 'E'(f('AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),K)),s(s(s(s('0')))))
| ~ 'E'(f(A_3),s(s(s(s(s(s('0')))))))
| ~ 'E'(f(A_0),s(s(s(s(s(s(s(s(s('0'))))))))))
| ~ 'E'(f(A_2),s(s(s(s(s(s(s('0'))))))))
| ~ 'E'(f(B_0),s(s(s(s(s(s(s(s(s(s('0')))))))))))
| ~ 'E'(f(A_4),s(s(s(s(s('0'))))))
| ~ 'E'(f(A_1),s(s(s(s(s(s(s(s('0'))))))))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f14,axiom,
! [E,A_0,B_0,A_1] :
( 'E'(f(B_0),s(s(s(s(s(s(s('0'))))))))
| ~ 'E'(f(A_1),s(s(s(s(s(s(s(s('0')))))))))
| ~ 'E'(f(B_0),s(s(s(s(s(s(s(s(s(s('0')))))))))))
| ~ 'E'(f(A_0),s(s(s(s(s(s(s(s(s('0')))))))))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [E,A_1,A_4,B_0,A_5,A_2,A_0,A_3,AP,K] :
( 'E'(f('AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),K)),s(s(s('0'))))
| ~ 'E'(f(A_3),s(s(s(s(s(s('0')))))))
| ~ 'E'(f(A_0),s(s(s(s(s(s(s(s(s('0'))))))))))
| ~ 'E'(f(A_2),s(s(s(s(s(s(s('0'))))))))
| ~ 'E'(f(A_5),s(s(s(s('0')))))
| ~ 'E'(f(B_0),s(s(s(s(s(s(s(s(s(s('0')))))))))))
| ~ 'E'(f(A_4),s(s(s(s(s('0'))))))
| ~ 'E'(f(A_1),s(s(s(s(s(s(s(s('0'))))))))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f17,axiom,
! [E,A_1,A_4,A_8,B_0,A_5,A_7,A_2,A_6,A_0,A_3,A_9] :
( ~ 'E'(f(A_9),'0')
| ~ 'E'(f(A_3),s(s(s(s(s(s('0')))))))
| ~ 'E'(f(A_0),s(s(s(s(s(s(s(s(s('0'))))))))))
| ~ 'E'(f(A_6),s(s(s('0'))))
| ~ 'E'(f(A_2),s(s(s(s(s(s(s('0'))))))))
| ~ 'E'(f(A_7),s(s('0')))
| ~ 'E'(f(A_5),s(s(s(s('0')))))
| ~ 'E'(f(B_0),s(s(s(s(s(s(s(s(s(s('0')))))))))))
| ~ 'E'(f(A_8),s('0'))
| ~ 'E'(f(A_4),s(s(s(s(s('0'))))))
| ~ 'E'(f(A_1),s(s(s(s(s(s(s(s('0'))))))))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f19,axiom,
! [E,A_1,A_4,B_0,A_5,A_2,A_6,A_0,A_3,AP,K] :
( 'E'(f('AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),K)),s(s('0')))
| ~ 'E'(f(A_3),s(s(s(s(s(s('0')))))))
| ~ 'E'(f(A_0),s(s(s(s(s(s(s(s(s('0'))))))))))
| ~ 'E'(f(A_6),s(s(s('0'))))
| ~ 'E'(f(A_2),s(s(s(s(s(s(s('0'))))))))
| ~ 'E'(f(A_5),s(s(s(s('0')))))
| ~ 'E'(f(B_0),s(s(s(s(s(s(s(s(s(s('0')))))))))))
| ~ 'E'(f(A_4),s(s(s(s(s('0'))))))
| ~ 'E'(f(A_1),s(s(s(s(s(s(s(s('0'))))))))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f20,axiom,
! [E,A_1,B_0,A_2,A_0,A_3] :
( 'E'(f(B_0),s(s(s(s(s('0'))))))
| ~ 'E'(f(A_3),s(s(s(s(s(s('0')))))))
| ~ 'E'(f(A_0),s(s(s(s(s(s(s(s(s('0'))))))))))
| ~ 'E'(f(A_2),s(s(s(s(s(s(s('0'))))))))
| ~ 'E'(f(B_0),s(s(s(s(s(s(s(s(s(s('0')))))))))))
| ~ 'E'(f(A_1),s(s(s(s(s(s(s(s('0'))))))))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f22,axiom,
! [E,A_1,A_4,A_8,B_0,A_5,A_7,A_2,A_6,A_0,A_3,AP,K] :
( 'E'(f('AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),K)),'0')
| ~ 'E'(f(A_3),s(s(s(s(s(s('0')))))))
| ~ 'E'(f(A_0),s(s(s(s(s(s(s(s(s('0'))))))))))
| ~ 'E'(f(A_6),s(s(s('0'))))
| ~ 'E'(f(A_2),s(s(s(s(s(s(s('0'))))))))
| ~ 'E'(f(A_7),s(s('0')))
| ~ 'E'(f(A_5),s(s(s(s('0')))))
| ~ 'E'(f(B_0),s(s(s(s(s(s(s(s(s(s('0')))))))))))
| ~ 'E'(f(A_8),s('0'))
| ~ 'E'(f(A_4),s(s(s(s(s('0'))))))
| ~ 'E'(f(A_1),s(s(s(s(s(s(s(s('0'))))))))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f24,plain,
! [B_0] :
( 'E'(f(B_0),s(s(s(s(s(s(s(s('0')))))))))
| ~ 'E'(f(B_0),s(s(s(s(s(s(s(s(s(s('0')))))))))))
| ! [A_0] : ~ 'E'(f(A_0),s(s(s(s(s(s(s(s(s('0')))))))))) ),
inference(miniscoping,[status(thm)],[f1]) ).
fof(f25,plain,
! [E,X0,X1] :
( 'E'(f(X1),s(s(s(s(s(s(s(s('0')))))))))
| ~ 'E'(f(X1),s(s(s(s(s(s(s(s(s(s('0')))))))))))
| ~ 'E'(f(X0),s(s(s(s(s(s(s(s(s('0')))))))))) ),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f28,plain,
! [B] : 'E'(f(B),s(s(s(s(s(s(s(s(s(s('0'))))))))))),
inference(miniscoping,[status(thm)],[f3]) ).
fof(f29,plain,
! [E,X0] : 'E'(f(X0),s(s(s(s(s(s(s(s(s(s('0'))))))))))),
inference(cnf_transformation,[status(thm)],[f28]) ).
fof(f34,plain,
! [B_0] :
( 'E'(f(B_0),s(s(s(s(s(s('0')))))))
| ! [A_2] : ~ 'E'(f(A_2),s(s(s(s(s(s(s('0'))))))))
| ! [A_1] : ~ 'E'(f(A_1),s(s(s(s(s(s(s(s('0')))))))))
| ~ 'E'(f(B_0),s(s(s(s(s(s(s(s(s(s('0')))))))))))
| ! [A_0] : ~ 'E'(f(A_0),s(s(s(s(s(s(s(s(s('0')))))))))) ),
inference(miniscoping,[status(thm)],[f6]) ).
fof(f35,plain,
! [E,X0,X1,X2,X3] :
( 'E'(f(X1),s(s(s(s(s(s('0')))))))
| ~ 'E'(f(X3),s(s(s(s(s(s(s('0'))))))))
| ~ 'E'(f(X2),s(s(s(s(s(s(s(s('0')))))))))
| ~ 'E'(f(X1),s(s(s(s(s(s(s(s(s(s('0')))))))))))
| ~ 'E'(f(X0),s(s(s(s(s(s(s(s(s('0')))))))))) ),
inference(cnf_transformation,[status(thm)],[f34]) ).
fof(f40,plain,
! [B_0] : 'E'(f(B_0),s(s(s(s(s(s(s(s(s('0')))))))))),
inference(miniscoping,[status(thm)],[f9]) ).
fof(f41,plain,
! [E,X0] : 'E'(f(X0),s(s(s(s(s(s(s(s(s('0')))))))))),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f44,plain,
( ! [K] : 'E'(f('AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),K)),s('0'))
| ! [A_3] : ~ 'E'(f(A_3),s(s(s(s(s(s('0')))))))
| ! [A_0] : ~ 'E'(f(A_0),s(s(s(s(s(s(s(s(s('0'))))))))))
| ! [A_6] : ~ 'E'(f(A_6),s(s(s('0'))))
| ! [A_2] : ~ 'E'(f(A_2),s(s(s(s(s(s(s('0'))))))))
| ! [A_7] : ~ 'E'(f(A_7),s(s('0')))
| ! [A_5] : ~ 'E'(f(A_5),s(s(s(s('0')))))
| ! [B_0] : ~ 'E'(f(B_0),s(s(s(s(s(s(s(s(s(s('0')))))))))))
| ! [A_4] : ~ 'E'(f(A_4),s(s(s(s(s('0'))))))
| ! [A_1] : ~ 'E'(f(A_1),s(s(s(s(s(s(s(s('0'))))))))) ),
inference(miniscoping,[status(thm)],[f11]) ).
fof(f45,plain,
! [E,X0,X1,X2,X3,X4,X5,X6,X7,X8,AP,X9] :
( 'E'(f('AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),X9)),s('0'))
| ~ 'E'(f(X8),s(s(s(s(s(s('0')))))))
| ~ 'E'(f(X7),s(s(s(s(s(s(s(s(s('0'))))))))))
| ~ 'E'(f(X6),s(s(s('0'))))
| ~ 'E'(f(X5),s(s(s(s(s(s(s('0'))))))))
| ~ 'E'(f(X4),s(s('0')))
| ~ 'E'(f(X3),s(s(s(s('0')))))
| ~ 'E'(f(X2),s(s(s(s(s(s(s(s(s(s('0')))))))))))
| ~ 'E'(f(X1),s(s(s(s(s('0'))))))
| ~ 'E'(f(X0),s(s(s(s(s(s(s(s('0'))))))))) ),
inference(cnf_transformation,[status(thm)],[f44]) ).
fof(f46,plain,
( ! [K] : 'E'(f('AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),K)),s(s(s(s('0')))))
| ! [A_3] : ~ 'E'(f(A_3),s(s(s(s(s(s('0')))))))
| ! [A_0] : ~ 'E'(f(A_0),s(s(s(s(s(s(s(s(s('0'))))))))))
| ! [A_2] : ~ 'E'(f(A_2),s(s(s(s(s(s(s('0'))))))))
| ! [B_0] : ~ 'E'(f(B_0),s(s(s(s(s(s(s(s(s(s('0')))))))))))
| ! [A_4] : ~ 'E'(f(A_4),s(s(s(s(s('0'))))))
| ! [A_1] : ~ 'E'(f(A_1),s(s(s(s(s(s(s(s('0'))))))))) ),
inference(miniscoping,[status(thm)],[f12]) ).
fof(f47,plain,
! [E,X0,X1,X2,X3,X4,X5,AP,X6] :
( 'E'(f('AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),X6)),s(s(s(s('0')))))
| ~ 'E'(f(X5),s(s(s(s(s(s('0')))))))
| ~ 'E'(f(X4),s(s(s(s(s(s(s(s(s('0'))))))))))
| ~ 'E'(f(X3),s(s(s(s(s(s(s('0'))))))))
| ~ 'E'(f(X2),s(s(s(s(s(s(s(s(s(s('0')))))))))))
| ~ 'E'(f(X1),s(s(s(s(s('0'))))))
| ~ 'E'(f(X0),s(s(s(s(s(s(s(s('0'))))))))) ),
inference(cnf_transformation,[status(thm)],[f46]) ).
fof(f50,plain,
! [B_0] :
( 'E'(f(B_0),s(s(s(s(s(s(s('0'))))))))
| ! [A_1] : ~ 'E'(f(A_1),s(s(s(s(s(s(s(s('0')))))))))
| ~ 'E'(f(B_0),s(s(s(s(s(s(s(s(s(s('0')))))))))))
| ! [A_0] : ~ 'E'(f(A_0),s(s(s(s(s(s(s(s(s('0')))))))))) ),
inference(miniscoping,[status(thm)],[f14]) ).
fof(f51,plain,
! [E,X0,X1,X2] :
( 'E'(f(X1),s(s(s(s(s(s(s('0'))))))))
| ~ 'E'(f(X2),s(s(s(s(s(s(s(s('0')))))))))
| ~ 'E'(f(X1),s(s(s(s(s(s(s(s(s(s('0')))))))))))
| ~ 'E'(f(X0),s(s(s(s(s(s(s(s(s('0')))))))))) ),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f52,plain,
( ! [K] : 'E'(f('AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),K)),s(s(s('0'))))
| ! [A_3] : ~ 'E'(f(A_3),s(s(s(s(s(s('0')))))))
| ! [A_0] : ~ 'E'(f(A_0),s(s(s(s(s(s(s(s(s('0'))))))))))
| ! [A_2] : ~ 'E'(f(A_2),s(s(s(s(s(s(s('0'))))))))
| ! [A_5] : ~ 'E'(f(A_5),s(s(s(s('0')))))
| ! [B_0] : ~ 'E'(f(B_0),s(s(s(s(s(s(s(s(s(s('0')))))))))))
| ! [A_4] : ~ 'E'(f(A_4),s(s(s(s(s('0'))))))
| ! [A_1] : ~ 'E'(f(A_1),s(s(s(s(s(s(s(s('0'))))))))) ),
inference(miniscoping,[status(thm)],[f15]) ).
fof(f53,plain,
! [E,X0,X1,X2,X3,X4,X5,X6,AP,X7] :
( 'E'(f('AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),X7)),s(s(s('0'))))
| ~ 'E'(f(X6),s(s(s(s(s(s('0')))))))
| ~ 'E'(f(X5),s(s(s(s(s(s(s(s(s('0'))))))))))
| ~ 'E'(f(X4),s(s(s(s(s(s(s('0'))))))))
| ~ 'E'(f(X3),s(s(s(s('0')))))
| ~ 'E'(f(X2),s(s(s(s(s(s(s(s(s(s('0')))))))))))
| ~ 'E'(f(X1),s(s(s(s(s('0'))))))
| ~ 'E'(f(X0),s(s(s(s(s(s(s(s('0'))))))))) ),
inference(cnf_transformation,[status(thm)],[f52]) ).
fof(f56,plain,
( ! [A_9] : ~ 'E'(f(A_9),'0')
| ! [A_3] : ~ 'E'(f(A_3),s(s(s(s(s(s('0')))))))
| ! [A_0] : ~ 'E'(f(A_0),s(s(s(s(s(s(s(s(s('0'))))))))))
| ! [A_6] : ~ 'E'(f(A_6),s(s(s('0'))))
| ! [A_2] : ~ 'E'(f(A_2),s(s(s(s(s(s(s('0'))))))))
| ! [A_7] : ~ 'E'(f(A_7),s(s('0')))
| ! [A_5] : ~ 'E'(f(A_5),s(s(s(s('0')))))
| ! [B_0] : ~ 'E'(f(B_0),s(s(s(s(s(s(s(s(s(s('0')))))))))))
| ! [A_8] : ~ 'E'(f(A_8),s('0'))
| ! [A_4] : ~ 'E'(f(A_4),s(s(s(s(s('0'))))))
| ! [A_1] : ~ 'E'(f(A_1),s(s(s(s(s(s(s(s('0'))))))))) ),
inference(miniscoping,[status(thm)],[f17]) ).
fof(f57,plain,
! [E,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10] :
( ~ 'E'(f(X10),'0')
| ~ 'E'(f(X9),s(s(s(s(s(s('0')))))))
| ~ 'E'(f(X8),s(s(s(s(s(s(s(s(s('0'))))))))))
| ~ 'E'(f(X7),s(s(s('0'))))
| ~ 'E'(f(X6),s(s(s(s(s(s(s('0'))))))))
| ~ 'E'(f(X5),s(s('0')))
| ~ 'E'(f(X4),s(s(s(s('0')))))
| ~ 'E'(f(X3),s(s(s(s(s(s(s(s(s(s('0')))))))))))
| ~ 'E'(f(X2),s('0'))
| ~ 'E'(f(X1),s(s(s(s(s('0'))))))
| ~ 'E'(f(X0),s(s(s(s(s(s(s(s('0'))))))))) ),
inference(cnf_transformation,[status(thm)],[f56]) ).
fof(f60,plain,
( ! [K] : 'E'(f('AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),K)),s(s('0')))
| ! [A_3] : ~ 'E'(f(A_3),s(s(s(s(s(s('0')))))))
| ! [A_0] : ~ 'E'(f(A_0),s(s(s(s(s(s(s(s(s('0'))))))))))
| ! [A_6] : ~ 'E'(f(A_6),s(s(s('0'))))
| ! [A_2] : ~ 'E'(f(A_2),s(s(s(s(s(s(s('0'))))))))
| ! [A_5] : ~ 'E'(f(A_5),s(s(s(s('0')))))
| ! [B_0] : ~ 'E'(f(B_0),s(s(s(s(s(s(s(s(s(s('0')))))))))))
| ! [A_4] : ~ 'E'(f(A_4),s(s(s(s(s('0'))))))
| ! [A_1] : ~ 'E'(f(A_1),s(s(s(s(s(s(s(s('0'))))))))) ),
inference(miniscoping,[status(thm)],[f19]) ).
fof(f61,plain,
! [E,X0,X1,X2,X3,X4,X5,X6,X7,AP,X8] :
( 'E'(f('AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),X8)),s(s('0')))
| ~ 'E'(f(X7),s(s(s(s(s(s('0')))))))
| ~ 'E'(f(X6),s(s(s(s(s(s(s(s(s('0'))))))))))
| ~ 'E'(f(X5),s(s(s('0'))))
| ~ 'E'(f(X4),s(s(s(s(s(s(s('0'))))))))
| ~ 'E'(f(X3),s(s(s(s('0')))))
| ~ 'E'(f(X2),s(s(s(s(s(s(s(s(s(s('0')))))))))))
| ~ 'E'(f(X1),s(s(s(s(s('0'))))))
| ~ 'E'(f(X0),s(s(s(s(s(s(s(s('0'))))))))) ),
inference(cnf_transformation,[status(thm)],[f60]) ).
fof(f62,plain,
! [B_0] :
( 'E'(f(B_0),s(s(s(s(s('0'))))))
| ! [A_3] : ~ 'E'(f(A_3),s(s(s(s(s(s('0')))))))
| ! [A_0] : ~ 'E'(f(A_0),s(s(s(s(s(s(s(s(s('0'))))))))))
| ! [A_2] : ~ 'E'(f(A_2),s(s(s(s(s(s(s('0'))))))))
| ~ 'E'(f(B_0),s(s(s(s(s(s(s(s(s(s('0')))))))))))
| ! [A_1] : ~ 'E'(f(A_1),s(s(s(s(s(s(s(s('0'))))))))) ),
inference(miniscoping,[status(thm)],[f20]) ).
fof(f63,plain,
! [E,X0,X1,X2,X3,X4] :
( 'E'(f(X1),s(s(s(s(s('0'))))))
| ~ 'E'(f(X4),s(s(s(s(s(s('0')))))))
| ~ 'E'(f(X3),s(s(s(s(s(s(s(s(s('0'))))))))))
| ~ 'E'(f(X2),s(s(s(s(s(s(s('0'))))))))
| ~ 'E'(f(X1),s(s(s(s(s(s(s(s(s(s('0')))))))))))
| ~ 'E'(f(X0),s(s(s(s(s(s(s(s('0'))))))))) ),
inference(cnf_transformation,[status(thm)],[f62]) ).
fof(f66,plain,
( ! [K] : 'E'(f('AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),K)),'0')
| ! [A_3] : ~ 'E'(f(A_3),s(s(s(s(s(s('0')))))))
| ! [A_0] : ~ 'E'(f(A_0),s(s(s(s(s(s(s(s(s('0'))))))))))
| ! [A_6] : ~ 'E'(f(A_6),s(s(s('0'))))
| ! [A_2] : ~ 'E'(f(A_2),s(s(s(s(s(s(s('0'))))))))
| ! [A_7] : ~ 'E'(f(A_7),s(s('0')))
| ! [A_5] : ~ 'E'(f(A_5),s(s(s(s('0')))))
| ! [B_0] : ~ 'E'(f(B_0),s(s(s(s(s(s(s(s(s(s('0')))))))))))
| ! [A_8] : ~ 'E'(f(A_8),s('0'))
| ! [A_4] : ~ 'E'(f(A_4),s(s(s(s(s('0'))))))
| ! [A_1] : ~ 'E'(f(A_1),s(s(s(s(s(s(s(s('0'))))))))) ),
inference(miniscoping,[status(thm)],[f22]) ).
fof(f67,plain,
! [E,X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,AP,X10] :
( 'E'(f('AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),X10)),'0')
| ~ 'E'(f(X9),s(s(s(s(s(s('0')))))))
| ~ 'E'(f(X8),s(s(s(s(s(s(s(s(s('0'))))))))))
| ~ 'E'(f(X7),s(s(s('0'))))
| ~ 'E'(f(X6),s(s(s(s(s(s(s('0'))))))))
| ~ 'E'(f(X5),s(s('0')))
| ~ 'E'(f(X4),s(s(s(s('0')))))
| ~ 'E'(f(X3),s(s(s(s(s(s(s(s(s(s('0')))))))))))
| ~ 'E'(f(X2),s('0'))
| ~ 'E'(f(X1),s(s(s(s(s('0'))))))
| ~ 'E'(f(X0),s(s(s(s(s(s(s(s('0'))))))))) ),
inference(cnf_transformation,[status(thm)],[f66]) ).
fof(f70,definition,
! [E,X0] :
( sQ0_spl
<=> ~ 'E'(f(X0),s(s(s(s(s(s(s(s(s('0')))))))))) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f71,plain,
! [E,X0] :
( ~ sQ0_spl
| ~ 'E'(f(X0),s(s(s(s(s(s(s(s(s('0')))))))))) ),
inference(component_clause,[status(thm)],[f70]) ).
fof(f73,definition,
! [E,X1] :
( sQ1_spl
<=> ( 'E'(f(X1),s(s(s(s(s(s(s(s('0')))))))))
| ~ 'E'(f(X1),s(s(s(s(s(s(s(s(s(s('0'))))))))))) ) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f74,plain,
! [E,X0] :
( ~ sQ1_spl
| 'E'(f(X0),s(s(s(s(s(s(s(s('0')))))))))
| ~ 'E'(f(X0),s(s(s(s(s(s(s(s(s(s('0'))))))))))) ),
inference(component_clause,[status(thm)],[f73]) ).
fof(f76,plain,
( sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f25,f70,f73]) ).
fof(f77,definition,
! [E,X0] :
( sQ2_spl
<=> ~ 'E'(f(X0),s(s(s(s(s(s(s(s('0'))))))))) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f78,plain,
! [E,X0] :
( ~ sQ2_spl
| ~ 'E'(f(X0),s(s(s(s(s(s(s(s('0'))))))))) ),
inference(component_clause,[status(thm)],[f77]) ).
fof(f80,definition,
! [E,X1] :
( sQ3_spl
<=> ~ 'E'(f(X1),s(s(s(s(s('0')))))) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f81,plain,
! [E,X0] :
( ~ sQ3_spl
| ~ 'E'(f(X0),s(s(s(s(s('0')))))) ),
inference(component_clause,[status(thm)],[f80]) ).
fof(f83,definition,
! [E,X2] :
( sQ4_spl
<=> ~ 'E'(f(X2),s('0')) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f84,plain,
! [E,X0] :
( ~ sQ4_spl
| ~ 'E'(f(X0),s('0')) ),
inference(component_clause,[status(thm)],[f83]) ).
fof(f86,definition,
! [E,X3] :
( sQ5_spl
<=> ~ 'E'(f(X3),s(s(s(s(s(s(s(s(s(s('0'))))))))))) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f87,plain,
! [E,X0] :
( ~ sQ5_spl
| ~ 'E'(f(X0),s(s(s(s(s(s(s(s(s(s('0'))))))))))) ),
inference(component_clause,[status(thm)],[f86]) ).
fof(f89,definition,
! [E,X4] :
( sQ6_spl
<=> ~ 'E'(f(X4),s(s(s(s('0'))))) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f90,plain,
! [E,X0] :
( ~ sQ6_spl
| ~ 'E'(f(X0),s(s(s(s('0'))))) ),
inference(component_clause,[status(thm)],[f89]) ).
fof(f92,definition,
! [E,X5] :
( sQ7_spl
<=> ~ 'E'(f(X5),s(s('0'))) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f93,plain,
! [E,X0] :
( ~ sQ7_spl
| ~ 'E'(f(X0),s(s('0'))) ),
inference(component_clause,[status(thm)],[f92]) ).
fof(f95,definition,
! [E,X6] :
( sQ8_spl
<=> ~ 'E'(f(X6),s(s(s(s(s(s(s('0')))))))) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f96,plain,
! [E,X0] :
( ~ sQ8_spl
| ~ 'E'(f(X0),s(s(s(s(s(s(s('0')))))))) ),
inference(component_clause,[status(thm)],[f95]) ).
fof(f98,definition,
! [E,X7] :
( sQ9_spl
<=> ~ 'E'(f(X7),s(s(s('0')))) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f99,plain,
! [E,X0] :
( ~ sQ9_spl
| ~ 'E'(f(X0),s(s(s('0')))) ),
inference(component_clause,[status(thm)],[f98]) ).
fof(f101,definition,
! [E,X9] :
( sQ10_spl
<=> ~ 'E'(f(X9),s(s(s(s(s(s('0'))))))) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f102,plain,
! [E,X0] :
( ~ sQ10_spl
| ~ 'E'(f(X0),s(s(s(s(s(s('0'))))))) ),
inference(component_clause,[status(thm)],[f101]) ).
fof(f116,definition,
! [E,X1] :
( sQ14_spl
<=> ( 'E'(f(X1),s(s(s(s(s(s('0')))))))
| ~ 'E'(f(X1),s(s(s(s(s(s(s(s(s(s('0'))))))))))) ) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f117,plain,
! [E,X0] :
( ~ sQ14_spl
| 'E'(f(X0),s(s(s(s(s(s('0')))))))
| ~ 'E'(f(X0),s(s(s(s(s(s(s(s(s(s('0'))))))))))) ),
inference(component_clause,[status(thm)],[f116]) ).
fof(f119,plain,
( sQ8_spl
| sQ2_spl
| sQ14_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f35,f70,f116,f77,f95]) ).
fof(f132,definition,
! [E,AP,X9] :
( sQ18_spl
<=> 'E'(f('AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),X9)),s('0')) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f133,plain,
! [E,AP,X0] :
( ~ sQ18_spl
| 'E'(f('AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),X0)),s('0')) ),
inference(component_clause,[status(thm)],[f132]) ).
fof(f135,plain,
( sQ18_spl
| sQ10_spl
| sQ0_spl
| sQ9_spl
| sQ8_spl
| sQ7_spl
| sQ6_spl
| sQ5_spl
| sQ3_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f45,f77,f80,f86,f89,f92,f95,f98,f70,f101,f132]) ).
fof(f136,definition,
! [E,AP,X6] :
( sQ19_spl
<=> 'E'(f('AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),X6)),s(s(s(s('0'))))) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f137,plain,
! [E,AP,X0] :
( ~ sQ19_spl
| 'E'(f('AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),X0)),s(s(s(s('0'))))) ),
inference(component_clause,[status(thm)],[f136]) ).
fof(f139,plain,
( sQ19_spl
| sQ10_spl
| sQ0_spl
| sQ8_spl
| sQ5_spl
| sQ3_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f47,f77,f80,f86,f95,f70,f101,f136]) ).
fof(f140,definition,
! [E,X1] :
( sQ20_spl
<=> ( 'E'(f(X1),s(s(s(s(s(s(s('0'))))))))
| ~ 'E'(f(X1),s(s(s(s(s(s(s(s(s(s('0'))))))))))) ) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f141,plain,
! [E,X0] :
( ~ sQ20_spl
| 'E'(f(X0),s(s(s(s(s(s(s('0'))))))))
| ~ 'E'(f(X0),s(s(s(s(s(s(s(s(s(s('0'))))))))))) ),
inference(component_clause,[status(thm)],[f140]) ).
fof(f143,plain,
( sQ2_spl
| sQ20_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f51,f70,f140,f77]) ).
fof(f144,definition,
! [E,AP,X7] :
( sQ21_spl
<=> 'E'(f('AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),X7)),s(s(s('0')))) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f145,plain,
! [E,AP,X0] :
( ~ sQ21_spl
| 'E'(f('AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),X0)),s(s(s('0')))) ),
inference(component_clause,[status(thm)],[f144]) ).
fof(f147,plain,
( sQ21_spl
| sQ10_spl
| sQ0_spl
| sQ8_spl
| sQ6_spl
| sQ5_spl
| sQ3_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f53,f77,f80,f86,f89,f95,f70,f101,f144]) ).
fof(f152,definition,
! [E,X10] :
( sQ23_spl
<=> ~ 'E'(f(X10),'0') ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f153,plain,
! [E,X0] :
( ~ sQ23_spl
| ~ 'E'(f(X0),'0') ),
inference(component_clause,[status(thm)],[f152]) ).
fof(f155,plain,
( sQ23_spl
| sQ10_spl
| sQ0_spl
| sQ9_spl
| sQ8_spl
| sQ7_spl
| sQ6_spl
| sQ5_spl
| sQ4_spl
| sQ3_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f57,f77,f80,f83,f86,f89,f92,f95,f98,f70,f101,f152]) ).
fof(f160,definition,
! [E,AP,X8] :
( sQ25_spl
<=> 'E'(f('AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),X8)),s(s('0'))) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f161,plain,
! [E,AP,X0] :
( ~ sQ25_spl
| 'E'(f('AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),X0)),s(s('0'))) ),
inference(component_clause,[status(thm)],[f160]) ).
fof(f163,plain,
( sQ25_spl
| sQ10_spl
| sQ0_spl
| sQ9_spl
| sQ8_spl
| sQ6_spl
| sQ5_spl
| sQ3_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f61,f77,f80,f86,f89,f95,f98,f70,f101,f160]) ).
fof(f164,definition,
! [E,X1] :
( sQ26_spl
<=> ( 'E'(f(X1),s(s(s(s(s('0'))))))
| ~ 'E'(f(X1),s(s(s(s(s(s(s(s(s(s('0'))))))))))) ) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f165,plain,
! [E,X0] :
( ~ sQ26_spl
| 'E'(f(X0),s(s(s(s(s('0'))))))
| ~ 'E'(f(X0),s(s(s(s(s(s(s(s(s(s('0'))))))))))) ),
inference(component_clause,[status(thm)],[f164]) ).
fof(f167,plain,
( sQ10_spl
| sQ0_spl
| sQ8_spl
| sQ26_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f63,f77,f164,f95,f70,f101]) ).
fof(f172,definition,
! [E,AP,X10] :
( sQ28_spl
<=> 'E'(f('AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),X10)),'0') ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f173,plain,
! [E,AP,X0] :
( ~ sQ28_spl
| 'E'(f('AP'(s(s(s(s(s(s(s(s(s(s(s('0'))))))))))),X0)),'0') ),
inference(component_clause,[status(thm)],[f172]) ).
fof(f175,plain,
( sQ28_spl
| sQ10_spl
| sQ0_spl
| sQ9_spl
| sQ8_spl
| sQ7_spl
| sQ6_spl
| sQ5_spl
| sQ4_spl
| sQ3_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f67,f77,f80,f83,f86,f89,f92,f95,f98,f70,f101,f172]) ).
fof(f176,plain,
( ~ sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f71,f41]) ).
fof(f177,plain,
~ sQ0_spl,
inference(contradiction_clause,[status(thm)],[f176]) ).
fof(f178,plain,
( ~ sQ2_spl
| ~ sQ1_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f78,f179]) ).
fof(f179,plain,
! [E,X0] :
( ~ sQ1_spl
| 'E'(f(X0),s(s(s(s(s(s(s(s('0'))))))))) ),
inference(forward_subsumption_resolution,[status(thm)],[f74,f29]) ).
fof(f180,plain,
( ~ sQ2_spl
| ~ sQ1_spl ),
inference(contradiction_clause,[status(thm)],[f178]) ).
fof(f181,plain,
! [E,X0] :
( ~ sQ20_spl
| 'E'(f(X0),s(s(s(s(s(s(s('0')))))))) ),
inference(forward_subsumption_resolution,[status(thm)],[f141,f29]) ).
fof(f184,plain,
( ~ sQ20_spl
| ~ sQ8_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f181,f96]) ).
fof(f185,plain,
( ~ sQ20_spl
| ~ sQ8_spl ),
inference(contradiction_clause,[status(thm)],[f184]) ).
fof(f186,plain,
! [E,X0] :
( ~ sQ14_spl
| 'E'(f(X0),s(s(s(s(s(s('0'))))))) ),
inference(forward_subsumption_resolution,[status(thm)],[f117,f29]) ).
fof(f188,plain,
( ~ sQ14_spl
| ~ sQ10_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f186,f102]) ).
fof(f189,plain,
( ~ sQ14_spl
| ~ sQ10_spl ),
inference(contradiction_clause,[status(thm)],[f188]) ).
fof(f190,plain,
( ~ sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f87,f29]) ).
fof(f191,plain,
~ sQ5_spl,
inference(contradiction_clause,[status(thm)],[f190]) ).
fof(f192,plain,
! [E,X0] :
( ~ sQ26_spl
| 'E'(f(X0),s(s(s(s(s('0')))))) ),
inference(forward_subsumption_resolution,[status(thm)],[f165,f29]) ).
fof(f194,plain,
( ~ sQ3_spl
| ~ sQ26_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f81,f192]) ).
fof(f195,plain,
( ~ sQ3_spl
| ~ sQ26_spl ),
inference(contradiction_clause,[status(thm)],[f194]) ).
fof(f196,plain,
( ~ sQ19_spl
| ~ sQ6_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f137,f90]) ).
fof(f197,plain,
( ~ sQ19_spl
| ~ sQ6_spl ),
inference(contradiction_clause,[status(thm)],[f196]) ).
fof(f198,plain,
( ~ sQ21_spl
| ~ sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f145,f99]) ).
fof(f199,plain,
( ~ sQ21_spl
| ~ sQ9_spl ),
inference(contradiction_clause,[status(thm)],[f198]) ).
fof(f200,plain,
( ~ sQ25_spl
| ~ sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f161,f93]) ).
fof(f201,plain,
( ~ sQ25_spl
| ~ sQ7_spl ),
inference(contradiction_clause,[status(thm)],[f200]) ).
fof(f202,plain,
( ~ sQ18_spl
| ~ sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f133,f84]) ).
fof(f203,plain,
( ~ sQ18_spl
| ~ sQ4_spl ),
inference(contradiction_clause,[status(thm)],[f202]) ).
fof(f204,plain,
( ~ sQ28_spl
| ~ sQ23_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f173,f153]) ).
fof(f205,plain,
( ~ sQ28_spl
| ~ sQ23_spl ),
inference(contradiction_clause,[status(thm)],[f204]) ).
fof(f206,plain,
$false,
inference(sat_refutation,[status(thm)],[f76,f119,f135,f139,f143,f147,f155,f163,f167,f175,f177,f180,f185,f189,f191,f195,f197,f199,f201,f203,f205]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO634-1 : TPTP v9.3.1. Released v7.1.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.12/5.38 % Computer : n016.cluster.edu
% 0.12/5.38 % Model : x86_64 x86_64
% 0.12/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/5.38 % Memory : 8046.5625MB
% 0.12/5.38 % OS : Linux 6.8.0-71-generic
% 0.12/5.38 % CPULimit : 300
% 0.12/5.38 % WCLimit : 300
% 0.12/5.38 % DateTime : Mon Sep 21 12:11:14 UTC 2026
% 0.12/5.38 % CPUTime :
% 0.12/5.39 % Drodi V4.1.1
% 0.16/5.41 % Refutation found
% 0.16/5.41 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.16/5.41 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.16/5.43 % Elapsed time: 0.043629 seconds
% 0.16/5.43 % CPU time: 0.102437 seconds
% 0.16/5.43 % Total memory used: 5.895 MB
% 0.16/5.43 % Net memory used: 5.705 MB
%------------------------------------------------------------------------------