%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SYN353-1 : TPTP v9.3.1. Released v1.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 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 : Fri Sep 25 03:34:28 PM UTC 2026
% Result : Unsatisfiable 19.50s 8.19s
% Output : Proof 19.50s
% Verified :
% SZS Type : Refutation
% Derivation depth : 44
% Number of leaves : 11
% Syntax : Number of formulae : 111 ( 6 unt; 0 def)
% Number of atoms : 324 ( 0 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 313 ( 100 ~; 213 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 2 ( 1 usr; 1 prp; 0-3 aty)
% Number of functors : 2 ( 2 usr; 1 con; 0-3 aty)
% Number of variables : 212 ( 3 sgn 66 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f0,negated_conjecture,
( f(Y3,Y1,Y2)
| f(Y2,Y3,Y1)
| ~ f(a,a,z(Y1,Y2,Y3))
| ~ f(Y1,Y2,Y3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause1) ).
fof(f0_nnf,plain,
! [Y1,Y2,Y3] :
( f(Y3,Y1,Y2)
| f(Y2,Y3,Y1)
| ~ f(a,a,z(Y1,Y2,Y3))
| ~ f(Y1,Y2,Y3) ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [Y1,Y2,Y3] :
( f(Y3,Y1,Y2)
| f(Y2,Y3,Y1)
| ~ f(a,a,z(Y1,Y2,Y3))
| ~ f(Y1,Y2,Y3) ),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
( f(X2,X0,X1)
| f(X1,X2,X0)
| ~ f(a,a,z(X0,X1,X2))
| ~ f(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(f3,negated_conjecture,
( f(Y2,Y1,z(Y1,Y2,Y3))
| f(Y3,Y1,Y2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause4) ).
fof(f3_nnf,plain,
! [Y3,Y1,Y2] :
( f(Y2,Y1,z(Y1,Y2,Y3))
| f(Y3,Y1,Y2) ),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [Y3,Y1,Y2] :
( f(Y2,Y1,z(Y1,Y2,Y3))
| f(Y3,Y1,Y2) ),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
( f(X2,X1,z(X1,X2,X0))
| f(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p20,plain,
( f(X2,X1,X0)
| f(z(X1,X0,X2),X0,X1)
| f(X1,z(X1,X0,X2),X0)
| ~ f(a,a,z(X0,X1,z(X1,X0,X2))) ),
inference(resolution,[status(thm)],[c0,c3]) ).
cnf(p123,plain,
( f(z(a,a,X0),a,a)
| f(X0,a,a)
| f(z(a,a,X0),a,a)
| f(a,z(a,a,X0),a) ),
inference(resolution,[status(thm)],[p20,c3]) ).
cnf(p244,plain,
( f(X0,a,a)
| f(z(a,a,X0),a,a)
| f(a,z(a,a,X0),a) ),
inference(factoring,[status(thm)],[p123]) ).
cnf(f9,negated_conjecture,
( ~ f(z(Y1,Y2,Y3),Y2,Y1)
| f(Y1,Y2,Y3)
| f(Y3,Y1,Y2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause10) ).
fof(f9_nnf,plain,
! [Y3,Y1,Y2] :
( ~ f(z(Y1,Y2,Y3),Y2,Y1)
| f(Y1,Y2,Y3)
| f(Y3,Y1,Y2) ),
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
! [Y3,Y1,Y2] :
( ~ f(z(Y1,Y2,Y3),Y2,Y1)
| f(Y1,Y2,Y3)
| f(Y3,Y1,Y2) ),
inference(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c9,plain,
( ~ f(z(X1,X2,X0),X2,X1)
| f(X1,X2,X0)
| f(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(p248,plain,
( f(a,a,X0)
| f(X0,a,a)
| f(X0,a,a)
| f(a,z(a,a,X0),a) ),
inference(resolution,[status(thm)],[p244,c9]) ).
cnf(p250,plain,
( f(a,a,X0)
| f(X0,a,a)
| f(a,z(a,a,X0),a) ),
inference(factoring,[status(thm)],[p248]) ).
cnf(f5,negated_conjecture,
( ~ f(Y1,z(Y1,Y2,Y3),Y2)
| f(Y1,Y2,Y3)
| ~ f(Y2,Y3,Y1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause6) ).
fof(f5_nnf,plain,
! [Y2,Y3,Y1] :
( ~ f(Y1,z(Y1,Y2,Y3),Y2)
| f(Y1,Y2,Y3)
| ~ f(Y2,Y3,Y1) ),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [Y2,Y3,Y1] :
( ~ f(Y1,z(Y1,Y2,Y3),Y2)
| f(Y1,Y2,Y3)
| ~ f(Y2,Y3,Y1) ),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c5,plain,
( ~ f(X2,z(X2,X0,X1),X0)
| f(X2,X0,X1)
| ~ f(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(f7,negated_conjecture,
( f(Y1,z(Y1,Y2,Y3),Y2)
| f(Y2,Y3,Y1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause8) ).
fof(f7_nnf,plain,
! [Y2,Y3,Y1] :
( f(Y1,z(Y1,Y2,Y3),Y2)
| f(Y2,Y3,Y1) ),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [Y2,Y3,Y1] :
( f(Y1,z(Y1,Y2,Y3),Y2)
| f(Y2,Y3,Y1) ),
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c7,plain,
( f(X2,z(X2,X0,X1),X0)
| f(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(p34,plain,
( f(X0,X2,X1)
| ~ f(X0,z(X0,X1,z(X1,X0,X2)),X1)
| f(X0,X1,z(X1,X0,X2)) ),
inference(resolution,[status(thm)],[c5,c7]) ).
cnf(p257,plain,
( f(a,X0,a)
| f(a,a,z(a,a,X0))
| f(a,a,z(a,a,X0))
| f(z(a,a,X0),a,a) ),
inference(resolution,[status(thm)],[p250,p34]) ).
cnf(p298,plain,
( f(a,X0,a)
| f(a,a,z(a,a,X0))
| f(z(a,a,X0),a,a) ),
inference(factoring,[status(thm)],[p257]) ).
cnf(f11,negated_conjecture,
( f(z(Y1,Y2,Y3),Y2,Y1)
| ~ f(Y2,Y3,Y1)
| ~ f(Y3,Y1,Y2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause12) ).
fof(f11_nnf,plain,
! [Y3,Y1,Y2] :
( f(z(Y1,Y2,Y3),Y2,Y1)
| ~ f(Y2,Y3,Y1)
| ~ f(Y3,Y1,Y2) ),
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
! [Y3,Y1,Y2] :
( f(z(Y1,Y2,Y3),Y2,Y1)
| ~ f(Y2,Y3,Y1)
| ~ f(Y3,Y1,Y2) ),
inference(skolemisation,[status(esa)],[f11_nnf]) ).
cnf(c11,plain,
( f(z(X1,X2,X0),X2,X1)
| ~ f(X2,X0,X1)
| ~ f(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(p305,plain,
( f(z(a,a,z(a,a,X0)),a,a)
| ~ f(a,z(a,a,X0),a)
| f(a,X0,a)
| f(a,a,z(a,a,X0)) ),
inference(resolution,[status(thm)],[p298,c11]) ).
cnf(p511,plain,
( f(a,X0,a)
| f(z(a,a,z(a,a,X0)),a,a)
| f(a,X0,a)
| f(a,a,z(a,a,X0)) ),
inference(resolution,[status(thm)],[p305,c7]) ).
cnf(p513,plain,
( f(z(a,a,z(a,a,X0)),a,a)
| f(a,X0,a)
| f(a,a,z(a,a,X0)) ),
inference(factoring,[status(thm)],[p511]) ).
cnf(f1,negated_conjecture,
( ~ f(Y2,Y1,z(Y1,Y2,Y3))
| f(Y1,Y2,Y3)
| ~ f(Y3,Y1,Y2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause2) ).
fof(f1_nnf,plain,
! [Y3,Y1,Y2] :
( ~ f(Y2,Y1,z(Y1,Y2,Y3))
| f(Y1,Y2,Y3)
| ~ f(Y3,Y1,Y2) ),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [Y3,Y1,Y2] :
( ~ f(Y2,Y1,z(Y1,Y2,Y3))
| f(Y1,Y2,Y3)
| ~ f(Y3,Y1,Y2) ),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
( ~ f(X2,X1,z(X1,X2,X0))
| f(X1,X2,X0)
| ~ f(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p516,plain,
( ~ f(a,a,z(a,a,z(a,a,z(a,a,X0))))
| f(a,a,z(a,a,z(a,a,X0)))
| f(a,X0,a)
| f(a,a,z(a,a,X0)) ),
inference(resolution,[status(thm)],[p513,c1]) ).
cnf(f10,negated_conjecture,
( ~ f(z(Y1,Y2,Y3),Y2,Y1)
| f(Y1,Y2,Y3)
| f(Y2,Y3,Y1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause11) ).
fof(f10_nnf,plain,
! [Y2,Y3,Y1] :
( ~ f(z(Y1,Y2,Y3),Y2,Y1)
| f(Y1,Y2,Y3)
| f(Y2,Y3,Y1) ),
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
! [Y2,Y3,Y1] :
( ~ f(z(Y1,Y2,Y3),Y2,Y1)
| f(Y1,Y2,Y3)
| f(Y2,Y3,Y1) ),
inference(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c10,plain,
( ~ f(z(X2,X0,X1),X0,X2)
| f(X2,X0,X1)
| f(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(p304,plain,
( f(a,a,X0)
| f(a,X0,a)
| f(a,X0,a)
| f(a,a,z(a,a,X0)) ),
inference(resolution,[status(thm)],[p298,c10]) ).
cnf(p306,plain,
( f(a,a,X0)
| f(a,X0,a)
| f(a,a,z(a,a,X0)) ),
inference(factoring,[status(thm)],[p304]) ).
cnf(p1076,plain,
( f(a,a,z(a,a,z(a,a,X0)))
| f(a,z(a,a,z(a,a,X0)),a)
| f(a,a,z(a,a,z(a,a,X0)))
| f(a,X0,a)
| f(a,a,z(a,a,X0)) ),
inference(resolution,[status(thm)],[p516,p306]) ).
cnf(p1831,plain,
( f(a,z(a,a,z(a,a,X0)),a)
| f(a,a,z(a,a,z(a,a,X0)))
| f(a,X0,a)
| f(a,a,z(a,a,X0)) ),
inference(factoring,[status(thm)],[p1076]) ).
cnf(p1835,plain,
( f(a,X0,a)
| f(a,a,z(a,a,X0))
| f(a,a,z(a,a,z(a,a,X0)))
| f(a,X0,a)
| f(a,a,z(a,a,X0)) ),
inference(resolution,[status(thm)],[p1831,p34]) ).
cnf(p1848,plain,
( f(a,X0,a)
| f(a,a,z(a,a,z(a,a,X0)))
| f(a,X0,a)
| f(a,a,z(a,a,X0)) ),
inference(factoring,[status(thm)],[p1835]) ).
cnf(p1850,plain,
( f(a,a,z(a,a,z(a,a,X0)))
| f(a,X0,a)
| f(a,a,z(a,a,X0)) ),
inference(factoring,[status(thm)],[p1848]) ).
cnf(p302,plain,
( ~ f(a,a,z(a,a,z(a,a,X0)))
| f(a,a,z(a,a,X0))
| f(a,X0,a)
| f(a,a,z(a,a,X0)) ),
inference(resolution,[status(thm)],[p298,c1]) ).
cnf(p494,plain,
( ~ f(a,a,z(a,a,z(a,a,X0)))
| f(a,X0,a)
| f(a,a,z(a,a,X0)) ),
inference(factoring,[status(thm)],[p302]) ).
cnf(p1857,plain,
( f(a,X0,a)
| f(a,a,z(a,a,X0))
| f(a,X0,a)
| f(a,a,z(a,a,X0)) ),
inference(resolution,[status(thm)],[p1850,p494]) ).
cnf(p1862,plain,
( f(a,X0,a)
| f(a,X0,a)
| f(a,a,z(a,a,X0)) ),
inference(factoring,[status(thm)],[p1857]) ).
cnf(p1865,plain,
( f(a,X0,a)
| f(a,a,z(a,a,X0)) ),
inference(factoring,[status(thm)],[p1862]) ).
cnf(f2,negated_conjecture,
( ~ f(Y2,Y1,z(Y1,Y2,Y3))
| f(Y2,Y3,Y1)
| ~ f(Y3,Y1,Y2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause3) ).
fof(f2_nnf,plain,
! [Y3,Y1,Y2] :
( ~ f(Y2,Y1,z(Y1,Y2,Y3))
| f(Y2,Y3,Y1)
| ~ f(Y3,Y1,Y2) ),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [Y3,Y1,Y2] :
( ~ f(Y2,Y1,z(Y1,Y2,Y3))
| f(Y2,Y3,Y1)
| ~ f(Y3,Y1,Y2) ),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
( ~ f(X2,X1,z(X1,X2,X0))
| f(X2,X0,X1)
| ~ f(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p246,plain,
( ~ f(a,a,z(a,a,z(a,a,X0)))
| f(a,z(a,a,X0),a)
| f(X0,a,a)
| f(a,z(a,a,X0),a) ),
inference(resolution,[status(thm)],[p244,c2]) ).
cnf(p459,plain,
( ~ f(a,a,z(a,a,z(a,a,X0)))
| f(X0,a,a)
| f(a,z(a,a,X0),a) ),
inference(factoring,[status(thm)],[p246]) ).
cnf(p1876,plain,
( f(X0,a,a)
| f(a,z(a,a,X0),a)
| f(a,z(a,a,X0),a) ),
inference(resolution,[status(thm)],[p1865,p459]) ).
cnf(p1901,plain,
( f(X0,a,a)
| f(a,z(a,a,X0),a) ),
inference(factoring,[status(thm)],[p1876]) ).
cnf(f6,negated_conjecture,
( ~ f(Y1,z(Y1,Y2,Y3),Y2)
| f(Y3,Y1,Y2)
| ~ f(Y2,Y3,Y1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause7) ).
fof(f6_nnf,plain,
! [Y2,Y3,Y1] :
( ~ f(Y1,z(Y1,Y2,Y3),Y2)
| f(Y3,Y1,Y2)
| ~ f(Y2,Y3,Y1) ),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [Y2,Y3,Y1] :
( ~ f(Y1,z(Y1,Y2,Y3),Y2)
| f(Y3,Y1,Y2)
| ~ f(Y2,Y3,Y1) ),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c6,plain,
( ~ f(X2,z(X2,X0,X1),X0)
| f(X1,X2,X0)
| ~ f(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(p37,plain,
( f(X1,X2,X0)
| ~ f(X1,z(X1,X0,z(X0,X1,X2)),X0)
| f(z(X0,X1,X2),X1,X0) ),
inference(resolution,[status(thm)],[c6,c7]) ).
cnf(p1916,plain,
( f(a,X0,a)
| f(z(a,a,X0),a,a)
| f(z(a,a,X0),a,a) ),
inference(resolution,[status(thm)],[p1901,p37]) ).
cnf(p1969,plain,
( f(a,X0,a)
| f(z(a,a,X0),a,a) ),
inference(factoring,[status(thm)],[p1916]) ).
cnf(p1974,plain,
( f(a,a,X0)
| f(a,X0,a)
| f(a,X0,a) ),
inference(resolution,[status(thm)],[p1969,c10]) ).
cnf(p2060,plain,
( f(a,a,X0)
| f(a,X0,a) ),
inference(factoring,[status(thm)],[p1974]) ).
cnf(p2068,plain,
( ~ f(a,z(a,a,X0),a)
| f(a,a,X0)
| f(a,a,X0) ),
inference(resolution,[status(thm)],[p2060,c5]) ).
cnf(p2102,plain,
( ~ f(a,z(a,a,X0),a)
| f(a,a,X0) ),
inference(factoring,[status(thm)],[p2068]) ).
cnf(p2103,plain,
( f(X0,a,a)
| f(a,a,X0) ),
inference(resolution,[status(thm)],[p2102,p1901]) ).
cnf(p2108,plain,
( ~ f(a,a,z(a,a,X0))
| f(a,a,X0)
| f(a,a,X0) ),
inference(resolution,[status(thm)],[p2103,c1]) ).
cnf(p2171,plain,
( ~ f(a,a,z(a,a,X0))
| f(a,a,X0) ),
inference(factoring,[status(thm)],[p2108]) ).
cnf(p2104,plain,
( f(a,a,z(a,a,X0))
| f(a,a,X0) ),
inference(resolution,[status(thm)],[p2102,p2060]) ).
cnf(p2174,plain,
( f(a,a,X0)
| f(a,a,X0) ),
inference(resolution,[status(thm)],[p2171,p2104]) ).
cnf(p2175,plain,
f(a,a,X0),
inference(factoring,[status(thm)],[p2174]) ).
cnf(p45,plain,
( f(X0,X2,X1)
| f(z(z(X1,X0,X2),X0,X1),X0,z(X1,X0,X2))
| ~ f(X0,X1,z(X1,X0,X2)) ),
inference(resolution,[status(thm)],[c11,c7]) ).
cnf(p146,plain,
( f(X2,X0,X1)
| f(X1,X2,X0)
| f(z(z(X0,X1,X2),X1,X0),X1,z(X0,X1,X2)) ),
inference(resolution,[status(thm)],[p45,c3]) ).
cnf(p147,plain,
( f(X0,X0,X0)
| f(z(z(X0,X0,X0),X0,X0),X0,z(X0,X0,X0)) ),
inference(factoring,[status(thm)],[p146]) ).
cnf(p159,plain,
( f(z(X0,X0,X0),z(z(X0,X0,X0),X0,X0),X0)
| f(X0,z(X0,X0,X0),z(z(X0,X0,X0),X0,X0))
| ~ f(a,a,z(z(z(X0,X0,X0),X0,X0),X0,z(X0,X0,X0)))
| f(X0,X0,X0) ),
inference(resolution,[status(thm)],[p147,c0]) ).
cnf(p2195,plain,
( f(z(X0,X0,X0),z(z(X0,X0,X0),X0,X0),X0)
| f(X0,z(X0,X0,X0),z(z(X0,X0,X0),X0,X0))
| f(X0,X0,X0) ),
inference(resolution,[status(thm)],[p2175,p159]) ).
cnf(p33,plain,
( f(X2,X0,X1)
| ~ f(z(X0,X1,X2),z(z(X0,X1,X2),X1,X0),X1)
| f(z(X0,X1,X2),X1,X0) ),
inference(resolution,[status(thm)],[c5,c3]) ).
cnf(p3309,plain,
( f(X0,X0,X0)
| f(z(X0,X0,X0),X0,X0)
| f(X0,z(X0,X0,X0),z(z(X0,X0,X0),X0,X0))
| f(X0,X0,X0) ),
inference(resolution,[status(thm)],[p2195,p33]) ).
cnf(p3311,plain,
( f(z(X0,X0,X0),X0,X0)
| f(X0,z(X0,X0,X0),z(z(X0,X0,X0),X0,X0))
| f(X0,X0,X0) ),
inference(factoring,[status(thm)],[p3309]) ).
cnf(p24,plain,
( f(X1,X2,X0)
| ~ f(X1,z(X0,X1,X2),z(z(X0,X1,X2),X1,X0))
| f(z(X0,X1,X2),X1,X0) ),
inference(resolution,[status(thm)],[c1,c7]) ).
cnf(p3317,plain,
( f(X0,X0,X0)
| f(z(X0,X0,X0),X0,X0)
| f(z(X0,X0,X0),X0,X0)
| f(X0,X0,X0) ),
inference(resolution,[status(thm)],[p3311,p24]) ).
cnf(p3320,plain,
( f(X0,X0,X0)
| f(z(X0,X0,X0),X0,X0)
| f(X0,X0,X0) ),
inference(factoring,[status(thm)],[p3317]) ).
cnf(p3325,plain,
( f(z(X0,X0,X0),X0,X0)
| f(X0,X0,X0) ),
inference(factoring,[status(thm)],[p3320]) ).
cnf(p43,plain,
( ~ f(z(X0,X0,X0),X0,X0)
| f(X0,X0,X0) ),
inference(factoring,[status(thm)],[c9]) ).
cnf(p3329,plain,
( f(X0,X0,X0)
| f(X0,X0,X0) ),
inference(resolution,[status(thm)],[p3325,p43]) ).
cnf(p3331,plain,
f(X0,X0,X0),
inference(factoring,[status(thm)],[p3329]) ).
cnf(f16,negated_conjecture,
( ~ f(z(Y1,Y2,Y3),z(Y1,Y2,Y3),z(Y1,Y2,Y3))
| ~ f(Y3,Y1,Y2)
| ~ f(Y2,Y3,Y1)
| ~ f(Y1,Y2,Y3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause17) ).
fof(f16_nnf,plain,
! [Y1,Y2,Y3] :
( ~ f(z(Y1,Y2,Y3),z(Y1,Y2,Y3),z(Y1,Y2,Y3))
| ~ f(Y3,Y1,Y2)
| ~ f(Y2,Y3,Y1)
| ~ f(Y1,Y2,Y3) ),
inference(nnf_transformation,[status(thm)],[f16]) ).
fof(f16_sk,plain,
! [Y1,Y2,Y3] :
( ~ f(z(Y1,Y2,Y3),z(Y1,Y2,Y3),z(Y1,Y2,Y3))
| ~ f(Y3,Y1,Y2)
| ~ f(Y2,Y3,Y1)
| ~ f(Y1,Y2,Y3) ),
inference(skolemisation,[status(esa)],[f16_nnf]) ).
cnf(c16,plain,
( ~ f(z(X0,X1,X2),z(X0,X1,X2),z(X0,X1,X2))
| ~ f(X2,X0,X1)
| ~ f(X1,X2,X0)
| ~ f(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(p2182,plain,
( ~ f(z(a,a,X0),z(a,a,X0),z(a,a,X0))
| ~ f(X0,a,a)
| ~ f(a,X0,a) ),
inference(resolution,[status(thm)],[p2175,c16]) ).
cnf(p2177,plain,
( f(X0,a,a)
| f(a,X0,a)
| ~ f(a,a,z(a,a,X0)) ),
inference(resolution,[status(thm)],[p2175,c0]) ).
cnf(p2247,plain,
( f(X0,a,a)
| f(a,X0,a) ),
inference(resolution,[status(thm)],[p2177,p2175]) ).
cnf(p2251,plain,
( ~ f(a,a,z(a,a,X0))
| f(a,X0,a)
| f(a,X0,a) ),
inference(resolution,[status(thm)],[p2247,c2]) ).
cnf(p2279,plain,
( ~ f(a,a,z(a,a,X0))
| f(a,X0,a) ),
inference(factoring,[status(thm)],[p2251]) ).
cnf(p2282,plain,
f(a,X0,a),
inference(resolution,[status(thm)],[p2279,p2175]) ).
cnf(p2701,plain,
( ~ f(z(a,a,X0),z(a,a,X0),z(a,a,X0))
| ~ f(X0,a,a) ),
inference(resolution,[status(thm)],[p2182,p2282]) ).
cnf(p2285,plain,
( ~ f(a,z(a,a,X0),a)
| f(X0,a,a) ),
inference(resolution,[status(thm)],[p2282,c6]) ).
cnf(p2305,plain,
f(X0,a,a),
inference(resolution,[status(thm)],[p2285,p2282]) ).
cnf(p2703,plain,
~ f(z(a,a,X0),z(a,a,X0),z(a,a,X0)),
inference(resolution,[status(thm)],[p2701,p2305]) ).
cnf(p3336,plain,
$false,
inference(resolution,[status(thm)],[p3331,p2703]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN353-1 : TPTP v9.3.1. Released v1.2.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.12/5.38 % Computer : n001.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 : Fri Sep 25 01:03:14 UTC 2026
% 0.12/5.38 % CPUTime :
% 0.12/5.38 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 19.50/8.19 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 19.50/8.19 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------