%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : GEO126+1 : TPTP v9.0.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n019.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:50 PM UTC 2025
% Result : Theorem 6.04s 2.38s
% Output : CNFRefutation 6.04s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 13
% Syntax : Number of formulae : 71 ( 25 unt; 0 typ; 0 def)
% Number of atoms : 144 ( 20 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 122 ( 49 ~; 46 |; 12 &)
% ( 10 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 15 ( 13 usr; 1 prp; 0-4 aty)
% Number of functors : 33 ( 33 usr; 1 con; 0-5 aty)
% Number of variables : 97 ( 90 !; 7 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ between_o > between_c > ordered_by > meet > start_point > part_of > inner_point > incident_o > incident_c > finish_point > end_point > open > closed > sum > #nlpp > underlying_curve > #skF_9 > #skF_7 > #skF_24 > #skF_11 > #skF_26 > #skF_6 > #skF_30 > #skF_31 > #skF_19 > #skF_17 > #skF_20 > #skF_8 > #skF_13 > #skF_14 > #skF_12 > #skF_18 > #skF_16 > #skF_10 > #skF_2 > #skF_23 > #skF_28 > #skF_25 > #skF_3 > #skF_29 > #skF_27 > #skF_1 > #skF_5 > #skF_22 > #skF_15 > #skF_4 > #skF_21
%Foreground sorts:
%Background operators:
%Foreground operators:
tff('#skF_9',type,
'#skF_9': $i > $i ).
tff(underlying_curve,type,
underlying_curve: $i > $i ).
tff('#skF_7',type,
'#skF_7': $i > $i ).
tff('#skF_24',type,
'#skF_24': ( $i * $i * $i ) > $i ).
tff(between_c,type,
between_c: ( $i * $i * $i * $i ) > $o ).
tff(closed,type,
closed: $i > $o ).
tff('#skF_11',type,
'#skF_11': ( $i * $i ) > $i ).
tff(inner_point,type,
inner_point: ( $i * $i ) > $o ).
tff(end_point,type,
end_point: ( $i * $i ) > $o ).
tff('#skF_26',type,
'#skF_26': ( $i * $i ) > $i ).
tff('#skF_6',type,
'#skF_6': ( $i * $i * $i ) > $i ).
tff('#skF_30',type,
'#skF_30': ( $i * $i ) > $i ).
tff(finish_point,type,
finish_point: ( $i * $i ) > $o ).
tff('#skF_31',type,
'#skF_31': $i ).
tff('#skF_19',type,
'#skF_19': $i > $i ).
tff('#skF_17',type,
'#skF_17': ( $i * $i ) > $i ).
tff(start_point,type,
start_point: ( $i * $i ) > $o ).
tff('#skF_20',type,
'#skF_20': ( $i * $i * $i * $i * $i ) > $i ).
tff('#skF_8',type,
'#skF_8': $i > $i ).
tff(part_of,type,
part_of: ( $i * $i ) > $o ).
tff('#skF_13',type,
'#skF_13': ( $i * $i ) > $i ).
tff(between_o,type,
between_o: ( $i * $i * $i * $i ) > $o ).
tff('#skF_14',type,
'#skF_14': ( $i * $i ) > $i ).
tff('#skF_12',type,
'#skF_12': ( $i * $i ) > $i ).
tff(meet,type,
meet: ( $i * $i * $i ) > $o ).
tff('#skF_18',type,
'#skF_18': ( $i * $i ) > $i ).
tff(incident_c,type,
incident_c: ( $i * $i ) > $o ).
tff('#skF_16',type,
'#skF_16': ( $i * $i * $i * $i ) > $i ).
tff('#skF_10',type,
'#skF_10': ( $i * $i ) > $i ).
tff('#skF_2',type,
'#skF_2': ( $i * $i * $i ) > $i ).
tff(sum,type,
sum: ( $i * $i ) > $i ).
tff(ordered_by,type,
ordered_by: ( $i * $i * $i ) > $o ).
tff('#skF_23',type,
'#skF_23': $i > $i ).
tff('#skF_28',type,
'#skF_28': ( $i * $i ) > $i ).
tff(incident_o,type,
incident_o: ( $i * $i ) > $o ).
tff('#skF_25',type,
'#skF_25': ( $i * $i ) > $i ).
tff('#skF_3',type,
'#skF_3': ( $i * $i * $i ) > $i ).
tff('#skF_29',type,
'#skF_29': ( $i * $i ) > $i ).
tff('#skF_27',type,
'#skF_27': ( $i * $i ) > $i ).
tff('#skF_1',type,
'#skF_1': ( $i * $i ) > $i ).
tff('#skF_5',type,
'#skF_5': ( $i * $i ) > $i ).
tff('#skF_22',type,
'#skF_22': ( $i * $i * $i * $i ) > $i ).
tff('#skF_15',type,
'#skF_15': ( $i * $i ) > $i ).
tff('#skF_4',type,
'#skF_4': ( $i * $i ) > $i ).
tff(open,type,
open: $i > $o ).
tff('#skF_21',type,
'#skF_21': ( $i * $i * $i * $i * $i ) > $i ).
tff(f_111,axiom,
! [C] :
( closed(C)
<=> ~ ? [P] : end_point(P,C) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004+0.ax',closed_defn) ).
tff(f_83,axiom,
! [P,C] :
( end_point(P,C)
<=> ( incident_c(P,C)
& ! [C1,C2] :
( ( part_of(C1,C)
& part_of(C2,C)
& incident_c(P,C1)
& incident_c(P,C2) )
=> ( part_of(C1,C2)
| part_of(C2,C1) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004+0.ax',end_point_defn) ).
tff(f_360,axiom,
! [C,O] :
( ( C = underlying_curve(O) )
<=> ! [P] :
( incident_o(P,O)
<=> incident_c(P,C) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004+2.ax',underlying_curve_defn) ).
tff(f_302,axiom,
! [P,O] :
( finish_point(P,O)
<=> ( incident_o(P,O)
& ! [Q] :
( ( ( P != Q )
& incident_o(Q,O) )
=> ordered_by(O,Q,P) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004+2.ax',finish_point_defn) ).
tff(f_369,negated_conjecture,
~ ! [O] :
? [P,Q] :
( ordered_by(O,P,Q)
& ( P != Q ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',theorem_4_11) ).
tff(f_316,axiom,
! [O] :
? [C] :
( open(C)
& ! [P] :
( incident_o(P,O)
<=> incident_c(P,C) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004+2.ax',o2) ).
tff(f_116,axiom,
! [C] :
( open(C)
<=> ? [P] : end_point(P,C) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004+0.ax',open_defn) ).
tff(f_57,axiom,
! [C,C1] :
( part_of(C1,C)
<=> ! [P] :
( incident_c(P,C1)
=> incident_c(P,C) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004+0.ax',part_of_defn) ).
tff(f_123,axiom,
! [C,C1] :
( ( part_of(C1,C)
& ( C1 != C ) )
=> open(C1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004+0.ax',c1) ).
tff(f_329,axiom,
! [O] :
? [P] : start_point(P,O),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004+2.ax',o4) ).
tff(f_290,axiom,
! [P,O] :
( start_point(P,O)
<=> ( incident_o(P,O)
& ! [Q] :
( ( ( P != Q )
& incident_o(Q,O) )
=> ordered_by(O,P,Q) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004+2.ax',start_point_defn) ).
tff(f_151,axiom,
! [C] :
? [P] : inner_point(P,C),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004+0.ax',c3) ).
tff(f_90,axiom,
! [P,C] :
( inner_point(P,C)
<=> ( incident_c(P,C)
& ~ end_point(P,C) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004+0.ax',inner_point_defn) ).
tff(c_64,plain,
! [C_28] :
( closed(C_28)
| end_point('#skF_7'(C_28),C_28) ),
inference(cnfTransformation,[status(thm)],[f_111]) ).
tff(c_28,plain,
! [P_12,C_13] :
( incident_c(P_12,C_13)
| ~ end_point(P_12,C_13) ),
inference(cnfTransformation,[status(thm)],[f_83]) ).
tff(c_280,plain,
! [P_183,O_184] :
( incident_o(P_183,O_184)
| ~ incident_c(P_183,underlying_curve(O_184)) ),
inference(cnfTransformation,[status(thm)],[f_360]) ).
tff(c_299,plain,
! [P_194,O_195] :
( incident_o(P_194,O_195)
| ~ end_point(P_194,underlying_curve(O_195)) ),
inference(resolution,[status(thm)],[c_28,c_280]) ).
tff(c_309,plain,
! [O_195] :
( incident_o('#skF_7'(underlying_curve(O_195)),O_195)
| closed(underlying_curve(O_195)) ),
inference(resolution,[status(thm)],[c_64,c_299]) ).
tff(c_1143,plain,
! [O_351,Q_352,P_353] :
( ordered_by(O_351,Q_352,P_353)
| ~ incident_o(Q_352,O_351)
| ( Q_352 = P_353 )
| ~ finish_point(P_353,O_351) ),
inference(cnfTransformation,[status(thm)],[f_302]) ).
tff(c_194,plain,
! [Q_137,P_136] :
( ( Q_137 = P_136 )
| ~ ordered_by('#skF_31',P_136,Q_137) ),
inference(cnfTransformation,[status(thm)],[f_369]) ).
tff(c_1157,plain,
! [Q_354,P_355] :
( ~ incident_o(Q_354,'#skF_31')
| ( Q_354 = P_355 )
| ~ finish_point(P_355,'#skF_31') ),
inference(resolution,[status(thm)],[c_1143,c_194]) ).
tff(c_1214,plain,
! [P_355] :
( ( P_355 = '#skF_7'(underlying_curve('#skF_31')) )
| ~ finish_point(P_355,'#skF_31')
| closed(underlying_curve('#skF_31')) ),
inference(resolution,[status(thm)],[c_309,c_1157]) ).
tff(c_1312,plain,
closed(underlying_curve('#skF_31')),
inference(splitLeft,[status(thm)],[c_1214]) ).
tff(c_150,plain,
! [O_95] : open('#skF_19'(O_95)),
inference(cnfTransformation,[status(thm)],[f_316]) ).
tff(c_232,plain,
! [C_165] :
( end_point('#skF_8'(C_165),C_165)
| ~ open(C_165) ),
inference(cnfTransformation,[status(thm)],[f_116]) ).
tff(c_62,plain,
! [P_31,C_28] :
( ~ end_point(P_31,C_28)
| ~ closed(C_28) ),
inference(cnfTransformation,[status(thm)],[f_111]) ).
tff(c_241,plain,
! [C_166] :
( ~ closed(C_166)
| ~ open(C_166) ),
inference(resolution,[status(thm)],[c_232,c_62]) ).
tff(c_249,plain,
! [O_95] : ~ closed('#skF_19'(O_95)),
inference(resolution,[status(thm)],[c_150,c_241]) ).
tff(c_349,plain,
! [C_205,C1_206] :
( incident_c('#skF_1'(C_205,C1_206),C1_206)
| part_of(C1_206,C_205) ),
inference(cnfTransformation,[status(thm)],[f_57]) ).
tff(c_184,plain,
! [P_133,O_130] :
( incident_o(P_133,O_130)
| ~ incident_c(P_133,underlying_curve(O_130)) ),
inference(cnfTransformation,[status(thm)],[f_360]) ).
tff(c_519,plain,
! [C_244,O_245] :
( incident_o('#skF_1'(C_244,underlying_curve(O_245)),O_245)
| part_of(underlying_curve(O_245),C_244) ),
inference(resolution,[status(thm)],[c_349,c_184]) ).
tff(c_146,plain,
! [P_100,O_95] :
( incident_c(P_100,'#skF_19'(O_95))
| ~ incident_o(P_100,O_95) ),
inference(cnfTransformation,[status(thm)],[f_316]) ).
tff(c_328,plain,
! [C_203,C1_204] :
( ~ incident_c('#skF_1'(C_203,C1_204),C_203)
| part_of(C1_204,C_203) ),
inference(cnfTransformation,[status(thm)],[f_57]) ).
tff(c_347,plain,
! [C1_204,O_95] :
( part_of(C1_204,'#skF_19'(O_95))
| ~ incident_o('#skF_1'('#skF_19'(O_95),C1_204),O_95) ),
inference(resolution,[status(thm)],[c_146,c_328]) ).
tff(c_539,plain,
! [O_248] : part_of(underlying_curve(O_248),'#skF_19'(O_248)),
inference(resolution,[status(thm)],[c_519,c_347]) ).
tff(c_70,plain,
! [C1_37,C_36] :
( open(C1_37)
| ( C_36 = C1_37 )
| ~ part_of(C1_37,C_36) ),
inference(cnfTransformation,[status(thm)],[f_123]) ).
tff(c_551,plain,
! [O_248] :
( open(underlying_curve(O_248))
| ( underlying_curve(O_248) = '#skF_19'(O_248) ) ),
inference(resolution,[status(thm)],[c_539,c_70]) ).
tff(c_66,plain,
! [C_32] :
( end_point('#skF_8'(C_32),C_32)
| ~ open(C_32) ),
inference(cnfTransformation,[status(thm)],[f_116]) ).
tff(c_308,plain,
! [O_195] :
( incident_o('#skF_8'(underlying_curve(O_195)),O_195)
| ~ open(underlying_curve(O_195)) ),
inference(resolution,[status(thm)],[c_66,c_299]) ).
tff(c_1215,plain,
! [P_355] :
( ( P_355 = '#skF_8'(underlying_curve('#skF_31')) )
| ~ finish_point(P_355,'#skF_31')
| ~ open(underlying_curve('#skF_31')) ),
inference(resolution,[status(thm)],[c_308,c_1157]) ).
tff(c_1254,plain,
~ open(underlying_curve('#skF_31')),
inference(splitLeft,[status(thm)],[c_1215]) ).
tff(c_1261,plain,
underlying_curve('#skF_31') = '#skF_19'('#skF_31'),
inference(resolution,[status(thm)],[c_551,c_1254]) ).
tff(c_209,plain,
! [C_155] :
( closed(C_155)
| end_point('#skF_7'(C_155),C_155) ),
inference(cnfTransformation,[status(thm)],[f_111]) ).
tff(c_68,plain,
! [C_32,P_35] :
( open(C_32)
| ~ end_point(P_35,C_32) ),
inference(cnfTransformation,[status(thm)],[f_116]) ).
tff(c_217,plain,
! [C_155] :
( open(C_155)
| closed(C_155) ),
inference(resolution,[status(thm)],[c_209,c_68]) ).
tff(c_1262,plain,
closed(underlying_curve('#skF_31')),
inference(resolution,[status(thm)],[c_217,c_1254]) ).
tff(c_1301,plain,
closed('#skF_19'('#skF_31')),
inference(demodulation,[status(thm),theory(equality)],[c_1261,c_1262]) ).
tff(c_1305,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_249,c_1301]) ).
tff(c_1307,plain,
open(underlying_curve('#skF_31')),
inference(splitRight,[status(thm)],[c_1215]) ).
tff(c_239,plain,
! [C_165] :
( ~ closed(C_165)
| ~ open(C_165) ),
inference(resolution,[status(thm)],[c_232,c_62]) ).
tff(c_1311,plain,
~ closed(underlying_curve('#skF_31')),
inference(resolution,[status(thm)],[c_1307,c_239]) ).
tff(c_1318,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1312,c_1311]) ).
tff(c_1320,plain,
~ closed(underlying_curve('#skF_31')),
inference(splitRight,[status(thm)],[c_1214]) ).
tff(c_166,plain,
! [O_115] : start_point('#skF_23'(O_115),O_115),
inference(cnfTransformation,[status(thm)],[f_329]) ).
tff(c_1406,plain,
! [O_401,P_402,Q_403] :
( ordered_by(O_401,P_402,Q_403)
| ~ incident_o(Q_403,O_401)
| ( Q_403 = P_402 )
| ~ start_point(P_402,O_401) ),
inference(cnfTransformation,[status(thm)],[f_290]) ).
tff(c_1420,plain,
! [Q_404,P_405] :
( ~ incident_o(Q_404,'#skF_31')
| ( Q_404 = P_405 )
| ~ start_point(P_405,'#skF_31') ),
inference(resolution,[status(thm)],[c_1406,c_194]) ).
tff(c_1453,plain,
! [P_405] :
( ( P_405 = '#skF_7'(underlying_curve('#skF_31')) )
| ~ start_point(P_405,'#skF_31')
| closed(underlying_curve('#skF_31')) ),
inference(resolution,[status(thm)],[c_309,c_1420]) ).
tff(c_1509,plain,
! [P_407] :
( ( P_407 = '#skF_7'(underlying_curve('#skF_31')) )
| ~ start_point(P_407,'#skF_31') ),
inference(negUnitSimplification,[status(thm)],[c_1320,c_1453]) ).
tff(c_1517,plain,
'#skF_7'(underlying_curve('#skF_31')) = '#skF_23'('#skF_31'),
inference(resolution,[status(thm)],[c_166,c_1509]) ).
tff(c_1538,plain,
( closed(underlying_curve('#skF_31'))
| end_point('#skF_23'('#skF_31'),underlying_curve('#skF_31')) ),
inference(superposition,[status(thm),theory(equality)],[c_1517,c_64]) ).
tff(c_1545,plain,
end_point('#skF_23'('#skF_31'),underlying_curve('#skF_31')),
inference(negUnitSimplification,[status(thm)],[c_1320,c_1538]) ).
tff(c_74,plain,
! [C_44] : inner_point('#skF_9'(C_44),C_44),
inference(cnfTransformation,[status(thm)],[f_151]) ).
tff(c_219,plain,
! [P_157,C_158] :
( incident_c(P_157,C_158)
| ~ inner_point(P_157,C_158) ),
inference(cnfTransformation,[status(thm)],[f_90]) ).
tff(c_223,plain,
! [C_44] : incident_c('#skF_9'(C_44),C_44),
inference(resolution,[status(thm)],[c_74,c_219]) ).
tff(c_294,plain,
! [O_184] : incident_o('#skF_9'(underlying_curve(O_184)),O_184),
inference(resolution,[status(thm)],[c_223,c_280]) ).
tff(c_1602,plain,
! [P_409] :
( ( P_409 = '#skF_9'(underlying_curve('#skF_31')) )
| ~ start_point(P_409,'#skF_31') ),
inference(resolution,[status(thm)],[c_294,c_1420]) ).
tff(c_1610,plain,
'#skF_9'(underlying_curve('#skF_31')) = '#skF_23'('#skF_31'),
inference(resolution,[status(thm)],[c_166,c_1602]) ).
tff(c_225,plain,
! [P_160,C_161] :
( ~ end_point(P_160,C_161)
| ~ inner_point(P_160,C_161) ),
inference(cnfTransformation,[status(thm)],[f_90]) ).
tff(c_229,plain,
! [C_44] : ~ end_point('#skF_9'(C_44),C_44),
inference(resolution,[status(thm)],[c_74,c_225]) ).
tff(c_1662,plain,
~ end_point('#skF_23'('#skF_31'),underlying_curve('#skF_31')),
inference(superposition,[status(thm),theory(equality)],[c_1610,c_229]) ).
tff(c_1674,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1545,c_1662]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : GEO126+1 : TPTP v9.0.0. Released v2.4.0.
% 0.03/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.12/0.34 % Computer : n019.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Mon Apr 7 19:40:47 EDT 2025
% 0.12/0.34 % CPUTime :
% 6.04/2.38 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 6.04/2.39
% 6.04/2.39 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------