%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GEO580+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 : n019.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:12 PM UTC 2026
% Result : Theorem 236.49s 31.52s
% Output : Proof 236.49s
% Verified :
% SZS Type : Refutation
% Derivation depth : 69
% Number of leaves : 15
% Syntax : Number of formulae : 181 ( 125 unt; 0 def)
% Number of atoms : 301 ( 119 equ)
% Maximal formula atoms : 11 ( 1 avg)
% Number of connectives : 186 ( 66 ~; 60 |; 45 &)
% ( 0 <=>; 15 =>; 0 <=; 0 <~>)
% Maximal formula depth : 20 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 9 ( 7 usr; 1 prp; 0-8 aty)
% Number of functors : 10 ( 10 usr; 9 con; 0-4 aty)
% Number of variables : 622 ( 78 sgn 229 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
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(t235,plain,
ifeq(cong(X1,X2,X1,X3),true,ifeq(cong(X1,X2,X1,X4),true,ifeq(cong(X1,X2,X1,X5),true,cyclic(X2,X3,X4,X5),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c12]) ).
cnf(t296,plain,
ifeq(cong(X1,X2,X1,X3),true,ifeq(cong(X1,X2,X1,X4),true,ifeq(cong(X1,X2,X1,X5),true,cyclic(X2,X3,X4,X5),true),true),true) = true,
inference(orient,[status(thm)],[t235]) ).
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(t105,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)],[t105]) ).
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(t227,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)],[t227]) ).
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(t190,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(t265,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)],[t190]) ).
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(t115,plain,
ifeq(perp(X1,X2,X3,X4),true,perp(X3,X4,X1,X2),true) = true,
inference(equality_encoding,[status(esa)],[c7]) ).
cnf(t274,plain,
ifeq(perp(X1,X2,X3,X4),true,perp(X3,X4,X1,X2),true) = true,
inference(orient,[status(thm)],[t115]) ).
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(t177,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(t289,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)],[t177]) ).
fof(f73,axiom,
! [A,B,C,D,P,Q,U,V] :
( ( para(P,Q,U,V)
& eqangle(A,B,C,D,P,Q,U,V) )
=> para(A,B,C,D) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ruleD73) ).
fof(f73_nnf,plain,
! [A,B,C,D,P,Q,U,V] :
( para(A,B,C,D)
| ~ para(P,Q,U,V)
| ~ eqangle(A,B,C,D,P,Q,U,V) ),
inference(nnf_transformation,[status(thm)],[f73]) ).
fof(f73_sk,plain,
! [A,B,C,D,P,Q,U,V] :
( para(A,B,C,D)
| ~ para(P,Q,U,V)
| ~ eqangle(A,B,C,D,P,Q,U,V) ),
inference(skolemisation,[status(esa)],[f73_nnf]) ).
cnf(c73,plain,
( para(X0,X1,X2,X3)
| ~ para(X4,X5,X6,X7)
| ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7) ),
inference(cnf_transformation,[status(esa)],[f73_sk]) ).
cnf(t211,plain,
ifeq(eqangle(X1,X2,X3,X4,X5,X6,X7,X8),true,ifeq(para(X5,X6,X7,X8),true,para(X1,X2,X3,X4),true),true) = true,
inference(equality_encoding,[status(esa)],[c73]) ).
cnf(t305,plain,
ifeq(eqangle(X1,X2,X3,X4,X5,X6,X7,X8),true,ifeq(para(X5,X6,X7,X8),true,para(X1,X2,X3,X4),true),true) = true,
inference(orient,[status(thm)],[t211]) ).
fof(f20,axiom,
! [A,B,C,D,P,Q,U,V] :
( eqangle(A,B,C,D,P,Q,U,V)
=> eqangle(A,B,P,Q,C,D,U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ruleD21) ).
fof(f20_nnf,plain,
! [A,B,C,D,P,Q,U,V] :
( eqangle(A,B,P,Q,C,D,U,V)
| ~ eqangle(A,B,C,D,P,Q,U,V) ),
inference(nnf_transformation,[status(thm)],[f20]) ).
fof(f20_sk,plain,
! [A,B,C,D,P,Q,U,V] :
( eqangle(A,B,P,Q,C,D,U,V)
| ~ eqangle(A,B,C,D,P,Q,U,V) ),
inference(skolemisation,[status(esa)],[f20_nnf]) ).
cnf(c20,plain,
( eqangle(X0,X1,X4,X5,X2,X3,X6,X7)
| ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7) ),
inference(cnf_transformation,[status(esa)],[f20_sk]) ).
cnf(t180,plain,
ifeq(eqangle(X1,X2,X3,X4,X5,X6,X7,X8),true,eqangle(X1,X2,X5,X6,X3,X4,X7,X8),true) = true,
inference(equality_encoding,[status(esa)],[c20]) ).
cnf(t312,plain,
ifeq(eqangle(X1,X2,X3,X4,X5,X6,X7,X8),true,eqangle(X1,X2,X5,X6,X3,X4,X7,X8),true) = true,
inference(orient,[status(thm)],[t180]) ).
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,D,E,F,G,H] :
( ( midp(H,C,B)
& coll(G,A,D)
& perp(G,C,A,D)
& coll(F,A,D)
& perp(F,B,A,D)
& coll(E,B,C)
& perp(E,A,B,C)
& eqangle(D,C,C,A,D,C,C,B)
& eqangle(D,B,B,C,D,B,B,A)
& eqangle(D,A,A,B,D,A,A,C) )
=> cyclic(E,F,G,H) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',exemplo6GDDFULL416042) ).
fof(f94_neg,negated_conjecture,
~ ! [A,B,C,D,E,F,G,H] :
( ( midp(H,C,B)
& coll(G,A,D)
& perp(G,C,A,D)
& coll(F,A,D)
& perp(F,B,A,D)
& coll(E,B,C)
& perp(E,A,B,C)
& eqangle(D,C,C,A,D,C,C,B)
& eqangle(D,B,B,C,D,B,B,A)
& eqangle(D,A,A,B,D,A,A,C) )
=> cyclic(E,F,G,H) ),
inference(negated_conjecture,[status(cth)],[f94]) ).
fof(f94_nnf,plain,
? [A,B,C,D,E,F,G,H] :
( ~ cyclic(E,F,G,H)
& midp(H,C,B)
& coll(G,A,D)
& perp(G,C,A,D)
& coll(F,A,D)
& perp(F,B,A,D)
& coll(E,B,C)
& perp(E,A,B,C)
& eqangle(D,C,C,A,D,C,C,B)
& eqangle(D,B,B,C,D,B,B,A)
& eqangle(D,A,A,B,D,A,A,C) ),
inference(nnf_transformation,[status(thm)],[f94_neg]) ).
fof(f94_sk,plain,
( ~ cyclic(sk24,sk25,sk26,sk27)
& midp(sk27,sk22,sk21)
& coll(sk26,sk20,sk23)
& perp(sk26,sk22,sk20,sk23)
& coll(sk25,sk20,sk23)
& perp(sk25,sk21,sk20,sk23)
& coll(sk24,sk21,sk22)
& perp(sk24,sk20,sk21,sk22)
& eqangle(sk23,sk22,sk22,sk20,sk23,sk22,sk22,sk21)
& eqangle(sk23,sk21,sk21,sk22,sk23,sk21,sk21,sk20)
& eqangle(sk23,sk20,sk20,sk21,sk23,sk20,sk20,sk22) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk20,sk21,sk22,sk23,sk24,sk25,sk26,sk27])],[f94_nnf]) ).
cnf(c118,plain,
perp(sk25,sk21,sk20,sk23),
inference(cnf_transformation,[status(esa)],[f94_sk]) ).
cnf(hi118,negated_conjecture,
perp(sk25,sk21,sk20,sk23) = true,
inference(equality_encoding,[status(esa)],[c118]) ).
cnf(h17,plain,
perp(sk20,sk23,sk25,sk21) = true,
inference(hyper_resolution,[status(thm)],[hi7,hi118]) ).
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(c120,plain,
perp(sk26,sk22,sk20,sk23),
inference(cnf_transformation,[status(esa)],[f94_sk]) ).
cnf(hi120,negated_conjecture,
perp(sk26,sk22,sk20,sk23) = true,
inference(equality_encoding,[status(esa)],[c120]) ).
cnf(h87,plain,
para(sk26,sk22,sk25,sk21) = true,
inference(hyper_resolution,[status(thm)],[hi8,hi120,h17]) ).
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(h301,plain,
eqangle(sk26,sk22,V0,V1,sk25,sk21,V0,V1) = true,
inference(hyper_resolution,[status(thm)],[hi39,h87]) ).
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(hi18,axiom,
ifeq(eqangle(X0,X1,X2,X3,X4,X5,X6,X7),true,eqangle(X2,X3,X0,X1,X6,X7,X4,X5),true) = true,
inference(equality_encoding,[status(esa)],[c18]) ).
cnf(t51,plain,
eqangle(X1,X2,sk26,sk22,X1,X2,sk25,sk21) = true,
inference(hyper_resolution,[status(thm)],[hi18,h301]) ).
cnf(t1791,plain,
eqangle(X1,X2,sk26,sk22,X1,X2,sk25,sk21) = true,
inference(orient,[status(thm)],[t51]) ).
cnf(t1792,plain,
true = ifeq(true,true,eqangle(X1,X2,X1,X2,sk26,sk22,sk25,sk21),true),
inference(cp,[status(thm)],[t312,t1791]) ).
cnf(t33,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t256,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t33]) ).
cnf(t40014,plain,
true = eqangle(X1,X2,X1,X2,sk26,sk22,sk25,sk21),
inference(step,[status(thm)],[t1792,t256]) ).
cnf(t7848,plain,
eqangle(X1,X2,X1,X2,sk26,sk22,sk25,sk21) = true,
inference(orient,[status(thm)],[t40014]) ).
cnf(t7853,plain,
true = ifeq(true,true,ifeq(para(sk26,sk22,sk25,sk21),true,para(X1,X2,X1,X2),true),true),
inference(cp,[status(thm)],[t305,t7848]) ).
cnf(t40015,plain,
true = ifeq(para(sk26,sk22,sk25,sk21),true,para(X1,X2,X1,X2),true),
inference(step,[status(thm)],[t7853,t256]) ).
cnf(t43,plain,
para(sk26,sk22,sk25,sk21) = true,
inference(hyper_resolution,[status(thm)],[hi8,hi120,h17]) ).
cnf(t3030,plain,
para(sk26,sk22,sk25,sk21) = true,
inference(orient,[status(thm)],[t43]) ).
cnf(t40016,plain,
true = ifeq(true,true,para(X1,X2,X1,X2),true),
inference(step,[status(thm)],[t40015,t3030]) ).
cnf(t40017,plain,
true = para(X1,X2,X1,X2),
inference(step,[status(thm)],[t40016,t256]) ).
cnf(t7858,plain,
para(X1,X2,X1,X2) = true,
inference(orient,[status(thm)],[t40017]) ).
cnf(t7875,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,t7858]) ).
cnf(t42949,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)],[t7875,t256]) ).
cnf(t42950,plain,
true = ifeq(midp(X1,X2,X2),true,ifeq(true,true,midp(X1,X3,X3),true),true),
inference(step,[status(thm)],[t42949,t7858]) ).
cnf(t42951,plain,
true = ifeq(midp(X1,X2,X2),true,midp(X1,X3,X3),true),
inference(step,[status(thm)],[t42950,t256]) ).
cnf(t37421,plain,
ifeq(midp(X1,X2,X2),true,midp(X1,X3,X3),true) = true,
inference(orient,[status(thm)],[t42951]) ).
fof(f3,axiom,
! [A,B,C,D] :
( para(A,B,C,D)
=> para(A,B,D,C) ),
file('/export/starexec/sandbox2/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(t112,plain,
ifeq(para(X1,X2,X3,X4),true,para(X1,X2,X4,X3),true) = true,
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(t362,plain,
ifeq(para(X1,X2,X3,X4),true,para(X1,X2,X4,X3),true) = true,
inference(orient,[status(thm)],[t112]) ).
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(t113,plain,
ifeq(para(X1,X2,X3,X4),true,para(X3,X4,X1,X2),true) = true,
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(t359,plain,
ifeq(para(X1,X2,X3,X4),true,para(X3,X4,X1,X2),true) = true,
inference(orient,[status(thm)],[t113]) ).
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(t141,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)],[t141]) ).
cnf(t182,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)],[t182]) ).
cnf(c113,plain,
eqangle(sk23,sk20,sk20,sk21,sk23,sk20,sk20,sk22),
inference(cnf_transformation,[status(esa)],[f94_sk]) ).
cnf(t53,plain,
eqangle(sk23,sk20,sk20,sk21,sk23,sk20,sk20,sk22) = true,
inference(equality_encoding,[status(esa)],[c113]) ).
cnf(t2005,plain,
eqangle(sk23,sk20,sk20,sk21,sk23,sk20,sk20,sk22) = true,
inference(orient,[status(thm)],[t53]) ).
cnf(t2011,plain,
true = ifeq(true,true,eqangle(sk20,sk21,sk23,sk20,sk20,sk22,sk23,sk20),true),
inference(cp,[status(thm)],[t308,t2005]) ).
cnf(t40128,plain,
true = eqangle(sk20,sk21,sk23,sk20,sk20,sk22,sk23,sk20),
inference(step,[status(thm)],[t2011,t256]) ).
cnf(t8506,plain,
eqangle(sk20,sk21,sk23,sk20,sk20,sk22,sk23,sk20) = true,
inference(orient,[status(thm)],[t40128]) ).
cnf(t8508,plain,
true = ifeq(true,true,para(sk20,sk21,sk20,sk22),true),
inference(cp,[status(thm)],[t314,t8506]) ).
cnf(t40129,plain,
true = para(sk20,sk21,sk20,sk22),
inference(step,[status(thm)],[t8508,t256]) ).
cnf(t8520,plain,
para(sk20,sk21,sk20,sk22) = true,
inference(orient,[status(thm)],[t40129]) ).
cnf(t8521,plain,
true = ifeq(true,true,para(sk20,sk21,sk22,sk20),true),
inference(cp,[status(thm)],[t362,t8520]) ).
cnf(t40130,plain,
true = para(sk20,sk21,sk22,sk20),
inference(step,[status(thm)],[t8521,t256]) ).
cnf(t8538,plain,
para(sk20,sk21,sk22,sk20) = true,
inference(orient,[status(thm)],[t40130]) ).
cnf(t8539,plain,
true = ifeq(true,true,para(sk22,sk20,sk20,sk21),true),
inference(cp,[status(thm)],[t359,t8538]) ).
cnf(t40132,plain,
true = para(sk22,sk20,sk20,sk21),
inference(step,[status(thm)],[t8539,t256]) ).
cnf(t8570,plain,
para(sk22,sk20,sk20,sk21) = true,
inference(orient,[status(thm)],[t40132]) ).
cnf(t8571,plain,
true = ifeq(true,true,para(sk22,sk20,sk21,sk20),true),
inference(cp,[status(thm)],[t362,t8570]) ).
cnf(t40134,plain,
true = para(sk22,sk20,sk21,sk20),
inference(step,[status(thm)],[t8571,t256]) ).
cnf(t8602,plain,
para(sk22,sk20,sk21,sk20) = true,
inference(orient,[status(thm)],[t40134]) ).
cnf(t8615,plain,
true = ifeq(midp(X1,sk22,sk21),true,ifeq(true,true,ifeq(para(sk22,sk20,sk21,sk20),true,midp(X1,sk20,sk20),true),true),true),
inference(cp,[status(thm)],[t333,t8602]) ).
cnf(t42983,plain,
true = ifeq(midp(X1,sk22,sk21),true,ifeq(para(sk22,sk20,sk21,sk20),true,midp(X1,sk20,sk20),true),true),
inference(step,[status(thm)],[t8615,t256]) ).
cnf(t42984,plain,
true = ifeq(midp(X1,sk22,sk21),true,ifeq(true,true,midp(X1,sk20,sk20),true),true),
inference(step,[status(thm)],[t42983,t8602]) ).
cnf(t42985,plain,
true = ifeq(midp(X1,sk22,sk21),true,midp(X1,sk20,sk20),true),
inference(step,[status(thm)],[t42984,t256]) ).
cnf(t37486,plain,
ifeq(midp(X1,sk22,sk21),true,midp(X1,sk20,sk20),true) = true,
inference(orient,[status(thm)],[t42985]) ).
cnf(c122,plain,
midp(sk27,sk22,sk21),
inference(cnf_transformation,[status(esa)],[f94_sk]) ).
cnf(t8,plain,
midp(sk27,sk22,sk21) = true,
inference(equality_encoding,[status(esa)],[c122]) ).
cnf(t2021,plain,
midp(sk27,sk22,sk21) = true,
inference(orient,[status(thm)],[t8]) ).
cnf(t37491,plain,
true = ifeq(true,true,midp(sk27,sk20,sk20),true),
inference(cp,[status(thm)],[t37486,t2021]) ).
cnf(t42986,plain,
true = midp(sk27,sk20,sk20),
inference(step,[status(thm)],[t37491,t256]) ).
cnf(t37492,plain,
midp(sk27,sk20,sk20) = true,
inference(orient,[status(thm)],[t42986]) ).
cnf(t37493,plain,
true = ifeq(true,true,midp(sk27,X1,X1),true),
inference(cp,[status(thm)],[t37421,t37492]) ).
cnf(t42987,plain,
true = midp(sk27,X1,X1),
inference(step,[status(thm)],[t37493,t256]) ).
cnf(t37513,plain,
midp(sk27,X1,X1) = true,
inference(orient,[status(thm)],[t42987]) ).
cnf(t37518,plain,
true = ifeq(true,true,cong(sk27,X1,sk27,X1),true),
inference(cp,[status(thm)],[t336,t37513]) ).
cnf(t42992,plain,
true = cong(sk27,X1,sk27,X1),
inference(step,[status(thm)],[t37518,t256]) ).
cnf(t37619,plain,
cong(sk27,X1,sk27,X1) = true,
inference(orient,[status(thm)],[t42992]) ).
cnf(t37630,plain,
true = ifeq(true,true,ifeq(cong(sk27,X1,sk27,X1),true,perp(sk27,sk27,X2,X1),true),true),
inference(cp,[status(thm)],[t289,t37619]) ).
cnf(t42998,plain,
true = ifeq(cong(sk27,X1,sk27,X1),true,perp(sk27,sk27,X2,X1),true),
inference(step,[status(thm)],[t37630,t256]) ).
cnf(t42999,plain,
true = ifeq(true,true,perp(sk27,sk27,X2,X1),true),
inference(step,[status(thm)],[t42998,t37619]) ).
cnf(t43000,plain,
true = perp(sk27,sk27,X2,X1),
inference(step,[status(thm)],[t42999,t256]) ).
cnf(t37785,plain,
perp(sk27,sk27,X1,X2) = true,
inference(orient,[status(thm)],[t43000]) ).
cnf(t37790,plain,
true = ifeq(true,true,perp(X1,X2,sk27,sk27),true),
inference(cp,[status(thm)],[t274,t37785]) ).
cnf(t43008,plain,
true = perp(X1,X2,sk27,sk27),
inference(step,[status(thm)],[t37790,t256]) ).
cnf(t37916,plain,
perp(X1,X2,sk27,sk27) = true,
inference(orient,[status(thm)],[t43008]) ).
cnf(t37936,plain,
true = ifeq(true,true,ifeq(perp(sk27,sk27,X1,X2),true,para(X3,X4,X1,X2),true),true),
inference(cp,[status(thm)],[t265,t37916]) ).
cnf(t43020,plain,
true = ifeq(perp(sk27,sk27,X1,X2),true,para(X3,X4,X1,X2),true),
inference(step,[status(thm)],[t37936,t256]) ).
cnf(t43021,plain,
true = ifeq(true,true,para(X3,X4,X1,X2),true),
inference(step,[status(thm)],[t43020,t37785]) ).
cnf(t43022,plain,
true = para(X3,X4,X1,X2),
inference(step,[status(thm)],[t43021,t256]) ).
cnf(t38104,plain,
para(X1,X2,X3,X4) = true,
inference(orient,[status(thm)],[t43022]) ).
cnf(t43053,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,t38104]) ).
cnf(t43054,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)],[t43053,t256]) ).
cnf(t43055,plain,
ifeq(midp(X1,X2,X3),true,ifeq(true,true,midp(X1,X4,X5),true),true) = true,
inference(step,[status(thm)],[t43054,t38104]) ).
cnf(t43056,plain,
ifeq(midp(X1,X2,X3),true,midp(X1,X4,X5),true) = true,
inference(step,[status(thm)],[t43055,t256]) ).
cnf(t38124,plain,
ifeq(midp(X1,X2,X3),true,midp(X1,X4,X5),true) = true,
inference(rw,[status(thm)],[t43056]) ).
cnf(t39726,plain,
ifeq(midp(X1,X2,X3),true,midp(X1,X4,X5),true) = true,
inference(orient,[status(thm)],[t38124]) ).
cnf(t39737,plain,
true = ifeq(true,true,midp(sk27,X1,X2),true),
inference(cp,[status(thm)],[t39726,t37513]) ).
cnf(t43233,plain,
true = midp(sk27,X1,X2),
inference(step,[status(thm)],[t39737,t256]) ).
cnf(t39747,plain,
midp(sk27,X1,X2) = true,
inference(orient,[status(thm)],[t43233]) ).
cnf(t39748,plain,
true = ifeq(true,true,cong(sk27,X1,sk27,X2),true),
inference(cp,[status(thm)],[t336,t39747]) ).
cnf(t43234,plain,
true = cong(sk27,X1,sk27,X2),
inference(step,[status(thm)],[t39748,t256]) ).
cnf(t39753,plain,
cong(sk27,X1,sk27,X2) = true,
inference(orient,[status(thm)],[t43234]) ).
cnf(t39767,plain,
true = ifeq(true,true,ifeq(cong(sk27,X1,sk27,X2),true,ifeq(cong(sk27,X1,sk27,X3),true,cyclic(X1,X4,X2,X3),true),true),true),
inference(cp,[status(thm)],[t296,t39753]) ).
cnf(t43239,plain,
true = ifeq(cong(sk27,X1,sk27,X2),true,ifeq(cong(sk27,X1,sk27,X3),true,cyclic(X1,X4,X2,X3),true),true),
inference(step,[status(thm)],[t39767,t256]) ).
cnf(t43240,plain,
true = ifeq(true,true,ifeq(cong(sk27,X1,sk27,X3),true,cyclic(X1,X4,X2,X3),true),true),
inference(step,[status(thm)],[t43239,t39753]) ).
cnf(t43241,plain,
true = ifeq(cong(sk27,X1,sk27,X3),true,cyclic(X1,X4,X2,X3),true),
inference(step,[status(thm)],[t43240,t256]) ).
cnf(t43242,plain,
true = ifeq(true,true,cyclic(X1,X4,X2,X3),true),
inference(step,[status(thm)],[t43241,t39753]) ).
cnf(t43243,plain,
true = cyclic(X1,X4,X2,X3),
inference(step,[status(thm)],[t43242,t256]) ).
cnf(t39798,plain,
cyclic(X1,X2,X3,X4) = true,
inference(orient,[status(thm)],[t43243]) ).
cnf(c123,plain,
~ cyclic(sk24,sk25,sk26,sk27),
inference(cnf_transformation,[status(esa)],[f94_sk]) ).
cnf(goal_0,negated_conjecture,
cyclic(sk24,sk25,sk26,sk27) != true,
inference(equality_encoding,[status(esa)],[c123]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t39798]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO580+1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.11/0.36 % Computer : n019.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Wed Sep 23 12:27:49 UTC 2026
% 0.13/0.36 % CPUTime :
% 0.13/0.36 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 236.49/31.52 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 236.49/31.52 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------