%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GEO053-3 : TPTP v9.3.1. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n009.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 07:16:55 AM UTC 2026
% Result : Unsatisfiable 3.61s 0.96s
% Output : CNFRefutation 3.61s
% Verified :
% SZS Type : Refutation
% Derivation depth : 6
% Number of leaves : 9
% Syntax : Number of formulae : 31 ( 19 unt; 0 def)
% Number of atoms : 51 ( 15 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 45 ( 25 ~; 20 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-4 aty)
% Number of functors : 7 ( 7 usr; 5 con; 0-4 aty)
% Number of variables : 58 ( 2 sgn 20 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(insertion,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] : insertion(VAR_0,VAR_1,VAR_2,VAR_3) = extension(extension(VAR_1,VAR_0,lower_dimension_point_1,lower_dimension_point_2),VAR_0,VAR_2,VAR_3),
file('theBenchmark.p',insertion) ).
cnf(c_20,plain,
insertion(A,B,C,D) = extension(extension(B,A,lower_dimension_point_1,lower_dimension_point_2),A,C,D),
inference(clausify,[status(thm)],[insertion]) ).
fof(t3,axiom,
! [VAR_0,VAR_1] : between(VAR_0,VAR_1,VAR_1),
file('theBenchmark.p',t3) ).
cnf(c_53,plain,
between(A,B,B),
inference(clausify,[status(thm)],[t3]) ).
fof(t2,axiom,
! [VAR_0,VAR_1] : between(VAR_0,VAR_0,VAR_1),
file('theBenchmark.p',t2) ).
cnf(c_56,plain,
between(A,A,B),
inference(clausify,[status(thm)],[t2]) ).
fof(d15,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( VAR_1 = VAR_3
| ~ equidistant(VAR_2,VAR_1,VAR_2,VAR_3)
| ~ equidistant(VAR_0,VAR_1,VAR_0,VAR_3)
| ~ between(VAR_0,VAR_1,VAR_2) ),
file('theBenchmark.p',d15) ).
cnf(c_78,plain,
( B = D
| ~ equidistant(C,B,C,D)
| ~ equidistant(A,B,A,D)
| ~ between(A,B,C) ),
inference(clausify,[status(thm)],[d15]) ).
fof(i2_3,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( equidistant(VAR_1,VAR_2,insertion(VAR_3,VAR_4,VAR_0,VAR_1),VAR_4)
| ~ equidistant(VAR_0,VAR_2,VAR_3,VAR_4)
| ~ between(VAR_0,VAR_1,VAR_2) ),
file('theBenchmark.p',i2_3) ).
cnf(c_83,plain,
( equidistant(B,C,insertion(D,E,A,B),E)
| ~ equidistant(A,C,D,E)
| ~ between(A,B,C) ),
inference(clausify,[status(thm)],[i2_3]) ).
cnf(c_84,plain,
( equidistant(B,C,extension(extension(E,D,lower_dimension_point_1,lower_dimension_point_2),D,A,B),E)
| ~ equidistant(A,C,D,E)
| ~ between(A,B,C) ),
inference(paramod,[status(thm)],[c_20,c_83]) ).
fof(i3,axiom,
! [VAR_0,VAR_1,VAR_2] :
( VAR_1 = insertion(VAR_0,VAR_2,VAR_0,VAR_1)
| ~ between(VAR_0,VAR_1,VAR_2) ),
file('theBenchmark.p',i3) ).
cnf(c_85,plain,
( B = insertion(A,C,A,B)
| ~ between(A,B,C) ),
inference(clausify,[status(thm)],[i3]) ).
cnf(c_788,plain,
( B = extension(extension(C,A,lower_dimension_point_1,lower_dimension_point_2),A,A,B)
| ~ between(A,B,C) ),
inference(paramod,[status(thm)],[c_20,c_85]) ).
cnf(c_86,plain,
( extension(extension(C,A,lower_dimension_point_1,lower_dimension_point_2),A,A,B) = B
| ~ between(A,B,C) ),
inference(copy,[status(thm)],[c_788]) ).
fof(v_between_u_and_w,axiom,
between(u,v,w),
file('theBenchmark.p',v_between_u_and_w) ).
cnf(c_96,plain,
between(u,v,w),
inference(clausify,[status(thm)],[v_between_u_and_w]) ).
fof(u_to_v_equals_u_to_w,axiom,
equidistant(u,v,u,w),
file('theBenchmark.p',u_to_v_equals_u_to_w) ).
cnf(c_97,plain,
equidistant(u,v,u,w),
inference(clausify,[status(thm)],[u_to_v_equals_u_to_w]) ).
fof(prove_v_equals_w,axiom,
v != w,
file('theBenchmark.p',prove_v_equals_w) ).
cnf(c_98,plain,
v != w,
inference(clausify,[status(thm)],[prove_v_equals_w]) ).
cnf(c_99,plain,
w != v,
inference(copy,[status(thm)],[c_98]) ).
cnf(c_597,plain,
extension(extension(w,u,lower_dimension_point_1,lower_dimension_point_2),u,u,v) = v,
inference(resolve,[status(thm)],[c_96,c_86]) ).
cnf(c_789,plain,
( equidistant(B,B,extension(extension(D,C,lower_dimension_point_1,lower_dimension_point_2),C,A,B),D)
| ~ equidistant(A,B,C,D) ),
inference(resolve,[status(thm)],[c_84,c_53]) ).
cnf(c_790,plain,
equidistant(v,v,extension(extension(w,u,lower_dimension_point_1,lower_dimension_point_2),u,u,v),w),
inference(resolve,[status(thm)],[c_789,c_97]) ).
cnf(c_745,plain,
equidistant(v,v,v,w),
inference(paramod,[status(thm)],[c_597,c_790]) ).
cnf(c_791,plain,
( A = B
| ~ equidistant(C,A,C,B)
| ~ equidistant(A,A,A,B) ),
inference(resolve,[status(thm)],[c_78,c_56]) ).
cnf(c_792,plain,
( v = w
| ~ equidistant(v,v,v,w) ),
inference(resolve,[status(thm)],[c_791,c_97]) ).
cnf(c_793,plain,
v != w,
inference(copy,[status(thm)],[c_99]) ).
cnf(c_794,plain,
~ equidistant(v,v,v,w),
inference(resolve,[status(thm)],[c_792,c_793]) ).
cnf(c_787,plain,
$false,
inference(resolve,[status(thm)],[c_745,c_794]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO053-3 : TPTP v9.3.1. Bugfixed v1.2.1.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n009.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Fri Sep 25 12:36:58 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.37 % Process 1619335 was started by sandbox on n009,
% 0.10/0.37 % Fri Sep 25 12:36:58 2026
% 0.10/0.37 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.10/0.38
% 0.10/0.38 % From the command line: assign(max_seconds, 300).
% 3.61/0.96
% 3.61/0.96 % SZS status Unsatisfiable for theBenchmark
% 3.61/0.96
% 3.61/0.96 % Proof 1 at 0.50 (+ 0.07) seconds.
% 3.61/0.96 % Length of proof is 15.
% 3.61/0.96 % Level of proof is 4.
% 3.61/0.96 % Maximum clause weight is 37.000.
% 3.61/0.96 % Given clauses 75.
% 3.61/0.96
% 3.61/0.96 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------