%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : GEO210+3 : TPTP v9.0.0. Released v4.0.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 : n009.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:14:16 PM UTC 2025
% Result : Theorem 7.67s 3.03s
% Output : CNFRefutation 7.67s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 10
% Syntax : Number of formulae : 37 ( 15 unt; 0 typ; 0 def)
% Number of atoms : 73 ( 0 equ)
% Maximal formula atoms : 6 ( 1 avg)
% Number of connectives : 65 ( 29 ~; 23 |; 6 &)
% ( 2 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 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 : 13 ( 12 usr; 1 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 3 con; 0-2 aty)
% Number of variables : 54 ( 54 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ unorthogonal_lines > parallel_lines > orthogonal_lines > incident_point_and_line > equal_points > equal_lines > distinct_points > distinct_lines > convergent_lines > apart_point_and_line > point > line > parallel_through_point > orthogonal_through_point > line_connecting > intersection_point > #nlpp > #skF_2 > #skF_3 > #skF_1
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(line_connecting,type,
line_connecting: ( $i * $i ) > $i ).
tff(equal_lines,type,
equal_lines: ( $i * $i ) > $o ).
tff(equal_points,type,
equal_points: ( $i * $i ) > $o ).
tff(incident_point_and_line,type,
incident_point_and_line: ( $i * $i ) > $o ).
tff(distinct_points,type,
distinct_points: ( $i * $i ) > $o ).
tff(intersection_point,type,
intersection_point: ( $i * $i ) > $i ).
tff(parallel_through_point,type,
parallel_through_point: ( $i * $i ) > $i ).
tff(apart_point_and_line,type,
apart_point_and_line: ( $i * $i ) > $o ).
tff(convergent_lines,type,
convergent_lines: ( $i * $i ) > $o ).
tff(orthogonal_through_point,type,
orthogonal_through_point: ( $i * $i ) > $i ).
tff(point,type,
point: $i > $o ).
tff(line,type,
line: $i > $o ).
tff(parallel_lines,type,
parallel_lines: ( $i * $i ) > $o ).
tff('#skF_2',type,
'#skF_2': $i ).
tff('#skF_3',type,
'#skF_3': $i ).
tff('#skF_1',type,
'#skF_1': $i ).
tff(unorthogonal_lines,type,
unorthogonal_lines: ( $i * $i ) > $o ).
tff(distinct_lines,type,
distinct_lines: ( $i * $i ) > $o ).
tff(orthogonal_lines,type,
orthogonal_lines: ( $i * $i ) > $o ).
tff(f_61,axiom,
! [X] : ~ convergent_lines(X,X),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+0.ax',apart3) ).
tff(f_411,axiom,
! [X,Y] :
( equal_lines(X,Y)
<=> ~ distinct_lines(X,Y) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+6.ax',ax2) ).
tff(f_435,negated_conjecture,
~ ! [A,L,M] :
( ( incident_point_and_line(A,L)
& orthogonal_lines(L,M) )
=> equal_lines(L,orthogonal_through_point(M,A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',con) ).
tff(f_160,axiom,
! [X,Y] :
( distinct_lines(X,Y)
=> convergent_lines(X,Y) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+1.ax',p1) ).
tff(f_79,axiom,
! [X,Y,Z] :
( convergent_lines(X,Y)
=> ( convergent_lines(X,Z)
| convergent_lines(Y,Z) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+0.ax',ax6) ).
tff(f_292,axiom,
! [L,M] :
~ ( ~ convergent_lines(L,M)
& ~ unorthogonal_lines(L,M) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+4.ax',coipo1) ).
tff(f_426,axiom,
! [X,Y] :
( orthogonal_lines(X,Y)
<=> ~ unorthogonal_lines(X,Y) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+6.ax',a5) ).
tff(f_321,axiom,
! [L,M,N] :
( ( ~ unorthogonal_lines(L,M)
& ~ unorthogonal_lines(L,N) )
=> ~ convergent_lines(M,N) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+4.ax',couo1) ).
tff(f_242,axiom,
! [L,M,N] :
( ( convergent_lines(L,M)
& unorthogonal_lines(L,M) )
=> ( ( convergent_lines(L,N)
& unorthogonal_lines(L,N) )
| ( convergent_lines(M,N)
& unorthogonal_lines(M,N) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+3.ax',oac1) ).
tff(f_246,axiom,
! [A,L] : ~ unorthogonal_lines(orthogonal_through_point(L,A),L),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+3.ax',ooc1) ).
tff(c_6,plain,
! [X_3] : ~ convergent_lines(X_3,X_3),
inference(cnfTransformation,[status(thm)],[f_61]) ).
tff(c_127,plain,
! [X_107,Y_108] :
( equal_lines(X_107,Y_108)
| distinct_lines(X_107,Y_108) ),
inference(cnfTransformation,[status(thm)],[f_411]) ).
tff(c_94,plain,
~ equal_lines('#skF_2',orthogonal_through_point('#skF_3','#skF_1')),
inference(cnfTransformation,[status(thm)],[f_435]) ).
tff(c_131,plain,
distinct_lines('#skF_2',orthogonal_through_point('#skF_3','#skF_1')),
inference(resolution,[status(thm)],[c_127,c_94]) ).
tff(c_30,plain,
! [X_34,Y_35] :
( convergent_lines(X_34,Y_35)
| ~ distinct_lines(X_34,Y_35) ),
inference(cnfTransformation,[status(thm)],[f_160]) ).
tff(c_135,plain,
convergent_lines('#skF_2',orthogonal_through_point('#skF_3','#skF_1')),
inference(resolution,[status(thm)],[c_131,c_30]) ).
tff(c_402,plain,
! [Y_188,Z_189,X_190] :
( convergent_lines(Y_188,Z_189)
| convergent_lines(X_190,Z_189)
| ~ convergent_lines(X_190,Y_188) ),
inference(cnfTransformation,[status(thm)],[f_79]) ).
tff(c_425,plain,
! [Z_189] :
( convergent_lines(orthogonal_through_point('#skF_3','#skF_1'),Z_189)
| convergent_lines('#skF_2',Z_189) ),
inference(resolution,[status(thm)],[c_135,c_402]) ).
tff(c_96,plain,
orthogonal_lines('#skF_2','#skF_3'),
inference(cnfTransformation,[status(thm)],[f_435]) ).
tff(c_54,plain,
! [L_56,M_57] :
( unorthogonal_lines(L_56,M_57)
| convergent_lines(L_56,M_57) ),
inference(cnfTransformation,[status(thm)],[f_292]) ).
tff(c_137,plain,
! [X_111,Y_112] :
( ~ unorthogonal_lines(X_111,Y_112)
| ~ orthogonal_lines(X_111,Y_112) ),
inference(cnfTransformation,[status(thm)],[f_426]) ).
tff(c_166,plain,
! [L_121,M_122] :
( ~ orthogonal_lines(L_121,M_122)
| convergent_lines(L_121,M_122) ),
inference(resolution,[status(thm)],[c_54,c_137]) ).
tff(c_175,plain,
convergent_lines('#skF_2','#skF_3'),
inference(resolution,[status(thm)],[c_96,c_166]) ).
tff(c_182,plain,
! [M_135,N_136,L_137] :
( ~ convergent_lines(M_135,N_136)
| unorthogonal_lines(L_137,N_136)
| unorthogonal_lines(L_137,M_135) ),
inference(cnfTransformation,[status(thm)],[f_321]) ).
tff(c_189,plain,
! [L_137] :
( unorthogonal_lines(L_137,'#skF_3')
| unorthogonal_lines(L_137,'#skF_2') ),
inference(resolution,[status(thm)],[c_175,c_182]) ).
tff(c_1915,plain,
! [L_310,N_311,M_312] :
( unorthogonal_lines(L_310,N_311)
| unorthogonal_lines(M_312,N_311)
| ~ unorthogonal_lines(L_310,M_312)
| ~ convergent_lines(L_310,M_312) ),
inference(cnfTransformation,[status(thm)],[f_242]) ).
tff(c_1985,plain,
! [L_137,N_311] :
( unorthogonal_lines(L_137,N_311)
| unorthogonal_lines('#skF_2',N_311)
| ~ convergent_lines(L_137,'#skF_2')
| unorthogonal_lines(L_137,'#skF_3') ),
inference(resolution,[status(thm)],[c_189,c_1915]) ).
tff(c_2904,plain,
! [L_137] :
( unorthogonal_lines('#skF_2','#skF_3')
| ~ convergent_lines(L_137,'#skF_2')
| unorthogonal_lines(L_137,'#skF_3') ),
inference(factorization,[status(thm),theory(equality)],[c_1985]) ).
tff(c_2995,plain,
unorthogonal_lines('#skF_2','#skF_3'),
inference(splitLeft,[status(thm)],[c_2904]) ).
tff(c_90,plain,
! [X_80,Y_81] :
( ~ unorthogonal_lines(X_80,Y_81)
| ~ orthogonal_lines(X_80,Y_81) ),
inference(cnfTransformation,[status(thm)],[f_426]) ).
tff(c_3012,plain,
~ orthogonal_lines('#skF_2','#skF_3'),
inference(resolution,[status(thm)],[c_2995,c_90]) ).
tff(c_3037,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_96,c_3012]) ).
tff(c_3234,plain,
! [L_359] :
( ~ convergent_lines(L_359,'#skF_2')
| unorthogonal_lines(L_359,'#skF_3') ),
inference(splitRight,[status(thm)],[c_2904]) ).
tff(c_48,plain,
! [L_49,A_48] : ~ unorthogonal_lines(orthogonal_through_point(L_49,A_48),L_49),
inference(cnfTransformation,[status(thm)],[f_246]) ).
tff(c_3270,plain,
! [A_360] : ~ convergent_lines(orthogonal_through_point('#skF_3',A_360),'#skF_2'),
inference(resolution,[status(thm)],[c_3234,c_48]) ).
tff(c_3300,plain,
convergent_lines('#skF_2','#skF_2'),
inference(resolution,[status(thm)],[c_425,c_3270]) ).
tff(c_3329,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_6,c_3300]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.09 % Problem : GEO210+3 : TPTP v9.0.0. Released v4.0.0.
% 0.00/0.09 % 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.09/0.29 % Computer : n009.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:58:26 EDT 2025
% 0.14/0.29 % CPUTime :
% 7.67/3.03 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.67/3.03
% 7.67/3.03 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------