%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GEO647+1 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n001.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 01:18:23 PM UTC 2026
% Result : Theorem 17.37s 2.80s
% Output : Proof 17.37s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 17
% Syntax : Number of formulae : 220 ( 152 unt; 0 def)
% Number of atoms : 344 ( 145 equ)
% Maximal formula atoms : 6 ( 1 avg)
% Number of connectives : 208 ( 84 ~; 78 |; 28 &)
% ( 0 <=>; 18 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-4 aty)
% Number of functors : 9 ( 9 usr; 8 con; 0-4 aty)
% Number of variables : 346 ( 0 sgn 209 !; 7 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f69,axiom,
! [A,B,C] :
( midp(A,B,C)
=> coll(A,B,C) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD69) ).
fof(f69_nnf,plain,
! [A,B,C] :
( coll(A,B,C)
| ~ midp(A,B,C) ),
inference(nnf_transformation,[status(thm)],[f69]) ).
fof(f69_sk,plain,
! [A,B,C] :
( coll(A,B,C)
| ~ midp(A,B,C) ),
inference(skolemisation,[status(esa)],[f69_nnf]) ).
cnf(c69,plain,
( coll(X0,X1,X2)
| ~ midp(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f69_sk]) ).
cnf(hi69,axiom,
ifeq(midp(X0,X1,X2),true,coll(X0,X1,X2),true) = true,
inference(equality_encoding,[status(esa)],[c69]) ).
fof(f94,conjecture,
! [A,B,C,D,E,F,G] :
( ( para(A,C,G,F)
& para(A,F,G,D)
& midp(F,C,B)
& midp(E,B,A)
& midp(D,A,C) )
=> para(C,E,G,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',exemplo6GDDFULLmoreE0156) ).
fof(f94_neg,negated_conjecture,
~ ! [A,B,C,D,E,F,G] :
( ( para(A,C,G,F)
& para(A,F,G,D)
& midp(F,C,B)
& midp(E,B,A)
& midp(D,A,C) )
=> para(C,E,G,B) ),
inference(negated_conjecture,[status(cth)],[f94]) ).
fof(f94_nnf,plain,
? [A,B,C,D,E,F,G] :
( ~ para(C,E,G,B)
& para(A,C,G,F)
& para(A,F,G,D)
& midp(F,C,B)
& midp(E,B,A)
& midp(D,A,C) ),
inference(nnf_transformation,[status(thm)],[f94_neg]) ).
fof(f94_sk,plain,
( ~ para(sk22,sk24,sk26,sk21)
& para(sk20,sk22,sk26,sk25)
& para(sk20,sk25,sk26,sk23)
& midp(sk25,sk22,sk21)
& midp(sk24,sk21,sk20)
& midp(sk23,sk20,sk22) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk20,sk21,sk22,sk23,sk24,sk25,sk26])],[f94_nnf]) ).
cnf(c114,plain,
midp(sk24,sk21,sk20),
inference(cnf_transformation,[status(esa)],[f94_sk]) ).
cnf(hi114,negated_conjecture,
midp(sk24,sk21,sk20) = true,
inference(equality_encoding,[status(esa)],[c114]) ).
cnf(h5,plain,
coll(sk24,sk21,sk20) = true,
inference(hyper_resolution,[status(thm)],[hi69,hi114]) ).
fof(f0,axiom,
! [A,B,C] :
( coll(A,B,C)
=> coll(A,C,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD1) ).
fof(f0_nnf,plain,
! [A,B,C] :
( coll(A,C,B)
| ~ coll(A,B,C) ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [A,B,C] :
( coll(A,C,B)
| ~ coll(A,B,C) ),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
( coll(X0,X2,X1)
| ~ coll(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(hi0,axiom,
ifeq(coll(X0,X1,X2),true,coll(X0,X2,X1),true) = true,
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(h27,plain,
coll(sk24,sk20,sk21) = true,
inference(hyper_resolution,[status(thm)],[hi0,h5]) ).
fof(f2,axiom,
! [A,B,C,D] :
( ( coll(A,B,D)
& coll(A,B,C) )
=> coll(C,D,A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD3) ).
fof(f2_nnf,plain,
! [A,B,C,D] :
( coll(C,D,A)
| ~ coll(A,B,D)
| ~ coll(A,B,C) ),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [A,B,C,D] :
( coll(C,D,A)
| ~ coll(A,B,D)
| ~ coll(A,B,C) ),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
( coll(X2,X3,X0)
| ~ coll(X0,X1,X3)
| ~ coll(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(hi2,axiom,
ifeq(coll(X0,X1,X2),true,ifeq(coll(X0,X1,X3),true,coll(X2,X3,X0),true),true) = true,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(h25,plain,
coll(sk20,sk20,sk24) = true,
inference(hyper_resolution,[status(thm)],[hi2,h5,h5]) ).
cnf(h51,plain,
coll(sk24,sk24,sk20) = true,
inference(hyper_resolution,[status(thm)],[hi2,h25,h25]) ).
cnf(h74,plain,
coll(sk24,sk20,sk24) = true,
inference(hyper_resolution,[status(thm)],[hi0,h51]) ).
cnf(h118,plain,
coll(sk24,sk21,sk24) = true,
inference(hyper_resolution,[status(thm)],[hi2,h74,h27]) ).
fof(f10,axiom,
! [A,B,M] :
( midp(M,B,A)
=> midp(M,A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD11) ).
fof(f10_nnf,plain,
! [A,B,M] :
( midp(M,A,B)
| ~ midp(M,B,A) ),
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
! [M,B,A] :
( midp(M,A,B)
| ~ midp(M,B,A) ),
inference(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c10,plain,
( midp(X2,X0,X1)
| ~ midp(X2,X1,X0) ),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(hi10,axiom,
ifeq(midp(X0,X1,X2),true,midp(X0,X2,X1),true) = true,
inference(equality_encoding,[status(esa)],[c10]) ).
cnf(h9,plain,
midp(sk24,sk20,sk21) = true,
inference(hyper_resolution,[status(thm)],[hi10,hi114]) ).
fof(f44,axiom,
! [A,B,C,E,F] :
( ( midp(F,A,C)
& midp(E,A,B) )
=> para(E,F,B,C) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD44) ).
fof(f44_nnf,plain,
! [A,B,C,E,F] :
( para(E,F,B,C)
| ~ midp(F,A,C)
| ~ midp(E,A,B) ),
inference(nnf_transformation,[status(thm)],[f44]) ).
fof(f44_sk,plain,
! [E,A,B,F,C] :
( para(E,F,B,C)
| ~ midp(F,A,C)
| ~ midp(E,A,B) ),
inference(skolemisation,[status(esa)],[f44_nnf]) ).
cnf(c44,plain,
( para(X3,X4,X1,X2)
| ~ midp(X4,X0,X2)
| ~ midp(X3,X0,X1) ),
inference(cnf_transformation,[status(esa)],[f44_sk]) ).
cnf(hi44,axiom,
ifeq(midp(X0,X1,X2),true,ifeq(midp(X3,X1,X4),true,para(X0,X3,X2,X4),true),true) = true,
inference(equality_encoding,[status(esa)],[c44]) ).
cnf(c113,plain,
midp(sk23,sk20,sk22),
inference(cnf_transformation,[status(esa)],[f94_sk]) ).
cnf(hi113,negated_conjecture,
midp(sk23,sk20,sk22) = true,
inference(equality_encoding,[status(esa)],[c113]) ).
cnf(h33,plain,
para(sk23,sk24,sk22,sk21) = true,
inference(hyper_resolution,[status(thm)],[hi44,hi113,h9]) ).
fof(f4,axiom,
! [A,B,C,D] :
( para(A,B,C,D)
=> para(C,D,A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD5) ).
fof(f4_nnf,plain,
! [A,B,C,D] :
( para(C,D,A,B)
| ~ para(A,B,C,D) ),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [A,B,C,D] :
( para(C,D,A,B)
| ~ para(A,B,C,D) ),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c4,plain,
( para(X2,X3,X0,X1)
| ~ para(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(hi4,axiom,
ifeq(para(X0,X1,X2,X3),true,para(X2,X3,X0,X1),true) = true,
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(h292,plain,
para(sk22,sk21,sk23,sk24) = true,
inference(hyper_resolution,[status(thm)],[hi4,h33]) ).
fof(f5,axiom,
! [A,B,C,D,E,F] :
( ( para(C,D,E,F)
& para(A,B,C,D) )
=> para(A,B,E,F) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD6) ).
fof(f5_nnf,plain,
! [A,B,C,D,E,F] :
( para(A,B,E,F)
| ~ para(C,D,E,F)
| ~ para(A,B,C,D) ),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [A,B,C,D,E,F] :
( para(A,B,E,F)
| ~ para(C,D,E,F)
| ~ para(A,B,C,D) ),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c5,plain,
( para(X0,X1,X4,X5)
| ~ para(X2,X3,X4,X5)
| ~ para(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(hi5,axiom,
ifeq(para(X0,X1,X2,X3),true,ifeq(para(X2,X3,X4,X5),true,para(X0,X1,X4,X5),true),true) = true,
inference(equality_encoding,[status(esa)],[c5]) ).
cnf(h547,plain,
para(sk23,sk24,sk23,sk24) = true,
inference(hyper_resolution,[status(thm)],[hi5,h33,h292]) ).
fof(f1,axiom,
! [A,B,C] :
( coll(A,B,C)
=> coll(B,A,C) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD2) ).
fof(f1_nnf,plain,
! [A,B,C] :
( coll(B,A,C)
| ~ coll(A,B,C) ),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [A,B,C] :
( coll(B,A,C)
| ~ coll(A,B,C) ),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
( coll(X1,X0,X2)
| ~ coll(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(hi1,axiom,
ifeq(coll(X0,X1,X2),true,coll(X1,X0,X2),true) = true,
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(h26,plain,
coll(sk21,sk24,sk20) = true,
inference(hyper_resolution,[status(thm)],[hi1,h5]) ).
cnf(h53,plain,
coll(sk20,sk20,sk21) = true,
inference(hyper_resolution,[status(thm)],[hi2,h26,h26]) ).
cnf(h0,plain,
coll(sk23,sk20,sk22) = true,
inference(hyper_resolution,[status(thm)],[hi69,hi113]) ).
cnf(h17,plain,
coll(sk23,sk22,sk20) = true,
inference(hyper_resolution,[status(thm)],[hi0,h0]) ).
cnf(h49,plain,
coll(sk20,sk20,sk23) = true,
inference(hyper_resolution,[status(thm)],[hi2,h17,h17]) ).
cnf(h78,plain,
coll(sk23,sk21,sk20) = true,
inference(hyper_resolution,[status(thm)],[hi2,h49,h53]) ).
cnf(h125,plain,
coll(sk23,sk20,sk21) = true,
inference(hyper_resolution,[status(thm)],[hi0,h78]) ).
cnf(h15,plain,
coll(sk22,sk22,sk23) = true,
inference(hyper_resolution,[status(thm)],[hi2,h0,h0]) ).
cnf(h45,plain,
coll(sk23,sk23,sk22) = true,
inference(hyper_resolution,[status(thm)],[hi2,h15,h15]) ).
cnf(h63,plain,
coll(sk23,sk22,sk23) = true,
inference(hyper_resolution,[status(thm)],[hi0,h45]) ).
cnf(h104,plain,
coll(sk23,sk20,sk23) = true,
inference(hyper_resolution,[status(thm)],[hi2,h63,h17]) ).
cnf(h166,plain,
coll(sk23,sk21,sk23) = true,
inference(hyper_resolution,[status(thm)],[hi2,h104,h125]) ).
cnf(h4,plain,
midp(sk23,sk22,sk20) = true,
inference(hyper_resolution,[status(thm)],[hi10,hi113]) ).
cnf(c115,plain,
midp(sk25,sk22,sk21),
inference(cnf_transformation,[status(esa)],[f94_sk]) ).
cnf(hi115,negated_conjecture,
midp(sk25,sk22,sk21) = true,
inference(equality_encoding,[status(esa)],[c115]) ).
cnf(h23,plain,
para(sk25,sk23,sk21,sk20) = true,
inference(hyper_resolution,[status(thm)],[hi44,hi115,h4]) ).
cnf(h279,plain,
para(sk21,sk20,sk25,sk23) = true,
inference(hyper_resolution,[status(thm)],[hi4,h23]) ).
cnf(h415,plain,
para(sk25,sk23,sk25,sk23) = true,
inference(hyper_resolution,[status(thm)],[hi5,h23,h279]) ).
cnf(h10,plain,
coll(sk25,sk22,sk21) = true,
inference(hyper_resolution,[status(thm)],[hi69,hi115]) ).
cnf(h35,plain,
coll(sk21,sk21,sk25) = true,
inference(hyper_resolution,[status(thm)],[hi2,h10,h10]) ).
cnf(h57,plain,
coll(sk25,sk25,sk21) = true,
inference(hyper_resolution,[status(thm)],[hi2,h35,h35]) ).
cnf(h24,plain,
para(sk23,sk25,sk20,sk21) = true,
inference(hyper_resolution,[status(thm)],[hi44,h4,hi115]) ).
cnf(h37,plain,
coll(sk25,sk21,sk22) = true,
inference(hyper_resolution,[status(thm)],[hi0,h10]) ).
cnf(h61,plain,
coll(sk22,sk22,sk25) = true,
inference(hyper_resolution,[status(thm)],[hi2,h37,h37]) ).
cnf(h16,plain,
coll(sk20,sk23,sk22) = true,
inference(hyper_resolution,[status(thm)],[hi1,h0]) ).
cnf(h47,plain,
coll(sk22,sk22,sk20) = true,
inference(hyper_resolution,[status(thm)],[hi2,h16,h16]) ).
cnf(h96,plain,
coll(sk20,sk25,sk22) = true,
inference(hyper_resolution,[status(thm)],[hi2,h47,h61]) ).
cnf(h143,plain,
coll(sk20,sk22,sk25) = true,
inference(hyper_resolution,[status(thm)],[hi0,h96]) ).
cnf(h48,plain,
coll(sk20,sk22,sk23) = true,
inference(hyper_resolution,[status(thm)],[hi0,h16]) ).
cnf(h209,plain,
coll(sk23,sk25,sk20) = true,
inference(hyper_resolution,[status(thm)],[hi2,h48,h143]) ).
cnf(c116,plain,
para(sk20,sk25,sk26,sk23),
inference(cnf_transformation,[status(esa)],[f94_sk]) ).
cnf(hi116,negated_conjecture,
para(sk20,sk25,sk26,sk23) = true,
inference(equality_encoding,[status(esa)],[c116]) ).
cnf(h249,plain,
para(sk26,sk23,sk20,sk25) = true,
inference(hyper_resolution,[status(thm)],[hi4,hi116]) ).
fof(f3,axiom,
! [A,B,C,D] :
( para(A,B,C,D)
=> para(A,B,D,C) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD4) ).
fof(f3_nnf,plain,
! [A,B,C,D] :
( para(A,B,D,C)
| ~ para(A,B,C,D) ),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [A,B,C,D] :
( para(A,B,D,C)
| ~ para(A,B,C,D) ),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
( para(X0,X1,X3,X2)
| ~ para(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(hi3,axiom,
ifeq(para(X0,X1,X2,X3),true,para(X0,X1,X3,X2),true) = true,
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(h311,plain,
para(sk26,sk23,sk25,sk20) = true,
inference(hyper_resolution,[status(thm)],[hi3,h249]) ).
cnf(h309,plain,
para(sk20,sk25,sk20,sk25) = true,
inference(hyper_resolution,[status(thm)],[hi5,hi116,h249]) ).
fof(f63,axiom,
! [A,B,C,D,M] :
( ( midp(M,C,D)
& midp(M,A,B) )
=> para(A,C,B,D) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD63) ).
fof(f63_nnf,plain,
! [A,B,C,D,M] :
( para(A,C,B,D)
| ~ midp(M,C,D)
| ~ midp(M,A,B) ),
inference(nnf_transformation,[status(thm)],[f63]) ).
fof(f63_sk,plain,
! [M,A,B,C,D] :
( para(A,C,B,D)
| ~ midp(M,C,D)
| ~ midp(M,A,B) ),
inference(skolemisation,[status(esa)],[f63_nnf]) ).
cnf(c63,plain,
( para(X0,X2,X1,X3)
| ~ midp(X4,X2,X3)
| ~ midp(X4,X0,X1) ),
inference(cnf_transformation,[status(esa)],[f63_sk]) ).
cnf(hi63,axiom,
ifeq(midp(X0,X1,X2),true,ifeq(midp(X0,X3,X4),true,para(X1,X3,X2,X4),true),true) = true,
inference(equality_encoding,[status(esa)],[c63]) ).
cnf(h20,plain,
para(sk20,sk22,sk22,sk20) = true,
inference(hyper_resolution,[status(thm)],[hi63,hi113,h4]) ).
cnf(h21,plain,
para(sk22,sk20,sk20,sk22) = true,
inference(hyper_resolution,[status(thm)],[hi63,h4,hi113]) ).
cnf(h276,plain,
para(sk22,sk20,sk22,sk20) = true,
inference(hyper_resolution,[status(thm)],[hi5,h21,h20]) ).
cnf(h46,plain,
coll(sk22,sk23,sk22) = true,
inference(hyper_resolution,[status(thm)],[hi0,h15]) ).
cnf(h310,plain,
para(sk26,sk23,sk26,sk23) = true,
inference(hyper_resolution,[status(thm)],[hi5,h249,hi116]) ).
fof(f66,axiom,
! [A,B,C] :
( para(A,B,A,C)
=> coll(A,B,C) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD66) ).
fof(f66_nnf,plain,
! [A,B,C] :
( coll(A,B,C)
| ~ para(A,B,A,C) ),
inference(nnf_transformation,[status(thm)],[f66]) ).
fof(f66_sk,plain,
! [A,B,C] :
( coll(A,B,C)
| ~ para(A,B,A,C) ),
inference(skolemisation,[status(esa)],[f66_nnf]) ).
cnf(c66,plain,
( coll(X0,X1,X2)
| ~ para(X0,X1,X0,X2) ),
inference(cnf_transformation,[status(esa)],[f66_sk]) ).
cnf(hi66,axiom,
ifeq(para(X0,X1,X0,X2),true,coll(X0,X1,X2),true) = true,
inference(equality_encoding,[status(esa)],[c66]) ).
cnf(h626,plain,
coll(sk26,sk23,sk23) = true,
inference(hyper_resolution,[status(thm)],[hi66,h310]) ).
cnf(h627,plain,
coll(sk23,sk23,sk26) = true,
inference(hyper_resolution,[status(thm)],[hi2,h626,h626]) ).
cnf(h634,plain,
coll(sk22,sk26,sk23) = true,
inference(hyper_resolution,[status(thm)],[hi2,h45,h627]) ).
cnf(h645,plain,
coll(sk22,sk23,sk26) = true,
inference(hyper_resolution,[status(thm)],[hi0,h634]) ).
cnf(h716,plain,
coll(sk26,sk22,sk22) = true,
inference(hyper_resolution,[status(thm)],[hi2,h645,h46]) ).
cnf(c117,plain,
para(sk20,sk22,sk26,sk25),
inference(cnf_transformation,[status(esa)],[f94_sk]) ).
cnf(hi117,negated_conjecture,
para(sk20,sk22,sk26,sk25) = true,
inference(equality_encoding,[status(esa)],[c117]) ).
cnf(h252,plain,
para(sk20,sk22,sk25,sk26) = true,
inference(hyper_resolution,[status(thm)],[hi3,hi117]) ).
cnf(h319,plain,
para(sk25,sk26,sk20,sk22) = true,
inference(hyper_resolution,[status(thm)],[hi4,h252]) ).
cnf(h98,plain,
coll(sk25,sk20,sk22) = true,
inference(hyper_resolution,[status(thm)],[hi2,h61,h47]) ).
cnf(h145,plain,
coll(sk25,sk22,sk20) = true,
inference(hyper_resolution,[status(thm)],[hi0,h98]) ).
cnf(h282,plain,
para(sk23,sk25,sk21,sk20) = true,
inference(hyper_resolution,[status(thm)],[hi3,h24]) ).
cnf(h14,plain,
midp(sk25,sk21,sk22) = true,
inference(hyper_resolution,[status(thm)],[hi10,hi115]) ).
cnf(h39,plain,
para(sk21,sk21,sk22,sk22) = true,
inference(hyper_resolution,[status(thm)],[hi63,h14,h14]) ).
cnf(h41,plain,
para(sk21,sk22,sk22,sk21) = true,
inference(hyper_resolution,[status(thm)],[hi63,h14,hi115]) ).
cnf(h36,plain,
coll(sk22,sk25,sk21) = true,
inference(hyper_resolution,[status(thm)],[hi1,h10]) ).
cnf(h59,plain,
coll(sk21,sk21,sk22) = true,
inference(hyper_resolution,[status(thm)],[hi2,h36,h36]) ).
cnf(h90,plain,
coll(sk22,sk22,sk21) = true,
inference(hyper_resolution,[status(thm)],[hi2,h59,h59]) ).
cnf(h137,plain,
coll(sk23,sk21,sk22) = true,
inference(hyper_resolution,[status(thm)],[hi2,h15,h90]) ).
cnf(h34,plain,
para(sk24,sk23,sk21,sk22) = true,
inference(hyper_resolution,[status(thm)],[hi44,h9,hi113]) ).
cnf(h55,plain,
coll(sk21,sk21,sk24) = true,
inference(hyper_resolution,[status(thm)],[hi2,h27,h27]) ).
cnf(h85,plain,
coll(sk21,sk24,sk21) = true,
inference(hyper_resolution,[status(thm)],[hi0,h55]) ).
cnf(h130,plain,
coll(sk24,sk21,sk21) = true,
inference(hyper_resolution,[status(thm)],[hi1,h85]) ).
fof(f68,axiom,
! [A,B,C] :
( midp(A,B,C)
=> cong(A,B,A,C) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD68) ).
fof(f68_nnf,plain,
! [A,B,C] :
( cong(A,B,A,C)
| ~ midp(A,B,C) ),
inference(nnf_transformation,[status(thm)],[f68]) ).
fof(f68_sk,plain,
! [A,B,C] :
( cong(A,B,A,C)
| ~ midp(A,B,C) ),
inference(skolemisation,[status(esa)],[f68_nnf]) ).
cnf(c68,plain,
( cong(X0,X1,X0,X2)
| ~ midp(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f68_sk]) ).
cnf(hi68,axiom,
ifeq(midp(X0,X1,X2),true,cong(X0,X1,X0,X2),true) = true,
inference(equality_encoding,[status(esa)],[c68]) ).
cnf(h28,plain,
cong(sk24,sk20,sk24,sk21) = true,
inference(hyper_resolution,[status(thm)],[hi68,h9]) ).
cnf(h6,plain,
cong(sk24,sk21,sk24,sk20) = true,
inference(hyper_resolution,[status(thm)],[hi68,hi114]) ).
fof(f24,axiom,
! [A,B,C,D,E,F] :
( ( cong(C,D,E,F)
& cong(A,B,C,D) )
=> cong(A,B,E,F) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD25) ).
fof(f24_nnf,plain,
! [A,B,C,D,E,F] :
( cong(A,B,E,F)
| ~ cong(C,D,E,F)
| ~ cong(A,B,C,D) ),
inference(nnf_transformation,[status(thm)],[f24]) ).
fof(f24_sk,plain,
! [A,B,C,D,E,F] :
( cong(A,B,E,F)
| ~ cong(C,D,E,F)
| ~ cong(A,B,C,D) ),
inference(skolemisation,[status(esa)],[f24_nnf]) ).
cnf(c24,plain,
( cong(X0,X1,X4,X5)
| ~ cong(X2,X3,X4,X5)
| ~ cong(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(esa)],[f24_sk]) ).
cnf(hi24,axiom,
ifeq(cong(X0,X1,X2,X3),true,ifeq(cong(X2,X3,X4,X5),true,cong(X0,X1,X4,X5),true),true) = true,
inference(equality_encoding,[status(esa)],[c24]) ).
cnf(h283,plain,
cong(sk24,sk21,sk24,sk21) = true,
inference(hyper_resolution,[status(thm)],[hi24,h6,h28]) ).
fof(f67,axiom,
! [A,B,C] :
( ( coll(A,B,C)
& cong(A,B,A,C) )
=> midp(A,B,C) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD67) ).
fof(f67_nnf,plain,
! [A,B,C] :
( midp(A,B,C)
| ~ coll(A,B,C)
| ~ cong(A,B,A,C) ),
inference(nnf_transformation,[status(thm)],[f67]) ).
fof(f67_sk,plain,
! [A,B,C] :
( midp(A,B,C)
| ~ coll(A,B,C)
| ~ cong(A,B,A,C) ),
inference(skolemisation,[status(esa)],[f67_nnf]) ).
cnf(c67,plain,
( midp(X0,X1,X2)
| ~ coll(X0,X1,X2)
| ~ cong(X0,X1,X0,X2) ),
inference(cnf_transformation,[status(esa)],[f67_sk]) ).
cnf(hi67,axiom,
ifeq(cong(X0,X1,X0,X2),true,ifeq(coll(X0,X1,X2),true,midp(X0,X1,X2),true),true) = true,
inference(equality_encoding,[status(esa)],[c67]) ).
cnf(h430,plain,
midp(sk24,sk21,sk21) = true,
inference(hyper_resolution,[status(thm)],[hi67,h283,h130]) ).
fof(f45,axiom,
! [A,B,C,E,F] :
( ( coll(F,A,C)
& para(E,F,B,C)
& midp(E,A,B) )
=> midp(F,A,C) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD45) ).
fof(f45_nnf,plain,
! [A,B,C,E,F] :
( midp(F,A,C)
| ~ coll(F,A,C)
| ~ para(E,F,B,C)
| ~ midp(E,A,B) ),
inference(nnf_transformation,[status(thm)],[f45]) ).
fof(f45_sk,plain,
! [E,A,B,F,C] :
( midp(F,A,C)
| ~ coll(F,A,C)
| ~ para(E,F,B,C)
| ~ midp(E,A,B) ),
inference(skolemisation,[status(esa)],[f45_nnf]) ).
cnf(c45,plain,
( midp(X4,X0,X2)
| ~ coll(X4,X0,X2)
| ~ para(X3,X4,X1,X2)
| ~ midp(X3,X0,X1) ),
inference(cnf_transformation,[status(esa)],[f45_sk]) ).
cnf(hi45,axiom,
ifeq(midp(X0,X1,X2),true,ifeq(para(X0,X3,X2,X4),true,ifeq(coll(X3,X1,X4),true,midp(X3,X1,X4),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c45]) ).
cnf(h450,plain,
midp(sk23,sk21,sk22) = true,
inference(hyper_resolution,[status(thm)],[hi45,h430,h34,h137]) ).
fof(f64,axiom,
! [A,B,C,D,M] :
( ( para(A,D,B,C)
& para(A,C,B,D)
& midp(M,A,B) )
=> midp(M,C,D) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD64) ).
fof(f64_nnf,plain,
! [A,B,C,D,M] :
( midp(M,C,D)
| ~ para(A,D,B,C)
| ~ para(A,C,B,D)
| ~ midp(M,A,B) ),
inference(nnf_transformation,[status(thm)],[f64]) ).
fof(f64_sk,plain,
! [M,A,B,C,D] :
( midp(M,C,D)
| ~ para(A,D,B,C)
| ~ para(A,C,B,D)
| ~ midp(M,A,B) ),
inference(skolemisation,[status(esa)],[f64_nnf]) ).
cnf(c64,plain,
( midp(X4,X2,X3)
| ~ para(X0,X3,X1,X2)
| ~ para(X0,X2,X1,X3)
| ~ midp(X4,X0,X1) ),
inference(cnf_transformation,[status(esa)],[f64_sk]) ).
cnf(hi64,axiom,
ifeq(midp(X0,X1,X2),true,ifeq(para(X1,X3,X2,X4),true,ifeq(para(X1,X4,X2,X3),true,midp(X0,X3,X4),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c64]) ).
cnf(h462,plain,
midp(sk23,sk22,sk21) = true,
inference(hyper_resolution,[status(thm)],[hi64,h450,h41,h39]) ).
cnf(h490,plain,
midp(sk25,sk22,sk20) = true,
inference(hyper_resolution,[status(thm)],[hi45,h462,h282,h145]) ).
cnf(h1605,plain,
midp(sk26,sk22,sk22) = true,
inference(hyper_resolution,[status(thm)],[hi45,h490,h319,h716]) ).
cnf(h1627,plain,
midp(sk26,sk20,sk20) = true,
inference(hyper_resolution,[status(thm)],[hi64,h1605,h276,h276]) ).
cnf(h1666,plain,
midp(sk26,sk25,sk25) = true,
inference(hyper_resolution,[status(thm)],[hi64,h1627,h309,h309]) ).
cnf(h1732,plain,
midp(sk23,sk25,sk20) = true,
inference(hyper_resolution,[status(thm)],[hi45,h1666,h311,h209]) ).
cnf(h1785,plain,
midp(sk25,sk25,sk21) = true,
inference(hyper_resolution,[status(thm)],[hi45,h1732,h24,h57]) ).
cnf(h1819,plain,
midp(sk25,sk21,sk25) = true,
inference(hyper_resolution,[status(thm)],[hi10,h1785]) ).
cnf(h2329,plain,
midp(sk23,sk21,sk23) = true,
inference(hyper_resolution,[status(thm)],[hi45,h1819,h415,h166]) ).
cnf(h2539,plain,
midp(sk24,sk21,sk24) = true,
inference(hyper_resolution,[status(thm)],[hi45,h2329,h547,h118]) ).
cnf(h2753,plain,
midp(sk24,sk24,sk21) = true,
inference(hyper_resolution,[status(thm)],[hi10,h2539]) ).
cnf(h70,plain,
coll(sk24,sk23,sk20) = true,
inference(hyper_resolution,[status(thm)],[hi2,h25,h49]) ).
cnf(h112,plain,
coll(sk24,sk20,sk23) = true,
inference(hyper_resolution,[status(thm)],[hi0,h70]) ).
cnf(h66,plain,
coll(sk20,sk20,sk22) = true,
inference(hyper_resolution,[status(thm)],[hi2,h47,h47]) ).
cnf(h108,plain,
coll(sk24,sk22,sk20) = true,
inference(hyper_resolution,[status(thm)],[hi2,h25,h66]) ).
cnf(h147,plain,
coll(sk24,sk20,sk22) = true,
inference(hyper_resolution,[status(thm)],[hi0,h108]) ).
cnf(h232,plain,
coll(sk22,sk23,sk24) = true,
inference(hyper_resolution,[status(thm)],[hi2,h147,h112]) ).
cnf(h706,plain,
coll(sk24,sk26,sk22) = true,
inference(hyper_resolution,[status(thm)],[hi2,h232,h645]) ).
cnf(h44,plain,
para(sk25,sk24,sk22,sk20) = true,
inference(hyper_resolution,[status(thm)],[hi44,h14,hi114]) ).
cnf(h307,plain,
para(sk25,sk24,sk20,sk22) = true,
inference(hyper_resolution,[status(thm)],[hi5,h44,h21]) ).
cnf(h68,plain,
coll(sk23,sk23,sk20) = true,
inference(hyper_resolution,[status(thm)],[hi2,h48,h48]) ).
cnf(h638,plain,
coll(sk26,sk20,sk23) = true,
inference(hyper_resolution,[status(thm)],[hi2,h627,h68]) ).
cnf(h649,plain,
coll(sk26,sk23,sk20) = true,
inference(hyper_resolution,[status(thm)],[hi0,h638]) ).
cnf(h99,plain,
coll(sk25,sk23,sk22) = true,
inference(hyper_resolution,[status(thm)],[hi2,h61,h15]) ).
cnf(h146,plain,
coll(sk25,sk22,sk23) = true,
inference(hyper_resolution,[status(thm)],[hi0,h99]) ).
cnf(h224,plain,
coll(sk23,sk23,sk25) = true,
inference(hyper_resolution,[status(thm)],[hi2,h146,h146]) ).
cnf(h635,plain,
coll(sk26,sk25,sk23) = true,
inference(hyper_resolution,[status(thm)],[hi2,h627,h224]) ).
cnf(h646,plain,
coll(sk26,sk23,sk25) = true,
inference(hyper_resolution,[status(thm)],[hi0,h635]) ).
cnf(h736,plain,
coll(sk25,sk20,sk26) = true,
inference(hyper_resolution,[status(thm)],[hi2,h646,h649]) ).
cnf(h251,plain,
para(sk26,sk25,sk20,sk22) = true,
inference(hyper_resolution,[status(thm)],[hi4,hi117]) ).
cnf(h316,plain,
para(sk26,sk25,sk25,sk26) = true,
inference(hyper_resolution,[status(thm)],[hi5,h251,h252]) ).
cnf(h211,plain,
coll(sk25,sk23,sk20) = true,
inference(hyper_resolution,[status(thm)],[hi2,h143,h48]) ).
cnf(h630,plain,
coll(sk25,sk26,sk23) = true,
inference(hyper_resolution,[status(thm)],[hi2,h224,h627]) ).
cnf(h641,plain,
coll(sk25,sk23,sk26) = true,
inference(hyper_resolution,[status(thm)],[hi0,h630]) ).
cnf(h663,plain,
coll(sk26,sk20,sk25) = true,
inference(hyper_resolution,[status(thm)],[hi2,h641,h211]) ).
cnf(h250,plain,
para(sk20,sk25,sk23,sk26) = true,
inference(hyper_resolution,[status(thm)],[hi3,hi116]) ).
cnf(h313,plain,
para(sk23,sk26,sk20,sk25) = true,
inference(hyper_resolution,[status(thm)],[hi4,h250]) ).
cnf(h72,plain,
coll(sk20,sk23,sk20) = true,
inference(hyper_resolution,[status(thm)],[hi0,h49]) ).
cnf(h115,plain,
coll(sk23,sk20,sk20) = true,
inference(hyper_resolution,[status(thm)],[hi1,h72]) ).
cnf(h18,plain,
cong(sk23,sk22,sk23,sk20) = true,
inference(hyper_resolution,[status(thm)],[hi68,h4]) ).
cnf(h1,plain,
cong(sk23,sk20,sk23,sk22) = true,
inference(hyper_resolution,[status(thm)],[hi68,hi113]) ).
cnf(h268,plain,
cong(sk23,sk20,sk23,sk20) = true,
inference(hyper_resolution,[status(thm)],[hi24,h1,h18]) ).
cnf(h347,plain,
midp(sk23,sk20,sk20) = true,
inference(hyper_resolution,[status(thm)],[hi67,h268,h115]) ).
cnf(h756,plain,
midp(sk26,sk20,sk25) = true,
inference(hyper_resolution,[status(thm)],[hi45,h347,h313,h663]) ).
cnf(h1057,plain,
midp(sk25,sk20,sk26) = true,
inference(hyper_resolution,[status(thm)],[hi45,h756,h316,h736]) ).
cnf(h1140,plain,
midp(sk25,sk26,sk20) = true,
inference(hyper_resolution,[status(thm)],[hi10,h1057]) ).
cnf(h1237,plain,
midp(sk24,sk26,sk22) = true,
inference(hyper_resolution,[status(thm)],[hi45,h1140,h307,h706]) ).
cnf(h1272,plain,
midp(sk24,sk22,sk26) = true,
inference(hyper_resolution,[status(thm)],[hi10,h1237]) ).
cnf(t113,plain,
para(sk22,sk24,sk26,sk21) = true,
inference(hyper_resolution,[status(thm)],[hi63,h1272,h2753]) ).
cnf(t2986,plain,
para(sk22,sk24,sk26,sk21) = true,
inference(orient,[status(thm)],[t113]) ).
cnf(c118,plain,
~ para(sk22,sk24,sk26,sk21),
inference(cnf_transformation,[status(esa)],[f94_sk]) ).
cnf(goal_0,negated_conjecture,
para(sk22,sk24,sk26,sk21) != true,
inference(equality_encoding,[status(esa)],[c118]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t2986]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO647+1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/0.36 % Computer : n001.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Wed Sep 23 12:44:51 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 17.37/2.80 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 17.37/2.80 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------