%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : GEO026-3 : TPTP v9.0.0. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n011.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 : Wed Apr 9 06:13:31 PM UTC 2025
% Result : Unsatisfiable 148.05s 129.00s
% Output : CNFRefutation 148.08s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 8
% Syntax : Number of formulae : 24 ( 14 unt; 0 typ; 0 def)
% Number of atoms : 59 ( 14 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 69 ( 34 ~; 35 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 5 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-4 aty)
% Number of functors : 13 ( 13 usr; 7 con; 0-6 aty)
% Number of variables : 38 ( 38 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ equidistant > between > continuous > inner_pasch > euclid2 > euclid1 > extension > reflection > #nlpp > x > w > v > u > lower_dimension_point_3 > lower_dimension_point_2 > lower_dimension_point_1
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(lower_dimension_point_1,type,
lower_dimension_point_1: $i ).
tff(euclid2,type,
euclid2: ( $i * $i * $i * $i * $i ) > $i ).
tff(x,type,
x: $i ).
tff(lower_dimension_point_2,type,
lower_dimension_point_2: $i ).
tff(w,type,
w: $i ).
tff(equidistant,type,
equidistant: ( $i * $i * $i * $i ) > $o ).
tff(u,type,
u: $i ).
tff(lower_dimension_point_3,type,
lower_dimension_point_3: $i ).
tff(v,type,
v: $i ).
tff(extension,type,
extension: ( $i * $i * $i * $i ) > $i ).
tff(reflection,type,
reflection: ( $i * $i ) > $i ).
tff(euclid1,type,
euclid1: ( $i * $i * $i * $i * $i ) > $i ).
tff(between,type,
between: ( $i * $i * $i ) > $o ).
tff(inner_pasch,type,
inner_pasch: ( $i * $i * $i * $i * $i ) > $i ).
tff(continuous,type,
continuous: ( $i * $i * $i * $i * $i * $i ) > $i ).
tff(f_338,axiom,
w != x,
file(unknown,unknown) ).
tff(f_249,axiom,
! [U,V] : equidistant(U,V,U,V),
file(unknown,unknown) ).
tff(f_336,axiom,
u != v,
file(unknown,unknown) ).
tff(f_334,axiom,
equidistant(v,w,v,x),
file(unknown,unknown) ).
tff(f_332,axiom,
between(u,v,w),
file(unknown,unknown) ).
tff(f_333,axiom,
between(u,v,x),
file(unknown,unknown) ).
tff(f_101,axiom,
! [Y1,Z,X1,V1,X,Y,V,Z1] :
( ~ equidistant(X,Y,X1,Y1)
| ~ equidistant(Y,Z,Y1,Z1)
| ~ equidistant(X,V,X1,V1)
| ~ equidistant(Y,V,Y1,V1)
| ~ between(X,Y,Z)
| ~ between(X1,Y1,Z1)
| ( X = Y )
| equidistant(Z,V,Z1,V1) ),
file(unknown,unknown) ).
tff(f_71,axiom,
! [X,Y,Z] :
( ~ equidistant(X,Y,Z,Z)
| ( X = Y ) ),
file(unknown,unknown) ).
tff(c_84,plain,
x != w,
inference(cnfTransformation,[status(thm)],[f_338]) ).
tff(c_40,plain,
! [U_74,V_75] : equidistant(U_74,V_75,U_74,V_75),
inference(cnfTransformation,[status(thm)],[f_249]) ).
tff(c_82,plain,
v != u,
inference(cnfTransformation,[status(thm)],[f_336]) ).
tff(c_80,plain,
equidistant(v,w,v,x),
inference(cnfTransformation,[status(thm)],[f_334]) ).
tff(c_76,plain,
between(u,v,w),
inference(cnfTransformation,[status(thm)],[f_332]) ).
tff(c_78,plain,
between(u,v,x),
inference(cnfTransformation,[status(thm)],[f_333]) ).
tff(c_1582,plain,
! [V_303,Z1_301,V1_307,Z_302,Y1_304,Y_308,X_306,X1_305] :
( equidistant(Z_302,V_303,Z1_301,V1_307)
| ( Y_308 = X_306 )
| ~ between(X1_305,Y1_304,Z1_301)
| ~ between(X_306,Y_308,Z_302)
| ~ equidistant(Y_308,V_303,Y1_304,V1_307)
| ~ equidistant(X_306,V_303,X1_305,V1_307)
| ~ equidistant(Y_308,Z_302,Y1_304,Z1_301)
| ~ equidistant(X_306,Y_308,X1_305,Y1_304) ),
inference(cnfTransformation,[status(thm)],[f_101]) ).
tff(c_6193,plain,
! [X_482,Y_483,V1_484,Z_486,V_485] :
( equidistant(Z_486,V_485,x,V1_484)
| ( Y_483 = X_482 )
| ~ between(X_482,Y_483,Z_486)
| ~ equidistant(Y_483,V_485,v,V1_484)
| ~ equidistant(X_482,V_485,u,V1_484)
| ~ equidistant(Y_483,Z_486,v,x)
| ~ equidistant(X_482,Y_483,u,v) ),
inference(resolution,[status(thm)],[c_78,c_1582]) ).
tff(c_6213,plain,
! [V_485,V1_484] :
( equidistant(w,V_485,x,V1_484)
| ( v = u )
| ~ equidistant(v,V_485,v,V1_484)
| ~ equidistant(u,V_485,u,V1_484)
| ~ equidistant(v,w,v,x)
| ~ equidistant(u,v,u,v) ),
inference(resolution,[status(thm)],[c_76,c_6193]) ).
tff(c_6227,plain,
! [V_485,V1_484] :
( equidistant(w,V_485,x,V1_484)
| ( v = u )
| ~ equidistant(v,V_485,v,V1_484)
| ~ equidistant(u,V_485,u,V1_484) ),
inference(demodulation,[status(thm),theory(equality)],[c_40,c_80,c_6213]) ).
tff(c_40106,plain,
! [V_1199,V1_1200] :
( equidistant(w,V_1199,x,V1_1200)
| ~ equidistant(v,V_1199,v,V1_1200)
| ~ equidistant(u,V_1199,u,V1_1200) ),
inference(negUnitSimplification,[status(thm)],[c_82,c_6227]) ).
tff(c_6,plain,
! [Y_10,X_9,Z_11] :
( ( Y_10 = X_9 )
| ~ equidistant(X_9,Y_10,Z_11,Z_11) ),
inference(cnfTransformation,[status(thm)],[f_71]) ).
tff(c_157974,plain,
! [V_3990] :
( ( w = V_3990 )
| ~ equidistant(v,V_3990,v,x)
| ~ equidistant(u,V_3990,u,x) ),
inference(resolution,[status(thm)],[c_40106,c_6]) ).
tff(c_158121,plain,
( ( x = w )
| ~ equidistant(u,x,u,x) ),
inference(resolution,[status(thm)],[c_40,c_157974]) ).
tff(c_158164,plain,
x = w,
inference(demodulation,[status(thm),theory(equality)],[c_40,c_158121]) ).
tff(c_158166,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_84,c_158164]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : GEO026-3 : TPTP v9.0.0. Released v1.0.0.
% 0.07/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.13/0.34 % Computer : n011.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Mon Apr 7 19:19:03 EDT 2025
% 0.13/0.34 % CPUTime :
% 148.05/129.00 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 148.05/129.01
% 148.05/129.01 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------