%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWV370+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n004.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:13:06 PM UTC 2026
% Result : Theorem 32.14s 9.79s
% Output : Proof 32.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 5
% Syntax : Number of formulae : 51 ( 10 unt; 0 def)
% Number of atoms : 138 ( 34 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 128 ( 41 ~; 60 |; 18 &)
% ( 7 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 6 con; 0-3 aty)
% Number of variables : 138 ( 32 sgn 72 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f54,axiom,
! [U,V,W,X,Y] : i(triple(U,insert_slb(V,pair(X,Y)),W)) = insert_pq(i(triple(U,V,W)),X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax55) ).
fof(f54_nnf,plain,
! [U,V,W,X,Y] : i(triple(U,insert_slb(V,pair(X,Y)),W)) = insert_pq(i(triple(U,V,W)),X),
inference(nnf_transformation,[status(thm)],[f54]) ).
fof(f54_sk,plain,
! [U,V,X,Y,W] : i(triple(U,insert_slb(V,pair(X,Y)),W)) = insert_pq(i(triple(U,V,W)),X),
inference(skolemisation,[status(esa)],[f54_nnf]) ).
cnf(c69,plain,
i(triple(X0,insert_slb(X1,pair(X3,X4)),X2)) = insert_pq(i(triple(X0,X1,X2)),X3),
inference(cnf_transformation,[status(esa)],[f54_sk]) ).
fof(f62,conjecture,
! [U] :
( ! [V,W,X] :
( contains_cpq(triple(V,U,W),X)
<=> contains_pq(i(triple(V,U,W)),X) )
=> ! [Y,Z,X1,X2,X3] :
( contains_cpq(triple(Y,insert_slb(U,pair(X1,X2)),Z),X3)
<=> contains_pq(i(triple(Y,insert_slb(U,pair(X1,X2)),Z)),X3) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',l6_co) ).
fof(f62_neg,negated_conjecture,
~ ! [U] :
( ! [V,W,X] :
( contains_cpq(triple(V,U,W),X)
<=> contains_pq(i(triple(V,U,W)),X) )
=> ! [Y,Z,X1,X2,X3] :
( contains_cpq(triple(Y,insert_slb(U,pair(X1,X2)),Z),X3)
<=> contains_pq(i(triple(Y,insert_slb(U,pair(X1,X2)),Z)),X3) ) ),
inference(negated_conjecture,[status(cth)],[f62]) ).
fof(f62_nnf,plain,
? [U] :
( ? [Y,Z,X1,X2,X3] :
( ( contains_pq(i(triple(Y,insert_slb(U,pair(X1,X2)),Z)),X3)
& ~ contains_cpq(triple(Y,insert_slb(U,pair(X1,X2)),Z),X3) )
| ( ~ contains_pq(i(triple(Y,insert_slb(U,pair(X1,X2)),Z)),X3)
& contains_cpq(triple(Y,insert_slb(U,pair(X1,X2)),Z),X3) ) )
& ! [V,W,X] :
( ( ~ contains_pq(i(triple(V,U,W)),X)
| contains_cpq(triple(V,U,W),X) )
& ( contains_pq(i(triple(V,U,W)),X)
| ~ contains_cpq(triple(V,U,W),X) ) ) ),
inference(nnf_transformation,[status(thm)],[f62_neg]) ).
fof(f62_sk,plain,
! [V,W,X] :
( ( ( contains_pq(i(triple(sk5,insert_slb(sk4,pair(sk7,sk8)),sk6)),sk9)
& ~ contains_cpq(triple(sk5,insert_slb(sk4,pair(sk7,sk8)),sk6),sk9) )
| ( ~ contains_pq(i(triple(sk5,insert_slb(sk4,pair(sk7,sk8)),sk6)),sk9)
& contains_cpq(triple(sk5,insert_slb(sk4,pair(sk7,sk8)),sk6),sk9) ) )
& ( ~ contains_pq(i(triple(V,sk4,W)),X)
| contains_cpq(triple(V,sk4,W),X) )
& ( contains_pq(i(triple(V,sk4,W)),X)
| ~ contains_cpq(triple(V,sk4,W),X) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk4,sk5,sk6,sk7,sk8,sk9])],[f62_nnf]) ).
cnf(c92,plain,
( ~ contains_cpq(triple(sk5,insert_slb(sk4,pair(sk7,sk8)),sk6),sk9)
| ~ contains_pq(i(triple(sk5,insert_slb(sk4,pair(sk7,sk8)),sk6)),sk9) ),
inference(cnf_transformation,[status(esa)],[f62_sk]) ).
cnf(p788,plain,
( ~ contains_cpq(triple(sk5,insert_slb(sk4,pair(sk7,sk8)),sk6),sk9)
| ~ contains_pq(insert_pq(i(triple(sk5,sk4,sk6)),sk7),sk9) ),
inference(superposition,[status(thm)],[c69,c92]) ).
cnf(c91,plain,
( contains_pq(i(triple(sk5,insert_slb(sk4,pair(sk7,sk8)),sk6)),sk9)
| contains_cpq(triple(sk5,insert_slb(sk4,pair(sk7,sk8)),sk6),sk9) ),
inference(cnf_transformation,[status(esa)],[f62_sk]) ).
cnf(p787,plain,
( contains_pq(insert_pq(i(triple(sk5,sk4,sk6)),sk7),sk9)
| contains_cpq(triple(sk5,insert_slb(sk4,pair(sk7,sk8)),sk6),sk9) ),
inference(superposition,[status(thm)],[c69,c91]) ).
fof(f38,axiom,
! [U,V,W,X] :
( contains_cpq(triple(U,V,W),X)
<=> contains_slb(V,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax39) ).
fof(f38_nnf,plain,
! [U,V,W,X] :
( ( ~ contains_slb(V,X)
| contains_cpq(triple(U,V,W),X) )
& ( contains_slb(V,X)
| ~ contains_cpq(triple(U,V,W),X) ) ),
inference(nnf_transformation,[status(thm)],[f38]) ).
fof(f38_sk,plain,
! [U,V,W,X] :
( ( ~ contains_slb(V,X)
| contains_cpq(triple(U,V,W),X) )
& ( contains_slb(V,X)
| ~ contains_cpq(triple(U,V,W),X) ) ),
inference(skolemisation,[status(esa)],[f38_nnf]) ).
cnf(c51,plain,
( contains_slb(X1,X3)
| ~ contains_cpq(triple(X0,X1,X2),X3) ),
inference(cnf_transformation,[status(esa)],[f38_sk]) ).
cnf(p916,plain,
( contains_slb(insert_slb(sk4,pair(sk7,sk8)),sk9)
| contains_pq(insert_pq(i(triple(sk5,sk4,sk6)),sk7),sk9) ),
inference(resolution,[status(thm)],[p787,c51]) ).
fof(f8,axiom,
! [U,V,W] :
( contains_pq(insert_pq(U,V),W)
<=> ( V = W
| contains_pq(U,W) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax9) ).
fof(f8_nnf,plain,
! [U,V,W] :
( ( ( V != W
& ~ contains_pq(U,W) )
| contains_pq(insert_pq(U,V),W) )
& ( V = W
| contains_pq(U,W)
| ~ contains_pq(insert_pq(U,V),W) ) ),
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [U,V,W] :
( ( ( V != W
& ~ contains_pq(U,W) )
| contains_pq(insert_pq(U,V),W) )
& ( V = W
| contains_pq(U,W)
| ~ contains_pq(insert_pq(U,V),W) ) ),
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c10,plain,
( X1 = X2
| contains_pq(X0,X2)
| ~ contains_pq(insert_pq(X0,X1),X2) ),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(p917,plain,
( sk7 = sk9
| contains_pq(i(triple(sk5,sk4,sk6)),sk9)
| contains_slb(insert_slb(sk4,pair(sk7,sk8)),sk9) ),
inference(resolution,[status(thm)],[p916,c10]) ).
fof(f20,axiom,
! [U,V,W,X] :
( contains_slb(insert_slb(U,pair(V,X)),W)
<=> ( V = W
| contains_slb(U,W) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax21) ).
fof(f20_nnf,plain,
! [U,V,W,X] :
( ( ( V != W
& ~ contains_slb(U,W) )
| contains_slb(insert_slb(U,pair(V,X)),W) )
& ( V = W
| contains_slb(U,W)
| ~ contains_slb(insert_slb(U,pair(V,X)),W) ) ),
inference(nnf_transformation,[status(thm)],[f20]) ).
fof(f20_sk,plain,
! [U,V,X,W] :
( ( ( V != W
& ~ contains_slb(U,W) )
| contains_slb(insert_slb(U,pair(V,X)),W) )
& ( V = W
| contains_slb(U,W)
| ~ contains_slb(insert_slb(U,pair(V,X)),W) ) ),
inference(skolemisation,[status(esa)],[f20_nnf]) ).
cnf(c26,plain,
( X1 = X2
| contains_slb(X0,X2)
| ~ contains_slb(insert_slb(X0,pair(X1,X3)),X2) ),
inference(cnf_transformation,[status(esa)],[f20_sk]) ).
cnf(p925,plain,
( sk7 = sk9
| contains_slb(sk4,sk9)
| sk7 = sk9
| contains_pq(i(triple(sk5,sk4,sk6)),sk9) ),
inference(resolution,[status(thm)],[p917,c26]) ).
cnf(p940,plain,
( contains_slb(sk4,sk9)
| sk7 = sk9
| contains_pq(i(triple(sk5,sk4,sk6)),sk9) ),
inference(factoring,[status(thm)],[p925]) ).
cnf(c89,plain,
( ~ contains_pq(i(triple(X1,sk4,X2)),X3)
| contains_cpq(triple(X1,sk4,X2),X3) ),
inference(cnf_transformation,[status(esa)],[f62_sk]) ).
cnf(p941,plain,
( contains_cpq(triple(sk5,sk4,sk6),sk9)
| contains_slb(sk4,sk9)
| sk7 = sk9 ),
inference(resolution,[status(thm)],[p940,c89]) ).
cnf(p949,plain,
( contains_slb(sk4,sk9)
| contains_slb(sk4,sk9)
| sk7 = sk9 ),
inference(resolution,[status(thm)],[p941,c51]) ).
cnf(p954,plain,
( contains_slb(sk4,sk9)
| sk7 = sk9 ),
inference(factoring,[status(thm)],[p949]) ).
cnf(c52,plain,
( ~ contains_slb(X1,X3)
| contains_cpq(triple(X0,X1,X2),X3) ),
inference(cnf_transformation,[status(esa)],[f38_sk]) ).
cnf(p958,plain,
( contains_cpq(triple(X0,sk4,X1),sk9)
| sk7 = sk9 ),
inference(resolution,[status(thm)],[p954,c52]) ).
cnf(c88,plain,
( contains_pq(i(triple(X1,sk4,X2)),X3)
| ~ contains_cpq(triple(X1,sk4,X2),X3) ),
inference(cnf_transformation,[status(esa)],[f62_sk]) ).
cnf(p961,plain,
( contains_pq(i(triple(X0,sk4,X1)),sk9)
| sk7 = sk9 ),
inference(resolution,[status(thm)],[p958,c88]) ).
cnf(c11,plain,
( ~ contains_pq(X0,X2)
| contains_pq(insert_pq(X0,X1),X2) ),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(p969,plain,
( contains_pq(insert_pq(i(triple(X0,sk4,X1)),X2),sk9)
| sk7 = sk9 ),
inference(resolution,[status(thm)],[p961,c11]) ).
cnf(p1220,plain,
( sk7 = sk9
| ~ contains_cpq(triple(sk5,insert_slb(sk4,pair(sk7,sk8)),sk6),sk9) ),
inference(resolution,[status(thm)],[p788,p969]) ).
cnf(c27,plain,
( ~ contains_slb(X0,X2)
| contains_slb(insert_slb(X0,pair(X1,X3)),X2) ),
inference(cnf_transformation,[status(esa)],[f20_sk]) ).
cnf(p955,plain,
( contains_slb(insert_slb(sk4,pair(X0,X1)),sk9)
| sk7 = sk9 ),
inference(resolution,[status(thm)],[p954,c27]) ).
cnf(p965,plain,
( contains_cpq(triple(X0,insert_slb(sk4,pair(X1,X2)),X3),sk9)
| sk7 = sk9 ),
inference(resolution,[status(thm)],[p955,c52]) ).
cnf(p1221,plain,
( sk7 = sk9
| sk7 = sk9 ),
inference(resolution,[status(thm)],[p1220,p965]) ).
cnf(p1222,plain,
sk7 = sk9,
inference(factoring,[status(thm)],[p1221]) ).
cnf(c28,plain,
( X1 != X2
| contains_slb(insert_slb(X0,pair(X1,X3)),X2) ),
inference(cnf_transformation,[status(esa)],[f20_sk]) ).
cnf(p1276,plain,
contains_slb(insert_slb(X0,pair(sk7,X1)),sk9),
inference(resolution,[status(thm)],[p1222,c28]) ).
cnf(p1421,plain,
contains_cpq(triple(X0,insert_slb(X1,pair(sk7,X2)),X3),sk9),
inference(resolution,[status(thm)],[p1276,c52]) ).
cnf(c12,plain,
( X1 != X2
| contains_pq(insert_pq(X0,X1),X2) ),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(p1230,plain,
contains_pq(insert_pq(X0,sk7),sk9),
inference(resolution,[status(thm)],[p1222,c12]) ).
cnf(p1413,plain,
~ contains_cpq(triple(sk5,insert_slb(sk4,pair(sk7,sk8)),sk6),sk9),
inference(resolution,[status(thm)],[p1230,p788]) ).
cnf(p1466,plain,
$false,
inference(resolution,[status(thm)],[p1421,p1413]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV370+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/5.58 % Computer : n004.cluster.edu
% 0.09/5.58 % Model : x86_64 x86_64
% 0.09/5.58 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.58 % Memory : 8046.5625MB
% 0.09/5.58 % OS : Linux 6.8.0-71-generic
% 0.09/5.58 % CPULimit : 300
% 0.09/5.58 % WCLimit : 300
% 0.09/5.58 % DateTime : Thu Sep 24 19:23:42 UTC 2026
% 0.09/5.58 % CPUTime :
% 0.09/5.58 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 32.14/9.79 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 32.14/9.79 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------