%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : GEO010-1 : TPTP v9.0.0. Bugfixed v2.5.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 : n026.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:26 PM UTC 2025
% Result : Unsatisfiable 8.30s 2.94s
% Output : CNFRefutation 8.48s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 13
% Syntax : Number of formulae : 148 ( 91 unt; 0 typ; 0 def)
% Number of atoms : 248 ( 25 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 235 ( 135 ~; 100 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-4 aty)
% Number of functors : 11 ( 11 usr; 6 con; 0-6 aty)
% Number of variables : 117 ( 117 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ equidistant > colinear > between > continuous > outer_pasch > euclid2 > euclid1 > extension > #nlpp > lower_dimension_point_3 > lower_dimension_point_2 > lower_dimension_point_1 > c > b > a
%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(a,type,
a: $i ).
tff(outer_pasch,type,
outer_pasch: ( $i * $i * $i * $i * $i ) > $i ).
tff(lower_dimension_point_2,type,
lower_dimension_point_2: $i ).
tff(colinear,type,
colinear: ( $i * $i * $i ) > $o ).
tff(equidistant,type,
equidistant: ( $i * $i * $i * $i ) > $o ).
tff(b,type,
b: $i ).
tff(lower_dimension_point_3,type,
lower_dimension_point_3: $i ).
tff(extension,type,
extension: ( $i * $i * $i * $i ) > $i ).
tff(euclid1,type,
euclid1: ( $i * $i * $i * $i * $i ) > $i ).
tff(between,type,
between: ( $i * $i * $i ) > $o ).
tff(continuous,type,
continuous: ( $i * $i * $i * $i * $i * $i ) > $i ).
tff(c,type,
c: $i ).
tff(f_167,axiom,
! [Y,X,W,V] : equidistant(Y,extension(X,Y,W,V),W,V),
file(unknown,unknown) ).
tff(f_87,axiom,
! [X,Y,Z] :
( ~ equidistant(X,Y,Z,Z)
| ( X = Y ) ),
file(unknown,unknown) ).
tff(f_165,axiom,
! [X,Y,W,V] : between(X,Y,extension(X,Y,W,V)),
file(unknown,unknown) ).
tff(f_255,axiom,
! [X,Y,Z] :
( ~ between(X,Y,Z)
| colinear(X,Y,Z) ),
file(unknown,unknown) ).
tff(f_265,axiom,
! [X,Z,Y] :
( ~ between(X,Z,Y)
| colinear(X,Y,Z) ),
file(unknown,unknown) ).
tff(f_268,axiom,
colinear(a,b,c),
file(unknown,unknown) ).
tff(f_250,axiom,
! [X,Y,Z] :
( ~ colinear(X,Y,Z)
| between(X,Y,Z)
| between(Y,X,Z)
| between(X,Z,Y) ),
file(unknown,unknown) ).
tff(f_260,axiom,
! [Y,X,Z] :
( ~ between(Y,X,Z)
| colinear(X,Y,Z) ),
file(unknown,unknown) ).
tff(f_282,axiom,
( ~ colinear(a,c,b)
| ~ colinear(b,a,c)
| ~ colinear(b,c,a)
| ~ colinear(c,a,b)
| ~ colinear(c,b,a) ),
file(unknown,unknown) ).
tff(f_103,axiom,
! [W,Z,X,Y,V] :
( ~ between(X,W,V)
| ~ between(Y,V,Z)
| between(X,outer_pasch(W,X,Y,Z,V),Y) ),
file(unknown,unknown) ).
tff(f_60,axiom,
! [X,Y] :
( ~ between(X,Y,X)
| ( X = Y ) ),
file(unknown,unknown) ).
tff(f_111,axiom,
! [W,Z,X,Y,V] :
( ~ between(X,W,V)
| ~ between(Y,V,Z)
| between(Z,W,outer_pasch(W,X,Y,Z,V)) ),
file(unknown,unknown) ).
tff(f_68,axiom,
! [X,Y,V,Z] :
( ~ between(X,Y,V)
| ~ between(Y,Z,V)
| between(X,Y,Z) ),
file(unknown,unknown) ).
tff(c_66,plain,
! [Y_112,X_113,W_114,V_115] : equidistant(Y_112,extension(X_113,Y_112,W_114,V_115),W_114,V_115),
inference(cnfTransformation,[status(thm)],[f_167]) ).
tff(c_10,plain,
! [Y_14,X_13,Z_15] :
( ( Y_14 = X_13 )
| ~ equidistant(X_13,Y_14,Z_15,Z_15) ),
inference(cnfTransformation,[status(thm)],[f_87]) ).
tff(c_72,plain,
! [X_116,Y_117,V_118] : ( extension(X_116,Y_117,V_118,V_118) = Y_117 ),
inference(resolution,[status(thm)],[c_66,c_10]) ).
tff(c_26,plain,
! [X_55,Y_56,W_57,V_58] : between(X_55,Y_56,extension(X_55,Y_56,W_57,V_58)),
inference(cnfTransformation,[status(thm)],[f_165]) ).
tff(c_81,plain,
! [X_116,Y_117] : between(X_116,Y_117,Y_117),
inference(superposition,[status(thm),theory(equality)],[c_72,c_26]) ).
tff(c_44,plain,
! [X_83,Y_84,Z_85] :
( colinear(X_83,Y_84,Z_85)
| ~ between(X_83,Y_84,Z_85) ),
inference(cnfTransformation,[status(thm)],[f_255]) ).
tff(c_48,plain,
! [X_89,Y_91,Z_90] :
( colinear(X_89,Y_91,Z_90)
| ~ between(X_89,Z_90,Y_91) ),
inference(cnfTransformation,[status(thm)],[f_265]) ).
tff(c_50,plain,
colinear(a,b,c),
inference(cnfTransformation,[status(thm)],[f_268]) ).
tff(c_138,plain,
! [X_142,Z_143,Y_144] :
( between(X_142,Z_143,Y_144)
| between(Y_144,X_142,Z_143)
| between(X_142,Y_144,Z_143)
| ~ colinear(X_142,Y_144,Z_143) ),
inference(cnfTransformation,[status(thm)],[f_250]) ).
tff(c_154,plain,
( between(a,c,b)
| between(b,a,c)
| between(a,b,c) ),
inference(resolution,[status(thm)],[c_50,c_138]) ).
tff(c_358,plain,
between(a,b,c),
inference(splitLeft,[status(thm)],[c_154]) ).
tff(c_46,plain,
! [X_87,Y_86,Z_88] :
( colinear(X_87,Y_86,Z_88)
| ~ between(Y_86,X_87,Z_88) ),
inference(cnfTransformation,[status(thm)],[f_260]) ).
tff(c_52,plain,
( ~ colinear(c,b,a)
| ~ colinear(c,a,b)
| ~ colinear(b,c,a)
| ~ colinear(b,a,c)
| ~ colinear(a,c,b) ),
inference(cnfTransformation,[status(thm)],[f_282]) ).
tff(c_601,plain,
~ colinear(a,c,b),
inference(splitLeft,[status(thm)],[c_52]) ).
tff(c_610,plain,
~ between(a,b,c),
inference(resolution,[status(thm)],[c_48,c_601]) ).
tff(c_616,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_358,c_610]) ).
tff(c_617,plain,
( ~ colinear(b,a,c)
| ~ colinear(b,c,a)
| ~ colinear(c,a,b)
| ~ colinear(c,b,a) ),
inference(splitRight,[status(thm)],[c_52]) ).
tff(c_699,plain,
~ colinear(c,b,a),
inference(splitLeft,[status(thm)],[c_617]) ).
tff(c_709,plain,
~ between(c,b,a),
inference(resolution,[status(thm)],[c_44,c_699]) ).
tff(c_290,plain,
! [Z_183,V_180,X_181,Y_182,W_184] :
( between(X_181,outer_pasch(W_184,X_181,Y_182,Z_183,V_180),Y_182)
| ~ between(Y_182,V_180,Z_183)
| ~ between(X_181,W_184,V_180) ),
inference(cnfTransformation,[status(thm)],[f_103]) ).
tff(c_2,plain,
! [Y_2,X_1] :
( ( Y_2 = X_1 )
| ~ between(X_1,Y_2,X_1) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_1264,plain,
! [W_353,Y_354,Z_355,V_356] :
( ( outer_pasch(W_353,Y_354,Y_354,Z_355,V_356) = Y_354 )
| ~ between(Y_354,V_356,Z_355)
| ~ between(Y_354,W_353,V_356) ),
inference(resolution,[status(thm)],[c_290,c_2]) ).
tff(c_1295,plain,
! [W_357] :
( ( outer_pasch(W_357,a,a,c,b) = a )
| ~ between(a,W_357,b) ),
inference(resolution,[status(thm)],[c_358,c_1264]) ).
tff(c_1312,plain,
outer_pasch(b,a,a,c,b) = a,
inference(resolution,[status(thm)],[c_81,c_1295]) ).
tff(c_16,plain,
! [W_27,Z_28,X_29,V_31,Y_30] :
( between(Z_28,W_27,outer_pasch(W_27,X_29,Y_30,Z_28,V_31))
| ~ between(Y_30,V_31,Z_28)
| ~ between(X_29,W_27,V_31) ),
inference(cnfTransformation,[status(thm)],[f_111]) ).
tff(c_1319,plain,
( between(c,b,a)
| ~ between(a,b,c)
| ~ between(a,b,b) ),
inference(superposition,[status(thm),theory(equality)],[c_1312,c_16]) ).
tff(c_1325,plain,
between(c,b,a),
inference(demodulation,[status(thm),theory(equality)],[c_81,c_358,c_1319]) ).
tff(c_1327,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_709,c_1325]) ).
tff(c_1328,plain,
( ~ colinear(c,a,b)
| ~ colinear(b,c,a)
| ~ colinear(b,a,c) ),
inference(splitRight,[status(thm)],[c_617]) ).
tff(c_1341,plain,
~ colinear(b,a,c),
inference(splitLeft,[status(thm)],[c_1328]) ).
tff(c_1347,plain,
~ between(a,b,c),
inference(resolution,[status(thm)],[c_46,c_1341]) ).
tff(c_1355,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_358,c_1347]) ).
tff(c_1356,plain,
( ~ colinear(b,c,a)
| ~ colinear(c,a,b) ),
inference(splitRight,[status(thm)],[c_1328]) ).
tff(c_1363,plain,
~ colinear(c,a,b),
inference(splitLeft,[status(thm)],[c_1356]) ).
tff(c_1375,plain,
~ between(c,b,a),
inference(resolution,[status(thm)],[c_48,c_1363]) ).
tff(c_1750,plain,
! [W_427,Y_428,Z_429,V_430] :
( ( outer_pasch(W_427,Y_428,Y_428,Z_429,V_430) = Y_428 )
| ~ between(Y_428,V_430,Z_429)
| ~ between(Y_428,W_427,V_430) ),
inference(resolution,[status(thm)],[c_290,c_2]) ).
tff(c_1781,plain,
! [W_431] :
( ( outer_pasch(W_431,a,a,c,b) = a )
| ~ between(a,W_431,b) ),
inference(resolution,[status(thm)],[c_358,c_1750]) ).
tff(c_1791,plain,
outer_pasch(b,a,a,c,b) = a,
inference(resolution,[status(thm)],[c_81,c_1781]) ).
tff(c_1798,plain,
( between(c,b,a)
| ~ between(a,b,c)
| ~ between(a,b,b) ),
inference(superposition,[status(thm),theory(equality)],[c_1791,c_16]) ).
tff(c_1804,plain,
between(c,b,a),
inference(demodulation,[status(thm),theory(equality)],[c_81,c_358,c_1798]) ).
tff(c_1806,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1375,c_1804]) ).
tff(c_1807,plain,
~ colinear(b,c,a),
inference(splitRight,[status(thm)],[c_1356]) ).
tff(c_1820,plain,
~ between(b,a,c),
inference(resolution,[status(thm)],[c_48,c_1807]) ).
tff(c_1819,plain,
~ between(c,b,a),
inference(resolution,[status(thm)],[c_46,c_1807]) ).
tff(c_1818,plain,
~ between(b,c,a),
inference(resolution,[status(thm)],[c_44,c_1807]) ).
tff(c_1329,plain,
colinear(c,b,a),
inference(splitRight,[status(thm)],[c_617]) ).
tff(c_42,plain,
! [X_80,Z_82,Y_81] :
( between(X_80,Z_82,Y_81)
| between(Y_81,X_80,Z_82)
| between(X_80,Y_81,Z_82)
| ~ colinear(X_80,Y_81,Z_82) ),
inference(cnfTransformation,[status(thm)],[f_250]) ).
tff(c_1333,plain,
( between(c,a,b)
| between(b,c,a)
| between(c,b,a) ),
inference(resolution,[status(thm)],[c_1329,c_42]) ).
tff(c_1873,plain,
between(c,a,b),
inference(negUnitSimplification,[status(thm)],[c_1819,c_1818,c_1333]) ).
tff(c_2218,plain,
! [W_489,Y_490,Z_491,V_492] :
( ( outer_pasch(W_489,Y_490,Y_490,Z_491,V_492) = Y_490 )
| ~ between(Y_490,V_492,Z_491)
| ~ between(Y_490,W_489,V_492) ),
inference(resolution,[status(thm)],[c_290,c_2]) ).
tff(c_2252,plain,
! [W_493] :
( ( outer_pasch(W_493,c,c,b,a) = c )
| ~ between(c,W_493,a) ),
inference(resolution,[status(thm)],[c_1873,c_2218]) ).
tff(c_2262,plain,
outer_pasch(a,c,c,b,a) = c,
inference(resolution,[status(thm)],[c_81,c_2252]) ).
tff(c_2269,plain,
( between(b,a,c)
| ~ between(c,a,b)
| ~ between(c,a,a) ),
inference(superposition,[status(thm),theory(equality)],[c_2262,c_16]) ).
tff(c_2275,plain,
between(b,a,c),
inference(demodulation,[status(thm),theory(equality)],[c_81,c_1873,c_2269]) ).
tff(c_2277,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1820,c_2275]) ).
tff(c_2279,plain,
~ between(a,b,c),
inference(splitRight,[status(thm)],[c_154]) ).
tff(c_2278,plain,
( between(b,a,c)
| between(a,c,b) ),
inference(splitRight,[status(thm)],[c_154]) ).
tff(c_2293,plain,
between(a,c,b),
inference(splitLeft,[status(thm)],[c_2278]) ).
tff(c_4,plain,
! [X_3,Y_4,Z_6,V_5] :
( between(X_3,Y_4,Z_6)
| ~ between(Y_4,Z_6,V_5)
| ~ between(X_3,Y_4,V_5) ),
inference(cnfTransformation,[status(thm)],[f_68]) ).
tff(c_2300,plain,
! [X_498] :
( between(X_498,a,c)
| ~ between(X_498,a,b) ),
inference(resolution,[status(thm)],[c_2293,c_4]) ).
tff(c_2311,plain,
( ( c = a )
| ~ between(c,a,b) ),
inference(resolution,[status(thm)],[c_2300,c_2]) ).
tff(c_2312,plain,
~ between(c,a,b),
inference(splitLeft,[status(thm)],[c_2311]) ).
tff(c_2527,plain,
~ colinear(a,c,b),
inference(splitLeft,[status(thm)],[c_52]) ).
tff(c_2530,plain,
~ between(a,c,b),
inference(resolution,[status(thm)],[c_44,c_2527]) ).
tff(c_2540,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2293,c_2530]) ).
tff(c_2541,plain,
( ~ colinear(b,a,c)
| ~ colinear(b,c,a)
| ~ colinear(c,a,b)
| ~ colinear(c,b,a) ),
inference(splitRight,[status(thm)],[c_52]) ).
tff(c_2678,plain,
~ colinear(c,b,a),
inference(splitLeft,[status(thm)],[c_2541]) ).
tff(c_2689,plain,
~ between(b,c,a),
inference(resolution,[status(thm)],[c_46,c_2678]) ).
tff(c_3584,plain,
! [W_681,Y_682,Z_683,V_684] :
( ( outer_pasch(W_681,Y_682,Y_682,Z_683,V_684) = Y_682 )
| ~ between(Y_682,V_684,Z_683)
| ~ between(Y_682,W_681,V_684) ),
inference(resolution,[status(thm)],[c_290,c_2]) ).
tff(c_3612,plain,
! [W_685] :
( ( outer_pasch(W_685,a,a,b,c) = a )
| ~ between(a,W_685,c) ),
inference(resolution,[status(thm)],[c_2293,c_3584]) ).
tff(c_3627,plain,
outer_pasch(c,a,a,b,c) = a,
inference(resolution,[status(thm)],[c_81,c_3612]) ).
tff(c_3634,plain,
( between(b,c,a)
| ~ between(a,c,b)
| ~ between(a,c,c) ),
inference(superposition,[status(thm),theory(equality)],[c_3627,c_16]) ).
tff(c_3640,plain,
between(b,c,a),
inference(demodulation,[status(thm),theory(equality)],[c_81,c_2293,c_3634]) ).
tff(c_3642,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_2689,c_3640]) ).
tff(c_3644,plain,
colinear(c,b,a),
inference(splitRight,[status(thm)],[c_2541]) ).
tff(c_3647,plain,
( between(c,a,b)
| between(b,c,a)
| between(c,b,a) ),
inference(resolution,[status(thm)],[c_3644,c_42]) ).
tff(c_3650,plain,
( between(b,c,a)
| between(c,b,a) ),
inference(negUnitSimplification,[status(thm)],[c_2312,c_3647]) ).
tff(c_3699,plain,
between(c,b,a),
inference(splitLeft,[status(thm)],[c_3650]) ).
tff(c_4295,plain,
! [W_762,Y_763,Z_764,V_765] :
( ( outer_pasch(W_762,Y_763,Y_763,Z_764,V_765) = Y_763 )
| ~ between(Y_763,V_765,Z_764)
| ~ between(Y_763,W_762,V_765) ),
inference(resolution,[status(thm)],[c_290,c_2]) ).
tff(c_4329,plain,
! [W_766] :
( ( outer_pasch(W_766,c,c,a,b) = c )
| ~ between(c,W_766,b) ),
inference(resolution,[status(thm)],[c_3699,c_4295]) ).
tff(c_4344,plain,
outer_pasch(b,c,c,a,b) = c,
inference(resolution,[status(thm)],[c_81,c_4329]) ).
tff(c_4351,plain,
( between(a,b,c)
| ~ between(c,b,a)
| ~ between(c,b,b) ),
inference(superposition,[status(thm),theory(equality)],[c_4344,c_16]) ).
tff(c_4357,plain,
between(a,b,c),
inference(demodulation,[status(thm),theory(equality)],[c_81,c_3699,c_4351]) ).
tff(c_4359,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_2279,c_4357]) ).
tff(c_4360,plain,
between(b,c,a),
inference(splitRight,[status(thm)],[c_3650]) ).
tff(c_3643,plain,
( ~ colinear(c,a,b)
| ~ colinear(b,c,a)
| ~ colinear(b,a,c) ),
inference(splitRight,[status(thm)],[c_2541]) ).
tff(c_4409,plain,
~ colinear(b,a,c),
inference(splitLeft,[status(thm)],[c_3643]) ).
tff(c_4418,plain,
~ between(b,c,a),
inference(resolution,[status(thm)],[c_48,c_4409]) ).
tff(c_4424,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_4360,c_4418]) ).
tff(c_4425,plain,
( ~ colinear(b,c,a)
| ~ colinear(c,a,b) ),
inference(splitRight,[status(thm)],[c_3643]) ).
tff(c_4433,plain,
~ colinear(c,a,b),
inference(splitLeft,[status(thm)],[c_4425]) ).
tff(c_4439,plain,
~ between(a,c,b),
inference(resolution,[status(thm)],[c_46,c_4433]) ).
tff(c_4447,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2293,c_4439]) ).
tff(c_4448,plain,
~ colinear(b,c,a),
inference(splitRight,[status(thm)],[c_4425]) ).
tff(c_4518,plain,
~ between(b,c,a),
inference(resolution,[status(thm)],[c_44,c_4448]) ).
tff(c_4528,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_4360,c_4518]) ).
tff(c_4529,plain,
c = a,
inference(splitRight,[status(thm)],[c_2311]) ).
tff(c_4530,plain,
between(c,a,b),
inference(splitRight,[status(thm)],[c_2311]) ).
tff(c_4540,plain,
between(a,a,b),
inference(demodulation,[status(thm),theory(equality)],[c_4529,c_4530]) ).
tff(c_4534,plain,
colinear(a,b,a),
inference(demodulation,[status(thm),theory(equality)],[c_4529,c_50]) ).
tff(c_4734,plain,
( ~ colinear(b,a,a)
| ~ colinear(a,a,b) ),
inference(demodulation,[status(thm),theory(equality)],[c_4529,c_4529,c_4529,c_4529,c_4534,c_4529,c_52]) ).
tff(c_4735,plain,
~ colinear(a,a,b),
inference(splitLeft,[status(thm)],[c_4734]) ).
tff(c_4738,plain,
~ between(a,a,b),
inference(resolution,[status(thm)],[c_44,c_4735]) ).
tff(c_4748,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_4540,c_4738]) ).
tff(c_4749,plain,
~ colinear(b,a,a),
inference(splitRight,[status(thm)],[c_4734]) ).
tff(c_4753,plain,
~ between(b,a,a),
inference(resolution,[status(thm)],[c_44,c_4749]) ).
tff(c_4763,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_81,c_4753]) ).
tff(c_4764,plain,
between(b,a,c),
inference(splitRight,[status(thm)],[c_2278]) ).
tff(c_4765,plain,
~ between(a,c,b),
inference(splitRight,[status(thm)],[c_2278]) ).
tff(c_4949,plain,
~ colinear(a,c,b),
inference(splitLeft,[status(thm)],[c_52]) ).
tff(c_4960,plain,
~ between(c,a,b),
inference(resolution,[status(thm)],[c_46,c_4949]) ).
tff(c_5734,plain,
! [W_995,Y_996,Z_997,V_998] :
( ( outer_pasch(W_995,Y_996,Y_996,Z_997,V_998) = Y_996 )
| ~ between(Y_996,V_998,Z_997)
| ~ between(Y_996,W_995,V_998) ),
inference(resolution,[status(thm)],[c_290,c_2]) ).
tff(c_5765,plain,
! [W_999] :
( ( outer_pasch(W_999,b,b,c,a) = b )
| ~ between(b,W_999,a) ),
inference(resolution,[status(thm)],[c_4764,c_5734]) ).
tff(c_5782,plain,
outer_pasch(a,b,b,c,a) = b,
inference(resolution,[status(thm)],[c_81,c_5765]) ).
tff(c_5789,plain,
( between(c,a,b)
| ~ between(b,a,c)
| ~ between(b,a,a) ),
inference(superposition,[status(thm),theory(equality)],[c_5782,c_16]) ).
tff(c_5795,plain,
between(c,a,b),
inference(demodulation,[status(thm),theory(equality)],[c_81,c_4764,c_5789]) ).
tff(c_5797,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_4960,c_5795]) ).
tff(c_5799,plain,
colinear(a,c,b),
inference(splitRight,[status(thm)],[c_52]) ).
tff(c_5802,plain,
( between(a,b,c)
| between(c,a,b)
| between(a,c,b) ),
inference(resolution,[status(thm)],[c_5799,c_42]) ).
tff(c_5805,plain,
between(c,a,b),
inference(negUnitSimplification,[status(thm)],[c_4765,c_2279,c_5802]) ).
tff(c_5798,plain,
( ~ colinear(b,a,c)
| ~ colinear(b,c,a)
| ~ colinear(c,a,b)
| ~ colinear(c,b,a) ),
inference(splitRight,[status(thm)],[c_52]) ).
tff(c_5890,plain,
~ colinear(c,b,a),
inference(splitLeft,[status(thm)],[c_5798]) ).
tff(c_5899,plain,
~ between(c,a,b),
inference(resolution,[status(thm)],[c_48,c_5890]) ).
tff(c_5905,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_5805,c_5899]) ).
tff(c_5906,plain,
( ~ colinear(c,a,b)
| ~ colinear(b,c,a)
| ~ colinear(b,a,c) ),
inference(splitRight,[status(thm)],[c_5798]) ).
tff(c_5913,plain,
~ colinear(b,a,c),
inference(splitLeft,[status(thm)],[c_5906]) ).
tff(c_5960,plain,
~ between(b,a,c),
inference(resolution,[status(thm)],[c_44,c_5913]) ).
tff(c_5970,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_4764,c_5960]) ).
tff(c_5971,plain,
( ~ colinear(b,c,a)
| ~ colinear(c,a,b) ),
inference(splitRight,[status(thm)],[c_5906]) ).
tff(c_5979,plain,
~ colinear(c,a,b),
inference(splitLeft,[status(thm)],[c_5971]) ).
tff(c_5982,plain,
~ between(c,a,b),
inference(resolution,[status(thm)],[c_44,c_5979]) ).
tff(c_5992,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_5805,c_5982]) ).
tff(c_5993,plain,
~ colinear(b,c,a),
inference(splitRight,[status(thm)],[c_5971]) ).
tff(c_6003,plain,
~ between(b,a,c),
inference(resolution,[status(thm)],[c_48,c_5993]) ).
tff(c_6009,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_4764,c_6003]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.02/0.12 % Problem : GEO010-1 : TPTP v9.0.0. Bugfixed v2.5.0.
% 0.02/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.12/0.33 % Computer : n026.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Mon Apr 7 19:16:08 EDT 2025
% 0.12/0.33 % CPUTime :
% 8.30/2.94 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 8.48/2.97
% 8.48/2.97 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------