%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GEO147-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n016.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 : Fri Sep 25 01:17:10 PM UTC 2026
% Result : Unsatisfiable 9.53s 1.91s
% Output : Proof 9.53s
% Verified :
% Comments :
%------------------------------------------------------------------------------
cnf(t116,axiom,
sF0 = connect(sk28,sk29,sk27),
introduced(definition) ).
cnf(f110,negated_conjecture,
connect(sk28,sk29,sk27),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t13_156) ).
fof(f110_nnf,plain,
connect(sk28,sk29,sk27),
inference(nnf_transformation,[status(thm)],[f110]) ).
cnf(c110,plain,
connect(sk28,sk29,sk27),
inference(cnf_transformation,[status(esa)],[f110_nnf]) ).
cnf(t8,plain,
connect(sk28,sk29,sk27) = true,
inference(equality_encoding,[status(esa)],[c110]) ).
cnf(t136,plain,
connect(sk28,sk29,sk27) = true,
inference(orient,[status(thm)],[t8]) ).
cnf(t1334,plain,
sF0 = true,
inference(step,[status(thm)],[t116,t136]) ).
cnf(t139,plain,
true = sF0,
inference(orient,[status(thm)],[t1334]) ).
cnf(t119,axiom,
sF3 = not(incident_o(sk27,ax3_sk1(sk28))),
introduced(definition) ).
cnf(t117,axiom,
sF1 = ax3_sk1(sk28),
introduced(definition) ).
cnf(t128,plain,
ax3_sk1(sk28) = sF1,
inference(orient,[status(thm)],[t117]) ).
cnf(t1352,plain,
sF3 = not(incident_o(sk27,sF1)),
inference(step,[status(thm)],[t119,t128]) ).
cnf(t118,axiom,
sF2 = incident_o(sk27,ax3_sk1(sk28)),
introduced(definition) ).
cnf(t1350,plain,
sF2 = incident_o(sk27,sF1),
inference(step,[status(thm)],[t118,t128]) ).
cnf(t158,plain,
incident_o(sk27,sF1) = sF2,
inference(orient,[status(thm)],[t1350]) ).
cnf(t1353,plain,
sF3 = not(sF2),
inference(step,[status(thm)],[t1352,t158]) ).
cnf(t161,plain,
not(sF2) = sF3,
inference(orient,[status(thm)],[t1353]) ).
cnf(t1211,plain,
not(sF0) = sF3,
inference(rw,[status(thm)],[t161]) ).
cnf(t1,plain,
not(true) = false,
introduced(definition) ).
cnf(t127,plain,
not(true) = false,
inference(orient,[status(thm)],[t1]) ).
cnf(t1337,plain,
not(sF0) = false,
inference(step,[status(thm)],[t127,t139]) ).
cnf(t142,plain,
not(sF0) = false,
inference(rw,[status(thm)],[t1337]) ).
cnf(t155,plain,
not(sF0) = false,
inference(orient,[status(thm)],[t142]) ).
cnf(t1631,plain,
false = sF3,
inference(step,[status(thm)],[t1211,t155]) ).
cnf(t1221,plain,
false = sF3,
inference(orient,[status(thm)],[t1631]) ).
cnf(t122,axiom,
sF6 = not(incident_o(sk27,ax3_sk1(sk29))),
introduced(definition) ).
cnf(t120,axiom,
sF4 = ax3_sk1(sk29),
introduced(definition) ).
cnf(t129,plain,
ax3_sk1(sk29) = sF4,
inference(orient,[status(thm)],[t120]) ).
cnf(t1355,plain,
sF6 = not(incident_o(sk27,sF4)),
inference(step,[status(thm)],[t122,t129]) ).
cnf(t121,axiom,
sF5 = incident_o(sk27,ax3_sk1(sk29)),
introduced(definition) ).
cnf(t1351,plain,
sF5 = incident_o(sk27,sF4),
inference(step,[status(thm)],[t121,t129]) ).
cnf(t159,plain,
incident_o(sk27,sF4) = sF5,
inference(orient,[status(thm)],[t1351]) ).
cnf(t1356,plain,
sF6 = not(sF5),
inference(step,[status(thm)],[t1355,t159]) ).
cnf(t165,plain,
not(sF5) = sF6,
inference(orient,[status(thm)],[t1356]) ).
cnf(f111,negated_conjecture,
( ~ incident_o(sk27,trajectory_of(sk29))
| ~ incident_o(sk27,trajectory_of(sk28)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t13_157) ).
fof(f111_nnf,plain,
( ~ incident_o(sk27,trajectory_of(sk29))
| ~ incident_o(sk27,trajectory_of(sk28)) ),
inference(nnf_transformation,[status(thm)],[f111]) ).
fof(f111_sk,plain,
( ~ incident_o(sk27,trajectory_of(sk29))
| ~ incident_o(sk27,trajectory_of(sk28)) ),
inference(skolemisation,[status(esa)],[f111_nnf]) ).
cnf(c111,plain,
( ~ incident_o(sk27,trajectory_of(sk29))
| ~ incident_o(sk27,trajectory_of(sk28)) ),
inference(cnf_transformation,[status(esa)],[f111_sk]) ).
cnf(u5,axiom,
or(not(incident_o(sk27,trajectory_of(sk28))),not(incident_o(sk27,trajectory_of(sk29)))) = true,
inference(equality_encoding,[status(esa)],[c111]) ).
cnf(f107,axiom,
trajectory_of(A) = ax3_sk1(A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',trajectories_are_oriented_curves_12) ).
fof(f107_nnf,plain,
! [A] : trajectory_of(A) = ax3_sk1(A),
inference(nnf_transformation,[status(thm)],[f107]) ).
fof(f107_sk,plain,
! [A] : trajectory_of(A) = ax3_sk1(A),
inference(skolemisation,[status(esa)],[f107_nnf]) ).
cnf(c107,plain,
trajectory_of(X0) = ax3_sk1(X0),
inference(cnf_transformation,[status(esa)],[f107_sk]) ).
cnf(d0,axiom,
trajectory_of(X0) = ax3_sk1(X0),
inference(equality_encoding,[status(esa)],[c107]) ).
cnf(t41,plain,
or(not(incident_o(sk27,ax3_sk1(sk28))),not(incident_o(sk27,ax3_sk1(sk29)))) = true,
inference(definition_unfolding,[status(thm)],[u5,d0]) ).
cnf(t1476,plain,
or(not(incident_o(sk27,sF1)),not(incident_o(sk27,ax3_sk1(sk29)))) = true,
inference(step,[status(thm)],[t41,t128]) ).
cnf(t1477,plain,
or(not(sF2),not(incident_o(sk27,ax3_sk1(sk29)))) = true,
inference(step,[status(thm)],[t1476,t158]) ).
cnf(t1478,plain,
or(sF3,not(incident_o(sk27,ax3_sk1(sk29)))) = true,
inference(step,[status(thm)],[t1477,t161]) ).
cnf(t1479,plain,
or(sF3,not(incident_o(sk27,sF4))) = true,
inference(step,[status(thm)],[t1478,t129]) ).
cnf(t1480,plain,
or(sF3,not(sF5)) = true,
inference(step,[status(thm)],[t1479,t159]) ).
cnf(t1481,plain,
or(sF3,sF6) = true,
inference(step,[status(thm)],[t1480,t165]) ).
cnf(t1482,plain,
or(sF3,sF6) = sF0,
inference(step,[status(thm)],[t1481,t139]) ).
cnf(t479,plain,
or(sF3,sF6) = sF0,
inference(orient,[status(thm)],[t1482]) ).
cnf(t6,plain,
or(false,X1) = X1,
introduced(definition) ).
cnf(t134,plain,
or(false,X1) = X1,
inference(orient,[status(thm)],[t6]) ).
cnf(t1634,plain,
or(sF3,X1) = X1,
inference(step,[status(thm)],[t134,t1221]) ).
cnf(t1224,plain,
or(sF3,X1) = X1,
inference(rw,[status(thm)],[t1634]) ).
cnf(t1266,plain,
or(sF3,X1) = X1,
inference(orient,[status(thm)],[t1224]) ).
cnf(t1673,plain,
sF6 = sF0,
inference(step,[status(thm)],[t479,t1266]) ).
cnf(t1267,plain,
sF6 = sF0,
inference(rw,[status(thm)],[t1673]) ).
cnf(t1268,plain,
sF6 = sF0,
inference(orient,[status(thm)],[t1267]) ).
cnf(t1674,plain,
not(sF5) = sF0,
inference(step,[status(thm)],[t165,t1268]) ).
cnf(t1269,plain,
not(sF5) = sF0,
inference(orient,[status(thm)],[t1674]) ).
cnf(t1282,plain,
not(sF0) = sF0,
inference(rw,[status(thm)],[t1269]) ).
cnf(t1635,plain,
not(sF0) = sF3,
inference(step,[status(thm)],[t155,t1221]) ).
cnf(t1225,plain,
not(sF0) = sF3,
inference(orient,[status(thm)],[t1635]) ).
cnf(t1692,plain,
sF3 = sF0,
inference(step,[status(thm)],[t1282,t1225]) ).
cnf(t1308,plain,
sF3 = sF0,
inference(orient,[status(thm)],[t1692]) ).
cnf(t1713,plain,
false = sF0,
inference(step,[status(thm)],[t1221,t1308]) ).
cnf(t1329,plain,
false = sF0,
inference(orient,[status(thm)],[t1713]) ).
cnf(f21,axiom,
( ~ end_point(A,B)
| ~ inner_point(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',inner_point_defn_22) ).
fof(f21_nnf,plain,
! [A,B] :
( ~ end_point(A,B)
| ~ inner_point(A,B) ),
inference(nnf_transformation,[status(thm)],[f21]) ).
fof(f21_sk,plain,
! [A,B] :
( ~ end_point(A,B)
| ~ inner_point(A,B) ),
inference(skolemisation,[status(esa)],[f21_nnf]) ).
cnf(c21,plain,
( ~ end_point(X0,X1)
| ~ inner_point(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f21_sk]) ).
cnf(f30,axiom,
( ~ end_point(B,A)
| ~ closed(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',closed_defn_31) ).
fof(f30_nnf,plain,
! [A,B] :
( ~ end_point(B,A)
| ~ closed(A) ),
inference(nnf_transformation,[status(thm)],[f30]) ).
fof(f30_sk,plain,
! [A,B] :
( ~ end_point(B,A)
| ~ closed(A) ),
inference(skolemisation,[status(esa)],[f30_nnf]) ).
cnf(c30,plain,
( ~ end_point(X1,X0)
| ~ closed(X0) ),
inference(cnf_transformation,[status(esa)],[f30_sk]) ).
cnf(f41,axiom,
( A != ax0_sk11(A,B)
| ~ end_point(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c6_42) ).
fof(f41_nnf,plain,
! [A,B] :
( A != ax0_sk11(A,B)
| ~ end_point(A,B) ),
inference(nnf_transformation,[status(thm)],[f41]) ).
fof(f41_sk,plain,
! [A,B] :
( A != ax0_sk11(A,B)
| ~ end_point(A,B) ),
inference(skolemisation,[status(esa)],[f41_nnf]) ).
cnf(c41,plain,
( X0 != ax0_sk11(X0,X1)
| ~ end_point(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f41_sk]) ).
cnf(f48,axiom,
( B != D
| ~ between_c(A,B,C,D) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',between_c_defn_1) ).
fof(f48_nnf,plain,
! [A,B,C,D] :
( B != D
| ~ between_c(A,B,C,D) ),
inference(nnf_transformation,[status(thm)],[f48]) ).
fof(f48_sk,plain,
! [A,B,C,D] :
( B != D
| ~ between_c(A,B,C,D) ),
inference(skolemisation,[status(esa)],[f48_nnf]) ).
cnf(c48,plain,
( X1 != X3
| ~ between_c(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(esa)],[f48_sk]) ).
cnf(f108,axiom,
( ~ ordered_by(trajectory_of(C),F,D)
| ~ ordered_by(trajectory_of(A),B,E)
| ~ once(at_the_same_time(at(A,E),at(C,F)))
| ~ once(at_the_same_time(at(A,B),at(C,D))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',homogeneous_behaviour_13) ).
fof(f108_nnf,plain,
! [A,B,C,D,E,F] :
( ~ ordered_by(trajectory_of(C),F,D)
| ~ ordered_by(trajectory_of(A),B,E)
| ~ once(at_the_same_time(at(A,E),at(C,F)))
| ~ once(at_the_same_time(at(A,B),at(C,D))) ),
inference(nnf_transformation,[status(thm)],[f108]) ).
fof(f108_sk,plain,
! [A,B,C,D,E,F] :
( ~ ordered_by(trajectory_of(C),F,D)
| ~ ordered_by(trajectory_of(A),B,E)
| ~ once(at_the_same_time(at(A,E),at(C,F)))
| ~ once(at_the_same_time(at(A,B),at(C,D))) ),
inference(skolemisation,[status(esa)],[f108_nnf]) ).
cnf(c108,plain,
( ~ ordered_by(trajectory_of(X2),X5,X3)
| ~ ordered_by(trajectory_of(X0),X1,X4)
| ~ once(at_the_same_time(at(X0,X4),at(X2,X5)))
| ~ once(at_the_same_time(at(X0,X1),at(X2,X3))) ),
inference(cnf_transformation,[status(esa)],[f108_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c21,c30,c41,c48,c108,c111]) ).
cnf(g0_0,plain,
sF0 != false,
inference(rw,[status(thm)],[goal_0,t139]) ).
cnf(g0_1,plain,
sF0 != sF0,
inference(rw,[status(thm)],[g0_0,t1329]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO147-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.12/0.38 % Computer : n016.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Wed Sep 23 11:13:26 UTC 2026
% 0.12/0.39 % CPUTime :
% 0.12/0.39 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 9.53/1.91 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 9.53/1.91 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------