%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWW430-1 : TPTP v9.3.1. Released v5.2.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:27:05 PM UTC 2026
% Result : Unsatisfiable 46.76s 17.22s
% Output : Proof 46.76s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 5
% Syntax : Number of formulae : 34 ( 19 unt; 0 def)
% Number of atoms : 58 ( 46 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 40 ( 16 ~; 24 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 2 avg)
% Maximal term depth : 19 ( 3 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 13 con; 0-2 aty)
% Number of variables : 38 ( 6 sgn 14 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f0,axiom,
sep(S,sep(T,Sigma)) = sep(T,sep(S,Sigma)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',associative_commutative) ).
fof(f0_nnf,plain,
! [S,T,Sigma] : sep(S,sep(T,Sigma)) = sep(T,sep(S,Sigma)),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [S,T,Sigma] : sep(S,sep(T,Sigma)) = sep(T,sep(S,Sigma)),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
sep(X0,sep(X1,X2)) = sep(X1,sep(X0,X2)),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(f16,hypothesis,
heap(sep(lseg(x5,x2),sep(lseg(x5,x7),sep(lseg(x5,x4),sep(lseg(x12,x1),sep(lseg(x12,x6),sep(lseg(x2,x12),sep(lseg(x9,x10),sep(lseg(x3,x11),sep(lseg(x3,x1),sep(lseg(x3,x6),sep(lseg(x4,x9),sep(lseg(x4,x8),sep(lseg(x11,x8),sep(lseg(x11,x6),sep(lseg(x1,x9),sep(lseg(x1,x8),sep(lseg(x6,x2),emp)))))))))))))))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',premise_6) ).
fof(f16_nnf,plain,
heap(sep(lseg(x5,x2),sep(lseg(x5,x7),sep(lseg(x5,x4),sep(lseg(x12,x1),sep(lseg(x12,x6),sep(lseg(x2,x12),sep(lseg(x9,x10),sep(lseg(x3,x11),sep(lseg(x3,x1),sep(lseg(x3,x6),sep(lseg(x4,x9),sep(lseg(x4,x8),sep(lseg(x11,x8),sep(lseg(x11,x6),sep(lseg(x1,x9),sep(lseg(x1,x8),sep(lseg(x6,x2),emp)))))))))))))))))),
inference(nnf_transformation,[status(thm)],[f16]) ).
cnf(c16,plain,
heap(sep(lseg(x5,x2),sep(lseg(x5,x7),sep(lseg(x5,x4),sep(lseg(x12,x1),sep(lseg(x12,x6),sep(lseg(x2,x12),sep(lseg(x9,x10),sep(lseg(x3,x11),sep(lseg(x3,x1),sep(lseg(x3,x6),sep(lseg(x4,x9),sep(lseg(x4,x8),sep(lseg(x11,x8),sep(lseg(x11,x6),sep(lseg(x1,x9),sep(lseg(x1,x8),sep(lseg(x6,x2),emp)))))))))))))))))),
inference(cnf_transformation,[status(esa)],[f16_nnf]) ).
cnf(p71,plain,
heap(sep(lseg(x3,x11),sep(lseg(x12,x1),sep(lseg(x12,x6),sep(lseg(x2,x12),sep(lseg(x5,x7),sep(lseg(x5,x2),sep(lseg(x5,x4),sep(lseg(x9,x10),sep(lseg(x3,x1),sep(lseg(x3,x6),sep(lseg(x4,x9),sep(lseg(x4,x8),sep(lseg(x11,x8),sep(lseg(x11,x6),sep(lseg(x1,x9),sep(lseg(x1,x8),sep(lseg(x6,x2),emp)))))))))))))))))),
inference(superposition,[status(thm)],[c0,c16]) ).
cnf(p223,plain,
heap(sep(lseg(x3,x11),sep(lseg(x3,x1),sep(lseg(x3,x6),sep(lseg(x12,x1),sep(lseg(x12,x6),sep(lseg(x2,x12),sep(lseg(x5,x7),sep(lseg(x5,x2),sep(lseg(x5,x4),sep(lseg(x4,x9),sep(lseg(x9,x10),sep(lseg(x4,x8),sep(lseg(x11,x8),sep(lseg(x11,x6),sep(lseg(x1,x9),sep(lseg(x1,x8),sep(lseg(x6,x2),emp)))))))))))))))))),
inference(superposition,[status(thm)],[c0,p71]) ).
cnf(f6,axiom,
( X = Z
| X = Y
| ~ heap(sep(lseg(X,Y),sep(lseg(X,Z),Sigma))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',wellformedness_5) ).
fof(f6_nnf,plain,
! [X,Y,Z,Sigma] :
( X = Z
| X = Y
| ~ heap(sep(lseg(X,Y),sep(lseg(X,Z),Sigma))) ),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [X,Y,Z,Sigma] :
( X = Z
| X = Y
| ~ heap(sep(lseg(X,Y),sep(lseg(X,Z),Sigma))) ),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c6,plain,
( X0 = X2
| X0 = X1
| ~ heap(sep(lseg(X0,X1),sep(lseg(X0,X2),X3))) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(p2705,plain,
( x3 = x1
| x3 = x11 ),
inference(resolution,[status(thm)],[p223,c6]) ).
cnf(p34,plain,
( X0 = X3
| X0 = X1
| ~ heap(sep(lseg(X0,X1),sep(X2,sep(lseg(X0,X3),X4)))) ),
inference(superposition,[status(thm)],[c0,c6]) ).
cnf(p95,plain,
( X1 = X3
| X1 = X2
| ~ heap(sep(X0,sep(lseg(X1,X2),sep(lseg(X1,X3),X4)))) ),
inference(superposition,[status(thm)],[c0,p34]) ).
cnf(p240,plain,
( x12 = x6
| x12 = x1 ),
inference(resolution,[status(thm)],[p71,p95]) ).
cnf(p274,plain,
( x1 != x6
| x12 = x1 ),
inference(equality_factoring,[status(thm)],[p240]) ).
cnf(p2817,plain,
( x3 != x6
| x12 = x1
| x3 = x11 ),
inference(superposition,[status(thm)],[p2705,p274]) ).
cnf(p2711,plain,
( x3 = x6
| x3 = x11 ),
inference(resolution,[status(thm)],[p223,p34]) ).
cnf(p3341,plain,
( x3 = x11
| x12 = x1
| x3 = x11 ),
inference(resolution,[status(thm)],[p2817,p2711]) ).
cnf(p4175,plain,
( x12 = x1
| x3 = x11 ),
inference(factoring,[status(thm)],[p3341]) ).
cnf(p4316,plain,
( x3 = x12
| x3 = x11
| x3 = x11 ),
inference(superposition,[status(thm)],[p4175,p2705]) ).
cnf(p4605,plain,
( x3 = x12
| x3 = x11 ),
inference(factoring,[status(thm)],[p4316]) ).
cnf(f12,hypothesis,
x3 != x12,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',premise_2) ).
fof(f12_nnf,plain,
x3 != x12,
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
x3 != x12,
inference(skolemisation,[status(esa)],[f12_nnf]) ).
cnf(c12,plain,
x3 != x12,
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(p4727,plain,
x3 = x11,
inference(resolution,[status(thm)],[p4605,c12]) ).
cnf(f11,hypothesis,
x3 != x11,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',premise_1) ).
fof(f11_nnf,plain,
x3 != x11,
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
x3 != x11,
inference(skolemisation,[status(esa)],[f11_nnf]) ).
cnf(c11,plain,
x3 != x11,
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(p4728,plain,
$false,
inference(resolution,[status(thm)],[p4727,c11]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW430-1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.12/10.40 % Computer : n013.cluster.edu
% 0.12/10.40 % Model : x86_64 x86_64
% 0.12/10.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/10.40 % Memory : 8046.5625MB
% 0.12/10.40 % OS : Linux 6.8.0-71-generic
% 0.12/10.40 % CPULimit : 300
% 0.12/10.40 % WCLimit : 300
% 0.12/10.40 % DateTime : Thu Sep 24 22:21:49 UTC 2026
% 0.12/10.41 % CPUTime :
% 0.12/10.41 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 46.76/17.22 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 46.76/17.22 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------