%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : GRA005+1 : TPTP v9.3.1. Bugfixed v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n015.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 : Thu Sep 24 08:40:46 AM UTC 2026
% Result : Theorem 0.38s 0.64s
% Output : Proof 0.38s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 2
% Syntax : Number of formulae : 29 ( 12 unt; 0 def)
% Number of atoms : 95 ( 38 equ)
% Maximal formula atoms : 5 ( 3 avg)
% Number of connectives : 89 ( 23 ~; 12 |; 51 &)
% ( 0 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 5 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-3 aty)
% Number of functors : 8 ( 8 usr; 6 con; 0-1 aty)
% Number of variables : 69 ( 2 sgn 27 !; 36 ?)
% Comments :
%------------------------------------------------------------------------------
fof(shortest_path_properties,axiom,
! [V1,V2,E1,E2,P] :
( ( precedes(E1,E2,P)
& shortest_path(V1,V2,P) )
=> ( ~ precedes(E2,E1,P)
& ~ ? [E3] :
( head_of(E3) = head_of(E2)
& tail_of(E3) = tail_of(E1) ) ) ),
file('GRA001+0.ax',shortest_path_properties) ).
fof(no_short_cut_edge,conjecture,
! [V1,V2,E1,E2,P] :
( ( precedes(E1,E2,P)
& shortest_path(V1,V2,P) )
=> ~ ? [E3] :
( head_of(E3) = head_of(E2)
& tail_of(E3) = tail_of(E1)
& edge(E3) ) ),
file('theBenchmark.p',no_short_cut_edge) ).
fof(f_12_1,plain,
! [V1,V2,E1,E2,P] :
( ( ~ precedes(E2,E1,P)
& ! [E3] :
( head_of(E3) != head_of(E2)
| tail_of(E3) != tail_of(E1) ) )
| ~ precedes(E1,E2,P)
| ~ shortest_path(V1,V2,P) ),
inference(fof_nnf,[status(thm)],[shortest_path_properties]) ).
fof(f_12_2,plain,
! [U_60,U_59,U_58,U_57,U_56] :
( ( ~ precedes(U_57,U_58,U_56)
& ! [U_55] :
( head_of(U_55) != head_of(U_57)
| tail_of(U_55) != tail_of(U_58) ) )
| ~ precedes(U_58,U_57,U_56)
| ~ shortest_path(U_60,U_59,U_56) ),
inference(variable_rename,[status(thm)],[f_12_1]) ).
cnf(f_12_3,plain,
( head_of(U_55) != head_of(U_57)
| tail_of(U_55) != tail_of(U_58)
| ~ precedes(U_58,U_57,U_56)
| ~ shortest_path(U_60,U_59,U_56) ),
inference(clausify,[status(thm)],[f_12_2]) ).
fof(f_18_1,negated_conjecture,
~ ! [V1,V2,E1,E2,P] :
( ( precedes(E1,E2,P)
& shortest_path(V1,V2,P) )
=> ~ ? [E3] :
( head_of(E3) = head_of(E2)
& tail_of(E3) = tail_of(E1)
& edge(E3) ) ),
inference(negate,[status(cth)],[no_short_cut_edge]) ).
fof(f_18_2,negated_conjecture,
? [V1,V2,E1,E2,P] :
( ? [E3] :
( head_of(E3) = head_of(E2)
& tail_of(E3) = tail_of(E1)
& edge(E3) )
& precedes(E1,E2,P)
& shortest_path(V1,V2,P) ),
inference(fof_nnf,[status(thm)],[f_18_1]) ).
fof(f_18_3,negated_conjecture,
? [U_89,U_88,U_87,U_86,U_85] :
( ? [U_84] :
( head_of(U_84) = head_of(U_86)
& tail_of(U_84) = tail_of(U_87)
& edge(U_84) )
& precedes(U_87,U_86,U_85)
& shortest_path(U_89,U_88,U_85) ),
inference(variable_rename,[status(thm)],[f_18_2]) ).
fof(f_18_4,negated_conjecture,
? [U_89,U_88,U_87,U_86] :
( ? [U_85] :
( precedes(U_87,U_86,U_85)
& shortest_path(U_89,U_88,U_85) )
& ? [U_84] :
( head_of(U_84) = head_of(U_86)
& tail_of(U_84) = tail_of(U_87)
& edge(U_84) ) ),
inference(miniscope,[status(thm)],[f_18_3]) ).
fof(f_18_5,negated_conjecture,
? [U_88,U_87,U_86] :
( ? [U_85] :
( precedes(U_87,U_86,U_85)
& shortest_path(sK9,U_88,U_85) )
& ? [U_84] :
( head_of(U_84) = head_of(U_86)
& tail_of(U_84) = tail_of(U_87)
& edge(U_84) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9]),skolemize(U_89,sK9)],[f_18_4]) ).
fof(f_18_6,negated_conjecture,
? [U_87,U_86] :
( ? [U_85] :
( precedes(U_87,U_86,U_85)
& shortest_path(sK9,sK10,U_85) )
& ? [U_84] :
( head_of(U_84) = head_of(U_86)
& tail_of(U_84) = tail_of(U_87)
& edge(U_84) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10]),skolemize(U_88,sK10)],[f_18_5]) ).
fof(f_18_7,negated_conjecture,
? [U_86] :
( ? [U_85] :
( precedes(sK11,U_86,U_85)
& shortest_path(sK9,sK10,U_85) )
& ? [U_84] :
( head_of(U_84) = head_of(U_86)
& tail_of(U_84) = tail_of(sK11)
& edge(U_84) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11]),skolemize(U_87,sK11)],[f_18_6]) ).
fof(f_18_8,negated_conjecture,
( ? [U_85] :
( precedes(sK11,sK12,U_85)
& shortest_path(sK9,sK10,U_85) )
& ? [U_84] :
( head_of(U_84) = head_of(sK12)
& tail_of(U_84) = tail_of(sK11)
& edge(U_84) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12]),skolemize(U_86,sK12)],[f_18_7]) ).
fof(f_18_9,negated_conjecture,
( ? [U_85] :
( precedes(sK11,sK12,U_85)
& shortest_path(sK9,sK10,U_85) )
& head_of(sK13) = head_of(sK12)
& tail_of(sK13) = tail_of(sK11)
& edge(sK13) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13]),skolemize(U_84,sK13)],[f_18_8]) ).
fof(f_18_10,negated_conjecture,
( precedes(sK11,sK12,sK14)
& shortest_path(sK9,sK10,sK14)
& head_of(sK13) = head_of(sK12)
& tail_of(sK13) = tail_of(sK11)
& edge(sK13) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14]),skolemize(U_85,sK14)],[f_18_9]) ).
fof(f_18_11,negated_conjecture,
( precedes(sK11,sK12,sK14)
& shortest_path(sK9,sK10,sK14)
& head_of(sK13) = head_of(sK12)
& tail_of(sK13) = tail_of(sK11)
& edge(sK13) ),
inference(definitional_conversion,[status(esa)],[f_18_10]) ).
cnf(f_18_13,negated_conjecture,
tail_of(sK13) = tail_of(sK11),
inference(clausify,[status(thm)],[f_18_11]) ).
cnf(f_18_14,negated_conjecture,
head_of(sK13) = head_of(sK12),
inference(clausify,[status(thm)],[f_18_11]) ).
cnf(f_18_15,negated_conjecture,
shortest_path(sK9,sK10,sK14),
inference(clausify,[status(thm)],[f_18_11]) ).
cnf(f_18_16,negated_conjecture,
precedes(sK11,sK12,sK14),
inference(clausify,[status(thm)],[f_18_11]) ).
cnf(t1,plain,
( ~ precedes(sK11,sK12,sK14)
| tail_of(sK13) != tail_of(sK11)
| head_of(sK13) != head_of(sK12)
| ~ shortest_path(sK9,sK10,sK14) ),
inference(start,[status(thm),parent(0:0)],[f_12_3]) ).
cnf(t2,plain,
shortest_path(sK9,sK10,sK14),
inference(extension,[status(thm),parent(t1:1)],[f_18_15]) ).
cnf(t3,plain,
$false,
inference(connection,[status(thm),parent(t2:1)],[t2:1,t1:1]) ).
cnf(t4,plain,
head_of(sK13) = head_of(sK12),
inference(extension,[status(thm),parent(t1:2)],[f_18_14]) ).
cnf(t5,plain,
$false,
inference(connection,[status(thm),parent(t4:1)],[t4:1,t1:2]) ).
cnf(t6,plain,
tail_of(sK13) = tail_of(sK11),
inference(extension,[status(thm),parent(t1:3)],[f_18_13]) ).
cnf(t7,plain,
$false,
inference(connection,[status(thm),parent(t6:1)],[t6:1,t1:3]) ).
cnf(t8,plain,
precedes(sK11,sK12,sK14),
inference(extension,[status(thm),parent(t1:4)],[f_18_16]) ).
cnf(t9,plain,
$false,
inference(connection,[status(thm),parent(t8:1)],[t8:1,t1:4]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRA005+1 : TPTP v9.3.1. Bugfixed v3.2.0.
% 0.00/0.03 This is a FOF_THM_RFO_SEQ problem
% 0.00/0.04 % Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n015.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 : Sat Sep 19 08:21:48 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.38/0.64 % SZS status Theorem for theBenchmark
% 0.38/0.64 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------