%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SYN796-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n007.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:36:01 PM UTC 2026
% Result : Unsatisfiable 21.86s 3.38s
% Output : Proof 21.86s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)
% Comments :
%------------------------------------------------------------------------------
cnf(f7,negated_conjecture,
( ssPv2(V)
| ssPv1(V)
| ssPv2(W)
| ssPv4(U)
| ~ ssRr(V,W)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause8) ).
fof(f7_nnf,plain,
! [U,V,W] :
( ssPv2(V)
| ssPv1(V)
| ssPv2(W)
| ssPv4(U)
| ~ ssRr(V,W)
| ~ ssRr(U,V) ),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [U,V,W] :
( ssPv2(V)
| ssPv1(V)
| ssPv2(W)
| ssPv4(U)
| ~ ssRr(V,W)
| ~ ssRr(U,V) ),
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c7,plain,
( ssPv2(X1)
| ssPv1(X1)
| ssPv2(X2)
| ssPv4(X0)
| ~ ssRr(X1,X2)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(f0,negated_conjecture,
ssRr(skf3(U),U),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause1) ).
fof(f0_nnf,plain,
! [U] : ssRr(skf3(U),U),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [U] : ssRr(skf3(U),U),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
ssRr(skf3(X0),X0),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p69,plain,
( ssPv2(X0)
| ssPv1(X0)
| ssPv2(X1)
| ssPv4(skf3(X0))
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[c7,c0]) ).
cnf(f1,negated_conjecture,
ssRr(U,skf2(U)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause2) ).
fof(f1_nnf,plain,
! [U] : ssRr(U,skf2(U)),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [U] : ssRr(U,skf2(U)),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
ssRr(X0,skf2(X0)),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p81,plain,
( ssPv2(X0)
| ssPv1(X0)
| ssPv2(skf2(X0))
| ssPv4(skf3(X0)) ),
inference(resolution,[status(thm)],[p69,c1]) ).
cnf(f4,negated_conjecture,
( ssPv4(V)
| ssPv1(V)
| ssPv2(U)
| ~ ssPv2(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause5) ).
fof(f4_nnf,plain,
! [U,V] :
( ssPv4(V)
| ssPv1(V)
| ssPv2(U)
| ~ ssPv2(V)
| ~ ssRr(U,V) ),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [U,V] :
( ssPv4(V)
| ssPv1(V)
| ssPv2(U)
| ~ ssPv2(V)
| ~ ssRr(U,V) ),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c4,plain,
( ssPv4(X1)
| ssPv1(X1)
| ssPv2(X0)
| ~ ssPv2(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p60,plain,
( ssPv4(skf2(X0))
| ssPv1(skf2(X0))
| ssPv2(X0)
| ~ ssPv2(skf2(X0)) ),
inference(resolution,[status(thm)],[c4,c1]) ).
cnf(p87,plain,
( ssPv4(skf2(X0))
| ssPv1(skf2(X0))
| ssPv2(X0)
| ssPv2(X0)
| ssPv1(X0)
| ssPv4(skf3(X0)) ),
inference(resolution,[status(thm)],[p81,p60]) ).
cnf(p471,plain,
( ssPv4(skf2(X0))
| ssPv1(skf2(X0))
| ssPv2(X0)
| ssPv1(X0)
| ssPv4(skf3(X0)) ),
inference(factoring,[status(thm)],[p87]) ).
cnf(f27,negated_conjecture,
( ssPv2(U)
| ssPv1(U)
| ~ ssPv2(W)
| ~ ssRr(U,W)
| ~ ssPv4(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause28) ).
fof(f27_nnf,plain,
! [U,V,W] :
( ssPv2(U)
| ssPv1(U)
| ~ ssPv2(W)
| ~ ssRr(U,W)
| ~ ssPv4(V)
| ~ ssRr(U,V) ),
inference(nnf_transformation,[status(thm)],[f27]) ).
fof(f27_sk,plain,
! [U,V,W] :
( ssPv2(U)
| ssPv1(U)
| ~ ssPv2(W)
| ~ ssRr(U,W)
| ~ ssPv4(V)
| ~ ssRr(U,V) ),
inference(skolemisation,[status(esa)],[f27_nnf]) ).
cnf(c27,plain,
( ssPv2(X0)
| ssPv1(X0)
| ~ ssPv2(X2)
| ~ ssRr(X0,X2)
| ~ ssPv4(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f27_sk]) ).
cnf(p194,plain,
( ssPv2(X0)
| ssPv1(X0)
| ~ ssPv2(X1)
| ~ ssPv4(X1)
| ~ ssRr(X0,X1) ),
inference(factoring,[status(thm)],[c27]) ).
cnf(p198,plain,
( ssPv2(X0)
| ssPv1(X0)
| ~ ssPv2(skf2(X0))
| ~ ssPv4(skf2(X0)) ),
inference(resolution,[status(thm)],[p194,c1]) ).
cnf(p477,plain,
( ssPv2(X0)
| ssPv1(X0)
| ~ ssPv2(skf2(X0))
| ssPv1(skf2(X0))
| ssPv2(X0)
| ssPv1(X0)
| ssPv4(skf3(X0)) ),
inference(resolution,[status(thm)],[p471,p198]) ).
cnf(p1388,plain,
( ssPv2(X0)
| ~ ssPv2(skf2(X0))
| ssPv1(skf2(X0))
| ssPv2(X0)
| ssPv1(X0)
| ssPv4(skf3(X0)) ),
inference(factoring,[status(thm)],[p477]) ).
cnf(p1390,plain,
( ~ ssPv2(skf2(X0))
| ssPv1(skf2(X0))
| ssPv2(X0)
| ssPv1(X0)
| ssPv4(skf3(X0)) ),
inference(factoring,[status(thm)],[p1388]) ).
cnf(p1391,plain,
( ssPv2(X0)
| ssPv1(X0)
| ssPv4(skf3(X0))
| ssPv1(skf2(X0))
| ssPv2(X0)
| ssPv1(X0)
| ssPv4(skf3(X0)) ),
inference(resolution,[status(thm)],[p1390,p81]) ).
cnf(p1460,plain,
( ssPv2(X0)
| ssPv1(X0)
| ssPv1(skf2(X0))
| ssPv2(X0)
| ssPv1(X0)
| ssPv4(skf3(X0)) ),
inference(factoring,[status(thm)],[p1391]) ).
cnf(p1463,plain,
( ssPv2(X0)
| ssPv1(skf2(X0))
| ssPv2(X0)
| ssPv1(X0)
| ssPv4(skf3(X0)) ),
inference(factoring,[status(thm)],[p1460]) ).
cnf(p1465,plain,
( ssPv1(skf2(X0))
| ssPv2(X0)
| ssPv1(X0)
| ssPv4(skf3(X0)) ),
inference(factoring,[status(thm)],[p1463]) ).
cnf(f9,negated_conjecture,
( ssPv4(V)
| ssPv3(V)
| ssPv3(W)
| ~ ssRr(W,V)
| ~ ssPv4(U)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause10) ).
fof(f9_nnf,plain,
! [U,V,W] :
( ssPv4(V)
| ssPv3(V)
| ssPv3(W)
| ~ ssRr(W,V)
| ~ ssPv4(U)
| ~ ssRr(U,V) ),
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
! [U,V,W] :
( ssPv4(V)
| ssPv3(V)
| ssPv3(W)
| ~ ssRr(W,V)
| ~ ssPv4(U)
| ~ ssRr(U,V) ),
inference(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c9,plain,
( ssPv4(X1)
| ssPv3(X1)
| ssPv3(X2)
| ~ ssRr(X2,X1)
| ~ ssPv4(X0)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(p82,plain,
( ssPv4(X1)
| ssPv3(X1)
| ssPv3(X0)
| ~ ssPv4(X0)
| ~ ssRr(X0,X1) ),
inference(factoring,[status(thm)],[c9]) ).
cnf(p91,plain,
( ssPv4(X0)
| ssPv3(X0)
| ssPv3(skf3(X0))
| ~ ssPv4(skf3(X0)) ),
inference(resolution,[status(thm)],[p82,c0]) ).
cnf(p1469,plain,
( ssPv4(X0)
| ssPv3(X0)
| ssPv3(skf3(X0))
| ssPv1(skf2(X0))
| ssPv2(X0)
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p1465,p91]) ).
cnf(f19,negated_conjecture,
( ssPv2(W)
| ssPv3(U)
| ~ ssPv2(V)
| ~ ssPv1(V)
| ~ ssRr(W,V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause20) ).
fof(f19_nnf,plain,
! [U,V,W] :
( ssPv2(W)
| ssPv3(U)
| ~ ssPv2(V)
| ~ ssPv1(V)
| ~ ssRr(W,V)
| ~ ssRr(U,V) ),
inference(nnf_transformation,[status(thm)],[f19]) ).
fof(f19_sk,plain,
! [U,V,W] :
( ssPv2(W)
| ssPv3(U)
| ~ ssPv2(V)
| ~ ssPv1(V)
| ~ ssRr(W,V)
| ~ ssRr(U,V) ),
inference(skolemisation,[status(esa)],[f19_nnf]) ).
cnf(c19,plain,
( ssPv2(X2)
| ssPv3(X0)
| ~ ssPv2(X1)
| ~ ssPv1(X1)
| ~ ssRr(X2,X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f19_sk]) ).
cnf(p151,plain,
( ssPv2(X0)
| ssPv3(X0)
| ~ ssPv2(X1)
| ~ ssPv1(X1)
| ~ ssRr(X0,X1) ),
inference(factoring,[status(thm)],[c19]) ).
cnf(p155,plain,
( ssPv2(X0)
| ssPv3(X0)
| ~ ssPv2(skf2(X0))
| ~ ssPv1(skf2(X0)) ),
inference(resolution,[status(thm)],[p151,c1]) ).
cnf(p1517,plain,
( ssPv2(X0)
| ssPv3(X0)
| ~ ssPv2(skf2(X0))
| ssPv4(X0)
| ssPv3(X0)
| ssPv3(skf3(X0))
| ssPv2(X0)
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p1469,p155]) ).
cnf(p2341,plain,
( ssPv3(X0)
| ~ ssPv2(skf2(X0))
| ssPv4(X0)
| ssPv3(X0)
| ssPv3(skf3(X0))
| ssPv2(X0)
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p1517]) ).
cnf(p2343,plain,
( ~ ssPv2(skf2(X0))
| ssPv4(X0)
| ssPv3(X0)
| ssPv3(skf3(X0))
| ssPv2(X0)
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p2341]) ).
cnf(p2344,plain,
( ssPv2(X0)
| ssPv1(X0)
| ssPv4(skf3(X0))
| ssPv4(X0)
| ssPv3(X0)
| ssPv3(skf3(X0))
| ssPv2(X0)
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p2343,p81]) ).
cnf(p2405,plain,
( ssPv2(X0)
| ssPv4(skf3(X0))
| ssPv4(X0)
| ssPv3(X0)
| ssPv3(skf3(X0))
| ssPv2(X0)
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p2344]) ).
cnf(p2407,plain,
( ssPv4(skf3(X0))
| ssPv4(X0)
| ssPv3(X0)
| ssPv3(skf3(X0))
| ssPv2(X0)
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p2405]) ).
cnf(p2410,plain,
( ssPv4(X0)
| ssPv3(X0)
| ssPv3(skf3(X0))
| ssPv4(X0)
| ssPv3(X0)
| ssPv3(skf3(X0))
| ssPv2(X0)
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p2407,p91]) ).
cnf(p2437,plain,
( ssPv4(X0)
| ssPv3(X0)
| ssPv4(X0)
| ssPv3(X0)
| ssPv3(skf3(X0))
| ssPv2(X0)
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p2410]) ).
cnf(p2440,plain,
( ssPv4(X0)
| ssPv4(X0)
| ssPv3(X0)
| ssPv3(skf3(X0))
| ssPv2(X0)
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p2437]) ).
cnf(p2442,plain,
( ssPv4(X0)
| ssPv3(X0)
| ssPv3(skf3(X0))
| ssPv2(X0)
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p2440]) ).
cnf(f14,negated_conjecture,
( ssPv4(V)
| ssPv1(V)
| ssPv4(W)
| ~ ssRr(W,V)
| ~ ssPv3(U)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause15) ).
fof(f14_nnf,plain,
! [U,V,W] :
( ssPv4(V)
| ssPv1(V)
| ssPv4(W)
| ~ ssRr(W,V)
| ~ ssPv3(U)
| ~ ssRr(U,V) ),
inference(nnf_transformation,[status(thm)],[f14]) ).
fof(f14_sk,plain,
! [U,V,W] :
( ssPv4(V)
| ssPv1(V)
| ssPv4(W)
| ~ ssRr(W,V)
| ~ ssPv3(U)
| ~ ssRr(U,V) ),
inference(skolemisation,[status(esa)],[f14_nnf]) ).
cnf(c14,plain,
( ssPv4(X1)
| ssPv1(X1)
| ssPv4(X2)
| ~ ssRr(X2,X1)
| ~ ssPv3(X0)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(p120,plain,
( ssPv4(X1)
| ssPv1(X1)
| ssPv4(X0)
| ~ ssPv3(X0)
| ~ ssRr(X0,X1) ),
inference(factoring,[status(thm)],[c14]) ).
cnf(p125,plain,
( ssPv4(X0)
| ssPv1(X0)
| ssPv4(skf3(X0))
| ~ ssPv3(skf3(X0)) ),
inference(resolution,[status(thm)],[p120,c0]) ).
cnf(p2443,plain,
( ssPv4(X0)
| ssPv1(X0)
| ssPv4(skf3(X0))
| ssPv4(X0)
| ssPv3(X0)
| ssPv2(X0)
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p2442,p125]) ).
cnf(p2514,plain,
( ssPv4(X0)
| ssPv4(skf3(X0))
| ssPv4(X0)
| ssPv3(X0)
| ssPv2(X0)
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p2443]) ).
cnf(p2516,plain,
( ssPv4(skf3(X0))
| ssPv4(X0)
| ssPv3(X0)
| ssPv2(X0)
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p2514]) ).
cnf(p84,plain,
( ssPv4(X0)
| ssPv3(X0)
| ssPv3(X1)
| ~ ssRr(X1,X0)
| ~ ssPv4(skf3(X0)) ),
inference(resolution,[status(thm)],[c9,c0]) ).
cnf(p2517,plain,
( ssPv4(X0)
| ssPv3(X0)
| ssPv3(X1)
| ~ ssRr(X1,X0)
| ssPv4(X0)
| ssPv3(X0)
| ssPv2(X0)
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p2516,p84]) ).
cnf(p2658,plain,
( ssPv4(X0)
| ssPv3(X1)
| ~ ssRr(X1,X0)
| ssPv4(X0)
| ssPv3(X0)
| ssPv2(X0)
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p2517]) ).
cnf(p2660,plain,
( ssPv3(X1)
| ~ ssRr(X1,X0)
| ssPv4(X0)
| ssPv3(X0)
| ssPv2(X0)
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p2658]) ).
cnf(p2661,plain,
( ssPv3(X0)
| ssPv4(skf2(X0))
| ssPv3(skf2(X0))
| ssPv2(skf2(X0))
| ssPv1(skf2(X0)) ),
inference(resolution,[status(thm)],[p2660,c1]) ).
cnf(p2663,plain,
( ssPv4(skf2(X0))
| ssPv1(skf2(X0))
| ssPv2(X0)
| ssPv3(X0)
| ssPv4(skf2(X0))
| ssPv3(skf2(X0))
| ssPv1(skf2(X0)) ),
inference(resolution,[status(thm)],[p2661,p60]) ).
cnf(p3461,plain,
( ssPv4(skf2(X0))
| ssPv2(X0)
| ssPv3(X0)
| ssPv4(skf2(X0))
| ssPv3(skf2(X0))
| ssPv1(skf2(X0)) ),
inference(factoring,[status(thm)],[p2663]) ).
cnf(p3463,plain,
( ssPv2(X0)
| ssPv3(X0)
| ssPv4(skf2(X0))
| ssPv3(skf2(X0))
| ssPv1(skf2(X0)) ),
inference(factoring,[status(thm)],[p3461]) ).
cnf(f5,negated_conjecture,
( ssPv3(V)
| ssPv1(V)
| ssPv2(U)
| ~ ssPv4(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause6) ).
fof(f5_nnf,plain,
! [U,V] :
( ssPv3(V)
| ssPv1(V)
| ssPv2(U)
| ~ ssPv4(V)
| ~ ssRr(U,V) ),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [U,V] :
( ssPv3(V)
| ssPv1(V)
| ssPv2(U)
| ~ ssPv4(V)
| ~ ssRr(U,V) ),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c5,plain,
( ssPv3(X1)
| ssPv1(X1)
| ssPv2(X0)
| ~ ssPv4(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p62,plain,
( ssPv3(skf2(X0))
| ssPv1(skf2(X0))
| ssPv2(X0)
| ~ ssPv4(skf2(X0)) ),
inference(resolution,[status(thm)],[c5,c1]) ).
cnf(p3467,plain,
( ssPv3(skf2(X0))
| ssPv1(skf2(X0))
| ssPv2(X0)
| ssPv2(X0)
| ssPv3(X0)
| ssPv3(skf2(X0))
| ssPv1(skf2(X0)) ),
inference(resolution,[status(thm)],[p3463,p62]) ).
cnf(p3504,plain,
( ssPv3(skf2(X0))
| ssPv2(X0)
| ssPv2(X0)
| ssPv3(X0)
| ssPv3(skf2(X0))
| ssPv1(skf2(X0)) ),
inference(factoring,[status(thm)],[p3467]) ).
cnf(p3507,plain,
( ssPv2(X0)
| ssPv2(X0)
| ssPv3(X0)
| ssPv3(skf2(X0))
| ssPv1(skf2(X0)) ),
inference(factoring,[status(thm)],[p3504]) ).
cnf(p3509,plain,
( ssPv2(X0)
| ssPv3(X0)
| ssPv3(skf2(X0))
| ssPv1(skf2(X0)) ),
inference(factoring,[status(thm)],[p3507]) ).
cnf(f34,negated_conjecture,
( ssPv4(X)
| ssPv2(W)
| ssPv3(U)
| ~ ssPv1(V)
| ~ ssRr(V,X)
| ~ ssRr(W,V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause35) ).
fof(f34_nnf,plain,
! [U,V,W,X] :
( ssPv4(X)
| ssPv2(W)
| ssPv3(U)
| ~ ssPv1(V)
| ~ ssRr(V,X)
| ~ ssRr(W,V)
| ~ ssRr(U,V) ),
inference(nnf_transformation,[status(thm)],[f34]) ).
fof(f34_sk,plain,
! [U,V,W,X] :
( ssPv4(X)
| ssPv2(W)
| ssPv3(U)
| ~ ssPv1(V)
| ~ ssRr(V,X)
| ~ ssRr(W,V)
| ~ ssRr(U,V) ),
inference(skolemisation,[status(esa)],[f34_nnf]) ).
cnf(c34,plain,
( ssPv4(X3)
| ssPv2(X2)
| ssPv3(X0)
| ~ ssPv1(X1)
| ~ ssRr(X1,X3)
| ~ ssRr(X2,X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f34_sk]) ).
cnf(p246,plain,
( ssPv4(X2)
| ssPv2(X0)
| ssPv3(X0)
| ~ ssPv1(X1)
| ~ ssRr(X1,X2)
| ~ ssRr(X0,X1) ),
inference(factoring,[status(thm)],[c34]) ).
cnf(p379,plain,
( ssPv4(X1)
| ssPv2(X0)
| ssPv3(X0)
| ~ ssPv1(skf2(X0))
| ~ ssRr(skf2(X0),X1) ),
inference(resolution,[status(thm)],[p246,c1]) ).
cnf(p388,plain,
( ssPv4(skf2(skf2(X0)))
| ssPv2(X0)
| ssPv3(X0)
| ~ ssPv1(skf2(X0)) ),
inference(resolution,[status(thm)],[p379,c1]) ).
cnf(p3528,plain,
( ssPv4(skf2(skf2(X0)))
| ssPv2(X0)
| ssPv3(X0)
| ssPv2(X0)
| ssPv3(X0)
| ssPv3(skf2(X0)) ),
inference(resolution,[status(thm)],[p3509,p388]) ).
cnf(p3635,plain,
( ssPv4(skf2(skf2(X0)))
| ssPv2(X0)
| ssPv2(X0)
| ssPv3(X0)
| ssPv3(skf2(X0)) ),
inference(factoring,[status(thm)],[p3528]) ).
cnf(p3637,plain,
( ssPv4(skf2(skf2(X0)))
| ssPv2(X0)
| ssPv3(X0)
| ssPv3(skf2(X0)) ),
inference(factoring,[status(thm)],[p3635]) ).
cnf(f24,negated_conjecture,
( ssPv2(V)
| ssPv2(U)
| ~ ssPv1(V)
| ~ ssPv4(W)
| ~ ssRr(V,W)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause25) ).
fof(f24_nnf,plain,
! [U,V,W] :
( ssPv2(V)
| ssPv2(U)
| ~ ssPv1(V)
| ~ ssPv4(W)
| ~ ssRr(V,W)
| ~ ssRr(U,V) ),
inference(nnf_transformation,[status(thm)],[f24]) ).
fof(f24_sk,plain,
! [U,V,W] :
( ssPv2(V)
| ssPv2(U)
| ~ ssPv1(V)
| ~ ssPv4(W)
| ~ ssRr(V,W)
| ~ ssRr(U,V) ),
inference(skolemisation,[status(esa)],[f24_nnf]) ).
cnf(c24,plain,
( ssPv2(X1)
| ssPv2(X0)
| ~ ssPv1(X1)
| ~ ssPv4(X2)
| ~ ssRr(X1,X2)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f24_sk]) ).
cnf(p180,plain,
( ssPv2(skf2(X0))
| ssPv2(X0)
| ~ ssPv1(skf2(X0))
| ~ ssPv4(X1)
| ~ ssRr(skf2(X0),X1) ),
inference(resolution,[status(thm)],[c24,c1]) ).
cnf(p342,plain,
( ssPv2(skf2(X0))
| ssPv2(X0)
| ~ ssPv1(skf2(X0))
| ~ ssPv4(skf2(skf2(X0))) ),
inference(resolution,[status(thm)],[p180,c1]) ).
cnf(p3648,plain,
( ssPv2(skf2(X0))
| ssPv2(X0)
| ~ ssPv1(skf2(X0))
| ssPv2(X0)
| ssPv3(X0)
| ssPv3(skf2(X0)) ),
inference(resolution,[status(thm)],[p3637,p342]) ).
cnf(p3709,plain,
( ssPv2(skf2(X0))
| ~ ssPv1(skf2(X0))
| ssPv2(X0)
| ssPv3(X0)
| ssPv3(skf2(X0)) ),
inference(factoring,[status(thm)],[p3648]) ).
cnf(p3711,plain,
( ssPv2(X0)
| ssPv3(X0)
| ssPv3(skf2(X0))
| ssPv2(skf2(X0))
| ssPv2(X0)
| ssPv3(X0)
| ssPv3(skf2(X0)) ),
inference(resolution,[status(thm)],[p3709,p3509]) ).
cnf(p4161,plain,
( ssPv2(X0)
| ssPv3(X0)
| ssPv2(skf2(X0))
| ssPv2(X0)
| ssPv3(X0)
| ssPv3(skf2(X0)) ),
inference(factoring,[status(thm)],[p3711]) ).
cnf(p4167,plain,
( ssPv2(X0)
| ssPv2(skf2(X0))
| ssPv2(X0)
| ssPv3(X0)
| ssPv3(skf2(X0)) ),
inference(factoring,[status(thm)],[p4161]) ).
cnf(p4169,plain,
( ssPv2(skf2(X0))
| ssPv2(X0)
| ssPv3(X0)
| ssPv3(skf2(X0)) ),
inference(factoring,[status(thm)],[p4167]) ).
cnf(p3515,plain,
( ssPv2(X0)
| ssPv3(X0)
| ~ ssPv2(skf2(X0))
| ssPv2(X0)
| ssPv3(X0)
| ssPv3(skf2(X0)) ),
inference(resolution,[status(thm)],[p3509,p155]) ).
cnf(p3562,plain,
( ssPv2(X0)
| ~ ssPv2(skf2(X0))
| ssPv2(X0)
| ssPv3(X0)
| ssPv3(skf2(X0)) ),
inference(factoring,[status(thm)],[p3515]) ).
cnf(p3564,plain,
( ~ ssPv2(skf2(X0))
| ssPv2(X0)
| ssPv3(X0)
| ssPv3(skf2(X0)) ),
inference(factoring,[status(thm)],[p3562]) ).
cnf(p4204,plain,
( ssPv2(X0)
| ssPv3(X0)
| ssPv3(skf2(X0))
| ssPv2(X0)
| ssPv3(X0)
| ssPv3(skf2(X0)) ),
inference(resolution,[status(thm)],[p4169,p3564]) ).
cnf(p4207,plain,
( ssPv2(X0)
| ssPv3(X0)
| ssPv2(X0)
| ssPv3(X0)
| ssPv3(skf2(X0)) ),
inference(factoring,[status(thm)],[p4204]) ).
cnf(p4210,plain,
( ssPv2(X0)
| ssPv2(X0)
| ssPv3(X0)
| ssPv3(skf2(X0)) ),
inference(factoring,[status(thm)],[p4207]) ).
cnf(p4212,plain,
( ssPv2(X0)
| ssPv3(X0)
| ssPv3(skf2(X0)) ),
inference(factoring,[status(thm)],[p4210]) ).
cnf(f21,negated_conjecture,
( ssPv3(U)
| ssPv1(W)
| ~ ssPv1(U)
| ~ ssRr(U,W)
| ~ ssPv3(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause22) ).
fof(f21_nnf,plain,
! [U,V,W] :
( ssPv3(U)
| ssPv1(W)
| ~ ssPv1(U)
| ~ ssRr(U,W)
| ~ ssPv3(V)
| ~ ssRr(U,V) ),
inference(nnf_transformation,[status(thm)],[f21]) ).
fof(f21_sk,plain,
! [U,V,W] :
( ssPv3(U)
| ssPv1(W)
| ~ ssPv1(U)
| ~ ssRr(U,W)
| ~ ssPv3(V)
| ~ ssRr(U,V) ),
inference(skolemisation,[status(esa)],[f21_nnf]) ).
cnf(c21,plain,
( ssPv3(X0)
| ssPv1(X2)
| ~ ssPv1(X0)
| ~ ssRr(X0,X2)
| ~ ssPv3(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f21_sk]) ).
cnf(p162,plain,
( ssPv3(X0)
| ssPv1(X1)
| ~ ssPv1(X0)
| ~ ssPv3(X1)
| ~ ssRr(X0,X1) ),
inference(factoring,[status(thm)],[c21]) ).
cnf(p167,plain,
( ssPv3(X0)
| ssPv1(skf2(X0))
| ~ ssPv1(X0)
| ~ ssPv3(skf2(X0)) ),
inference(resolution,[status(thm)],[p162,c1]) ).
cnf(p4216,plain,
( ssPv3(X0)
| ssPv1(skf2(X0))
| ~ ssPv1(X0)
| ssPv2(X0)
| ssPv3(X0) ),
inference(resolution,[status(thm)],[p4212,p167]) ).
cnf(p4249,plain,
( ssPv1(skf2(X0))
| ~ ssPv1(X0)
| ssPv2(X0)
| ssPv3(X0) ),
inference(factoring,[status(thm)],[p4216]) ).
cnf(p122,plain,
( ssPv4(X0)
| ssPv1(X0)
| ssPv4(X1)
| ~ ssRr(X1,X0)
| ~ ssPv3(skf3(X0)) ),
inference(resolution,[status(thm)],[c14,c0]) ).
cnf(p2447,plain,
( ssPv4(X0)
| ssPv1(X0)
| ssPv4(X1)
| ~ ssRr(X1,X0)
| ssPv4(X0)
| ssPv3(X0)
| ssPv2(X0)
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p2442,p122]) ).
cnf(p2621,plain,
( ssPv4(X0)
| ssPv4(X1)
| ~ ssRr(X1,X0)
| ssPv4(X0)
| ssPv3(X0)
| ssPv2(X0)
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p2447]) ).
cnf(p2623,plain,
( ssPv4(X1)
| ~ ssRr(X1,X0)
| ssPv4(X0)
| ssPv3(X0)
| ssPv2(X0)
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p2621]) ).
cnf(p2624,plain,
( ssPv4(X0)
| ssPv4(skf2(X0))
| ssPv3(skf2(X0))
| ssPv2(skf2(X0))
| ssPv1(skf2(X0)) ),
inference(resolution,[status(thm)],[p2623,c1]) ).
cnf(p2630,plain,
( ssPv4(skf2(X0))
| ssPv1(skf2(X0))
| ssPv2(X0)
| ssPv4(X0)
| ssPv4(skf2(X0))
| ssPv3(skf2(X0))
| ssPv1(skf2(X0)) ),
inference(resolution,[status(thm)],[p2624,p60]) ).
cnf(p2715,plain,
( ssPv4(skf2(X0))
| ssPv2(X0)
| ssPv4(X0)
| ssPv4(skf2(X0))
| ssPv3(skf2(X0))
| ssPv1(skf2(X0)) ),
inference(factoring,[status(thm)],[p2630]) ).
cnf(p2717,plain,
( ssPv2(X0)
| ssPv4(X0)
| ssPv4(skf2(X0))
| ssPv3(skf2(X0))
| ssPv1(skf2(X0)) ),
inference(factoring,[status(thm)],[p2715]) ).
cnf(p2720,plain,
( ssPv3(skf2(X0))
| ssPv1(skf2(X0))
| ssPv2(X0)
| ssPv2(X0)
| ssPv4(X0)
| ssPv3(skf2(X0))
| ssPv1(skf2(X0)) ),
inference(resolution,[status(thm)],[p2717,p62]) ).
cnf(p2756,plain,
( ssPv3(skf2(X0))
| ssPv2(X0)
| ssPv2(X0)
| ssPv4(X0)
| ssPv3(skf2(X0))
| ssPv1(skf2(X0)) ),
inference(factoring,[status(thm)],[p2720]) ).
cnf(p2761,plain,
( ssPv2(X0)
| ssPv2(X0)
| ssPv4(X0)
| ssPv3(skf2(X0))
| ssPv1(skf2(X0)) ),
inference(factoring,[status(thm)],[p2756]) ).
cnf(p2763,plain,
( ssPv2(X0)
| ssPv4(X0)
| ssPv3(skf2(X0))
| ssPv1(skf2(X0)) ),
inference(factoring,[status(thm)],[p2761]) ).
cnf(p4252,plain,
( ssPv2(X0)
| ssPv4(X0)
| ssPv3(skf2(X0))
| ssPv1(skf2(skf2(X0)))
| ssPv2(skf2(X0))
| ssPv3(skf2(X0)) ),
inference(resolution,[status(thm)],[p4249,p2763]) ).
cnf(p4470,plain,
( ssPv2(X0)
| ssPv4(X0)
| ssPv1(skf2(skf2(X0)))
| ssPv2(skf2(X0))
| ssPv3(skf2(X0)) ),
inference(factoring,[status(thm)],[p4252]) ).
cnf(f37,negated_conjecture,
( ssPv2(V)
| ssPv4(X)
| ssPv4(U)
| ~ ssRr(V,X)
| ~ ssPv1(W)
| ~ ssRr(V,W)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause38) ).
fof(f37_nnf,plain,
! [U,V,W,X] :
( ssPv2(V)
| ssPv4(X)
| ssPv4(U)
| ~ ssRr(V,X)
| ~ ssPv1(W)
| ~ ssRr(V,W)
| ~ ssRr(U,V) ),
inference(nnf_transformation,[status(thm)],[f37]) ).
fof(f37_sk,plain,
! [U,V,W,X] :
( ssPv2(V)
| ssPv4(X)
| ssPv4(U)
| ~ ssRr(V,X)
| ~ ssPv1(W)
| ~ ssRr(V,W)
| ~ ssRr(U,V) ),
inference(skolemisation,[status(esa)],[f37_nnf]) ).
cnf(c37,plain,
( ssPv2(X1)
| ssPv4(X3)
| ssPv4(X0)
| ~ ssRr(X1,X3)
| ~ ssPv1(X2)
| ~ ssRr(X1,X2)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f37_sk]) ).
cnf(p269,plain,
( ssPv2(X1)
| ssPv4(X2)
| ssPv4(X0)
| ~ ssPv1(X2)
| ~ ssRr(X1,X2)
| ~ ssRr(X0,X1) ),
inference(factoring,[status(thm)],[c37]) ).
cnf(p488,plain,
( ssPv2(skf2(X0))
| ssPv4(X1)
| ssPv4(X0)
| ~ ssPv1(X1)
| ~ ssRr(skf2(X0),X1) ),
inference(resolution,[status(thm)],[p269,c1]) ).
cnf(p513,plain,
( ssPv2(skf2(X0))
| ssPv4(skf2(skf2(X0)))
| ssPv4(X0)
| ~ ssPv1(skf2(skf2(X0))) ),
inference(resolution,[status(thm)],[p488,c1]) ).
cnf(p4495,plain,
( ssPv2(skf2(X0))
| ssPv4(skf2(skf2(X0)))
| ssPv4(X0)
| ssPv2(X0)
| ssPv4(X0)
| ssPv2(skf2(X0))
| ssPv3(skf2(X0)) ),
inference(resolution,[status(thm)],[p4470,p513]) ).
cnf(p5013,plain,
( ssPv4(skf2(skf2(X0)))
| ssPv4(X0)
| ssPv2(X0)
| ssPv4(X0)
| ssPv2(skf2(X0))
| ssPv3(skf2(X0)) ),
inference(factoring,[status(thm)],[p4495]) ).
cnf(p5015,plain,
( ssPv4(skf2(skf2(X0)))
| ssPv2(X0)
| ssPv4(X0)
| ssPv2(skf2(X0))
| ssPv3(skf2(X0)) ),
inference(factoring,[status(thm)],[p5013]) ).
cnf(p5023,plain,
( ssPv2(skf2(X0))
| ssPv2(X0)
| ~ ssPv1(skf2(X0))
| ssPv2(X0)
| ssPv4(X0)
| ssPv2(skf2(X0))
| ssPv3(skf2(X0)) ),
inference(resolution,[status(thm)],[p5015,p342]) ).
cnf(p5043,plain,
( ssPv2(X0)
| ~ ssPv1(skf2(X0))
| ssPv2(X0)
| ssPv4(X0)
| ssPv2(skf2(X0))
| ssPv3(skf2(X0)) ),
inference(factoring,[status(thm)],[p5023]) ).
cnf(p5045,plain,
( ~ ssPv1(skf2(X0))
| ssPv2(X0)
| ssPv4(X0)
| ssPv2(skf2(X0))
| ssPv3(skf2(X0)) ),
inference(factoring,[status(thm)],[p5043]) ).
cnf(p5046,plain,
( ssPv2(X0)
| ssPv4(X0)
| ssPv3(skf2(X0))
| ssPv2(X0)
| ssPv4(X0)
| ssPv2(skf2(X0))
| ssPv3(skf2(X0)) ),
inference(resolution,[status(thm)],[p5045,p2763]) ).
cnf(p5047,plain,
( ssPv2(X0)
| ssPv4(X0)
| ssPv2(X0)
| ssPv4(X0)
| ssPv2(skf2(X0))
| ssPv3(skf2(X0)) ),
inference(factoring,[status(thm)],[p5046]) ).
cnf(p5051,plain,
( ssPv2(X0)
| ssPv2(X0)
| ssPv4(X0)
| ssPv2(skf2(X0))
| ssPv3(skf2(X0)) ),
inference(factoring,[status(thm)],[p5047]) ).
cnf(p5053,plain,
( ssPv2(X0)
| ssPv4(X0)
| ssPv2(skf2(X0))
| ssPv3(skf2(X0)) ),
inference(factoring,[status(thm)],[p5051]) ).
cnf(f8,negated_conjecture,
( ssPv4(V)
| ssPv1(W)
| ssPv4(U)
| ~ ssPv1(V)
| ~ ssRr(W,V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause9) ).
fof(f8_nnf,plain,
! [U,V,W] :
( ssPv4(V)
| ssPv1(W)
| ssPv4(U)
| ~ ssPv1(V)
| ~ ssRr(W,V)
| ~ ssRr(U,V) ),
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [U,V,W] :
( ssPv4(V)
| ssPv1(W)
| ssPv4(U)
| ~ ssPv1(V)
| ~ ssRr(W,V)
| ~ ssRr(U,V) ),
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c8,plain,
( ssPv4(X1)
| ssPv1(X2)
| ssPv4(X0)
| ~ ssPv1(X1)
| ~ ssRr(X2,X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(p74,plain,
( ssPv4(X1)
| ssPv1(X0)
| ssPv4(X0)
| ~ ssPv1(X1)
| ~ ssRr(X0,X1) ),
inference(factoring,[status(thm)],[c8]) ).
cnf(p79,plain,
( ssPv4(skf2(X0))
| ssPv1(X0)
| ssPv4(X0)
| ~ ssPv1(skf2(X0)) ),
inference(resolution,[status(thm)],[p74,c1]) ).
cnf(p2766,plain,
( ssPv4(skf2(X0))
| ssPv1(X0)
| ssPv4(X0)
| ssPv2(X0)
| ssPv4(X0)
| ssPv3(skf2(X0)) ),
inference(resolution,[status(thm)],[p2763,p79]) ).
cnf(p2817,plain,
( ssPv4(skf2(X0))
| ssPv1(X0)
| ssPv2(X0)
| ssPv4(X0)
| ssPv3(skf2(X0)) ),
inference(factoring,[status(thm)],[p2766]) ).
cnf(p2824,plain,
( ssPv2(X0)
| ssPv1(X0)
| ~ ssPv2(skf2(X0))
| ssPv1(X0)
| ssPv2(X0)
| ssPv4(X0)
| ssPv3(skf2(X0)) ),
inference(resolution,[status(thm)],[p2817,p198]) ).
cnf(p3145,plain,
( ssPv1(X0)
| ~ ssPv2(skf2(X0))
| ssPv1(X0)
| ssPv2(X0)
| ssPv4(X0)
| ssPv3(skf2(X0)) ),
inference(factoring,[status(thm)],[p2824]) ).
cnf(p3147,plain,
( ~ ssPv2(skf2(X0))
| ssPv1(X0)
| ssPv2(X0)
| ssPv4(X0)
| ssPv3(skf2(X0)) ),
inference(factoring,[status(thm)],[p3145]) ).
cnf(p5088,plain,
( ssPv1(X0)
| ssPv2(X0)
| ssPv4(X0)
| ssPv3(skf2(X0))
| ssPv2(X0)
| ssPv4(X0)
| ssPv3(skf2(X0)) ),
inference(resolution,[status(thm)],[p5053,p3147]) ).
cnf(p5099,plain,
( ssPv1(X0)
| ssPv2(X0)
| ssPv4(X0)
| ssPv2(X0)
| ssPv4(X0)
| ssPv3(skf2(X0)) ),
inference(factoring,[status(thm)],[p5088]) ).
cnf(p5103,plain,
( ssPv1(X0)
| ssPv2(X0)
| ssPv2(X0)
| ssPv4(X0)
| ssPv3(skf2(X0)) ),
inference(factoring,[status(thm)],[p5099]) ).
cnf(p5105,plain,
( ssPv1(X0)
| ssPv2(X0)
| ssPv4(X0)
| ssPv3(skf2(X0)) ),
inference(factoring,[status(thm)],[p5103]) ).
cnf(f23,negated_conjecture,
( ssPv2(V)
| ssPv2(U)
| ~ ssPv3(V)
| ~ ssPv2(W)
| ~ ssRr(V,W)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause24) ).
fof(f23_nnf,plain,
! [U,V,W] :
( ssPv2(V)
| ssPv2(U)
| ~ ssPv3(V)
| ~ ssPv2(W)
| ~ ssRr(V,W)
| ~ ssRr(U,V) ),
inference(nnf_transformation,[status(thm)],[f23]) ).
fof(f23_sk,plain,
! [U,V,W] :
( ssPv2(V)
| ssPv2(U)
| ~ ssPv3(V)
| ~ ssPv2(W)
| ~ ssRr(V,W)
| ~ ssRr(U,V) ),
inference(skolemisation,[status(esa)],[f23_nnf]) ).
cnf(c23,plain,
( ssPv2(X1)
| ssPv2(X0)
| ~ ssPv3(X1)
| ~ ssPv2(X2)
| ~ ssRr(X1,X2)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f23_sk]) ).
cnf(p176,plain,
( ssPv2(skf2(X0))
| ssPv2(X0)
| ~ ssPv3(skf2(X0))
| ~ ssPv2(X1)
| ~ ssRr(skf2(X0),X1) ),
inference(resolution,[status(thm)],[c23,c1]) ).
cnf(p339,plain,
( ssPv2(skf2(X0))
| ssPv2(X0)
| ~ ssPv3(skf2(X0))
| ~ ssPv2(skf2(skf2(X0))) ),
inference(resolution,[status(thm)],[p176,c1]) ).
cnf(p70,plain,
( ssPv2(skf2(X0))
| ssPv1(skf2(X0))
| ssPv2(X1)
| ssPv4(X0)
| ~ ssRr(skf2(X0),X1) ),
inference(resolution,[status(thm)],[c7,c1]) ).
cnf(p278,plain,
( ssPv2(skf2(X0))
| ssPv1(skf2(X0))
| ssPv2(skf2(skf2(X0)))
| ssPv4(X0) ),
inference(resolution,[status(thm)],[p70,c1]) ).
cnf(p341,plain,
( ssPv2(skf2(X0))
| ssPv1(skf2(X0))
| ssPv4(X0)
| ssPv2(skf2(X0))
| ssPv2(X0)
| ~ ssPv3(skf2(X0)) ),
inference(resolution,[status(thm)],[p339,p278]) ).
cnf(p1196,plain,
( ssPv1(skf2(X0))
| ssPv4(X0)
| ssPv2(skf2(X0))
| ssPv2(X0)
| ~ ssPv3(skf2(X0)) ),
inference(factoring,[status(thm)],[p341]) ).
cnf(p5132,plain,
( ssPv1(skf2(X0))
| ssPv4(X0)
| ssPv2(skf2(X0))
| ssPv2(X0)
| ssPv1(X0)
| ssPv2(X0)
| ssPv4(X0) ),
inference(resolution,[status(thm)],[p5105,p1196]) ).
cnf(p5214,plain,
( ssPv1(skf2(X0))
| ssPv2(skf2(X0))
| ssPv2(X0)
| ssPv1(X0)
| ssPv2(X0)
| ssPv4(X0) ),
inference(factoring,[status(thm)],[p5132]) ).
cnf(p5216,plain,
( ssPv1(skf2(X0))
| ssPv2(skf2(X0))
| ssPv1(X0)
| ssPv2(X0)
| ssPv4(X0) ),
inference(factoring,[status(thm)],[p5214]) ).
cnf(p5220,plain,
( ssPv4(skf2(X0))
| ssPv1(skf2(X0))
| ssPv2(X0)
| ssPv1(skf2(X0))
| ssPv1(X0)
| ssPv2(X0)
| ssPv4(X0) ),
inference(resolution,[status(thm)],[p5216,p60]) ).
cnf(p5323,plain,
( ssPv4(skf2(X0))
| ssPv2(X0)
| ssPv1(skf2(X0))
| ssPv1(X0)
| ssPv2(X0)
| ssPv4(X0) ),
inference(factoring,[status(thm)],[p5220]) ).
cnf(p5324,plain,
( ssPv4(skf2(X0))
| ssPv1(skf2(X0))
| ssPv1(X0)
| ssPv2(X0)
| ssPv4(X0) ),
inference(factoring,[status(thm)],[p5323]) ).
cnf(p5331,plain,
( ssPv2(X0)
| ssPv1(X0)
| ~ ssPv2(skf2(X0))
| ssPv1(skf2(X0))
| ssPv1(X0)
| ssPv2(X0)
| ssPv4(X0) ),
inference(resolution,[status(thm)],[p5324,p198]) ).
cnf(p5347,plain,
( ssPv1(X0)
| ~ ssPv2(skf2(X0))
| ssPv1(skf2(X0))
| ssPv1(X0)
| ssPv2(X0)
| ssPv4(X0) ),
inference(factoring,[status(thm)],[p5331]) ).
cnf(p5349,plain,
( ~ ssPv2(skf2(X0))
| ssPv1(skf2(X0))
| ssPv1(X0)
| ssPv2(X0)
| ssPv4(X0) ),
inference(factoring,[status(thm)],[p5347]) ).
cnf(f10,negated_conjecture,
( ssPv4(U)
| ssPv3(U)
| ssPv2(W)
| ~ ssRr(U,W)
| ~ ssPv1(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause11) ).
fof(f10_nnf,plain,
! [U,V,W] :
( ssPv4(U)
| ssPv3(U)
| ssPv2(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)
| ssPv2(W)
| ~ ssRr(U,W)
| ~ ssPv1(V)
| ~ ssRr(U,V) ),
inference(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c10,plain,
( ssPv4(X0)
| ssPv3(X0)
| ssPv2(X2)
| ~ ssRr(X0,X2)
| ~ ssPv1(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(p95,plain,
( ssPv4(X0)
| ssPv3(X0)
| ssPv2(X1)
| ~ ssPv1(X1)
| ~ ssRr(X0,X1) ),
inference(factoring,[status(thm)],[c10]) ).
cnf(p101,plain,
( ssPv4(X0)
| ssPv3(X0)
| ssPv2(skf2(X0))
| ~ ssPv1(skf2(X0)) ),
inference(resolution,[status(thm)],[p95,c1]) ).
cnf(p2768,plain,
( ssPv4(X0)
| ssPv3(X0)
| ssPv2(skf2(X0))
| ssPv2(X0)
| ssPv4(X0)
| ssPv3(skf2(X0)) ),
inference(resolution,[status(thm)],[p2763,p101]) ).
cnf(p2844,plain,
( ssPv3(X0)
| ssPv2(skf2(X0))
| ssPv2(X0)
| ssPv4(X0)
| ssPv3(skf2(X0)) ),
inference(factoring,[status(thm)],[p2768]) ).
cnf(p3570,plain,
( ssPv3(X0)
| ssPv2(X0)
| ssPv4(X0)
| ssPv3(skf2(X0))
| ssPv2(X0)
| ssPv3(X0)
| ssPv3(skf2(X0)) ),
inference(resolution,[status(thm)],[p3564,p2844]) ).
cnf(p3776,plain,
( ssPv3(X0)
| ssPv2(X0)
| ssPv4(X0)
| ssPv2(X0)
| ssPv3(X0)
| ssPv3(skf2(X0)) ),
inference(factoring,[status(thm)],[p3570]) ).
cnf(p3779,plain,
( ssPv2(X0)
| ssPv4(X0)
| ssPv2(X0)
| ssPv3(X0)
| ssPv3(skf2(X0)) ),
inference(factoring,[status(thm)],[p3776]) ).
cnf(p3781,plain,
( ssPv4(X0)
| ssPv2(X0)
| ssPv3(X0)
| ssPv3(skf2(X0)) ),
inference(factoring,[status(thm)],[p3779]) ).
cnf(p3807,plain,
( ssPv1(skf2(X0))
| ssPv4(X0)
| ssPv2(skf2(X0))
| ssPv2(X0)
| ssPv4(X0)
| ssPv2(X0)
| ssPv3(X0) ),
inference(resolution,[status(thm)],[p3781,p1196]) ).
cnf(p3907,plain,
( ssPv1(skf2(X0))
| ssPv4(X0)
| ssPv2(skf2(X0))
| ssPv4(X0)
| ssPv2(X0)
| ssPv3(X0) ),
inference(factoring,[status(thm)],[p3807]) ).
cnf(p3909,plain,
( ssPv1(skf2(X0))
| ssPv2(skf2(X0))
| ssPv4(X0)
| ssPv2(X0)
| ssPv3(X0) ),
inference(factoring,[status(thm)],[p3907]) ).
cnf(p5355,plain,
( ssPv1(skf2(X0))
| ssPv4(X0)
| ssPv2(X0)
| ssPv3(X0)
| ssPv1(skf2(X0))
| ssPv1(X0)
| ssPv2(X0)
| ssPv4(X0) ),
inference(resolution,[status(thm)],[p5349,p3909]) ).
cnf(p5581,plain,
( ssPv4(X0)
| ssPv2(X0)
| ssPv3(X0)
| ssPv1(skf2(X0))
| ssPv1(X0)
| ssPv2(X0)
| ssPv4(X0) ),
inference(factoring,[status(thm)],[p5355]) ).
cnf(p5582,plain,
( ssPv2(X0)
| ssPv3(X0)
| ssPv1(skf2(X0))
| ssPv1(X0)
| ssPv2(X0)
| ssPv4(X0) ),
inference(factoring,[status(thm)],[p5581]) ).
cnf(p5586,plain,
( ssPv3(X0)
| ssPv1(skf2(X0))
| ssPv1(X0)
| ssPv2(X0)
| ssPv4(X0) ),
inference(factoring,[status(thm)],[p5582]) ).
cnf(p5596,plain,
( ssPv2(X0)
| ssPv3(X0)
| ~ ssPv2(skf2(X0))
| ssPv3(X0)
| ssPv1(X0)
| ssPv2(X0)
| ssPv4(X0) ),
inference(resolution,[status(thm)],[p5586,p155]) ).
cnf(p5697,plain,
( ssPv3(X0)
| ~ ssPv2(skf2(X0))
| ssPv3(X0)
| ssPv1(X0)
| ssPv2(X0)
| ssPv4(X0) ),
inference(factoring,[status(thm)],[p5596]) ).
cnf(p5699,plain,
( ~ ssPv2(skf2(X0))
| ssPv3(X0)
| ssPv1(X0)
| ssPv2(X0)
| ssPv4(X0) ),
inference(factoring,[status(thm)],[p5697]) ).
cnf(p5591,plain,
( ssPv4(X0)
| ssPv3(X0)
| ssPv2(skf2(X0))
| ssPv3(X0)
| ssPv1(X0)
| ssPv2(X0)
| ssPv4(X0) ),
inference(resolution,[status(thm)],[p5586,p101]) ).
cnf(p5663,plain,
( ssPv3(X0)
| ssPv2(skf2(X0))
| ssPv3(X0)
| ssPv1(X0)
| ssPv2(X0)
| ssPv4(X0) ),
inference(factoring,[status(thm)],[p5591]) ).
cnf(p5665,plain,
( ssPv2(skf2(X0))
| ssPv3(X0)
| ssPv1(X0)
| ssPv2(X0)
| ssPv4(X0) ),
inference(factoring,[status(thm)],[p5663]) ).
cnf(p5703,plain,
( ssPv3(X0)
| ssPv1(X0)
| ssPv2(X0)
| ssPv4(X0)
| ssPv3(X0)
| ssPv1(X0)
| ssPv2(X0)
| ssPv4(X0) ),
inference(resolution,[status(thm)],[p5699,p5665]) ).
cnf(p5793,plain,
( ssPv3(X0)
| ssPv1(X0)
| ssPv2(X0)
| ssPv3(X0)
| ssPv1(X0)
| ssPv2(X0)
| ssPv4(X0) ),
inference(factoring,[status(thm)],[p5703]) ).
cnf(p5797,plain,
( ssPv3(X0)
| ssPv1(X0)
| ssPv3(X0)
| ssPv1(X0)
| ssPv2(X0)
| ssPv4(X0) ),
inference(factoring,[status(thm)],[p5793]) ).
cnf(p5800,plain,
( ssPv3(X0)
| ssPv3(X0)
| ssPv1(X0)
| ssPv2(X0)
| ssPv4(X0) ),
inference(factoring,[status(thm)],[p5797]) ).
cnf(p5802,plain,
( ssPv3(X0)
| ssPv1(X0)
| ssPv2(X0)
| ssPv4(X0) ),
inference(factoring,[status(thm)],[p5800]) ).
cnf(p59,plain,
( ssPv4(X0)
| ssPv1(X0)
| ssPv2(skf3(X0))
| ~ ssPv2(X0) ),
inference(resolution,[status(thm)],[c4,c0]) ).
cnf(p5803,plain,
( ssPv4(X0)
| ssPv1(X0)
| ssPv2(skf3(X0))
| ssPv3(X0)
| ssPv1(X0)
| ssPv4(X0) ),
inference(resolution,[status(thm)],[p5802,p59]) ).
cnf(p5855,plain,
( ssPv1(X0)
| ssPv2(skf3(X0))
| ssPv3(X0)
| ssPv1(X0)
| ssPv4(X0) ),
inference(factoring,[status(thm)],[p5803]) ).
cnf(p5857,plain,
( ssPv2(skf3(X0))
| ssPv3(X0)
| ssPv1(X0)
| ssPv4(X0) ),
inference(factoring,[status(thm)],[p5855]) ).
cnf(f16,negated_conjecture,
( ssPv3(V)
| ssPv1(V)
| ssPv2(W)
| ~ ssRr(V,W)
| ~ ssPv2(U)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause17) ).
fof(f16_nnf,plain,
! [U,V,W] :
( ssPv3(V)
| ssPv1(V)
| ssPv2(W)
| ~ ssRr(V,W)
| ~ ssPv2(U)
| ~ ssRr(U,V) ),
inference(nnf_transformation,[status(thm)],[f16]) ).
fof(f16_sk,plain,
! [U,V,W] :
( ssPv3(V)
| ssPv1(V)
| ssPv2(W)
| ~ ssRr(V,W)
| ~ ssPv2(U)
| ~ ssRr(U,V) ),
inference(skolemisation,[status(esa)],[f16_nnf]) ).
cnf(c16,plain,
( ssPv3(X1)
| ssPv1(X1)
| ssPv2(X2)
| ~ ssRr(X1,X2)
| ~ ssPv2(X0)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(p134,plain,
( ssPv3(X0)
| ssPv1(X0)
| ssPv2(X1)
| ~ ssRr(X0,X1)
| ~ ssPv2(skf3(X0)) ),
inference(resolution,[status(thm)],[c16,c0]) ).
cnf(p5862,plain,
( ssPv3(X0)
| ssPv1(X0)
| ssPv2(X1)
| ~ ssRr(X0,X1)
| ssPv3(X0)
| ssPv1(X0)
| ssPv4(X0) ),
inference(resolution,[status(thm)],[p5857,p134]) ).
cnf(p6013,plain,
( ssPv3(X0)
| ssPv2(X1)
| ~ ssRr(X0,X1)
| ssPv3(X0)
| ssPv1(X0)
| ssPv4(X0) ),
inference(factoring,[status(thm)],[p5862]) ).
cnf(p6015,plain,
( ssPv2(X1)
| ~ ssRr(X0,X1)
| ssPv3(X0)
| ssPv1(X0)
| ssPv4(X0) ),
inference(factoring,[status(thm)],[p6013]) ).
cnf(p6017,plain,
( ssPv2(skf2(X0))
| ssPv3(X0)
| ssPv1(X0)
| ssPv4(X0) ),
inference(resolution,[status(thm)],[p6015,c1]) ).
cnf(f13,negated_conjecture,
( ssPv1(V)
| ssPv4(W)
| ssPv1(U)
| ~ ssPv2(V)
| ~ ssRr(V,W)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause14) ).
fof(f13_nnf,plain,
! [U,V,W] :
( ssPv1(V)
| ssPv4(W)
| ssPv1(U)
| ~ ssPv2(V)
| ~ ssRr(V,W)
| ~ ssRr(U,V) ),
inference(nnf_transformation,[status(thm)],[f13]) ).
fof(f13_sk,plain,
! [U,V,W] :
( ssPv1(V)
| ssPv4(W)
| ssPv1(U)
| ~ ssPv2(V)
| ~ ssRr(V,W)
| ~ ssRr(U,V) ),
inference(skolemisation,[status(esa)],[f13_nnf]) ).
cnf(c13,plain,
( ssPv1(X1)
| ssPv4(X2)
| ssPv1(X0)
| ~ ssPv2(X1)
| ~ ssRr(X1,X2)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(p116,plain,
( ssPv1(skf2(X0))
| ssPv4(X1)
| ssPv1(X0)
| ~ ssPv2(skf2(X0))
| ~ ssRr(skf2(X0),X1) ),
inference(resolution,[status(thm)],[c13,c1]) ).
cnf(p306,plain,
( ssPv1(skf2(X0))
| ssPv4(skf2(skf2(X0)))
| ssPv1(X0)
| ~ ssPv2(skf2(X0)) ),
inference(resolution,[status(thm)],[p116,c1]) ).
cnf(p6027,plain,
( ssPv1(skf2(X0))
| ssPv4(skf2(skf2(X0)))
| ssPv1(X0)
| ssPv3(X0)
| ssPv1(X0)
| ssPv4(X0) ),
inference(resolution,[status(thm)],[p6017,p306]) ).
cnf(p6088,plain,
( ssPv1(skf2(X0))
| ssPv4(skf2(skf2(X0)))
| ssPv3(X0)
| ssPv1(X0)
| ssPv4(X0) ),
inference(factoring,[status(thm)],[p6027]) ).
cnf(f26,negated_conjecture,
( ssPv1(V)
| ssPv1(U)
| ~ ssPv2(V)
| ~ ssPv4(W)
| ~ ssRr(V,W)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause27) ).
fof(f26_nnf,plain,
! [U,V,W] :
( ssPv1(V)
| ssPv1(U)
| ~ ssPv2(V)
| ~ ssPv4(W)
| ~ ssRr(V,W)
| ~ ssRr(U,V) ),
inference(nnf_transformation,[status(thm)],[f26]) ).
fof(f26_sk,plain,
! [U,V,W] :
( ssPv1(V)
| ssPv1(U)
| ~ ssPv2(V)
| ~ ssPv4(W)
| ~ ssRr(V,W)
| ~ ssRr(U,V) ),
inference(skolemisation,[status(esa)],[f26_nnf]) ).
cnf(c26,plain,
( ssPv1(X1)
| ssPv1(X0)
| ~ ssPv2(X1)
| ~ ssPv4(X2)
| ~ ssRr(X1,X2)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f26_sk]) ).
cnf(p191,plain,
( ssPv1(skf2(X0))
| ssPv1(X0)
| ~ ssPv2(skf2(X0))
| ~ ssPv4(X1)
| ~ ssRr(skf2(X0),X1) ),
inference(resolution,[status(thm)],[c26,c1]) ).
cnf(p350,plain,
( ssPv1(skf2(X0))
| ssPv1(X0)
| ~ ssPv2(skf2(X0))
| ~ ssPv4(skf2(skf2(X0))) ),
inference(resolution,[status(thm)],[p191,c1]) ).
cnf(p6099,plain,
( ssPv1(skf2(X0))
| ssPv1(X0)
| ~ ssPv2(skf2(X0))
| ssPv1(skf2(X0))
| ssPv3(X0)
| ssPv1(X0)
| ssPv4(X0) ),
inference(resolution,[status(thm)],[p6088,p350]) ).
cnf(p7663,plain,
( ssPv1(X0)
| ~ ssPv2(skf2(X0))
| ssPv1(skf2(X0))
| ssPv3(X0)
| ssPv1(X0)
| ssPv4(X0) ),
inference(factoring,[status(thm)],[p6099]) ).
cnf(p7664,plain,
( ~ ssPv2(skf2(X0))
| ssPv1(skf2(X0))
| ssPv3(X0)
| ssPv1(X0)
| ssPv4(X0) ),
inference(factoring,[status(thm)],[p7663]) ).
cnf(p7667,plain,
( ssPv3(X0)
| ssPv1(X0)
| ssPv4(X0)
| ssPv1(skf2(X0))
| ssPv3(X0)
| ssPv1(X0)
| ssPv4(X0) ),
inference(resolution,[status(thm)],[p7664,p6017]) ).
cnf(p7670,plain,
( ssPv3(X0)
| ssPv1(X0)
| ssPv1(skf2(X0))
| ssPv3(X0)
| ssPv1(X0)
| ssPv4(X0) ),
inference(factoring,[status(thm)],[p7667]) ).
cnf(p7673,plain,
( ssPv3(X0)
| ssPv1(skf2(X0))
| ssPv3(X0)
| ssPv1(X0)
| ssPv4(X0) ),
inference(factoring,[status(thm)],[p7670]) ).
cnf(p7675,plain,
( ssPv1(skf2(X0))
| ssPv3(X0)
| ssPv1(X0)
| ssPv4(X0) ),
inference(factoring,[status(thm)],[p7673]) ).
cnf(f43,negated_conjecture,
( ssPv3(W)
| ~ ssPv2(V)
| ~ ssPv1(X)
| ~ ssRr(V,X)
| ~ ssRr(W,V)
| ~ ssPv2(U)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause44) ).
fof(f43_nnf,plain,
! [U,V,W,X] :
( ssPv3(W)
| ~ ssPv2(V)
| ~ ssPv1(X)
| ~ ssRr(V,X)
| ~ ssRr(W,V)
| ~ ssPv2(U)
| ~ ssRr(U,V) ),
inference(nnf_transformation,[status(thm)],[f43]) ).
fof(f43_sk,plain,
! [U,V,W,X] :
( ssPv3(W)
| ~ ssPv2(V)
| ~ ssPv1(X)
| ~ ssRr(V,X)
| ~ ssRr(W,V)
| ~ ssPv2(U)
| ~ ssRr(U,V) ),
inference(skolemisation,[status(esa)],[f43_nnf]) ).
cnf(c43,plain,
( ssPv3(X2)
| ~ ssPv2(X1)
| ~ ssPv1(X3)
| ~ ssRr(X1,X3)
| ~ ssRr(X2,X1)
| ~ ssPv2(X0)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f43_sk]) ).
cnf(p324,plain,
( ssPv3(X0)
| ~ ssPv2(X1)
| ~ ssPv1(X2)
| ~ ssRr(X1,X2)
| ~ ssPv2(X0)
| ~ ssRr(X0,X1) ),
inference(factoring,[status(thm)],[c43]) ).
cnf(p647,plain,
( ssPv3(skf3(X0))
| ~ ssPv2(X0)
| ~ ssPv1(X1)
| ~ ssRr(X0,X1)
| ~ ssPv2(skf3(X0)) ),
inference(resolution,[status(thm)],[p324,c0]) ).
cnf(p5880,plain,
( ssPv3(skf3(X0))
| ~ ssPv2(X0)
| ~ ssPv1(X1)
| ~ ssRr(X0,X1)
| ssPv3(X0)
| ssPv1(X0)
| ssPv4(X0) ),
inference(resolution,[status(thm)],[p5857,p647]) ).
cnf(p6971,plain,
( ssPv3(skf3(X0))
| ~ ssPv2(X0)
| ~ ssPv1(skf2(X0))
| ssPv3(X0)
| ssPv1(X0)
| ssPv4(X0) ),
inference(resolution,[status(thm)],[p5880,c1]) ).
cnf(p7709,plain,
( ssPv3(skf3(X0))
| ~ ssPv2(X0)
| ssPv3(X0)
| ssPv1(X0)
| ssPv4(X0)
| ssPv3(X0)
| ssPv1(X0)
| ssPv4(X0) ),
inference(resolution,[status(thm)],[p7675,p6971]) ).
cnf(p9138,plain,
( ssPv3(skf3(X0))
| ~ ssPv2(X0)
| ssPv3(X0)
| ssPv1(X0)
| ssPv3(X0)
| ssPv1(X0)
| ssPv4(X0) ),
inference(factoring,[status(thm)],[p7709]) ).
cnf(p9144,plain,
( ssPv3(skf3(X0))
| ~ ssPv2(X0)
| ssPv3(X0)
| ssPv3(X0)
| ssPv1(X0)
| ssPv4(X0) ),
inference(factoring,[status(thm)],[p9138]) ).
cnf(p9146,plain,
( ssPv3(skf3(X0))
| ~ ssPv2(X0)
| ssPv3(X0)
| ssPv1(X0)
| ssPv4(X0) ),
inference(factoring,[status(thm)],[p9144]) ).
cnf(p9150,plain,
( ssPv3(X0)
| ssPv1(X0)
| ssPv4(X0)
| ssPv3(skf3(X0))
| ssPv3(X0)
| ssPv1(X0)
| ssPv4(X0) ),
inference(resolution,[status(thm)],[p9146,p5802]) ).
cnf(p9155,plain,
( ssPv3(X0)
| ssPv1(X0)
| ssPv3(skf3(X0))
| ssPv3(X0)
| ssPv1(X0)
| ssPv4(X0) ),
inference(factoring,[status(thm)],[p9150]) ).
cnf(p9160,plain,
( ssPv3(X0)
| ssPv3(skf3(X0))
| ssPv3(X0)
| ssPv1(X0)
| ssPv4(X0) ),
inference(factoring,[status(thm)],[p9155]) ).
cnf(p9162,plain,
( ssPv3(skf3(X0))
| ssPv3(X0)
| ssPv1(X0)
| ssPv4(X0) ),
inference(factoring,[status(thm)],[p9160]) ).
cnf(p115,plain,
( ssPv1(X0)
| ssPv4(X1)
| ssPv1(skf3(X0))
| ~ ssPv2(X0)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[c13,c0]) ).
cnf(p139,plain,
( ssPv1(X0)
| ssPv4(skf2(X0))
| ssPv1(skf3(X0))
| ~ ssPv2(X0) ),
inference(resolution,[status(thm)],[p115,c1]) ).
cnf(p5805,plain,
( ssPv1(X0)
| ssPv4(skf2(X0))
| ssPv1(skf3(X0))
| ssPv3(X0)
| ssPv1(X0)
| ssPv4(X0) ),
inference(resolution,[status(thm)],[p5802,p139]) ).
cnf(p5898,plain,
( ssPv4(skf2(X0))
| ssPv1(skf3(X0))
| ssPv3(X0)
| ssPv1(X0)
| ssPv4(X0) ),
inference(factoring,[status(thm)],[p5805]) ).
cnf(p190,plain,
( ssPv1(X0)
| ssPv1(skf3(X0))
| ~ ssPv2(X0)
| ~ ssPv4(X1)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[c26,c0]) ).
cnf(p215,plain,
( ssPv1(X0)
| ssPv1(skf3(X0))
| ~ ssPv2(X0)
| ~ ssPv4(skf2(X0)) ),
inference(resolution,[status(thm)],[p190,c1]) ).
cnf(p5902,plain,
( ssPv1(X0)
| ssPv1(skf3(X0))
| ~ ssPv2(X0)
| ssPv1(skf3(X0))
| ssPv3(X0)
| ssPv1(X0)
| ssPv4(X0) ),
inference(resolution,[status(thm)],[p5898,p215]) ).
cnf(p6973,plain,
( ssPv1(X0)
| ~ ssPv2(X0)
| ssPv1(skf3(X0))
| ssPv3(X0)
| ssPv1(X0)
| ssPv4(X0) ),
inference(factoring,[status(thm)],[p5902]) ).
cnf(p6976,plain,
( ~ ssPv2(X0)
| ssPv1(skf3(X0))
| ssPv3(X0)
| ssPv1(X0)
| ssPv4(X0) ),
inference(factoring,[status(thm)],[p6973]) ).
cnf(p6985,plain,
( ssPv3(X0)
| ssPv1(X0)
| ssPv4(X0)
| ssPv1(skf3(X0))
| ssPv3(X0)
| ssPv1(X0)
| ssPv4(X0) ),
inference(resolution,[status(thm)],[p6976,p5802]) ).
cnf(p6987,plain,
( ssPv3(X0)
| ssPv1(X0)
| ssPv1(skf3(X0))
| ssPv3(X0)
| ssPv1(X0)
| ssPv4(X0) ),
inference(factoring,[status(thm)],[p6985]) ).
cnf(p6990,plain,
( ssPv3(X0)
| ssPv1(skf3(X0))
| ssPv3(X0)
| ssPv1(X0)
| ssPv4(X0) ),
inference(factoring,[status(thm)],[p6987]) ).
cnf(p6993,plain,
( ssPv1(skf3(X0))
| ssPv3(X0)
| ssPv1(X0)
| ssPv4(X0) ),
inference(factoring,[status(thm)],[p6990]) ).
cnf(f31,negated_conjecture,
( ssPv1(W)
| ~ ssPv3(U)
| ~ ssPv1(U)
| ~ ssRr(U,W)
| ~ ssPv2(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause32) ).
fof(f31_nnf,plain,
! [U,V,W] :
( ssPv1(W)
| ~ ssPv3(U)
| ~ ssPv1(U)
| ~ ssRr(U,W)
| ~ ssPv2(V)
| ~ ssRr(U,V) ),
inference(nnf_transformation,[status(thm)],[f31]) ).
fof(f31_sk,plain,
! [U,V,W] :
( ssPv1(W)
| ~ ssPv3(U)
| ~ ssPv1(U)
| ~ ssRr(U,W)
| ~ ssPv2(V)
| ~ ssRr(U,V) ),
inference(skolemisation,[status(esa)],[f31_nnf]) ).
cnf(c31,plain,
( ssPv1(X2)
| ~ ssPv3(X0)
| ~ ssPv1(X0)
| ~ ssRr(X0,X2)
| ~ ssPv2(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f31_sk]) ).
cnf(p223,plain,
( ssPv1(X1)
| ~ ssPv3(X0)
| ~ ssPv1(X0)
| ~ ssPv2(X1)
| ~ ssRr(X0,X1) ),
inference(factoring,[status(thm)],[c31]) ).
cnf(p226,plain,
( ssPv1(X0)
| ~ ssPv3(skf3(X0))
| ~ ssPv1(skf3(X0))
| ~ ssPv2(X0) ),
inference(resolution,[status(thm)],[p223,c0]) ).
cnf(p5809,plain,
( ssPv1(X0)
| ~ ssPv3(skf3(X0))
| ~ ssPv1(skf3(X0))
| ssPv3(X0)
| ssPv1(X0)
| ssPv4(X0) ),
inference(resolution,[status(thm)],[p5802,p226]) ).
cnf(p5925,plain,
( ~ ssPv3(skf3(X0))
| ~ ssPv1(skf3(X0))
| ssPv3(X0)
| ssPv1(X0)
| ssPv4(X0) ),
inference(factoring,[status(thm)],[p5809]) ).
cnf(p7024,plain,
( ~ ssPv3(skf3(X0))
| ssPv3(X0)
| ssPv1(X0)
| ssPv4(X0)
| ssPv3(X0)
| ssPv1(X0)
| ssPv4(X0) ),
inference(resolution,[status(thm)],[p6993,p5925]) ).
cnf(p7078,plain,
( ~ ssPv3(skf3(X0))
| ssPv3(X0)
| ssPv1(X0)
| ssPv3(X0)
| ssPv1(X0)
| ssPv4(X0) ),
inference(factoring,[status(thm)],[p7024]) ).
cnf(p7119,plain,
( ~ ssPv3(skf3(X0))
| ssPv3(X0)
| ssPv3(X0)
| ssPv1(X0)
| ssPv4(X0) ),
inference(factoring,[status(thm)],[p7078]) ).
cnf(p7121,plain,
( ~ ssPv3(skf3(X0))
| ssPv3(X0)
| ssPv1(X0)
| ssPv4(X0) ),
inference(factoring,[status(thm)],[p7119]) ).
cnf(p9185,plain,
( ssPv3(X0)
| ssPv1(X0)
| ssPv4(X0)
| ssPv3(X0)
| ssPv1(X0)
| ssPv4(X0) ),
inference(resolution,[status(thm)],[p9162,p7121]) ).
cnf(p9190,plain,
( ssPv3(X0)
| ssPv1(X0)
| ssPv3(X0)
| ssPv1(X0)
| ssPv4(X0) ),
inference(factoring,[status(thm)],[p9185]) ).
cnf(p9194,plain,
( ssPv3(X0)
| ssPv3(X0)
| ssPv1(X0)
| ssPv4(X0) ),
inference(factoring,[status(thm)],[p9190]) ).
cnf(p9196,plain,
( ssPv3(X0)
| ssPv1(X0)
| ssPv4(X0) ),
inference(factoring,[status(thm)],[p9194]) ).
cnf(p61,plain,
( ssPv3(X0)
| ssPv1(X0)
| ssPv2(skf3(X0))
| ~ ssPv4(X0) ),
inference(resolution,[status(thm)],[c5,c0]) ).
cnf(p9199,plain,
( ssPv3(X0)
| ssPv1(X0)
| ssPv2(skf3(X0))
| ssPv3(X0)
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p9196,p61]) ).
cnf(p9294,plain,
( ssPv3(X0)
| ssPv2(skf3(X0))
| ssPv3(X0)
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p9199]) ).
cnf(p9296,plain,
( ssPv2(skf3(X0))
| ssPv3(X0)
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p9294]) ).
cnf(p9302,plain,
( ssPv3(X0)
| ssPv1(X0)
| ssPv2(X1)
| ~ ssRr(X0,X1)
| ssPv3(X0)
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p9296,p134]) ).
cnf(p9704,plain,
( ssPv3(X0)
| ssPv2(X1)
| ~ ssRr(X0,X1)
| ssPv3(X0)
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p9302]) ).
cnf(p9706,plain,
( ssPv2(X1)
| ~ ssRr(X0,X1)
| ssPv3(X0)
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p9704]) ).
cnf(p9708,plain,
( ssPv2(skf2(X0))
| ssPv3(X0)
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p9706,c1]) ).
cnf(p9718,plain,
( ssPv1(skf2(X0))
| ssPv4(skf2(skf2(X0)))
| ssPv1(X0)
| ssPv3(X0)
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p9708,p306]) ).
cnf(p9796,plain,
( ssPv1(skf2(X0))
| ssPv4(skf2(skf2(X0)))
| ssPv3(X0)
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p9718]) ).
cnf(p9807,plain,
( ssPv1(skf2(X0))
| ssPv1(X0)
| ~ ssPv2(skf2(X0))
| ssPv1(skf2(X0))
| ssPv3(X0)
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p9796,p350]) ).
cnf(p10481,plain,
( ssPv1(X0)
| ~ ssPv2(skf2(X0))
| ssPv1(skf2(X0))
| ssPv3(X0)
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p9807]) ).
cnf(p10485,plain,
( ~ ssPv2(skf2(X0))
| ssPv1(skf2(X0))
| ssPv3(X0)
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p10481]) ).
cnf(p10488,plain,
( ssPv3(X0)
| ssPv1(X0)
| ssPv1(skf2(X0))
| ssPv3(X0)
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p10485,p9708]) ).
cnf(p10489,plain,
( ssPv3(X0)
| ssPv1(skf2(X0))
| ssPv3(X0)
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p10488]) ).
cnf(p10491,plain,
( ssPv1(skf2(X0))
| ssPv3(X0)
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p10489]) ).
cnf(p9323,plain,
( ssPv3(skf3(X0))
| ~ ssPv2(X0)
| ~ ssPv1(X1)
| ~ ssRr(X0,X1)
| ssPv3(X0)
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p9296,p647]) ).
cnf(p9951,plain,
( ssPv3(skf3(X0))
| ~ ssPv2(X0)
| ~ ssPv1(skf2(X0))
| ssPv3(X0)
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p9323,c1]) ).
cnf(p10522,plain,
( ssPv3(skf3(X0))
| ~ ssPv2(X0)
| ssPv3(X0)
| ssPv1(X0)
| ssPv3(X0)
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p10491,p9951]) ).
cnf(p10604,plain,
( ssPv3(skf3(X0))
| ~ ssPv2(X0)
| ssPv3(X0)
| ssPv3(X0)
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p10522]) ).
cnf(p10606,plain,
( ssPv3(skf3(X0))
| ~ ssPv2(X0)
| ssPv3(X0)
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p10604]) ).
cnf(f11,negated_conjecture,
( ssPv3(V)
| ssPv2(V)
| ssPv2(W)
| ~ ssRr(V,W)
| ~ ssPv2(U)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause12) ).
fof(f11_nnf,plain,
! [U,V,W] :
( ssPv3(V)
| ssPv2(V)
| ssPv2(W)
| ~ ssRr(V,W)
| ~ ssPv2(U)
| ~ ssRr(U,V) ),
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
! [U,V,W] :
( ssPv3(V)
| ssPv2(V)
| ssPv2(W)
| ~ ssRr(V,W)
| ~ ssPv2(U)
| ~ ssRr(U,V) ),
inference(skolemisation,[status(esa)],[f11_nnf]) ).
cnf(c11,plain,
( ssPv3(X1)
| ssPv2(X1)
| ssPv2(X2)
| ~ ssRr(X1,X2)
| ~ ssPv2(X0)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(p103,plain,
( ssPv3(X0)
| ssPv2(X0)
| ssPv2(X1)
| ~ ssRr(X0,X1)
| ~ ssPv2(skf3(X0)) ),
inference(resolution,[status(thm)],[c11,c0]) ).
cnf(p9299,plain,
( ssPv3(X0)
| ssPv2(X0)
| ssPv2(X1)
| ~ ssRr(X0,X1)
| ssPv3(X0)
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p9296,p103]) ).
cnf(p9500,plain,
( ssPv2(X0)
| ssPv2(X1)
| ~ ssRr(X0,X1)
| ssPv3(X0)
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p9299]) ).
cnf(p9502,plain,
( ssPv2(X0)
| ssPv2(skf2(X0))
| ssPv3(X0)
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p9500,c1]) ).
cnf(f3,negated_conjecture,
( ssPv3(U)
| ssPv2(U)
| ssPv1(V)
| ~ ssPv4(U)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause4) ).
fof(f3_nnf,plain,
! [U,V] :
( ssPv3(U)
| ssPv2(U)
| ssPv1(V)
| ~ ssPv4(U)
| ~ ssRr(U,V) ),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [U,V] :
( ssPv3(U)
| ssPv2(U)
| ssPv1(V)
| ~ ssPv4(U)
| ~ ssRr(U,V) ),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
( ssPv3(X0)
| ssPv2(X0)
| ssPv1(X1)
| ~ ssPv4(X0)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p56,plain,
( ssPv3(X0)
| ssPv2(X0)
| ssPv1(skf2(X0))
| ~ ssPv4(X0) ),
inference(resolution,[status(thm)],[c3,c1]) ).
cnf(p9197,plain,
( ssPv3(X0)
| ssPv2(X0)
| ssPv1(skf2(X0))
| ssPv3(X0)
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p9196,p56]) ).
cnf(p9233,plain,
( ssPv2(X0)
| ssPv1(skf2(X0))
| ssPv3(X0)
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p9197]) ).
cnf(p9240,plain,
( ssPv2(X0)
| ssPv3(X0)
| ~ ssPv2(skf2(X0))
| ssPv2(X0)
| ssPv3(X0)
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p9233,p155]) ).
cnf(p9450,plain,
( ssPv2(X0)
| ~ ssPv2(skf2(X0))
| ssPv2(X0)
| ssPv3(X0)
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p9240]) ).
cnf(p9452,plain,
( ~ ssPv2(skf2(X0))
| ssPv2(X0)
| ssPv3(X0)
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p9450]) ).
cnf(p9534,plain,
( ssPv2(X0)
| ssPv3(X0)
| ssPv1(X0)
| ssPv2(X0)
| ssPv3(X0)
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p9502,p9452]) ).
cnf(p9572,plain,
( ssPv2(X0)
| ssPv3(X0)
| ssPv2(X0)
| ssPv3(X0)
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p9534]) ).
cnf(p9575,plain,
( ssPv2(X0)
| ssPv2(X0)
| ssPv3(X0)
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p9572]) ).
cnf(p9577,plain,
( ssPv2(X0)
| ssPv3(X0)
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p9575]) ).
cnf(p10613,plain,
( ssPv3(X0)
| ssPv1(X0)
| ssPv3(skf3(X0))
| ssPv3(X0)
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p10606,p9577]) ).
cnf(p10616,plain,
( ssPv3(X0)
| ssPv3(skf3(X0))
| ssPv3(X0)
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p10613]) ).
cnf(p10619,plain,
( ssPv3(skf3(X0))
| ssPv3(X0)
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p10616]) ).
cnf(p9579,plain,
( ssPv1(X0)
| ssPv4(skf2(X0))
| ssPv1(skf3(X0))
| ssPv3(X0)
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p9577,p139]) ).
cnf(p9634,plain,
( ssPv4(skf2(X0))
| ssPv1(skf3(X0))
| ssPv3(X0)
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p9579]) ).
cnf(p9641,plain,
( ssPv1(X0)
| ssPv1(skf3(X0))
| ~ ssPv2(X0)
| ssPv1(skf3(X0))
| ssPv3(X0)
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p9634,p215]) ).
cnf(p10023,plain,
( ssPv1(X0)
| ~ ssPv2(X0)
| ssPv1(skf3(X0))
| ssPv3(X0)
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p9641]) ).
cnf(p10024,plain,
( ~ ssPv2(X0)
| ssPv1(skf3(X0))
| ssPv3(X0)
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p10023]) ).
cnf(p10032,plain,
( ssPv3(X0)
| ssPv1(X0)
| ssPv1(skf3(X0))
| ssPv3(X0)
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p10024,p9577]) ).
cnf(p10034,plain,
( ssPv3(X0)
| ssPv1(skf3(X0))
| ssPv3(X0)
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p10032]) ).
cnf(p10036,plain,
( ssPv1(skf3(X0))
| ssPv3(X0)
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p10034]) ).
cnf(p9582,plain,
( ssPv1(X0)
| ~ ssPv3(skf3(X0))
| ~ ssPv1(skf3(X0))
| ssPv3(X0)
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p9577,p226]) ).
cnf(p9665,plain,
( ~ ssPv3(skf3(X0))
| ~ ssPv1(skf3(X0))
| ssPv3(X0)
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p9582]) ).
cnf(p10064,plain,
( ~ ssPv3(skf3(X0))
| ssPv3(X0)
| ssPv1(X0)
| ssPv3(X0)
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p10036,p9665]) ).
cnf(p10067,plain,
( ~ ssPv3(skf3(X0))
| ssPv3(X0)
| ssPv3(X0)
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p10064]) ).
cnf(p10069,plain,
( ~ ssPv3(skf3(X0))
| ssPv3(X0)
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p10067]) ).
cnf(p10644,plain,
( ssPv3(X0)
| ssPv1(X0)
| ssPv3(X0)
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p10619,p10069]) ).
cnf(p10645,plain,
( ssPv3(X0)
| ssPv3(X0)
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p10644]) ).
cnf(p10647,plain,
( ssPv3(X0)
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p10645]) ).
cnf(p10693,plain,
( ssPv1(skf2(X0))
| ssPv2(X0)
| ssPv3(X0)
| ssPv3(X0) ),
inference(resolution,[status(thm)],[p10647,p4249]) ).
cnf(p10718,plain,
( ssPv1(skf2(X0))
| ssPv2(X0)
| ssPv3(X0) ),
inference(factoring,[status(thm)],[p10693]) ).
cnf(p10739,plain,
( ssPv4(skf2(skf2(X0)))
| ssPv2(X0)
| ssPv3(X0)
| ssPv2(X0)
| ssPv3(X0) ),
inference(resolution,[status(thm)],[p10718,p388]) ).
cnf(p11532,plain,
( ssPv4(skf2(skf2(X0)))
| ssPv2(X0)
| ssPv2(X0)
| ssPv3(X0) ),
inference(factoring,[status(thm)],[p10739]) ).
cnf(p11534,plain,
( ssPv4(skf2(skf2(X0)))
| ssPv2(X0)
| ssPv3(X0) ),
inference(factoring,[status(thm)],[p11532]) ).
cnf(p11546,plain,
( ssPv2(skf2(X0))
| ssPv2(X0)
| ~ ssPv1(skf2(X0))
| ssPv2(X0)
| ssPv3(X0) ),
inference(resolution,[status(thm)],[p11534,p342]) ).
cnf(p11636,plain,
( ssPv2(skf2(X0))
| ~ ssPv1(skf2(X0))
| ssPv2(X0)
| ssPv3(X0) ),
inference(factoring,[status(thm)],[p11546]) ).
cnf(p11638,plain,
( ssPv2(X0)
| ssPv3(X0)
| ssPv2(skf2(X0))
| ssPv2(X0)
| ssPv3(X0) ),
inference(resolution,[status(thm)],[p11636,p10718]) ).
cnf(p11639,plain,
( ssPv2(X0)
| ssPv2(skf2(X0))
| ssPv2(X0)
| ssPv3(X0) ),
inference(factoring,[status(thm)],[p11638]) ).
cnf(p11641,plain,
( ssPv2(skf2(X0))
| ssPv2(X0)
| ssPv3(X0) ),
inference(factoring,[status(thm)],[p11639]) ).
cnf(p10726,plain,
( ssPv2(X0)
| ssPv3(X0)
| ~ ssPv2(skf2(X0))
| ssPv2(X0)
| ssPv3(X0) ),
inference(resolution,[status(thm)],[p10718,p155]) ).
cnf(p11205,plain,
( ssPv2(X0)
| ~ ssPv2(skf2(X0))
| ssPv2(X0)
| ssPv3(X0) ),
inference(factoring,[status(thm)],[p10726]) ).
cnf(p11207,plain,
( ~ ssPv2(skf2(X0))
| ssPv2(X0)
| ssPv3(X0) ),
inference(factoring,[status(thm)],[p11205]) ).
cnf(p11675,plain,
( ssPv2(X0)
| ssPv3(X0)
| ssPv2(X0)
| ssPv3(X0) ),
inference(resolution,[status(thm)],[p11641,p11207]) ).
cnf(p11677,plain,
( ssPv2(X0)
| ssPv2(X0)
| ssPv3(X0) ),
inference(factoring,[status(thm)],[p11675]) ).
cnf(p11679,plain,
( ssPv2(X0)
| ssPv3(X0) ),
inference(factoring,[status(thm)],[p11677]) ).
cnf(f44,negated_conjecture,
( ssPv1(X)
| ~ ssPv2(V)
| ~ ssRr(V,X)
| ~ ssPv3(W)
| ~ ssRr(V,W)
| ~ ssPv2(U)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause45) ).
fof(f44_nnf,plain,
! [U,V,W,X] :
( ssPv1(X)
| ~ ssPv2(V)
| ~ ssRr(V,X)
| ~ ssPv3(W)
| ~ ssRr(V,W)
| ~ ssPv2(U)
| ~ ssRr(U,V) ),
inference(nnf_transformation,[status(thm)],[f44]) ).
fof(f44_sk,plain,
! [U,V,W,X] :
( ssPv1(X)
| ~ ssPv2(V)
| ~ ssRr(V,X)
| ~ ssPv3(W)
| ~ ssRr(V,W)
| ~ ssPv2(U)
| ~ ssRr(U,V) ),
inference(skolemisation,[status(esa)],[f44_nnf]) ).
cnf(c44,plain,
( ssPv1(X3)
| ~ ssPv2(X1)
| ~ ssRr(X1,X3)
| ~ ssPv3(X2)
| ~ ssRr(X1,X2)
| ~ ssPv2(X0)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f44_sk]) ).
cnf(p336,plain,
( ssPv1(X2)
| ~ ssPv2(X1)
| ~ ssPv3(X2)
| ~ ssRr(X1,X2)
| ~ ssPv2(X0)
| ~ ssRr(X0,X1) ),
inference(factoring,[status(thm)],[c44]) ).
cnf(p677,plain,
( ssPv1(X1)
| ~ ssPv2(skf2(X0))
| ~ ssPv3(X1)
| ~ ssRr(skf2(X0),X1)
| ~ ssPv2(X0) ),
inference(resolution,[status(thm)],[p336,c1]) ).
cnf(p11706,plain,
( ssPv1(X1)
| ~ ssPv2(skf2(X0))
| ~ ssPv3(X1)
| ~ ssRr(skf2(X0),X1)
| ssPv3(X0) ),
inference(resolution,[status(thm)],[p11679,p677]) ).
cnf(p12670,plain,
( ssPv1(skf2(skf2(X0)))
| ~ ssPv2(skf2(X0))
| ~ ssPv3(skf2(skf2(X0)))
| ssPv3(X0) ),
inference(resolution,[status(thm)],[p11706,c1]) ).
cnf(p648,plain,
( ssPv3(X0)
| ~ ssPv2(skf2(X0))
| ~ ssPv1(X1)
| ~ ssRr(skf2(X0),X1)
| ~ ssPv2(X0) ),
inference(resolution,[status(thm)],[p324,c1]) ).
cnf(p11704,plain,
( ssPv3(X0)
| ~ ssPv2(skf2(X0))
| ~ ssPv1(X1)
| ~ ssRr(skf2(X0),X1)
| ssPv3(X0) ),
inference(resolution,[status(thm)],[p11679,p648]) ).
cnf(p12629,plain,
( ~ ssPv2(skf2(X0))
| ~ ssPv1(X1)
| ~ ssRr(skf2(X0),X1)
| ssPv3(X0) ),
inference(factoring,[status(thm)],[p11704]) ).
cnf(p12630,plain,
( ~ ssPv2(skf2(X0))
| ~ ssPv1(skf2(skf2(X0)))
| ssPv3(X0) ),
inference(resolution,[status(thm)],[p12629,c1]) ).
cnf(p12631,plain,
( ssPv3(skf2(skf2(X0)))
| ~ ssPv2(skf2(X0))
| ssPv3(X0) ),
inference(resolution,[status(thm)],[p12630,p10647]) ).
cnf(p12635,plain,
( ssPv3(skf2(X0))
| ssPv3(skf2(skf2(X0)))
| ssPv3(X0) ),
inference(resolution,[status(thm)],[p12631,p11679]) ).
cnf(p12671,plain,
( ssPv3(skf2(X0))
| ssPv3(X0)
| ssPv1(skf2(skf2(X0)))
| ~ ssPv2(skf2(X0))
| ssPv3(X0) ),
inference(resolution,[status(thm)],[p12670,p12635]) ).
cnf(p13083,plain,
( ssPv3(skf2(X0))
| ssPv1(skf2(skf2(X0)))
| ~ ssPv2(skf2(X0))
| ssPv3(X0) ),
inference(factoring,[status(thm)],[p12671]) ).
cnf(p13085,plain,
( ssPv3(skf2(X0))
| ssPv3(skf2(X0))
| ssPv1(skf2(skf2(X0)))
| ssPv3(X0) ),
inference(resolution,[status(thm)],[p13083,p11679]) ).
cnf(p13086,plain,
( ssPv3(skf2(X0))
| ssPv1(skf2(skf2(X0)))
| ssPv3(X0) ),
inference(factoring,[status(thm)],[p13085]) ).
cnf(p13112,plain,
( ~ ssPv2(skf2(X0))
| ssPv3(X0)
| ssPv3(skf2(X0))
| ssPv3(X0) ),
inference(resolution,[status(thm)],[p13086,p12630]) ).
cnf(p13117,plain,
( ~ ssPv2(skf2(X0))
| ssPv3(skf2(X0))
| ssPv3(X0) ),
inference(factoring,[status(thm)],[p13112]) ).
cnf(p13119,plain,
( ssPv3(skf2(X0))
| ssPv3(skf2(X0))
| ssPv3(X0) ),
inference(resolution,[status(thm)],[p13117,p11679]) ).
cnf(p13121,plain,
( ssPv3(skf2(X0))
| ssPv3(X0) ),
inference(factoring,[status(thm)],[p13119]) ).
cnf(p13125,plain,
( ssPv3(X0)
| ssPv1(skf2(X0))
| ~ ssPv1(X0)
| ssPv3(X0) ),
inference(resolution,[status(thm)],[p13121,p167]) ).
cnf(p13152,plain,
( ssPv1(skf2(X0))
| ~ ssPv1(X0)
| ssPv3(X0) ),
inference(factoring,[status(thm)],[p13125]) ).
cnf(p13153,plain,
( ssPv3(X0)
| ssPv1(skf2(X0))
| ssPv3(X0) ),
inference(resolution,[status(thm)],[p13152,p10647]) ).
cnf(p13158,plain,
( ssPv1(skf2(X0))
| ssPv3(X0) ),
inference(factoring,[status(thm)],[p13153]) ).
cnf(f51,negated_conjecture,
( ~ ssPv1(V)
| ~ ssPv1(X)
| ~ ssRr(V,X)
| ~ ssPv1(W)
| ~ ssRr(W,V)
| ~ ssPv2(U)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause52) ).
fof(f51_nnf,plain,
! [U,V,W,X] :
( ~ ssPv1(V)
| ~ ssPv1(X)
| ~ ssRr(V,X)
| ~ ssPv1(W)
| ~ ssRr(W,V)
| ~ ssPv2(U)
| ~ ssRr(U,V) ),
inference(nnf_transformation,[status(thm)],[f51]) ).
fof(f51_sk,plain,
! [U,V,W,X] :
( ~ ssPv1(V)
| ~ ssPv1(X)
| ~ ssRr(V,X)
| ~ ssPv1(W)
| ~ ssRr(W,V)
| ~ ssPv2(U)
| ~ ssRr(U,V) ),
inference(skolemisation,[status(esa)],[f51_nnf]) ).
cnf(c51,plain,
( ~ ssPv1(X1)
| ~ ssPv1(X3)
| ~ ssRr(X1,X3)
| ~ ssPv1(X2)
| ~ ssRr(X2,X1)
| ~ ssPv2(X0)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f51_sk]) ).
cnf(p399,plain,
( ~ ssPv1(X1)
| ~ ssPv1(X2)
| ~ ssRr(X1,X2)
| ~ ssPv1(X0)
| ~ ssPv2(X0)
| ~ ssRr(X0,X1) ),
inference(factoring,[status(thm)],[c51]) ).
cnf(p803,plain,
( ~ ssPv1(skf2(X0))
| ~ ssPv1(X1)
| ~ ssRr(skf2(X0),X1)
| ~ ssPv1(X0)
| ~ ssPv2(X0) ),
inference(resolution,[status(thm)],[p399,c1]) ).
cnf(p11712,plain,
( ~ ssPv1(skf2(X0))
| ~ ssPv1(X1)
| ~ ssRr(skf2(X0),X1)
| ~ ssPv1(X0)
| ssPv3(X0) ),
inference(resolution,[status(thm)],[p11679,p803]) ).
cnf(p12674,plain,
( ssPv3(X0)
| ~ ssPv1(skf2(X0))
| ~ ssPv1(X1)
| ~ ssRr(skf2(X0),X1)
| ssPv3(X0) ),
inference(resolution,[status(thm)],[p11712,p10647]) ).
cnf(p12891,plain,
( ~ ssPv1(skf2(X0))
| ~ ssPv1(X1)
| ~ ssRr(skf2(X0),X1)
| ssPv3(X0) ),
inference(factoring,[status(thm)],[p12674]) ).
cnf(p12892,plain,
( ~ ssPv1(skf2(X0))
| ~ ssPv1(skf2(skf2(X0)))
| ssPv3(X0) ),
inference(resolution,[status(thm)],[p12891,c1]) ).
cnf(p12893,plain,
( ssPv3(skf2(skf2(X0)))
| ~ ssPv1(skf2(X0))
| ssPv3(X0) ),
inference(resolution,[status(thm)],[p12892,p10647]) ).
cnf(p13187,plain,
( ssPv3(skf2(skf2(X0)))
| ssPv3(X0)
| ssPv3(X0) ),
inference(resolution,[status(thm)],[p13158,p12893]) ).
cnf(p13188,plain,
( ssPv3(skf2(skf2(X0)))
| ssPv3(X0) ),
inference(factoring,[status(thm)],[p13187]) ).
cnf(p13225,plain,
( ssPv1(skf2(skf2(X0)))
| ~ ssPv2(skf2(X0))
| ssPv3(X0)
| ssPv3(X0) ),
inference(resolution,[status(thm)],[p13188,p12670]) ).
cnf(p13342,plain,
( ssPv1(skf2(skf2(X0)))
| ~ ssPv2(skf2(X0))
| ssPv3(X0) ),
inference(factoring,[status(thm)],[p13225]) ).
cnf(p13162,plain,
( ssPv4(X0)
| ssPv3(X0)
| ssPv2(skf2(X0))
| ssPv3(X0) ),
inference(resolution,[status(thm)],[p13158,p101]) ).
cnf(p13227,plain,
( ssPv4(X0)
| ssPv2(skf2(X0))
| ssPv3(X0) ),
inference(factoring,[status(thm)],[p13162]) ).
cnf(p13345,plain,
( ssPv4(X0)
| ssPv3(X0)
| ssPv1(skf2(skf2(X0)))
| ssPv3(X0) ),
inference(resolution,[status(thm)],[p13342,p13227]) ).
cnf(p13347,plain,
( ssPv4(X0)
| ssPv1(skf2(skf2(X0)))
| ssPv3(X0) ),
inference(factoring,[status(thm)],[p13345]) ).
cnf(p13371,plain,
( ~ ssPv2(skf2(X0))
| ssPv3(X0)
| ssPv4(X0)
| ssPv3(X0) ),
inference(resolution,[status(thm)],[p13347,p12630]) ).
cnf(p13377,plain,
( ~ ssPv2(skf2(X0))
| ssPv4(X0)
| ssPv3(X0) ),
inference(factoring,[status(thm)],[p13371]) ).
cnf(p13379,plain,
( ssPv4(X0)
| ssPv3(X0)
| ssPv4(X0)
| ssPv3(X0) ),
inference(resolution,[status(thm)],[p13377,p13227]) ).
cnf(p13382,plain,
( ssPv4(X0)
| ssPv4(X0)
| ssPv3(X0) ),
inference(factoring,[status(thm)],[p13379]) ).
cnf(p13384,plain,
( ssPv4(X0)
| ssPv3(X0) ),
inference(factoring,[status(thm)],[p13382]) ).
cnf(p11703,plain,
( ssPv3(skf3(X0))
| ~ ssPv2(X0)
| ~ ssPv1(X1)
| ~ ssRr(X0,X1)
| ssPv3(skf3(X0)) ),
inference(resolution,[status(thm)],[p11679,p647]) ).
cnf(p12126,plain,
( ~ ssPv2(X0)
| ~ ssPv1(X1)
| ~ ssRr(X0,X1)
| ssPv3(skf3(X0)) ),
inference(factoring,[status(thm)],[p11703]) ).
cnf(p12128,plain,
( ~ ssPv2(X0)
| ~ ssPv1(skf2(X0))
| ssPv3(skf3(X0)) ),
inference(resolution,[status(thm)],[p12126,c1]) ).
cnf(p12129,plain,
( ssPv3(skf2(X0))
| ~ ssPv2(X0)
| ssPv3(skf3(X0)) ),
inference(resolution,[status(thm)],[p12128,p10647]) ).
cnf(p12138,plain,
( ssPv3(X0)
| ssPv3(skf2(X0))
| ssPv3(skf3(X0)) ),
inference(resolution,[status(thm)],[p12129,p11679]) ).
cnf(p12145,plain,
( ssPv3(X0)
| ssPv1(skf2(X0))
| ~ ssPv1(X0)
| ssPv3(X0)
| ssPv3(skf3(X0)) ),
inference(resolution,[status(thm)],[p12138,p167]) ).
cnf(p12217,plain,
( ssPv1(skf2(X0))
| ~ ssPv1(X0)
| ssPv3(X0)
| ssPv3(skf3(X0)) ),
inference(factoring,[status(thm)],[p12145]) ).
cnf(p12218,plain,
( ssPv3(X0)
| ssPv1(skf2(X0))
| ssPv3(X0)
| ssPv3(skf3(X0)) ),
inference(resolution,[status(thm)],[p12217,p10647]) ).
cnf(p12220,plain,
( ssPv1(skf2(X0))
| ssPv3(X0)
| ssPv3(skf3(X0)) ),
inference(factoring,[status(thm)],[p12218]) ).
cnf(p12251,plain,
( ~ ssPv2(X0)
| ssPv3(skf3(X0))
| ssPv3(X0)
| ssPv3(skf3(X0)) ),
inference(resolution,[status(thm)],[p12220,p12128]) ).
cnf(p12253,plain,
( ~ ssPv2(X0)
| ssPv3(X0)
| ssPv3(skf3(X0)) ),
inference(factoring,[status(thm)],[p12251]) ).
cnf(p12258,plain,
( ssPv3(X0)
| ssPv3(X0)
| ssPv3(skf3(X0)) ),
inference(resolution,[status(thm)],[p12253,p11679]) ).
cnf(p12261,plain,
( ssPv3(X0)
| ssPv3(skf3(X0)) ),
inference(factoring,[status(thm)],[p12258]) ).
cnf(f20,negated_conjecture,
( ssPv3(V)
| ssPv2(W)
| ~ ssPv4(V)
| ~ ssRr(V,W)
| ~ ssPv3(U)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause21) ).
fof(f20_nnf,plain,
! [U,V,W] :
( ssPv3(V)
| ssPv2(W)
| ~ ssPv4(V)
| ~ ssRr(V,W)
| ~ ssPv3(U)
| ~ ssRr(U,V) ),
inference(nnf_transformation,[status(thm)],[f20]) ).
fof(f20_sk,plain,
! [U,V,W] :
( ssPv3(V)
| ssPv2(W)
| ~ ssPv4(V)
| ~ ssRr(V,W)
| ~ ssPv3(U)
| ~ ssRr(U,V) ),
inference(skolemisation,[status(esa)],[f20_nnf]) ).
cnf(c20,plain,
( ssPv3(X1)
| ssPv2(X2)
| ~ ssPv4(X1)
| ~ ssRr(X1,X2)
| ~ ssPv3(X0)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f20_sk]) ).
cnf(p158,plain,
( ssPv3(X0)
| ssPv2(X1)
| ~ ssPv4(X0)
| ~ ssRr(X0,X1)
| ~ ssPv3(skf3(X0)) ),
inference(resolution,[status(thm)],[c20,c0]) ).
cnf(p12266,plain,
( ssPv3(X0)
| ssPv2(X1)
| ~ ssPv4(X0)
| ~ ssRr(X0,X1)
| ssPv3(X0) ),
inference(resolution,[status(thm)],[p12261,p158]) ).
cnf(p12346,plain,
( ssPv2(X1)
| ~ ssPv4(X0)
| ~ ssRr(X0,X1)
| ssPv3(X0) ),
inference(factoring,[status(thm)],[p12266]) ).
cnf(p12349,plain,
( ssPv2(skf2(X0))
| ~ ssPv4(X0)
| ssPv3(X0) ),
inference(resolution,[status(thm)],[p12346,c1]) ).
cnf(p13414,plain,
( ssPv2(skf2(X0))
| ssPv3(X0)
| ssPv3(X0) ),
inference(resolution,[status(thm)],[p13384,p12349]) ).
cnf(p13416,plain,
( ssPv2(skf2(X0))
| ssPv3(X0) ),
inference(factoring,[status(thm)],[p13414]) ).
cnf(p13450,plain,
( ssPv1(skf2(skf2(X0)))
| ssPv3(X0)
| ssPv3(X0) ),
inference(resolution,[status(thm)],[p13416,p13342]) ).
cnf(p13557,plain,
( ssPv1(skf2(skf2(X0)))
| ssPv3(X0) ),
inference(factoring,[status(thm)],[p13450]) ).
cnf(p13577,plain,
( ~ ssPv2(skf2(X0))
| ssPv3(X0)
| ssPv3(X0) ),
inference(resolution,[status(thm)],[p13557,p12630]) ).
cnf(p13582,plain,
( ~ ssPv2(skf2(X0))
| ssPv3(X0) ),
inference(factoring,[status(thm)],[p13577]) ).
cnf(p13583,plain,
( ssPv3(X0)
| ssPv3(X0) ),
inference(resolution,[status(thm)],[p13582,p13416]) ).
cnf(p13584,plain,
ssPv3(X0),
inference(factoring,[status(thm)],[p13583]) ).
cnf(p13585,plain,
( ssPv4(X0)
| ssPv1(X0)
| ssPv4(skf3(X0)) ),
inference(resolution,[status(thm)],[p13584,p125]) ).
cnf(f49,negated_conjecture,
( ssPv1(V)
| ~ ssPv3(X)
| ~ ssRr(V,X)
| ~ ssPv3(W)
| ~ ssRr(W,V)
| ~ ssPv4(U)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause50) ).
fof(f49_nnf,plain,
! [U,V,W,X] :
( ssPv1(V)
| ~ ssPv3(X)
| ~ ssRr(V,X)
| ~ ssPv3(W)
| ~ ssRr(W,V)
| ~ ssPv4(U)
| ~ ssRr(U,V) ),
inference(nnf_transformation,[status(thm)],[f49]) ).
fof(f49_sk,plain,
! [U,V,W,X] :
( ssPv1(V)
| ~ ssPv3(X)
| ~ ssRr(V,X)
| ~ ssPv3(W)
| ~ ssRr(W,V)
| ~ ssPv4(U)
| ~ ssRr(U,V) ),
inference(skolemisation,[status(esa)],[f49_nnf]) ).
cnf(c49,plain,
( ssPv1(X1)
| ~ ssPv3(X3)
| ~ ssRr(X1,X3)
| ~ ssPv3(X2)
| ~ ssRr(X2,X1)
| ~ ssPv4(X0)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f49_sk]) ).
cnf(p382,plain,
( ssPv1(X1)
| ~ ssPv3(X2)
| ~ ssRr(X1,X2)
| ~ ssPv3(X0)
| ~ ssPv4(X0)
| ~ ssRr(X0,X1) ),
inference(factoring,[status(thm)],[c49]) ).
cnf(p757,plain,
( ssPv1(X0)
| ~ ssPv3(X1)
| ~ ssRr(X0,X1)
| ~ ssPv3(skf3(X0))
| ~ ssPv4(skf3(X0)) ),
inference(resolution,[status(thm)],[p382,c0]) ).
cnf(p13654,plain,
( ssPv1(X0)
| ~ ssPv3(X1)
| ~ ssRr(X0,X1)
| ~ ssPv3(skf3(X0))
| ssPv4(X0)
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p13585,p757]) ).
cnf(p14369,plain,
( ~ ssPv3(X1)
| ~ ssRr(X0,X1)
| ~ ssPv3(skf3(X0))
| ssPv4(X0)
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p13654]) ).
cnf(p14370,plain,
( ~ ssPv3(X1)
| ~ ssRr(X0,X1)
| ssPv4(X0)
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p14369,p13584]) ).
cnf(p14372,plain,
( ~ ssPv3(skf2(X0))
| ssPv4(X0)
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p14370,c1]) ).
cnf(p14373,plain,
( ssPv4(X0)
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p14372,p13584]) ).
cnf(f28,negated_conjecture,
( ssPv4(U)
| ~ ssPv4(V)
| ~ ssPv3(V)
| ~ ssPv4(W)
| ~ ssRr(V,W)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause29) ).
fof(f28_nnf,plain,
! [U,V,W] :
( ssPv4(U)
| ~ ssPv4(V)
| ~ ssPv3(V)
| ~ ssPv4(W)
| ~ ssRr(V,W)
| ~ ssRr(U,V) ),
inference(nnf_transformation,[status(thm)],[f28]) ).
fof(f28_sk,plain,
! [U,V,W] :
( ssPv4(U)
| ~ ssPv4(V)
| ~ ssPv3(V)
| ~ ssPv4(W)
| ~ ssRr(V,W)
| ~ ssRr(U,V) ),
inference(skolemisation,[status(esa)],[f28_nnf]) ).
cnf(c28,plain,
( ssPv4(X0)
| ~ ssPv4(X1)
| ~ ssPv3(X1)
| ~ ssPv4(X2)
| ~ ssRr(X1,X2)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f28_sk]) ).
cnf(p205,plain,
( ssPv4(X0)
| ~ ssPv4(skf2(X0))
| ~ ssPv3(skf2(X0))
| ~ ssPv4(X1)
| ~ ssRr(skf2(X0),X1) ),
inference(resolution,[status(thm)],[c28,c1]) ).
cnf(p358,plain,
( ssPv4(X0)
| ~ ssPv4(skf2(X0))
| ~ ssPv3(skf2(X0))
| ~ ssPv4(skf2(skf2(X0))) ),
inference(resolution,[status(thm)],[p205,c1]) ).
cnf(p14385,plain,
( ssPv4(X0)
| ~ ssPv4(skf2(X0))
| ~ ssPv3(skf2(X0))
| ssPv1(skf2(skf2(X0))) ),
inference(resolution,[status(thm)],[p14373,p358]) ).
cnf(p14611,plain,
( ssPv4(X0)
| ~ ssPv4(skf2(X0))
| ssPv1(skf2(skf2(X0))) ),
inference(resolution,[status(thm)],[p14385,p13584]) ).
cnf(p14612,plain,
( ssPv1(skf2(X0))
| ssPv4(X0)
| ssPv1(skf2(skf2(X0))) ),
inference(resolution,[status(thm)],[p14611,p14373]) ).
cnf(f50,negated_conjecture,
( ssPv4(U)
| ~ ssPv3(V)
| ~ ssPv1(X)
| ~ ssRr(V,X)
| ~ ssPv3(W)
| ~ ssRr(V,W)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause51) ).
fof(f50_nnf,plain,
! [U,V,W,X] :
( ssPv4(U)
| ~ ssPv3(V)
| ~ ssPv1(X)
| ~ ssRr(V,X)
| ~ ssPv3(W)
| ~ ssRr(V,W)
| ~ ssRr(U,V) ),
inference(nnf_transformation,[status(thm)],[f50]) ).
fof(f50_sk,plain,
! [U,V,W,X] :
( ssPv4(U)
| ~ ssPv3(V)
| ~ ssPv1(X)
| ~ ssRr(V,X)
| ~ ssPv3(W)
| ~ ssRr(V,W)
| ~ ssRr(U,V) ),
inference(skolemisation,[status(esa)],[f50_nnf]) ).
cnf(c50,plain,
( ssPv4(X0)
| ~ ssPv3(X1)
| ~ ssPv1(X3)
| ~ ssRr(X1,X3)
| ~ ssPv3(X2)
| ~ ssRr(X1,X2)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f50_sk]) ).
cnf(p391,plain,
( ssPv4(X0)
| ~ ssPv3(X1)
| ~ ssPv1(X2)
| ~ ssPv3(X2)
| ~ ssRr(X1,X2)
| ~ ssRr(X0,X1) ),
inference(factoring,[status(thm)],[c50]) ).
cnf(p789,plain,
( ssPv4(X0)
| ~ ssPv3(skf2(X0))
| ~ ssPv1(X1)
| ~ ssPv3(X1)
| ~ ssRr(skf2(X0),X1) ),
inference(resolution,[status(thm)],[p391,c1]) ).
cnf(p797,plain,
( ssPv4(X0)
| ~ ssPv3(skf2(X0))
| ~ ssPv1(skf2(skf2(X0)))
| ~ ssPv3(skf2(skf2(X0))) ),
inference(resolution,[status(thm)],[p789,c1]) ).
cnf(p13601,plain,
( ssPv4(X0)
| ~ ssPv3(skf2(X0))
| ~ ssPv1(skf2(skf2(X0))) ),
inference(resolution,[status(thm)],[p13584,p797]) ).
cnf(p14628,plain,
( ssPv4(X0)
| ~ ssPv3(skf2(X0))
| ssPv1(skf2(X0))
| ssPv4(X0) ),
inference(resolution,[status(thm)],[p14612,p13601]) ).
cnf(p14632,plain,
( ~ ssPv3(skf2(X0))
| ssPv1(skf2(X0))
| ssPv4(X0) ),
inference(factoring,[status(thm)],[p14628]) ).
cnf(p14633,plain,
( ssPv1(skf2(X0))
| ssPv4(X0) ),
inference(resolution,[status(thm)],[p14632,p13584]) ).
cnf(p14655,plain,
( ssPv4(X0)
| ~ ssPv3(skf2(X0))
| ssPv4(skf2(X0)) ),
inference(resolution,[status(thm)],[p14633,p13601]) ).
cnf(p14690,plain,
( ssPv4(X0)
| ssPv4(skf2(X0)) ),
inference(resolution,[status(thm)],[p14655,p13584]) ).
cnf(p14712,plain,
( ssPv4(X0)
| ssPv1(skf2(skf2(X0)))
| ssPv4(X0) ),
inference(resolution,[status(thm)],[p14690,p14611]) ).
cnf(p14713,plain,
( ssPv1(skf2(skf2(X0)))
| ssPv4(X0) ),
inference(factoring,[status(thm)],[p14712]) ).
cnf(p14736,plain,
( ssPv4(X0)
| ~ ssPv3(skf2(X0))
| ssPv4(X0) ),
inference(resolution,[status(thm)],[p14713,p13601]) ).
cnf(p14740,plain,
( ~ ssPv3(skf2(X0))
| ssPv4(X0) ),
inference(factoring,[status(thm)],[p14736]) ).
cnf(p14741,plain,
ssPv4(X0),
inference(resolution,[status(thm)],[p14740,p13584]) ).
cnf(p14761,plain,
( ssPv1(X0)
| ~ ssPv3(X1)
| ~ ssRr(X0,X1)
| ~ ssPv3(skf3(X0)) ),
inference(resolution,[status(thm)],[p14741,p757]) ).
cnf(p14888,plain,
( ssPv1(X0)
| ~ ssPv3(X1)
| ~ ssRr(X0,X1) ),
inference(resolution,[status(thm)],[p14761,p13584]) ).
cnf(p14890,plain,
( ssPv1(skf3(X0))
| ~ ssPv3(X0) ),
inference(resolution,[status(thm)],[p14888,c0]) ).
cnf(p14892,plain,
ssPv1(skf3(X0)),
inference(resolution,[status(thm)],[p14890,p13584]) ).
cnf(f45,negated_conjecture,
( ssPv2(V)
| ~ ssPv1(X)
| ~ ssRr(X,V)
| ~ ssPv3(W)
| ~ ssRr(W,V)
| ~ ssPv4(U)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause46) ).
fof(f45_nnf,plain,
! [U,V,W,X] :
( ssPv2(V)
| ~ ssPv1(X)
| ~ ssRr(X,V)
| ~ ssPv3(W)
| ~ ssRr(W,V)
| ~ ssPv4(U)
| ~ ssRr(U,V) ),
inference(nnf_transformation,[status(thm)],[f45]) ).
fof(f45_sk,plain,
! [U,V,W,X] :
( ssPv2(V)
| ~ ssPv1(X)
| ~ ssRr(X,V)
| ~ ssPv3(W)
| ~ ssRr(W,V)
| ~ ssPv4(U)
| ~ ssRr(U,V) ),
inference(skolemisation,[status(esa)],[f45_nnf]) ).
cnf(c45,plain,
( ssPv2(X1)
| ~ ssPv1(X3)
| ~ ssRr(X3,X1)
| ~ ssPv3(X2)
| ~ ssRr(X2,X1)
| ~ ssPv4(X0)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f45_sk]) ).
cnf(p343,plain,
( ssPv2(X1)
| ~ ssPv1(X2)
| ~ ssRr(X2,X1)
| ~ ssPv3(X0)
| ~ ssPv4(X0)
| ~ ssRr(X0,X1) ),
inference(factoring,[status(thm)],[c45]) ).
cnf(p686,plain,
( ssPv2(X1)
| ~ ssPv1(X0)
| ~ ssPv3(X0)
| ~ ssPv4(X0)
| ~ ssRr(X0,X1) ),
inference(factoring,[status(thm)],[p343]) ).
cnf(p689,plain,
( ssPv2(X0)
| ~ ssPv1(skf3(X0))
| ~ ssPv3(skf3(X0))
| ~ ssPv4(skf3(X0)) ),
inference(resolution,[status(thm)],[p686,c0]) ).
cnf(p14750,plain,
( ssPv2(X0)
| ~ ssPv1(skf3(X0))
| ~ ssPv3(skf3(X0)) ),
inference(resolution,[status(thm)],[p14741,p689]) ).
cnf(p14782,plain,
( ssPv2(X0)
| ~ ssPv1(skf3(X0)) ),
inference(resolution,[status(thm)],[p14750,p13584]) ).
cnf(p14898,plain,
ssPv2(X0),
inference(resolution,[status(thm)],[p14892,p14782]) ).
cnf(f33,negated_conjecture,
( ~ ssPv4(U)
| ~ ssPv1(U)
| ~ ssPv1(W)
| ~ ssRr(U,W)
| ~ ssPv2(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause34) ).
fof(f33_nnf,plain,
! [U,V,W] :
( ~ ssPv4(U)
| ~ ssPv1(U)
| ~ ssPv1(W)
| ~ ssRr(U,W)
| ~ ssPv2(V)
| ~ ssRr(U,V) ),
inference(nnf_transformation,[status(thm)],[f33]) ).
fof(f33_sk,plain,
! [U,V,W] :
( ~ ssPv4(U)
| ~ ssPv1(U)
| ~ ssPv1(W)
| ~ ssRr(U,W)
| ~ ssPv2(V)
| ~ ssRr(U,V) ),
inference(skolemisation,[status(esa)],[f33_nnf]) ).
cnf(c33,plain,
( ~ ssPv4(X0)
| ~ ssPv1(X0)
| ~ ssPv1(X2)
| ~ ssRr(X0,X2)
| ~ ssPv2(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f33_sk]) ).
cnf(p237,plain,
( ~ ssPv4(X0)
| ~ ssPv1(X0)
| ~ ssPv1(X1)
| ~ ssPv2(X1)
| ~ ssRr(X0,X1) ),
inference(factoring,[status(thm)],[c33]) ).
cnf(p244,plain,
( ~ ssPv4(skf3(X0))
| ~ ssPv1(skf3(X0))
| ~ ssPv1(X0)
| ~ ssPv2(X0) ),
inference(resolution,[status(thm)],[p237,c0]) ).
cnf(p14901,plain,
( ~ ssPv4(skf3(X0))
| ~ ssPv1(skf3(X0))
| ~ ssPv1(X0) ),
inference(resolution,[status(thm)],[p14898,p244]) ).
cnf(p14747,plain,
( ssPv2(skf2(X0))
| ssPv2(X0)
| ~ ssPv1(skf2(X0)) ),
inference(resolution,[status(thm)],[p14741,p342]) ).
cnf(p1493,plain,
( ssPv1(X0)
| ~ ssPv3(X1)
| ~ ssRr(X0,X1)
| ~ ssPv3(skf3(X0))
| ssPv1(skf2(X0))
| ssPv2(X0)
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p1465,p757]) ).
cnf(p1725,plain,
( ~ ssPv3(X1)
| ~ ssRr(X0,X1)
| ~ ssPv3(skf3(X0))
| ssPv1(skf2(X0))
| ssPv2(X0)
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p1493]) ).
cnf(p13613,plain,
( ~ ssPv3(X1)
| ~ ssRr(X0,X1)
| ssPv1(skf2(X0))
| ssPv2(X0)
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p13584,p1725]) ).
cnf(p13902,plain,
( ~ ssPv3(skf2(X0))
| ssPv1(skf2(X0))
| ssPv2(X0)
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p13613,c1]) ).
cnf(p13903,plain,
( ssPv1(skf2(X0))
| ssPv2(X0)
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p13902,p13584]) ).
cnf(p14781,plain,
( ssPv2(X0)
| ssPv1(X0)
| ssPv2(skf2(X0))
| ssPv2(X0) ),
inference(resolution,[status(thm)],[p14747,p13903]) ).
cnf(p14812,plain,
( ssPv1(X0)
| ssPv2(skf2(X0))
| ssPv2(X0) ),
inference(factoring,[status(thm)],[p14781]) ).
cnf(p14743,plain,
( ssPv2(X0)
| ssPv1(X0)
| ~ ssPv2(skf2(X0)) ),
inference(resolution,[status(thm)],[p14741,p198]) ).
cnf(p14829,plain,
( ssPv2(X0)
| ssPv1(X0)
| ssPv1(X0)
| ssPv2(X0) ),
inference(resolution,[status(thm)],[p14812,p14743]) ).
cnf(p14831,plain,
( ssPv1(X0)
| ssPv1(X0)
| ssPv2(X0) ),
inference(factoring,[status(thm)],[p14829]) ).
cnf(p14833,plain,
( ssPv1(X0)
| ssPv2(X0) ),
inference(factoring,[status(thm)],[p14831]) ).
cnf(p14745,plain,
( ssPv1(X0)
| ssPv1(skf3(X0))
| ~ ssPv2(X0) ),
inference(resolution,[status(thm)],[p14741,p215]) ).
cnf(p14859,plain,
( ssPv1(X0)
| ssPv1(skf3(X0))
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p14833,p14745]) ).
cnf(p14862,plain,
( ssPv1(skf3(X0))
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p14859]) ).
cnf(f32,negated_conjecture,
( ssPv1(W)
| ~ ssPv2(U)
| ~ ssPv1(U)
| ~ ssRr(U,W)
| ~ ssPv3(V)
| ~ ssRr(U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause33) ).
fof(f32_nnf,plain,
! [U,V,W] :
( ssPv1(W)
| ~ ssPv2(U)
| ~ ssPv1(U)
| ~ ssRr(U,W)
| ~ ssPv3(V)
| ~ ssRr(U,V) ),
inference(nnf_transformation,[status(thm)],[f32]) ).
fof(f32_sk,plain,
! [U,V,W] :
( ssPv1(W)
| ~ ssPv2(U)
| ~ ssPv1(U)
| ~ ssRr(U,W)
| ~ ssPv3(V)
| ~ ssRr(U,V) ),
inference(skolemisation,[status(esa)],[f32_nnf]) ).
cnf(c32,plain,
( ssPv1(X2)
| ~ ssPv2(X0)
| ~ ssPv1(X0)
| ~ ssRr(X0,X2)
| ~ ssPv3(X1)
| ~ ssRr(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f32_sk]) ).
cnf(p229,plain,
( ssPv1(X1)
| ~ ssPv2(X0)
| ~ ssPv1(X0)
| ~ ssPv3(X1)
| ~ ssRr(X0,X1) ),
inference(factoring,[status(thm)],[c32]) ).
cnf(p232,plain,
( ssPv1(X0)
| ~ ssPv2(skf3(X0))
| ~ ssPv1(skf3(X0))
| ~ ssPv3(X0) ),
inference(resolution,[status(thm)],[p229,c0]) ).
cnf(p13591,plain,
( ssPv1(X0)
| ~ ssPv2(skf3(X0))
| ~ ssPv1(skf3(X0)) ),
inference(resolution,[status(thm)],[p13584,p232]) ).
cnf(p14865,plain,
( ssPv1(X0)
| ~ ssPv2(skf3(X0))
| ssPv1(X0) ),
inference(resolution,[status(thm)],[p14862,p13591]) ).
cnf(p14889,plain,
( ~ ssPv2(skf3(X0))
| ssPv1(X0) ),
inference(factoring,[status(thm)],[p14865]) ).
cnf(p14921,plain,
ssPv1(X0),
inference(resolution,[status(thm)],[p14898,p14889]) ).
cnf(p14922,plain,
( ~ ssPv4(skf3(X0))
| ~ ssPv1(skf3(X0)) ),
inference(resolution,[status(thm)],[p14901,p14921]) ).
cnf(p14923,plain,
~ ssPv4(skf3(X0)),
inference(resolution,[status(thm)],[p14922,p14921]) ).
cnf(p14924,plain,
$false,
inference(resolution,[status(thm)],[p14923,p14741]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN796-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.08/0.35 % Computer : n007.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Fri Sep 25 02:16:26 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.35 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 21.86/3.38 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 21.86/3.38 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------