%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SYN036-4 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n013.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:33:32 PM UTC 2026
% Result : Unsatisfiable 0.14s 10.81s
% Output : Proof 0.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 49
% Number of leaves : 17
% Syntax : Number of formulae : 149 ( 6 unt; 0 def)
% Number of atoms : 610 ( 0 equ)
% Maximal formula atoms : 6 ( 4 avg)
% Number of connectives : 704 ( 243 ~; 461 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 5 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 3 ( 2 usr; 1 prp; 0-1 aty)
% Number of functors : 6 ( 6 usr; 2 con; 0-1 aty)
% Number of variables : 206 ( 94 sgn 72 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f31,negated_conjecture,
( q(fz5(W9))
| q(W9)
| q(cw)
| p(fy5(X7))
| p(X7)
| p(cx) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_32) ).
fof(f31_nnf,plain,
! [X7,W9] :
( q(fz5(W9))
| q(W9)
| q(cw)
| p(fy5(X7))
| p(X7)
| p(cx) ),
inference(nnf_transformation,[status(thm)],[f31]) ).
fof(f31_sk,plain,
! [X7,W9] :
( q(fz5(W9))
| q(W9)
| q(cw)
| p(fy5(X7))
| p(X7)
| p(cx) ),
inference(skolemisation,[status(esa)],[f31_nnf]) ).
cnf(c31,plain,
( q(fz5(X1))
| q(X1)
| q(cw)
| p(fy5(X0))
| p(X0)
| p(cx) ),
inference(cnf_transformation,[status(esa)],[f31_sk]) ).
cnf(p54,plain,
( q(fz5(X0))
| q(X0)
| q(cw)
| p(fy5(cx))
| p(cx) ),
inference(factoring,[status(thm)],[c31]) ).
cnf(p68,plain,
( q(fz5(cw))
| q(cw)
| p(fy5(cx))
| p(cx) ),
inference(factoring,[status(thm)],[p54]) ).
cnf(f19,negated_conjecture,
( q(cw)
| p(fy(X1))
| p(X1)
| p(cx)
| ~ q(Z2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_20) ).
fof(f19_nnf,plain,
! [Z2,X1] :
( q(cw)
| p(fy(X1))
| p(X1)
| p(cx)
| ~ q(Z2) ),
inference(nnf_transformation,[status(thm)],[f19]) ).
fof(f19_sk,plain,
! [Z2,X1] :
( q(cw)
| p(fy(X1))
| p(X1)
| p(cx)
| ~ q(Z2) ),
inference(skolemisation,[status(esa)],[f19_nnf]) ).
cnf(c19,plain,
( q(cw)
| p(fy(X1))
| p(X1)
| p(cx)
| ~ q(X0) ),
inference(cnf_transformation,[status(esa)],[f19_sk]) ).
cnf(p40,plain,
( q(cw)
| p(fy(cx))
| p(cx)
| ~ q(X0) ),
inference(factoring,[status(thm)],[c19]) ).
cnf(p73,plain,
( q(cw)
| p(fy(cx))
| p(cx)
| q(cw)
| p(fy5(cx))
| p(cx) ),
inference(resolution,[status(thm)],[p68,p40]) ).
cnf(p86,plain,
( q(cw)
| p(fy(cx))
| q(cw)
| p(fy5(cx))
| p(cx) ),
inference(factoring,[status(thm)],[p73]) ).
cnf(p88,plain,
( p(fy(cx))
| q(cw)
| p(fy5(cx))
| p(cx) ),
inference(factoring,[status(thm)],[p86]) ).
cnf(f3,negated_conjecture,
( q(cw)
| p(cx)
| ~ q(Z4)
| ~ p(Y4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_4) ).
fof(f3_nnf,plain,
! [Y4,Z4] :
( q(cw)
| p(cx)
| ~ q(Z4)
| ~ p(Y4) ),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [Y4,Z4] :
( q(cw)
| p(cx)
| ~ q(Z4)
| ~ p(Y4) ),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
( q(cw)
| p(cx)
| ~ q(X1)
| ~ p(X0) ),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p91,plain,
( q(cw)
| p(cx)
| ~ q(X0)
| q(cw)
| p(fy5(cx))
| p(cx) ),
inference(resolution,[status(thm)],[p88,c3]) ).
cnf(p95,plain,
( q(cw)
| ~ q(X0)
| q(cw)
| p(fy5(cx))
| p(cx) ),
inference(factoring,[status(thm)],[p91]) ).
cnf(p97,plain,
( ~ q(X0)
| q(cw)
| p(fy5(cx))
| p(cx) ),
inference(factoring,[status(thm)],[p95]) ).
cnf(p100,plain,
( q(cw)
| p(fy5(cx))
| p(cx)
| q(cw)
| p(fy5(cx))
| p(cx) ),
inference(resolution,[status(thm)],[p97,p68]) ).
cnf(p112,plain,
( q(cw)
| p(cx)
| q(cw)
| p(fy5(cx))
| p(cx) ),
inference(factoring,[status(thm)],[p100]) ).
cnf(p120,plain,
( q(cw)
| q(cw)
| p(fy5(cx))
| p(cx) ),
inference(factoring,[status(thm)],[p112]) ).
cnf(p122,plain,
( q(cw)
| p(fy5(cx))
| p(cx) ),
inference(factoring,[status(thm)],[p120]) ).
cnf(f14,negated_conjecture,
( q(fz(W3))
| q(W3)
| q(cw)
| p(cx)
| ~ p(Y2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_15) ).
fof(f14_nnf,plain,
! [Y2,W3] :
( q(fz(W3))
| q(W3)
| q(cw)
| p(cx)
| ~ p(Y2) ),
inference(nnf_transformation,[status(thm)],[f14]) ).
fof(f14_sk,plain,
! [Y2,W3] :
( q(fz(W3))
| q(W3)
| q(cw)
| p(cx)
| ~ p(Y2) ),
inference(skolemisation,[status(esa)],[f14_nnf]) ).
cnf(c14,plain,
( q(fz(X1))
| q(X1)
| q(cw)
| p(cx)
| ~ p(X0) ),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(p37,plain,
( q(fz(cw))
| q(cw)
| p(cx)
| ~ p(X0) ),
inference(factoring,[status(thm)],[c14]) ).
cnf(p126,plain,
( q(fz(cw))
| q(cw)
| p(cx)
| q(cw)
| p(cx) ),
inference(resolution,[status(thm)],[p122,p37]) ).
cnf(p141,plain,
( q(fz(cw))
| q(cw)
| q(cw)
| p(cx) ),
inference(factoring,[status(thm)],[p126]) ).
cnf(p143,plain,
( q(fz(cw))
| q(cw)
| p(cx) ),
inference(factoring,[status(thm)],[p141]) ).
cnf(f12,negated_conjecture,
( q(cw)
| p(X8)
| ~ q(Z4)
| ~ p(fy5(X9))
| ~ p(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_13) ).
fof(f12_nnf,plain,
! [X2,X9,Z4,X8] :
( q(cw)
| p(X8)
| ~ q(Z4)
| ~ p(fy5(X9))
| ~ p(X2) ),
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
! [X2,X9,Z4,X8] :
( q(cw)
| p(X8)
| ~ q(Z4)
| ~ p(fy5(X9))
| ~ p(X2) ),
inference(skolemisation,[status(esa)],[f12_nnf]) ).
cnf(c12,plain,
( q(cw)
| p(X3)
| ~ q(X2)
| ~ p(fy5(X1))
| ~ p(X0) ),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(p36,plain,
( q(cw)
| p(X2)
| ~ q(X1)
| ~ p(fy5(X0)) ),
inference(factoring,[status(thm)],[c12]) ).
cnf(p124,plain,
( q(cw)
| p(X1)
| ~ q(X0)
| q(cw)
| p(cx) ),
inference(resolution,[status(thm)],[p122,p36]) ).
cnf(p131,plain,
( q(cw)
| ~ q(X0)
| q(cw)
| p(cx) ),
inference(factoring,[status(thm)],[p124]) ).
cnf(p138,plain,
( ~ q(X0)
| q(cw)
| p(cx) ),
inference(factoring,[status(thm)],[p131]) ).
cnf(p147,plain,
( q(cw)
| p(cx)
| q(cw)
| p(cx) ),
inference(resolution,[status(thm)],[p143,p138]) ).
cnf(p148,plain,
( q(cw)
| q(cw)
| p(cx) ),
inference(factoring,[status(thm)],[p147]) ).
cnf(p150,plain,
( q(cw)
| p(cx) ),
inference(factoring,[status(thm)],[p148]) ).
cnf(f29,negated_conjecture,
( p(fy(X1))
| p(X1)
| p(cx)
| ~ q(fz(W3))
| ~ q(W3)
| ~ q(cw) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_30) ).
fof(f29_nnf,plain,
! [W3,X1] :
( p(fy(X1))
| p(X1)
| p(cx)
| ~ q(fz(W3))
| ~ q(W3)
| ~ q(cw) ),
inference(nnf_transformation,[status(thm)],[f29]) ).
fof(f29_sk,plain,
! [W3,X1] :
( p(fy(X1))
| p(X1)
| p(cx)
| ~ q(fz(W3))
| ~ q(W3)
| ~ q(cw) ),
inference(skolemisation,[status(esa)],[f29_nnf]) ).
cnf(c29,plain,
( p(fy(X1))
| p(X1)
| p(cx)
| ~ q(fz(X0))
| ~ q(X0)
| ~ q(cw) ),
inference(cnf_transformation,[status(esa)],[f29_sk]) ).
cnf(p50,plain,
( p(fy(X0))
| p(X0)
| p(cx)
| ~ q(fz(cw))
| ~ q(cw) ),
inference(factoring,[status(thm)],[c29]) ).
cnf(p52,plain,
( p(fy(cx))
| p(cx)
| ~ q(fz(cw))
| ~ q(cw) ),
inference(factoring,[status(thm)],[p50]) ).
cnf(p155,plain,
( p(fy(cx))
| p(cx)
| ~ q(fz(cw))
| p(cx) ),
inference(resolution,[status(thm)],[p150,p52]) ).
cnf(p173,plain,
( p(fy(cx))
| ~ q(fz(cw))
| p(cx) ),
inference(factoring,[status(thm)],[p155]) ).
cnf(f18,negated_conjecture,
( q(Z1)
| p(fy(X1))
| p(X1)
| p(cx)
| ~ q(cw) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_19) ).
fof(f18_nnf,plain,
! [X1,Z1] :
( q(Z1)
| p(fy(X1))
| p(X1)
| p(cx)
| ~ q(cw) ),
inference(nnf_transformation,[status(thm)],[f18]) ).
fof(f18_sk,plain,
! [X1,Z1] :
( q(Z1)
| p(fy(X1))
| p(X1)
| p(cx)
| ~ q(cw) ),
inference(skolemisation,[status(esa)],[f18_nnf]) ).
cnf(c18,plain,
( q(X1)
| p(fy(X0))
| p(X0)
| p(cx)
| ~ q(cw) ),
inference(cnf_transformation,[status(esa)],[f18_sk]) ).
cnf(p151,plain,
( q(X1)
| p(fy(X0))
| p(X0)
| p(cx)
| p(cx) ),
inference(resolution,[status(thm)],[p150,c18]) ).
cnf(p157,plain,
( q(X1)
| p(fy(X0))
| p(X0)
| p(cx) ),
inference(factoring,[status(thm)],[p151]) ).
cnf(p158,plain,
( q(X0)
| p(fy(cx))
| p(cx) ),
inference(factoring,[status(thm)],[p157]) ).
cnf(p175,plain,
( p(fy(cx))
| p(cx)
| p(fy(cx))
| p(cx) ),
inference(resolution,[status(thm)],[p173,p158]) ).
cnf(p178,plain,
( p(cx)
| p(fy(cx))
| p(cx) ),
inference(factoring,[status(thm)],[p175]) ).
cnf(p179,plain,
( p(fy(cx))
| p(cx) ),
inference(factoring,[status(thm)],[p178]) ).
cnf(f15,negated_conjecture,
( p(cx)
| ~ q(fz5(W9))
| ~ q(W9)
| ~ q(cw)
| ~ p(Y4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_16) ).
fof(f15_nnf,plain,
! [Y4,W9] :
( p(cx)
| ~ q(fz5(W9))
| ~ q(W9)
| ~ q(cw)
| ~ p(Y4) ),
inference(nnf_transformation,[status(thm)],[f15]) ).
fof(f15_sk,plain,
! [Y4,W9] :
( p(cx)
| ~ q(fz5(W9))
| ~ q(W9)
| ~ q(cw)
| ~ p(Y4) ),
inference(skolemisation,[status(esa)],[f15_nnf]) ).
cnf(c15,plain,
( p(cx)
| ~ q(fz5(X1))
| ~ q(X1)
| ~ q(cw)
| ~ p(X0) ),
inference(cnf_transformation,[status(esa)],[f15_sk]) ).
cnf(p38,plain,
( p(cx)
| ~ q(fz5(cw))
| ~ q(cw)
| ~ p(X0) ),
inference(factoring,[status(thm)],[c15]) ).
cnf(p182,plain,
( p(cx)
| ~ q(fz5(cw))
| ~ q(cw)
| p(cx) ),
inference(resolution,[status(thm)],[p179,p38]) ).
cnf(p193,plain,
( ~ q(fz5(cw))
| ~ q(cw)
| p(cx) ),
inference(factoring,[status(thm)],[p182]) ).
cnf(f2,negated_conjecture,
( q(Z3)
| p(cx)
| ~ q(cw)
| ~ p(Y4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_3) ).
fof(f2_nnf,plain,
! [Y4,Z3] :
( q(Z3)
| p(cx)
| ~ q(cw)
| ~ p(Y4) ),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [Y4,Z3] :
( q(Z3)
| p(cx)
| ~ q(cw)
| ~ p(Y4) ),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
( q(X1)
| p(cx)
| ~ q(cw)
| ~ p(X0) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p180,plain,
( q(X0)
| p(cx)
| ~ q(cw)
| p(cx) ),
inference(resolution,[status(thm)],[p179,c2]) ).
cnf(p189,plain,
( q(X0)
| ~ q(cw)
| p(cx) ),
inference(factoring,[status(thm)],[p180]) ).
cnf(p191,plain,
( p(cx)
| q(X0)
| p(cx) ),
inference(resolution,[status(thm)],[p189,p150]) ).
cnf(p192,plain,
( q(X0)
| p(cx) ),
inference(factoring,[status(thm)],[p191]) ).
cnf(p195,plain,
( p(cx)
| ~ q(fz5(cw))
| p(cx) ),
inference(resolution,[status(thm)],[p193,p192]) ).
cnf(p196,plain,
( ~ q(fz5(cw))
| p(cx) ),
inference(factoring,[status(thm)],[p195]) ).
cnf(p197,plain,
( p(cx)
| p(cx) ),
inference(resolution,[status(thm)],[p196,p192]) ).
cnf(p198,plain,
p(cx),
inference(factoring,[status(thm)],[p197]) ).
cnf(f9,negated_conjecture,
( q(fz(W3))
| q(W3)
| q(cw)
| p(Y1)
| ~ p(cx) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_10) ).
fof(f9_nnf,plain,
! [Y1,W3] :
( q(fz(W3))
| q(W3)
| q(cw)
| p(Y1)
| ~ p(cx) ),
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
! [Y1,W3] :
( q(fz(W3))
| q(W3)
| q(cw)
| p(Y1)
| ~ p(cx) ),
inference(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c9,plain,
( q(fz(X1))
| q(X1)
| q(cw)
| p(X0)
| ~ p(cx) ),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(p35,plain,
( q(fz(cw))
| q(cw)
| p(X0)
| ~ p(cx) ),
inference(factoring,[status(thm)],[c9]) ).
cnf(p208,plain,
( q(fz(cw))
| q(cw)
| p(X0) ),
inference(resolution,[status(thm)],[p198,p35]) ).
cnf(f1,negated_conjecture,
( q(cw)
| p(Y3)
| ~ q(Z4)
| ~ p(cx) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_2) ).
fof(f1_nnf,plain,
! [Z4,Y3] :
( q(cw)
| p(Y3)
| ~ q(Z4)
| ~ p(cx) ),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [Z4,Y3] :
( q(cw)
| p(Y3)
| ~ q(Z4)
| ~ p(cx) ),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
( q(cw)
| p(X1)
| ~ q(X0)
| ~ p(cx) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p200,plain,
( q(cw)
| p(X1)
| ~ q(X0) ),
inference(resolution,[status(thm)],[p198,c1]) ).
cnf(p216,plain,
( q(cw)
| p(X1)
| q(cw)
| p(X0) ),
inference(resolution,[status(thm)],[p208,p200]) ).
cnf(p219,plain,
( q(cw)
| q(cw)
| p(X0) ),
inference(factoring,[status(thm)],[p216]) ).
cnf(p223,plain,
( q(cw)
| p(X0) ),
inference(factoring,[status(thm)],[p219]) ).
cnf(f6,negated_conjecture,
( p(Y3)
| ~ q(fz5(W9))
| ~ q(W9)
| ~ q(cw)
| ~ p(cx) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_7) ).
fof(f6_nnf,plain,
! [W9,Y3] :
( p(Y3)
| ~ q(fz5(W9))
| ~ q(W9)
| ~ q(cw)
| ~ p(cx) ),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [W9,Y3] :
( p(Y3)
| ~ q(fz5(W9))
| ~ q(W9)
| ~ q(cw)
| ~ p(cx) ),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c6,plain,
( p(X1)
| ~ q(fz5(X0))
| ~ q(X0)
| ~ q(cw)
| ~ p(cx) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(p34,plain,
( p(X0)
| ~ q(fz5(cw))
| ~ q(cw)
| ~ p(cx) ),
inference(factoring,[status(thm)],[c6]) ).
cnf(p205,plain,
( p(X0)
| ~ q(fz5(cw))
| ~ q(cw) ),
inference(resolution,[status(thm)],[p198,p34]) ).
cnf(p225,plain,
( p(X1)
| ~ q(fz5(cw))
| p(X0) ),
inference(resolution,[status(thm)],[p223,p205]) ).
cnf(p240,plain,
( ~ q(fz5(cw))
| p(X0) ),
inference(factoring,[status(thm)],[p225]) ).
cnf(f0,negated_conjecture,
( q(Z3)
| p(Y3)
| ~ q(cw)
| ~ p(cx) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_1) ).
fof(f0_nnf,plain,
! [Y3,Z3] :
( q(Z3)
| p(Y3)
| ~ q(cw)
| ~ p(cx) ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [Y3,Z3] :
( q(Z3)
| p(Y3)
| ~ q(cw)
| ~ p(cx) ),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
( q(X1)
| p(X0)
| ~ q(cw)
| ~ p(cx) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p199,plain,
( q(X1)
| p(X0)
| ~ q(cw) ),
inference(resolution,[status(thm)],[p198,c0]) ).
cnf(p224,plain,
( q(X2)
| p(X1)
| p(X0) ),
inference(resolution,[status(thm)],[p223,p199]) ).
cnf(p228,plain,
( q(X1)
| p(X0) ),
inference(factoring,[status(thm)],[p224]) ).
cnf(p241,plain,
( p(X1)
| p(X0) ),
inference(resolution,[status(thm)],[p240,p228]) ).
cnf(p242,plain,
p(X0),
inference(factoring,[status(thm)],[p241]) ).
cnf(f21,negated_conjecture,
( q(fz(W3))
| q(W3)
| q(cw)
| ~ p(fy(X1))
| ~ p(X1)
| ~ p(cx) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_22) ).
fof(f21_nnf,plain,
! [X1,W3] :
( q(fz(W3))
| q(W3)
| q(cw)
| ~ p(fy(X1))
| ~ p(X1)
| ~ p(cx) ),
inference(nnf_transformation,[status(thm)],[f21]) ).
fof(f21_sk,plain,
! [X1,W3] :
( q(fz(W3))
| q(W3)
| q(cw)
| ~ p(fy(X1))
| ~ p(X1)
| ~ p(cx) ),
inference(skolemisation,[status(esa)],[f21_nnf]) ).
cnf(c21,plain,
( q(fz(X1))
| q(X1)
| q(cw)
| ~ p(fy(X0))
| ~ p(X0)
| ~ p(cx) ),
inference(cnf_transformation,[status(esa)],[f21_sk]) ).
cnf(p42,plain,
( q(fz(X0))
| q(X0)
| q(cw)
| ~ p(fy(cx))
| ~ p(cx) ),
inference(factoring,[status(thm)],[c21]) ).
cnf(p44,plain,
( q(fz(cw))
| q(cw)
| ~ p(fy(cx))
| ~ p(cx) ),
inference(factoring,[status(thm)],[p42]) ).
cnf(p211,plain,
( q(fz(cw))
| q(cw)
| ~ p(fy(cx)) ),
inference(resolution,[status(thm)],[p198,p44]) ).
cnf(p243,plain,
( q(fz(cw))
| q(cw) ),
inference(resolution,[status(thm)],[p242,p211]) ).
cnf(f5,negated_conjecture,
( q(cw)
| ~ q(Z4)
| ~ p(fy5(X7))
| ~ p(X7)
| ~ p(cx) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_6) ).
fof(f5_nnf,plain,
! [X7,Z4] :
( q(cw)
| ~ q(Z4)
| ~ p(fy5(X7))
| ~ p(X7)
| ~ p(cx) ),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [X7,Z4] :
( q(cw)
| ~ q(Z4)
| ~ p(fy5(X7))
| ~ p(X7)
| ~ p(cx) ),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c5,plain,
( q(cw)
| ~ q(X1)
| ~ p(fy5(X0))
| ~ p(X0)
| ~ p(cx) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p202,plain,
( q(cw)
| ~ q(X1)
| ~ p(fy5(X0))
| ~ p(X0) ),
inference(resolution,[status(thm)],[p198,c5]) ).
cnf(p221,plain,
( q(cw)
| ~ q(X0)
| ~ p(fy5(cx)) ),
inference(resolution,[status(thm)],[p202,p198]) ).
cnf(p236,plain,
( q(X1)
| q(cw)
| ~ q(X0) ),
inference(resolution,[status(thm)],[p221,p228]) ).
cnf(p237,plain,
( q(cw)
| ~ q(X0) ),
inference(factoring,[status(thm)],[p236]) ).
cnf(p247,plain,
( q(cw)
| q(cw) ),
inference(resolution,[status(thm)],[p243,p237]) ).
cnf(p248,plain,
q(cw),
inference(factoring,[status(thm)],[p247]) ).
cnf(f4,negated_conjecture,
( q(Z3)
| ~ q(cw)
| ~ p(fy5(X7))
| ~ p(X7)
| ~ p(cx) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_5) ).
fof(f4_nnf,plain,
! [X7,Z3] :
( q(Z3)
| ~ q(cw)
| ~ p(fy5(X7))
| ~ p(X7)
| ~ p(cx) ),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [X7,Z3] :
( q(Z3)
| ~ q(cw)
| ~ p(fy5(X7))
| ~ p(X7)
| ~ p(cx) ),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c4,plain,
( q(X1)
| ~ q(cw)
| ~ p(fy5(X0))
| ~ p(X0)
| ~ p(cx) ),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p201,plain,
( q(X1)
| ~ q(cw)
| ~ p(fy5(X0))
| ~ p(X0) ),
inference(resolution,[status(thm)],[p198,c4]) ).
cnf(p217,plain,
( q(X0)
| ~ q(cw)
| ~ p(fy5(cx)) ),
inference(resolution,[status(thm)],[p201,p198]) ).
cnf(p230,plain,
( q(X1)
| ~ q(cw)
| q(X0) ),
inference(resolution,[status(thm)],[p228,p217]) ).
cnf(p235,plain,
( ~ q(cw)
| q(X0) ),
inference(factoring,[status(thm)],[p230]) ).
cnf(p249,plain,
q(X0),
inference(resolution,[status(thm)],[p248,p235]) ).
cnf(f22,negated_conjecture,
( ~ q(fz5(W9))
| ~ q(W9)
| ~ q(cw)
| ~ p(fy5(X7))
| ~ p(X7)
| ~ p(cx) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_23) ).
fof(f22_nnf,plain,
! [X7,W9] :
( ~ q(fz5(W9))
| ~ q(W9)
| ~ q(cw)
| ~ p(fy5(X7))
| ~ p(X7)
| ~ p(cx) ),
inference(nnf_transformation,[status(thm)],[f22]) ).
fof(f22_sk,plain,
! [X7,W9] :
( ~ q(fz5(W9))
| ~ q(W9)
| ~ q(cw)
| ~ p(fy5(X7))
| ~ p(X7)
| ~ p(cx) ),
inference(skolemisation,[status(esa)],[f22_nnf]) ).
cnf(c22,plain,
( ~ q(fz5(X1))
| ~ q(X1)
| ~ q(cw)
| ~ p(fy5(X0))
| ~ p(X0)
| ~ p(cx) ),
inference(cnf_transformation,[status(esa)],[f22_sk]) ).
cnf(p45,plain,
( ~ q(fz5(X0))
| ~ q(X0)
| ~ q(cw)
| ~ p(fy5(cx))
| ~ p(cx) ),
inference(factoring,[status(thm)],[c22]) ).
cnf(p47,plain,
( ~ q(fz5(cw))
| ~ q(cw)
| ~ p(fy5(cx))
| ~ p(cx) ),
inference(factoring,[status(thm)],[p45]) ).
cnf(p214,plain,
( ~ q(fz5(cw))
| ~ q(cw)
| ~ p(fy5(cx)) ),
inference(resolution,[status(thm)],[p198,p47]) ).
cnf(p244,plain,
( ~ q(fz5(cw))
| ~ q(cw) ),
inference(resolution,[status(thm)],[p242,p214]) ).
cnf(p250,plain,
~ q(fz5(cw)),
inference(resolution,[status(thm)],[p249,p244]) ).
cnf(p251,plain,
$false,
inference(resolution,[status(thm)],[p250,p249]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN036-4 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/10.36 % Computer : n013.cluster.edu
% 0.10/10.36 % Model : x86_64 x86_64
% 0.10/10.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/10.36 % Memory : 8046.5625MB
% 0.10/10.36 % OS : Linux 6.8.0-71-generic
% 0.10/10.37 % CPULimit : 300
% 0.10/10.37 % WCLimit : 300
% 0.10/10.37 % DateTime : Thu Sep 24 23:54:01 UTC 2026
% 0.10/10.37 % CPUTime :
% 0.10/10.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.14/10.81 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.14/10.81 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------