%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : GEO111-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/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 : n028.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:48 PM UTC 2025
% Result : Unsatisfiable 166.17s 136.71s
% Output : CNFRefutation 166.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 11
% Syntax : Number of formulae : 58 ( 23 unt; 0 typ; 0 def)
% Number of atoms : 114 ( 21 equ)
% Maximal formula atoms : 6 ( 1 avg)
% Number of connectives : 112 ( 56 ~; 56 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 5 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 : 10 ( 8 usr; 1 prp; 0-4 aty)
% Number of functors : 19 ( 19 usr; 4 con; 0-4 aty)
% Number of variables : 112 ( 112 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ between_c > meet > part_of > inner_point > incident_c > end_point > open > closed > ax1_sk1 > ax0_sk5 > ax0_sk2 > sum > ax0_sk9 > ax0_sk4 > ax0_sk3 > ax0_sk13 > ax0_sk12 > ax0_sk11 > ax0_sk10 > ax0_sk1 > #nlpp > ax0_sk8 > ax0_sk7 > ax0_sk6 > sk18 > sk17 > sk16 > sk15
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(sk17,type,
sk17: $i ).
tff(between_c,type,
between_c: ( $i * $i * $i * $i ) > $o ).
tff(closed,type,
closed: $i > $o ).
tff(ax0_sk8,type,
ax0_sk8: $i > $i ).
tff(ax0_sk9,type,
ax0_sk9: ( $i * $i ) > $i ).
tff(inner_point,type,
inner_point: ( $i * $i ) > $o ).
tff(sk16,type,
sk16: $i ).
tff(end_point,type,
end_point: ( $i * $i ) > $o ).
tff(ax0_sk12,type,
ax0_sk12: ( $i * $i ) > $i ).
tff(ax0_sk13,type,
ax0_sk13: ( $i * $i ) > $i ).
tff(part_of,type,
part_of: ( $i * $i ) > $o ).
tff(meet,type,
meet: ( $i * $i * $i ) > $o ).
tff(ax0_sk4,type,
ax0_sk4: ( $i * $i ) > $i ).
tff(incident_c,type,
incident_c: ( $i * $i ) > $o ).
tff(sum,type,
sum: ( $i * $i ) > $i ).
tff(sk18,type,
sk18: $i ).
tff(ax0_sk11,type,
ax0_sk11: ( $i * $i ) > $i ).
tff(ax0_sk1,type,
ax0_sk1: ( $i * $i ) > $i ).
tff(ax0_sk2,type,
ax0_sk2: ( $i * $i * $i ) > $i ).
tff(sk15,type,
sk15: $i ).
tff(ax0_sk7,type,
ax0_sk7: $i > $i ).
tff(ax0_sk10,type,
ax0_sk10: ( $i * $i ) > $i ).
tff(ax1_sk1,type,
ax1_sk1: ( $i * $i * $i * $i ) > $i ).
tff(ax0_sk3,type,
ax0_sk3: ( $i * $i ) > $i ).
tff(ax0_sk5,type,
ax0_sk5: ( $i * $i * $i ) > $i ).
tff(ax0_sk6,type,
ax0_sk6: $i > $i ).
tff(open,type,
open: $i > $o ).
tff(f_476,axiom,
! [A,B,C,D] :
( ~ between_c(A,B,C,D)
| end_point(D,ax1_sk1(D,C,B,A)) ),
file(unknown,unknown) ).
tff(f_481,axiom,
! [A,B,C,D] :
( ~ between_c(A,B,C,D)
| inner_point(C,ax1_sk1(D,C,B,A)) ),
file(unknown,unknown) ).
tff(f_216,axiom,
! [A,B] :
( ~ inner_point(A,B)
| ~ end_point(A,B) ),
file(unknown,unknown) ).
tff(f_471,axiom,
! [A,B,C,D] :
( ~ between_c(A,B,C,D)
| end_point(B,ax1_sk1(D,C,B,A)) ),
file(unknown,unknown) ).
tff(f_461,axiom,
! [A,B,C,D] :
( ~ between_c(A,B,C,D)
| ( B != D ) ),
file(unknown,unknown) ).
tff(f_514,axiom,
( ~ incident_c(sk16,sk15)
| ~ incident_c(sk17,sk15)
| ~ incident_c(sk18,sk15)
| ( sk16 = sk17 )
| ( sk17 = sk18 )
| ( sk16 = sk18 ) ),
file(unknown,unknown) ).
tff(f_500,axiom,
between_c(sk15,sk16,sk17,sk18),
file(unknown,unknown) ).
tff(f_466,axiom,
! [A,B,C,D] :
( ~ between_c(A,B,C,D)
| part_of(ax1_sk1(D,C,B,A),A) ),
file(unknown,unknown) ).
tff(f_142,axiom,
! [A,B] :
( ~ end_point(A,B)
| incident_c(A,B) ),
file(unknown,unknown) ).
tff(f_53,axiom,
! [A,B,C] :
( ~ part_of(A,B)
| ~ incident_c(C,A)
| incident_c(C,B) ),
file(unknown,unknown) ).
tff(f_210,axiom,
! [A,B] :
( ~ inner_point(A,B)
| incident_c(A,B) ),
file(unknown,unknown) ).
tff(c_104,plain,
! [D_142,C_141,B_140,A_139] :
( end_point(D_142,ax1_sk1(D_142,C_141,B_140,A_139))
| ~ between_c(A_139,B_140,C_141,D_142) ),
inference(cnfTransformation,[status(thm)],[f_476]) ).
tff(c_638,plain,
! [C_292,D_293,B_294,A_295] :
( inner_point(C_292,ax1_sk1(D_293,C_292,B_294,A_295))
| ~ between_c(A_295,B_294,C_292,D_293) ),
inference(cnfTransformation,[status(thm)],[f_481]) ).
tff(c_44,plain,
! [A_58,B_59] :
( ~ end_point(A_58,B_59)
| ~ inner_point(A_58,B_59) ),
inference(cnfTransformation,[status(thm)],[f_216]) ).
tff(c_2161791,plain,
! [C_763687,D_763688,B_763689,A_763690] :
( ~ end_point(C_763687,ax1_sk1(D_763688,C_763687,B_763689,A_763690))
| ~ between_c(A_763690,B_763689,C_763687,D_763688) ),
inference(resolution,[status(thm)],[c_638,c_44]) ).
tff(c_2161801,plain,
! [A_139,B_140,C_141] : ~ between_c(A_139,B_140,C_141,C_141),
inference(resolution,[status(thm)],[c_104,c_2161791]) ).
tff(c_102,plain,
! [B_136,D_138,C_137,A_135] :
( end_point(B_136,ax1_sk1(D_138,C_137,B_136,A_135))
| ~ between_c(A_135,B_136,C_137,D_138) ),
inference(cnfTransformation,[status(thm)],[f_471]) ).
tff(c_2160727,plain,
! [C_763525,D_763526,B_763527,A_763528] :
( ~ end_point(C_763525,ax1_sk1(D_763526,C_763525,B_763527,A_763528))
| ~ between_c(A_763528,B_763527,C_763525,D_763526) ),
inference(resolution,[status(thm)],[c_638,c_44]) ).
tff(c_2160742,plain,
! [A_135,C_137,D_138] : ~ between_c(A_135,C_137,C_137,D_138),
inference(resolution,[status(thm)],[c_102,c_2160727]) ).
tff(c_98,plain,
! [A_127,D_130,C_129] : ~ between_c(A_127,D_130,C_129,D_130),
inference(cnfTransformation,[status(thm)],[f_461]) ).
tff(c_112,plain,
( ( sk18 = sk16 )
| ( sk18 = sk17 )
| ( sk17 = sk16 )
| ~ incident_c(sk18,sk15)
| ~ incident_c(sk17,sk15)
| ~ incident_c(sk16,sk15) ),
inference(cnfTransformation,[status(thm)],[f_514]) ).
tff(c_1272,plain,
~ incident_c(sk16,sk15),
inference(splitLeft,[status(thm)],[c_112]) ).
tff(c_110,plain,
between_c(sk15,sk16,sk17,sk18),
inference(cnfTransformation,[status(thm)],[f_500]) ).
tff(c_611,plain,
! [D_285,C_286,B_287,A_288] :
( part_of(ax1_sk1(D_285,C_286,B_287,A_288),A_288)
| ~ between_c(A_288,B_287,C_286,D_285) ),
inference(cnfTransformation,[status(thm)],[f_466]) ).
tff(c_26,plain,
! [A_38,B_39] :
( incident_c(A_38,B_39)
| ~ end_point(A_38,B_39) ),
inference(cnfTransformation,[status(thm)],[f_142]) ).
tff(c_221,plain,
! [C_201,B_202,A_203] :
( incident_c(C_201,B_202)
| ~ incident_c(C_201,A_203)
| ~ part_of(A_203,B_202) ),
inference(cnfTransformation,[status(thm)],[f_53]) ).
tff(c_235,plain,
! [A_38,B_202,B_39] :
( incident_c(A_38,B_202)
| ~ part_of(B_39,B_202)
| ~ end_point(A_38,B_39) ),
inference(resolution,[status(thm)],[c_26,c_221]) ).
tff(c_641304,plain,
! [D_235422,C_235423,B_235421,A_235420,A_235424] :
( incident_c(A_235420,A_235424)
| ~ end_point(A_235420,ax1_sk1(D_235422,C_235423,B_235421,A_235424))
| ~ between_c(A_235424,B_235421,C_235423,D_235422) ),
inference(resolution,[status(thm)],[c_611,c_235]) ).
tff(c_641372,plain,
! [B_235673,A_235674,C_235675,D_235676] :
( incident_c(B_235673,A_235674)
| ~ between_c(A_235674,B_235673,C_235675,D_235676) ),
inference(resolution,[status(thm)],[c_102,c_641304]) ).
tff(c_641378,plain,
incident_c(sk16,sk15),
inference(resolution,[status(thm)],[c_110,c_641372]) ).
tff(c_641383,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1272,c_641378]) ).
tff(c_641384,plain,
( ~ incident_c(sk17,sk15)
| ~ incident_c(sk18,sk15)
| ( sk17 = sk16 )
| ( sk18 = sk17 )
| ( sk18 = sk16 ) ),
inference(splitRight,[status(thm)],[c_112]) ).
tff(c_641578,plain,
~ incident_c(sk18,sk15),
inference(splitLeft,[status(thm)],[c_641384]) ).
tff(c_1356336,plain,
! [A_488287,D_488285,A_488283,B_488284,C_488286] :
( incident_c(A_488283,A_488287)
| ~ end_point(A_488283,ax1_sk1(D_488285,C_488286,B_488284,A_488287))
| ~ between_c(A_488287,B_488284,C_488286,D_488285) ),
inference(resolution,[status(thm)],[c_611,c_235]) ).
tff(c_1356394,plain,
! [D_488788,A_488789,B_488790,C_488791] :
( incident_c(D_488788,A_488789)
| ~ between_c(A_488789,B_488790,C_488791,D_488788) ),
inference(resolution,[status(thm)],[c_104,c_1356336]) ).
tff(c_1356400,plain,
incident_c(sk18,sk15),
inference(resolution,[status(thm)],[c_110,c_1356394]) ).
tff(c_1356405,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_641578,c_1356400]) ).
tff(c_1356406,plain,
( ~ incident_c(sk17,sk15)
| ( sk18 = sk16 )
| ( sk18 = sk17 )
| ( sk17 = sk16 ) ),
inference(splitRight,[status(thm)],[c_641384]) ).
tff(c_1356564,plain,
~ incident_c(sk17,sk15),
inference(splitLeft,[status(thm)],[c_1356406]) ).
tff(c_100,plain,
! [D_134,C_133,B_132,A_131] :
( part_of(ax1_sk1(D_134,C_133,B_132,A_131),A_131)
| ~ between_c(A_131,B_132,C_133,D_134) ),
inference(cnfTransformation,[status(thm)],[f_466]) ).
tff(c_42,plain,
! [A_56,B_57] :
( incident_c(A_56,B_57)
| ~ inner_point(A_56,B_57) ),
inference(cnfTransformation,[status(thm)],[f_210]) ).
tff(c_1372402,plain,
! [C_498402,D_498403,B_498404,A_498405] :
( incident_c(C_498402,ax1_sk1(D_498403,C_498402,B_498404,A_498405))
| ~ between_c(A_498405,B_498404,C_498402,D_498403) ),
inference(resolution,[status(thm)],[c_638,c_42]) ).
tff(c_2,plain,
! [C_3,B_2,A_1] :
( incident_c(C_3,B_2)
| ~ incident_c(C_3,A_1)
| ~ part_of(A_1,B_2) ),
inference(cnfTransformation,[status(thm)],[f_53]) ).
tff(c_2143307,plain,
! [B_753416,C_753414,B_753415,D_753413,A_753412] :
( incident_c(C_753414,B_753415)
| ~ part_of(ax1_sk1(D_753413,C_753414,B_753416,A_753412),B_753415)
| ~ between_c(A_753412,B_753416,C_753414,D_753413) ),
inference(resolution,[status(thm)],[c_1372402,c_2]) ).
tff(c_2143436,plain,
! [C_753665,A_753666,B_753667,D_753668] :
( incident_c(C_753665,A_753666)
| ~ between_c(A_753666,B_753667,C_753665,D_753668) ),
inference(resolution,[status(thm)],[c_100,c_2143307]) ).
tff(c_2143442,plain,
incident_c(sk17,sk15),
inference(resolution,[status(thm)],[c_110,c_2143436]) ).
tff(c_2143447,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1356564,c_2143442]) ).
tff(c_2143448,plain,
( ( sk17 = sk16 )
| ( sk18 = sk17 )
| ( sk18 = sk16 ) ),
inference(splitRight,[status(thm)],[c_1356406]) ).
tff(c_2143507,plain,
sk18 = sk16,
inference(splitLeft,[status(thm)],[c_2143448]) ).
tff(c_2143513,plain,
between_c(sk15,sk16,sk17,sk16),
inference(demodulation,[status(thm),theory(equality)],[c_2143507,c_110]) ).
tff(c_2143517,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_98,c_2143513]) ).
tff(c_2143518,plain,
( ( sk18 = sk17 )
| ( sk17 = sk16 ) ),
inference(splitRight,[status(thm)],[c_2143448]) ).
tff(c_2143520,plain,
sk17 = sk16,
inference(splitLeft,[status(thm)],[c_2143518]) ).
tff(c_2143523,plain,
between_c(sk15,sk16,sk16,sk18),
inference(demodulation,[status(thm),theory(equality)],[c_2143520,c_110]) ).
tff(c_2160745,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_2160742,c_2143523]) ).
tff(c_2160746,plain,
sk18 = sk17,
inference(splitRight,[status(thm)],[c_2143518]) ).
tff(c_2160754,plain,
between_c(sk15,sk16,sk17,sk17),
inference(demodulation,[status(thm),theory(equality)],[c_2160746,c_110]) ).
tff(c_2161804,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_2161801,c_2160754]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.09 % Problem : GEO111-1 : TPTP v9.0.0. Released v2.4.0.
% 0.08/0.09 % 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.09/0.29 % Computer : n028.cluster.edu
% 0.09/0.29 % Model : x86_64 x86_64
% 0.09/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.29 % Memory : 8042.1875MB
% 0.09/0.29 % OS : Linux 3.10.0-693.el7.x86_64
% 0.09/0.29 % CPULimit : 300
% 0.09/0.29 % WCLimit : 300
% 0.09/0.29 % DateTime : Mon Apr 7 19:36:34 EDT 2025
% 0.09/0.29 % CPUTime :
% 166.17/136.71 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 166.17/136.72
% 166.17/136.72 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------