%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SYN314-1.002.001 : TPTP v9.3.1. Released v1.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n010.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:42 PM UTC 2026
% Result : Unsatisfiable 91.55s 12.02s
% Output : CNFRefutation 91.55s
% Verified :
% SZS Type : Refutation
% Derivation depth : 64
% Number of leaves : 2
% Syntax : Number of formulae : 68 ( 5 unt; 0 def)
% Number of atoms : 265 ( 0 equ)
% Maximal formula atoms : 9 ( 3 avg)
% Number of connectives : 429 ( 232 ~; 197 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 8 avg)
% Maximal term depth : 13 ( 3 avg)
% Number of predicates : 2 ( 1 usr; 1 prp; 0-4 aty)
% Number of functors : 10 ( 10 usr; 1 con; 0-1 aty)
% Number of variables : 242 ( 242 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,negated_conjecture,
! [X0,X1,X3,X2] :
( p(X0,f2(X2),X3,g2(X3))
| p(X0,f1(X1),X2,g1(X3))
| p(X0,f0(X0),X1,g0(X3)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
! [Y0,Y1,Y2,Y3] :
( ~ p(h1(Y0),Y1,j1(Y2),Y3)
| ~ p(h0,Y0,j0(Y1),Y2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,plain,
! [X0,X3,X2] :
( p(X0,f2(X2),X3,g2(X3))
| ! [X1] :
( p(X0,f1(X1),X2,g1(X3))
| p(X0,f0(X0),X1,g0(X3)) ) ),
inference(miniscoping,[status(thm)],[f1]) ).
fof(f4,plain,
! [X0,X1,X2,X3] :
( p(X0,f2(X3),X2,g2(X2))
| p(X0,f1(X1),X3,g1(X2))
| p(X0,f0(X0),X1,g0(X2)) ),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f5,plain,
! [Y0,Y1,Y2] :
( ! [Y3] : ~ p(h1(Y0),Y1,j1(Y2),Y3)
| ~ p(h0,Y0,j0(Y1),Y2) ),
inference(miniscoping,[status(thm)],[f2]) ).
fof(f6,plain,
! [X0,X1,X2,X3] :
( ~ p(h1(X0),X1,j1(X2),X3)
| ~ p(h0,X0,j0(X1),X2) ),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f7,plain,
! [X0,X1,X2,X3] :
( ~ p(h0,X0,j0(f0(h1(X0))),X1)
| p(h1(X0),f2(X2),X3,g2(X3))
| p(h1(X0),f1(j1(X1)),X2,g1(X3)) ),
inference(resolution,[status(thm)],[f4,f6]) ).
fof(f8,plain,
! [X0,X1,X2,X3] :
( ~ p(h0,X0,j0(f1(j1(X3))),X1)
| ~ p(h0,X0,j0(f0(h1(X0))),X3)
| p(h1(X0),f2(j1(X1)),X2,g2(X2)) ),
inference(resolution,[status(thm)],[f7,f6]) ).
fof(f9,plain,
! [X0,X1,X2,X3] :
( ~ p(h0,X0,j0(f2(j1(X2))),X3)
| ~ p(h0,X0,j0(f1(j1(X1))),X2)
| ~ p(h0,X0,j0(f0(h1(X0))),X1) ),
inference(resolution,[status(thm)],[f8,f6]) ).
fof(f12,plain,
! [X0,X1,X2,X3] :
( p(h0,f2(X2),X3,g2(X3))
| p(h0,f1(j0(f2(j1(X1)))),X2,g1(X3))
| ~ p(h0,f0(h0),j0(f1(j1(X0))),X1)
| ~ p(h0,f0(h0),j0(f0(h1(f0(h0)))),X0) ),
inference(resolution,[status(thm)],[f9,f4]) ).
fof(f13,plain,
! [X0,X1,X2,X3,X4] :
( ~ p(h0,f1(j0(f2(j1(X1)))),j0(f1(j1(X4))),X2)
| ~ p(h0,f1(j0(f2(j1(X1)))),j0(f0(h1(f1(j0(f2(j1(X1))))))),X4)
| p(h0,f2(j0(f2(j1(X2)))),X3,g2(X3))
| ~ p(h0,f0(h0),j0(f1(j1(X0))),X1)
| ~ p(h0,f0(h0),j0(f0(h1(f0(h0)))),X0) ),
inference(resolution,[status(thm)],[f12,f9]) ).
fof(f22,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ p(h0,f2(j0(f2(j1(X3)))),j0(f1(j1(X4))),X5)
| ~ p(h0,f2(j0(f2(j1(X3)))),j0(f0(h1(f2(j0(f2(j1(X3))))))),X4)
| ~ p(h0,f1(j0(f2(j1(X1)))),j0(f1(j1(X2))),X3)
| ~ p(h0,f1(j0(f2(j1(X1)))),j0(f0(h1(f1(j0(f2(j1(X1))))))),X2)
| ~ p(h0,f0(h0),j0(f1(j1(X0))),X1)
| ~ p(h0,f0(h0),j0(f0(h1(f0(h0)))),X0) ),
inference(resolution,[status(thm)],[f13,f9]) ).
fof(f55,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ p(h0,f1(j0(f2(j1(X6)))),j0(f1(j1(X7))),X3)
| ~ p(h0,f1(j0(f2(j1(X6)))),j0(f0(h1(f1(j0(f2(j1(X6))))))),X7)
| ~ p(h0,f0(h0),j0(f1(j1(X5))),X6)
| ~ p(h0,f0(h0),j0(f0(h1(f0(h0)))),X5)
| ~ p(h0,f2(j0(f2(j1(X3)))),j0(f1(j1(g2(j0(f0(h1(f2(j0(f2(j1(X3))))))))))),X4)
| ~ p(h0,f1(j0(f2(j1(X1)))),j0(f1(j1(X2))),X3)
| ~ p(h0,f1(j0(f2(j1(X1)))),j0(f0(h1(f1(j0(f2(j1(X1))))))),X2)
| ~ p(h0,f0(h0),j0(f1(j1(X0))),X1)
| ~ p(h0,f0(h0),j0(f0(h1(f0(h0)))),X0) ),
inference(resolution,[status(thm)],[f22,f13]) ).
fof(f1785,plain,
! [X0,X1,X2,X3,X4] :
( ~ p(h0,f2(j0(f2(j1(X3)))),j0(f1(j1(g2(j0(f0(h1(f2(j0(f2(j1(X3))))))))))),X4)
| ~ p(h0,f1(j0(f2(j1(X1)))),j0(f1(j1(X2))),X3)
| ~ p(h0,f1(j0(f2(j1(X1)))),j0(f0(h1(f1(j0(f2(j1(X1))))))),X2)
| ~ p(h0,f0(h0),j0(f1(j1(X0))),X1)
| ~ p(h0,f0(h0),j0(f0(h1(f0(h0)))),X0) ),
inference(factoring,[status(thm)],[f55]) ).
fof(f1853,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ~ p(h0,f1(j0(f2(j1(X5)))),j0(f1(j1(X6))),X3)
| ~ p(h0,f1(j0(f2(j1(X5)))),j0(f0(h1(f1(j0(f2(j1(X5))))))),X6)
| ~ p(h0,f0(h0),j0(f1(j1(X4))),X5)
| ~ p(h0,f0(h0),j0(f0(h1(f0(h0)))),X4)
| ~ p(h0,f1(j0(f2(j1(X1)))),j0(f1(j1(X2))),X3)
| ~ p(h0,f1(j0(f2(j1(X1)))),j0(f0(h1(f1(j0(f2(j1(X1))))))),X2)
| ~ p(h0,f0(h0),j0(f1(j1(X0))),X1)
| ~ p(h0,f0(h0),j0(f0(h1(f0(h0)))),X0) ),
inference(resolution,[status(thm)],[f1785,f13]) ).
fof(f2033,plain,
! [X0,X1,X2,X3] :
( ~ p(h0,f1(j0(f2(j1(X1)))),j0(f1(j1(X2))),X3)
| ~ p(h0,f1(j0(f2(j1(X1)))),j0(f0(h1(f1(j0(f2(j1(X1))))))),X2)
| ~ p(h0,f0(h0),j0(f1(j1(X0))),X1)
| ~ p(h0,f0(h0),j0(f0(h1(f0(h0)))),X0) ),
inference(factoring,[status(thm)],[f1853]) ).
fof(f2092,plain,
! [X0,X1,X2,X3,X4] :
( p(h0,f2(j0(f1(j1(X2)))),X4,g2(X4))
| ~ p(h0,f0(h0),j0(f1(j1(X3))),X1)
| ~ p(h0,f0(h0),j0(f0(h1(f0(h0)))),X3)
| ~ p(h0,f1(j0(f2(j1(X1)))),j0(f0(h1(f1(j0(f2(j1(X1))))))),X2)
| ~ p(h0,f0(h0),j0(f1(j1(X0))),X1)
| ~ p(h0,f0(h0),j0(f0(h1(f0(h0)))),X0) ),
inference(resolution,[status(thm)],[f2033,f12]) ).
fof(f2170,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ p(h0,f2(j0(f1(j1(X2)))),j0(f1(j1(X4))),X5)
| ~ p(h0,f2(j0(f1(j1(X2)))),j0(f0(h1(f2(j0(f1(j1(X2))))))),X4)
| ~ p(h0,f0(h0),j0(f1(j1(X3))),X1)
| ~ p(h0,f0(h0),j0(f0(h1(f0(h0)))),X3)
| ~ p(h0,f1(j0(f2(j1(X1)))),j0(f0(h1(f1(j0(f2(j1(X1))))))),X2)
| ~ p(h0,f0(h0),j0(f1(j1(X0))),X1)
| ~ p(h0,f0(h0),j0(f0(h1(f0(h0)))),X0) ),
inference(resolution,[status(thm)],[f2092,f9]) ).
fof(f2326,plain,
! [X0,X1,X2,X3,X4] :
( ~ p(h0,f2(j0(f1(j1(X2)))),j0(f1(j1(X3))),X4)
| ~ p(h0,f2(j0(f1(j1(X2)))),j0(f0(h1(f2(j0(f1(j1(X2))))))),X3)
| ~ p(h0,f1(j0(f2(j1(X1)))),j0(f0(h1(f1(j0(f2(j1(X1))))))),X2)
| ~ p(h0,f0(h0),j0(f1(j1(X0))),X1)
| ~ p(h0,f0(h0),j0(f0(h1(f0(h0)))),X0) ),
inference(factoring,[status(thm)],[f2170]) ).
fof(f2359,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ~ p(h0,f0(h0),j0(f1(j1(X6))),X5)
| ~ p(h0,f0(h0),j0(f0(h1(f0(h0)))),X6)
| ~ p(h0,f1(j0(f2(j1(X5)))),j0(f0(h1(f1(j0(f2(j1(X5))))))),X2)
| ~ p(h0,f0(h0),j0(f1(j1(X4))),X5)
| ~ p(h0,f0(h0),j0(f0(h1(f0(h0)))),X4)
| ~ p(h0,f2(j0(f1(j1(X2)))),j0(f0(h1(f2(j0(f1(j1(X2))))))),X3)
| ~ p(h0,f1(j0(f2(j1(X1)))),j0(f0(h1(f1(j0(f2(j1(X1))))))),X2)
| ~ p(h0,f0(h0),j0(f1(j1(X0))),X1)
| ~ p(h0,f0(h0),j0(f0(h1(f0(h0)))),X0) ),
inference(resolution,[status(thm)],[f2326,f2092]) ).
fof(f4815,plain,
! [X0,X1,X2,X3] :
( ~ p(h0,f2(j0(f1(j1(X2)))),j0(f0(h1(f2(j0(f1(j1(X2))))))),X3)
| ~ p(h0,f1(j0(f2(j1(X1)))),j0(f0(h1(f1(j0(f2(j1(X1))))))),X2)
| ~ p(h0,f0(h0),j0(f1(j1(X0))),X1)
| ~ p(h0,f0(h0),j0(f0(h1(f0(h0)))),X0) ),
inference(factoring,[status(thm)],[f2359]) ).
fof(f4852,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ p(h0,f0(h0),j0(f1(j1(X5))),X4)
| ~ p(h0,f0(h0),j0(f0(h1(f0(h0)))),X5)
| ~ p(h0,f1(j0(f2(j1(X4)))),j0(f0(h1(f1(j0(f2(j1(X4))))))),X2)
| ~ p(h0,f0(h0),j0(f1(j1(X3))),X4)
| ~ p(h0,f0(h0),j0(f0(h1(f0(h0)))),X3)
| ~ p(h0,f1(j0(f2(j1(X1)))),j0(f0(h1(f1(j0(f2(j1(X1))))))),X2)
| ~ p(h0,f0(h0),j0(f1(j1(X0))),X1)
| ~ p(h0,f0(h0),j0(f0(h1(f0(h0)))),X0) ),
inference(resolution,[status(thm)],[f4815,f2092]) ).
fof(f5322,plain,
! [X0,X1,X2] :
( ~ p(h0,f1(j0(f2(j1(X1)))),j0(f0(h1(f1(j0(f2(j1(X1))))))),X2)
| ~ p(h0,f0(h0),j0(f1(j1(X0))),X1)
| ~ p(h0,f0(h0),j0(f0(h1(f0(h0)))),X0) ),
inference(factoring,[status(thm)],[f4852]) ).
fof(f5343,plain,
! [X0,X1,X2,X3] :
( p(h0,f2(j0(f0(h1(f1(j0(f2(j1(X1)))))))),X3,g2(X3))
| ~ p(h0,f0(h0),j0(f1(j1(X2))),X1)
| ~ p(h0,f0(h0),j0(f0(h1(f0(h0)))),X2)
| ~ p(h0,f0(h0),j0(f1(j1(X0))),X1)
| ~ p(h0,f0(h0),j0(f0(h1(f0(h0)))),X0) ),
inference(resolution,[status(thm)],[f5322,f12]) ).
fof(f5425,plain,
! [X0,X1,X2,X3,X4] :
( ~ p(h0,f2(j0(f0(h1(f1(j0(f2(j1(X1)))))))),j0(f1(j1(X3))),X4)
| ~ p(h0,f2(j0(f0(h1(f1(j0(f2(j1(X1)))))))),j0(f0(h1(f2(j0(f0(h1(f1(j0(f2(j1(X1))))))))))),X3)
| ~ p(h0,f0(h0),j0(f1(j1(X2))),X1)
| ~ p(h0,f0(h0),j0(f0(h1(f0(h0)))),X2)
| ~ p(h0,f0(h0),j0(f1(j1(X0))),X1)
| ~ p(h0,f0(h0),j0(f0(h1(f0(h0)))),X0) ),
inference(resolution,[status(thm)],[f5343,f9]) ).
fof(f5699,plain,
! [X0,X1,X2,X3] :
( ~ p(h0,f2(j0(f0(h1(f1(j0(f2(j1(X1)))))))),j0(f1(j1(X2))),X3)
| ~ p(h0,f2(j0(f0(h1(f1(j0(f2(j1(X1)))))))),j0(f0(h1(f2(j0(f0(h1(f1(j0(f2(j1(X1))))))))))),X2)
| ~ p(h0,f0(h0),j0(f1(j1(X0))),X1)
| ~ p(h0,f0(h0),j0(f0(h1(f0(h0)))),X0) ),
inference(factoring,[status(thm)],[f5425]) ).
fof(f5706,plain,
! [X0,X1,X2,X3,X4] :
( ~ p(h0,f0(h0),j0(f1(j1(X4))),X1)
| ~ p(h0,f0(h0),j0(f0(h1(f0(h0)))),X4)
| ~ p(h0,f0(h0),j0(f1(j1(X3))),X1)
| ~ p(h0,f0(h0),j0(f0(h1(f0(h0)))),X3)
| ~ p(h0,f2(j0(f0(h1(f1(j0(f2(j1(X1)))))))),j0(f0(h1(f2(j0(f0(h1(f1(j0(f2(j1(X1))))))))))),X2)
| ~ p(h0,f0(h0),j0(f1(j1(X0))),X1)
| ~ p(h0,f0(h0),j0(f0(h1(f0(h0)))),X0) ),
inference(resolution,[status(thm)],[f5699,f5343]) ).
fof(f5866,plain,
! [X0,X1,X2] :
( ~ p(h0,f2(j0(f0(h1(f1(j0(f2(j1(X1)))))))),j0(f0(h1(f2(j0(f0(h1(f1(j0(f2(j1(X1))))))))))),X2)
| ~ p(h0,f0(h0),j0(f1(j1(X0))),X1)
| ~ p(h0,f0(h0),j0(f0(h1(f0(h0)))),X0) ),
inference(factoring,[status(thm)],[f5706]) ).
fof(f5873,plain,
! [X0,X1,X2,X3] :
( ~ p(h0,f0(h0),j0(f1(j1(X3))),X1)
| ~ p(h0,f0(h0),j0(f0(h1(f0(h0)))),X3)
| ~ p(h0,f0(h0),j0(f1(j1(X2))),X1)
| ~ p(h0,f0(h0),j0(f0(h1(f0(h0)))),X2)
| ~ p(h0,f0(h0),j0(f1(j1(X0))),X1)
| ~ p(h0,f0(h0),j0(f0(h1(f0(h0)))),X0) ),
inference(resolution,[status(thm)],[f5866,f5343]) ).
fof(f5986,plain,
! [X0,X1,X2] :
( p(h0,f2(X1),X2,g2(X2))
| p(h0,f1(j0(f1(j1(X0)))),X1,g1(X2))
| ~ p(h0,f0(h0),j0(f0(h1(f0(h0)))),X0)
| ~ p(h0,f0(h0),j0(f0(h1(f0(h0)))),X0)
| ~ p(h0,f0(h0),j0(f0(h1(f0(h0)))),X0) ),
inference(resolution,[status(thm)],[f5873,f4]) ).
fof(f5996,plain,
! [X0,X1,X2] :
( p(h0,f2(X1),X2,g2(X2))
| p(h0,f1(j0(f1(j1(X0)))),X1,g1(X2))
| ~ p(h0,f0(h0),j0(f0(h1(f0(h0)))),X0) ),
inference(duplicate_literals_removal,[status(thm)],[f5986]) ).
fof(f6033,plain,
! [X0,X1,X2,X3] :
( ~ p(h0,f1(j0(f1(j1(X0)))),j0(f1(j1(X3))),X1)
| ~ p(h0,f1(j0(f1(j1(X0)))),j0(f0(h1(f1(j0(f1(j1(X0))))))),X3)
| p(h0,f2(j0(f2(j1(X1)))),X2,g2(X2))
| ~ p(h0,f0(h0),j0(f0(h1(f0(h0)))),X0) ),
inference(resolution,[status(thm)],[f5996,f9]) ).
fof(f6170,plain,
! [X0,X1,X2,X3,X4] :
( ~ p(h0,f2(j0(f2(j1(X2)))),j0(f1(j1(X3))),X4)
| ~ p(h0,f2(j0(f2(j1(X2)))),j0(f0(h1(f2(j0(f2(j1(X2))))))),X3)
| ~ p(h0,f1(j0(f1(j1(X0)))),j0(f1(j1(X1))),X2)
| ~ p(h0,f1(j0(f1(j1(X0)))),j0(f0(h1(f1(j0(f1(j1(X0))))))),X1)
| ~ p(h0,f0(h0),j0(f0(h1(f0(h0)))),X0) ),
inference(resolution,[status(thm)],[f6033,f9]) ).
fof(f6291,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ p(h0,f1(j0(f1(j1(X4)))),j0(f1(j1(X5))),X2)
| ~ p(h0,f1(j0(f1(j1(X4)))),j0(f0(h1(f1(j0(f1(j1(X4))))))),X5)
| ~ p(h0,f0(h0),j0(f0(h1(f0(h0)))),X4)
| ~ p(h0,f2(j0(f2(j1(X2)))),j0(f0(h1(f2(j0(f2(j1(X2))))))),X3)
| ~ p(h0,f1(j0(f1(j1(X0)))),j0(f1(j1(X1))),X2)
| ~ p(h0,f1(j0(f1(j1(X0)))),j0(f0(h1(f1(j0(f1(j1(X0))))))),X1)
| ~ p(h0,f0(h0),j0(f0(h1(f0(h0)))),X0) ),
inference(resolution,[status(thm)],[f6170,f6033]) ).
fof(f7832,plain,
! [X0,X1,X2,X3] :
( ~ p(h0,f0(h0),j0(f0(h1(f0(h0)))),X0)
| ~ p(h0,f2(j0(f2(j1(X2)))),j0(f0(h1(f2(j0(f2(j1(X2))))))),X3)
| ~ p(h0,f1(j0(f1(j1(X0)))),j0(f1(j1(X1))),X2)
| ~ p(h0,f1(j0(f1(j1(X0)))),j0(f0(h1(f1(j0(f1(j1(X0))))))),X1)
| ~ p(h0,f0(h0),j0(f0(h1(f0(h0)))),X0) ),
inference(factoring,[status(thm)],[f6291]) ).
fof(f7849,plain,
! [X0,X1,X2,X3] :
( ~ p(h0,f2(j0(f2(j1(X2)))),j0(f0(h1(f2(j0(f2(j1(X2))))))),X3)
| ~ p(h0,f1(j0(f1(j1(X0)))),j0(f1(j1(X1))),X2)
| ~ p(h0,f1(j0(f1(j1(X0)))),j0(f0(h1(f1(j0(f1(j1(X0))))))),X1)
| ~ p(h0,f0(h0),j0(f0(h1(f0(h0)))),X0) ),
inference(duplicate_literals_removal,[status(thm)],[f7832]) ).
fof(f7903,plain,
! [X0,X1,X2,X3,X4] :
( ~ p(h0,f1(j0(f1(j1(X3)))),j0(f1(j1(X4))),X2)
| ~ p(h0,f1(j0(f1(j1(X3)))),j0(f0(h1(f1(j0(f1(j1(X3))))))),X4)
| ~ p(h0,f0(h0),j0(f0(h1(f0(h0)))),X3)
| ~ p(h0,f1(j0(f1(j1(X0)))),j0(f1(j1(X1))),X2)
| ~ p(h0,f1(j0(f1(j1(X0)))),j0(f0(h1(f1(j0(f1(j1(X0))))))),X1)
| ~ p(h0,f0(h0),j0(f0(h1(f0(h0)))),X0) ),
inference(resolution,[status(thm)],[f7849,f6033]) ).
fof(f7928,plain,
! [X0,X1,X2] :
( p(h0,f2(j0(f1(j1(X1)))),X2,g2(X2))
| ~ p(h0,f0(h0),j0(f0(h1(f0(h0)))),X0)
| ~ p(h0,f1(j0(f1(j1(X0)))),j0(f0(h1(f1(j0(f1(j1(X0))))))),X1)
| ~ p(h0,f0(h0),j0(f0(h1(f0(h0)))),X0)
| ~ p(h0,f1(j0(f1(j1(X0)))),j0(f0(h1(f1(j0(f1(j1(X0))))))),X1)
| ~ p(h0,f0(h0),j0(f0(h1(f0(h0)))),X0) ),
inference(resolution,[status(thm)],[f7903,f5996]) ).
fof(f7955,plain,
! [X0,X1,X2] :
( p(h0,f2(j0(f1(j1(X1)))),X2,g2(X2))
| ~ p(h0,f1(j0(f1(j1(X0)))),j0(f0(h1(f1(j0(f1(j1(X0))))))),X1)
| ~ p(h0,f0(h0),j0(f0(h1(f0(h0)))),X0) ),
inference(duplicate_literals_removal,[status(thm)],[f7928]) ).
fof(f7974,plain,
! [X0,X1,X2,X3] :
( ~ p(h0,f2(j0(f1(j1(X1)))),j0(f1(j1(X2))),X3)
| ~ p(h0,f2(j0(f1(j1(X1)))),j0(f0(h1(f2(j0(f1(j1(X1))))))),X2)
| ~ p(h0,f1(j0(f1(j1(X0)))),j0(f0(h1(f1(j0(f1(j1(X0))))))),X1)
| ~ p(h0,f0(h0),j0(f0(h1(f0(h0)))),X0) ),
inference(resolution,[status(thm)],[f7955,f9]) ).
fof(f8022,plain,
! [X0,X1,X2,X3] :
( ~ p(h0,f1(j0(f1(j1(X3)))),j0(f0(h1(f1(j0(f1(j1(X3))))))),X1)
| ~ p(h0,f0(h0),j0(f0(h1(f0(h0)))),X3)
| ~ p(h0,f2(j0(f1(j1(X1)))),j0(f0(h1(f2(j0(f1(j1(X1))))))),X2)
| ~ p(h0,f1(j0(f1(j1(X0)))),j0(f0(h1(f1(j0(f1(j1(X0))))))),X1)
| ~ p(h0,f0(h0),j0(f0(h1(f0(h0)))),X0) ),
inference(resolution,[status(thm)],[f7974,f7955]) ).
fof(f8263,plain,
! [X0,X1,X2] :
( ~ p(h0,f0(h0),j0(f0(h1(f0(h0)))),X0)
| ~ p(h0,f2(j0(f1(j1(X1)))),j0(f0(h1(f2(j0(f1(j1(X1))))))),X2)
| ~ p(h0,f1(j0(f1(j1(X0)))),j0(f0(h1(f1(j0(f1(j1(X0))))))),X1)
| ~ p(h0,f0(h0),j0(f0(h1(f0(h0)))),X0) ),
inference(factoring,[status(thm)],[f8022]) ).
fof(f8272,plain,
! [X0,X1,X2] :
( ~ p(h0,f2(j0(f1(j1(X1)))),j0(f0(h1(f2(j0(f1(j1(X1))))))),X2)
| ~ p(h0,f1(j0(f1(j1(X0)))),j0(f0(h1(f1(j0(f1(j1(X0))))))),X1)
| ~ p(h0,f0(h0),j0(f0(h1(f0(h0)))),X0) ),
inference(duplicate_literals_removal,[status(thm)],[f8263]) ).
fof(f8316,plain,
! [X0,X1,X2] :
( ~ p(h0,f1(j0(f1(j1(X2)))),j0(f0(h1(f1(j0(f1(j1(X2))))))),X1)
| ~ p(h0,f0(h0),j0(f0(h1(f0(h0)))),X2)
| ~ p(h0,f1(j0(f1(j1(X0)))),j0(f0(h1(f1(j0(f1(j1(X0))))))),X1)
| ~ p(h0,f0(h0),j0(f0(h1(f0(h0)))),X0) ),
inference(resolution,[status(thm)],[f8272,f7955]) ).
fof(f8331,plain,
! [X0,X1] :
( p(h0,f2(j0(f0(h1(f1(j0(f1(j1(X0)))))))),X1,g2(X1))
| ~ p(h0,f0(h0),j0(f0(h1(f0(h0)))),X0)
| ~ p(h0,f0(h0),j0(f0(h1(f0(h0)))),X0)
| ~ p(h0,f0(h0),j0(f0(h1(f0(h0)))),X0) ),
inference(resolution,[status(thm)],[f8316,f5996]) ).
fof(f8345,plain,
! [X0,X1] :
( p(h0,f2(j0(f0(h1(f1(j0(f1(j1(X0)))))))),X1,g2(X1))
| ~ p(h0,f0(h0),j0(f0(h1(f0(h0)))),X0) ),
inference(duplicate_literals_removal,[status(thm)],[f8331]) ).
fof(f8355,plain,
! [X0,X1,X2] :
( ~ p(h0,f2(j0(f0(h1(f1(j0(f1(j1(X0)))))))),j0(f1(j1(X1))),X2)
| ~ p(h0,f2(j0(f0(h1(f1(j0(f1(j1(X0)))))))),j0(f0(h1(f2(j0(f0(h1(f1(j0(f1(j1(X0))))))))))),X1)
| ~ p(h0,f0(h0),j0(f0(h1(f0(h0)))),X0) ),
inference(resolution,[status(thm)],[f8345,f9]) ).
fof(f8372,plain,
! [X0,X1] :
( ~ p(h0,f0(h0),j0(f0(h1(f0(h0)))),X0)
| ~ p(h0,f2(j0(f0(h1(f1(j0(f1(j1(X0)))))))),j0(f0(h1(f2(j0(f0(h1(f1(j0(f1(j1(X0))))))))))),X1)
| ~ p(h0,f0(h0),j0(f0(h1(f0(h0)))),X0) ),
inference(resolution,[status(thm)],[f8355,f8345]) ).
fof(f8374,plain,
! [X0,X1] :
( ~ p(h0,f2(j0(f0(h1(f1(j0(f1(j1(X0)))))))),j0(f0(h1(f2(j0(f0(h1(f1(j0(f1(j1(X0))))))))))),X1)
| ~ p(h0,f0(h0),j0(f0(h1(f0(h0)))),X0) ),
inference(duplicate_literals_removal,[status(thm)],[f8372]) ).
fof(f8375,plain,
! [X0] :
( ~ p(h0,f0(h0),j0(f0(h1(f0(h0)))),X0)
| ~ p(h0,f0(h0),j0(f0(h1(f0(h0)))),X0) ),
inference(resolution,[status(thm)],[f8374,f8345]) ).
fof(f8376,plain,
! [X0] : ~ p(h0,f0(h0),j0(f0(h1(f0(h0)))),X0),
inference(duplicate_literals_removal,[status(thm)],[f8375]) ).
fof(f8377,plain,
! [X0,X1] :
( p(h0,f2(X0),X1,g2(X1))
| p(h0,f1(j0(f0(h1(f0(h0))))),X0,g1(X1)) ),
inference(resolution,[status(thm)],[f8376,f4]) ).
fof(f8421,plain,
! [X0,X1,X2] :
( ~ p(h0,f1(j0(f0(h1(f0(h0))))),j0(f1(j1(X2))),X0)
| ~ p(h0,f1(j0(f0(h1(f0(h0))))),j0(f0(h1(f1(j0(f0(h1(f0(h0)))))))),X2)
| p(h0,f2(j0(f2(j1(X0)))),X1,g2(X1)) ),
inference(resolution,[status(thm)],[f8377,f9]) ).
fof(f8446,plain,
! [X0,X1,X2,X3] :
( ~ p(h0,f2(j0(f2(j1(X1)))),j0(f1(j1(X2))),X3)
| ~ p(h0,f2(j0(f2(j1(X1)))),j0(f0(h1(f2(j0(f2(j1(X1))))))),X2)
| ~ p(h0,f1(j0(f0(h1(f0(h0))))),j0(f1(j1(X0))),X1)
| ~ p(h0,f1(j0(f0(h1(f0(h0))))),j0(f0(h1(f1(j0(f0(h1(f0(h0)))))))),X0) ),
inference(resolution,[status(thm)],[f8421,f9]) ).
fof(f8480,plain,
! [X0,X1,X2,X3] :
( ~ p(h0,f1(j0(f0(h1(f0(h0))))),j0(f1(j1(X3))),X1)
| ~ p(h0,f1(j0(f0(h1(f0(h0))))),j0(f0(h1(f1(j0(f0(h1(f0(h0)))))))),X3)
| ~ p(h0,f2(j0(f2(j1(X1)))),j0(f0(h1(f2(j0(f2(j1(X1))))))),X2)
| ~ p(h0,f1(j0(f0(h1(f0(h0))))),j0(f1(j1(X0))),X1)
| ~ p(h0,f1(j0(f0(h1(f0(h0))))),j0(f0(h1(f1(j0(f0(h1(f0(h0)))))))),X0) ),
inference(resolution,[status(thm)],[f8446,f8421]) ).
fof(f8874,plain,
! [X0,X1,X2] :
( ~ p(h0,f2(j0(f2(j1(X1)))),j0(f0(h1(f2(j0(f2(j1(X1))))))),X2)
| ~ p(h0,f1(j0(f0(h1(f0(h0))))),j0(f1(j1(X0))),X1)
| ~ p(h0,f1(j0(f0(h1(f0(h0))))),j0(f0(h1(f1(j0(f0(h1(f0(h0)))))))),X0) ),
inference(factoring,[status(thm)],[f8480]) ).
fof(f8916,plain,
! [X0,X1,X2] :
( ~ p(h0,f1(j0(f0(h1(f0(h0))))),j0(f1(j1(X2))),X1)
| ~ p(h0,f1(j0(f0(h1(f0(h0))))),j0(f0(h1(f1(j0(f0(h1(f0(h0)))))))),X2)
| ~ p(h0,f1(j0(f0(h1(f0(h0))))),j0(f1(j1(X0))),X1)
| ~ p(h0,f1(j0(f0(h1(f0(h0))))),j0(f0(h1(f1(j0(f0(h1(f0(h0)))))))),X0) ),
inference(resolution,[status(thm)],[f8874,f8421]) ).
fof(f8919,plain,
! [X0,X1] :
( p(h0,f2(j0(f1(j1(X0)))),X1,g2(X1))
| ~ p(h0,f1(j0(f0(h1(f0(h0))))),j0(f0(h1(f1(j0(f0(h1(f0(h0)))))))),X0)
| ~ p(h0,f1(j0(f0(h1(f0(h0))))),j0(f0(h1(f1(j0(f0(h1(f0(h0)))))))),X0) ),
inference(resolution,[status(thm)],[f8916,f8377]) ).
fof(f8925,plain,
! [X0,X1] :
( p(h0,f2(j0(f1(j1(X0)))),X1,g2(X1))
| ~ p(h0,f1(j0(f0(h1(f0(h0))))),j0(f0(h1(f1(j0(f0(h1(f0(h0)))))))),X0) ),
inference(duplicate_literals_removal,[status(thm)],[f8919]) ).
fof(f8934,plain,
! [X0,X1,X2] :
( ~ p(h0,f2(j0(f1(j1(X0)))),j0(f1(j1(X1))),X2)
| ~ p(h0,f2(j0(f1(j1(X0)))),j0(f0(h1(f2(j0(f1(j1(X0))))))),X1)
| ~ p(h0,f1(j0(f0(h1(f0(h0))))),j0(f0(h1(f1(j0(f0(h1(f0(h0)))))))),X0) ),
inference(resolution,[status(thm)],[f8925,f9]) ).
fof(f8962,plain,
! [X0,X1] :
( ~ p(h0,f1(j0(f0(h1(f0(h0))))),j0(f0(h1(f1(j0(f0(h1(f0(h0)))))))),X0)
| ~ p(h0,f2(j0(f1(j1(X0)))),j0(f0(h1(f2(j0(f1(j1(X0))))))),X1)
| ~ p(h0,f1(j0(f0(h1(f0(h0))))),j0(f0(h1(f1(j0(f0(h1(f0(h0)))))))),X0) ),
inference(resolution,[status(thm)],[f8934,f8925]) ).
fof(f8964,plain,
! [X0,X1] :
( ~ p(h0,f2(j0(f1(j1(X0)))),j0(f0(h1(f2(j0(f1(j1(X0))))))),X1)
| ~ p(h0,f1(j0(f0(h1(f0(h0))))),j0(f0(h1(f1(j0(f0(h1(f0(h0)))))))),X0) ),
inference(duplicate_literals_removal,[status(thm)],[f8962]) ).
fof(f8968,plain,
! [X0] :
( ~ p(h0,f1(j0(f0(h1(f0(h0))))),j0(f0(h1(f1(j0(f0(h1(f0(h0)))))))),X0)
| ~ p(h0,f1(j0(f0(h1(f0(h0))))),j0(f0(h1(f1(j0(f0(h1(f0(h0)))))))),X0) ),
inference(resolution,[status(thm)],[f8964,f8925]) ).
fof(f8969,plain,
! [X0] : ~ p(h0,f1(j0(f0(h1(f0(h0))))),j0(f0(h1(f1(j0(f0(h1(f0(h0)))))))),X0),
inference(duplicate_literals_removal,[status(thm)],[f8968]) ).
fof(f8970,plain,
! [X0] : p(h0,f2(j0(f0(h1(f1(j0(f0(h1(f0(h0))))))))),X0,g2(X0)),
inference(resolution,[status(thm)],[f8969,f8377]) ).
fof(f8977,plain,
! [X0,X1] :
( ~ p(h0,f2(j0(f0(h1(f1(j0(f0(h1(f0(h0))))))))),j0(f1(j1(X0))),X1)
| ~ p(h0,f2(j0(f0(h1(f1(j0(f0(h1(f0(h0))))))))),j0(f0(h1(f2(j0(f0(h1(f1(j0(f0(h1(f0(h0)))))))))))),X0) ),
inference(resolution,[status(thm)],[f8970,f9]) ).
fof(f8981,plain,
! [X0] : ~ p(h0,f2(j0(f0(h1(f1(j0(f0(h1(f0(h0))))))))),j0(f0(h1(f2(j0(f0(h1(f1(j0(f0(h1(f0(h0)))))))))))),X0),
inference(resolution,[status(thm)],[f8977,f8970]) ).
fof(f8982,plain,
$false,
inference(resolution,[status(thm)],[f8981,f8970]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN314-1.002.001 : TPTP v9.3.1. Released v1.2.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n010.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 10:48:55 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.37 % Drodi V4.1.1
% 91.55/12.02 % Refutation found
% 91.55/12.02 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 91.55/12.02 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 91.55/12.17 % Elapsed time: 11.785629 seconds
% 91.55/12.17 % CPU time: 92.503526 seconds
% 91.55/12.17 % Total memory used: 539.801 MB
% 91.55/12.17 % Net memory used: 505.073 MB
%------------------------------------------------------------------------------