%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : GEO507+1 : TPTP v9.0.0. Released v7.0.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n032.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Jul 24 01:39:07 PM UTC 2025
% Result : Theorem 9.51s 1.48s
% Output : CNFRefutation 9.51s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 7
% Syntax : Number of formulae : 34 ( 10 unt; 0 def)
% Number of atoms : 128 ( 27 equ)
% Maximal formula atoms : 30 ( 3 avg)
% Number of connectives : 173 ( 79 ~; 78 |; 16 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 21 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-5 aty)
% Number of functors : 9 ( 9 usr; 4 con; 0-5 aty)
% Number of variables : 78 ( 7 sgn 36 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(aSatz8_14a,plain,
! [Xa,Xb,Xp,Xq] :
( ~ perp(Xa,Xb,Xp,Xq)
| ~ s_col(Xa,Xb,Xp)
| ~ s_col(Xa,Xb,Xq) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aSatz8_14a) ).
fof(aSatz8_14a_negated,plain,
~ ! [Xa,Xb,Xp,Xq] :
( ~ perp(Xa,Xb,Xp,Xq)
| ~ s_col(Xa,Xb,Xp)
| ~ s_col(Xa,Xb,Xq) ),
inference(negate_conjecture,[status(cth)],[aSatz8_14a]) ).
cnf(152,plain,
perp(sK1,sK2,sK3,sK4),
inference(cnf,[status(esa)],[aSatz8_14a_negated]) ).
cnf(l0,plain,
perp(sK1,sK2,sK3,sK4),
inference(instantiation,[status(thm)],[152]) ).
fof(d_Defn8_11b,plain,
! [Xp,Xq,Xp1,Xq1,X] :
( ( ~ perp(Xp,Xq,Xp1,Xq1)
| perpAt(Xp,Xq,il(Xp,Xq,Xp1,Xq1),Xp1,Xq1) )
& ( perp(Xp,Xq,Xp1,Xq1)
| ~ perpAt(Xp,Xq,X,Xp1,Xq1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d_Defn8_11b) ).
cnf(211,plain,
( ~ perp(X0,X1,X2,X3)
| perpAt(X0,X1,il(X0,X1,X2,X3),X2,X3) ),
inference(cnf,[status(esa)],[d_Defn8_11b]) ).
cnf(l1,plain,
( ~ perp(sK1,sK2,sK3,sK4)
| perpAt(sK1,sK2,il(sK1,sK2,sK3,sK4),sK3,sK4) ),
inference(instantiation,[status(thm)],[211]) ).
fof(d_Defn8_11a,plain,
! [Y,Z,X,Y1,Z1,U,V] :
( ( ~ perpAt(Y,Z,X,Y1,Z1)
| s_col(Y,Z,X) )
& ( ~ perpAt(Y,Z,X,Y1,Z1)
| s_col(Y1,Z1,X) )
& ( ~ perpAt(Y,Z,X,Y1,Z1)
| Y != Z )
& ( ~ perpAt(Y,Z,X,Y1,Z1)
| Y1 != Z1 )
& ( ~ perpAt(Y,Z,X,Y1,Z1)
| ~ s_col(Y,Z,U)
| ~ s_col(Y1,Z1,V)
| s_r(U,X,V) )
& ( perpAt(Y,Z,X,Y1,Z1)
| Y = Z
| Y1 = Z1
| ~ s_col(Y,Z,X)
| ~ s_col(Y1,Z1,X)
| s_col(Y,Z,f811(Y,Z,Y1,Z1,X)) )
& ( perpAt(Y,Z,X,Y1,Z1)
| Y = Z
| Y1 = Z1
| ~ s_col(Y,Z,X)
| ~ s_col(Y1,Z1,X)
| s_col(Y1,Z1,g811(Y,Z,Y1,Z1,X)) )
& ( perpAt(Y,Z,X,Y1,Z1)
| Y = Z
| Y1 = Z1
| ~ s_col(Y,Z,X)
| ~ s_col(Y1,Z1,X)
| ~ s_r(f811(Y,Z,Y1,Z1,X),X,g811(Y,Z,Y1,Z1,X)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d_Defn8_11a) ).
cnf(207,plain,
( ~ s_col(X0,X1,X2)
| ~ s_col(X3,X4,X5)
| ~ perpAt(X0,X1,X6,X3,X4)
| s_r(X2,X6,X5) ),
inference(cnf,[status(esa)],[d_Defn8_11a]) ).
cnf(l2,plain,
( ~ s_col(sK1,sK2,f813(sK1,sK2,sK3,sK4,il(sK1,sK2,sK3,sK4)))
| ~ s_col(sK3,sK4,f813(sK1,sK2,sK3,sK4,il(sK1,sK2,sK3,sK4)))
| ~ perpAt(sK1,sK2,il(sK1,sK2,sK3,sK4),sK3,sK4)
| s_r(f813(sK1,sK2,sK3,sK4,il(sK1,sK2,sK3,sK4)),il(sK1,sK2,sK3,sK4),f813(sK1,sK2,sK3,sK4,il(sK1,sK2,sK3,sK4))) ),
inference(instantiation,[status(thm)],[207]) ).
fof(aSatz8_6,plain,
! [Xa,Xb,Xc,Xa1] :
( ~ s_r(Xa,Xb,Xc)
| ~ s_r(Xa1,Xb,Xc)
| ~ s_t(Xa,Xc,Xa1)
| Xb = Xc ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aSatz8_6) ).
cnf(135,plain,
( ~ s_t(X0,X1,X2)
| ~ s_r(X0,X3,X1)
| ~ s_r(X2,X3,X1)
| X3 = X1 ),
inference(cnf,[status(esa)],[aSatz8_6]) ).
cnf(l25,plain,
( ~ s_t(f813(sK1,sK2,sK3,sK4,il(sK1,sK2,sK3,sK4)),f813(sK1,sK2,sK3,sK4,il(sK1,sK2,sK3,sK4)),f813(sK1,sK2,sK3,sK4,il(sK1,sK2,sK3,sK4)))
| ~ s_r(f813(sK1,sK2,sK3,sK4,il(sK1,sK2,sK3,sK4)),il(sK1,sK2,sK3,sK4),f813(sK1,sK2,sK3,sK4,il(sK1,sK2,sK3,sK4)))
| ~ s_r(f813(sK1,sK2,sK3,sK4,il(sK1,sK2,sK3,sK4)),il(sK1,sK2,sK3,sK4),f813(sK1,sK2,sK3,sK4,il(sK1,sK2,sK3,sK4)))
| il(sK1,sK2,sK3,sK4) = f813(sK1,sK2,sK3,sK4,il(sK1,sK2,sK3,sK4)) ),
inference(instantiation,[status(thm)],[135]) ).
fof(aSatz3_1,plain,
! [Xa,Xb] : s_t(Xa,Xb,Xb),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aSatz3_1) ).
cnf(23,plain,
s_t(X0,X1,X1),
inference(cnf,[status(esa)],[aSatz3_1]) ).
cnf(l29,plain,
s_t(f813(sK1,sK2,sK3,sK4,il(sK1,sK2,sK3,sK4)),f813(sK1,sK2,sK3,sK4,il(sK1,sK2,sK3,sK4)),f813(sK1,sK2,sK3,sK4,il(sK1,sK2,sK3,sK4))),
inference(instantiation,[status(thm)],[23]) ).
fof(aSatz8_13a,plain,
! [Xa,Xb,Xc,Xp,Xq] :
( ( ~ perpAt(Xa,Xb,Xc,Xp,Xq)
| Xa != Xb )
& ( ~ perpAt(Xa,Xb,Xc,Xp,Xq)
| Xp != Xq )
& ( ~ perpAt(Xa,Xb,Xc,Xp,Xq)
| s_col(Xp,Xq,Xc) )
& ( ~ perpAt(Xa,Xb,Xc,Xp,Xq)
| s_col(Xa,Xb,Xc) )
& ( ~ perpAt(Xa,Xb,Xc,Xp,Xq)
| s_col(Xa,Xb,f813(Xa,Xb,Xp,Xq,Xc)) )
& ( ~ perpAt(Xa,Xb,Xc,Xp,Xq)
| s_col(Xp,Xq,g813(Xa,Xb,Xp,Xq,Xc)) )
& ( ~ perpAt(Xa,Xb,Xc,Xp,Xq)
| Xc != f813(Xa,Xb,Xp,Xq,Xc) )
& ( ~ perpAt(Xa,Xb,Xc,Xp,Xq)
| Xc != g813(Xa,Xb,Xp,Xq,Xc) )
& ( ~ perpAt(Xa,Xb,Xc,Xp,Xq)
| s_r(f813(Xa,Xb,Xp,Xq,Xc),Xc,g813(Xa,Xb,Xp,Xq,Xc)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aSatz8_13a) ).
cnf(148,plain,
( X0 != f813(X1,X2,X3,X4,X0)
| ~ perpAt(X1,X2,X0,X3,X4) ),
inference(cnf,[status(esa)],[aSatz8_13a]) ).
cnf(l30,plain,
( il(sK1,sK2,sK3,sK4) != f813(sK1,sK2,sK3,sK4,il(sK1,sK2,sK3,sK4))
| ~ perpAt(sK1,sK2,il(sK1,sK2,sK3,sK4),sK3,sK4) ),
inference(instantiation,[status(thm)],[148]) ).
cnf(146,plain,
( ~ perpAt(X0,X1,X2,X3,X4)
| s_col(X0,X1,f813(X0,X1,X3,X4,X2)) ),
inference(cnf,[status(esa)],[aSatz8_13a]) ).
cnf(l3,plain,
( ~ perpAt(sK1,sK2,il(sK1,sK2,sK3,sK4),sK3,sK4)
| s_col(sK1,sK2,f813(sK1,sK2,sK3,sK4,il(sK1,sK2,sK3,sK4))) ),
inference(instantiation,[status(thm)],[146]) ).
fof(aSatz6_18,plain,
! [Xa,Xb,Xp,Xq,Xr] :
( Xa = Xb
| Xp = Xq
| ~ s_col(Xp,Xq,Xa)
| ~ s_col(Xp,Xq,Xb)
| ~ s_col(Xp,Xq,Xr)
| s_col(Xa,Xb,Xr) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aSatz6_18) ).
cnf(102,plain,
( ~ s_col(X0,X1,X2)
| ~ s_col(X0,X1,X3)
| ~ s_col(X0,X1,X4)
| X2 = X3
| X0 = X1
| s_col(X2,X3,X4) ),
inference(cnf,[status(esa)],[aSatz6_18]) ).
cnf(l14,plain,
( ~ s_col(sK1,sK2,sK3)
| ~ s_col(sK1,sK2,sK4)
| ~ s_col(sK1,sK2,f813(sK1,sK2,sK3,sK4,il(sK1,sK2,sK3,sK4)))
| sK3 = sK4
| sK1 = sK2
| s_col(sK3,sK4,f813(sK1,sK2,sK3,sK4,il(sK1,sK2,sK3,sK4))) ),
inference(instantiation,[status(thm)],[102]) ).
cnf(206,plain,
( X0 != X1
| ~ perpAt(X2,X3,X4,X0,X1) ),
inference(cnf,[status(esa)],[d_Defn8_11a]) ).
cnf(l16,plain,
( sK3 != sK4
| ~ perpAt(sK1,sK2,il(sK1,sK2,sK3,sK4),sK3,sK4) ),
inference(instantiation,[status(thm)],[206]) ).
cnf(153,plain,
s_col(sK1,sK2,sK3),
inference(cnf,[status(esa)],[aSatz8_14a_negated]) ).
cnf(l17,plain,
s_col(sK1,sK2,sK3),
inference(instantiation,[status(thm)],[153]) ).
cnf(l24,plain,
( ~ perpAt(sK1,sK2,il(sK1,sK2,sK3,sK4),sK3,sK4)
| s_col(sK1,sK2,f813(sK1,sK2,sK3,sK4,il(sK1,sK2,sK3,sK4))) ),
inference(instantiation,[status(thm)],[146]) ).
cnf(154,plain,
s_col(sK1,sK2,sK4),
inference(cnf,[status(esa)],[aSatz8_14a_negated]) ).
cnf(l15,plain,
s_col(sK1,sK2,sK4),
inference(instantiation,[status(thm)],[154]) ).
cnf(205,plain,
( X0 != X1
| ~ perpAt(X0,X1,X2,X3,X4) ),
inference(cnf,[status(esa)],[d_Defn8_11a]) ).
cnf(l20,plain,
( sK1 != sK2
| ~ perpAt(sK1,sK2,il(sK1,sK2,sK3,sK4),sK3,sK4) ),
inference(instantiation,[status(thm)],[205]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l1,l2,l25,l29,l30,l3,l14,l16,l17,l24,l15,l20]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.08 % Problem : GEO507+1 : TPTP v9.0.0. Released v7.0.0.
% 0.04/0.08 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.27 % Computer : n032.cluster.edu
% 0.08/0.27 % Model : x86_64 x86_64
% 0.08/0.27 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.27 % Memory : 8042.1875MB
% 0.08/0.27 % OS : Linux 3.10.0-693.el7.x86_64
% 0.08/0.27 % CPULimit : 300
% 0.08/0.27 % WCLimit : 300
% 0.08/0.27 % DateTime : Sun Jul 20 12:32:04 EDT 2025
% 0.08/0.27 % CPUTime :
% 0.08/0.28 % launching worker at depth: 4
% 0.08/0.28 % launching worker at depth: 1
% 0.08/0.28 % launching worker at depth: 5
% 0.08/0.28 % launching worker at depth: 3
% 0.08/0.28 % launching worker at depth: 2
% 0.08/0.28 % launching worker at depth: 6
% 0.08/0.28 % launching worker at depth: 7
% 0.08/0.28 % launching worker at depth: 8
% 0.08/0.28 % launching worker at depth: 9
% 0.13/0.35 % launching worker at depth: 10
% 9.51/1.48 % SZS status Theorem for theBenchmark
% 9.51/1.48 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------