%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SYN312-1 : TPTP v9.3.1. Bugfixed v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n009.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:34:18 PM UTC 2026
% Result : Unsatisfiable 20.91s 3.31s
% Output : Proof 20.91s
% Verified :
% SZS Type : Refutation
% Derivation depth : 52
% Number of leaves : 15
% Syntax : Number of formulae : 118 ( 98 unt; 0 def)
% Number of atoms : 142 ( 87 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 60 ( 36 ~; 24 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 2 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-3 aty)
% Number of functors : 14 ( 14 usr; 11 con; 0-4 aty)
% Number of variables : 105 ( 2 sgn 32 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(t8,axiom,
sFlat0 = g(a),
introduced(definition) ).
cnf(t58,plain,
g(a) = sFlat0,
inference(orient,[status(thm)],[t8]) ).
cnf(t9,axiom,
sFlat1 = f(g(a)),
introduced(definition) ).
cnf(t3233,plain,
sFlat1 = f(sFlat0),
inference(step,[status(thm)],[t9,t58]) ).
cnf(t64,plain,
f(sFlat0) = sFlat1,
inference(orient,[status(thm)],[t3233]) ).
cnf(t10,axiom,
sFlat2 = g(d),
introduced(definition) ).
cnf(t60,plain,
g(d) = sFlat2,
inference(orient,[status(thm)],[t10]) ).
cnf(t11,axiom,
sFlat3 = f(g(d)),
introduced(definition) ).
cnf(t3234,plain,
sFlat3 = f(sFlat2),
inference(step,[status(thm)],[t11,t60]) ).
cnf(t66,plain,
f(sFlat2) = sFlat3,
inference(orient,[status(thm)],[t3234]) ).
cnf(t12,axiom,
sFlat4 = g(c),
introduced(definition) ).
cnf(t55,plain,
g(c) = sFlat4,
inference(orient,[status(thm)],[t12]) ).
cnf(t13,axiom,
sFlat5 = f(g(c)),
introduced(definition) ).
cnf(t3232,plain,
sFlat5 = f(sFlat4),
inference(step,[status(thm)],[t13,t55]) ).
cnf(t62,plain,
f(sFlat4) = sFlat5,
inference(orient,[status(thm)],[t3232]) ).
cnf(f3,negated_conjecture,
( ~ p(X,X1,X2)
| p(X,X1,f(X2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause4) ).
fof(f3_nnf,plain,
! [X,X1,X2] :
( ~ p(X,X1,X2)
| p(X,X1,f(X2)) ),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [X,X1,X2] :
( ~ p(X,X1,X2)
| p(X,X1,f(X2)) ),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
( ~ p(X0,X1,X2)
| p(X0,X1,f(X2)) ),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(t5,plain,
ifeq(p(X1,X2,X3),true,p(X1,X2,f(X3)),true) = true,
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(t28,plain,
ifeq(p(X1,X2,X3),true,p(X1,X2,f(X3)),true) = true,
inference(orient,[status(thm)],[t5]) ).
cnf(f1,negated_conjecture,
( ~ p(X,X1,X2)
| p(X2,X1,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause2) ).
fof(f1_nnf,plain,
! [X2,X1,X] :
( ~ p(X,X1,X2)
| p(X2,X1,X) ),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [X2,X1,X] :
( ~ p(X,X1,X2)
| p(X2,X1,X) ),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
( ~ p(X2,X1,X0)
| p(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(t4,plain,
ifeq(p(X1,X2,X3),true,p(X3,X2,X1),true) = true,
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t18,plain,
ifeq(p(X1,X2,X3),true,p(X3,X2,X1),true) = true,
inference(orient,[status(thm)],[t4]) ).
cnf(f4,negated_conjecture,
( ~ p(X,X1,X2)
| p(g(X),X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause5) ).
fof(f4_nnf,plain,
! [X,X1,X2] :
( ~ p(X,X1,X2)
| p(g(X),X1,X2) ),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [X,X1,X2] :
( ~ p(X,X1,X2)
| p(g(X),X1,X2) ),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c4,plain,
( ~ p(X0,X1,X2)
| p(g(X0),X1,X2) ),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(t6,plain,
ifeq(p(X1,X2,X3),true,p(g(X1),X2,X3),true) = true,
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(t31,plain,
ifeq(p(X1,X2,X3),true,p(g(X1),X2,X3),true) = true,
inference(orient,[status(thm)],[t6]) ).
cnf(f0,negated_conjecture,
( ~ p(X1,X3,X2)
| ~ p(X,X1,X2)
| p(X,X3,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause1) ).
fof(f0_nnf,plain,
! [X,X3,X2,X1] :
( ~ p(X1,X3,X2)
| ~ p(X,X1,X2)
| p(X,X3,X2) ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [X,X3,X2,X1] :
( ~ p(X1,X3,X2)
| ~ p(X,X1,X2)
| p(X,X3,X2) ),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
( ~ p(X3,X1,X2)
| ~ p(X0,X3,X2)
| p(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t7,plain,
ifeq(p(X1,X2,X3),true,ifeq(p(X2,X4,X3),true,p(X1,X4,X3),true),true) = true,
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t34,plain,
ifeq(p(X1,X2,X3),true,ifeq(p(X2,X4,X3),true,p(X1,X4,X3),true),true) = true,
inference(orient,[status(thm)],[t7]) ).
cnf(f5,negated_conjecture,
p(a,f(b),c),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause6) ).
fof(f5_nnf,plain,
p(a,f(b),c),
inference(nnf_transformation,[status(thm)],[f5]) ).
cnf(c5,plain,
p(a,f(b),c),
inference(cnf_transformation,[status(esa)],[f5_nnf]) ).
cnf(t1,plain,
p(a,f(b),c) = true,
inference(equality_encoding,[status(esa)],[c5]) ).
cnf(t17,plain,
p(a,f(b),c) = true,
inference(orient,[status(thm)],[t1]) ).
cnf(t36,plain,
true = ifeq(true,true,ifeq(p(f(b),X1,c),true,p(a,X1,c),true),true),
inference(cp,[status(thm)],[t34,t17]) ).
cnf(t0,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t15,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t0]) ).
cnf(t3463,plain,
true = ifeq(p(f(b),X1,c),true,p(a,X1,c),true),
inference(step,[status(thm)],[t36,t15]) ).
cnf(t1746,plain,
ifeq(p(f(b),X1,c),true,p(a,X1,c),true) = true,
inference(orient,[status(thm)],[t3463]) ).
cnf(f2,negated_conjecture,
( ~ p(X,X1,X2)
| p(X1,X,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause3) ).
fof(f2_nnf,plain,
! [X1,X,X2] :
( ~ p(X,X1,X2)
| p(X1,X,X2) ),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [X1,X,X2] :
( ~ p(X,X1,X2)
| p(X1,X,X2) ),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
( ~ p(X1,X0,X2)
| p(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(t3,plain,
ifeq(p(X1,X2,X3),true,p(X2,X1,X3),true) = true,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t23,plain,
ifeq(p(X1,X2,X3),true,p(X2,X1,X3),true) = true,
inference(orient,[status(thm)],[t3]) ).
cnf(f6,negated_conjecture,
p(f(b),d,c),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause7) ).
fof(f6_nnf,plain,
p(f(b),d,c),
inference(nnf_transformation,[status(thm)],[f6]) ).
cnf(c6,plain,
p(f(b),d,c),
inference(cnf_transformation,[status(esa)],[f6_nnf]) ).
cnf(t2,plain,
p(f(b),d,c) = true,
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(t16,plain,
p(f(b),d,c) = true,
inference(orient,[status(thm)],[t2]) ).
cnf(t24,plain,
true = ifeq(true,true,p(d,f(b),c),true),
inference(cp,[status(thm)],[t23,t16]) ).
cnf(t3237,plain,
true = p(d,f(b),c),
inference(step,[status(thm)],[t24,t15]) ).
cnf(t85,plain,
p(d,f(b),c) = true,
inference(orient,[status(thm)],[t3237]) ).
cnf(t92,plain,
true = ifeq(true,true,p(g(d),f(b),c),true),
inference(cp,[status(thm)],[t31,t85]) ).
cnf(t3246,plain,
true = p(g(d),f(b),c),
inference(step,[status(thm)],[t92,t15]) ).
cnf(t3247,plain,
true = p(sFlat2,f(b),c),
inference(step,[status(thm)],[t3246,t60]) ).
cnf(t147,plain,
p(sFlat2,f(b),c) = true,
inference(orient,[status(thm)],[t3247]) ).
cnf(t150,plain,
true = ifeq(true,true,p(c,f(b),sFlat2),true),
inference(cp,[status(thm)],[t18,t147]) ).
cnf(t3260,plain,
true = p(c,f(b),sFlat2),
inference(step,[status(thm)],[t150,t15]) ).
cnf(t241,plain,
p(c,f(b),sFlat2) = true,
inference(orient,[status(thm)],[t3260]) ).
cnf(t244,plain,
true = ifeq(true,true,p(c,f(b),f(sFlat2)),true),
inference(cp,[status(thm)],[t28,t241]) ).
cnf(t3279,plain,
true = p(c,f(b),f(sFlat2)),
inference(step,[status(thm)],[t244,t15]) ).
cnf(t3280,plain,
true = p(c,f(b),sFlat3),
inference(step,[status(thm)],[t3279,t66]) ).
cnf(t350,plain,
p(c,f(b),sFlat3) = true,
inference(orient,[status(thm)],[t3280]) ).
cnf(t353,plain,
true = ifeq(true,true,p(sFlat3,f(b),c),true),
inference(cp,[status(thm)],[t18,t350]) ).
cnf(t3305,plain,
true = p(sFlat3,f(b),c),
inference(step,[status(thm)],[t353,t15]) ).
cnf(t498,plain,
p(sFlat3,f(b),c) = true,
inference(orient,[status(thm)],[t3305]) ).
cnf(t499,plain,
true = ifeq(true,true,p(f(b),sFlat3,c),true),
inference(cp,[status(thm)],[t23,t498]) ).
cnf(t3329,plain,
true = p(f(b),sFlat3,c),
inference(step,[status(thm)],[t499,t15]) ).
cnf(t647,plain,
p(f(b),sFlat3,c) = true,
inference(orient,[status(thm)],[t3329]) ).
cnf(t1748,plain,
true = ifeq(true,true,p(a,sFlat3,c),true),
inference(cp,[status(thm)],[t1746,t647]) ).
cnf(t3465,plain,
true = p(a,sFlat3,c),
inference(step,[status(thm)],[t1748,t15]) ).
cnf(t1764,plain,
p(a,sFlat3,c) = true,
inference(orient,[status(thm)],[t3465]) ).
cnf(t1773,plain,
true = ifeq(true,true,p(g(a),sFlat3,c),true),
inference(cp,[status(thm)],[t31,t1764]) ).
cnf(t3476,plain,
true = p(g(a),sFlat3,c),
inference(step,[status(thm)],[t1773,t15]) ).
cnf(t3477,plain,
true = p(sFlat0,sFlat3,c),
inference(step,[status(thm)],[t3476,t58]) ).
cnf(t1854,plain,
p(sFlat0,sFlat3,c) = true,
inference(orient,[status(thm)],[t3477]) ).
cnf(t1857,plain,
true = ifeq(true,true,p(c,sFlat3,sFlat0),true),
inference(cp,[status(thm)],[t18,t1854]) ).
cnf(t3502,plain,
true = p(c,sFlat3,sFlat0),
inference(step,[status(thm)],[t1857,t15]) ).
cnf(t2023,plain,
p(c,sFlat3,sFlat0) = true,
inference(orient,[status(thm)],[t3502]) ).
cnf(t2026,plain,
true = ifeq(true,true,p(c,sFlat3,f(sFlat0)),true),
inference(cp,[status(thm)],[t28,t2023]) ).
cnf(t3541,plain,
true = p(c,sFlat3,f(sFlat0)),
inference(step,[status(thm)],[t2026,t15]) ).
cnf(t3542,plain,
true = p(c,sFlat3,sFlat1),
inference(step,[status(thm)],[t3541,t64]) ).
cnf(t2277,plain,
p(c,sFlat3,sFlat1) = true,
inference(orient,[status(thm)],[t3542]) ).
cnf(t2286,plain,
true = ifeq(true,true,p(g(c),sFlat3,sFlat1),true),
inference(cp,[status(thm)],[t31,t2277]) ).
cnf(t3606,plain,
true = p(g(c),sFlat3,sFlat1),
inference(step,[status(thm)],[t2286,t15]) ).
cnf(t3607,plain,
true = p(sFlat4,sFlat3,sFlat1),
inference(step,[status(thm)],[t3606,t55]) ).
cnf(t2624,plain,
p(sFlat4,sFlat3,sFlat1) = true,
inference(orient,[status(thm)],[t3607]) ).
cnf(t2627,plain,
true = ifeq(true,true,p(sFlat1,sFlat3,sFlat4),true),
inference(cp,[status(thm)],[t18,t2624]) ).
cnf(t3671,plain,
true = p(sFlat1,sFlat3,sFlat4),
inference(step,[status(thm)],[t2627,t15]) ).
cnf(t2949,plain,
p(sFlat1,sFlat3,sFlat4) = true,
inference(orient,[status(thm)],[t3671]) ).
cnf(t2952,plain,
true = ifeq(true,true,p(sFlat1,sFlat3,f(sFlat4)),true),
inference(cp,[status(thm)],[t28,t2949]) ).
cnf(t3715,plain,
true = p(sFlat1,sFlat3,f(sFlat4)),
inference(step,[status(thm)],[t2952,t15]) ).
cnf(t3716,plain,
true = p(sFlat1,sFlat3,sFlat5),
inference(step,[status(thm)],[t3715,t62]) ).
cnf(t3221,plain,
p(sFlat1,sFlat3,sFlat5) = true,
inference(orient,[status(thm)],[t3716]) ).
cnf(f7,negated_conjecture,
~ p(f(g(a)),f(g(d)),f(g(c))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause8) ).
fof(f7_nnf,plain,
~ p(f(g(a)),f(g(d)),f(g(c))),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
~ p(f(g(a)),f(g(d)),f(g(c))),
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c7,plain,
~ p(f(g(a)),f(g(d)),f(g(c))),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(goal_0,negated_conjecture,
p(f(g(a)),f(g(d)),f(g(c))) != true,
inference(equality_encoding,[status(esa)],[c7]) ).
cnf(g0_0,plain,
p(f(sFlat0),f(g(d)),f(g(c))) != true,
inference(rw,[status(thm)],[goal_0,t58]) ).
cnf(g0_1,plain,
p(sFlat1,f(g(d)),f(g(c))) != true,
inference(rw,[status(thm)],[g0_0,t64]) ).
cnf(g0_2,plain,
p(sFlat1,f(sFlat2),f(g(c))) != true,
inference(rw,[status(thm)],[g0_1,t60]) ).
cnf(g0_3,plain,
p(sFlat1,sFlat3,f(g(c))) != true,
inference(rw,[status(thm)],[g0_2,t66]) ).
cnf(g0_4,plain,
p(sFlat1,sFlat3,f(sFlat4)) != true,
inference(rw,[status(thm)],[g0_3,t55]) ).
cnf(g0_5,plain,
p(sFlat1,sFlat3,sFlat5) != true,
inference(rw,[status(thm)],[g0_4,t62]) ).
cnf(g0_6,plain,
true != true,
inference(rw,[status(thm)],[g0_5,t3221]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_6]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN312-1 : TPTP v9.3.1. Bugfixed v2.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/0.35 % Computer : n009.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Fri Sep 25 00:47:58 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.09/0.35 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 20.91/3.31 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 20.91/3.31 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------