%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GEO634+1 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n007.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:21 PM UTC 2026
% Result : Theorem 150.21s 19.64s
% Output : Proof 150.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 85
% Number of leaves : 28
% Syntax : Number of formulae : 310 ( 202 unt; 0 def)
% Number of atoms : 536 ( 197 equ)
% Maximal formula atoms : 13 ( 1 avg)
% Number of connectives : 361 ( 135 ~; 129 |; 69 &)
% ( 0 <=>; 28 =>; 0 <=; 0 <~>)
% Maximal formula depth : 26 ( 3 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 11 ( 9 usr; 1 prp; 0-8 aty)
% Number of functors : 15 ( 15 usr; 13 con; 0-6 aty)
% Number of variables : 1054 ( 127 sgn 417 !; 14 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f56,axiom,
! [A,B,P,Q] :
( ( cong(A,Q,B,Q)
& cong(A,P,B,P) )
=> perp(A,B,P,Q) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ruleD56) ).
fof(f56_nnf,plain,
! [A,B,P,Q] :
( perp(A,B,P,Q)
| ~ cong(A,Q,B,Q)
| ~ cong(A,P,B,P) ),
inference(nnf_transformation,[status(thm)],[f56]) ).
fof(f56_sk,plain,
! [A,P,B,Q] :
( perp(A,B,P,Q)
| ~ cong(A,Q,B,Q)
| ~ cong(A,P,B,P) ),
inference(skolemisation,[status(esa)],[f56_nnf]) ).
cnf(c56,plain,
( perp(X0,X1,X2,X3)
| ~ cong(X0,X3,X1,X3)
| ~ cong(X0,X2,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f56_sk]) ).
cnf(t158,plain,
ifeq(cong(X1,X2,X3,X2),true,ifeq(cong(X1,X4,X3,X4),true,perp(X1,X3,X2,X4),true),true) = true,
inference(equality_encoding,[status(esa)],[c56]) ).
cnf(t271,plain,
ifeq(cong(X1,X2,X3,X2),true,ifeq(cong(X1,X4,X3,X4),true,perp(X1,X3,X2,X4),true),true) = true,
inference(orient,[status(thm)],[t158]) ).
fof(f22,axiom,
! [A,B,C,D] :
( cong(A,B,C,D)
=> cong(A,B,D,C) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ruleD23) ).
fof(f22_nnf,plain,
! [A,B,C,D] :
( cong(A,B,D,C)
| ~ cong(A,B,C,D) ),
inference(nnf_transformation,[status(thm)],[f22]) ).
fof(f22_sk,plain,
! [A,B,C,D] :
( cong(A,B,D,C)
| ~ cong(A,B,C,D) ),
inference(skolemisation,[status(esa)],[f22_nnf]) ).
cnf(c22,plain,
( cong(X0,X1,X3,X2)
| ~ cong(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(esa)],[f22_sk]) ).
cnf(t108,plain,
ifeq(cong(X1,X2,X3,X4),true,cong(X1,X2,X4,X3),true) = true,
inference(equality_encoding,[status(esa)],[c22]) ).
cnf(t268,plain,
ifeq(cong(X1,X2,X3,X4),true,cong(X1,X2,X4,X3),true) = true,
inference(orient,[status(thm)],[t108]) ).
fof(f23,axiom,
! [A,B,C,D] :
( cong(A,B,C,D)
=> cong(C,D,A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ruleD24) ).
fof(f23_nnf,plain,
! [A,B,C,D] :
( cong(C,D,A,B)
| ~ cong(A,B,C,D) ),
inference(nnf_transformation,[status(thm)],[f23]) ).
fof(f23_sk,plain,
! [A,B,C,D] :
( cong(C,D,A,B)
| ~ cong(A,B,C,D) ),
inference(skolemisation,[status(esa)],[f23_nnf]) ).
cnf(c23,plain,
( cong(X2,X3,X0,X1)
| ~ cong(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(esa)],[f23_sk]) ).
cnf(t109,plain,
ifeq(cong(X1,X2,X3,X4),true,cong(X3,X4,X1,X2),true) = true,
inference(equality_encoding,[status(esa)],[c23]) ).
cnf(t266,plain,
ifeq(cong(X1,X2,X3,X4),true,cong(X3,X4,X1,X2),true) = true,
inference(orient,[status(thm)],[t109]) ).
fof(f68,axiom,
! [A,B,C] :
( midp(A,B,C)
=> cong(A,B,A,C) ),
file('/export/starexec/sandbox2/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(t106,plain,
ifeq(midp(X1,X2,X3),true,cong(X1,X2,X1,X3),true) = true,
inference(equality_encoding,[status(esa)],[c68]) ).
cnf(t336,plain,
ifeq(midp(X1,X2,X3),true,cong(X1,X2,X1,X3),true) = true,
inference(orient,[status(thm)],[t106]) ).
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/sandbox2/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(t217,plain,
ifeq(midp(X1,X2,X3),true,ifeq(para(X2,X4,X3,X5),true,ifeq(para(X2,X5,X3,X4),true,midp(X1,X4,X5),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c64]) ).
cnf(t333,plain,
ifeq(midp(X1,X2,X3),true,ifeq(para(X2,X4,X3,X5),true,ifeq(para(X2,X5,X3,X4),true,midp(X1,X4,X5),true),true),true) = true,
inference(orient,[status(thm)],[t217]) ).
fof(f8,axiom,
! [A,B,C,D,E,F] :
( ( perp(C,D,E,F)
& perp(A,B,C,D) )
=> para(A,B,E,F) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ruleD9) ).
fof(f8_nnf,plain,
! [A,B,C,D,E,F] :
( para(A,B,E,F)
| ~ perp(C,D,E,F)
| ~ perp(A,B,C,D) ),
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [A,B,C,D,E,F] :
( para(A,B,E,F)
| ~ perp(C,D,E,F)
| ~ perp(A,B,C,D) ),
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c8,plain,
( para(X0,X1,X4,X5)
| ~ perp(X2,X3,X4,X5)
| ~ perp(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(t171,plain,
ifeq(perp(X1,X2,X3,X4),true,ifeq(perp(X3,X4,X5,X6),true,para(X1,X2,X5,X6),true),true) = true,
inference(equality_encoding,[status(esa)],[c8]) ).
cnf(t285,plain,
ifeq(perp(X1,X2,X3,X4),true,ifeq(perp(X3,X4,X5,X6),true,para(X1,X2,X5,X6),true),true) = true,
inference(orient,[status(thm)],[t171]) ).
fof(f7,axiom,
! [A,B,C,D] :
( perp(A,B,C,D)
=> perp(C,D,A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ruleD8) ).
fof(f7_nnf,plain,
! [A,B,C,D] :
( perp(C,D,A,B)
| ~ perp(A,B,C,D) ),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [A,B,C,D] :
( perp(C,D,A,B)
| ~ perp(A,B,C,D) ),
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c7,plain,
( perp(X2,X3,X0,X1)
| ~ perp(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(t116,plain,
ifeq(perp(X1,X2,X3,X4),true,perp(X3,X4,X1,X2),true) = true,
inference(equality_encoding,[status(esa)],[c7]) ).
cnf(t292,plain,
ifeq(perp(X1,X2,X3,X4),true,perp(X3,X4,X1,X2),true) = true,
inference(orient,[status(thm)],[t116]) ).
fof(f38,axiom,
! [A,B,C,D,P,Q] :
( eqangle(A,B,P,Q,C,D,P,Q)
=> para(A,B,C,D) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ruleD39) ).
fof(f38_nnf,plain,
! [A,B,C,D,P,Q] :
( para(A,B,C,D)
| ~ eqangle(A,B,P,Q,C,D,P,Q) ),
inference(nnf_transformation,[status(thm)],[f38]) ).
fof(f38_sk,plain,
! [A,B,P,Q,C,D] :
( para(A,B,C,D)
| ~ eqangle(A,B,P,Q,C,D,P,Q) ),
inference(skolemisation,[status(esa)],[f38_nnf]) ).
cnf(c38,plain,
( para(X0,X1,X2,X3)
| ~ eqangle(X0,X1,X4,X5,X2,X3,X4,X5) ),
inference(cnf_transformation,[status(esa)],[f38_sk]) ).
cnf(t143,plain,
ifeq(eqangle(X1,X2,X3,X4,X5,X6,X3,X4),true,para(X1,X2,X5,X6),true) = true,
inference(equality_encoding,[status(esa)],[c38]) ).
cnf(t314,plain,
ifeq(eqangle(X1,X2,X3,X4,X5,X6,X3,X4),true,para(X1,X2,X5,X6),true) = true,
inference(orient,[status(thm)],[t143]) ).
fof(f18,axiom,
! [A,B,C,D,P,Q,U,V] :
( eqangle(A,B,C,D,P,Q,U,V)
=> eqangle(C,D,A,B,U,V,P,Q) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ruleD19) ).
fof(f18_nnf,plain,
! [A,B,C,D,P,Q,U,V] :
( eqangle(C,D,A,B,U,V,P,Q)
| ~ eqangle(A,B,C,D,P,Q,U,V) ),
inference(nnf_transformation,[status(thm)],[f18]) ).
fof(f18_sk,plain,
! [A,B,C,D,P,Q,U,V] :
( eqangle(C,D,A,B,U,V,P,Q)
| ~ eqangle(A,B,C,D,P,Q,U,V) ),
inference(skolemisation,[status(esa)],[f18_nnf]) ).
cnf(c18,plain,
( eqangle(X2,X3,X0,X1,X6,X7,X4,X5)
| ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7) ),
inference(cnf_transformation,[status(esa)],[f18_sk]) ).
cnf(t163,plain,
ifeq(eqangle(X1,X2,X3,X4,X5,X6,X7,X8),true,eqangle(X3,X4,X1,X2,X7,X8,X5,X6),true) = true,
inference(equality_encoding,[status(esa)],[c18]) ).
cnf(t308,plain,
ifeq(eqangle(X1,X2,X3,X4,X5,X6,X7,X8),true,eqangle(X3,X4,X1,X2,X7,X8,X5,X6),true) = true,
inference(orient,[status(thm)],[t163]) ).
cnf(hi7,axiom,
ifeq(perp(X0,X1,X2,X3),true,perp(X2,X3,X0,X1),true) = true,
inference(equality_encoding,[status(esa)],[c7]) ).
fof(f94,conjecture,
! [A,B,C,O,A1,P,Q,S,D,G,NWPNT1,NWPNT2] :
( ( coll(G,A,B)
& perp(G,Q,A,B)
& coll(D,B,C)
& perp(D,Q,B,C)
& coll(S,A,Q)
& coll(S,B,C)
& circle(O,A,Q,NWPNT2)
& eqangle(Q,A,A,B,C,A,A,A1)
& coll(P,A,A1)
& circle(O,A,P,NWPNT1)
& midp(A1,C,B)
& circle(O,A,B,C) )
=> perp(D,G,P,A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',exemplo6GDDFULL8110997) ).
fof(f94_neg,negated_conjecture,
~ ! [A,B,C,O,A1,P,Q,S,D,G,NWPNT1,NWPNT2] :
( ( coll(G,A,B)
& perp(G,Q,A,B)
& coll(D,B,C)
& perp(D,Q,B,C)
& coll(S,A,Q)
& coll(S,B,C)
& circle(O,A,Q,NWPNT2)
& eqangle(Q,A,A,B,C,A,A,A1)
& coll(P,A,A1)
& circle(O,A,P,NWPNT1)
& midp(A1,C,B)
& circle(O,A,B,C) )
=> perp(D,G,P,A) ),
inference(negated_conjecture,[status(cth)],[f94]) ).
fof(f94_nnf,plain,
? [A,B,C,O,A1,P,Q,S,D,G,NWPNT1,NWPNT2] :
( ~ perp(D,G,P,A)
& coll(G,A,B)
& perp(G,Q,A,B)
& coll(D,B,C)
& perp(D,Q,B,C)
& coll(S,A,Q)
& coll(S,B,C)
& circle(O,A,Q,NWPNT2)
& eqangle(Q,A,A,B,C,A,A,A1)
& coll(P,A,A1)
& circle(O,A,P,NWPNT1)
& midp(A1,C,B)
& circle(O,A,B,C) ),
inference(nnf_transformation,[status(thm)],[f94_neg]) ).
fof(f94_sk,plain,
( ~ perp(sk28,sk29,sk25,sk20)
& coll(sk29,sk20,sk21)
& perp(sk29,sk26,sk20,sk21)
& coll(sk28,sk21,sk22)
& perp(sk28,sk26,sk21,sk22)
& coll(sk27,sk20,sk26)
& coll(sk27,sk21,sk22)
& circle(sk23,sk20,sk26,sk31)
& eqangle(sk26,sk20,sk20,sk21,sk22,sk20,sk20,sk24)
& coll(sk25,sk20,sk24)
& circle(sk23,sk20,sk25,sk30)
& midp(sk24,sk22,sk21)
& circle(sk23,sk20,sk21,sk22) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk20,sk21,sk22,sk23,sk24,sk25,sk26,sk27,sk28,sk29,sk30,sk31])],[f94_nnf]) ).
cnf(c123,plain,
perp(sk29,sk26,sk20,sk21),
inference(cnf_transformation,[status(esa)],[f94_sk]) ).
cnf(hi123,negated_conjecture,
perp(sk29,sk26,sk20,sk21) = true,
inference(equality_encoding,[status(esa)],[c123]) ).
cnf(h30,plain,
perp(sk20,sk21,sk29,sk26) = true,
inference(hyper_resolution,[status(thm)],[hi7,hi123]) ).
cnf(hi8,axiom,
ifeq(perp(X0,X1,X2,X3),true,ifeq(perp(X2,X3,X4,X5),true,para(X0,X1,X4,X5),true),true) = true,
inference(equality_encoding,[status(esa)],[c8]) ).
cnf(h146,plain,
para(sk20,sk21,sk20,sk21) = true,
inference(hyper_resolution,[status(thm)],[hi8,h30,hi123]) ).
fof(f39,axiom,
! [A,B,C,D,P,Q] :
( para(A,B,C,D)
=> eqangle(A,B,P,Q,C,D,P,Q) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ruleD40) ).
fof(f39_nnf,plain,
! [A,B,C,D,P,Q] :
( eqangle(A,B,P,Q,C,D,P,Q)
| ~ para(A,B,C,D) ),
inference(nnf_transformation,[status(thm)],[f39]) ).
fof(f39_sk,plain,
! [A,B,C,D,P,Q] :
( eqangle(A,B,P,Q,C,D,P,Q)
| ~ para(A,B,C,D) ),
inference(skolemisation,[status(esa)],[f39_nnf]) ).
cnf(c39,plain,
( eqangle(X0,X1,X4,X5,X2,X3,X4,X5)
| ~ para(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(esa)],[f39_sk]) ).
cnf(hi39,axiom,
ifeq(para(X0,X1,X2,X3),true,eqangle(X0,X1,X4,X5,X2,X3,X4,X5),true) = true,
inference(equality_encoding,[status(esa)],[c39]) ).
cnf(t63,plain,
eqangle(sk20,sk21,X1,X2,sk20,sk21,X1,X2) = true,
inference(hyper_resolution,[status(thm)],[hi39,h146]) ).
cnf(t1884,plain,
eqangle(sk20,sk21,X1,X2,sk20,sk21,X1,X2) = true,
inference(orient,[status(thm)],[t63]) ).
cnf(t1893,plain,
true = ifeq(true,true,eqangle(X1,X2,sk20,sk21,X1,X2,sk20,sk21),true),
inference(cp,[status(thm)],[t308,t1884]) ).
cnf(t41,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t256,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t41]) ).
cnf(t25254,plain,
true = eqangle(X1,X2,sk20,sk21,X1,X2,sk20,sk21),
inference(step,[status(thm)],[t1893,t256]) ).
cnf(t6830,plain,
eqangle(X1,X2,sk20,sk21,X1,X2,sk20,sk21) = true,
inference(orient,[status(thm)],[t25254]) ).
cnf(t6833,plain,
true = ifeq(true,true,para(X1,X2,X1,X2),true),
inference(cp,[status(thm)],[t314,t6830]) ).
cnf(t25255,plain,
true = para(X1,X2,X1,X2),
inference(step,[status(thm)],[t6833,t256]) ).
cnf(t6856,plain,
para(X1,X2,X1,X2) = true,
inference(orient,[status(thm)],[t25255]) ).
cnf(t6873,plain,
true = ifeq(midp(X1,X2,X2),true,ifeq(true,true,ifeq(para(X2,X3,X2,X3),true,midp(X1,X3,X3),true),true),true),
inference(cp,[status(thm)],[t333,t6856]) ).
cnf(t26675,plain,
true = ifeq(midp(X1,X2,X2),true,ifeq(para(X2,X3,X2,X3),true,midp(X1,X3,X3),true),true),
inference(step,[status(thm)],[t6873,t256]) ).
cnf(t26676,plain,
true = ifeq(midp(X1,X2,X2),true,ifeq(true,true,midp(X1,X3,X3),true),true),
inference(step,[status(thm)],[t26675,t6856]) ).
cnf(t26677,plain,
true = ifeq(midp(X1,X2,X2),true,midp(X1,X3,X3),true),
inference(step,[status(thm)],[t26676,t256]) ).
cnf(t19343,plain,
ifeq(midp(X1,X2,X2),true,midp(X1,X3,X3),true) = true,
inference(orient,[status(thm)],[t26677]) ).
fof(f67,axiom,
! [A,B,C] :
( ( coll(A,B,C)
& cong(A,B,A,C) )
=> midp(A,B,C) ),
file('/export/starexec/sandbox2/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(t149,plain,
ifeq(cong(X1,X2,X1,X3),true,ifeq(coll(X1,X2,X3),true,midp(X1,X2,X3),true),true) = true,
inference(equality_encoding,[status(esa)],[c67]) ).
cnf(t272,plain,
ifeq(cong(X1,X2,X1,X3),true,ifeq(coll(X1,X2,X3),true,midp(X1,X2,X3),true),true) = true,
inference(orient,[status(thm)],[t149]) ).
fof(f2,axiom,
! [A,B,C,D] :
( ( coll(A,B,D)
& coll(A,B,C) )
=> coll(C,D,A) ),
file('/export/starexec/sandbox2/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(t148,plain,
ifeq(coll(X1,X2,X3),true,ifeq(coll(X1,X2,X4),true,coll(X3,X4,X1),true),true) = true,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t260,plain,
ifeq(coll(X1,X2,X3),true,ifeq(coll(X1,X2,X4),true,coll(X3,X4,X1),true),true) = true,
inference(orient,[status(thm)],[t148]) ).
fof(f0,axiom,
! [A,B,C] :
( coll(A,B,C)
=> coll(A,C,B) ),
file('/export/starexec/sandbox2/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(t102,plain,
ifeq(coll(X1,X2,X3),true,coll(X1,X3,X2),true) = true,
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t263,plain,
ifeq(coll(X1,X2,X3),true,coll(X1,X3,X2),true) = true,
inference(orient,[status(thm)],[t102]) ).
fof(f1,axiom,
! [A,B,C] :
( coll(A,B,C)
=> coll(B,A,C) ),
file('/export/starexec/sandbox2/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(t103,plain,
ifeq(coll(X1,X2,X3),true,coll(X2,X1,X3),true) = true,
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t261,plain,
ifeq(coll(X1,X2,X3),true,coll(X2,X1,X3),true) = true,
inference(orient,[status(thm)],[t103]) ).
fof(f66,axiom,
! [A,B,C] :
( para(A,B,A,C)
=> coll(A,B,C) ),
file('/export/starexec/sandbox2/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(t107,plain,
ifeq(para(X1,X2,X1,X3),true,coll(X1,X2,X3),true) = true,
inference(equality_encoding,[status(esa)],[c66]) ).
cnf(t353,plain,
ifeq(para(X1,X2,X1,X3),true,coll(X1,X2,X3),true) = true,
inference(orient,[status(thm)],[t107]) ).
cnf(t6857,plain,
true = ifeq(true,true,coll(X1,X2,X2),true),
inference(cp,[status(thm)],[t353,t6856]) ).
cnf(t25256,plain,
true = coll(X1,X2,X2),
inference(step,[status(thm)],[t6857,t256]) ).
cnf(t6882,plain,
coll(X1,X2,X2) = true,
inference(orient,[status(thm)],[t25256]) ).
cnf(t6884,plain,
true = ifeq(true,true,coll(X1,X2,X1),true),
inference(cp,[status(thm)],[t261,t6882]) ).
cnf(t25257,plain,
true = coll(X1,X2,X1),
inference(step,[status(thm)],[t6884,t256]) ).
cnf(t6925,plain,
coll(X1,X2,X1) = true,
inference(orient,[status(thm)],[t25257]) ).
cnf(t6928,plain,
true = ifeq(true,true,coll(X1,X1,X2),true),
inference(cp,[status(thm)],[t263,t6925]) ).
cnf(t25258,plain,
true = coll(X1,X1,X2),
inference(step,[status(thm)],[t6928,t256]) ).
cnf(t6957,plain,
coll(X1,X1,X2) = true,
inference(orient,[status(thm)],[t25258]) ).
cnf(t6960,plain,
true = ifeq(true,true,ifeq(coll(X1,X1,X2),true,coll(X3,X2,X1),true),true),
inference(cp,[status(thm)],[t260,t6957]) ).
cnf(t25259,plain,
true = ifeq(coll(X1,X1,X2),true,coll(X3,X2,X1),true),
inference(step,[status(thm)],[t6960,t256]) ).
cnf(t25260,plain,
true = ifeq(true,true,coll(X3,X2,X1),true),
inference(step,[status(thm)],[t25259,t6957]) ).
cnf(t25261,plain,
true = coll(X3,X2,X1),
inference(step,[status(thm)],[t25260,t256]) ).
cnf(t6991,plain,
coll(X1,X2,X3) = true,
inference(orient,[status(thm)],[t25261]) ).
cnf(t25272,plain,
ifeq(cong(X1,X2,X1,X3),true,ifeq(true,true,midp(X1,X2,X3),true),true) = true,
inference(step,[status(thm)],[t272,t6991]) ).
cnf(t25273,plain,
ifeq(cong(X1,X2,X1,X3),true,midp(X1,X2,X3),true) = true,
inference(step,[status(thm)],[t25272,t256]) ).
cnf(t6998,plain,
ifeq(cong(X1,X2,X1,X3),true,midp(X1,X2,X3),true) = true,
inference(rw,[status(thm)],[t25273]) ).
cnf(t20377,plain,
ifeq(cong(X1,X2,X1,X3),true,midp(X1,X2,X3),true) = true,
inference(orient,[status(thm)],[t6998]) ).
fof(f75,axiom,
! [A,B,C,D,P,Q,U,V] :
( ( cong(P,Q,U,V)
& eqratio(A,B,C,D,P,Q,U,V) )
=> cong(A,B,C,D) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ruleD75) ).
fof(f75_nnf,plain,
! [A,B,C,D,P,Q,U,V] :
( cong(A,B,C,D)
| ~ cong(P,Q,U,V)
| ~ eqratio(A,B,C,D,P,Q,U,V) ),
inference(nnf_transformation,[status(thm)],[f75]) ).
fof(f75_sk,plain,
! [A,B,C,D,P,Q,U,V] :
( cong(A,B,C,D)
| ~ cong(P,Q,U,V)
| ~ eqratio(A,B,C,D,P,Q,U,V) ),
inference(skolemisation,[status(esa)],[f75_nnf]) ).
cnf(c75,plain,
( cong(X0,X1,X2,X3)
| ~ cong(X4,X5,X6,X7)
| ~ eqratio(X0,X1,X2,X3,X4,X5,X6,X7) ),
inference(cnf_transformation,[status(esa)],[f75_sk]) ).
cnf(t199,plain,
ifeq(eqratio(X1,X2,X3,X4,X5,X6,X7,X8),true,ifeq(cong(X5,X6,X7,X8),true,cong(X1,X2,X3,X4),true),true) = true,
inference(equality_encoding,[status(esa)],[c75]) ).
cnf(t354,plain,
ifeq(eqratio(X1,X2,X3,X4,X5,X6,X7,X8),true,ifeq(cong(X5,X6,X7,X8),true,cong(X1,X2,X3,X4),true),true) = true,
inference(orient,[status(thm)],[t199]) ).
fof(f25,axiom,
! [A,B,C,D,P,Q,U,V] :
( eqratio(A,B,C,D,P,Q,U,V)
=> eqratio(B,A,C,D,P,Q,U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ruleD26) ).
fof(f25_nnf,plain,
! [A,B,C,D,P,Q,U,V] :
( eqratio(B,A,C,D,P,Q,U,V)
| ~ eqratio(A,B,C,D,P,Q,U,V) ),
inference(nnf_transformation,[status(thm)],[f25]) ).
fof(f25_sk,plain,
! [A,B,C,D,P,Q,U,V] :
( eqratio(B,A,C,D,P,Q,U,V)
| ~ eqratio(A,B,C,D,P,Q,U,V) ),
inference(skolemisation,[status(esa)],[f25_nnf]) ).
cnf(c25,plain,
( eqratio(X1,X0,X2,X3,X4,X5,X6,X7)
| ~ eqratio(X0,X1,X2,X3,X4,X5,X6,X7) ),
inference(cnf_transformation,[status(esa)],[f25_sk]) ).
cnf(t166,plain,
ifeq(eqratio(X1,X2,X3,X4,X5,X6,X7,X8),true,eqratio(X2,X1,X3,X4,X5,X6,X7,X8),true) = true,
inference(equality_encoding,[status(esa)],[c25]) ).
cnf(t362,plain,
ifeq(eqratio(X1,X2,X3,X4,X5,X6,X7,X8),true,eqratio(X2,X1,X3,X4,X5,X6,X7,X8),true) = true,
inference(orient,[status(thm)],[t166]) ).
fof(f28,axiom,
! [A,B,C,D,P,Q,U,V] :
( eqratio(A,B,C,D,P,Q,U,V)
=> eqratio(A,B,P,Q,C,D,U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ruleD29) ).
fof(f28_nnf,plain,
! [A,B,C,D,P,Q,U,V] :
( eqratio(A,B,P,Q,C,D,U,V)
| ~ eqratio(A,B,C,D,P,Q,U,V) ),
inference(nnf_transformation,[status(thm)],[f28]) ).
fof(f28_sk,plain,
! [A,B,C,D,P,Q,U,V] :
( eqratio(A,B,P,Q,C,D,U,V)
| ~ eqratio(A,B,C,D,P,Q,U,V) ),
inference(skolemisation,[status(esa)],[f28_nnf]) ).
cnf(c28,plain,
( eqratio(X0,X1,X4,X5,X2,X3,X6,X7)
| ~ eqratio(X0,X1,X2,X3,X4,X5,X6,X7) ),
inference(cnf_transformation,[status(esa)],[f28_sk]) ).
cnf(t165,plain,
ifeq(eqratio(X1,X2,X3,X4,X5,X6,X7,X8),true,eqratio(X1,X2,X5,X6,X3,X4,X7,X8),true) = true,
inference(equality_encoding,[status(esa)],[c28]) ).
cnf(t364,plain,
ifeq(eqratio(X1,X2,X3,X4,X5,X6,X7,X8),true,eqratio(X1,X2,X5,X6,X3,X4,X7,X8),true) = true,
inference(orient,[status(thm)],[t165]) ).
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(c124,plain,
coll(sk29,sk20,sk21),
inference(cnf_transformation,[status(esa)],[f94_sk]) ).
cnf(hi124,negated_conjecture,
coll(sk29,sk20,sk21) = true,
inference(equality_encoding,[status(esa)],[c124]) ).
cnf(h32,plain,
coll(sk21,sk21,sk29) = true,
inference(hyper_resolution,[status(thm)],[hi2,hi124,hi124]) ).
cnf(hi0,axiom,
ifeq(coll(X0,X1,X2),true,coll(X0,X2,X1),true) = true,
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(h144,plain,
coll(sk21,sk29,sk21) = true,
inference(hyper_resolution,[status(thm)],[hi0,h32]) ).
cnf(hi1,axiom,
ifeq(coll(X0,X1,X2),true,coll(X1,X0,X2),true) = true,
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(h1112,plain,
coll(sk29,sk21,sk21) = true,
inference(hyper_resolution,[status(thm)],[hi1,h144]) ).
fof(f81,axiom,
! [A,B,C,D,M,N] :
? [P] :
( ( midp(N,C,D)
& midp(M,A,B) )
=> ( para(P,N,A,C)
& para(P,M,B,D)
& midp(P,A,D) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ruleX6) ).
fof(f81_nnf,plain,
! [A,B,C,D,M,N] :
? [P] :
( ( para(P,N,A,C)
& para(P,M,B,D)
& midp(P,A,D) )
| ~ midp(N,C,D)
| ~ midp(M,A,B) ),
inference(nnf_transformation,[status(thm)],[f81]) ).
fof(f81_sk,plain,
! [M,A,B,N,C,D] :
( ( para(sk5(A,B,C,D,M,N),N,A,C)
& para(sk5(A,B,C,D,M,N),M,B,D)
& midp(sk5(A,B,C,D,M,N),A,D) )
| ~ midp(N,C,D)
| ~ midp(M,A,B) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk5])],[f81_nnf]) ).
cnf(c87,plain,
( para(sk5(X0,X1,X2,X3,X4,X5),X4,X1,X3)
| ~ midp(X5,X2,X3)
| ~ midp(X4,X0,X1) ),
inference(cnf_transformation,[status(esa)],[f81_sk]) ).
cnf(hi87,axiom,
ifeq(midp(X0,X1,X2),true,ifeq(midp(X3,X4,X5),true,para(sk5(X1,X2,X4,X5,X0,X3),X0,X2,X5),true),true) = true,
inference(equality_encoding,[status(esa)],[c87]) ).
cnf(c114,plain,
midp(sk24,sk22,sk21),
inference(cnf_transformation,[status(esa)],[f94_sk]) ).
cnf(hi114,negated_conjecture,
midp(sk24,sk22,sk21) = true,
inference(equality_encoding,[status(esa)],[c114]) ).
cnf(h2,plain,
para(sk5(sk22,sk21,sk22,sk21,sk24,sk24),sk24,sk21,sk21) = true,
inference(hyper_resolution,[status(thm)],[hi87,hi114,hi114]) ).
fof(f4,axiom,
! [A,B,C,D] :
( para(A,B,C,D)
=> para(C,D,A,B) ),
file('/export/starexec/sandbox2/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(h43,plain,
para(sk21,sk21,sk5(sk22,sk21,sk22,sk21,sk24,sk24),sk24) = true,
inference(hyper_resolution,[status(thm)],[hi4,h2]) ).
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/sandbox2/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(h183,plain,
para(sk21,sk21,sk21,sk21) = true,
inference(hyper_resolution,[status(thm)],[hi5,h43,h2]) ).
fof(f65,axiom,
! [A,B,C,D,O] :
( ( coll(O,B,D)
& coll(O,A,C)
& para(A,B,C,D) )
=> eqratio(O,A,A,C,O,B,B,D) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ruleD65) ).
fof(f65_nnf,plain,
! [A,B,C,D,O] :
( eqratio(O,A,A,C,O,B,B,D)
| ~ coll(O,B,D)
| ~ coll(O,A,C)
| ~ para(A,B,C,D) ),
inference(nnf_transformation,[status(thm)],[f65]) ).
fof(f65_sk,plain,
! [A,B,C,D,O] :
( eqratio(O,A,A,C,O,B,B,D)
| ~ coll(O,B,D)
| ~ coll(O,A,C)
| ~ para(A,B,C,D) ),
inference(skolemisation,[status(esa)],[f65_nnf]) ).
cnf(c65,plain,
( eqratio(X4,X0,X0,X2,X4,X1,X1,X3)
| ~ coll(X4,X1,X3)
| ~ coll(X4,X0,X2)
| ~ para(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(esa)],[f65_sk]) ).
cnf(hi65,axiom,
ifeq(para(X0,X1,X2,X3),true,ifeq(coll(X4,X0,X2),true,ifeq(coll(X4,X1,X3),true,eqratio(X4,X0,X0,X2,X4,X1,X1,X3),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c65]) ).
cnf(t89,plain,
eqratio(sk29,sk21,sk21,sk21,sk29,sk21,sk21,sk21) = true,
inference(hyper_resolution,[status(thm)],[hi65,h183,h1112,h1112]) ).
cnf(t3103,plain,
eqratio(sk29,sk21,sk21,sk21,sk29,sk21,sk21,sk21) = true,
inference(orient,[status(thm)],[t89]) ).
cnf(t3104,plain,
true = ifeq(true,true,eqratio(sk29,sk21,sk29,sk21,sk21,sk21,sk21,sk21),true),
inference(cp,[status(thm)],[t364,t3103]) ).
cnf(t25393,plain,
true = eqratio(sk29,sk21,sk29,sk21,sk21,sk21,sk21,sk21),
inference(step,[status(thm)],[t3104,t256]) ).
cnf(t7709,plain,
eqratio(sk29,sk21,sk29,sk21,sk21,sk21,sk21,sk21) = true,
inference(orient,[status(thm)],[t25393]) ).
cnf(t7711,plain,
true = ifeq(true,true,eqratio(sk21,sk29,sk29,sk21,sk21,sk21,sk21,sk21),true),
inference(cp,[status(thm)],[t362,t7709]) ).
cnf(t25550,plain,
true = eqratio(sk21,sk29,sk29,sk21,sk21,sk21,sk21,sk21),
inference(step,[status(thm)],[t7711,t256]) ).
cnf(t9255,plain,
eqratio(sk21,sk29,sk29,sk21,sk21,sk21,sk21,sk21) = true,
inference(orient,[status(thm)],[t25550]) ).
cnf(t9263,plain,
true = ifeq(true,true,ifeq(cong(sk21,sk21,sk21,sk21),true,cong(sk21,sk29,sk29,sk21),true),true),
inference(cp,[status(thm)],[t354,t9255]) ).
cnf(t25551,plain,
true = ifeq(cong(sk21,sk21,sk21,sk21),true,cong(sk21,sk29,sk29,sk21),true),
inference(step,[status(thm)],[t9263,t256]) ).
fof(f43,axiom,
! [A,B,C,P,Q,R] :
( ( eqangle(C,A,C,B,R,P,R,Q)
& cyclic(A,B,C,R)
& cyclic(A,B,C,Q)
& cyclic(A,B,C,P) )
=> cong(A,B,P,Q) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ruleD43) ).
fof(f43_nnf,plain,
! [A,B,C,P,Q,R] :
( cong(A,B,P,Q)
| ~ eqangle(C,A,C,B,R,P,R,Q)
| ~ cyclic(A,B,C,R)
| ~ cyclic(A,B,C,Q)
| ~ cyclic(A,B,C,P) ),
inference(nnf_transformation,[status(thm)],[f43]) ).
fof(f43_sk,plain,
! [A,B,C,P,Q,R] :
( cong(A,B,P,Q)
| ~ eqangle(C,A,C,B,R,P,R,Q)
| ~ cyclic(A,B,C,R)
| ~ cyclic(A,B,C,Q)
| ~ cyclic(A,B,C,P) ),
inference(skolemisation,[status(esa)],[f43_nnf]) ).
cnf(c43,plain,
( cong(X0,X1,X3,X4)
| ~ eqangle(X2,X0,X2,X1,X5,X3,X5,X4)
| ~ cyclic(X0,X1,X2,X5)
| ~ cyclic(X0,X1,X2,X4)
| ~ cyclic(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(esa)],[f43_sk]) ).
cnf(t253,plain,
ifeq(cyclic(X1,X2,X3,X4),true,ifeq(cyclic(X1,X2,X3,X5),true,ifeq(cyclic(X1,X2,X3,X6),true,ifeq(eqangle(X3,X1,X3,X2,X6,X4,X6,X5),true,cong(X1,X2,X4,X5),true),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c43]) ).
cnf(t369,plain,
ifeq(cyclic(X1,X2,X3,X4),true,ifeq(cyclic(X1,X2,X3,X5),true,ifeq(cyclic(X1,X2,X3,X6),true,ifeq(eqangle(X3,X1,X3,X2,X6,X4,X6,X5),true,cong(X1,X2,X4,X5),true),true),true),true) = true,
inference(orient,[status(thm)],[t253]) ).
fof(f40,axiom,
! [A,B,P,Q] :
( cyclic(A,B,P,Q)
=> eqangle(P,A,P,B,Q,A,Q,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ruleD41) ).
fof(f40_nnf,plain,
! [A,B,P,Q] :
( eqangle(P,A,P,B,Q,A,Q,B)
| ~ cyclic(A,B,P,Q) ),
inference(nnf_transformation,[status(thm)],[f40]) ).
fof(f40_sk,plain,
! [A,B,P,Q] :
( eqangle(P,A,P,B,Q,A,Q,B)
| ~ cyclic(A,B,P,Q) ),
inference(skolemisation,[status(esa)],[f40_nnf]) ).
cnf(c40,plain,
( eqangle(X2,X0,X2,X1,X3,X0,X3,X1)
| ~ cyclic(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(esa)],[f40_sk]) ).
cnf(t142,plain,
ifeq(cyclic(X1,X2,X3,X4),true,eqangle(X3,X1,X3,X2,X4,X1,X4,X2),true) = true,
inference(equality_encoding,[status(esa)],[c40]) ).
cnf(t371,plain,
ifeq(cyclic(X1,X2,X3,X4),true,eqangle(X3,X1,X3,X2,X4,X1,X4,X2),true) = true,
inference(orient,[status(thm)],[t142]) ).
cnf(hi68,axiom,
ifeq(midp(X0,X1,X2),true,cong(X0,X1,X0,X2),true) = true,
inference(equality_encoding,[status(esa)],[c68]) ).
cnf(h6,plain,
cong(sk24,sk22,sk24,sk21) = true,
inference(hyper_resolution,[status(thm)],[hi68,hi114]) ).
fof(f12,axiom,
! [A,B,C,D,O] :
( ( cong(O,A,O,D)
& cong(O,A,O,C)
& cong(O,A,O,B) )
=> cyclic(A,B,C,D) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ruleD13) ).
fof(f12_nnf,plain,
! [A,B,C,D,O] :
( cyclic(A,B,C,D)
| ~ cong(O,A,O,D)
| ~ cong(O,A,O,C)
| ~ cong(O,A,O,B) ),
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
! [O,A,B,C,D] :
( cyclic(A,B,C,D)
| ~ cong(O,A,O,D)
| ~ cong(O,A,O,C)
| ~ cong(O,A,O,B) ),
inference(skolemisation,[status(esa)],[f12_nnf]) ).
cnf(c12,plain,
( cyclic(X0,X1,X2,X3)
| ~ cong(X4,X0,X4,X3)
| ~ cong(X4,X0,X4,X2)
| ~ cong(X4,X0,X4,X1) ),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(hi12,axiom,
ifeq(cong(X0,X1,X0,X2),true,ifeq(cong(X0,X1,X0,X3),true,ifeq(cong(X0,X1,X0,X4),true,cyclic(X1,X2,X3,X4),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c12]) ).
cnf(h92,plain,
cyclic(sk22,sk21,sk21,sk21) = true,
inference(hyper_resolution,[status(thm)],[hi12,h6,h6,h6]) ).
fof(f16,axiom,
! [A,B,C,D,E] :
( ( cyclic(A,B,C,E)
& cyclic(A,B,C,D) )
=> cyclic(B,C,D,E) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ruleD17) ).
fof(f16_nnf,plain,
! [A,B,C,D,E] :
( cyclic(B,C,D,E)
| ~ cyclic(A,B,C,E)
| ~ cyclic(A,B,C,D) ),
inference(nnf_transformation,[status(thm)],[f16]) ).
fof(f16_sk,plain,
! [A,B,C,D,E] :
( cyclic(B,C,D,E)
| ~ cyclic(A,B,C,E)
| ~ cyclic(A,B,C,D) ),
inference(skolemisation,[status(esa)],[f16_nnf]) ).
cnf(c16,plain,
( cyclic(X1,X2,X3,X4)
| ~ cyclic(X0,X1,X2,X4)
| ~ cyclic(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(hi16,axiom,
ifeq(cyclic(X0,X1,X2,X3),true,ifeq(cyclic(X0,X1,X2,X4),true,cyclic(X1,X2,X3,X4),true),true) = true,
inference(equality_encoding,[status(esa)],[c16]) ).
cnf(t36,plain,
cyclic(sk21,sk21,sk21,sk21) = true,
inference(hyper_resolution,[status(thm)],[hi16,h92,h92]) ).
cnf(t3166,plain,
cyclic(sk21,sk21,sk21,sk21) = true,
inference(orient,[status(thm)],[t36]) ).
cnf(t3167,plain,
true = ifeq(true,true,eqangle(sk21,sk21,sk21,sk21,sk21,sk21,sk21,sk21),true),
inference(cp,[status(thm)],[t371,t3166]) ).
cnf(t25409,plain,
true = eqangle(sk21,sk21,sk21,sk21,sk21,sk21,sk21,sk21),
inference(step,[status(thm)],[t3167,t256]) ).
cnf(t7887,plain,
eqangle(sk21,sk21,sk21,sk21,sk21,sk21,sk21,sk21) = true,
inference(orient,[status(thm)],[t25409]) ).
cnf(t7894,plain,
true = ifeq(cyclic(sk21,sk21,sk21,sk21),true,ifeq(cyclic(sk21,sk21,sk21,sk21),true,ifeq(cyclic(sk21,sk21,sk21,sk21),true,ifeq(true,true,cong(sk21,sk21,sk21,sk21),true),true),true),true),
inference(cp,[status(thm)],[t369,t7887]) ).
cnf(t25410,plain,
true = ifeq(true,true,ifeq(cyclic(sk21,sk21,sk21,sk21),true,ifeq(cyclic(sk21,sk21,sk21,sk21),true,ifeq(true,true,cong(sk21,sk21,sk21,sk21),true),true),true),true),
inference(step,[status(thm)],[t7894,t3166]) ).
cnf(t25411,plain,
true = ifeq(cyclic(sk21,sk21,sk21,sk21),true,ifeq(cyclic(sk21,sk21,sk21,sk21),true,ifeq(true,true,cong(sk21,sk21,sk21,sk21),true),true),true),
inference(step,[status(thm)],[t25410,t256]) ).
cnf(t25412,plain,
true = ifeq(true,true,ifeq(cyclic(sk21,sk21,sk21,sk21),true,ifeq(true,true,cong(sk21,sk21,sk21,sk21),true),true),true),
inference(step,[status(thm)],[t25411,t3166]) ).
cnf(t25413,plain,
true = ifeq(cyclic(sk21,sk21,sk21,sk21),true,ifeq(true,true,cong(sk21,sk21,sk21,sk21),true),true),
inference(step,[status(thm)],[t25412,t256]) ).
cnf(t25414,plain,
true = ifeq(true,true,ifeq(true,true,cong(sk21,sk21,sk21,sk21),true),true),
inference(step,[status(thm)],[t25413,t3166]) ).
cnf(t25415,plain,
true = ifeq(true,true,cong(sk21,sk21,sk21,sk21),true),
inference(step,[status(thm)],[t25414,t256]) ).
cnf(t25416,plain,
true = cong(sk21,sk21,sk21,sk21),
inference(step,[status(thm)],[t25415,t256]) ).
cnf(t7895,plain,
cong(sk21,sk21,sk21,sk21) = true,
inference(orient,[status(thm)],[t25416]) ).
cnf(t25552,plain,
true = ifeq(true,true,cong(sk21,sk29,sk29,sk21),true),
inference(step,[status(thm)],[t25551,t7895]) ).
cnf(t25553,plain,
true = cong(sk21,sk29,sk29,sk21),
inference(step,[status(thm)],[t25552,t256]) ).
cnf(t9264,plain,
cong(sk21,sk29,sk29,sk21) = true,
inference(orient,[status(thm)],[t25553]) ).
cnf(t9267,plain,
true = ifeq(true,true,cong(sk29,sk21,sk21,sk29),true),
inference(cp,[status(thm)],[t266,t9264]) ).
cnf(t25555,plain,
true = cong(sk29,sk21,sk21,sk29),
inference(step,[status(thm)],[t9267,t256]) ).
cnf(t9303,plain,
cong(sk29,sk21,sk21,sk29) = true,
inference(orient,[status(thm)],[t25555]) ).
cnf(t9305,plain,
true = ifeq(true,true,cong(sk29,sk21,sk29,sk21),true),
inference(cp,[status(thm)],[t268,t9303]) ).
cnf(t25556,plain,
true = cong(sk29,sk21,sk29,sk21),
inference(step,[status(thm)],[t9305,t256]) ).
cnf(t9312,plain,
cong(sk29,sk21,sk29,sk21) = true,
inference(orient,[status(thm)],[t25556]) ).
cnf(t20378,plain,
true = ifeq(true,true,midp(sk29,sk21,sk21),true),
inference(cp,[status(thm)],[t20377,t9312]) ).
cnf(t26917,plain,
true = midp(sk29,sk21,sk21),
inference(step,[status(thm)],[t20378,t256]) ).
cnf(t20417,plain,
midp(sk29,sk21,sk21) = true,
inference(orient,[status(thm)],[t26917]) ).
cnf(t20420,plain,
true = ifeq(true,true,midp(sk29,X1,X1),true),
inference(cp,[status(thm)],[t19343,t20417]) ).
cnf(t26944,plain,
true = midp(sk29,X1,X1),
inference(step,[status(thm)],[t20420,t256]) ).
cnf(t20943,plain,
midp(sk29,X1,X1) = true,
inference(orient,[status(thm)],[t26944]) ).
cnf(t20948,plain,
true = ifeq(true,true,cong(sk29,X1,sk29,X1),true),
inference(cp,[status(thm)],[t336,t20943]) ).
cnf(t26960,plain,
true = cong(sk29,X1,sk29,X1),
inference(step,[status(thm)],[t20948,t256]) ).
cnf(t21317,plain,
cong(sk29,X1,sk29,X1) = true,
inference(orient,[status(thm)],[t26960]) ).
cnf(t21335,plain,
true = ifeq(true,true,ifeq(cong(sk29,X1,sk29,X1),true,perp(sk29,sk29,X2,X1),true),true),
inference(cp,[status(thm)],[t271,t21317]) ).
cnf(t27004,plain,
true = ifeq(cong(sk29,X1,sk29,X1),true,perp(sk29,sk29,X2,X1),true),
inference(step,[status(thm)],[t21335,t256]) ).
cnf(t27005,plain,
true = ifeq(true,true,perp(sk29,sk29,X2,X1),true),
inference(step,[status(thm)],[t27004,t21317]) ).
cnf(t27006,plain,
true = perp(sk29,sk29,X2,X1),
inference(step,[status(thm)],[t27005,t256]) ).
cnf(t22092,plain,
perp(sk29,sk29,X1,X2) = true,
inference(orient,[status(thm)],[t27006]) ).
cnf(t22093,plain,
true = ifeq(true,true,perp(X1,X2,sk29,sk29),true),
inference(cp,[status(thm)],[t292,t22092]) ).
cnf(t27057,plain,
true = perp(X1,X2,sk29,sk29),
inference(step,[status(thm)],[t22093,t256]) ).
cnf(t22859,plain,
perp(X1,X2,sk29,sk29) = true,
inference(orient,[status(thm)],[t27057]) ).
cnf(t22866,plain,
true = ifeq(true,true,ifeq(perp(sk29,sk29,X1,X2),true,para(X3,X4,X1,X2),true),true),
inference(cp,[status(thm)],[t285,t22859]) ).
cnf(t27073,plain,
true = ifeq(perp(sk29,sk29,X1,X2),true,para(X3,X4,X1,X2),true),
inference(step,[status(thm)],[t22866,t256]) ).
cnf(t27074,plain,
true = ifeq(true,true,para(X3,X4,X1,X2),true),
inference(step,[status(thm)],[t27073,t22092]) ).
cnf(t27075,plain,
true = para(X3,X4,X1,X2),
inference(step,[status(thm)],[t27074,t256]) ).
cnf(t23287,plain,
para(X1,X2,X3,X4) = true,
inference(orient,[status(thm)],[t27075]) ).
cnf(t27087,plain,
ifeq(midp(X1,X2,X3),true,ifeq(true,true,ifeq(para(X2,X5,X3,X4),true,midp(X1,X4,X5),true),true),true) = true,
inference(step,[status(thm)],[t333,t23287]) ).
cnf(t27088,plain,
ifeq(midp(X1,X2,X3),true,ifeq(para(X2,X5,X3,X4),true,midp(X1,X4,X5),true),true) = true,
inference(step,[status(thm)],[t27087,t256]) ).
cnf(t27089,plain,
ifeq(midp(X1,X2,X3),true,ifeq(true,true,midp(X1,X4,X5),true),true) = true,
inference(step,[status(thm)],[t27088,t23287]) ).
cnf(t27090,plain,
ifeq(midp(X1,X2,X3),true,midp(X1,X4,X5),true) = true,
inference(step,[status(thm)],[t27089,t256]) ).
cnf(t23294,plain,
ifeq(midp(X1,X2,X3),true,midp(X1,X4,X5),true) = true,
inference(rw,[status(thm)],[t27090]) ).
cnf(t24062,plain,
ifeq(midp(X1,X2,X3),true,midp(X1,X4,X5),true) = true,
inference(orient,[status(thm)],[t23294]) ).
cnf(t21324,plain,
true = ifeq(true,true,cong(sk29,X1,X1,sk29),true),
inference(cp,[status(thm)],[t268,t21317]) ).
cnf(t27003,plain,
true = cong(sk29,X1,X1,sk29),
inference(step,[status(thm)],[t21324,t256]) ).
cnf(t22057,plain,
cong(sk29,X1,X1,sk29) = true,
inference(orient,[status(thm)],[t27003]) ).
cnf(t22063,plain,
true = ifeq(true,true,cong(X1,sk29,sk29,X1),true),
inference(cp,[status(thm)],[t266,t22057]) ).
cnf(t27056,plain,
true = cong(X1,sk29,sk29,X1),
inference(step,[status(thm)],[t22063,t256]) ).
cnf(t22827,plain,
cong(X1,sk29,sk29,X1) = true,
inference(orient,[status(thm)],[t27056]) ).
cnf(t22834,plain,
true = ifeq(true,true,cong(X1,sk29,X1,sk29),true),
inference(cp,[status(thm)],[t268,t22827]) ).
cnf(t27070,plain,
true = cong(X1,sk29,X1,sk29),
inference(step,[status(thm)],[t22834,t256]) ).
cnf(t23207,plain,
cong(X1,sk29,X1,sk29) = true,
inference(orient,[status(thm)],[t27070]) ).
cnf(t23210,plain,
true = ifeq(true,true,midp(X1,sk29,sk29),true),
inference(cp,[status(thm)],[t20377,t23207]) ).
cnf(t27071,plain,
true = midp(X1,sk29,sk29),
inference(step,[status(thm)],[t23210,t256]) ).
cnf(t23243,plain,
midp(X1,sk29,sk29) = true,
inference(orient,[status(thm)],[t27071]) ).
cnf(t23244,plain,
true = ifeq(true,true,midp(X1,X2,X2),true),
inference(cp,[status(thm)],[t19343,t23243]) ).
cnf(t27072,plain,
true = midp(X1,X2,X2),
inference(step,[status(thm)],[t23244,t256]) ).
cnf(t23262,plain,
midp(X1,X2,X2) = true,
inference(orient,[status(thm)],[t27072]) ).
cnf(t24063,plain,
true = ifeq(true,true,midp(X1,X2,X3),true),
inference(cp,[status(thm)],[t24062,t23262]) ).
cnf(t27170,plain,
true = midp(X1,X2,X3),
inference(step,[status(thm)],[t24063,t256]) ).
cnf(t24087,plain,
midp(X1,X2,X3) = true,
inference(orient,[status(thm)],[t27170]) ).
cnf(t27195,plain,
ifeq(true,true,cong(X1,X2,X1,X3),true) = true,
inference(step,[status(thm)],[t336,t24087]) ).
cnf(t27196,plain,
cong(X1,X2,X1,X3) = true,
inference(step,[status(thm)],[t27195,t256]) ).
cnf(t24100,plain,
cong(X1,X2,X1,X3) = true,
inference(rw,[status(thm)],[t27196]) ).
cnf(t24485,plain,
cong(X1,X2,X1,X3) = true,
inference(orient,[status(thm)],[t24100]) ).
cnf(t24501,plain,
true = ifeq(true,true,cong(X1,X2,X3,X1),true),
inference(cp,[status(thm)],[t268,t24485]) ).
cnf(t27234,plain,
true = cong(X1,X2,X3,X1),
inference(step,[status(thm)],[t24501,t256]) ).
cnf(t24650,plain,
cong(X1,X2,X3,X1) = true,
inference(orient,[status(thm)],[t27234]) ).
cnf(t24665,plain,
true = ifeq(true,true,cong(X1,X2,X2,X3),true),
inference(cp,[status(thm)],[t266,t24650]) ).
cnf(t27245,plain,
true = cong(X1,X2,X2,X3),
inference(step,[status(thm)],[t24665,t256]) ).
cnf(t24822,plain,
cong(X1,X2,X2,X3) = true,
inference(orient,[status(thm)],[t27245]) ).
cnf(t24835,plain,
true = ifeq(true,true,cong(X1,X2,X3,X2),true),
inference(cp,[status(thm)],[t268,t24822]) ).
cnf(t27255,plain,
true = cong(X1,X2,X3,X2),
inference(step,[status(thm)],[t24835,t256]) ).
cnf(t25029,plain,
cong(X1,X2,X3,X2) = true,
inference(orient,[status(thm)],[t27255]) ).
cnf(t27256,plain,
ifeq(true,true,ifeq(cong(X1,X4,X3,X4),true,perp(X1,X3,X2,X4),true),true) = true,
inference(step,[status(thm)],[t271,t25029]) ).
cnf(t27257,plain,
ifeq(cong(X1,X4,X3,X4),true,perp(X1,X3,X2,X4),true) = true,
inference(step,[status(thm)],[t27256,t256]) ).
cnf(t27258,plain,
ifeq(true,true,perp(X1,X3,X2,X4),true) = true,
inference(step,[status(thm)],[t27257,t25029]) ).
cnf(t27259,plain,
perp(X1,X3,X2,X4) = true,
inference(step,[status(thm)],[t27258,t256]) ).
cnf(t25052,plain,
perp(X1,X3,X2,X4) = true,
inference(rw,[status(thm)],[t27259]) ).
cnf(t25125,plain,
perp(X1,X2,X3,X4) = true,
inference(orient,[status(thm)],[t25052]) ).
cnf(c125,plain,
~ perp(sk28,sk29,sk25,sk20),
inference(cnf_transformation,[status(esa)],[f94_sk]) ).
cnf(goal_0,negated_conjecture,
perp(sk28,sk29,sk25,sk20) != true,
inference(equality_encoding,[status(esa)],[c125]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t25125]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO634+1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/0.37 % Computer : n007.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 : Wed Sep 23 12:34:51 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 150.21/19.64 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 150.21/19.64 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------