%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SYN644-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n005.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 55.69s 7.45s
% Output : Proof 55.69s
% Verified :
% SZS Type : Refutation
% Derivation depth : 31
% Number of leaves : 13
% Syntax : Number of formulae : 103 ( 83 unt; 0 def)
% Number of atoms : 163 ( 62 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 122 ( 62 ~; 60 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 2 avg)
% Maximal term depth : 8 ( 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 : 158 ( 2 sgn 46 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f22,negated_conjecture,
~ p12(c28,f16(f10(c29,f11(c27,c30)),c32,c31)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_p12_23) ).
fof(f22_nnf,plain,
~ p12(c28,f16(f10(c29,f11(c27,c30)),c32,c31)),
inference(nnf_transformation,[status(thm)],[f22]) ).
fof(f22_sk,plain,
~ p12(c28,f16(f10(c29,f11(c27,c30)),c32,c31)),
inference(skolemisation,[status(esa)],[f22_nnf]) ).
cnf(c22,plain,
~ p12(c28,f16(f10(c29,f11(c27,c30)),c32,c31)),
inference(cnf_transformation,[status(esa)],[f22_sk]) ).
cnf(t54,plain,
p12(c28,f16(f10(c29,f11(c27,c30)),c32,c31)) = false,
inference(equality_encoding,[status(esa)],[c22]) ).
cnf(t729,plain,
p12(c28,f16(f10(c29,f11(c27,c30)),c32,c31)) = false,
inference(orient,[status(thm)],[t54]) ).
cnf(f39,negated_conjecture,
( ~ p25(f13(f14(X7,X3)),f13(f14(X7,f21(X4,X5,X6,X7,X3))))
| ~ p23(X3,f8(f10(X4,f11(X5,X6))))
| ~ p24(f17(f10(X4,f11(X5,X6)),X3))
| ~ p22(f3(f4(f5(c26))),X5)
| p12(X3,f16(f10(X4,f11(X5,X6)),c32,X7)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p12_40) ).
fof(f39_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))))
| ~ p24(f17(f10(X4,f11(X5,X6)),X3))
| ~ p22(f3(f4(f5(c26))),X5)
| p12(X3,f16(f10(X4,f11(X5,X6)),c32,X7)) ),
inference(nnf_transformation,[status(thm)],[f39]) ).
fof(f39_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))))
| ~ p24(f17(f10(X4,f11(X5,X6)),X3))
| ~ p22(f3(f4(f5(c26))),X5)
| p12(X3,f16(f10(X4,f11(X5,X6)),c32,X7)) ),
inference(skolemisation,[status(esa)],[f39_nnf]) ).
cnf(c39,plain,
( ~ p25(f13(f14(X4,X0)),f13(f14(X4,f21(X1,X2,X3,X4,X0))))
| ~ p23(X0,f8(f10(X1,f11(X2,X3))))
| ~ p24(f17(f10(X1,f11(X2,X3)),X0))
| ~ p22(f3(f4(f5(c26))),X2)
| p12(X0,f16(f10(X1,f11(X2,X3)),c32,X4)) ),
inference(cnf_transformation,[status(esa)],[f39_sk]) ).
cnf(t253,plain,
ifeq(p22(f3(f4(f5(c26))),X1),true,ifeq(p24(f17(f10(X2,f11(X1,X3)),X4)),true,ifeq(p23(X4,f8(f10(X2,f11(X1,X3)))),true,ifeq(p25(f13(f14(X5,X4)),f13(f14(X5,f21(X2,X1,X3,X5,X4)))),true,p12(X4,f16(f10(X2,f11(X1,X3)),c32,X5)),true),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c39]) ).
cnf(t628,plain,
ifeq(p22(f3(f4(f5(c26))),X1),true,ifeq(p24(f17(f10(X2,f11(X1,X3)),X4)),true,ifeq(p23(X4,f8(f10(X2,f11(X1,X3)))),true,ifeq(p25(f13(f14(X5,X4)),f13(f14(X5,f21(X2,X1,X3,X5,X4)))),true,p12(X4,f16(f10(X2,f11(X1,X3)),c32,X5)),true),true),true),true) = true,
inference(orient,[status(thm)],[t253]) ).
cnf(f24,negated_conjecture,
( ~ p12(X68,X66)
| ~ p25(X68,X69)
| ~ p12(X69,X67)
| p25(X66,X67) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p25_25) ).
fof(f24_nnf,plain,
! [X66,X67,X69,X68] :
( ~ p12(X68,X66)
| ~ p25(X68,X69)
| ~ p12(X69,X67)
| p25(X66,X67) ),
inference(nnf_transformation,[status(thm)],[f24]) ).
fof(f24_sk,plain,
! [X66,X67,X69,X68] :
( ~ p12(X68,X66)
| ~ p25(X68,X69)
| ~ p12(X69,X67)
| p25(X66,X67) ),
inference(skolemisation,[status(esa)],[f24_nnf]) ).
cnf(c24,plain,
( ~ p12(X3,X0)
| ~ p25(X3,X2)
| ~ p12(X2,X1)
| p25(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f24_sk]) ).
cnf(t168,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)],[c24]) ).
cnf(t452,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)],[t168]) ).
cnf(f0,negated_conjecture,
p12(X0,X0),
file('/export/starexec/sandbox2/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(t259,plain,
p12(X1,X1) = true,
inference(orient,[status(thm)],[t4]) ).
cnf(t453,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)],[t452,t259]) ).
cnf(t10,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t256,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t10]) ).
cnf(t2035,plain,
true = ifeq(p25(X1,X2),true,ifeq(p12(X1,X3),true,p25(X3,X2),true),true),
inference(step,[status(thm)],[t453,t256]) ).
cnf(t956,plain,
ifeq(p25(X1,X2),true,ifeq(p12(X1,X3),true,p25(X3,X2),true),true) = true,
inference(orient,[status(thm)],[t2035]) ).
cnf(f16,negated_conjecture,
( ~ p12(X0,X2)
| ~ p12(X0,X1)
| p12(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p12_17) ).
fof(f16_nnf,plain,
! [X1,X2,X0] :
( ~ p12(X0,X2)
| ~ p12(X0,X1)
| p12(X1,X2) ),
inference(nnf_transformation,[status(thm)],[f16]) ).
fof(f16_sk,plain,
! [X1,X2,X0] :
( ~ p12(X0,X2)
| ~ p12(X0,X1)
| p12(X1,X2) ),
inference(skolemisation,[status(esa)],[f16_nnf]) ).
cnf(c16,plain,
( ~ p12(X2,X1)
| ~ p12(X2,X0)
| p12(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(hi16,negated_conjecture,
ifeq(p12(X0,X1),true,ifeq(p12(X0,X2),true,p12(X1,X2),true),true) = true,
inference(equality_encoding,[status(esa)],[c16]) ).
cnf(f32,negated_conjecture,
p12(f13(f14(c31,c28)),f13(f14(c31,f16(f10(c29,f11(c27,c30)),c32,c31)))),
file('/export/starexec/sandbox2/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(hi31,negated_conjecture,
p12(f13(f14(c31,c28)),f13(f14(c31,f16(f10(c29,f11(c27,c30)),c32,c31)))) = true,
inference(equality_encoding,[status(esa)],[c32]) ).
cnf(hi0,negated_conjecture,
p12(X0,X0) = true,
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t151,plain,
p12(f13(f14(c31,f16(f10(c29,f11(c27,c30)),c32,c31))),f13(f14(c31,c28))) = true,
inference(hyper_resolution,[status(thm)],[hi16,hi31,hi0]) ).
cnf(t261,plain,
p12(f13(f14(c31,f16(f10(c29,f11(c27,c30)),c32,c31))),f13(f14(c31,c28))) = true,
inference(orient,[status(thm)],[t151]) ).
cnf(t976,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)],[t956,t261]) ).
cnf(t2102,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)],[t976,t256]) ).
cnf(t1969,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)],[t2102]) ).
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/sandbox2/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(t246,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(t627,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)],[t246]) ).
cnf(f38,negated_conjecture,
( ~ p23(X3,f8(f10(X4,f11(X5,X6))))
| ~ p24(f17(f10(X4,f11(X5,X6)),X3))
| ~ p22(f3(f4(f5(c26))),X5)
| 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/sandbox2/benchmark/theBenchmark.p',p12_39) ).
fof(f38_nnf,plain,
! [X3,X4,X5,X6,X7] :
( ~ p23(X3,f8(f10(X4,f11(X5,X6))))
| ~ p24(f17(f10(X4,f11(X5,X6)),X3))
| ~ p22(f3(f4(f5(c26))),X5)
| 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)],[f38]) ).
fof(f38_sk,plain,
! [X3,X4,X5,X6,X7] :
( ~ p23(X3,f8(f10(X4,f11(X5,X6))))
| ~ p24(f17(f10(X4,f11(X5,X6)),X3))
| ~ p22(f3(f4(f5(c26))),X5)
| 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)],[f38_nnf]) ).
cnf(c38,plain,
( ~ p23(X0,f8(f10(X1,f11(X2,X3))))
| ~ p24(f17(f10(X1,f11(X2,X3)),X0))
| ~ p22(f3(f4(f5(c26))),X2)
| 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)],[f38_sk]) ).
cnf(hi37,negated_conjecture,
ifeq(p22(f3(f4(f5(c26))),X0),true,ifeq(p24(f17(f10(X1,f11(X0,X2)),X3)),true,ifeq(p23(X3,f8(f10(X1,f11(X0,X2)))),true,or(p12(X3,f16(f10(X1,f11(X0,X2)),c32,X4)),p23(f21(X1,X0,X2,X4,X3),f8(f10(X1,f11(X0,X2))))),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c38]) ).
cnf(f6,negated_conjecture,
p22(f3(f4(f5(c26))),c27),
file('/export/starexec/sandbox2/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(hi6,negated_conjecture,
p22(f3(f4(f5(c26))),c27) = true,
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(f8,negated_conjecture,
p24(f17(f10(c29,f11(c27,c30)),c28)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f17_is_p24_9) ).
fof(f8_nnf,plain,
p24(f17(f10(c29,f11(c27,c30)),c28)),
inference(nnf_transformation,[status(thm)],[f8]) ).
cnf(c8,plain,
p24(f17(f10(c29,f11(c27,c30)),c28)),
inference(cnf_transformation,[status(esa)],[f8_nnf]) ).
cnf(hi8,negated_conjecture,
p24(f17(f10(c29,f11(c27,c30)),c28)) = true,
inference(equality_encoding,[status(esa)],[c8]) ).
cnf(f9,negated_conjecture,
p23(c28,f8(f10(c29,f11(c27,c30)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p23_10) ).
fof(f9_nnf,plain,
p23(c28,f8(f10(c29,f11(c27,c30)))),
inference(nnf_transformation,[status(thm)],[f9]) ).
cnf(c9,plain,
p23(c28,f8(f10(c29,f11(c27,c30)))),
inference(cnf_transformation,[status(esa)],[f9_nnf]) ).
cnf(hi9,negated_conjecture,
p23(c28,f8(f10(c29,f11(c27,c30)))) = true,
inference(equality_encoding,[status(esa)],[c9]) ).
cnf(t184,plain,
or(p12(c28,f16(f10(c29,f11(c27,c30)),c32,X1)),p23(f21(c29,c27,c30,X1,c28),f8(f10(c29,f11(c27,c30))))) = true,
inference(hyper_resolution,[status(thm)],[hi37,hi6,hi8,hi9]) ).
cnf(t693,plain,
or(p12(c28,f16(f10(c29,f11(c27,c30)),c32,X1)),p23(f21(c29,c27,c30,X1,c28),f8(f10(c29,f11(c27,c30))))) = true,
inference(orient,[status(thm)],[t184]) ).
cnf(t743,plain,
true = or(false,p23(f21(c29,c27,c30,c31,c28),f8(f10(c29,f11(c27,c30))))),
inference(cp,[status(thm)],[t693,t729]) ).
cnf(t2,plain,
or(false,X1) = X1,
introduced(definition) ).
cnf(t258,plain,
or(false,X1) = X1,
inference(orient,[status(thm)],[t2]) ).
cnf(t2033,plain,
true = p23(f21(c29,c27,c30,c31,c28),f8(f10(c29,f11(c27,c30)))),
inference(step,[status(thm)],[t743,t258]) ).
cnf(t945,plain,
p23(f21(c29,c27,c30,c31,c28),f8(f10(c29,f11(c27,c30)))) = true,
inference(orient,[status(thm)],[t2033]) ).
cnf(t950,plain,
true = ifeq(p22(f3(f4(f5(c26))),c27),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),true),
inference(cp,[status(thm)],[t627,t945]) ).
cnf(t15,plain,
p22(f3(f4(f5(c26))),c27) = true,
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(t697,plain,
p22(f3(f4(f5(c26))),c27) = true,
inference(orient,[status(thm)],[t15]) ).
cnf(t2071,plain,
true = ifeq(true,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),true),
inference(step,[status(thm)],[t950,t697]) ).
cnf(t2072,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(step,[status(thm)],[t2071,t256]) ).
cnf(t2073,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)],[t2072,t256]) ).
cnf(t1451,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)],[t2073]) ).
cnf(t1970,plain,
true = ifeq(true,true,p25(f13(f14(c31,c28)),f13(f14(c31,f21(c29,c27,c30,c31,c28)))),true),
inference(cp,[status(thm)],[t1969,t1451]) ).
cnf(t2103,plain,
true = p25(f13(f14(c31,c28)),f13(f14(c31,f21(c29,c27,c30,c31,c28)))),
inference(step,[status(thm)],[t1970,t256]) ).
cnf(t1973,plain,
p25(f13(f14(c31,c28)),f13(f14(c31,f21(c29,c27,c30,c31,c28)))) = true,
inference(orient,[status(thm)],[t2103]) ).
cnf(t1983,plain,
true = ifeq(p22(f3(f4(f5(c26))),c27),true,ifeq(p24(f17(f10(c29,f11(c27,c30)),c28)),true,ifeq(p23(c28,f8(f10(c29,f11(c27,c30)))),true,ifeq(true,true,p12(c28,f16(f10(c29,f11(c27,c30)),c32,c31)),true),true),true),true),
inference(cp,[status(thm)],[t628,t1973]) ).
cnf(t2104,plain,
true = ifeq(true,true,ifeq(p24(f17(f10(c29,f11(c27,c30)),c28)),true,ifeq(p23(c28,f8(f10(c29,f11(c27,c30)))),true,ifeq(true,true,p12(c28,f16(f10(c29,f11(c27,c30)),c32,c31)),true),true),true),true),
inference(step,[status(thm)],[t1983,t697]) ).
cnf(t2105,plain,
true = ifeq(p24(f17(f10(c29,f11(c27,c30)),c28)),true,ifeq(p23(c28,f8(f10(c29,f11(c27,c30)))),true,ifeq(true,true,p12(c28,f16(f10(c29,f11(c27,c30)),c32,c31)),true),true),true),
inference(step,[status(thm)],[t2104,t256]) ).
cnf(t29,plain,
p24(f17(f10(c29,f11(c27,c30)),c28)) = true,
inference(equality_encoding,[status(esa)],[c8]) ).
cnf(t715,plain,
p24(f17(f10(c29,f11(c27,c30)),c28)) = true,
inference(orient,[status(thm)],[t29]) ).
cnf(t2106,plain,
true = ifeq(true,true,ifeq(p23(c28,f8(f10(c29,f11(c27,c30)))),true,ifeq(true,true,p12(c28,f16(f10(c29,f11(c27,c30)),c32,c31)),true),true),true),
inference(step,[status(thm)],[t2105,t715]) ).
cnf(t2107,plain,
true = ifeq(p23(c28,f8(f10(c29,f11(c27,c30)))),true,ifeq(true,true,p12(c28,f16(f10(c29,f11(c27,c30)),c32,c31)),true),true),
inference(step,[status(thm)],[t2106,t256]) ).
cnf(t28,plain,
p23(c28,f8(f10(c29,f11(c27,c30)))) = true,
inference(equality_encoding,[status(esa)],[c9]) ).
cnf(t680,plain,
p23(c28,f8(f10(c29,f11(c27,c30)))) = true,
inference(orient,[status(thm)],[t28]) ).
cnf(t2108,plain,
true = ifeq(true,true,ifeq(true,true,p12(c28,f16(f10(c29,f11(c27,c30)),c32,c31)),true),true),
inference(step,[status(thm)],[t2107,t680]) ).
cnf(t2109,plain,
true = ifeq(true,true,p12(c28,f16(f10(c29,f11(c27,c30)),c32,c31)),true),
inference(step,[status(thm)],[t2108,t256]) ).
cnf(t2110,plain,
true = p12(c28,f16(f10(c29,f11(c27,c30)),c32,c31)),
inference(step,[status(thm)],[t2109,t256]) ).
cnf(t2111,plain,
true = false,
inference(step,[status(thm)],[t2110,t729]) ).
cnf(t1985,plain,
false = true,
inference(orient,[status(thm)],[t2111]) ).
cnf(t2112,plain,
p12(c28,f16(f10(c29,f11(c27,c30)),c32,c31)) = true,
inference(step,[status(thm)],[t729,t1985]) ).
cnf(t1986,plain,
p12(c28,f16(f10(c29,f11(c27,c30)),c32,c31)) = true,
inference(orient,[status(thm)],[t2112]) ).
cnf(goal_0,negated_conjecture,
p12(c28,f16(f10(c29,f11(c27,c30)),c32,c31)) != true,
inference(equality_encoding,[status(esa)],[c22]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t1986]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN644-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.11/0.37 % Computer : n005.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Fri Sep 25 01:58:03 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 55.69/7.45 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 55.69/7.45 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------