%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SYN645-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n026.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:35:23 PM UTC 2026
% Result : Unsatisfiable 30.29s 4.29s
% Output : Proof 30.29s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 14
% Syntax : Number of formulae : 114 ( 94 unt; 0 def)
% Number of atoms : 174 ( 72 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 118 ( 58 ~; 60 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 2 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-2 aty)
% Number of functors : 22 ( 22 usr; 9 con; 0-5 aty)
% Number of variables : 191 ( 2 sgn 46 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f41,negated_conjecture,
( ~ p25(f13(f14(X7,X3)),f13(f14(X7,f21(X4,X5,X6,X7,X3))))
| ~ p23(X3,f8(f10(X4,f11(X5,X6))))
| ~ p22(f3(f4(f5(c26))),X5)
| p24(f17(f10(X4,f11(X5,X6)),f16(f10(X4,f11(X5,X6)),c32,X7)))
| p12(X3,f16(f10(X4,f11(X5,X6)),c32,X7)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p12_42) ).
fof(f41_nnf,plain,
! [X3,X4,X5,X6,X7] :
( ~ p25(f13(f14(X7,X3)),f13(f14(X7,f21(X4,X5,X6,X7,X3))))
| ~ p23(X3,f8(f10(X4,f11(X5,X6))))
| ~ p22(f3(f4(f5(c26))),X5)
| p24(f17(f10(X4,f11(X5,X6)),f16(f10(X4,f11(X5,X6)),c32,X7)))
| p12(X3,f16(f10(X4,f11(X5,X6)),c32,X7)) ),
inference(nnf_transformation,[status(thm)],[f41]) ).
fof(f41_sk,plain,
! [X3,X4,X5,X6,X7] :
( ~ p25(f13(f14(X7,X3)),f13(f14(X7,f21(X4,X5,X6,X7,X3))))
| ~ p23(X3,f8(f10(X4,f11(X5,X6))))
| ~ p22(f3(f4(f5(c26))),X5)
| p24(f17(f10(X4,f11(X5,X6)),f16(f10(X4,f11(X5,X6)),c32,X7)))
| p12(X3,f16(f10(X4,f11(X5,X6)),c32,X7)) ),
inference(skolemisation,[status(esa)],[f41_nnf]) ).
cnf(c41,plain,
( ~ p25(f13(f14(X4,X0)),f13(f14(X4,f21(X1,X2,X3,X4,X0))))
| ~ p23(X0,f8(f10(X1,f11(X2,X3))))
| ~ p22(f3(f4(f5(c26))),X2)
| p24(f17(f10(X1,f11(X2,X3)),f16(f10(X1,f11(X2,X3)),c32,X4)))
| p12(X0,f16(f10(X1,f11(X2,X3)),c32,X4)) ),
inference(cnf_transformation,[status(esa)],[f41_sk]) ).
cnf(t48,plain,
ifeq(p22(f3(f4(f5(c26))),X1),true,ifeq(p23(X2,f8(f10(X3,f11(X1,X4)))),true,ifeq(p25(f13(f14(X5,X2)),f13(f14(X5,f21(X3,X1,X4,X5,X2)))),true,or(p12(X2,f16(f10(X3,f11(X1,X4)),c32,X5)),p24(f17(f10(X3,f11(X1,X4)),f16(f10(X3,f11(X1,X4)),c32,X5)))),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c41]) ).
cnf(t70,plain,
ifeq(p22(f3(f4(f5(c26))),X1),true,ifeq(p23(X2,f8(f10(X3,f11(X1,X4)))),true,ifeq(p25(f13(f14(X5,X2)),f13(f14(X5,f21(X3,X1,X4,X5,X2)))),true,or(p12(X2,f16(f10(X3,f11(X1,X4)),c32,X5)),p24(f17(f10(X3,f11(X1,X4)),f16(f10(X3,f11(X1,X4)),c32,X5)))),true),true),true) = true,
inference(orient,[status(thm)],[t48]) ).
cnf(f8,negated_conjecture,
p23(c28,f8(f10(c29,f11(c27,c30)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p23_9) ).
fof(f8_nnf,plain,
p23(c28,f8(f10(c29,f11(c27,c30)))),
inference(nnf_transformation,[status(thm)],[f8]) ).
cnf(c8,plain,
p23(c28,f8(f10(c29,f11(c27,c30)))),
inference(cnf_transformation,[status(esa)],[f8_nnf]) ).
cnf(t12,plain,
p23(c28,f8(f10(c29,f11(c27,c30)))) = true,
inference(equality_encoding,[status(esa)],[c8]) ).
cnf(t141,plain,
p23(c28,f8(f10(c29,f11(c27,c30)))) = true,
inference(orient,[status(thm)],[t12]) ).
cnf(t147,plain,
true = ifeq(p22(f3(f4(f5(c26))),c27),true,ifeq(true,true,ifeq(p25(f13(f14(X1,c28)),f13(f14(X1,f21(c29,c27,c30,X1,c28)))),true,or(p12(c28,f16(f10(c29,f11(c27,c30)),c32,X1)),p24(f17(f10(c29,f11(c27,c30)),f16(f10(c29,f11(c27,c30)),c32,X1)))),true),true),true),
inference(cp,[status(thm)],[t70,t141]) ).
cnf(f6,negated_conjecture,
p22(f3(f4(f5(c26))),c27),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p22_7) ).
fof(f6_nnf,plain,
p22(f3(f4(f5(c26))),c27),
inference(nnf_transformation,[status(thm)],[f6]) ).
cnf(c6,plain,
p22(f3(f4(f5(c26))),c27),
inference(cnf_transformation,[status(esa)],[f6_nnf]) ).
cnf(t11,plain,
p22(f3(f4(f5(c26))),c27) = true,
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(t149,plain,
p22(f3(f4(f5(c26))),c27) = true,
inference(orient,[status(thm)],[t11]) ).
cnf(t40950,plain,
true = ifeq(true,true,ifeq(true,true,ifeq(p25(f13(f14(X1,c28)),f13(f14(X1,f21(c29,c27,c30,X1,c28)))),true,or(p12(c28,f16(f10(c29,f11(c27,c30)),c32,X1)),p24(f17(f10(c29,f11(c27,c30)),f16(f10(c29,f11(c27,c30)),c32,X1)))),true),true),true),
inference(step,[status(thm)],[t147,t149]) ).
cnf(t10,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t49,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t10]) ).
cnf(t40951,plain,
true = ifeq(true,true,ifeq(p25(f13(f14(X1,c28)),f13(f14(X1,f21(c29,c27,c30,X1,c28)))),true,or(p12(c28,f16(f10(c29,f11(c27,c30)),c32,X1)),p24(f17(f10(c29,f11(c27,c30)),f16(f10(c29,f11(c27,c30)),c32,X1)))),true),true),
inference(step,[status(thm)],[t40950,t49]) ).
cnf(t40952,plain,
true = ifeq(p25(f13(f14(X1,c28)),f13(f14(X1,f21(c29,c27,c30,X1,c28)))),true,or(p12(c28,f16(f10(c29,f11(c27,c30)),c32,X1)),p24(f17(f10(c29,f11(c27,c30)),f16(f10(c29,f11(c27,c30)),c32,X1)))),true),
inference(step,[status(thm)],[t40951,t49]) ).
cnf(t38617,plain,
ifeq(p25(f13(f14(X1,c28)),f13(f14(X1,f21(c29,c27,c30,X1,c28)))),true,or(p12(c28,f16(f10(c29,f11(c27,c30)),c32,X1)),p24(f17(f10(c29,f11(c27,c30)),f16(f10(c29,f11(c27,c30)),c32,X1)))),true) = true,
inference(orient,[status(thm)],[t40952]) ).
cnf(f22,negated_conjecture,
( ~ p12(X68,X66)
| ~ p25(X68,X69)
| ~ p12(X69,X67)
| p25(X66,X67) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p25_23) ).
fof(f22_nnf,plain,
! [X66,X67,X69,X68] :
( ~ p12(X68,X66)
| ~ p25(X68,X69)
| ~ p12(X69,X67)
| p25(X66,X67) ),
inference(nnf_transformation,[status(thm)],[f22]) ).
fof(f22_sk,plain,
! [X66,X67,X69,X68] :
( ~ p12(X68,X66)
| ~ p25(X68,X69)
| ~ p12(X69,X67)
| p25(X66,X67) ),
inference(skolemisation,[status(esa)],[f22_nnf]) ).
cnf(c22,plain,
( ~ p12(X3,X0)
| ~ p25(X3,X2)
| ~ p12(X2,X1)
| p25(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f22_sk]) ).
cnf(t37,plain,
ifeq(p12(X1,X2),true,ifeq(p25(X3,X1),true,ifeq(p12(X3,X4),true,p25(X4,X2),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c22]) ).
cnf(t57,plain,
ifeq(p12(X1,X2),true,ifeq(p25(X3,X1),true,ifeq(p12(X3,X4),true,p25(X4,X2),true),true),true) = true,
inference(orient,[status(thm)],[t37]) ).
cnf(f0,negated_conjecture,
p12(X0,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p12_1) ).
fof(f0_nnf,plain,
! [X0] : p12(X0,X0),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [X0] : p12(X0,X0),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
p12(X0,X0),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t4,plain,
p12(X1,X1) = true,
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t85,plain,
p12(X1,X1) = true,
inference(orient,[status(thm)],[t4]) ).
cnf(t93,plain,
true = ifeq(true,true,ifeq(p25(X1,X2),true,ifeq(p12(X1,X3),true,p25(X3,X2),true),true),true),
inference(cp,[status(thm)],[t57,t85]) ).
cnf(t40068,plain,
true = ifeq(p25(X1,X2),true,ifeq(p12(X1,X3),true,p25(X3,X2),true),true),
inference(step,[status(thm)],[t93,t49]) ).
cnf(t274,plain,
ifeq(p25(X1,X2),true,ifeq(p12(X1,X3),true,p25(X3,X2),true),true) = true,
inference(orient,[status(thm)],[t40068]) ).
cnf(f15,negated_conjecture,
( ~ p12(X0,X2)
| ~ p12(X0,X1)
| p12(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p12_16) ).
fof(f15_nnf,plain,
! [X1,X2,X0] :
( ~ p12(X0,X2)
| ~ p12(X0,X1)
| p12(X1,X2) ),
inference(nnf_transformation,[status(thm)],[f15]) ).
fof(f15_sk,plain,
! [X1,X2,X0] :
( ~ p12(X0,X2)
| ~ p12(X0,X1)
| p12(X1,X2) ),
inference(skolemisation,[status(esa)],[f15_nnf]) ).
cnf(c15,plain,
( ~ p12(X2,X1)
| ~ p12(X2,X0)
| p12(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f15_sk]) ).
cnf(t22,plain,
ifeq(p12(X1,X2),true,ifeq(p12(X1,X3),true,p12(X2,X3),true),true) = true,
inference(equality_encoding,[status(esa)],[c15]) ).
cnf(t54,plain,
ifeq(p12(X1,X2),true,ifeq(p12(X1,X3),true,p12(X2,X3),true),true) = true,
inference(orient,[status(thm)],[t22]) ).
cnf(t87,plain,
true = ifeq(p12(X1,X2),true,ifeq(true,true,p12(X2,X1),true),true),
inference(cp,[status(thm)],[t54,t85]) ).
cnf(t40041,plain,
true = ifeq(p12(X1,X2),true,p12(X2,X1),true),
inference(step,[status(thm)],[t87,t49]) ).
cnf(t218,plain,
ifeq(p12(X1,X2),true,p12(X2,X1),true) = true,
inference(orient,[status(thm)],[t40041]) ).
cnf(f32,negated_conjecture,
p12(f13(f14(c31,c28)),f13(f14(c31,f16(f10(c29,f11(c27,c30)),c32,c31)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p12_33) ).
fof(f32_nnf,plain,
p12(f13(f14(c31,c28)),f13(f14(c31,f16(f10(c29,f11(c27,c30)),c32,c31)))),
inference(nnf_transformation,[status(thm)],[f32]) ).
cnf(c32,plain,
p12(f13(f14(c31,c28)),f13(f14(c31,f16(f10(c29,f11(c27,c30)),c32,c31)))),
inference(cnf_transformation,[status(esa)],[f32_nnf]) ).
cnf(t29,plain,
p12(f13(f14(c31,c28)),f13(f14(c31,f16(f10(c29,f11(c27,c30)),c32,c31)))) = true,
inference(equality_encoding,[status(esa)],[c32]) ).
cnf(t109,plain,
p12(f13(f14(c31,c28)),f13(f14(c31,f16(f10(c29,f11(c27,c30)),c32,c31)))) = true,
inference(orient,[status(thm)],[t29]) ).
cnf(t220,plain,
true = ifeq(true,true,p12(f13(f14(c31,f16(f10(c29,f11(c27,c30)),c32,c31))),f13(f14(c31,c28))),true),
inference(cp,[status(thm)],[t218,t109]) ).
cnf(t40083,plain,
true = p12(f13(f14(c31,f16(f10(c29,f11(c27,c30)),c32,c31))),f13(f14(c31,c28))),
inference(step,[status(thm)],[t220,t49]) ).
cnf(t325,plain,
p12(f13(f14(c31,f16(f10(c29,f11(c27,c30)),c32,c31))),f13(f14(c31,c28))) = true,
inference(orient,[status(thm)],[t40083]) ).
cnf(t331,plain,
true = ifeq(p25(f13(f14(c31,f16(f10(c29,f11(c27,c30)),c32,c31))),X1),true,ifeq(true,true,p25(f13(f14(c31,c28)),X1),true),true),
inference(cp,[status(thm)],[t274,t325]) ).
cnf(t40118,plain,
true = ifeq(p25(f13(f14(c31,f16(f10(c29,f11(c27,c30)),c32,c31))),X1),true,p25(f13(f14(c31,c28)),X1),true),
inference(step,[status(thm)],[t331,t49]) ).
cnf(t900,plain,
ifeq(p25(f13(f14(c31,f16(f10(c29,f11(c27,c30)),c32,c31))),X1),true,p25(f13(f14(c31,c28)),X1),true) = true,
inference(orient,[status(thm)],[t40118]) ).
cnf(f36,negated_conjecture,
( ~ p23(X3,f8(f10(X4,f11(X5,X6))))
| ~ p22(f3(f4(f5(c26))),X5)
| p25(f13(f14(X7,f16(f10(X4,f11(X5,X6)),c32,X7))),f13(f14(X7,X3))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p25_37) ).
fof(f36_nnf,plain,
! [X7,X4,X5,X6,X3] :
( ~ p23(X3,f8(f10(X4,f11(X5,X6))))
| ~ p22(f3(f4(f5(c26))),X5)
| p25(f13(f14(X7,f16(f10(X4,f11(X5,X6)),c32,X7))),f13(f14(X7,X3))) ),
inference(nnf_transformation,[status(thm)],[f36]) ).
fof(f36_sk,plain,
! [X7,X4,X5,X6,X3] :
( ~ p23(X3,f8(f10(X4,f11(X5,X6))))
| ~ p22(f3(f4(f5(c26))),X5)
| p25(f13(f14(X7,f16(f10(X4,f11(X5,X6)),c32,X7))),f13(f14(X7,X3))) ),
inference(skolemisation,[status(esa)],[f36_nnf]) ).
cnf(c36,plain,
( ~ p23(X4,f8(f10(X1,f11(X2,X3))))
| ~ p22(f3(f4(f5(c26))),X2)
| p25(f13(f14(X0,f16(f10(X1,f11(X2,X3)),c32,X0))),f13(f14(X0,X4))) ),
inference(cnf_transformation,[status(esa)],[f36_sk]) ).
cnf(t43,plain,
ifeq(p22(f3(f4(f5(c26))),X1),true,ifeq(p23(X2,f8(f10(X3,f11(X1,X4)))),true,p25(f13(f14(X5,f16(f10(X3,f11(X1,X4)),c32,X5))),f13(f14(X5,X2))),true),true) = true,
inference(equality_encoding,[status(esa)],[c36]) ).
cnf(t72,plain,
ifeq(p22(f3(f4(f5(c26))),X1),true,ifeq(p23(X2,f8(f10(X3,f11(X1,X4)))),true,p25(f13(f14(X5,f16(f10(X3,f11(X1,X4)),c32,X5))),f13(f14(X5,X2))),true),true) = true,
inference(orient,[status(thm)],[t43]) ).
cnf(t154,plain,
true = ifeq(true,true,ifeq(p23(X1,f8(f10(X2,f11(c27,X3)))),true,p25(f13(f14(X4,f16(f10(X2,f11(c27,X3)),c32,X4))),f13(f14(X4,X1))),true),true),
inference(cp,[status(thm)],[t72,t149]) ).
cnf(t40875,plain,
true = ifeq(p23(X1,f8(f10(X2,f11(c27,X3)))),true,p25(f13(f14(X4,f16(f10(X2,f11(c27,X3)),c32,X4))),f13(f14(X4,X1))),true),
inference(step,[status(thm)],[t154,t49]) ).
cnf(t33017,plain,
ifeq(p23(X1,f8(f10(X2,f11(c27,X3)))),true,p25(f13(f14(X4,f16(f10(X2,f11(c27,X3)),c32,X4))),f13(f14(X4,X1))),true) = true,
inference(orient,[status(thm)],[t40875]) ).
cnf(f40,negated_conjecture,
( ~ p23(X3,f8(f10(X4,f11(X5,X6))))
| ~ p22(f3(f4(f5(c26))),X5)
| p24(f17(f10(X4,f11(X5,X6)),f16(f10(X4,f11(X5,X6)),c32,X7)))
| p23(f21(X4,X5,X6,X7,X3),f8(f10(X4,f11(X5,X6))))
| p12(X3,f16(f10(X4,f11(X5,X6)),c32,X7)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p12_41) ).
fof(f40_nnf,plain,
! [X3,X4,X5,X6,X7] :
( ~ p23(X3,f8(f10(X4,f11(X5,X6))))
| ~ p22(f3(f4(f5(c26))),X5)
| p24(f17(f10(X4,f11(X5,X6)),f16(f10(X4,f11(X5,X6)),c32,X7)))
| p23(f21(X4,X5,X6,X7,X3),f8(f10(X4,f11(X5,X6))))
| p12(X3,f16(f10(X4,f11(X5,X6)),c32,X7)) ),
inference(nnf_transformation,[status(thm)],[f40]) ).
fof(f40_sk,plain,
! [X3,X4,X5,X6,X7] :
( ~ p23(X3,f8(f10(X4,f11(X5,X6))))
| ~ p22(f3(f4(f5(c26))),X5)
| p24(f17(f10(X4,f11(X5,X6)),f16(f10(X4,f11(X5,X6)),c32,X7)))
| p23(f21(X4,X5,X6,X7,X3),f8(f10(X4,f11(X5,X6))))
| p12(X3,f16(f10(X4,f11(X5,X6)),c32,X7)) ),
inference(skolemisation,[status(esa)],[f40_nnf]) ).
cnf(c40,plain,
( ~ p23(X0,f8(f10(X1,f11(X2,X3))))
| ~ p22(f3(f4(f5(c26))),X2)
| p24(f17(f10(X1,f11(X2,X3)),f16(f10(X1,f11(X2,X3)),c32,X4)))
| p23(f21(X1,X2,X3,X4,X0),f8(f10(X1,f11(X2,X3))))
| p12(X0,f16(f10(X1,f11(X2,X3)),c32,X4)) ),
inference(cnf_transformation,[status(esa)],[f40_sk]) ).
cnf(t47,plain,
ifeq(p22(f3(f4(f5(c26))),X1),true,ifeq(p23(X2,f8(f10(X3,f11(X1,X4)))),true,or(p12(X2,f16(f10(X3,f11(X1,X4)),c32,X5)),or(p23(f21(X3,X1,X4,X5,X2),f8(f10(X3,f11(X1,X4)))),p24(f17(f10(X3,f11(X1,X4)),f16(f10(X3,f11(X1,X4)),c32,X5))))),true),true) = true,
inference(equality_encoding,[status(esa)],[c40]) ).
cnf(t71,plain,
ifeq(p22(f3(f4(f5(c26))),X1),true,ifeq(p23(X2,f8(f10(X3,f11(X1,X4)))),true,or(p12(X2,f16(f10(X3,f11(X1,X4)),c32,X5)),or(p23(f21(X3,X1,X4,X5,X2),f8(f10(X3,f11(X1,X4)))),p24(f17(f10(X3,f11(X1,X4)),f16(f10(X3,f11(X1,X4)),c32,X5))))),true),true) = true,
inference(orient,[status(thm)],[t47]) ).
cnf(t148,plain,
true = ifeq(p22(f3(f4(f5(c26))),c27),true,ifeq(true,true,or(p12(c28,f16(f10(c29,f11(c27,c30)),c32,X1)),or(p23(f21(c29,c27,c30,X1,c28),f8(f10(c29,f11(c27,c30)))),p24(f17(f10(c29,f11(c27,c30)),f16(f10(c29,f11(c27,c30)),c32,X1))))),true),true),
inference(cp,[status(thm)],[t71,t141]) ).
cnf(t41004,plain,
true = ifeq(true,true,ifeq(true,true,or(p12(c28,f16(f10(c29,f11(c27,c30)),c32,X1)),or(p23(f21(c29,c27,c30,X1,c28),f8(f10(c29,f11(c27,c30)))),p24(f17(f10(c29,f11(c27,c30)),f16(f10(c29,f11(c27,c30)),c32,X1))))),true),true),
inference(step,[status(thm)],[t148,t149]) ).
cnf(t41005,plain,
true = ifeq(true,true,or(p12(c28,f16(f10(c29,f11(c27,c30)),c32,X1)),or(p23(f21(c29,c27,c30,X1,c28),f8(f10(c29,f11(c27,c30)))),p24(f17(f10(c29,f11(c27,c30)),f16(f10(c29,f11(c27,c30)),c32,X1))))),true),
inference(step,[status(thm)],[t41004,t49]) ).
cnf(t41006,plain,
true = or(p12(c28,f16(f10(c29,f11(c27,c30)),c32,X1)),or(p23(f21(c29,c27,c30,X1,c28),f8(f10(c29,f11(c27,c30)))),p24(f17(f10(c29,f11(c27,c30)),f16(f10(c29,f11(c27,c30)),c32,X1))))),
inference(step,[status(thm)],[t41005,t49]) ).
cnf(t39924,plain,
or(p12(c28,f16(f10(c29,f11(c27,c30)),c32,X1)),or(p23(f21(c29,c27,c30,X1,c28),f8(f10(c29,f11(c27,c30)))),p24(f17(f10(c29,f11(c27,c30)),f16(f10(c29,f11(c27,c30)),c32,X1))))) = true,
inference(orient,[status(thm)],[t41006]) ).
cnf(f21,negated_conjecture,
~ p12(c28,f16(f10(c29,f11(c27,c30)),c32,c31)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',not_p12_22) ).
fof(f21_nnf,plain,
~ p12(c28,f16(f10(c29,f11(c27,c30)),c32,c31)),
inference(nnf_transformation,[status(thm)],[f21]) ).
fof(f21_sk,plain,
~ p12(c28,f16(f10(c29,f11(c27,c30)),c32,c31)),
inference(skolemisation,[status(esa)],[f21_nnf]) ).
cnf(c21,plain,
~ p12(c28,f16(f10(c29,f11(c27,c30)),c32,c31)),
inference(cnf_transformation,[status(esa)],[f21_sk]) ).
cnf(t13,plain,
p12(c28,f16(f10(c29,f11(c27,c30)),c32,c31)) = false,
inference(equality_encoding,[status(esa)],[c21]) ).
cnf(t185,plain,
p12(c28,f16(f10(c29,f11(c27,c30)),c32,c31)) = false,
inference(orient,[status(thm)],[t13]) ).
cnf(t39925,plain,
true = or(false,or(p23(f21(c29,c27,c30,c31,c28),f8(f10(c29,f11(c27,c30)))),p24(f17(f10(c29,f11(c27,c30)),f16(f10(c29,f11(c27,c30)),c32,c31))))),
inference(cp,[status(thm)],[t39924,t185]) ).
cnf(t2,plain,
or(false,X1) = X1,
introduced(definition) ).
cnf(t51,plain,
or(false,X1) = X1,
inference(orient,[status(thm)],[t2]) ).
cnf(t41007,plain,
true = or(p23(f21(c29,c27,c30,c31,c28),f8(f10(c29,f11(c27,c30)))),p24(f17(f10(c29,f11(c27,c30)),f16(f10(c29,f11(c27,c30)),c32,c31)))),
inference(step,[status(thm)],[t39925,t51]) ).
cnf(f31,negated_conjecture,
~ p24(f17(f10(c29,f11(c27,c30)),f16(f10(c29,f11(c27,c30)),c32,c31))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',f17_is_not_p24_32) ).
fof(f31_nnf,plain,
~ p24(f17(f10(c29,f11(c27,c30)),f16(f10(c29,f11(c27,c30)),c32,c31))),
inference(nnf_transformation,[status(thm)],[f31]) ).
fof(f31_sk,plain,
~ p24(f17(f10(c29,f11(c27,c30)),f16(f10(c29,f11(c27,c30)),c32,c31))),
inference(skolemisation,[status(esa)],[f31_nnf]) ).
cnf(c31,plain,
~ p24(f17(f10(c29,f11(c27,c30)),f16(f10(c29,f11(c27,c30)),c32,c31))),
inference(cnf_transformation,[status(esa)],[f31_sk]) ).
cnf(t28,plain,
p24(f17(f10(c29,f11(c27,c30)),f16(f10(c29,f11(c27,c30)),c32,c31))) = false,
inference(equality_encoding,[status(esa)],[c31]) ).
cnf(t207,plain,
p24(f17(f10(c29,f11(c27,c30)),f16(f10(c29,f11(c27,c30)),c32,c31))) = false,
inference(orient,[status(thm)],[t28]) ).
cnf(t41008,plain,
true = or(p23(f21(c29,c27,c30,c31,c28),f8(f10(c29,f11(c27,c30)))),false),
inference(step,[status(thm)],[t41007,t207]) ).
cnf(t0,plain,
or(X1,false) = X1,
introduced(definition) ).
cnf(t50,plain,
or(X1,false) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t41009,plain,
true = p23(f21(c29,c27,c30,c31,c28),f8(f10(c29,f11(c27,c30)))),
inference(step,[status(thm)],[t41008,t50]) ).
cnf(t39927,plain,
p23(f21(c29,c27,c30,c31,c28),f8(f10(c29,f11(c27,c30)))) = true,
inference(orient,[status(thm)],[t41009]) ).
cnf(t39942,plain,
true = ifeq(true,true,p25(f13(f14(X1,f16(f10(c29,f11(c27,c30)),c32,X1))),f13(f14(X1,f21(c29,c27,c30,c31,c28)))),true),
inference(cp,[status(thm)],[t33017,t39927]) ).
cnf(t41018,plain,
true = p25(f13(f14(X1,f16(f10(c29,f11(c27,c30)),c32,X1))),f13(f14(X1,f21(c29,c27,c30,c31,c28)))),
inference(step,[status(thm)],[t39942,t49]) ).
cnf(t39960,plain,
p25(f13(f14(X1,f16(f10(c29,f11(c27,c30)),c32,X1))),f13(f14(X1,f21(c29,c27,c30,c31,c28)))) = true,
inference(orient,[status(thm)],[t41018]) ).
cnf(t39970,plain,
true = ifeq(true,true,p25(f13(f14(c31,c28)),f13(f14(c31,f21(c29,c27,c30,c31,c28)))),true),
inference(cp,[status(thm)],[t900,t39960]) ).
cnf(t41019,plain,
true = p25(f13(f14(c31,c28)),f13(f14(c31,f21(c29,c27,c30,c31,c28)))),
inference(step,[status(thm)],[t39970,t49]) ).
cnf(t39980,plain,
p25(f13(f14(c31,c28)),f13(f14(c31,f21(c29,c27,c30,c31,c28)))) = true,
inference(orient,[status(thm)],[t41019]) ).
cnf(t39992,plain,
true = ifeq(true,true,or(p12(c28,f16(f10(c29,f11(c27,c30)),c32,c31)),p24(f17(f10(c29,f11(c27,c30)),f16(f10(c29,f11(c27,c30)),c32,c31)))),true),
inference(cp,[status(thm)],[t38617,t39980]) ).
cnf(t41022,plain,
true = or(p12(c28,f16(f10(c29,f11(c27,c30)),c32,c31)),p24(f17(f10(c29,f11(c27,c30)),f16(f10(c29,f11(c27,c30)),c32,c31)))),
inference(step,[status(thm)],[t39992,t49]) ).
cnf(t41023,plain,
true = or(false,p24(f17(f10(c29,f11(c27,c30)),f16(f10(c29,f11(c27,c30)),c32,c31)))),
inference(step,[status(thm)],[t41022,t185]) ).
cnf(t41024,plain,
true = p24(f17(f10(c29,f11(c27,c30)),f16(f10(c29,f11(c27,c30)),c32,c31))),
inference(step,[status(thm)],[t41023,t51]) ).
cnf(t41025,plain,
true = false,
inference(step,[status(thm)],[t41024,t207]) ).
cnf(t40002,plain,
false = true,
inference(orient,[status(thm)],[t41025]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c21,c31]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t40002]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN645-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/0.37 % Computer : n026.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Fri Sep 25 02:01:09 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 30.29/4.29 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 30.29/4.29 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------