%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SYN094-1.005 : TPTP v9.3.1. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n008.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:48 PM UTC 2026
% Result : Unsatisfiable 6.28s 6.52s
% Output : Proof 6.28s
% Verified :
% SZS Type : Refutation
% Derivation depth : 40
% Number of leaves : 32
% Syntax : Number of formulae : 185 ( 21 unt; 0 def)
% Number of atoms : 461 ( 0 equ)
% Maximal formula atoms : 4 ( 2 avg)
% Number of connectives : 457 ( 181 ~; 276 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 3 avg)
% Maximal term depth : 0 ( 0 avg)
% Number of predicates : 32 ( 31 usr; 32 prp; 0-0 aty)
% Number of functors : 0 ( 0 usr; 0 con; --- aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f58,axiom,
( ~ q_8
| ~ p_7
| q_6
| u_30 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u_s3_type12_13) ).
fof(f58_nnf,plain,
( ~ q_8
| ~ p_7
| q_6
| u_30 ),
inference(nnf_transformation,[status(thm)],[f58]) ).
fof(f58_sk,plain,
( ~ q_8
| ~ p_7
| q_6
| u_30 ),
inference(skolemisation,[status(esa)],[f58_nnf]) ).
cnf(c58,plain,
( ~ q_8
| ~ p_7
| q_6
| u_30 ),
inference(cnf_transformation,[status(esa)],[f58_sk]) ).
cnf(f30,axiom,
( ~ p_9
| ~ p_8
| p_7
| u_16 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u_s3_type11_15) ).
fof(f30_nnf,plain,
( ~ p_9
| ~ p_8
| p_7
| u_16 ),
inference(nnf_transformation,[status(thm)],[f30]) ).
fof(f30_sk,plain,
( ~ p_9
| ~ p_8
| p_7
| u_16 ),
inference(skolemisation,[status(esa)],[f30_nnf]) ).
cnf(c30,plain,
( ~ p_9
| ~ p_8
| p_7
| u_16 ),
inference(cnf_transformation,[status(esa)],[f30_sk]) ).
cnf(f75,axiom,
( ~ u_38
| p_8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u_38_t3_1) ).
fof(f75_nnf,plain,
( ~ u_38
| p_8 ),
inference(nnf_transformation,[status(thm)],[f75]) ).
fof(f75_sk,plain,
( ~ u_38
| p_8 ),
inference(skolemisation,[status(esa)],[f75_nnf]) ).
cnf(c75,plain,
( ~ u_38
| p_8 ),
inference(cnf_transformation,[status(esa)],[f75_sk]) ).
cnf(f74,axiom,
( p_8
| u_38 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u_t3_1) ).
fof(f74_nnf,plain,
( p_8
| u_38 ),
inference(nnf_transformation,[status(thm)],[f74]) ).
fof(f74_sk,plain,
( p_8
| u_38 ),
inference(skolemisation,[status(esa)],[f74_nnf]) ).
cnf(c74,plain,
( p_8
| u_38 ),
inference(cnf_transformation,[status(esa)],[f74_sk]) ).
cnf(p82,plain,
( p_8
| p_8 ),
inference(resolution,[status(thm)],[c75,c74]) ).
cnf(p86,plain,
p_8,
inference(factoring,[status(thm)],[p82]) ).
cnf(p90,plain,
( ~ p_9
| p_7
| u_16 ),
inference(resolution,[status(thm)],[c30,p86]) ).
cnf(f77,axiom,
( ~ u_39
| p_9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u_39_t3_2) ).
fof(f77_nnf,plain,
( ~ u_39
| p_9 ),
inference(nnf_transformation,[status(thm)],[f77]) ).
fof(f77_sk,plain,
( ~ u_39
| p_9 ),
inference(skolemisation,[status(esa)],[f77_nnf]) ).
cnf(c77,plain,
( ~ u_39
| p_9 ),
inference(cnf_transformation,[status(esa)],[f77_sk]) ).
cnf(f76,axiom,
( p_9
| u_39 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u_t3_2) ).
fof(f76_nnf,plain,
( p_9
| u_39 ),
inference(nnf_transformation,[status(thm)],[f76]) ).
fof(f76_sk,plain,
( p_9
| u_39 ),
inference(skolemisation,[status(esa)],[f76_nnf]) ).
cnf(c76,plain,
( p_9
| u_39 ),
inference(cnf_transformation,[status(esa)],[f76_sk]) ).
cnf(p83,plain,
( p_9
| p_9 ),
inference(resolution,[status(thm)],[c77,c76]) ).
cnf(p87,plain,
p_9,
inference(factoring,[status(thm)],[p83]) ).
cnf(p91,plain,
( p_7
| u_16 ),
inference(resolution,[status(thm)],[p90,p87]) ).
cnf(f31,axiom,
( ~ u_16
| p_7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u_16_s3_type11_15) ).
fof(f31_nnf,plain,
( ~ u_16
| p_7 ),
inference(nnf_transformation,[status(thm)],[f31]) ).
fof(f31_sk,plain,
( ~ u_16
| p_7 ),
inference(skolemisation,[status(esa)],[f31_nnf]) ).
cnf(c31,plain,
( ~ u_16
| p_7 ),
inference(cnf_transformation,[status(esa)],[f31_sk]) ).
cnf(p92,plain,
( p_7
| p_7 ),
inference(resolution,[status(thm)],[p91,c31]) ).
cnf(p93,plain,
p_7,
inference(factoring,[status(thm)],[p92]) ).
cnf(p130,plain,
( ~ q_8
| q_6
| u_30 ),
inference(resolution,[status(thm)],[c58,p93]) ).
cnf(f79,axiom,
( ~ u_40
| q_8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u_40_t3_3) ).
fof(f79_nnf,plain,
( ~ u_40
| q_8 ),
inference(nnf_transformation,[status(thm)],[f79]) ).
fof(f79_sk,plain,
( ~ u_40
| q_8 ),
inference(skolemisation,[status(esa)],[f79_nnf]) ).
cnf(c79,plain,
( ~ u_40
| q_8 ),
inference(cnf_transformation,[status(esa)],[f79_sk]) ).
cnf(f78,axiom,
( q_8
| u_40 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u_t3_3) ).
fof(f78_nnf,plain,
( q_8
| u_40 ),
inference(nnf_transformation,[status(thm)],[f78]) ).
fof(f78_sk,plain,
( q_8
| u_40 ),
inference(skolemisation,[status(esa)],[f78_nnf]) ).
cnf(c78,plain,
( q_8
| u_40 ),
inference(cnf_transformation,[status(esa)],[f78_sk]) ).
cnf(p84,plain,
( q_8
| q_8 ),
inference(resolution,[status(thm)],[c79,c78]) ).
cnf(p88,plain,
q_8,
inference(factoring,[status(thm)],[p84]) ).
cnf(p131,plain,
( q_6
| u_30 ),
inference(resolution,[status(thm)],[p130,p88]) ).
cnf(f59,axiom,
( ~ u_30
| q_6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u_30_s3_type12_13) ).
fof(f59_nnf,plain,
( ~ u_30
| q_6 ),
inference(nnf_transformation,[status(thm)],[f59]) ).
fof(f59_sk,plain,
( ~ u_30
| q_6 ),
inference(skolemisation,[status(esa)],[f59_nnf]) ).
cnf(c59,plain,
( ~ u_30
| q_6 ),
inference(cnf_transformation,[status(esa)],[f59_sk]) ).
cnf(p132,plain,
( q_6
| q_6 ),
inference(resolution,[status(thm)],[p131,c59]) ).
cnf(p133,plain,
q_6,
inference(factoring,[status(thm)],[p132]) ).
cnf(f50,axiom,
( ~ q_6
| ~ p_5
| q_4
| u_26 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u_s3_type12_9) ).
fof(f50_nnf,plain,
( ~ q_6
| ~ p_5
| q_4
| u_26 ),
inference(nnf_transformation,[status(thm)],[f50]) ).
fof(f50_sk,plain,
( ~ q_6
| ~ p_5
| q_4
| u_26 ),
inference(skolemisation,[status(esa)],[f50_nnf]) ).
cnf(c50,plain,
( ~ q_6
| ~ p_5
| q_4
| u_26 ),
inference(cnf_transformation,[status(esa)],[f50_sk]) ).
cnf(f26,axiom,
( ~ p_8
| ~ p_7
| p_6
| u_14 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u_s3_type11_13) ).
fof(f26_nnf,plain,
( ~ p_8
| ~ p_7
| p_6
| u_14 ),
inference(nnf_transformation,[status(thm)],[f26]) ).
fof(f26_sk,plain,
( ~ p_8
| ~ p_7
| p_6
| u_14 ),
inference(skolemisation,[status(esa)],[f26_nnf]) ).
cnf(c26,plain,
( ~ p_8
| ~ p_7
| p_6
| u_14 ),
inference(cnf_transformation,[status(esa)],[f26_sk]) ).
cnf(p94,plain,
( ~ p_8
| p_6
| u_14 ),
inference(resolution,[status(thm)],[p93,c26]) ).
cnf(p95,plain,
( p_6
| u_14 ),
inference(resolution,[status(thm)],[p94,p86]) ).
cnf(f27,axiom,
( ~ u_14
| p_6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u_14_s3_type11_13) ).
fof(f27_nnf,plain,
( ~ u_14
| p_6 ),
inference(nnf_transformation,[status(thm)],[f27]) ).
fof(f27_sk,plain,
( ~ u_14
| p_6 ),
inference(skolemisation,[status(esa)],[f27_nnf]) ).
cnf(c27,plain,
( ~ u_14
| p_6 ),
inference(cnf_transformation,[status(esa)],[f27_sk]) ).
cnf(p96,plain,
( p_6
| p_6 ),
inference(resolution,[status(thm)],[p95,c27]) ).
cnf(p97,plain,
p_6,
inference(factoring,[status(thm)],[p96]) ).
cnf(f22,axiom,
( ~ p_7
| ~ p_6
| p_5
| u_12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u_s3_type11_11) ).
fof(f22_nnf,plain,
( ~ p_7
| ~ p_6
| p_5
| u_12 ),
inference(nnf_transformation,[status(thm)],[f22]) ).
fof(f22_sk,plain,
( ~ p_7
| ~ p_6
| p_5
| u_12 ),
inference(skolemisation,[status(esa)],[f22_nnf]) ).
cnf(c22,plain,
( ~ p_7
| ~ p_6
| p_5
| u_12 ),
inference(cnf_transformation,[status(esa)],[f22_sk]) ).
cnf(p98,plain,
( ~ p_7
| p_5
| u_12 ),
inference(resolution,[status(thm)],[p97,c22]) ).
cnf(p99,plain,
( p_5
| u_12 ),
inference(resolution,[status(thm)],[p98,p93]) ).
cnf(f23,axiom,
( ~ u_12
| p_5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u_12_s3_type11_11) ).
fof(f23_nnf,plain,
( ~ u_12
| p_5 ),
inference(nnf_transformation,[status(thm)],[f23]) ).
fof(f23_sk,plain,
( ~ u_12
| p_5 ),
inference(skolemisation,[status(esa)],[f23_nnf]) ).
cnf(c23,plain,
( ~ u_12
| p_5 ),
inference(cnf_transformation,[status(esa)],[f23_sk]) ).
cnf(p100,plain,
( p_5
| p_5 ),
inference(resolution,[status(thm)],[p99,c23]) ).
cnf(p101,plain,
p_5,
inference(factoring,[status(thm)],[p100]) ).
cnf(p127,plain,
( ~ q_6
| q_4
| u_26 ),
inference(resolution,[status(thm)],[c50,p101]) ).
cnf(p134,plain,
( q_4
| u_26 ),
inference(resolution,[status(thm)],[p133,p127]) ).
cnf(f51,axiom,
( ~ u_26
| q_4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u_26_s3_type12_9) ).
fof(f51_nnf,plain,
( ~ u_26
| q_4 ),
inference(nnf_transformation,[status(thm)],[f51]) ).
fof(f51_sk,plain,
( ~ u_26
| q_4 ),
inference(skolemisation,[status(esa)],[f51_nnf]) ).
cnf(c51,plain,
( ~ u_26
| q_4 ),
inference(cnf_transformation,[status(esa)],[f51_sk]) ).
cnf(p137,plain,
( q_4
| q_4 ),
inference(resolution,[status(thm)],[p134,c51]) ).
cnf(p138,plain,
q_4,
inference(factoring,[status(thm)],[p137]) ).
cnf(f18,axiom,
( ~ p_6
| ~ p_5
| p_4
| u_10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u_s3_type11_9) ).
fof(f18_nnf,plain,
( ~ p_6
| ~ p_5
| p_4
| u_10 ),
inference(nnf_transformation,[status(thm)],[f18]) ).
fof(f18_sk,plain,
( ~ p_6
| ~ p_5
| p_4
| u_10 ),
inference(skolemisation,[status(esa)],[f18_nnf]) ).
cnf(c18,plain,
( ~ p_6
| ~ p_5
| p_4
| u_10 ),
inference(cnf_transformation,[status(esa)],[f18_sk]) ).
cnf(p102,plain,
( ~ p_6
| p_4
| u_10 ),
inference(resolution,[status(thm)],[p101,c18]) ).
cnf(p104,plain,
( p_4
| u_10 ),
inference(resolution,[status(thm)],[p102,p97]) ).
cnf(f19,axiom,
( ~ u_10
| p_4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u_10_s3_type11_9) ).
fof(f19_nnf,plain,
( ~ u_10
| p_4 ),
inference(nnf_transformation,[status(thm)],[f19]) ).
fof(f19_sk,plain,
( ~ u_10
| p_4 ),
inference(skolemisation,[status(esa)],[f19_nnf]) ).
cnf(c19,plain,
( ~ u_10
| p_4 ),
inference(cnf_transformation,[status(esa)],[f19_sk]) ).
cnf(p105,plain,
( p_4
| p_4 ),
inference(resolution,[status(thm)],[p104,c19]) ).
cnf(p106,plain,
p_4,
inference(factoring,[status(thm)],[p105]) ).
cnf(f14,axiom,
( ~ p_5
| ~ p_4
| p_3
| u_8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u_s3_type11_7) ).
fof(f14_nnf,plain,
( ~ p_5
| ~ p_4
| p_3
| u_8 ),
inference(nnf_transformation,[status(thm)],[f14]) ).
fof(f14_sk,plain,
( ~ p_5
| ~ p_4
| p_3
| u_8 ),
inference(skolemisation,[status(esa)],[f14_nnf]) ).
cnf(c14,plain,
( ~ p_5
| ~ p_4
| p_3
| u_8 ),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(p107,plain,
( ~ p_5
| p_3
| u_8 ),
inference(resolution,[status(thm)],[p106,c14]) ).
cnf(p108,plain,
( p_3
| u_8 ),
inference(resolution,[status(thm)],[p107,p101]) ).
cnf(f15,axiom,
( ~ u_8
| p_3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u_8_s3_type11_7) ).
fof(f15_nnf,plain,
( ~ u_8
| p_3 ),
inference(nnf_transformation,[status(thm)],[f15]) ).
fof(f15_sk,plain,
( ~ u_8
| p_3 ),
inference(skolemisation,[status(esa)],[f15_nnf]) ).
cnf(c15,plain,
( ~ u_8
| p_3 ),
inference(cnf_transformation,[status(esa)],[f15_sk]) ).
cnf(p109,plain,
( p_3
| p_3 ),
inference(resolution,[status(thm)],[p108,c15]) ).
cnf(p110,plain,
p_3,
inference(factoring,[status(thm)],[p109]) ).
cnf(f42,axiom,
( ~ q_4
| ~ p_3
| q_2
| u_22 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u_s3_type12_5) ).
fof(f42_nnf,plain,
( ~ q_4
| ~ p_3
| q_2
| u_22 ),
inference(nnf_transformation,[status(thm)],[f42]) ).
fof(f42_sk,plain,
( ~ q_4
| ~ p_3
| q_2
| u_22 ),
inference(skolemisation,[status(esa)],[f42_nnf]) ).
cnf(c42,plain,
( ~ q_4
| ~ p_3
| q_2
| u_22 ),
inference(cnf_transformation,[status(esa)],[f42_sk]) ).
cnf(p112,plain,
( ~ q_4
| q_2
| u_22 ),
inference(resolution,[status(thm)],[p110,c42]) ).
cnf(p139,plain,
( q_2
| u_22 ),
inference(resolution,[status(thm)],[p138,p112]) ).
cnf(f43,axiom,
( ~ u_22
| q_2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u_22_s3_type12_5) ).
fof(f43_nnf,plain,
( ~ u_22
| q_2 ),
inference(nnf_transformation,[status(thm)],[f43]) ).
fof(f43_sk,plain,
( ~ u_22
| q_2 ),
inference(skolemisation,[status(esa)],[f43_nnf]) ).
cnf(c43,plain,
( ~ u_22
| q_2 ),
inference(cnf_transformation,[status(esa)],[f43_sk]) ).
cnf(p141,plain,
( q_2
| q_2 ),
inference(resolution,[status(thm)],[p139,c43]) ).
cnf(p143,plain,
q_2,
inference(factoring,[status(thm)],[p141]) ).
cnf(f10,axiom,
( ~ p_4
| ~ p_3
| p_2
| u_6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u_s3_type11_5) ).
fof(f10_nnf,plain,
( ~ p_4
| ~ p_3
| p_2
| u_6 ),
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
( ~ p_4
| ~ p_3
| p_2
| u_6 ),
inference(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c10,plain,
( ~ p_4
| ~ p_3
| p_2
| u_6 ),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(p111,plain,
( ~ p_4
| p_2
| u_6 ),
inference(resolution,[status(thm)],[p110,c10]) ).
cnf(p113,plain,
( p_2
| u_6 ),
inference(resolution,[status(thm)],[p111,p106]) ).
cnf(f11,axiom,
( ~ u_6
| p_2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u_6_s3_type11_5) ).
fof(f11_nnf,plain,
( ~ u_6
| p_2 ),
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
( ~ u_6
| p_2 ),
inference(skolemisation,[status(esa)],[f11_nnf]) ).
cnf(c11,plain,
( ~ u_6
| p_2 ),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(p114,plain,
( p_2
| p_2 ),
inference(resolution,[status(thm)],[p113,c11]) ).
cnf(p115,plain,
p_2,
inference(factoring,[status(thm)],[p114]) ).
cnf(f6,axiom,
( ~ p_3
| ~ p_2
| p_1
| u_4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u_s3_type11_3) ).
fof(f6_nnf,plain,
( ~ p_3
| ~ p_2
| p_1
| u_4 ),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
( ~ p_3
| ~ p_2
| p_1
| u_4 ),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c6,plain,
( ~ p_3
| ~ p_2
| p_1
| u_4 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(p116,plain,
( ~ p_3
| p_1
| u_4 ),
inference(resolution,[status(thm)],[p115,c6]) ).
cnf(p118,plain,
( p_1
| u_4 ),
inference(resolution,[status(thm)],[p116,p110]) ).
cnf(f7,axiom,
( ~ u_4
| p_1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u_4_s3_type11_3) ).
fof(f7_nnf,plain,
( ~ u_4
| p_1 ),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
( ~ u_4
| p_1 ),
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c7,plain,
( ~ u_4
| p_1 ),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(p120,plain,
( p_1
| p_1 ),
inference(resolution,[status(thm)],[p118,c7]) ).
cnf(p121,plain,
p_1,
inference(factoring,[status(thm)],[p120]) ).
cnf(f34,axiom,
( ~ q_2
| ~ p_1
| q_0
| u_18 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u_s3_type12_1) ).
fof(f34_nnf,plain,
( ~ q_2
| ~ p_1
| q_0
| u_18 ),
inference(nnf_transformation,[status(thm)],[f34]) ).
fof(f34_sk,plain,
( ~ q_2
| ~ p_1
| q_0
| u_18 ),
inference(skolemisation,[status(esa)],[f34_nnf]) ).
cnf(c34,plain,
( ~ q_2
| ~ p_1
| q_0
| u_18 ),
inference(cnf_transformation,[status(esa)],[f34_sk]) ).
cnf(p123,plain,
( ~ q_2
| q_0
| u_18 ),
inference(resolution,[status(thm)],[p121,c34]) ).
cnf(p145,plain,
( q_0
| u_18 ),
inference(resolution,[status(thm)],[p143,p123]) ).
cnf(f35,axiom,
( ~ u_18
| q_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u_18_s3_type12_1) ).
fof(f35_nnf,plain,
( ~ u_18
| q_0 ),
inference(nnf_transformation,[status(thm)],[f35]) ).
fof(f35_sk,plain,
( ~ u_18
| q_0 ),
inference(skolemisation,[status(esa)],[f35_nnf]) ).
cnf(c35,plain,
( ~ u_18
| q_0 ),
inference(cnf_transformation,[status(esa)],[f35_sk]) ).
cnf(p146,plain,
( q_0
| q_0 ),
inference(resolution,[status(thm)],[p145,c35]) ).
cnf(p147,plain,
q_0,
inference(factoring,[status(thm)],[p146]) ).
cnf(f2,axiom,
( ~ p_2
| ~ p_1
| p_0
| u_2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u_s3_type11_1) ).
fof(f2_nnf,plain,
( ~ p_2
| ~ p_1
| p_0
| u_2 ),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
( ~ p_2
| ~ p_1
| p_0
| u_2 ),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
( ~ p_2
| ~ p_1
| p_0
| u_2 ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p122,plain,
( ~ p_2
| p_0
| u_2 ),
inference(resolution,[status(thm)],[p121,c2]) ).
cnf(p124,plain,
( p_0
| u_2 ),
inference(resolution,[status(thm)],[p122,p115]) ).
cnf(f3,axiom,
( ~ u_2
| p_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u_2_s3_type11_1) ).
fof(f3_nnf,plain,
( ~ u_2
| p_0 ),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
( ~ u_2
| p_0 ),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
( ~ u_2
| p_0 ),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p125,plain,
( p_0
| p_0 ),
inference(resolution,[status(thm)],[p124,c3]) ).
cnf(p126,plain,
p_0,
inference(factoring,[status(thm)],[p125]) ).
cnf(f0,negated_conjecture,
( ~ q_0
| ~ p_0
| u_1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u_s3_goal_1) ).
fof(f0_nnf,plain,
( ~ q_0
| ~ p_0
| u_1 ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
( ~ q_0
| ~ p_0
| u_1 ),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
( ~ q_0
| ~ p_0
| u_1 ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p128,plain,
( ~ q_0
| u_1 ),
inference(resolution,[status(thm)],[p126,c0]) ).
cnf(p149,plain,
u_1,
inference(resolution,[status(thm)],[p147,p128]) ).
cnf(f1,axiom,
~ u_1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u_1_s3_goal_1) ).
fof(f1_nnf,plain,
~ u_1,
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
~ u_1,
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
~ u_1,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p150,plain,
$false,
inference(resolution,[status(thm)],[p149,c1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN094-1.005 : TPTP v9.3.1. Bugfixed v1.2.1.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.11/5.38 % Computer : n008.cluster.edu
% 0.11/5.38 % Model : x86_64 x86_64
% 0.11/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.38 % Memory : 8046.5625MB
% 0.11/5.38 % OS : Linux 6.8.0-71-generic
% 0.11/5.38 % CPULimit : 300
% 0.11/5.38 % WCLimit : 300
% 0.11/5.38 % DateTime : Fri Sep 25 00:10:44 UTC 2026
% 0.11/5.38 % CPUTime :
% 0.11/5.39 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 6.28/6.52 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 6.28/6.52 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------