%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SYN755-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 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 : Fri Sep 25 03:35:38 PM UTC 2026
% Result : Unsatisfiable 5.74s 11.63s
% Output : Proof 5.74s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)
% Comments :
%------------------------------------------------------------------------------
cnf(f41,negated_conjecture,
( ssPv2(X)
| ssPv3(W)
| ~ ssPv4(U)
| ~ ssRr(U,X)
| ~ ssRr(U,W)
| ~ ssPv4(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause42) ).
fof(f41_nnf,plain,
! [U,V,W,X] :
( ssPv2(X)
| ssPv3(W)
| ~ ssPv4(U)
| ~ ssRr(U,X)
| ~ ssRr(U,W)
| ~ ssPv4(V)
| ~ ssRr(U,V) ),
inference(nnf_transformation,[status(thm)],[f41]) ).
fof(f41_sk,plain,
! [U,V,W,X] :
( ssPv2(X)
| ssPv3(W)
| ~ ssPv4(U)
| ~ ssRr(U,X)
| ~ ssRr(U,W)
| ~ ssPv4(V)
| ~ ssRr(U,V) ),
inference(skolemisation,[status(esa)],[f41_nnf]) ).
cnf(c41,plain,
( ssPv2(X3)
| ssPv3(X2)
| ~ ssPv4(X0)
| ~ ssRr(X0,X3)
| ~ ssRr(X0,X2)
| ~ ssPv4(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f41_sk]) ).
cnf(p190,plain,
( ssPv2(X2)
| ssPv3(X1)
| ~ ssPv4(X0)
| ~ ssRr(X0,X2)
| ~ ssPv4(X1)
| ~ ssRr(X0,X1) ),
inference(factoring,[status(thm)],[c41]) ).
cnf(p213,plain,
( ssPv2(X1)
| ssPv3(X1)
| ~ ssPv4(X0)
| ~ ssPv4(X1)
| ~ ssRr(X0,X1) ),
inference(factoring,[status(thm)],[p190]) ).
cnf(f0,negated_conjecture,
ssRr(U,skf1(U)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause1) ).
fof(f0_nnf,plain,
! [U] : ssRr(U,skf1(U)),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [U] : ssRr(U,skf1(U)),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
ssRr(X0,skf1(X0)),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p217,plain,
( ssPv2(skf1(X0))
| ssPv3(skf1(X0))
| ~ ssPv4(X0)
| ~ ssPv4(skf1(X0)) ),
inference(resolution,[status(thm)],[p213,c0]) ).
cnf(f7,negated_conjecture,
( ssPv3(U)
| ssPv2(U)
| ssPv1(W)
| ssPv4(V)
| ~ ssRr(U,W)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause8) ).
fof(f7_nnf,plain,
! [U,V,W] :
( ssPv3(U)
| ssPv2(U)
| ssPv1(W)
| ssPv4(V)
| ~ ssRr(U,W)
| ~ ssRr(U,V) ),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [U,V,W] :
( ssPv3(U)
| ssPv2(U)
| ssPv1(W)
| ssPv4(V)
| ~ ssRr(U,W)
| ~ ssRr(U,V) ),
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c7,plain,
( ssPv3(X0)
| ssPv2(X0)
| ssPv1(X2)
| ssPv4(X1)
| ~ ssRr(X0,X2)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(p57,plain,
( ssPv3(X0)
| ssPv2(X0)
| ssPv1(X1)
| ssPv4(X1)
| ~ ssRr(X0,X1) ),
inference(factoring,[status(thm)],[c7]) ).
cnf(p62,plain,
( ssPv3(X0)
| ssPv2(X0)
| ssPv1(skf1(X0))
| ssPv4(skf1(X0)) ),
inference(resolution,[status(thm)],[p57,c0]) ).
cnf(p218,plain,
( ssPv3(X0)
| ssPv2(X0)
| ssPv1(skf1(X0))
| ssPv2(skf1(X0))
| ssPv3(skf1(X0))
| ~ ssPv4(X0) ),
inference(resolution,[status(thm)],[p217,p62]) ).
cnf(p306,plain,
( ssPv3(X0)
| ssPv2(X0)
| ssPv1(skf1(X0))
| ssPv3(skf1(X0))
| ssPv2(skf1(X0))
| ssPv1(skf1(skf1(X0)))
| ssPv2(skf1(skf1(X0)))
| ssPv3(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[p218,p62]) ).
cnf(f32,negated_conjecture,
( ssPv3(U)
| ~ ssPv4(U)
| ~ ssPv3(W)
| ~ ssRr(U,W)
| ~ ssPv4(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause33) ).
fof(f32_nnf,plain,
! [U,V,W] :
( ssPv3(U)
| ~ ssPv4(U)
| ~ ssPv3(W)
| ~ ssRr(U,W)
| ~ ssPv4(V)
| ~ ssRr(U,V) ),
inference(nnf_transformation,[status(thm)],[f32]) ).
fof(f32_sk,plain,
! [U,V,W] :
( ssPv3(U)
| ~ ssPv4(U)
| ~ ssPv3(W)
| ~ ssRr(U,W)
| ~ ssPv4(V)
| ~ ssRr(U,V) ),
inference(skolemisation,[status(esa)],[f32_nnf]) ).
cnf(c32,plain,
( ssPv3(X0)
| ~ ssPv4(X0)
| ~ ssPv3(X2)
| ~ ssRr(X0,X2)
| ~ ssPv4(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f32_sk]) ).
cnf(p143,plain,
( ssPv3(X0)
| ~ ssPv4(X0)
| ~ ssPv3(X1)
| ~ ssPv4(X1)
| ~ ssRr(X0,X1) ),
inference(factoring,[status(thm)],[c32]) ).
cnf(p145,plain,
( ssPv3(X0)
| ~ ssPv4(X0)
| ~ ssPv3(skf1(X0))
| ~ ssPv4(skf1(X0)) ),
inference(resolution,[status(thm)],[p143,c0]) ).
cnf(p146,plain,
( ssPv3(X0)
| ssPv2(X0)
| ssPv1(skf1(X0))
| ssPv3(X0)
| ~ ssPv4(X0)
| ~ ssPv3(skf1(X0)) ),
inference(resolution,[status(thm)],[p145,p62]) ).
cnf(p172,plain,
( ssPv2(X0)
| ssPv1(skf1(X0))
| ssPv3(X0)
| ~ ssPv4(X0)
| ~ ssPv3(skf1(X0)) ),
inference(factoring,[status(thm)],[p146]) ).
cnf(p312,plain,
( ssPv2(skf1(X0))
| ssPv1(skf1(skf1(X0)))
| ssPv3(skf1(X0))
| ~ ssPv4(skf1(X0))
| ssPv3(X0)
| ssPv2(X0)
| ssPv1(skf1(X0))
| ssPv3(skf1(X0))
| ssPv2(skf1(X0))
| ssPv1(skf1(skf1(X0)))
| ssPv2(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[p306,p172]) ).
cnf(p330,plain,
( ssPv2(skf1(X0))
| ssPv3(skf1(X0))
| ~ ssPv4(skf1(X0))
| ssPv3(X0)
| ssPv2(X0)
| ssPv1(skf1(X0))
| ssPv3(skf1(X0))
| ssPv2(skf1(X0))
| ssPv1(skf1(skf1(X0)))
| ssPv2(skf1(skf1(X0))) ),
inference(factoring,[status(thm)],[p312]) ).
cnf(p333,plain,
( ssPv3(skf1(X0))
| ~ ssPv4(skf1(X0))
| ssPv3(X0)
| ssPv2(X0)
| ssPv1(skf1(X0))
| ssPv3(skf1(X0))
| ssPv2(skf1(X0))
| ssPv1(skf1(skf1(X0)))
| ssPv2(skf1(skf1(X0))) ),
inference(factoring,[status(thm)],[p330]) ).
cnf(p335,plain,
( ~ ssPv4(skf1(X0))
| ssPv3(X0)
| ssPv2(X0)
| ssPv1(skf1(X0))
| ssPv3(skf1(X0))
| ssPv2(skf1(X0))
| ssPv1(skf1(skf1(X0)))
| ssPv2(skf1(skf1(X0))) ),
inference(factoring,[status(thm)],[p333]) ).
cnf(p336,plain,
( ssPv3(X0)
| ssPv2(X0)
| ssPv1(skf1(X0))
| ssPv3(X0)
| ssPv2(X0)
| ssPv1(skf1(X0))
| ssPv3(skf1(X0))
| ssPv2(skf1(X0))
| ssPv1(skf1(skf1(X0)))
| ssPv2(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[p335,p62]) ).
cnf(p337,plain,
( ssPv3(X0)
| ssPv2(X0)
| ssPv3(X0)
| ssPv2(X0)
| ssPv1(skf1(X0))
| ssPv3(skf1(X0))
| ssPv2(skf1(X0))
| ssPv1(skf1(skf1(X0)))
| ssPv2(skf1(skf1(X0))) ),
inference(factoring,[status(thm)],[p336]) ).
cnf(p340,plain,
( ssPv3(X0)
| ssPv3(X0)
| ssPv2(X0)
| ssPv1(skf1(X0))
| ssPv3(skf1(X0))
| ssPv2(skf1(X0))
| ssPv1(skf1(skf1(X0)))
| ssPv2(skf1(skf1(X0))) ),
inference(factoring,[status(thm)],[p337]) ).
cnf(p342,plain,
( ssPv3(X0)
| ssPv2(X0)
| ssPv1(skf1(X0))
| ssPv3(skf1(X0))
| ssPv2(skf1(X0))
| ssPv1(skf1(skf1(X0)))
| ssPv2(skf1(skf1(X0))) ),
inference(factoring,[status(thm)],[p340]) ).
cnf(f28,negated_conjecture,
( ssPv3(U)
| ssPv1(U)
| ~ ssPv2(W)
| ~ ssRr(U,W)
| ~ ssPv4(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause29) ).
fof(f28_nnf,plain,
! [U,V,W] :
( ssPv3(U)
| ssPv1(U)
| ~ ssPv2(W)
| ~ ssRr(U,W)
| ~ ssPv4(V)
| ~ ssRr(U,V) ),
inference(nnf_transformation,[status(thm)],[f28]) ).
fof(f28_sk,plain,
! [U,V,W] :
( ssPv3(U)
| ssPv1(U)
| ~ ssPv2(W)
| ~ ssRr(U,W)
| ~ ssPv4(V)
| ~ ssRr(U,V) ),
inference(skolemisation,[status(esa)],[f28_nnf]) ).
cnf(c28,plain,
( ssPv3(X0)
| ssPv1(X0)
| ~ ssPv2(X2)
| ~ ssRr(X0,X2)
| ~ ssPv4(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f28_sk]) ).
cnf(p131,plain,
( ssPv3(X0)
| ssPv1(X0)
| ~ ssPv2(X1)
| ~ ssPv4(X1)
| ~ ssRr(X0,X1) ),
inference(factoring,[status(thm)],[c28]) ).
cnf(p133,plain,
( ssPv3(X0)
| ssPv1(X0)
| ~ ssPv2(skf1(X0))
| ~ ssPv4(skf1(X0)) ),
inference(resolution,[status(thm)],[p131,c0]) ).
cnf(p134,plain,
( ssPv3(X0)
| ssPv2(X0)
| ssPv1(skf1(X0))
| ssPv3(X0)
| ssPv1(X0)
| ~ ssPv2(skf1(X0)) ),
inference(resolution,[status(thm)],[p133,p62]) ).
cnf(p171,plain,
( ssPv2(X0)
| ssPv1(skf1(X0))
| ssPv3(X0)
| ssPv1(X0)
| ~ ssPv2(skf1(X0)) ),
inference(factoring,[status(thm)],[p134]) ).
cnf(p347,plain,
( ssPv2(skf1(X0))
| ssPv1(skf1(skf1(X0)))
| ssPv3(skf1(X0))
| ssPv1(skf1(X0))
| ssPv3(X0)
| ssPv2(X0)
| ssPv1(skf1(X0))
| ssPv3(skf1(X0))
| ssPv2(skf1(X0))
| ssPv1(skf1(skf1(X0))) ),
inference(resolution,[status(thm)],[p342,p171]) ).
cnf(p367,plain,
( ssPv2(skf1(X0))
| ssPv3(skf1(X0))
| ssPv1(skf1(X0))
| ssPv3(X0)
| ssPv2(X0)
| ssPv1(skf1(X0))
| ssPv3(skf1(X0))
| ssPv2(skf1(X0))
| ssPv1(skf1(skf1(X0))) ),
inference(factoring,[status(thm)],[p347]) ).
cnf(p371,plain,
( ssPv3(skf1(X0))
| ssPv1(skf1(X0))
| ssPv3(X0)
| ssPv2(X0)
| ssPv1(skf1(X0))
| ssPv3(skf1(X0))
| ssPv2(skf1(X0))
| ssPv1(skf1(skf1(X0))) ),
inference(factoring,[status(thm)],[p367]) ).
cnf(p374,plain,
( ssPv1(skf1(X0))
| ssPv3(X0)
| ssPv2(X0)
| ssPv1(skf1(X0))
| ssPv3(skf1(X0))
| ssPv2(skf1(X0))
| ssPv1(skf1(skf1(X0))) ),
inference(factoring,[status(thm)],[p371]) ).
cnf(p376,plain,
( ssPv3(X0)
| ssPv2(X0)
| ssPv1(skf1(X0))
| ssPv3(skf1(X0))
| ssPv2(skf1(X0))
| ssPv1(skf1(skf1(X0))) ),
inference(factoring,[status(thm)],[p374]) ).
cnf(f1,negated_conjecture,
( ssPv3(U)
| ssPv2(U)
| ssPv1(U)
| ~ ssPv1(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause2) ).
fof(f1_nnf,plain,
! [U,V] :
( ssPv3(U)
| ssPv2(U)
| ssPv1(U)
| ~ ssPv1(V)
| ~ ssRr(U,V) ),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [U,V] :
( ssPv3(U)
| ssPv2(U)
| ssPv1(U)
| ~ ssPv1(V)
| ~ ssRr(U,V) ),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
( ssPv3(X0)
| ssPv2(X0)
| ssPv1(X0)
| ~ ssPv1(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p51,plain,
( ssPv3(X0)
| ssPv2(X0)
| ssPv1(X0)
| ~ ssPv1(skf1(X0)) ),
inference(resolution,[status(thm)],[c1,c0]) ).
cnf(p377,plain,
( ssPv3(skf1(X0))
| ssPv2(skf1(X0))
| ssPv1(skf1(X0))
| ssPv3(X0)
| ssPv2(X0)
| ssPv1(skf1(X0))
| ssPv3(skf1(X0))
| ssPv2(skf1(X0)) ),
inference(resolution,[status(thm)],[p376,p51]) ).
cnf(p382,plain,
( ssPv3(skf1(X0))
| ssPv1(skf1(X0))
| ssPv3(X0)
| ssPv2(X0)
| ssPv1(skf1(X0))
| ssPv3(skf1(X0))
| ssPv2(skf1(X0)) ),
inference(factoring,[status(thm)],[p377]) ).
cnf(p385,plain,
( ssPv1(skf1(X0))
| ssPv3(X0)
| ssPv2(X0)
| ssPv1(skf1(X0))
| ssPv3(skf1(X0))
| ssPv2(skf1(X0)) ),
inference(factoring,[status(thm)],[p382]) ).
cnf(p387,plain,
( ssPv3(X0)
| ssPv2(X0)
| ssPv1(skf1(X0))
| ssPv3(skf1(X0))
| ssPv2(skf1(X0)) ),
inference(factoring,[status(thm)],[p385]) ).
cnf(p394,plain,
( ssPv2(X0)
| ssPv1(skf1(X0))
| ssPv3(X0)
| ~ ssPv4(X0)
| ssPv3(X0)
| ssPv2(X0)
| ssPv1(skf1(X0))
| ssPv2(skf1(X0)) ),
inference(resolution,[status(thm)],[p387,p172]) ).
cnf(p433,plain,
( ssPv2(X0)
| ssPv3(X0)
| ~ ssPv4(X0)
| ssPv3(X0)
| ssPv2(X0)
| ssPv1(skf1(X0))
| ssPv2(skf1(X0)) ),
inference(factoring,[status(thm)],[p394]) ).
cnf(p487,plain,
( ssPv3(X0)
| ~ ssPv4(X0)
| ssPv3(X0)
| ssPv2(X0)
| ssPv1(skf1(X0))
| ssPv2(skf1(X0)) ),
inference(factoring,[status(thm)],[p433]) ).
cnf(p567,plain,
( ~ ssPv4(X0)
| ssPv3(X0)
| ssPv2(X0)
| ssPv1(skf1(X0))
| ssPv2(skf1(X0)) ),
inference(factoring,[status(thm)],[p487]) ).
cnf(f23,negated_conjecture,
( ssPv4(U)
| ssPv2(U)
| ~ ssPv3(W)
| ~ ssRr(U,W)
| ~ ssPv4(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause24) ).
fof(f23_nnf,plain,
! [U,V,W] :
( ssPv4(U)
| ssPv2(U)
| ~ ssPv3(W)
| ~ ssRr(U,W)
| ~ ssPv4(V)
| ~ ssRr(U,V) ),
inference(nnf_transformation,[status(thm)],[f23]) ).
fof(f23_sk,plain,
! [U,V,W] :
( ssPv4(U)
| ssPv2(U)
| ~ ssPv3(W)
| ~ ssRr(U,W)
| ~ ssPv4(V)
| ~ ssRr(U,V) ),
inference(skolemisation,[status(esa)],[f23_nnf]) ).
cnf(c23,plain,
( ssPv4(X0)
| ssPv2(X0)
| ~ ssPv3(X2)
| ~ ssRr(X0,X2)
| ~ ssPv4(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f23_sk]) ).
cnf(p114,plain,
( ssPv4(X0)
| ssPv2(X0)
| ~ ssPv3(X1)
| ~ ssPv4(X1)
| ~ ssRr(X0,X1) ),
inference(factoring,[status(thm)],[c23]) ).
cnf(p116,plain,
( ssPv4(X0)
| ssPv2(X0)
| ~ ssPv3(skf1(X0))
| ~ ssPv4(skf1(X0)) ),
inference(resolution,[status(thm)],[p114,c0]) ).
cnf(p117,plain,
( ssPv3(X0)
| ssPv2(X0)
| ssPv1(skf1(X0))
| ssPv4(X0)
| ssPv2(X0)
| ~ ssPv3(skf1(X0)) ),
inference(resolution,[status(thm)],[p116,p62]) ).
cnf(p167,plain,
( ssPv3(X0)
| ssPv1(skf1(X0))
| ssPv4(X0)
| ssPv2(X0)
| ~ ssPv3(skf1(X0)) ),
inference(factoring,[status(thm)],[p117]) ).
cnf(p393,plain,
( ssPv3(X0)
| ssPv1(skf1(X0))
| ssPv4(X0)
| ssPv2(X0)
| ssPv3(X0)
| ssPv2(X0)
| ssPv1(skf1(X0))
| ssPv2(skf1(X0)) ),
inference(resolution,[status(thm)],[p387,p167]) ).
cnf(p411,plain,
( ssPv3(X0)
| ssPv4(X0)
| ssPv2(X0)
| ssPv3(X0)
| ssPv2(X0)
| ssPv1(skf1(X0))
| ssPv2(skf1(X0)) ),
inference(factoring,[status(thm)],[p393]) ).
cnf(p414,plain,
( ssPv3(X0)
| ssPv4(X0)
| ssPv3(X0)
| ssPv2(X0)
| ssPv1(skf1(X0))
| ssPv2(skf1(X0)) ),
inference(factoring,[status(thm)],[p411]) ).
cnf(p416,plain,
( ssPv4(X0)
| ssPv3(X0)
| ssPv2(X0)
| ssPv1(skf1(X0))
| ssPv2(skf1(X0)) ),
inference(factoring,[status(thm)],[p414]) ).
cnf(f12,negated_conjecture,
( ssPv4(U)
| ssPv2(U)
| ssPv1(W)
| ~ ssRr(U,W)
| ~ ssPv2(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause13) ).
fof(f12_nnf,plain,
! [U,V,W] :
( ssPv4(U)
| ssPv2(U)
| ssPv1(W)
| ~ ssRr(U,W)
| ~ ssPv2(V)
| ~ ssRr(U,V) ),
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
! [U,V,W] :
( ssPv4(U)
| ssPv2(U)
| ssPv1(W)
| ~ ssRr(U,W)
| ~ ssPv2(V)
| ~ ssRr(U,V) ),
inference(skolemisation,[status(esa)],[f12_nnf]) ).
cnf(c12,plain,
( ssPv4(X0)
| ssPv2(X0)
| ssPv1(X2)
| ~ ssRr(X0,X2)
| ~ ssPv2(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(p78,plain,
( ssPv4(X0)
| ssPv2(X0)
| ssPv1(X1)
| ~ ssPv2(X1)
| ~ ssRr(X0,X1) ),
inference(factoring,[status(thm)],[c12]) ).
cnf(p80,plain,
( ssPv4(X0)
| ssPv2(X0)
| ssPv1(skf1(X0))
| ~ ssPv2(skf1(X0)) ),
inference(resolution,[status(thm)],[p78,c0]) ).
cnf(p418,plain,
( ssPv4(X0)
| ssPv2(X0)
| ssPv1(skf1(X0))
| ssPv4(X0)
| ssPv3(X0)
| ssPv2(X0)
| ssPv1(skf1(X0)) ),
inference(resolution,[status(thm)],[p416,p80]) ).
cnf(p436,plain,
( ssPv4(X0)
| ssPv2(X0)
| ssPv4(X0)
| ssPv3(X0)
| ssPv2(X0)
| ssPv1(skf1(X0)) ),
inference(factoring,[status(thm)],[p418]) ).
cnf(p439,plain,
( ssPv4(X0)
| ssPv4(X0)
| ssPv3(X0)
| ssPv2(X0)
| ssPv1(skf1(X0)) ),
inference(factoring,[status(thm)],[p436]) ).
cnf(p441,plain,
( ssPv4(X0)
| ssPv3(X0)
| ssPv2(X0)
| ssPv1(skf1(X0)) ),
inference(factoring,[status(thm)],[p439]) ).
cnf(f10,negated_conjecture,
( ssPv4(U)
| ssPv3(U)
| ssPv3(W)
| ~ ssRr(U,W)
| ~ ssPv1(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause11) ).
fof(f10_nnf,plain,
! [U,V,W] :
( ssPv4(U)
| ssPv3(U)
| ssPv3(W)
| ~ ssRr(U,W)
| ~ ssPv1(V)
| ~ ssRr(U,V) ),
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
! [U,V,W] :
( ssPv4(U)
| ssPv3(U)
| ssPv3(W)
| ~ ssRr(U,W)
| ~ ssPv1(V)
| ~ ssRr(U,V) ),
inference(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c10,plain,
( ssPv4(X0)
| ssPv3(X0)
| ssPv3(X2)
| ~ ssRr(X0,X2)
| ~ ssPv1(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(p68,plain,
( ssPv4(X0)
| ssPv3(X0)
| ssPv3(X1)
| ~ ssPv1(X1)
| ~ ssRr(X0,X1) ),
inference(factoring,[status(thm)],[c10]) ).
cnf(p72,plain,
( ssPv4(X0)
| ssPv3(X0)
| ssPv3(skf1(X0))
| ~ ssPv1(skf1(X0)) ),
inference(resolution,[status(thm)],[p68,c0]) ).
cnf(p445,plain,
( ssPv4(X0)
| ssPv3(X0)
| ssPv3(skf1(X0))
| ssPv4(X0)
| ssPv3(X0)
| ssPv2(X0) ),
inference(resolution,[status(thm)],[p441,p72]) ).
cnf(p485,plain,
( ssPv4(X0)
| ssPv3(skf1(X0))
| ssPv4(X0)
| ssPv3(X0)
| ssPv2(X0) ),
inference(factoring,[status(thm)],[p445]) ).
cnf(p489,plain,
( ssPv3(skf1(X0))
| ssPv4(X0)
| ssPv3(X0)
| ssPv2(X0) ),
inference(factoring,[status(thm)],[p485]) ).
cnf(f11,negated_conjecture,
( ssPv4(U)
| ssPv2(U)
| ssPv4(W)
| ~ ssRr(U,W)
| ~ ssPv3(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause12) ).
fof(f11_nnf,plain,
! [U,V,W] :
( ssPv4(U)
| ssPv2(U)
| ssPv4(W)
| ~ ssRr(U,W)
| ~ ssPv3(V)
| ~ ssRr(U,V) ),
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
! [U,V,W] :
( ssPv4(U)
| ssPv2(U)
| ssPv4(W)
| ~ ssRr(U,W)
| ~ ssPv3(V)
| ~ ssRr(U,V) ),
inference(skolemisation,[status(esa)],[f11_nnf]) ).
cnf(c11,plain,
( ssPv4(X0)
| ssPv2(X0)
| ssPv4(X2)
| ~ ssRr(X0,X2)
| ~ ssPv3(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(p73,plain,
( ssPv4(X0)
| ssPv2(X0)
| ssPv4(X1)
| ~ ssPv3(X1)
| ~ ssRr(X0,X1) ),
inference(factoring,[status(thm)],[c11]) ).
cnf(p77,plain,
( ssPv4(X0)
| ssPv2(X0)
| ssPv4(skf1(X0))
| ~ ssPv3(skf1(X0)) ),
inference(resolution,[status(thm)],[p73,c0]) ).
cnf(p490,plain,
( ssPv4(X0)
| ssPv2(X0)
| ssPv4(skf1(X0))
| ssPv4(X0)
| ssPv3(X0)
| ssPv2(X0) ),
inference(resolution,[status(thm)],[p489,p77]) ).
cnf(p508,plain,
( ssPv4(X0)
| ssPv4(skf1(X0))
| ssPv4(X0)
| ssPv3(X0)
| ssPv2(X0) ),
inference(factoring,[status(thm)],[p490]) ).
cnf(p510,plain,
( ssPv4(skf1(X0))
| ssPv4(X0)
| ssPv3(X0)
| ssPv2(X0) ),
inference(factoring,[status(thm)],[p508]) ).
cnf(p511,plain,
( ssPv4(X0)
| ssPv2(X0)
| ~ ssPv3(skf1(X0))
| ssPv4(X0)
| ssPv3(X0)
| ssPv2(X0) ),
inference(resolution,[status(thm)],[p510,p116]) ).
cnf(p524,plain,
( ssPv4(X0)
| ~ ssPv3(skf1(X0))
| ssPv4(X0)
| ssPv3(X0)
| ssPv2(X0) ),
inference(factoring,[status(thm)],[p511]) ).
cnf(p526,plain,
( ~ ssPv3(skf1(X0))
| ssPv4(X0)
| ssPv3(X0)
| ssPv2(X0) ),
inference(factoring,[status(thm)],[p524]) ).
cnf(p528,plain,
( ssPv4(X0)
| ssPv3(X0)
| ssPv2(X0)
| ssPv4(X0)
| ssPv3(X0)
| ssPv2(X0) ),
inference(resolution,[status(thm)],[p526,p489]) ).
cnf(p529,plain,
( ssPv4(X0)
| ssPv3(X0)
| ssPv4(X0)
| ssPv3(X0)
| ssPv2(X0) ),
inference(factoring,[status(thm)],[p528]) ).
cnf(p532,plain,
( ssPv4(X0)
| ssPv4(X0)
| ssPv3(X0)
| ssPv2(X0) ),
inference(factoring,[status(thm)],[p529]) ).
cnf(p534,plain,
( ssPv4(X0)
| ssPv3(X0)
| ssPv2(X0) ),
inference(factoring,[status(thm)],[p532]) ).
cnf(p568,plain,
( ssPv3(X0)
| ssPv2(X0)
| ssPv3(X0)
| ssPv2(X0)
| ssPv1(skf1(X0))
| ssPv2(skf1(X0)) ),
inference(resolution,[status(thm)],[p567,p534]) ).
cnf(p586,plain,
( ssPv3(X0)
| ssPv3(X0)
| ssPv2(X0)
| ssPv1(skf1(X0))
| ssPv2(skf1(X0)) ),
inference(factoring,[status(thm)],[p568]) ).
cnf(p588,plain,
( ssPv3(X0)
| ssPv2(X0)
| ssPv1(skf1(X0))
| ssPv2(skf1(X0)) ),
inference(factoring,[status(thm)],[p586]) ).
cnf(p592,plain,
( ssPv2(X0)
| ssPv1(skf1(X0))
| ssPv3(X0)
| ssPv1(X0)
| ssPv3(X0)
| ssPv2(X0)
| ssPv1(skf1(X0)) ),
inference(resolution,[status(thm)],[p588,p171]) ).
cnf(p627,plain,
( ssPv2(X0)
| ssPv3(X0)
| ssPv1(X0)
| ssPv3(X0)
| ssPv2(X0)
| ssPv1(skf1(X0)) ),
inference(factoring,[status(thm)],[p592]) ).
cnf(p630,plain,
( ssPv3(X0)
| ssPv1(X0)
| ssPv3(X0)
| ssPv2(X0)
| ssPv1(skf1(X0)) ),
inference(factoring,[status(thm)],[p627]) ).
cnf(p632,plain,
( ssPv1(X0)
| ssPv3(X0)
| ssPv2(X0)
| ssPv1(skf1(X0)) ),
inference(factoring,[status(thm)],[p630]) ).
cnf(p633,plain,
( ssPv3(X0)
| ssPv2(X0)
| ssPv1(X0)
| ssPv1(X0)
| ssPv3(X0)
| ssPv2(X0) ),
inference(resolution,[status(thm)],[p632,p51]) ).
cnf(p638,plain,
( ssPv3(X0)
| ssPv1(X0)
| ssPv1(X0)
| ssPv3(X0)
| ssPv2(X0) ),
inference(factoring,[status(thm)],[p633]) ).
cnf(p644,plain,
( ssPv1(X0)
| ssPv1(X0)
| ssPv3(X0)
| ssPv2(X0) ),
inference(factoring,[status(thm)],[p638]) ).
cnf(p646,plain,
( ssPv1(X0)
| ssPv3(X0)
| ssPv2(X0) ),
inference(factoring,[status(thm)],[p644]) ).
cnf(p648,plain,
( ssPv4(X0)
| ssPv2(X0)
| ssPv4(skf1(X0))
| ssPv1(skf1(X0))
| ssPv2(skf1(X0)) ),
inference(resolution,[status(thm)],[p646,p77]) ).
cnf(p682,plain,
( ssPv4(X0)
| ssPv2(X0)
| ~ ssPv3(skf1(X0))
| ssPv4(X0)
| ssPv2(X0)
| ssPv1(skf1(X0))
| ssPv2(skf1(X0)) ),
inference(resolution,[status(thm)],[p648,p116]) ).
cnf(p736,plain,
( ssPv4(X0)
| ~ ssPv3(skf1(X0))
| ssPv4(X0)
| ssPv2(X0)
| ssPv1(skf1(X0))
| ssPv2(skf1(X0)) ),
inference(factoring,[status(thm)],[p682]) ).
cnf(p738,plain,
( ~ ssPv3(skf1(X0))
| ssPv4(X0)
| ssPv2(X0)
| ssPv1(skf1(X0))
| ssPv2(skf1(X0)) ),
inference(factoring,[status(thm)],[p736]) ).
cnf(p739,plain,
( ssPv1(skf1(X0))
| ssPv2(skf1(X0))
| ssPv4(X0)
| ssPv2(X0)
| ssPv1(skf1(X0))
| ssPv2(skf1(X0)) ),
inference(resolution,[status(thm)],[p738,p646]) ).
cnf(p740,plain,
( ssPv1(skf1(X0))
| ssPv4(X0)
| ssPv2(X0)
| ssPv1(skf1(X0))
| ssPv2(skf1(X0)) ),
inference(factoring,[status(thm)],[p739]) ).
cnf(p742,plain,
( ssPv4(X0)
| ssPv2(X0)
| ssPv1(skf1(X0))
| ssPv2(skf1(X0)) ),
inference(factoring,[status(thm)],[p740]) ).
cnf(p744,plain,
( ssPv4(X0)
| ssPv2(X0)
| ssPv1(skf1(X0))
| ssPv4(X0)
| ssPv2(X0)
| ssPv1(skf1(X0)) ),
inference(resolution,[status(thm)],[p742,p80]) ).
cnf(p762,plain,
( ssPv4(X0)
| ssPv2(X0)
| ssPv4(X0)
| ssPv2(X0)
| ssPv1(skf1(X0)) ),
inference(factoring,[status(thm)],[p744]) ).
cnf(p765,plain,
( ssPv4(X0)
| ssPv4(X0)
| ssPv2(X0)
| ssPv1(skf1(X0)) ),
inference(factoring,[status(thm)],[p762]) ).
cnf(p769,plain,
( ssPv4(X0)
| ssPv2(X0)
| ssPv1(skf1(X0)) ),
inference(factoring,[status(thm)],[p765]) ).
cnf(f15,negated_conjecture,
( ssPv2(U)
| ssPv1(U)
| ssPv3(W)
| ~ ssRr(U,W)
| ~ ssPv1(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause16) ).
fof(f15_nnf,plain,
! [U,V,W] :
( ssPv2(U)
| ssPv1(U)
| ssPv3(W)
| ~ ssRr(U,W)
| ~ ssPv1(V)
| ~ ssRr(U,V) ),
inference(nnf_transformation,[status(thm)],[f15]) ).
fof(f15_sk,plain,
! [U,V,W] :
( ssPv2(U)
| ssPv1(U)
| ssPv3(W)
| ~ ssRr(U,W)
| ~ ssPv1(V)
| ~ ssRr(U,V) ),
inference(skolemisation,[status(esa)],[f15_nnf]) ).
cnf(c15,plain,
( ssPv2(X0)
| ssPv1(X0)
| ssPv3(X2)
| ~ ssRr(X0,X2)
| ~ ssPv1(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f15_sk]) ).
cnf(p88,plain,
( ssPv2(X0)
| ssPv1(X0)
| ssPv3(X1)
| ~ ssPv1(X1)
| ~ ssRr(X0,X1) ),
inference(factoring,[status(thm)],[c15]) ).
cnf(p90,plain,
( ssPv2(X0)
| ssPv1(X0)
| ssPv3(skf1(X0))
| ~ ssPv1(skf1(X0)) ),
inference(resolution,[status(thm)],[p88,c0]) ).
cnf(p772,plain,
( ssPv2(X0)
| ssPv1(X0)
| ssPv3(skf1(X0))
| ssPv4(X0)
| ssPv2(X0) ),
inference(resolution,[status(thm)],[p769,p90]) ).
cnf(p778,plain,
( ssPv1(X0)
| ssPv3(skf1(X0))
| ssPv4(X0)
| ssPv2(X0) ),
inference(factoring,[status(thm)],[p772]) ).
cnf(p779,plain,
( ssPv4(X0)
| ssPv2(X0)
| ssPv4(skf1(X0))
| ssPv1(X0)
| ssPv4(X0)
| ssPv2(X0) ),
inference(resolution,[status(thm)],[p778,p77]) ).
cnf(p804,plain,
( ssPv4(X0)
| ssPv4(skf1(X0))
| ssPv1(X0)
| ssPv4(X0)
| ssPv2(X0) ),
inference(factoring,[status(thm)],[p779]) ).
cnf(p806,plain,
( ssPv4(skf1(X0))
| ssPv1(X0)
| ssPv4(X0)
| ssPv2(X0) ),
inference(factoring,[status(thm)],[p804]) ).
cnf(p807,plain,
( ssPv4(X0)
| ssPv2(X0)
| ~ ssPv3(skf1(X0))
| ssPv1(X0)
| ssPv4(X0)
| ssPv2(X0) ),
inference(resolution,[status(thm)],[p806,p116]) ).
cnf(p829,plain,
( ssPv4(X0)
| ~ ssPv3(skf1(X0))
| ssPv1(X0)
| ssPv4(X0)
| ssPv2(X0) ),
inference(factoring,[status(thm)],[p807]) ).
cnf(p831,plain,
( ~ ssPv3(skf1(X0))
| ssPv1(X0)
| ssPv4(X0)
| ssPv2(X0) ),
inference(factoring,[status(thm)],[p829]) ).
cnf(p832,plain,
( ssPv1(X0)
| ssPv4(X0)
| ssPv2(X0)
| ssPv1(X0)
| ssPv4(X0)
| ssPv2(X0) ),
inference(resolution,[status(thm)],[p831,p778]) ).
cnf(p833,plain,
( ssPv1(X0)
| ssPv4(X0)
| ssPv1(X0)
| ssPv4(X0)
| ssPv2(X0) ),
inference(factoring,[status(thm)],[p832]) ).
cnf(p836,plain,
( ssPv1(X0)
| ssPv1(X0)
| ssPv4(X0)
| ssPv2(X0) ),
inference(factoring,[status(thm)],[p833]) ).
cnf(p838,plain,
( ssPv1(X0)
| ssPv4(X0)
| ssPv2(X0) ),
inference(factoring,[status(thm)],[p836]) ).
cnf(p546,plain,
( ssPv2(skf1(X0))
| ssPv3(skf1(X0))
| ~ ssPv4(X0)
| ssPv3(skf1(X0))
| ssPv2(skf1(X0)) ),
inference(resolution,[status(thm)],[p534,p217]) ).
cnf(p569,plain,
( ssPv3(skf1(X0))
| ~ ssPv4(X0)
| ssPv3(skf1(X0))
| ssPv2(skf1(X0)) ),
inference(factoring,[status(thm)],[p546]) ).
cnf(p571,plain,
( ~ ssPv4(X0)
| ssPv3(skf1(X0))
| ssPv2(skf1(X0)) ),
inference(factoring,[status(thm)],[p569]) ).
cnf(p866,plain,
( ssPv3(skf1(X0))
| ssPv2(skf1(X0))
| ssPv1(X0)
| ssPv2(X0) ),
inference(resolution,[status(thm)],[p838,p571]) ).
cnf(f26,negated_conjecture,
( ssPv1(U)
| ssPv4(W)
| ~ ssPv3(U)
| ~ ssRr(U,W)
| ~ ssPv3(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause27) ).
fof(f26_nnf,plain,
! [U,V,W] :
( ssPv1(U)
| ssPv4(W)
| ~ ssPv3(U)
| ~ ssRr(U,W)
| ~ ssPv3(V)
| ~ ssRr(U,V) ),
inference(nnf_transformation,[status(thm)],[f26]) ).
fof(f26_sk,plain,
! [U,V,W] :
( ssPv1(U)
| ssPv4(W)
| ~ ssPv3(U)
| ~ ssRr(U,W)
| ~ ssPv3(V)
| ~ ssRr(U,V) ),
inference(skolemisation,[status(esa)],[f26_nnf]) ).
cnf(c26,plain,
( ssPv1(X0)
| ssPv4(X2)
| ~ ssPv3(X0)
| ~ ssRr(X0,X2)
| ~ ssPv3(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f26_sk]) ).
cnf(p123,plain,
( ssPv1(X0)
| ssPv4(X1)
| ~ ssPv3(X0)
| ~ ssPv3(X1)
| ~ ssRr(X0,X1) ),
inference(factoring,[status(thm)],[c26]) ).
cnf(p127,plain,
( ssPv1(X0)
| ssPv4(skf1(X0))
| ~ ssPv3(X0)
| ~ ssPv3(skf1(X0)) ),
inference(resolution,[status(thm)],[p123,c0]) ).
cnf(p868,plain,
( ssPv1(X0)
| ssPv4(skf1(X0))
| ~ ssPv3(X0)
| ssPv2(skf1(X0))
| ssPv1(X0)
| ssPv2(X0) ),
inference(resolution,[status(thm)],[p866,p127]) ).
cnf(p961,plain,
( ssPv4(skf1(X0))
| ~ ssPv3(X0)
| ssPv2(skf1(X0))
| ssPv1(X0)
| ssPv2(X0) ),
inference(factoring,[status(thm)],[p868]) ).
cnf(p963,plain,
( ssPv1(X0)
| ssPv2(X0)
| ssPv4(skf1(X0))
| ssPv2(skf1(X0))
| ssPv1(X0)
| ssPv2(X0) ),
inference(resolution,[status(thm)],[p961,p646]) ).
cnf(p985,plain,
( ssPv1(X0)
| ssPv4(skf1(X0))
| ssPv2(skf1(X0))
| ssPv1(X0)
| ssPv2(X0) ),
inference(factoring,[status(thm)],[p963]) ).
cnf(p987,plain,
( ssPv4(skf1(X0))
| ssPv2(skf1(X0))
| ssPv1(X0)
| ssPv2(X0) ),
inference(factoring,[status(thm)],[p985]) ).
cnf(f35,negated_conjecture,
( ssPv1(U)
| ~ ssPv3(U)
| ~ ssPv3(W)
| ~ ssRr(U,W)
| ~ ssPv4(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause36) ).
fof(f35_nnf,plain,
! [U,V,W] :
( ssPv1(U)
| ~ ssPv3(U)
| ~ ssPv3(W)
| ~ ssRr(U,W)
| ~ ssPv4(V)
| ~ ssRr(U,V) ),
inference(nnf_transformation,[status(thm)],[f35]) ).
fof(f35_sk,plain,
! [U,V,W] :
( ssPv1(U)
| ~ ssPv3(U)
| ~ ssPv3(W)
| ~ ssRr(U,W)
| ~ ssPv4(V)
| ~ ssRr(U,V) ),
inference(skolemisation,[status(esa)],[f35_nnf]) ).
cnf(c35,plain,
( ssPv1(X0)
| ~ ssPv3(X0)
| ~ ssPv3(X2)
| ~ ssRr(X0,X2)
| ~ ssPv4(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f35_sk]) ).
cnf(p157,plain,
( ssPv1(X0)
| ~ ssPv3(X0)
| ~ ssPv3(X1)
| ~ ssPv4(X1)
| ~ ssRr(X0,X1) ),
inference(factoring,[status(thm)],[c35]) ).
cnf(p161,plain,
( ssPv1(X0)
| ~ ssPv3(X0)
| ~ ssPv3(skf1(X0))
| ~ ssPv4(skf1(X0)) ),
inference(resolution,[status(thm)],[p157,c0]) ).
cnf(p988,plain,
( ssPv1(X0)
| ~ ssPv3(X0)
| ~ ssPv3(skf1(X0))
| ssPv2(skf1(X0))
| ssPv1(X0)
| ssPv2(X0) ),
inference(resolution,[status(thm)],[p987,p161]) ).
cnf(p1003,plain,
( ~ ssPv3(X0)
| ~ ssPv3(skf1(X0))
| ssPv2(skf1(X0))
| ssPv1(X0)
| ssPv2(X0) ),
inference(factoring,[status(thm)],[p988]) ).
cnf(p1006,plain,
( ssPv2(skf1(X0))
| ssPv1(X0)
| ssPv2(X0)
| ~ ssPv3(X0)
| ssPv2(skf1(X0))
| ssPv1(X0)
| ssPv2(X0) ),
inference(resolution,[status(thm)],[p1003,p866]) ).
cnf(p1182,plain,
( ssPv1(X0)
| ssPv2(X0)
| ~ ssPv3(X0)
| ssPv2(skf1(X0))
| ssPv1(X0)
| ssPv2(X0) ),
inference(factoring,[status(thm)],[p1006]) ).
cnf(p1191,plain,
( ssPv1(X0)
| ~ ssPv3(X0)
| ssPv2(skf1(X0))
| ssPv1(X0)
| ssPv2(X0) ),
inference(factoring,[status(thm)],[p1182]) ).
cnf(p1193,plain,
( ~ ssPv3(X0)
| ssPv2(skf1(X0))
| ssPv1(X0)
| ssPv2(X0) ),
inference(factoring,[status(thm)],[p1191]) ).
cnf(p1195,plain,
( ssPv1(X0)
| ssPv2(X0)
| ssPv2(skf1(X0))
| ssPv1(X0)
| ssPv2(X0) ),
inference(resolution,[status(thm)],[p1193,p646]) ).
cnf(p1199,plain,
( ssPv1(X0)
| ssPv2(skf1(X0))
| ssPv1(X0)
| ssPv2(X0) ),
inference(factoring,[status(thm)],[p1195]) ).
cnf(p1209,plain,
( ssPv2(skf1(X0))
| ssPv1(X0)
| ssPv2(X0) ),
inference(factoring,[status(thm)],[p1199]) ).
cnf(f14,negated_conjecture,
( ssPv2(U)
| ssPv1(U)
| ssPv3(W)
| ~ ssRr(U,W)
| ~ ssPv2(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause15) ).
fof(f14_nnf,plain,
! [U,V,W] :
( ssPv2(U)
| ssPv1(U)
| ssPv3(W)
| ~ ssRr(U,W)
| ~ ssPv2(V)
| ~ ssRr(U,V) ),
inference(nnf_transformation,[status(thm)],[f14]) ).
fof(f14_sk,plain,
! [U,V,W] :
( ssPv2(U)
| ssPv1(U)
| ssPv3(W)
| ~ ssRr(U,W)
| ~ ssPv2(V)
| ~ ssRr(U,V) ),
inference(skolemisation,[status(esa)],[f14_nnf]) ).
cnf(c14,plain,
( ssPv2(X0)
| ssPv1(X0)
| ssPv3(X2)
| ~ ssRr(X0,X2)
| ~ ssPv2(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(p85,plain,
( ssPv2(X0)
| ssPv1(X0)
| ssPv3(X1)
| ~ ssPv2(X1)
| ~ ssRr(X0,X1) ),
inference(factoring,[status(thm)],[c14]) ).
cnf(p87,plain,
( ssPv2(X0)
| ssPv1(X0)
| ssPv3(skf1(X0))
| ~ ssPv2(skf1(X0)) ),
inference(resolution,[status(thm)],[p85,c0]) ).
cnf(p1211,plain,
( ssPv2(X0)
| ssPv1(X0)
| ssPv3(skf1(X0))
| ssPv1(X0)
| ssPv2(X0) ),
inference(resolution,[status(thm)],[p1209,p87]) ).
cnf(p1223,plain,
( ssPv1(X0)
| ssPv3(skf1(X0))
| ssPv1(X0)
| ssPv2(X0) ),
inference(factoring,[status(thm)],[p1211]) ).
cnf(p1225,plain,
( ssPv3(skf1(X0))
| ssPv1(X0)
| ssPv2(X0) ),
inference(factoring,[status(thm)],[p1223]) ).
cnf(p1228,plain,
( ssPv1(X0)
| ssPv4(skf1(X0))
| ~ ssPv3(X0)
| ssPv1(X0)
| ssPv2(X0) ),
inference(resolution,[status(thm)],[p1225,p127]) ).
cnf(p1241,plain,
( ssPv4(skf1(X0))
| ~ ssPv3(X0)
| ssPv1(X0)
| ssPv2(X0) ),
inference(factoring,[status(thm)],[p1228]) ).
cnf(p1245,plain,
( ssPv1(X0)
| ssPv2(X0)
| ssPv4(skf1(X0))
| ssPv1(X0)
| ssPv2(X0) ),
inference(resolution,[status(thm)],[p1241,p646]) ).
cnf(p1248,plain,
( ssPv1(X0)
| ssPv4(skf1(X0))
| ssPv1(X0)
| ssPv2(X0) ),
inference(factoring,[status(thm)],[p1245]) ).
cnf(p1250,plain,
( ssPv4(skf1(X0))
| ssPv1(X0)
| ssPv2(X0) ),
inference(factoring,[status(thm)],[p1248]) ).
cnf(p1251,plain,
( ssPv1(X0)
| ~ ssPv3(X0)
| ~ ssPv3(skf1(X0))
| ssPv1(X0)
| ssPv2(X0) ),
inference(resolution,[status(thm)],[p1250,p161]) ).
cnf(p1266,plain,
( ~ ssPv3(X0)
| ~ ssPv3(skf1(X0))
| ssPv1(X0)
| ssPv2(X0) ),
inference(factoring,[status(thm)],[p1251]) ).
cnf(p1267,plain,
( ssPv1(X0)
| ssPv2(X0)
| ~ ssPv3(X0)
| ssPv1(X0)
| ssPv2(X0) ),
inference(resolution,[status(thm)],[p1266,p1225]) ).
cnf(p1268,plain,
( ssPv1(X0)
| ~ ssPv3(X0)
| ssPv1(X0)
| ssPv2(X0) ),
inference(factoring,[status(thm)],[p1267]) ).
cnf(p1270,plain,
( ~ ssPv3(X0)
| ssPv1(X0)
| ssPv2(X0) ),
inference(factoring,[status(thm)],[p1268]) ).
cnf(p1272,plain,
( ssPv1(X0)
| ssPv2(X0)
| ssPv1(X0)
| ssPv2(X0) ),
inference(resolution,[status(thm)],[p1270,p646]) ).
cnf(p1275,plain,
( ssPv1(X0)
| ssPv1(X0)
| ssPv2(X0) ),
inference(factoring,[status(thm)],[p1272]) ).
cnf(p1277,plain,
( ssPv1(X0)
| ssPv2(X0) ),
inference(factoring,[status(thm)],[p1275]) ).
cnf(f44,negated_conjecture,
( ssPv4(U)
| ssPv2(X)
| ~ ssRr(U,X)
| ~ ssPv3(W)
| ~ ssRr(U,W)
| ~ ssPv4(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause45) ).
fof(f44_nnf,plain,
! [U,V,W,X] :
( ssPv4(U)
| ssPv2(X)
| ~ ssRr(U,X)
| ~ ssPv3(W)
| ~ ssRr(U,W)
| ~ ssPv4(V)
| ~ ssRr(U,V) ),
inference(nnf_transformation,[status(thm)],[f44]) ).
fof(f44_sk,plain,
! [U,V,W,X] :
( ssPv4(U)
| ssPv2(X)
| ~ ssRr(U,X)
| ~ ssPv3(W)
| ~ ssRr(U,W)
| ~ ssPv4(V)
| ~ ssRr(U,V) ),
inference(skolemisation,[status(esa)],[f44_nnf]) ).
cnf(c44,plain,
( ssPv4(X0)
| ssPv2(X3)
| ~ ssRr(X0,X3)
| ~ ssPv3(X2)
| ~ ssRr(X0,X2)
| ~ ssPv4(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f44_sk]) ).
cnf(p209,plain,
( ssPv4(X0)
| ssPv2(X2)
| ~ ssRr(X0,X2)
| ~ ssPv3(X1)
| ~ ssPv4(X1)
| ~ ssRr(X0,X1) ),
inference(factoring,[status(thm)],[c44]) ).
cnf(p257,plain,
( ssPv4(X0)
| ssPv2(X1)
| ~ ssPv3(X1)
| ~ ssPv4(X1)
| ~ ssRr(X0,X1) ),
inference(factoring,[status(thm)],[p209]) ).
cnf(p259,plain,
( ssPv4(X0)
| ssPv2(skf1(X0))
| ~ ssPv3(skf1(X0))
| ~ ssPv4(skf1(X0)) ),
inference(resolution,[status(thm)],[p257,c0]) ).
cnf(p854,plain,
( ssPv4(X0)
| ssPv2(skf1(X0))
| ~ ssPv3(skf1(X0))
| ssPv1(skf1(X0))
| ssPv2(skf1(X0)) ),
inference(resolution,[status(thm)],[p838,p259]) ).
cnf(p887,plain,
( ssPv4(X0)
| ~ ssPv3(skf1(X0))
| ssPv1(skf1(X0))
| ssPv2(skf1(X0)) ),
inference(factoring,[status(thm)],[p854]) ).
cnf(p888,plain,
( ssPv1(skf1(X0))
| ssPv2(skf1(X0))
| ssPv4(X0)
| ssPv1(skf1(X0))
| ssPv2(skf1(X0)) ),
inference(resolution,[status(thm)],[p887,p646]) ).
cnf(p890,plain,
( ssPv1(skf1(X0))
| ssPv4(X0)
| ssPv1(skf1(X0))
| ssPv2(skf1(X0)) ),
inference(factoring,[status(thm)],[p888]) ).
cnf(p892,plain,
( ssPv4(X0)
| ssPv1(skf1(X0))
| ssPv2(skf1(X0)) ),
inference(factoring,[status(thm)],[p890]) ).
cnf(f36,negated_conjecture,
( ssPv4(U)
| ssPv1(X)
| ssPv3(W)
| ~ ssRr(U,X)
| ~ ssRr(U,W)
| ~ ssPv2(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause37) ).
fof(f36_nnf,plain,
! [U,V,W,X] :
( ssPv4(U)
| ssPv1(X)
| ssPv3(W)
| ~ ssRr(U,X)
| ~ ssRr(U,W)
| ~ ssPv2(V)
| ~ ssRr(U,V) ),
inference(nnf_transformation,[status(thm)],[f36]) ).
fof(f36_sk,plain,
! [U,V,W,X] :
( ssPv4(U)
| ssPv1(X)
| ssPv3(W)
| ~ ssRr(U,X)
| ~ ssRr(U,W)
| ~ ssPv2(V)
| ~ ssRr(U,V) ),
inference(skolemisation,[status(esa)],[f36_nnf]) ).
cnf(c36,plain,
( ssPv4(X0)
| ssPv1(X3)
| ssPv3(X2)
| ~ ssRr(X0,X3)
| ~ ssRr(X0,X2)
| ~ ssPv2(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f36_sk]) ).
cnf(p163,plain,
( ssPv4(X0)
| ssPv1(X2)
| ssPv3(X1)
| ~ ssRr(X0,X2)
| ~ ssPv2(X1)
| ~ ssRr(X0,X1) ),
inference(factoring,[status(thm)],[c36]) ).
cnf(p177,plain,
( ssPv4(X0)
| ssPv1(X1)
| ssPv3(X1)
| ~ ssPv2(X1)
| ~ ssRr(X0,X1) ),
inference(factoring,[status(thm)],[p163]) ).
cnf(p179,plain,
( ssPv4(X0)
| ssPv1(skf1(X0))
| ssPv3(skf1(X0))
| ~ ssPv2(skf1(X0)) ),
inference(resolution,[status(thm)],[p177,c0]) ).
cnf(p894,plain,
( ssPv4(X0)
| ssPv1(skf1(X0))
| ssPv3(skf1(X0))
| ssPv4(X0)
| ssPv1(skf1(X0)) ),
inference(resolution,[status(thm)],[p892,p179]) ).
cnf(p909,plain,
( ssPv4(X0)
| ssPv3(skf1(X0))
| ssPv4(X0)
| ssPv1(skf1(X0)) ),
inference(factoring,[status(thm)],[p894]) ).
cnf(p922,plain,
( ssPv3(skf1(X0))
| ssPv4(X0)
| ssPv1(skf1(X0)) ),
inference(factoring,[status(thm)],[p909]) ).
cnf(f2,negated_conjecture,
( ssPv4(U)
| ssPv3(U)
| ~ ssPv2(U)
| ~ ssPv3(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause3) ).
fof(f2_nnf,plain,
! [U,V] :
( ssPv4(U)
| ssPv3(U)
| ~ ssPv2(U)
| ~ ssPv3(V)
| ~ ssRr(U,V) ),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [U,V] :
( ssPv4(U)
| ssPv3(U)
| ~ ssPv2(U)
| ~ ssPv3(V)
| ~ ssRr(U,V) ),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
( ssPv4(X0)
| ssPv3(X0)
| ~ ssPv2(X0)
| ~ ssPv3(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p52,plain,
( ssPv4(X0)
| ssPv3(X0)
| ~ ssPv2(X0)
| ~ ssPv3(skf1(X0)) ),
inference(resolution,[status(thm)],[c2,c0]) ).
cnf(p923,plain,
( ssPv4(X0)
| ssPv3(X0)
| ~ ssPv2(X0)
| ssPv4(X0)
| ssPv1(skf1(X0)) ),
inference(resolution,[status(thm)],[p922,p52]) ).
cnf(p939,plain,
( ssPv3(X0)
| ~ ssPv2(X0)
| ssPv4(X0)
| ssPv1(skf1(X0)) ),
inference(factoring,[status(thm)],[p923]) ).
cnf(p1294,plain,
( ssPv3(X0)
| ssPv4(X0)
| ssPv1(skf1(X0))
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p1277,p939]) ).
cnf(f3,negated_conjecture,
( ssPv4(U)
| ssPv3(U)
| ~ ssPv2(U)
| ~ ssPv1(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause4) ).
fof(f3_nnf,plain,
! [U,V] :
( ssPv4(U)
| ssPv3(U)
| ~ ssPv2(U)
| ~ ssPv1(V)
| ~ ssRr(U,V) ),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [U,V] :
( ssPv4(U)
| ssPv3(U)
| ~ ssPv2(U)
| ~ ssPv1(V)
| ~ ssRr(U,V) ),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
( ssPv4(X0)
| ssPv3(X0)
| ~ ssPv2(X0)
| ~ ssPv1(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p53,plain,
( ssPv4(X0)
| ssPv3(X0)
| ~ ssPv2(X0)
| ~ ssPv1(skf1(X0)) ),
inference(resolution,[status(thm)],[c3,c0]) ).
cnf(p1299,plain,
( ssPv4(X0)
| ssPv3(X0)
| ~ ssPv2(X0)
| ssPv3(X0)
| ssPv4(X0)
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p1294,p53]) ).
cnf(p1357,plain,
( ssPv3(X0)
| ~ ssPv2(X0)
| ssPv3(X0)
| ssPv4(X0)
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p1299]) ).
cnf(p1359,plain,
( ~ ssPv2(X0)
| ssPv3(X0)
| ssPv4(X0)
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p1357]) ).
cnf(p1360,plain,
( ssPv1(X0)
| ssPv3(X0)
| ssPv4(X0)
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p1359,p1277]) ).
cnf(p1363,plain,
( ssPv3(X0)
| ssPv4(X0)
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p1360]) ).
cnf(f30,negated_conjecture,
( ssPv1(W)
| ~ ssPv4(U)
| ~ ssPv2(U)
| ~ ssRr(U,W)
| ~ ssPv2(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause31) ).
fof(f30_nnf,plain,
! [U,V,W] :
( ssPv1(W)
| ~ ssPv4(U)
| ~ ssPv2(U)
| ~ ssRr(U,W)
| ~ ssPv2(V)
| ~ ssRr(U,V) ),
inference(nnf_transformation,[status(thm)],[f30]) ).
fof(f30_sk,plain,
! [U,V,W] :
( ssPv1(W)
| ~ ssPv4(U)
| ~ ssPv2(U)
| ~ ssRr(U,W)
| ~ ssPv2(V)
| ~ ssRr(U,V) ),
inference(skolemisation,[status(esa)],[f30_nnf]) ).
cnf(c30,plain,
( ssPv1(X2)
| ~ ssPv4(X0)
| ~ ssPv2(X0)
| ~ ssRr(X0,X2)
| ~ ssPv2(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f30_sk]) ).
cnf(p137,plain,
( ssPv1(X1)
| ~ ssPv4(X0)
| ~ ssPv2(X0)
| ~ ssPv2(X1)
| ~ ssRr(X0,X1) ),
inference(factoring,[status(thm)],[c30]) ).
cnf(p141,plain,
( ssPv1(skf1(X0))
| ~ ssPv4(X0)
| ~ ssPv2(X0)
| ~ ssPv2(skf1(X0)) ),
inference(resolution,[status(thm)],[p137,c0]) ).
cnf(p1282,plain,
( ssPv1(skf1(X0))
| ~ ssPv4(X0)
| ~ ssPv2(X0)
| ssPv1(skf1(X0)) ),
inference(resolution,[status(thm)],[p1277,p141]) ).
cnf(p1316,plain,
( ~ ssPv4(X0)
| ~ ssPv2(X0)
| ssPv1(skf1(X0)) ),
inference(factoring,[status(thm)],[p1282]) ).
cnf(p1321,plain,
( ssPv1(X0)
| ~ ssPv4(X0)
| ssPv1(skf1(X0)) ),
inference(resolution,[status(thm)],[p1316,p1277]) ).
cnf(p1388,plain,
( ssPv1(X0)
| ssPv1(skf1(X0))
| ssPv3(X0)
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p1363,p1321]) ).
cnf(p1389,plain,
( ssPv1(skf1(X0))
| ssPv3(X0)
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p1388]) ).
cnf(f18,negated_conjecture,
( ssPv3(U)
| ssPv2(W)
| ~ ssPv2(U)
| ~ ssRr(U,W)
| ~ ssPv1(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause19) ).
fof(f18_nnf,plain,
! [U,V,W] :
( ssPv3(U)
| ssPv2(W)
| ~ ssPv2(U)
| ~ ssRr(U,W)
| ~ ssPv1(V)
| ~ ssRr(U,V) ),
inference(nnf_transformation,[status(thm)],[f18]) ).
fof(f18_sk,plain,
! [U,V,W] :
( ssPv3(U)
| ssPv2(W)
| ~ ssPv2(U)
| ~ ssRr(U,W)
| ~ ssPv1(V)
| ~ ssRr(U,V) ),
inference(skolemisation,[status(esa)],[f18_nnf]) ).
cnf(c18,plain,
( ssPv3(X0)
| ssPv2(X2)
| ~ ssPv2(X0)
| ~ ssRr(X0,X2)
| ~ ssPv1(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f18_sk]) ).
cnf(p98,plain,
( ssPv3(X0)
| ssPv2(X1)
| ~ ssPv2(X0)
| ~ ssPv1(X1)
| ~ ssRr(X0,X1) ),
inference(factoring,[status(thm)],[c18]) ).
cnf(p100,plain,
( ssPv3(X0)
| ssPv2(skf1(X0))
| ~ ssPv2(X0)
| ~ ssPv1(skf1(X0)) ),
inference(resolution,[status(thm)],[p98,c0]) ).
cnf(p1391,plain,
( ssPv3(X0)
| ssPv2(skf1(X0))
| ~ ssPv2(X0)
| ssPv3(X0)
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p1389,p100]) ).
cnf(p1397,plain,
( ssPv2(skf1(X0))
| ~ ssPv2(X0)
| ssPv3(X0)
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p1391]) ).
cnf(p1398,plain,
( ssPv1(X0)
| ssPv2(skf1(X0))
| ssPv3(X0)
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p1397,p1277]) ).
cnf(p1399,plain,
( ssPv2(skf1(X0))
| ssPv3(X0)
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p1398]) ).
cnf(p1405,plain,
( ssPv3(skf1(X0))
| ssPv4(skf1(X0))
| ssPv1(skf1(skf1(X0)))
| ssPv3(X0)
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p1399,p939]) ).
cnf(p1470,plain,
( ssPv4(skf1(X0))
| ssPv3(skf1(X0))
| ~ ssPv2(skf1(X0))
| ssPv3(skf1(X0))
| ssPv4(skf1(X0))
| ssPv3(X0)
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p1405,p53]) ).
cnf(p1987,plain,
( ssPv3(skf1(X0))
| ~ ssPv2(skf1(X0))
| ssPv3(skf1(X0))
| ssPv4(skf1(X0))
| ssPv3(X0)
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p1470]) ).
cnf(p1989,plain,
( ~ ssPv2(skf1(X0))
| ssPv3(skf1(X0))
| ssPv4(skf1(X0))
| ssPv3(X0)
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p1987]) ).
cnf(p1990,plain,
( ssPv3(X0)
| ssPv1(X0)
| ssPv3(skf1(X0))
| ssPv4(skf1(X0))
| ssPv3(X0)
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p1989,p1399]) ).
cnf(p1991,plain,
( ssPv3(X0)
| ssPv3(skf1(X0))
| ssPv4(skf1(X0))
| ssPv3(X0)
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p1990]) ).
cnf(p1993,plain,
( ssPv3(skf1(X0))
| ssPv4(skf1(X0))
| ssPv3(X0)
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p1991]) ).
cnf(f4,negated_conjecture,
( ssPv3(U)
| ssPv1(U)
| ~ ssPv2(U)
| ~ ssPv4(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause5) ).
fof(f4_nnf,plain,
! [U,V] :
( ssPv3(U)
| ssPv1(U)
| ~ ssPv2(U)
| ~ ssPv4(V)
| ~ ssRr(U,V) ),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [U,V] :
( ssPv3(U)
| ssPv1(U)
| ~ ssPv2(U)
| ~ ssPv4(V)
| ~ ssRr(U,V) ),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c4,plain,
( ssPv3(X0)
| ssPv1(X0)
| ~ ssPv2(X0)
| ~ ssPv4(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p54,plain,
( ssPv3(X0)
| ssPv1(X0)
| ~ ssPv2(X0)
| ~ ssPv4(skf1(X0)) ),
inference(resolution,[status(thm)],[c4,c0]) ).
cnf(p1994,plain,
( ssPv3(X0)
| ssPv1(X0)
| ~ ssPv2(X0)
| ssPv3(skf1(X0))
| ssPv3(X0)
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p1993,p54]) ).
cnf(p2001,plain,
( ssPv3(X0)
| ~ ssPv2(X0)
| ssPv3(skf1(X0))
| ssPv3(X0)
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p1994]) ).
cnf(p2003,plain,
( ~ ssPv2(X0)
| ssPv3(skf1(X0))
| ssPv3(X0)
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p2001]) ).
cnf(p2004,plain,
( ssPv1(X0)
| ssPv3(skf1(X0))
| ssPv3(X0)
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p2003,p1277]) ).
cnf(p2005,plain,
( ssPv3(skf1(X0))
| ssPv3(X0)
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p2004]) ).
cnf(f27,negated_conjecture,
( ssPv1(U)
| ssPv4(W)
| ~ ssPv2(U)
| ~ ssRr(U,W)
| ~ ssPv3(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause28) ).
fof(f27_nnf,plain,
! [U,V,W] :
( ssPv1(U)
| ssPv4(W)
| ~ ssPv2(U)
| ~ ssRr(U,W)
| ~ ssPv3(V)
| ~ ssRr(U,V) ),
inference(nnf_transformation,[status(thm)],[f27]) ).
fof(f27_sk,plain,
! [U,V,W] :
( ssPv1(U)
| ssPv4(W)
| ~ ssPv2(U)
| ~ ssRr(U,W)
| ~ ssPv3(V)
| ~ ssRr(U,V) ),
inference(skolemisation,[status(esa)],[f27_nnf]) ).
cnf(c27,plain,
( ssPv1(X0)
| ssPv4(X2)
| ~ ssPv2(X0)
| ~ ssRr(X0,X2)
| ~ ssPv3(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f27_sk]) ).
cnf(p128,plain,
( ssPv1(X0)
| ssPv4(X1)
| ~ ssPv2(X0)
| ~ ssPv3(X1)
| ~ ssRr(X0,X1) ),
inference(factoring,[status(thm)],[c27]) ).
cnf(p130,plain,
( ssPv1(X0)
| ssPv4(skf1(X0))
| ~ ssPv2(X0)
| ~ ssPv3(skf1(X0)) ),
inference(resolution,[status(thm)],[p128,c0]) ).
cnf(p2007,plain,
( ssPv1(X0)
| ssPv4(skf1(X0))
| ~ ssPv2(X0)
| ssPv3(X0)
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p2005,p130]) ).
cnf(p2010,plain,
( ssPv4(skf1(X0))
| ~ ssPv2(X0)
| ssPv3(X0)
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p2007]) ).
cnf(p2011,plain,
( ssPv1(X0)
| ssPv4(skf1(X0))
| ssPv3(X0)
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p2010,p1277]) ).
cnf(p2012,plain,
( ssPv4(skf1(X0))
| ssPv3(X0)
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p2011]) ).
cnf(p2013,plain,
( ssPv3(X0)
| ssPv1(X0)
| ~ ssPv2(X0)
| ssPv3(X0)
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p2012,p54]) ).
cnf(p2022,plain,
( ssPv3(X0)
| ~ ssPv2(X0)
| ssPv3(X0)
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p2013]) ).
cnf(p2025,plain,
( ~ ssPv2(X0)
| ssPv3(X0)
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p2022]) ).
cnf(p2026,plain,
( ssPv1(X0)
| ssPv3(X0)
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p2025,p1277]) ).
cnf(p2027,plain,
( ssPv3(X0)
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p2026]) ).
cnf(p2034,plain,
( ssPv1(X0)
| ssPv4(skf1(X0))
| ~ ssPv3(X0)
| ssPv1(skf1(X0)) ),
inference(resolution,[status(thm)],[p2027,p127]) ).
cnf(p2058,plain,
( ssPv1(X0)
| ssPv1(X0)
| ssPv4(skf1(X0))
| ssPv1(skf1(X0)) ),
inference(resolution,[status(thm)],[p2034,p2027]) ).
cnf(p2061,plain,
( ssPv1(X0)
| ssPv4(skf1(X0))
| ssPv1(skf1(X0)) ),
inference(factoring,[status(thm)],[p2058]) ).
cnf(p2062,plain,
( ssPv1(X0)
| ~ ssPv3(X0)
| ~ ssPv3(skf1(X0))
| ssPv1(X0)
| ssPv1(skf1(X0)) ),
inference(resolution,[status(thm)],[p2061,p161]) ).
cnf(p2128,plain,
( ~ ssPv3(X0)
| ~ ssPv3(skf1(X0))
| ssPv1(X0)
| ssPv1(skf1(X0)) ),
inference(factoring,[status(thm)],[p2062]) ).
cnf(p2129,plain,
( ssPv1(skf1(X0))
| ~ ssPv3(X0)
| ssPv1(X0)
| ssPv1(skf1(X0)) ),
inference(resolution,[status(thm)],[p2128,p2027]) ).
cnf(p2130,plain,
( ~ ssPv3(X0)
| ssPv1(X0)
| ssPv1(skf1(X0)) ),
inference(factoring,[status(thm)],[p2129]) ).
cnf(p2131,plain,
( ssPv1(X0)
| ssPv1(X0)
| ssPv1(skf1(X0)) ),
inference(resolution,[status(thm)],[p2130,p2027]) ).
cnf(p2132,plain,
( ssPv1(X0)
| ssPv1(skf1(X0)) ),
inference(factoring,[status(thm)],[p2131]) ).
cnf(p573,plain,
( ssPv3(X0)
| ssPv2(X0)
| ssPv3(skf1(X0))
| ssPv2(skf1(X0)) ),
inference(resolution,[status(thm)],[p571,p534]) ).
cnf(f21,negated_conjecture,
( ssPv2(U)
| ssPv2(W)
| ~ ssPv1(U)
| ~ ssRr(U,W)
| ~ ssPv3(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause22) ).
fof(f21_nnf,plain,
! [U,V,W] :
( ssPv2(U)
| ssPv2(W)
| ~ ssPv1(U)
| ~ ssRr(U,W)
| ~ ssPv3(V)
| ~ ssRr(U,V) ),
inference(nnf_transformation,[status(thm)],[f21]) ).
fof(f21_sk,plain,
! [U,V,W] :
( ssPv2(U)
| ssPv2(W)
| ~ ssPv1(U)
| ~ ssRr(U,W)
| ~ ssPv3(V)
| ~ ssRr(U,V) ),
inference(skolemisation,[status(esa)],[f21_nnf]) ).
cnf(c21,plain,
( ssPv2(X0)
| ssPv2(X2)
| ~ ssPv1(X0)
| ~ ssRr(X0,X2)
| ~ ssPv3(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f21_sk]) ).
cnf(p106,plain,
( ssPv2(X0)
| ssPv2(X1)
| ~ ssPv1(X0)
| ~ ssPv3(X1)
| ~ ssRr(X0,X1) ),
inference(factoring,[status(thm)],[c21]) ).
cnf(p110,plain,
( ssPv2(X0)
| ssPv2(skf1(X0))
| ~ ssPv1(X0)
| ~ ssPv3(skf1(X0)) ),
inference(resolution,[status(thm)],[p106,c0]) ).
cnf(p577,plain,
( ssPv2(X0)
| ssPv2(skf1(X0))
| ~ ssPv1(X0)
| ssPv3(X0)
| ssPv2(X0)
| ssPv2(skf1(X0)) ),
inference(resolution,[status(thm)],[p573,p110]) ).
cnf(p613,plain,
( ssPv2(X0)
| ~ ssPv1(X0)
| ssPv3(X0)
| ssPv2(X0)
| ssPv2(skf1(X0)) ),
inference(factoring,[status(thm)],[p577]) ).
cnf(p615,plain,
( ~ ssPv1(X0)
| ssPv3(X0)
| ssPv2(X0)
| ssPv2(skf1(X0)) ),
inference(factoring,[status(thm)],[p613]) ).
cnf(p2138,plain,
( ssPv3(skf1(X0))
| ssPv2(skf1(X0))
| ssPv2(skf1(skf1(X0)))
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p2132,p615]) ).
cnf(f34,negated_conjecture,
( ssPv2(U)
| ~ ssPv4(U)
| ~ ssPv1(W)
| ~ ssRr(U,W)
| ~ ssPv2(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause35) ).
fof(f34_nnf,plain,
! [U,V,W] :
( ssPv2(U)
| ~ ssPv4(U)
| ~ ssPv1(W)
| ~ ssRr(U,W)
| ~ ssPv2(V)
| ~ ssRr(U,V) ),
inference(nnf_transformation,[status(thm)],[f34]) ).
fof(f34_sk,plain,
! [U,V,W] :
( ssPv2(U)
| ~ ssPv4(U)
| ~ ssPv1(W)
| ~ ssRr(U,W)
| ~ ssPv2(V)
| ~ ssRr(U,V) ),
inference(skolemisation,[status(esa)],[f34_nnf]) ).
cnf(c34,plain,
( ssPv2(X0)
| ~ ssPv4(X0)
| ~ ssPv1(X2)
| ~ ssRr(X0,X2)
| ~ ssPv2(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f34_sk]) ).
cnf(p153,plain,
( ssPv2(X0)
| ~ ssPv4(X0)
| ~ ssPv1(X1)
| ~ ssPv2(X1)
| ~ ssRr(X0,X1) ),
inference(factoring,[status(thm)],[c34]) ).
cnf(p155,plain,
( ssPv2(X0)
| ~ ssPv4(X0)
| ~ ssPv1(skf1(X0))
| ~ ssPv2(skf1(X0)) ),
inference(resolution,[status(thm)],[p153,c0]) ).
cnf(p2209,plain,
( ssPv2(skf1(X0))
| ~ ssPv4(skf1(X0))
| ~ ssPv1(skf1(skf1(X0)))
| ssPv3(skf1(X0))
| ssPv2(skf1(X0))
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p2138,p155]) ).
cnf(p2951,plain,
( ~ ssPv4(skf1(X0))
| ~ ssPv1(skf1(skf1(X0)))
| ssPv3(skf1(X0))
| ssPv2(skf1(X0))
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p2209]) ).
cnf(f46,negated_conjecture,
( ssPv4(X)
| ~ ssPv1(U)
| ~ ssRr(U,X)
| ~ ssPv2(W)
| ~ ssRr(U,W)
| ~ ssPv3(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause47) ).
fof(f46_nnf,plain,
! [U,V,W,X] :
( ssPv4(X)
| ~ ssPv1(U)
| ~ ssRr(U,X)
| ~ ssPv2(W)
| ~ ssRr(U,W)
| ~ ssPv3(V)
| ~ ssRr(U,V) ),
inference(nnf_transformation,[status(thm)],[f46]) ).
fof(f46_sk,plain,
! [U,V,W,X] :
( ssPv4(X)
| ~ ssPv1(U)
| ~ ssRr(U,X)
| ~ ssPv2(W)
| ~ ssRr(U,W)
| ~ ssPv3(V)
| ~ ssRr(U,V) ),
inference(skolemisation,[status(esa)],[f46_nnf]) ).
cnf(c46,plain,
( ssPv4(X3)
| ~ ssPv1(X0)
| ~ ssRr(X0,X3)
| ~ ssPv2(X2)
| ~ ssRr(X0,X2)
| ~ ssPv3(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f46_sk]) ).
cnf(p225,plain,
( ssPv4(X2)
| ~ ssPv1(X0)
| ~ ssRr(X0,X2)
| ~ ssPv2(X1)
| ~ ssPv3(X1)
| ~ ssRr(X0,X1) ),
inference(factoring,[status(thm)],[c46]) ).
cnf(p267,plain,
( ssPv4(X1)
| ~ ssPv1(X0)
| ~ ssPv2(X1)
| ~ ssPv3(X1)
| ~ ssRr(X0,X1) ),
inference(factoring,[status(thm)],[p225]) ).
cnf(p269,plain,
( ssPv4(skf1(X0))
| ~ ssPv1(X0)
| ~ ssPv2(skf1(X0))
| ~ ssPv3(skf1(X0)) ),
inference(resolution,[status(thm)],[p267,c0]) ).
cnf(p2041,plain,
( ssPv4(skf1(X0))
| ~ ssPv1(X0)
| ~ ssPv2(skf1(X0))
| ssPv1(skf1(X0)) ),
inference(resolution,[status(thm)],[p2027,p269]) ).
cnf(p2070,plain,
( ssPv1(skf1(X0))
| ssPv4(skf1(X0))
| ~ ssPv1(X0)
| ssPv1(skf1(X0)) ),
inference(resolution,[status(thm)],[p2041,p1277]) ).
cnf(p2072,plain,
( ssPv4(skf1(X0))
| ~ ssPv1(X0)
| ssPv1(skf1(X0)) ),
inference(factoring,[status(thm)],[p2070]) ).
cnf(p2139,plain,
( ssPv4(skf1(skf1(X0)))
| ssPv1(skf1(skf1(X0)))
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p2132,p2072]) ).
cnf(f6,negated_conjecture,
( ~ ssPv4(U)
| ~ ssPv3(U)
| ~ ssPv2(U)
| ~ ssPv1(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause7) ).
fof(f6_nnf,plain,
! [U,V] :
( ~ ssPv4(U)
| ~ ssPv3(U)
| ~ ssPv2(U)
| ~ ssPv1(V)
| ~ ssRr(U,V) ),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [U,V] :
( ~ ssPv4(U)
| ~ ssPv3(U)
| ~ ssPv2(U)
| ~ ssPv1(V)
| ~ ssRr(U,V) ),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c6,plain,
( ~ ssPv4(X0)
| ~ ssPv3(X0)
| ~ ssPv2(X0)
| ~ ssPv1(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(p56,plain,
( ~ ssPv4(X0)
| ~ ssPv3(X0)
| ~ ssPv2(X0)
| ~ ssPv1(skf1(X0)) ),
inference(resolution,[status(thm)],[c6,c0]) ).
cnf(p2135,plain,
( ~ ssPv4(X0)
| ~ ssPv3(X0)
| ~ ssPv2(X0)
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p2132,p56]) ).
cnf(p2140,plain,
( ssPv1(X0)
| ~ ssPv4(X0)
| ~ ssPv3(X0)
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p2135,p1277]) ).
cnf(p2141,plain,
( ~ ssPv4(X0)
| ~ ssPv3(X0)
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p2140]) ).
cnf(p2142,plain,
( ssPv1(X0)
| ~ ssPv4(X0)
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p2141,p2027]) ).
cnf(p2144,plain,
( ~ ssPv4(X0)
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p2142]) ).
cnf(p2161,plain,
( ssPv1(skf1(skf1(X0)))
| ssPv1(skf1(skf1(X0)))
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p2139,p2144]) ).
cnf(p2162,plain,
( ssPv1(skf1(skf1(X0)))
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p2161]) ).
cnf(p3020,plain,
( ssPv1(X0)
| ~ ssPv4(skf1(X0))
| ssPv3(skf1(X0))
| ssPv2(skf1(X0))
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p2951,p2162]) ).
cnf(p3022,plain,
( ~ ssPv4(skf1(X0))
| ssPv3(skf1(X0))
| ssPv2(skf1(X0))
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p3020]) ).
cnf(p3023,plain,
( ssPv3(skf1(X0))
| ssPv2(skf1(X0))
| ssPv3(skf1(X0))
| ssPv2(skf1(X0))
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p3022,p534]) ).
cnf(p3024,plain,
( ssPv3(skf1(X0))
| ssPv3(skf1(X0))
| ssPv2(skf1(X0))
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p3023]) ).
cnf(p3026,plain,
( ssPv3(skf1(X0))
| ssPv2(skf1(X0))
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p3024]) ).
cnf(p3028,plain,
( ssPv1(X0)
| ssPv4(skf1(X0))
| ~ ssPv3(X0)
| ssPv2(skf1(X0))
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p3026,p127]) ).
cnf(p3037,plain,
( ssPv4(skf1(X0))
| ~ ssPv3(X0)
| ssPv2(skf1(X0))
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p3028]) ).
cnf(p3038,plain,
( ssPv1(X0)
| ssPv4(skf1(X0))
| ssPv2(skf1(X0))
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p3037,p2027]) ).
cnf(p3039,plain,
( ssPv4(skf1(X0))
| ssPv2(skf1(X0))
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p3038]) ).
cnf(p3041,plain,
( ssPv1(X0)
| ~ ssPv3(X0)
| ~ ssPv3(skf1(X0))
| ssPv2(skf1(X0))
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p3039,p161]) ).
cnf(p3050,plain,
( ~ ssPv3(X0)
| ~ ssPv3(skf1(X0))
| ssPv2(skf1(X0))
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p3041]) ).
cnf(p3051,plain,
( ssPv2(skf1(X0))
| ssPv1(X0)
| ~ ssPv3(X0)
| ssPv2(skf1(X0))
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p3050,p3026]) ).
cnf(p3069,plain,
( ssPv1(X0)
| ~ ssPv3(X0)
| ssPv2(skf1(X0))
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p3051]) ).
cnf(p3070,plain,
( ~ ssPv3(X0)
| ssPv2(skf1(X0))
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p3069]) ).
cnf(p3071,plain,
( ssPv1(X0)
| ssPv2(skf1(X0))
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p3070,p2027]) ).
cnf(p3072,plain,
( ssPv2(skf1(X0))
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p3071]) ).
cnf(p2164,plain,
( ssPv4(skf1(X0))
| ssPv3(skf1(X0))
| ~ ssPv2(skf1(X0))
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p2162,p53]) ).
cnf(p3080,plain,
( ssPv4(skf1(X0))
| ssPv3(skf1(X0))
| ssPv1(X0)
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p3072,p2164]) ).
cnf(p3086,plain,
( ssPv4(skf1(X0))
| ssPv3(skf1(X0))
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p3080]) ).
cnf(f50,negated_conjecture,
( ~ ssPv3(U)
| ~ ssPv1(X)
| ~ ssRr(U,X)
| ~ ssPv2(W)
| ~ ssRr(U,W)
| ~ ssPv4(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause51) ).
fof(f50_nnf,plain,
! [U,V,W,X] :
( ~ ssPv3(U)
| ~ ssPv1(X)
| ~ ssRr(U,X)
| ~ ssPv2(W)
| ~ ssRr(U,W)
| ~ ssPv4(V)
| ~ ssRr(U,V) ),
inference(nnf_transformation,[status(thm)],[f50]) ).
fof(f50_sk,plain,
! [U,V,W,X] :
( ~ ssPv3(U)
| ~ ssPv1(X)
| ~ ssRr(U,X)
| ~ ssPv2(W)
| ~ ssRr(U,W)
| ~ ssPv4(V)
| ~ ssRr(U,V) ),
inference(skolemisation,[status(esa)],[f50_nnf]) ).
cnf(c50,plain,
( ~ ssPv3(X0)
| ~ ssPv1(X3)
| ~ ssRr(X0,X3)
| ~ ssPv2(X2)
| ~ ssRr(X0,X2)
| ~ ssPv4(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f50_sk]) ).
cnf(p253,plain,
( ~ ssPv3(X0)
| ~ ssPv1(X2)
| ~ ssRr(X0,X2)
| ~ ssPv2(X1)
| ~ ssPv4(X1)
| ~ ssRr(X0,X1) ),
inference(factoring,[status(thm)],[c50]) ).
cnf(p298,plain,
( ~ ssPv3(X0)
| ~ ssPv1(X1)
| ~ ssPv2(X1)
| ~ ssPv4(X1)
| ~ ssRr(X0,X1) ),
inference(factoring,[status(thm)],[p253]) ).
cnf(p300,plain,
( ~ ssPv3(X0)
| ~ ssPv1(skf1(X0))
| ~ ssPv2(skf1(X0))
| ~ ssPv4(skf1(X0)) ),
inference(resolution,[status(thm)],[p298,c0]) ).
cnf(p3089,plain,
( ~ ssPv3(X0)
| ~ ssPv1(skf1(X0))
| ~ ssPv2(skf1(X0))
| ssPv3(skf1(X0))
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p3086,p300]) ).
cnf(p3132,plain,
( ssPv1(X0)
| ~ ssPv3(X0)
| ~ ssPv1(skf1(X0))
| ssPv3(skf1(X0))
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p3089,p3072]) ).
cnf(p3133,plain,
( ~ ssPv3(X0)
| ~ ssPv1(skf1(X0))
| ssPv3(skf1(X0))
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p3132]) ).
cnf(p3134,plain,
( ssPv1(X0)
| ~ ssPv3(X0)
| ssPv3(skf1(X0))
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p3133,p2132]) ).
cnf(p3135,plain,
( ~ ssPv3(X0)
| ssPv3(skf1(X0))
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p3134]) ).
cnf(p3137,plain,
( ssPv1(X0)
| ssPv3(skf1(X0))
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p3135,p2027]) ).
cnf(p3138,plain,
( ssPv3(skf1(X0))
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p3137]) ).
cnf(p3139,plain,
( ssPv1(X0)
| ssPv4(skf1(X0))
| ~ ssPv3(X0)
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p3138,p127]) ).
cnf(p3163,plain,
( ssPv4(skf1(X0))
| ~ ssPv3(X0)
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p3139]) ).
cnf(p3164,plain,
( ssPv1(X0)
| ssPv4(skf1(X0))
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p3163,p2027]) ).
cnf(p3165,plain,
( ssPv4(skf1(X0))
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p3164]) ).
cnf(p2166,plain,
( ~ ssPv4(skf1(X0))
| ~ ssPv3(skf1(X0))
| ~ ssPv2(skf1(X0))
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p2162,p56]) ).
cnf(p3081,plain,
( ~ ssPv4(skf1(X0))
| ~ ssPv3(skf1(X0))
| ssPv1(X0)
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p3072,p2166]) ).
cnf(p3094,plain,
( ~ ssPv4(skf1(X0))
| ~ ssPv3(skf1(X0))
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p3081]) ).
cnf(p3150,plain,
( ~ ssPv4(skf1(X0))
| ssPv1(X0)
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p3138,p3094]) ).
cnf(p3151,plain,
( ~ ssPv4(skf1(X0))
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p3150]) ).
cnf(p3178,plain,
( ssPv1(X0)
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p3165,p3151]) ).
cnf(p3179,plain,
ssPv1(X0),
inference(factoring,[status(thm)],[p3178]) ).
cnf(p3188,plain,
( ssPv3(X0)
| ssPv2(X0)
| ssPv2(skf1(X0)) ),
inference(resolution,[status(thm)],[p3179,p615]) ).
cnf(p3211,plain,
( ssPv2(X0)
| ~ ssPv4(X0)
| ~ ssPv1(skf1(X0))
| ssPv3(X0)
| ssPv2(X0) ),
inference(resolution,[status(thm)],[p3188,p155]) ).
cnf(p3275,plain,
( ~ ssPv4(X0)
| ~ ssPv1(skf1(X0))
| ssPv3(X0)
| ssPv2(X0) ),
inference(factoring,[status(thm)],[p3211]) ).
cnf(p3276,plain,
( ~ ssPv4(X0)
| ssPv3(X0)
| ssPv2(X0) ),
inference(resolution,[status(thm)],[p3275,p3179]) ).
cnf(p3277,plain,
( ssPv3(X0)
| ssPv2(X0)
| ssPv3(X0)
| ssPv2(X0) ),
inference(resolution,[status(thm)],[p3276,p534]) ).
cnf(p3278,plain,
( ssPv3(X0)
| ssPv3(X0)
| ssPv2(X0) ),
inference(factoring,[status(thm)],[p3277]) ).
cnf(p3280,plain,
( ssPv3(X0)
| ssPv2(X0) ),
inference(factoring,[status(thm)],[p3278]) ).
cnf(p3284,plain,
( ssPv2(X0)
| ssPv2(skf1(X0))
| ~ ssPv1(X0)
| ssPv2(skf1(X0)) ),
inference(resolution,[status(thm)],[p3280,p110]) ).
cnf(p3302,plain,
( ssPv2(X0)
| ~ ssPv1(X0)
| ssPv2(skf1(X0)) ),
inference(factoring,[status(thm)],[p3284]) ).
cnf(p3303,plain,
( ssPv2(X0)
| ssPv2(skf1(X0)) ),
inference(resolution,[status(thm)],[p3302,p3179]) ).
cnf(f20,negated_conjecture,
( ssPv2(U)
| ssPv4(W)
| ~ ssPv1(U)
| ~ ssRr(U,W)
| ~ ssPv2(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause21) ).
fof(f20_nnf,plain,
! [U,V,W] :
( ssPv2(U)
| ssPv4(W)
| ~ ssPv1(U)
| ~ ssRr(U,W)
| ~ ssPv2(V)
| ~ ssRr(U,V) ),
inference(nnf_transformation,[status(thm)],[f20]) ).
fof(f20_sk,plain,
! [U,V,W] :
( ssPv2(U)
| ssPv4(W)
| ~ ssPv1(U)
| ~ ssRr(U,W)
| ~ ssPv2(V)
| ~ ssRr(U,V) ),
inference(skolemisation,[status(esa)],[f20_nnf]) ).
cnf(c20,plain,
( ssPv2(X0)
| ssPv4(X2)
| ~ ssPv1(X0)
| ~ ssRr(X0,X2)
| ~ ssPv2(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f20_sk]) ).
cnf(p103,plain,
( ssPv2(X0)
| ssPv4(X1)
| ~ ssPv1(X0)
| ~ ssPv2(X1)
| ~ ssRr(X0,X1) ),
inference(factoring,[status(thm)],[c20]) ).
cnf(p105,plain,
( ssPv2(X0)
| ssPv4(skf1(X0))
| ~ ssPv1(X0)
| ~ ssPv2(skf1(X0)) ),
inference(resolution,[status(thm)],[p103,c0]) ).
cnf(p3304,plain,
( ssPv2(X0)
| ssPv4(skf1(X0))
| ~ ssPv1(X0)
| ssPv2(X0) ),
inference(resolution,[status(thm)],[p3303,p105]) ).
cnf(p3337,plain,
( ssPv4(skf1(X0))
| ~ ssPv1(X0)
| ssPv2(X0) ),
inference(factoring,[status(thm)],[p3304]) ).
cnf(p3338,plain,
( ssPv4(skf1(X0))
| ssPv2(X0) ),
inference(resolution,[status(thm)],[p3337,p3179]) ).
cnf(f47,negated_conjecture,
( ssPv3(X)
| ~ ssPv1(U)
| ~ ssRr(U,X)
| ~ ssPv2(W)
| ~ ssRr(U,W)
| ~ ssPv4(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause48) ).
fof(f47_nnf,plain,
! [U,V,W,X] :
( ssPv3(X)
| ~ ssPv1(U)
| ~ ssRr(U,X)
| ~ ssPv2(W)
| ~ ssRr(U,W)
| ~ ssPv4(V)
| ~ ssRr(U,V) ),
inference(nnf_transformation,[status(thm)],[f47]) ).
fof(f47_sk,plain,
! [U,V,W,X] :
( ssPv3(X)
| ~ ssPv1(U)
| ~ ssRr(U,X)
| ~ ssPv2(W)
| ~ ssRr(U,W)
| ~ ssPv4(V)
| ~ ssRr(U,V) ),
inference(skolemisation,[status(esa)],[f47_nnf]) ).
cnf(c47,plain,
( ssPv3(X3)
| ~ ssPv1(X0)
| ~ ssRr(X0,X3)
| ~ ssPv2(X2)
| ~ ssRr(X0,X2)
| ~ ssPv4(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f47_sk]) ).
cnf(p233,plain,
( ssPv3(X2)
| ~ ssPv1(X0)
| ~ ssRr(X0,X2)
| ~ ssPv2(X1)
| ~ ssPv4(X1)
| ~ ssRr(X0,X1) ),
inference(factoring,[status(thm)],[c47]) ).
cnf(p273,plain,
( ssPv3(X1)
| ~ ssPv1(X0)
| ~ ssPv2(X1)
| ~ ssPv4(X1)
| ~ ssRr(X0,X1) ),
inference(factoring,[status(thm)],[p233]) ).
cnf(p275,plain,
( ssPv3(skf1(X0))
| ~ ssPv1(X0)
| ~ ssPv2(skf1(X0))
| ~ ssPv4(skf1(X0)) ),
inference(resolution,[status(thm)],[p273,c0]) ).
cnf(p3343,plain,
( ssPv3(skf1(X0))
| ~ ssPv1(X0)
| ~ ssPv2(skf1(X0))
| ssPv2(X0) ),
inference(resolution,[status(thm)],[p3338,p275]) ).
cnf(p3374,plain,
( ssPv2(X0)
| ssPv3(skf1(X0))
| ~ ssPv1(X0)
| ssPv2(X0) ),
inference(resolution,[status(thm)],[p3343,p3303]) ).
cnf(p3375,plain,
( ssPv3(skf1(X0))
| ~ ssPv1(X0)
| ssPv2(X0) ),
inference(factoring,[status(thm)],[p3374]) ).
cnf(p3376,plain,
( ssPv3(skf1(X0))
| ssPv2(X0) ),
inference(resolution,[status(thm)],[p3375,p3179]) ).
cnf(p3182,plain,
( ~ ssPv4(X0)
| ~ ssPv3(X0)
| ~ ssPv2(X0) ),
inference(resolution,[status(thm)],[p3179,p56]) ).
cnf(p3313,plain,
( ~ ssPv4(skf1(X0))
| ~ ssPv3(skf1(X0))
| ssPv2(X0) ),
inference(resolution,[status(thm)],[p3303,p3182]) ).
cnf(p3389,plain,
( ~ ssPv4(skf1(X0))
| ssPv2(X0)
| ssPv2(X0) ),
inference(resolution,[status(thm)],[p3376,p3313]) ).
cnf(p3392,plain,
( ~ ssPv4(skf1(X0))
| ssPv2(X0) ),
inference(factoring,[status(thm)],[p3389]) ).
cnf(p3393,plain,
( ssPv2(X0)
| ssPv2(X0) ),
inference(resolution,[status(thm)],[p3392,p3338]) ).
cnf(p3394,plain,
ssPv2(X0),
inference(factoring,[status(thm)],[p3393]) ).
cnf(f5,negated_conjecture,
( ssPv3(V)
| ~ ssPv4(U)
| ~ ssPv2(U)
| ~ ssPv1(U)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause6) ).
fof(f5_nnf,plain,
! [U,V] :
( ssPv3(V)
| ~ ssPv4(U)
| ~ ssPv2(U)
| ~ ssPv1(U)
| ~ ssRr(U,V) ),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [U,V] :
( ssPv3(V)
| ~ ssPv4(U)
| ~ ssPv2(U)
| ~ ssPv1(U)
| ~ ssRr(U,V) ),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c5,plain,
( ssPv3(X1)
| ~ ssPv4(X0)
| ~ ssPv2(X0)
| ~ ssPv1(X0)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p55,plain,
( ssPv3(skf1(X0))
| ~ ssPv4(X0)
| ~ ssPv2(X0)
| ~ ssPv1(X0) ),
inference(resolution,[status(thm)],[c5,c0]) ).
cnf(p3181,plain,
( ssPv3(skf1(X0))
| ~ ssPv4(X0)
| ~ ssPv2(X0) ),
inference(resolution,[status(thm)],[p3179,p55]) ).
cnf(p3401,plain,
( ssPv3(skf1(X0))
| ~ ssPv4(X0) ),
inference(resolution,[status(thm)],[p3394,p3181]) ).
cnf(p3180,plain,
( ssPv4(X0)
| ssPv3(X0)
| ~ ssPv2(X0) ),
inference(resolution,[status(thm)],[p3179,p53]) ).
cnf(p3399,plain,
( ssPv4(X0)
| ssPv3(X0) ),
inference(resolution,[status(thm)],[p3394,p3180]) ).
cnf(p3415,plain,
( ssPv3(X0)
| ssPv3(skf1(X0)) ),
inference(resolution,[status(thm)],[p3401,p3399]) ).
cnf(p3420,plain,
( ssPv4(skf1(X0))
| ~ ssPv1(X0)
| ~ ssPv2(skf1(X0))
| ssPv3(X0) ),
inference(resolution,[status(thm)],[p3415,p269]) ).
cnf(p3427,plain,
( ssPv4(skf1(X0))
| ~ ssPv1(X0)
| ssPv3(X0) ),
inference(resolution,[status(thm)],[p3420,p3394]) ).
cnf(p3428,plain,
( ssPv4(skf1(X0))
| ssPv3(X0) ),
inference(resolution,[status(thm)],[p3427,p3179]) ).
cnf(p3400,plain,
( ~ ssPv4(X0)
| ~ ssPv3(X0) ),
inference(resolution,[status(thm)],[p3394,p3182]) ).
cnf(p3425,plain,
( ~ ssPv4(skf1(X0))
| ssPv3(X0) ),
inference(resolution,[status(thm)],[p3415,p3400]) ).
cnf(p3433,plain,
( ssPv3(X0)
| ssPv3(X0) ),
inference(resolution,[status(thm)],[p3428,p3425]) ).
cnf(p3434,plain,
ssPv3(X0),
inference(factoring,[status(thm)],[p3433]) ).
cnf(p3435,plain,
( ssPv4(skf1(X0))
| ~ ssPv1(X0)
| ~ ssPv2(skf1(X0)) ),
inference(resolution,[status(thm)],[p3434,p269]) ).
cnf(p3446,plain,
( ssPv4(skf1(X0))
| ~ ssPv1(X0) ),
inference(resolution,[status(thm)],[p3435,p3394]) ).
cnf(p3447,plain,
ssPv4(skf1(X0)),
inference(resolution,[status(thm)],[p3446,p3179]) ).
cnf(p3445,plain,
~ ssPv4(X0),
inference(resolution,[status(thm)],[p3434,p3400]) ).
cnf(p3448,plain,
$false,
inference(resolution,[status(thm)],[p3447,p3445]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN755-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.12/10.38 % Computer : n010.cluster.edu
% 0.12/10.38 % Model : x86_64 x86_64
% 0.12/10.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/10.38 % Memory : 8046.5625MB
% 0.12/10.38 % OS : Linux 6.8.0-71-generic
% 0.12/10.39 % CPULimit : 300
% 0.12/10.39 % WCLimit : 300
% 0.12/10.39 % DateTime : Fri Sep 25 02:15:41 UTC 2026
% 0.12/10.39 % CPUTime :
% 0.12/10.39 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 5.74/11.63 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.74/11.63 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------