%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : GRA007+2 : TPTP v9.3.1. Bugfixed v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% Computer : n001.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:18:21 AM UTC 2026
% Result : Theorem 105.43s 23.82s
% Output : Refutation 108.24s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 31
% Syntax : Number of formulae : 489 ( 43 unt; 0 typ; 12 def)
% Number of atoms : 1973 ( 694 equ; 0 cnn)
% Maximal formula atoms : 28 ( 4 avg)
% Number of connectives : 7636 ( 826 ~; 898 |; 228 &;5596 @)
% ( 3 <=>; 80 =>; 2 <=; 3 <~>)
% Maximal formula depth : 28 ( 8 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 40 ( 37 usr; 14 con; 0-4 aty)
% Number of variables : 983 ( 18 ^; 905 !; 48 ?; 983 :)
% ( 0 !>; 0 ?*; 0 @-; 12 @+)
% Comments :
%------------------------------------------------------------------------------
thf(complete_decl,type,
complete: $o ).
thf(shortest_path_decl,type,
shortest_path: $i > $i > $i > $o ).
thf(precedes_decl,type,
precedes: $i > $i > $i > $o ).
thf(edge_decl,type,
edge: $i > $o ).
thf(tail_of_decl,type,
tail_of: $i > $i ).
thf(head_of_decl,type,
head_of: $i > $i ).
thf(path_decl,type,
path: $i > $i > $i > $o ).
thf(number_of_in_decl,type,
number_of_in: $i > $i > $i ).
thf(sequential_pairs_decl,type,
sequential_pairs: $i ).
thf(minus_decl,type,
minus: $i > $i > $i ).
thf(length_of_decl,type,
length_of: $i > $i ).
thf(n1_decl,type,
n1: $i ).
thf(less_or_equal_decl,type,
less_or_equal: $i > $i > $o ).
thf(graph_decl,type,
graph: $i ).
thf(edges_decl,type,
edges: $i ).
thf(on_path_decl,type,
on_path: $i > $i > $o ).
thf(sequential_decl,type,
sequential: $i > $i > $o ).
thf(triangle_decl,type,
triangle: $i > $i > $i > $o ).
thf(triangles_decl,type,
triangles: $i ).
thf(vertex_decl,type,
vertex: $i > $o ).
thf(path_cons_decl,type,
path_cons: $i > $i > $i ).
thf(empty_decl,type,
empty: $i ).
thf(in_path_decl,type,
in_path: $i > $i > $o ).
thf(sk1_decl,type,
sk1: $i ).
thf(sk2_decl,type,
sk2: $i ).
thf(sk3_decl,type,
sk3: $i ).
thf(sk4_decl,type,
sk4: $i ).
thf(sk5_decl,type,
sk5: $i ).
thf(sk6_decl,type,
sk6: $i > $i ).
thf(sk7_decl,type,
sk7: $i > $i ).
thf(sk8_decl,type,
sk8: $i > $i > $i > $i ).
thf(sk9_decl,type,
sk9: $i > $i > $i > $o ).
thf(sk10_decl,type,
sk10: $i > $i > $i > $i ).
thf(sk11_decl,type,
sk11: $i > $i > $i > $i > $i ).
thf(sk12_decl,type,
sk12: $i > $i > $i > $o ).
thf(sk13_decl,type,
sk13: $i > $i > $i > $i ).
thf(sk14_decl,type,
sk14: $i > $i > $i > $i ).
thf(sk1_def,definition,
( sk1
= ( @+[A: $i] :
~ ! [B: $i,C: $i,D: $i] :
( ? [E: $i] :
( ( E @ ( D @ ( C @ precedes ) ) )
& ( E @ ( B @ ( A @ shortest_path ) ) ) )
=> ? [E: $i] :
( ( ( E @ head_of )
= ( C @ tail_of ) )
& ( ( E @ tail_of )
= ( D @ head_of ) )
& ( E @ edge ) ) ) ) ) ).
thf(sk2_def,definition,
( sk2
= ( @+[A: $i] :
~ ! [B: $i,C: $i] :
( ? [D: $i] :
( ( D @ ( C @ ( B @ precedes ) ) )
& ( D @ ( A @ ( sk1 @ shortest_path ) ) ) )
=> ? [D: $i] :
( ( ( D @ head_of )
= ( B @ tail_of ) )
& ( ( D @ tail_of )
= ( C @ head_of ) )
& ( D @ edge ) ) ) ) ) ).
thf(sk3_def,definition,
( sk3
= ( @+[A: $i] :
~ ! [B: $i] :
( ? [C: $i] :
( ( C @ ( B @ ( A @ precedes ) ) )
& ( C @ ( sk2 @ ( sk1 @ shortest_path ) ) ) )
=> ? [C: $i] :
( ( ( C @ head_of )
= ( A @ tail_of ) )
& ( ( C @ tail_of )
= ( B @ head_of ) )
& ( C @ edge ) ) ) ) ) ).
thf(sk4_def,definition,
( sk4
= ( @+[A: $i] :
~ ( ? [B: $i] :
( ( B @ ( A @ ( sk3 @ precedes ) ) )
& ( B @ ( sk2 @ ( sk1 @ shortest_path ) ) ) )
=> ? [B: $i] :
( ( ( B @ head_of )
= ( sk3 @ tail_of ) )
& ( ( B @ tail_of )
= ( A @ head_of ) )
& ( B @ edge ) ) ) ) ) ).
thf(sk5_def,definition,
( sk5
= ( @+[A: $i] :
( ( A @ ( sk4 @ ( sk3 @ precedes ) ) )
& ( A @ ( sk2 @ ( sk1 @ shortest_path ) ) ) ) ) ) ).
thf(sk6_def,definition,
( sk6
= ( ^ [A: $i] :
@+[B: $i] :
~ ! [C: $i] :
( ( ( C @ ( B @ sequential ) )
& ( A @ ( C @ on_path ) )
& ( A @ ( B @ on_path ) ) )
=> ? [D: $i] : ( D @ ( C @ ( B @ triangle ) ) ) ) ) ) ).
thf(sk7_def,definition,
( sk7
= ( ^ [A: $i] :
@+[B: $i] :
~ ( ( ( B @ ( A @ sk6 @ sequential ) )
& ( A @ ( B @ on_path ) )
& ( A @ ( A @ sk6 @ on_path ) ) )
=> ? [C: $i] : ( C @ ( B @ ( A @ sk6 @ triangle ) ) ) ) ) ) ).
thf(sk8_def,definition,
( sk8
= ( ^ [A: $i,B: $i,C: $i] :
@+[D: $i] :
( ~ ( ( ? [E: $i] :
( ( A
= ( E @ ( D @ path_cons ) ) )
& ( E @ ( B @ ( D @ head_of @ path ) ) ) )
=> ( ( A
= ( empty @ ( D @ path_cons ) ) )
& ( B
= ( D @ head_of ) ) ) )
& ( ( ( A
= ( empty @ ( D @ path_cons ) ) )
& ( B
= ( D @ head_of ) ) )
=> ? [E: $i] :
( ( A
= ( E @ ( D @ path_cons ) ) )
& ( E @ ( B @ ( D @ head_of @ path ) ) ) ) ) )
& ( C
= ( D @ tail_of ) )
& ( D @ edge ) ) ) ) ).
thf(sk10_def,definition,
( sk10
= ( ^ [A: $i,B: $i,C: $i] :
@+[D: $i] :
( ( A
= ( D @ ( C @ ( B @ ( A @ sk8 ) ) @ path_cons ) ) )
& ( D @ ( B @ ( C @ ( B @ ( A @ sk8 ) ) @ head_of @ path ) ) ) ) ) ) ).
thf(sk11_def,definition,
( sk11
= ( ^ [A: $i,B: $i,C: $i,D: $i] :
@+[E: $i] :
( ( ( A
= ( E @ tail_of ) )
| ( A
= ( E @ head_of ) ) )
& ( B @ ( E @ on_path ) ) ) ) ) ).
thf(sk13_def,definition,
( sk13
= ( ^ [A: $i,B: $i,C: $i] :
@+[D: $i] :
( ( C @ ( A @ ( D @ precedes ) ) )
& ( D @ ( B @ sequential ) ) ) ) ) ).
thf(sk14_def,definition,
( sk14
= ( ^ [A: $i,B: $i,C: $i] :
@+[D: $i] :
~ ( ( D @ ( B @ ( C @ path ) ) )
=> ( D @ length_of @ ( A @ length_of @ less_or_equal ) ) ) ) ) ).
thf(7,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ sequential ) )
<=> ( ( ( A @ head_of )
= ( B @ tail_of ) )
& ( A != B )
& ( B @ edge )
& ( A @ edge ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sequential_defn) ).
thf(48,plain,
! [A: $i,B: $i] :
( ( ( ( ( A @ head_of )
= ( B @ tail_of ) )
& ( A != B )
& ( B @ edge )
& ( A @ edge ) )
=> ( B @ ( A @ sequential ) ) )
& ( ( B @ ( A @ sequential ) )
=> ( ( ( A @ head_of )
= ( B @ tail_of ) )
& ( A != B )
& ( B @ edge )
& ( A @ edge ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).
thf(49,plain,
( ! [A: $i,B: $i] :
( ( ( ( A @ head_of )
= ( B @ tail_of ) )
& ( A != B )
& ( B @ edge )
& ( A @ edge ) )
=> ( B @ ( A @ sequential ) ) )
& ! [A: $i,B: $i] :
( ( B @ ( A @ sequential ) )
=> ( ( ( A @ head_of )
= ( B @ tail_of ) )
& ( A != B )
& ( B @ edge )
& ( A @ edge ) ) ) ),
inference(miniscope,[status(thm)],[48]) ).
thf(50,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ sequential ) )
| ( ( C @ head_of )
!= ( D @ tail_of ) )
| ( C = D )
| ~ ( D @ edge )
| ~ ( C @ edge ) )
& ( ( ( A @ head_of )
= ( B @ tail_of ) )
| ~ ( B @ ( A @ sequential ) ) )
& ( ( A != B )
| ~ ( B @ ( A @ sequential ) ) )
& ( ( B @ edge )
| ~ ( B @ ( A @ sequential ) ) )
& ( ( A @ edge )
| ~ ( B @ ( A @ sequential ) ) ) ),
inference(cnf,[status(esa)],[49]) ).
thf(52,plain,
! [B: $i,A: $i] :
( ( ( A @ head_of )
= ( B @ tail_of ) )
| ~ ( B @ ( A @ sequential ) ) ),
inference(cnfConj,[status(thm)],[50]) ).
thf(56,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ sequential ) )
| ( ( A @ head_of )
= ( B @ tail_of ) ) ),
inference(lifteq,[status(thm)],[52]) ).
thf(1,conjecture,
( complete
=> ! [A: $i,B: $i,C: $i,D: $i,E: $i] :
( ( ( E @ ( D @ ( C @ precedes ) ) )
& ( E @ ( B @ ( A @ shortest_path ) ) ) )
=> ? [F: $i] :
( ( ( F @ head_of )
= ( C @ tail_of ) )
& ( ( F @ tail_of )
= ( D @ head_of ) )
& ( F @ edge ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',back_edge) ).
thf(2,negated_conjecture,
~ ( complete
=> ! [A: $i,B: $i,C: $i,D: $i,E: $i] :
( ( ( E @ ( D @ ( C @ precedes ) ) )
& ( E @ ( B @ ( A @ shortest_path ) ) ) )
=> ? [F: $i] :
( ( ( F @ head_of )
= ( C @ tail_of ) )
& ( ( F @ tail_of )
= ( D @ head_of ) )
& ( F @ edge ) ) ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(21,plain,
~ ( complete
=> ! [A: $i,B: $i,C: $i,D: $i,E: $i] :
( ( ( E @ ( D @ ( C @ precedes ) ) )
& ( E @ ( B @ ( A @ shortest_path ) ) ) )
=> ? [F: $i] :
( ( ( F @ head_of )
= ( C @ tail_of ) )
& ( ( F @ tail_of )
= ( D @ head_of ) )
& ( F @ edge ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(22,plain,
~ ( complete
=> ! [A: $i,B: $i,C: $i,D: $i] :
( ? [E: $i] :
( ( E @ ( D @ ( C @ precedes ) ) )
& ( E @ ( B @ ( A @ shortest_path ) ) ) )
=> ? [E: $i] :
( ( ( E @ head_of )
= ( C @ tail_of ) )
& ( ( E @ tail_of )
= ( D @ head_of ) )
& ( E @ edge ) ) ) ),
inference(miniscope,[status(thm)],[21]) ).
thf(23,plain,
! [A: $i] :
( ( ( ( A @ head_of )
!= ( sk3 @ tail_of ) )
| ( ( A @ tail_of )
!= ( sk4 @ head_of ) )
| ~ ( A @ edge ) )
& ( sk5 @ ( sk4 @ ( sk3 @ precedes ) ) )
& ( sk5 @ ( sk2 @ ( sk1 @ shortest_path ) ) )
& complete ),
inference(cnf,[status(esa)],[22]) ).
thf(25,plain,
sk5 @ ( sk2 @ ( sk1 @ shortest_path ) ),
inference(cnfConj,[status(thm)],[23]) ).
thf(14,axiom,
! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ ( A @ shortest_path ) ) )
<=> ( ! [D: $i] :
( ( D @ ( B @ ( A @ path ) ) )
=> ( D @ length_of @ ( C @ length_of @ less_or_equal ) ) )
& ( A != B )
& ( C @ ( B @ ( A @ path ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',shortest_path_defn) ).
thf(111,plain,
! [A: $i,B: $i,C: $i] :
( ( ( ! [D: $i] :
( ( D @ ( B @ ( A @ path ) ) )
=> ( D @ length_of @ ( C @ length_of @ less_or_equal ) ) )
& ( A != B )
& ( C @ ( B @ ( A @ path ) ) ) )
=> ( C @ ( B @ ( A @ shortest_path ) ) ) )
& ( ( C @ ( B @ ( A @ shortest_path ) ) )
=> ( ! [D: $i] :
( ( D @ ( B @ ( A @ path ) ) )
=> ( D @ length_of @ ( C @ length_of @ less_or_equal ) ) )
& ( A != B )
& ( C @ ( B @ ( A @ path ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[14]) ).
thf(112,plain,
( ! [A: $i,B: $i,C: $i] :
( ( ! [D: $i] :
( ( D @ ( B @ ( A @ path ) ) )
=> ( D @ length_of @ ( C @ length_of @ less_or_equal ) ) )
& ( A != B )
& ( C @ ( B @ ( A @ path ) ) ) )
=> ( C @ ( B @ ( A @ shortest_path ) ) ) )
& ! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ ( A @ shortest_path ) ) )
=> ( ! [D: $i] :
( ( D @ ( B @ ( A @ path ) ) )
=> ( D @ length_of @ ( C @ length_of @ less_or_equal ) ) )
& ( A != B )
& ( C @ ( B @ ( A @ path ) ) ) ) ) ),
inference(miniscope,[status(thm)],[111]) ).
thf(113,plain,
! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( G @ ( F @ ( E @ shortest_path ) ) )
| ~ ( E @ ( F @ ( G @ sk14 ) ) @ length_of @ ( G @ length_of @ less_or_equal ) )
| ( E = F )
| ~ ( G @ ( F @ ( E @ path ) ) ) )
& ( ( G @ ( F @ ( E @ shortest_path ) ) )
| ( E @ ( F @ ( G @ sk14 ) ) @ ( F @ ( E @ path ) ) )
| ( E = F )
| ~ ( G @ ( F @ ( E @ path ) ) ) )
& ( ( D @ length_of @ ( C @ length_of @ less_or_equal ) )
| ~ ( D @ ( B @ ( A @ path ) ) )
| ~ ( C @ ( B @ ( A @ shortest_path ) ) ) )
& ( ( A != B )
| ~ ( C @ ( B @ ( A @ shortest_path ) ) ) )
& ( ( C @ ( B @ ( A @ path ) ) )
| ~ ( C @ ( B @ ( A @ shortest_path ) ) ) ) ),
inference(cnf,[status(esa)],[112]) ).
thf(115,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ path ) ) )
| ~ ( C @ ( B @ ( A @ shortest_path ) ) ) ),
inference(cnfConj,[status(thm)],[113]) ).
thf(1402,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ shortest_path ) ) )
!= ( C @ ( B @ ( A @ shortest_path ) ) ) )
| ( C @ ( B @ ( A @ path ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[25,115]) ).
thf(1403,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ shortest_path ) ) )
!= ( C @ ( B @ ( A @ shortest_path ) ) ) )
| ( C @ ( B @ ( A @ path ) ) ) ),
inference(simp,[status(thm)],[1402]) ).
thf(1404,plain,
sk5 @ ( sk2 @ ( sk1 @ path ) ),
inference(pattern_uni,[status(thm)],[1403:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 )),bind(C,$thf( sk5 ))]]) ).
thf(9,axiom,
! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ ( A @ path ) ) )
=> ( ? [D: $i] :
( ( ( ( C
= ( empty @ ( D @ path_cons ) ) )
& ( B
= ( D @ head_of ) ) )
<~> ? [E: $i] :
( ( C
= ( E @ ( D @ path_cons ) ) )
& ( E @ ( B @ ( D @ head_of @ path ) ) ) ) )
& ( A
= ( D @ tail_of ) )
& ( D @ edge ) )
& ( B @ vertex )
& ( A @ vertex ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',path_properties) ).
thf(66,plain,
! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ ( A @ path ) ) )
=> ( ? [D: $i] :
( ~ ( ( ? [E: $i] :
( ( C
= ( E @ ( D @ path_cons ) ) )
& ( E @ ( B @ ( D @ head_of @ path ) ) ) )
=> ( ( C
= ( empty @ ( D @ path_cons ) ) )
& ( B
= ( D @ head_of ) ) ) )
& ( ( ( C
= ( empty @ ( D @ path_cons ) ) )
& ( B
= ( D @ head_of ) ) )
=> ? [E: $i] :
( ( C
= ( E @ ( D @ path_cons ) ) )
& ( E @ ( B @ ( D @ head_of @ path ) ) ) ) ) )
& ( A
= ( D @ tail_of ) )
& ( D @ edge ) )
& ( B @ vertex )
& ( A @ vertex ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[9]) ).
thf(67,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C
!= ( empty @ ( A @ ( B @ ( C @ sk8 ) ) @ path_cons ) ) )
| ( B
!= ( A @ ( B @ ( C @ sk8 ) ) @ head_of ) )
| ( A @ ( B @ ( C @ sk9 ) ) )
| ~ ( C @ ( B @ ( A @ path ) ) ) )
& ( ( C
= ( A @ ( B @ ( C @ sk10 ) ) @ ( A @ ( B @ ( C @ sk8 ) ) @ path_cons ) ) )
| ( A @ ( B @ ( C @ sk9 ) ) )
| ~ ( C @ ( B @ ( A @ path ) ) ) )
& ( ( A @ ( B @ ( C @ sk10 ) ) @ ( B @ ( A @ ( B @ ( C @ sk8 ) ) @ head_of @ path ) ) )
| ( A @ ( B @ ( C @ sk9 ) ) )
| ~ ( C @ ( B @ ( A @ path ) ) ) )
& ( ~ ( A @ ( B @ ( C @ sk9 ) ) )
| ( C
!= ( D @ ( A @ ( B @ ( C @ sk8 ) ) @ path_cons ) ) )
| ~ ( D @ ( B @ ( A @ ( B @ ( C @ sk8 ) ) @ head_of @ path ) ) )
| ~ ( C @ ( B @ ( A @ path ) ) ) )
& ( ~ ( A @ ( B @ ( C @ sk9 ) ) )
| ( C
= ( empty @ ( A @ ( B @ ( C @ sk8 ) ) @ path_cons ) ) )
| ~ ( C @ ( B @ ( A @ path ) ) ) )
& ( ~ ( A @ ( B @ ( C @ sk9 ) ) )
| ( B
= ( A @ ( B @ ( C @ sk8 ) ) @ head_of ) )
| ~ ( C @ ( B @ ( A @ path ) ) ) )
& ( ( A
= ( A @ ( B @ ( C @ sk8 ) ) @ tail_of ) )
| ~ ( C @ ( B @ ( A @ path ) ) ) )
& ( ( A @ ( B @ ( C @ sk8 ) ) @ edge )
| ~ ( C @ ( B @ ( A @ path ) ) ) )
& ( ( B @ vertex )
| ~ ( C @ ( B @ ( A @ path ) ) ) )
& ( ( A @ vertex )
| ~ ( C @ ( B @ ( A @ path ) ) ) ) ),
inference(cnf,[status(esa)],[66]) ).
thf(70,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( B @ ( C @ sk8 ) ) @ edge )
| ~ ( C @ ( B @ ( A @ path ) ) ) ),
inference(cnfConj,[status(thm)],[67]) ).
thf(3352,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ path ) ) )
!= ( C @ ( B @ ( A @ path ) ) ) )
| ( A @ ( B @ ( C @ sk8 ) ) @ edge )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1404,70]) ).
thf(3353,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ path ) ) )
!= ( C @ ( B @ ( A @ path ) ) ) )
| ( A @ ( B @ ( C @ sk8 ) ) @ edge ) ),
inference(simp,[status(thm)],[3352]) ).
thf(3354,plain,
sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ edge,
inference(pattern_uni,[status(thm)],[3353:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 )),bind(C,$thf( sk5 ))]]) ).
thf(12,axiom,
! [A: $i] :
( ( A @ edge )
=> ( ( A @ head_of )
!= ( A @ tail_of ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',no_loops) ).
thf(100,plain,
! [A: $i] :
( ( A @ edge )
=> ( ( A @ head_of )
!= ( A @ tail_of ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[12]) ).
thf(101,plain,
! [A: $i] :
( ( ( A @ head_of )
!= ( A @ tail_of ) )
| ~ ( A @ edge ) ),
inference(cnf,[status(esa)],[100]) ).
thf(102,plain,
! [A: $i] :
( ~ ( A @ edge )
| ( ( A @ head_of )
!= ( A @ tail_of ) ) ),
inference(lifteq,[status(thm)],[101]) ).
thf(3426,plain,
! [A: $i] :
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ edge )
!= ( A @ edge ) )
| ~ $true
| ( ( A @ head_of )
!= ( A @ tail_of ) ) ),
inference(paramod_ordered,[status(thm)],[3354,102]) ).
thf(3427,plain,
! [A: $i] :
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ edge )
!= ( A @ edge ) )
| ( ( A @ head_of )
!= ( A @ tail_of ) ) ),
inference(simp,[status(thm)],[3426]) ).
thf(3428,plain,
( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of )
!= ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ tail_of ) ),
inference(pattern_uni,[status(thm)],[3427:[bind(A,$thf( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) ))]]) ).
thf(69,plain,
! [C: $i,B: $i,A: $i] :
( ( A
= ( A @ ( B @ ( C @ sk8 ) ) @ tail_of ) )
| ~ ( C @ ( B @ ( A @ path ) ) ) ),
inference(cnfConj,[status(thm)],[67]) ).
thf(78,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( C @ ( B @ ( A @ path ) ) )
| ( ( A @ ( B @ ( C @ sk8 ) ) @ tail_of )
= A ) ),
inference(lifteq,[status(thm)],[69]) ).
thf(4046,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ path ) ) )
!= ( C @ ( B @ ( A @ path ) ) ) )
| ~ $true
| ( ( A @ ( B @ ( C @ sk8 ) ) @ tail_of )
= A ) ),
inference(paramod_ordered,[status(thm)],[1404,78]) ).
thf(4047,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ path ) ) )
!= ( C @ ( B @ ( A @ path ) ) ) )
| ( ( A @ ( B @ ( C @ sk8 ) ) @ tail_of )
= A ) ),
inference(simp,[status(thm)],[4046]) ).
thf(4048,plain,
( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ tail_of )
= sk1 ),
inference(pattern_uni,[status(thm)],[4047:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 )),bind(C,$thf( sk5 ))]]) ).
thf(4106,plain,
( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of )
!= sk1 ),
inference(rewrite,[status(thm)],[3428,4048]) ).
thf(4189,plain,
! [B: $i,A: $i] :
( ( ( A @ head_of )
!= ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of ) )
| ( ( B @ tail_of )
!= sk1 )
| ~ ( B @ ( A @ sequential ) ) ),
inference(paramod_ordered,[status(thm)],[56,4106]) ).
thf(4190,plain,
! [A: $i] :
( ( ( A @ tail_of )
!= sk1 )
| ~ ( A @ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ sequential ) ) ),
inference(pattern_uni,[status(thm)],[4189:[bind(A,$thf( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) )),bind(B,$thf( B ))]]) ).
thf(4201,plain,
! [A: $i] :
( ( ( A @ tail_of )
!= sk1 )
| ~ ( A @ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ sequential ) ) ),
inference(simp,[status(thm)],[4190]) ).
thf(117,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ shortest_path ) ) )
| ( A @ ( B @ ( C @ sk14 ) ) @ ( B @ ( A @ path ) ) )
| ( A = B )
| ~ ( C @ ( B @ ( A @ path ) ) ) ),
inference(cnfConj,[status(thm)],[113]) ).
thf(121,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ shortest_path ) ) )
| ( A @ ( B @ ( C @ sk14 ) ) @ ( B @ ( A @ path ) ) )
| ~ ( C @ ( B @ ( A @ path ) ) )
| ( A = B ) ),
inference(lifteq,[status(thm)],[117]) ).
thf(122,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ shortest_path ) ) )
| ( A @ ( B @ ( C @ sk14 ) ) @ ( B @ ( A @ path ) ) )
| ~ ( C @ ( B @ ( A @ path ) ) )
| ( A = B ) ),
inference(simp,[status(thm)],[121]) ).
thf(116,plain,
! [C: $i,B: $i,A: $i] :
( ( A != B )
| ~ ( C @ ( B @ ( A @ shortest_path ) ) ) ),
inference(cnfConj,[status(thm)],[113]) ).
thf(119,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( C @ ( B @ ( A @ shortest_path ) ) )
| ( A != B ) ),
inference(lifteq,[status(thm)],[116]) ).
thf(120,plain,
! [B: $i,A: $i] :
~ ( B @ ( A @ ( A @ shortest_path ) ) ),
inference(simp,[status(thm)],[119]) ).
thf(170,plain,
! [B: $i,A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ shortest_path ) ) )
!= ( B @ ( A @ ( A @ shortest_path ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[25,120]) ).
thf(171,plain,
! [B: $i,A: $i] :
( ( sk5 @ ( sk2 @ ( sk1 @ shortest_path ) ) )
!= ( B @ ( A @ ( A @ shortest_path ) ) ) ),
inference(simp,[status(thm)],[170]) ).
thf(172,plain,
! [B: $i,A: $i] :
( ( sk5 != B )
| ( sk2 != A )
| ( sk1 != A ) ),
inference(simp,[status(thm)],[171]) ).
thf(173,plain,
sk2 != sk1,
inference(simp,[status(thm)],[172]) ).
thf(202,plain,
! [C: $i,B: $i,A: $i] :
( ( A != sk2 )
| ( B != sk1 )
| ( C @ ( B @ ( A @ shortest_path ) ) )
| ( A @ ( B @ ( C @ sk14 ) ) @ ( B @ ( A @ path ) ) )
| ~ ( C @ ( B @ ( A @ path ) ) ) ),
inference(paramod_ordered,[status(thm)],[122,173]) ).
thf(203,plain,
! [B: $i,A: $i] :
( ( A != sk1 )
| ( B @ ( A @ ( sk2 @ shortest_path ) ) )
| ( sk2 @ ( A @ ( B @ sk14 ) ) @ ( A @ ( sk2 @ path ) ) )
| ~ ( B @ ( A @ ( sk2 @ path ) ) ) ),
inference(pattern_uni,[status(thm)],[202:[bind(A,$thf( sk2 ))]]) ).
thf(362,plain,
! [A: $i] :
( ( A @ ( sk1 @ ( sk2 @ shortest_path ) ) )
| ( sk2 @ ( sk1 @ ( A @ sk14 ) ) @ ( sk1 @ ( sk2 @ path ) ) )
| ~ ( A @ ( sk1 @ ( sk2 @ path ) ) ) ),
inference(simp,[status(thm)],[203]) ).
thf(456,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( C @ sk14 ) ) @ ( B @ ( A @ path ) ) )
!= ( D @ ( sk1 @ ( sk2 @ path ) ) ) )
| ( D @ ( sk1 @ ( sk2 @ shortest_path ) ) )
| ( sk2 @ ( sk1 @ ( D @ sk14 ) ) @ ( sk1 @ ( sk2 @ path ) ) )
| ~ $true
| ( C @ ( B @ ( A @ shortest_path ) ) )
| ~ ( C @ ( B @ ( A @ path ) ) )
| ( A = B ) ),
inference(paramod_ordered,[status(thm)],[122,362]) ).
thf(457,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( C @ sk14 ) ) @ ( B @ ( A @ path ) ) )
!= ( D @ ( sk1 @ ( sk2 @ path ) ) ) )
| ( D @ ( sk1 @ ( sk2 @ shortest_path ) ) )
| ( sk2 @ ( sk1 @ ( D @ sk14 ) ) @ ( sk1 @ ( sk2 @ path ) ) )
| ( C @ ( B @ ( A @ shortest_path ) ) )
| ~ ( C @ ( B @ ( A @ path ) ) )
| ( A = B ) ),
inference(simp,[status(thm)],[456]) ).
thf(458,plain,
! [A: $i] :
( ( sk2 @ ( sk1 @ ( A @ sk14 ) ) @ ( sk1 @ ( sk2 @ shortest_path ) ) )
| ( sk2 @ ( sk1 @ ( sk2 @ ( sk1 @ ( A @ sk14 ) ) @ sk14 ) ) @ ( sk1 @ ( sk2 @ path ) ) )
| ( A @ ( sk1 @ ( sk2 @ shortest_path ) ) )
| ~ ( A @ ( sk1 @ ( sk2 @ path ) ) )
| ( sk2 = sk1 ) ),
inference(pattern_uni,[status(thm)],[457:[bind(A,$thf( sk2 )),bind(B,$thf( sk1 )),bind(C,$thf( E )),bind(D,$thf( sk2 @ ( sk1 @ ( E @ sk14 ) ) ))]]) ).
thf(465,plain,
! [A: $i] :
( ( sk2 @ ( sk1 @ ( A @ sk14 ) ) @ ( sk1 @ ( sk2 @ shortest_path ) ) )
| ( sk2 @ ( sk1 @ ( sk2 @ ( sk1 @ ( A @ sk14 ) ) @ sk14 ) ) @ ( sk1 @ ( sk2 @ path ) ) )
| ( A @ ( sk1 @ ( sk2 @ shortest_path ) ) )
| ~ ( A @ ( sk1 @ ( sk2 @ path ) ) )
| ( sk2 = sk1 ) ),
inference(simp,[status(thm)],[458]) ).
thf(568,plain,
! [A: $i] :
( ( sk2 @ ( sk1 @ ( A @ sk14 ) ) @ ( sk1 @ ( sk2 @ shortest_path ) ) )
| ( sk2 @ ( sk1 @ ( sk2 @ ( sk1 @ ( A @ sk14 ) ) @ sk14 ) ) @ ( sk1 @ ( sk2 @ path ) ) )
| ( A @ ( sk1 @ ( sk2 @ shortest_path ) ) )
| ~ ( A @ ( sk1 @ ( sk2 @ path ) ) ) ),
inference(simplifyReflect,[status(thm)],[465,173]) ).
thf(590,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( sk1 @ ( sk2 @ ( sk1 @ ( A @ sk14 ) ) @ sk14 ) ) @ ( sk1 @ ( sk2 @ path ) ) )
!= ( D @ ( C @ ( B @ path ) ) ) )
| ( D @ ( C @ ( B @ shortest_path ) ) )
| ( B @ ( C @ ( D @ sk14 ) ) @ ( C @ ( B @ path ) ) )
| ~ $true
| ( B = C )
| ( sk2 @ ( sk1 @ ( A @ sk14 ) ) @ ( sk1 @ ( sk2 @ shortest_path ) ) )
| ( A @ ( sk1 @ ( sk2 @ shortest_path ) ) )
| ~ ( A @ ( sk1 @ ( sk2 @ path ) ) ) ),
inference(paramod_ordered,[status(thm)],[568,122]) ).
thf(591,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( sk1 @ ( sk2 @ ( sk1 @ ( A @ sk14 ) ) @ sk14 ) ) @ ( sk1 @ ( sk2 @ path ) ) )
!= ( D @ ( C @ ( B @ path ) ) ) )
| ( D @ ( C @ ( B @ shortest_path ) ) )
| ( B @ ( C @ ( D @ sk14 ) ) @ ( C @ ( B @ path ) ) )
| ( B = C )
| ( sk2 @ ( sk1 @ ( A @ sk14 ) ) @ ( sk1 @ ( sk2 @ shortest_path ) ) )
| ( A @ ( sk1 @ ( sk2 @ shortest_path ) ) )
| ~ ( A @ ( sk1 @ ( sk2 @ path ) ) ) ),
inference(simp,[status(thm)],[590]) ).
thf(592,plain,
! [A: $i] :
( ( sk2 @ ( sk1 @ ( sk2 @ ( sk1 @ ( A @ sk14 ) ) @ sk14 ) ) @ ( sk1 @ ( sk2 @ shortest_path ) ) )
| ( sk2 @ ( sk1 @ ( sk2 @ ( sk1 @ ( sk2 @ ( sk1 @ ( A @ sk14 ) ) @ sk14 ) ) @ sk14 ) ) @ ( sk1 @ ( sk2 @ path ) ) )
| ( sk2 = sk1 )
| ( sk2 @ ( sk1 @ ( A @ sk14 ) ) @ ( sk1 @ ( sk2 @ shortest_path ) ) )
| ( A @ ( sk1 @ ( sk2 @ shortest_path ) ) )
| ~ ( A @ ( sk1 @ ( sk2 @ path ) ) ) ),
inference(pattern_uni,[status(thm)],[591:[bind(A,$thf( H )),bind(B,$thf( sk2 )),bind(C,$thf( sk1 )),bind(D,$thf( sk2 @ ( sk1 @ ( sk2 @ ( sk1 @ ( H @ sk14 ) ) @ sk14 ) ) ))]]) ).
thf(641,plain,
! [A: $i] :
( ( sk2 @ ( sk1 @ ( sk2 @ ( sk1 @ ( A @ sk14 ) ) @ sk14 ) ) @ ( sk1 @ ( sk2 @ shortest_path ) ) )
| ( sk2 @ ( sk1 @ ( sk2 @ ( sk1 @ ( sk2 @ ( sk1 @ ( A @ sk14 ) ) @ sk14 ) ) @ sk14 ) ) @ ( sk1 @ ( sk2 @ path ) ) )
| ( sk2 = sk1 )
| ( sk2 @ ( sk1 @ ( A @ sk14 ) ) @ ( sk1 @ ( sk2 @ shortest_path ) ) )
| ( A @ ( sk1 @ ( sk2 @ shortest_path ) ) )
| ~ ( A @ ( sk1 @ ( sk2 @ path ) ) ) ),
inference(simp,[status(thm)],[592]) ).
thf(760,plain,
! [A: $i] :
( ( sk2 @ ( sk1 @ ( sk2 @ ( sk1 @ ( A @ sk14 ) ) @ sk14 ) ) @ ( sk1 @ ( sk2 @ shortest_path ) ) )
| ( sk2 @ ( sk1 @ ( sk2 @ ( sk1 @ ( sk2 @ ( sk1 @ ( A @ sk14 ) ) @ sk14 ) ) @ sk14 ) ) @ ( sk1 @ ( sk2 @ path ) ) )
| ( sk2 @ ( sk1 @ ( A @ sk14 ) ) @ ( sk1 @ ( sk2 @ shortest_path ) ) )
| ( A @ ( sk1 @ ( sk2 @ shortest_path ) ) )
| ~ ( A @ ( sk1 @ ( sk2 @ path ) ) ) ),
inference(simplifyReflect,[status(thm)],[641,173]) ).
thf(5,axiom,
! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ ( A @ path ) ) )
=> ( ( C @ length_of )
= ( C @ ( edges @ number_of_in ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',length_defn) ).
thf(34,plain,
! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ ( A @ path ) ) )
=> ( ( C @ length_of )
= ( C @ ( edges @ number_of_in ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).
thf(35,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ length_of )
= ( C @ ( edges @ number_of_in ) ) )
| ~ ( C @ ( B @ ( A @ path ) ) ) ),
inference(cnf,[status(esa)],[34]) ).
thf(36,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( C @ ( B @ ( A @ path ) ) )
| ( ( C @ ( edges @ number_of_in ) )
= ( C @ length_of ) ) ),
inference(lifteq,[status(thm)],[35]) ).
thf(4,axiom,
! [A: $i,B: $i] : ( graph @ ( A @ number_of_in ) @ ( B @ ( A @ number_of_in ) @ less_or_equal ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',graph_has_them_all) ).
thf(32,plain,
! [A: $i,B: $i] : ( graph @ ( A @ number_of_in ) @ ( B @ ( A @ number_of_in ) @ less_or_equal ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).
thf(33,plain,
! [B: $i,A: $i] : ( graph @ ( A @ number_of_in ) @ ( B @ ( A @ number_of_in ) @ less_or_equal ) ),
inference(cnf,[status(esa)],[32]) ).
thf(491,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( edges @ number_of_in ) )
!= ( E @ ( D @ number_of_in ) ) )
| ( graph @ ( D @ number_of_in ) @ ( C @ length_of @ less_or_equal ) )
| ~ ( C @ ( B @ ( A @ path ) ) ) ),
inference(paramod_ordered,[status(thm)],[36,33]) ).
thf(492,plain,
! [C: $i,B: $i,A: $i] :
( ( graph @ ( edges @ number_of_in ) @ ( C @ length_of @ less_or_equal ) )
| ~ ( C @ ( B @ ( A @ path ) ) ) ),
inference(pattern_uni,[status(thm)],[491:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( edges )),bind(E,$thf( C ))]]) ).
thf(1454,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ path ) ) )
!= ( C @ ( B @ ( A @ path ) ) ) )
| ( graph @ ( edges @ number_of_in ) @ ( C @ length_of @ less_or_equal ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1404,492]) ).
thf(1455,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ path ) ) )
!= ( C @ ( B @ ( A @ path ) ) ) )
| ( graph @ ( edges @ number_of_in ) @ ( C @ length_of @ less_or_equal ) ) ),
inference(simp,[status(thm)],[1454]) ).
thf(1456,plain,
graph @ ( edges @ number_of_in ) @ ( sk5 @ length_of @ less_or_equal ),
inference(pattern_uni,[status(thm)],[1455:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 )),bind(C,$thf( sk5 ))]]) ).
thf(1676,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( edges @ number_of_in ) )
!= ( graph @ ( edges @ number_of_in ) ) )
| ( C @ length_of @ ( sk5 @ length_of @ less_or_equal ) )
| ~ ( C @ ( B @ ( A @ path ) ) ) ),
inference(paramod_ordered,[status(thm)],[36,1456]) ).
thf(1677,plain,
! [B: $i,A: $i] :
( ( graph @ length_of @ ( sk5 @ length_of @ less_or_equal ) )
| ~ ( graph @ ( B @ ( A @ path ) ) ) ),
inference(pattern_uni,[status(thm)],[1676:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( graph ))]]) ).
thf(4907,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ path ) ) )
!= ( graph @ ( E @ ( D @ path ) ) ) )
| ( graph @ length_of @ ( sk5 @ length_of @ less_or_equal ) )
| ~ $true
| ~ ( C @ ( B @ ( A @ shortest_path ) ) ) ),
inference(paramod_ordered,[status(thm)],[115,1677]) ).
thf(4908,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ path ) ) )
!= ( graph @ ( E @ ( D @ path ) ) ) )
| ( graph @ length_of @ ( sk5 @ length_of @ less_or_equal ) )
| ~ ( C @ ( B @ ( A @ shortest_path ) ) ) ),
inference(simp,[status(thm)],[4907]) ).
thf(4909,plain,
! [B: $i,A: $i] :
( ( graph @ length_of @ ( sk5 @ length_of @ less_or_equal ) )
| ~ ( graph @ ( B @ ( A @ shortest_path ) ) ) ),
inference(pattern_uni,[status(thm)],[4908:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( graph )),bind(D,$thf( A )),bind(E,$thf( B ))]]) ).
thf(77,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( B @ ( C @ sk10 ) ) @ ( B @ ( A @ ( B @ ( C @ sk8 ) ) @ head_of @ path ) ) )
| ( A @ ( B @ ( C @ sk9 ) ) )
| ~ ( C @ ( B @ ( A @ path ) ) ) ),
inference(cnfConj,[status(thm)],[67]) ).
thf(3846,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ path ) ) )
!= ( C @ ( B @ ( A @ path ) ) ) )
| ( A @ ( B @ ( C @ sk10 ) ) @ ( B @ ( A @ ( B @ ( C @ sk8 ) ) @ head_of @ path ) ) )
| ( A @ ( B @ ( C @ sk9 ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1404,77]) ).
thf(3847,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ path ) ) )
!= ( C @ ( B @ ( A @ path ) ) ) )
| ( A @ ( B @ ( C @ sk10 ) ) @ ( B @ ( A @ ( B @ ( C @ sk8 ) ) @ head_of @ path ) ) )
| ( A @ ( B @ ( C @ sk9 ) ) ) ),
inference(simp,[status(thm)],[3846]) ).
thf(3848,plain,
( ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ ( sk2 @ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of @ path ) ) )
| ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) ),
inference(pattern_uni,[status(thm)],[3847:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 )),bind(C,$thf( sk5 ))]]) ).
thf(5760,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ ( sk2 @ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of @ path ) ) )
!= ( C @ ( B @ ( A @ path ) ) ) )
| ( graph @ ( edges @ number_of_in ) @ ( C @ length_of @ less_or_equal ) )
| ~ $true
| ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) ),
inference(paramod_ordered,[status(thm)],[3848,492]) ).
thf(5761,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ ( sk2 @ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of @ path ) ) )
!= ( C @ ( B @ ( A @ path ) ) ) )
| ( graph @ ( edges @ number_of_in ) @ ( C @ length_of @ less_or_equal ) )
| ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) ),
inference(simp,[status(thm)],[5760]) ).
thf(5762,plain,
( ( graph @ ( edges @ number_of_in ) @ ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ length_of @ less_or_equal ) )
| ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) ),
inference(pattern_uni,[status(thm)],[5761:[bind(A,$thf( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of )),bind(B,$thf( sk2 )),bind(C,$thf( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) ))]]) ).
thf(75,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( A @ ( B @ ( C @ sk9 ) ) )
| ( C
= ( empty @ ( A @ ( B @ ( C @ sk8 ) ) @ path_cons ) ) )
| ~ ( C @ ( B @ ( A @ path ) ) ) ),
inference(cnfConj,[status(thm)],[67]) ).
thf(82,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( A @ ( B @ ( C @ sk9 ) ) )
| ~ ( C @ ( B @ ( A @ path ) ) )
| ( ( empty @ ( A @ ( B @ ( C @ sk8 ) ) @ path_cons ) )
= C ) ),
inference(lifteq,[status(thm)],[75]) ).
thf(5906,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ path ) ) )
!= ( C @ ( B @ ( A @ path ) ) ) )
| ~ ( A @ ( B @ ( C @ sk9 ) ) )
| ~ $true
| ( ( empty @ ( A @ ( B @ ( C @ sk8 ) ) @ path_cons ) )
= C ) ),
inference(paramod_ordered,[status(thm)],[1404,82]) ).
thf(5907,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ path ) ) )
!= ( C @ ( B @ ( A @ path ) ) ) )
| ~ ( A @ ( B @ ( C @ sk9 ) ) )
| ( ( empty @ ( A @ ( B @ ( C @ sk8 ) ) @ path_cons ) )
= C ) ),
inference(simp,[status(thm)],[5906]) ).
thf(5908,plain,
( ~ ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) )
| ( ( empty @ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ path_cons ) )
= sk5 ) ),
inference(pattern_uni,[status(thm)],[5907:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 )),bind(C,$thf( sk5 ))]]) ).
thf(6072,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) )
!= ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) )
| ~ $true
| ( ( empty @ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ path_cons ) )
= sk5 )
| ( graph @ ( edges @ number_of_in ) @ ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ length_of @ less_or_equal ) ) ),
inference(paramod_ordered,[status(thm)],[5762,5908]) ).
thf(6073,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) )
!= ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) )
| ( ( empty @ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ path_cons ) )
= sk5 )
| ( graph @ ( edges @ number_of_in ) @ ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ length_of @ less_or_equal ) ) ),
inference(simp,[status(thm)],[6072]) ).
thf(6074,plain,
( ( ( empty @ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ path_cons ) )
= sk5 )
| ( graph @ ( edges @ number_of_in ) @ ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ length_of @ less_or_equal ) ) ),
inference(pattern_uni,[status(thm)],[6073:[]]) ).
thf(26,plain,
sk5 @ ( sk4 @ ( sk3 @ precedes ) ),
inference(cnfConj,[status(thm)],[23]) ).
thf(8,axiom,
! [A: $i,B: $i,C: $i,D: $i,E: $i] :
( ( ( E @ ( D @ ( C @ precedes ) ) )
& ( E @ ( B @ ( A @ shortest_path ) ) ) )
=> ( ~ ( E @ ( C @ ( D @ precedes ) ) )
& ~ ? [F: $i] :
( ( ( F @ head_of )
= ( D @ head_of ) )
& ( ( F @ tail_of )
= ( C @ tail_of ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',shortest_path_properties) ).
thf(61,plain,
! [A: $i,B: $i,C: $i,D: $i,E: $i] :
( ( ( E @ ( D @ ( C @ precedes ) ) )
& ( E @ ( B @ ( A @ shortest_path ) ) ) )
=> ( ~ ( E @ ( C @ ( D @ precedes ) ) )
& ~ ? [F: $i] :
( ( ( F @ head_of )
= ( D @ head_of ) )
& ( ( F @ tail_of )
= ( C @ tail_of ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[8]) ).
thf(62,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ~ ( E @ ( C @ ( D @ precedes ) ) )
| ~ ( E @ ( D @ ( C @ precedes ) ) )
| ~ ( E @ ( B @ ( A @ shortest_path ) ) ) )
& ( ( ( F @ head_of )
!= ( D @ head_of ) )
| ( ( F @ tail_of )
!= ( C @ tail_of ) )
| ~ ( E @ ( D @ ( C @ precedes ) ) )
| ~ ( E @ ( B @ ( A @ shortest_path ) ) ) ) ),
inference(cnf,[status(esa)],[61]) ).
thf(64,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ~ ( E @ ( C @ ( D @ precedes ) ) )
| ~ ( E @ ( D @ ( C @ precedes ) ) )
| ~ ( E @ ( B @ ( A @ shortest_path ) ) ) ),
inference(cnfConj,[status(thm)],[62]) ).
thf(527,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( sk5 @ ( sk4 @ ( sk3 @ precedes ) ) )
!= ( E @ ( D @ ( C @ precedes ) ) ) )
| ~ ( E @ ( C @ ( D @ precedes ) ) )
| ~ $true
| ~ ( E @ ( B @ ( A @ shortest_path ) ) ) ),
inference(paramod_ordered,[status(thm)],[26,64]) ).
thf(528,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( sk5 @ ( sk4 @ ( sk3 @ precedes ) ) )
!= ( E @ ( D @ ( C @ precedes ) ) ) )
| ~ ( E @ ( C @ ( D @ precedes ) ) )
| ~ ( E @ ( B @ ( A @ shortest_path ) ) ) ),
inference(simp,[status(thm)],[527]) ).
thf(529,plain,
! [B: $i,A: $i] :
( ~ ( sk5 @ ( sk3 @ ( sk4 @ precedes ) ) )
| ~ ( sk5 @ ( B @ ( A @ shortest_path ) ) ) ),
inference(pattern_uni,[status(thm)],[528:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( sk3 )),bind(D,$thf( sk4 )),bind(E,$thf( sk5 ))]]) ).
thf(553,plain,
! [B: $i,A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ shortest_path ) ) )
!= ( sk5 @ ( B @ ( A @ shortest_path ) ) ) )
| ~ ( sk5 @ ( sk3 @ ( sk4 @ precedes ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[25,529]) ).
thf(554,plain,
! [B: $i,A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ shortest_path ) ) )
!= ( sk5 @ ( B @ ( A @ shortest_path ) ) ) )
| ~ ( sk5 @ ( sk3 @ ( sk4 @ precedes ) ) ) ),
inference(simp,[status(thm)],[553]) ).
thf(555,plain,
~ ( sk5 @ ( sk3 @ ( sk4 @ precedes ) ) ),
inference(pattern_uni,[status(thm)],[554:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 ))]]) ).
thf(677,plain,
( ( ( sk5 @ ( sk3 @ ( sk4 @ precedes ) ) )
!= ( sk5 @ ( sk4 @ ( sk3 @ precedes ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[26,555]) ).
thf(678,plain,
( ( sk5 @ ( sk3 @ ( sk4 @ precedes ) ) )
!= ( sk5 @ ( sk4 @ ( sk3 @ precedes ) ) ) ),
inference(simp,[status(thm)],[677]) ).
thf(679,plain,
( ( sk5 != sk5 )
| ( sk4 != sk3 )
| ( sk4 != sk3 ) ),
inference(simp,[status(thm)],[678]) ).
thf(683,plain,
sk4 != sk3,
inference(simp,[status(thm)],[679]) ).
thf(6,axiom,
! [A: $i,B: $i,C: $i] :
( ( ! [D: $i,E: $i] :
( ( ( E @ ( D @ sequential ) )
& ( A @ ( E @ on_path ) )
& ( A @ ( D @ on_path ) ) )
=> ? [F: $i] : ( F @ ( E @ ( D @ triangle ) ) ) )
& ( A @ ( C @ ( B @ path ) ) ) )
=> ( ( A @ ( sequential_pairs @ number_of_in ) )
= ( A @ ( triangles @ number_of_in ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sequential_pairs_and_triangles) ).
thf(37,plain,
! [A: $i,B: $i,C: $i] :
( ( ! [D: $i,E: $i] :
( ( ( E @ ( D @ sequential ) )
& ( A @ ( E @ on_path ) )
& ( A @ ( D @ on_path ) ) )
=> ? [F: $i] : ( F @ ( E @ ( D @ triangle ) ) ) )
& ( A @ ( C @ ( B @ path ) ) ) )
=> ( ( A @ ( sequential_pairs @ number_of_in ) )
= ( A @ ( triangles @ number_of_in ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[6]) ).
thf(38,plain,
! [A: $i] :
( ( ! [B: $i,C: $i] :
( ( ( C @ ( B @ sequential ) )
& ( A @ ( C @ on_path ) )
& ( A @ ( B @ on_path ) ) )
=> ? [D: $i] : ( D @ ( C @ ( B @ triangle ) ) ) )
& ? [B: $i,C: $i] : ( A @ ( C @ ( B @ path ) ) ) )
=> ( ( A @ ( sequential_pairs @ number_of_in ) )
= ( A @ ( triangles @ number_of_in ) ) ) ),
inference(miniscope,[status(thm)],[37]) ).
thf(39,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( ( A @ ( sequential_pairs @ number_of_in ) )
= ( A @ ( triangles @ number_of_in ) ) )
| ~ ( D @ ( A @ sk7 @ ( A @ sk6 @ triangle ) ) )
| ~ ( A @ ( C @ ( B @ path ) ) ) )
& ( ( ( A @ ( sequential_pairs @ number_of_in ) )
= ( A @ ( triangles @ number_of_in ) ) )
| ( A @ sk7 @ ( A @ sk6 @ sequential ) )
| ~ ( A @ ( C @ ( B @ path ) ) ) )
& ( ( ( A @ ( sequential_pairs @ number_of_in ) )
= ( A @ ( triangles @ number_of_in ) ) )
| ( A @ ( A @ sk7 @ on_path ) )
| ~ ( A @ ( C @ ( B @ path ) ) ) )
& ( ( ( A @ ( sequential_pairs @ number_of_in ) )
= ( A @ ( triangles @ number_of_in ) ) )
| ( A @ ( A @ sk6 @ on_path ) )
| ~ ( A @ ( C @ ( B @ path ) ) ) ) ),
inference(cnf,[status(esa)],[38]) ).
thf(42,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( sequential_pairs @ number_of_in ) )
= ( A @ ( triangles @ number_of_in ) ) )
| ( A @ sk7 @ ( A @ sk6 @ sequential ) )
| ~ ( A @ ( C @ ( B @ path ) ) ) ),
inference(cnfConj,[status(thm)],[39]) ).
thf(46,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ sk7 @ ( A @ sk6 @ sequential ) )
| ~ ( A @ ( C @ ( B @ path ) ) )
| ( ( A @ ( triangles @ number_of_in ) )
= ( A @ ( sequential_pairs @ number_of_in ) ) ) ),
inference(lifteq,[status(thm)],[42]) ).
thf(1418,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ path ) ) )
!= ( A @ ( C @ ( B @ path ) ) ) )
| ( A @ sk7 @ ( A @ sk6 @ sequential ) )
| ~ $true
| ( ( A @ ( triangles @ number_of_in ) )
= ( A @ ( sequential_pairs @ number_of_in ) ) ) ),
inference(paramod_ordered,[status(thm)],[1404,46]) ).
thf(1419,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ path ) ) )
!= ( A @ ( C @ ( B @ path ) ) ) )
| ( A @ sk7 @ ( A @ sk6 @ sequential ) )
| ( ( A @ ( triangles @ number_of_in ) )
= ( A @ ( sequential_pairs @ number_of_in ) ) ) ),
inference(simp,[status(thm)],[1418]) ).
thf(1420,plain,
( ( sk5 @ sk7 @ ( sk5 @ sk6 @ sequential ) )
| ( ( sk5 @ ( triangles @ number_of_in ) )
= ( sk5 @ ( sequential_pairs @ number_of_in ) ) ) ),
inference(pattern_uni,[status(thm)],[1419:[bind(A,$thf( sk5 )),bind(B,$thf( sk1 )),bind(C,$thf( sk2 ))]]) ).
thf(2229,plain,
! [B: $i,A: $i] :
( ( ( sk5 @ sk7 @ ( sk5 @ sk6 @ sequential ) )
!= ( B @ ( A @ sequential ) ) )
| ~ $true
| ( ( A @ head_of )
= ( B @ tail_of ) )
| ( ( sk5 @ ( triangles @ number_of_in ) )
= ( sk5 @ ( sequential_pairs @ number_of_in ) ) ) ),
inference(paramod_ordered,[status(thm)],[1420,56]) ).
thf(2230,plain,
! [B: $i,A: $i] :
( ( ( sk5 @ sk7 @ ( sk5 @ sk6 @ sequential ) )
!= ( B @ ( A @ sequential ) ) )
| ( ( A @ head_of )
= ( B @ tail_of ) )
| ( ( sk5 @ ( triangles @ number_of_in ) )
= ( sk5 @ ( sequential_pairs @ number_of_in ) ) ) ),
inference(simp,[status(thm)],[2229]) ).
thf(2231,plain,
( ( ( sk5 @ sk6 @ head_of )
= ( sk5 @ sk7 @ tail_of ) )
| ( ( sk5 @ ( triangles @ number_of_in ) )
= ( sk5 @ ( sequential_pairs @ number_of_in ) ) ) ),
inference(pattern_uni,[status(thm)],[2230:[bind(A,$thf( sk5 @ sk6 )),bind(B,$thf( sk5 @ sk7 ))]]) ).
thf(41,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( sequential_pairs @ number_of_in ) )
= ( A @ ( triangles @ number_of_in ) ) )
| ( A @ ( A @ sk7 @ on_path ) )
| ~ ( A @ ( C @ ( B @ path ) ) ) ),
inference(cnfConj,[status(thm)],[39]) ).
thf(45,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( A @ sk7 @ on_path ) )
| ~ ( A @ ( C @ ( B @ path ) ) )
| ( ( A @ ( triangles @ number_of_in ) )
= ( A @ ( sequential_pairs @ number_of_in ) ) ) ),
inference(lifteq,[status(thm)],[41]) ).
thf(1459,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ path ) ) )
!= ( A @ ( C @ ( B @ path ) ) ) )
| ( A @ ( A @ sk7 @ on_path ) )
| ~ $true
| ( ( A @ ( triangles @ number_of_in ) )
= ( A @ ( sequential_pairs @ number_of_in ) ) ) ),
inference(paramod_ordered,[status(thm)],[1404,45]) ).
thf(1460,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ path ) ) )
!= ( A @ ( C @ ( B @ path ) ) ) )
| ( A @ ( A @ sk7 @ on_path ) )
| ( ( A @ ( triangles @ number_of_in ) )
= ( A @ ( sequential_pairs @ number_of_in ) ) ) ),
inference(simp,[status(thm)],[1459]) ).
thf(1461,plain,
( ( sk5 @ ( sk5 @ sk7 @ on_path ) )
| ( ( sk5 @ ( triangles @ number_of_in ) )
= ( sk5 @ ( sequential_pairs @ number_of_in ) ) ) ),
inference(pattern_uni,[status(thm)],[1460:[bind(A,$thf( sk5 )),bind(B,$thf( sk1 )),bind(C,$thf( sk2 ))]]) ).
thf(1432,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ path ) ) )
!= ( C @ ( B @ ( A @ path ) ) ) )
| ~ $true
| ( ( C @ ( edges @ number_of_in ) )
= ( C @ length_of ) ) ),
inference(paramod_ordered,[status(thm)],[1404,36]) ).
thf(1433,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ path ) ) )
!= ( C @ ( B @ ( A @ path ) ) ) )
| ( ( C @ ( edges @ number_of_in ) )
= ( C @ length_of ) ) ),
inference(simp,[status(thm)],[1432]) ).
thf(1434,plain,
( ( sk5 @ ( edges @ number_of_in ) )
= ( sk5 @ length_of ) ),
inference(pattern_uni,[status(thm)],[1433:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 )),bind(C,$thf( sk5 ))]]) ).
thf(2083,plain,
( ( ( sk5 @ ( triangles @ number_of_in ) )
!= ( sk5 @ ( edges @ number_of_in ) ) )
| ( ( sk5 @ ( sequential_pairs @ number_of_in ) )
= ( sk5 @ length_of ) )
| ( sk5 @ ( sk5 @ sk7 @ on_path ) ) ),
inference(paramod_ordered,[status(thm)],[1461,1434]) ).
thf(2098,plain,
( ( sk5 != sk5 )
| ( triangles != edges )
| ( ( sk5 @ ( sequential_pairs @ number_of_in ) )
= ( sk5 @ length_of ) )
| ( sk5 @ ( sk5 @ sk7 @ on_path ) ) ),
inference(simp,[status(thm)],[2083]) ).
thf(2114,plain,
( ( triangles != edges )
| ( ( sk5 @ ( sequential_pairs @ number_of_in ) )
= ( sk5 @ length_of ) )
| ( sk5 @ ( sk5 @ sk7 @ on_path ) ) ),
inference(simp,[status(thm)],[2098]) ).
thf(3,axiom,
! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ ( A @ path ) ) )
=> ( ( C @ ( sequential_pairs @ number_of_in ) )
= ( n1 @ ( C @ length_of @ minus ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',path_length_sequential_pairs) ).
thf(29,plain,
! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ ( A @ path ) ) )
=> ( ( C @ ( sequential_pairs @ number_of_in ) )
= ( n1 @ ( C @ length_of @ minus ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(30,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( sequential_pairs @ number_of_in ) )
= ( n1 @ ( C @ length_of @ minus ) ) )
| ~ ( C @ ( B @ ( A @ path ) ) ) ),
inference(cnf,[status(esa)],[29]) ).
thf(31,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( C @ ( B @ ( A @ path ) ) )
| ( ( n1 @ ( C @ length_of @ minus ) )
= ( C @ ( sequential_pairs @ number_of_in ) ) ) ),
inference(lifteq,[status(thm)],[30]) ).
thf(5682,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ ( sk2 @ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of @ path ) ) )
!= ( C @ ( B @ ( A @ path ) ) ) )
| ~ $true
| ( ( n1 @ ( C @ length_of @ minus ) )
= ( C @ ( sequential_pairs @ number_of_in ) ) )
| ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) ),
inference(paramod_ordered,[status(thm)],[3848,31]) ).
thf(5683,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ ( sk2 @ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of @ path ) ) )
!= ( C @ ( B @ ( A @ path ) ) ) )
| ( ( n1 @ ( C @ length_of @ minus ) )
= ( C @ ( sequential_pairs @ number_of_in ) ) )
| ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) ),
inference(simp,[status(thm)],[5682]) ).
thf(5684,plain,
( ( ( n1 @ ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ length_of @ minus ) )
= ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ ( sequential_pairs @ number_of_in ) ) )
| ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) ),
inference(pattern_uni,[status(thm)],[5683:[bind(A,$thf( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of )),bind(B,$thf( sk2 )),bind(C,$thf( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) ))]]) ).
thf(68,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( A @ ( B @ ( C @ sk9 ) ) )
| ( B
= ( A @ ( B @ ( C @ sk8 ) ) @ head_of ) )
| ~ ( C @ ( B @ ( A @ path ) ) ) ),
inference(cnfConj,[status(thm)],[67]) ).
thf(83,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( A @ ( B @ ( C @ sk9 ) ) )
| ~ ( C @ ( B @ ( A @ path ) ) )
| ( ( A @ ( B @ ( C @ sk8 ) ) @ head_of )
= B ) ),
inference(lifteq,[status(thm)],[68]) ).
thf(6608,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ path ) ) )
!= ( C @ ( B @ ( A @ path ) ) ) )
| ~ ( A @ ( B @ ( C @ sk9 ) ) )
| ~ $true
| ( ( A @ ( B @ ( C @ sk8 ) ) @ head_of )
= B ) ),
inference(paramod_ordered,[status(thm)],[1404,83]) ).
thf(6609,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ path ) ) )
!= ( C @ ( B @ ( A @ path ) ) ) )
| ~ ( A @ ( B @ ( C @ sk9 ) ) )
| ( ( A @ ( B @ ( C @ sk8 ) ) @ head_of )
= B ) ),
inference(simp,[status(thm)],[6608]) ).
thf(6610,plain,
( ~ ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) )
| ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of )
= sk2 ) ),
inference(pattern_uni,[status(thm)],[6609:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 )),bind(C,$thf( sk5 ))]]) ).
thf(9001,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) )
!= ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) )
| ~ $true
| ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of )
= sk2 )
| ( ( n1 @ ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ length_of @ minus ) )
= ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ ( sequential_pairs @ number_of_in ) ) ) ),
inference(paramod_ordered,[status(thm)],[5684,6610]) ).
thf(9002,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) )
!= ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) )
| ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of )
= sk2 )
| ( ( n1 @ ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ length_of @ minus ) )
= ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ ( sequential_pairs @ number_of_in ) ) ) ),
inference(simp,[status(thm)],[9001]) ).
thf(9003,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of )
= sk2 )
| ( ( n1 @ ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ length_of @ minus ) )
= ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ ( sequential_pairs @ number_of_in ) ) ) ),
inference(pattern_uni,[status(thm)],[9002:[]]) ).
thf(40,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( sequential_pairs @ number_of_in ) )
= ( A @ ( triangles @ number_of_in ) ) )
| ( A @ ( A @ sk6 @ on_path ) )
| ~ ( A @ ( C @ ( B @ path ) ) ) ),
inference(cnfConj,[status(thm)],[39]) ).
thf(44,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( A @ sk6 @ on_path ) )
| ~ ( A @ ( C @ ( B @ path ) ) )
| ( ( A @ ( triangles @ number_of_in ) )
= ( A @ ( sequential_pairs @ number_of_in ) ) ) ),
inference(lifteq,[status(thm)],[40]) ).
thf(1424,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ path ) ) )
!= ( A @ ( C @ ( B @ path ) ) ) )
| ( A @ ( A @ sk6 @ on_path ) )
| ~ $true
| ( ( A @ ( triangles @ number_of_in ) )
= ( A @ ( sequential_pairs @ number_of_in ) ) ) ),
inference(paramod_ordered,[status(thm)],[1404,44]) ).
thf(1425,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ path ) ) )
!= ( A @ ( C @ ( B @ path ) ) ) )
| ( A @ ( A @ sk6 @ on_path ) )
| ( ( A @ ( triangles @ number_of_in ) )
= ( A @ ( sequential_pairs @ number_of_in ) ) ) ),
inference(simp,[status(thm)],[1424]) ).
thf(1426,plain,
( ( sk5 @ ( sk5 @ sk6 @ on_path ) )
| ( ( sk5 @ ( triangles @ number_of_in ) )
= ( sk5 @ ( sequential_pairs @ number_of_in ) ) ) ),
inference(pattern_uni,[status(thm)],[1425:[bind(A,$thf( sk5 )),bind(B,$thf( sk1 )),bind(C,$thf( sk2 ))]]) ).
thf(493,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( edges @ number_of_in ) )
!= ( graph @ ( D @ number_of_in ) ) )
| ( C @ length_of @ ( E @ ( D @ number_of_in ) @ less_or_equal ) )
| ~ ( C @ ( B @ ( A @ path ) ) ) ),
inference(paramod_ordered,[status(thm)],[36,33]) ).
thf(494,plain,
! [C: $i,B: $i,A: $i] :
( ( graph @ length_of @ ( C @ ( edges @ number_of_in ) @ less_or_equal ) )
| ~ ( graph @ ( B @ ( A @ path ) ) ) ),
inference(pattern_uni,[status(thm)],[493:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( graph )),bind(D,$thf( edges ))]]) ).
thf(500,plain,
! [C: $i,B: $i,A: $i] :
( ( graph @ length_of @ ( C @ ( edges @ number_of_in ) @ less_or_equal ) )
| ~ ( graph @ ( B @ ( A @ path ) ) ) ),
inference(simp,[status(thm)],[494]) ).
thf(1871,plain,
! [B: $i,A: $i] :
( ( ( sk5 @ ( triangles @ number_of_in ) )
!= ( B @ ( A @ number_of_in ) ) )
| ( graph @ ( A @ number_of_in ) @ ( sk5 @ ( sequential_pairs @ number_of_in ) @ less_or_equal ) )
| ( sk5 @ ( sk5 @ sk6 @ on_path ) ) ),
inference(paramod_ordered,[status(thm)],[1426,33]) ).
thf(1872,plain,
( ( graph @ ( triangles @ number_of_in ) @ ( sk5 @ ( sequential_pairs @ number_of_in ) @ less_or_equal ) )
| ( sk5 @ ( sk5 @ sk6 @ on_path ) ) ),
inference(pattern_uni,[status(thm)],[1871:[bind(A,$thf( triangles )),bind(B,$thf( sk5 ))]]) ).
thf(5763,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ ( sk2 @ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of @ path ) ) )
!= ( C @ ( B @ ( A @ path ) ) ) )
| ( A @ ( B @ ( C @ sk8 ) ) @ edge )
| ~ $true
| ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) ),
inference(paramod_ordered,[status(thm)],[3848,70]) ).
thf(5764,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ ( sk2 @ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of @ path ) ) )
!= ( C @ ( B @ ( A @ path ) ) ) )
| ( A @ ( B @ ( C @ sk8 ) ) @ edge )
| ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) ),
inference(simp,[status(thm)],[5763]) ).
thf(5765,plain,
( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of @ ( sk2 @ ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ sk8 ) ) @ edge )
| ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) ),
inference(pattern_uni,[status(thm)],[5764:[bind(A,$thf( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of )),bind(B,$thf( sk2 )),bind(C,$thf( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) ))]]) ).
thf(19,axiom,
! [A: $i] :
( ( A @ edge )
=> ( ( A @ tail_of @ vertex )
& ( A @ head_of @ vertex ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',edge_ends_are_vertices) ).
thf(155,plain,
! [A: $i] :
( ( A @ edge )
=> ( ( A @ tail_of @ vertex )
& ( A @ head_of @ vertex ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[19]) ).
thf(156,plain,
! [A: $i] :
( ( ( A @ tail_of @ vertex )
| ~ ( A @ edge ) )
& ( ( A @ head_of @ vertex )
| ~ ( A @ edge ) ) ),
inference(cnf,[status(esa)],[155]) ).
thf(157,plain,
! [A: $i] :
( ( A @ head_of @ vertex )
| ~ ( A @ edge ) ),
inference(cnfConj,[status(thm)],[156]) ).
thf(7603,plain,
! [A: $i] :
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of @ ( sk2 @ ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ sk8 ) ) @ edge )
!= ( A @ edge ) )
| ( A @ head_of @ vertex )
| ~ $true
| ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) ),
inference(paramod_ordered,[status(thm)],[5765,157]) ).
thf(7604,plain,
! [A: $i] :
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of @ ( sk2 @ ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ sk8 ) ) @ edge )
!= ( A @ edge ) )
| ( A @ head_of @ vertex )
| ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) ),
inference(simp,[status(thm)],[7603]) ).
thf(7605,plain,
( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of @ ( sk2 @ ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ sk8 ) ) @ head_of @ vertex )
| ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) ),
inference(pattern_uni,[status(thm)],[7604:[bind(A,$thf( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of @ ( sk2 @ ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ sk8 ) ) ))]]) ).
thf(55,plain,
! [B: $i,A: $i] :
( ( B @ edge )
| ~ ( B @ ( A @ sequential ) ) ),
inference(cnfConj,[status(thm)],[50]) ).
thf(2252,plain,
! [B: $i,A: $i] :
( ( ( sk5 @ sk7 @ ( sk5 @ sk6 @ sequential ) )
!= ( B @ ( A @ sequential ) ) )
| ( B @ edge )
| ~ $true
| ( ( sk5 @ ( triangles @ number_of_in ) )
= ( sk5 @ ( sequential_pairs @ number_of_in ) ) ) ),
inference(paramod_ordered,[status(thm)],[1420,55]) ).
thf(2253,plain,
! [B: $i,A: $i] :
( ( ( sk5 @ sk7 @ ( sk5 @ sk6 @ sequential ) )
!= ( B @ ( A @ sequential ) ) )
| ( B @ edge )
| ( ( sk5 @ ( triangles @ number_of_in ) )
= ( sk5 @ ( sequential_pairs @ number_of_in ) ) ) ),
inference(simp,[status(thm)],[2252]) ).
thf(2254,plain,
( ( sk5 @ sk7 @ edge )
| ( ( sk5 @ ( triangles @ number_of_in ) )
= ( sk5 @ ( sequential_pairs @ number_of_in ) ) ) ),
inference(pattern_uni,[status(thm)],[2253:[bind(A,$thf( sk5 @ sk6 )),bind(B,$thf( sk5 @ sk7 ))]]) ).
thf(2431,plain,
! [B: $i,A: $i] :
( ( ( sk5 @ ( triangles @ number_of_in ) )
!= ( B @ ( A @ number_of_in ) ) )
| ( graph @ ( A @ number_of_in ) @ ( sk5 @ ( sequential_pairs @ number_of_in ) @ less_or_equal ) )
| ( sk5 @ sk7 @ edge ) ),
inference(paramod_ordered,[status(thm)],[2254,33]) ).
thf(2432,plain,
( ( graph @ ( triangles @ number_of_in ) @ ( sk5 @ ( sequential_pairs @ number_of_in ) @ less_or_equal ) )
| ( sk5 @ sk7 @ edge ) ),
inference(pattern_uni,[status(thm)],[2431:[bind(A,$thf( triangles )),bind(B,$thf( sk5 ))]]) ).
thf(24,plain,
complete,
inference(cnfConj,[status(thm)],[23]) ).
thf(63,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( F @ head_of )
!= ( D @ head_of ) )
| ( ( F @ tail_of )
!= ( C @ tail_of ) )
| ~ ( E @ ( D @ ( C @ precedes ) ) )
| ~ ( E @ ( B @ ( A @ shortest_path ) ) ) ),
inference(cnfConj,[status(thm)],[62]) ).
thf(65,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ~ ( E @ ( D @ ( C @ precedes ) ) )
| ~ ( E @ ( B @ ( A @ shortest_path ) ) )
| ( ( F @ head_of )
!= ( D @ head_of ) )
| ( ( F @ tail_of )
!= ( C @ tail_of ) ) ),
inference(lifteq,[status(thm)],[63]) ).
thf(2725,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( sk5 @ ( sk4 @ ( sk3 @ precedes ) ) )
!= ( E @ ( D @ ( C @ precedes ) ) ) )
| ~ $true
| ~ ( E @ ( B @ ( A @ shortest_path ) ) )
| ( ( F @ head_of )
!= ( D @ head_of ) )
| ( ( F @ tail_of )
!= ( C @ tail_of ) ) ),
inference(paramod_ordered,[status(thm)],[26,65]) ).
thf(2726,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( sk5 @ ( sk4 @ ( sk3 @ precedes ) ) )
!= ( E @ ( D @ ( C @ precedes ) ) ) )
| ~ ( E @ ( B @ ( A @ shortest_path ) ) )
| ( ( F @ head_of )
!= ( D @ head_of ) )
| ( ( F @ tail_of )
!= ( C @ tail_of ) ) ),
inference(simp,[status(thm)],[2725]) ).
thf(2727,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( sk5 @ ( B @ ( A @ shortest_path ) ) )
| ( ( C @ head_of )
!= ( sk4 @ head_of ) )
| ( ( C @ tail_of )
!= ( sk3 @ tail_of ) ) ),
inference(pattern_uni,[status(thm)],[2726:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( sk3 )),bind(D,$thf( sk4 )),bind(E,$thf( sk5 ))]]) ).
thf(2732,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( sk5 @ ( B @ ( A @ shortest_path ) ) )
| ( ( C @ head_of )
!= ( sk4 @ head_of ) )
| ( ( C @ tail_of )
!= ( sk3 @ tail_of ) ) ),
inference(simp,[status(thm)],[2727]) ).
thf(3010,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( sk5 @ ( B @ ( A @ shortest_path ) ) )
| ( ( C @ head_of )
!= ( sk4 @ head_of ) )
| ( C != sk3 ) ),
inference(simp,[status(thm)],[2732]) ).
thf(3052,plain,
! [B: $i,A: $i] :
( ~ ( sk5 @ ( B @ ( A @ shortest_path ) ) )
| ( ( sk4 @ head_of )
!= ( sk3 @ head_of ) ) ),
inference(simp,[status(thm)],[3010]) ).
thf(3897,plain,
! [B: $i,A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ shortest_path ) ) )
!= ( sk5 @ ( B @ ( A @ shortest_path ) ) ) )
| ~ $true
| ( ( sk4 @ head_of )
!= ( sk3 @ head_of ) ) ),
inference(paramod_ordered,[status(thm)],[25,3052]) ).
thf(3898,plain,
! [B: $i,A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ shortest_path ) ) )
!= ( sk5 @ ( B @ ( A @ shortest_path ) ) ) )
| ( ( sk4 @ head_of )
!= ( sk3 @ head_of ) ) ),
inference(simp,[status(thm)],[3897]) ).
thf(3899,plain,
( ( sk4 @ head_of )
!= ( sk3 @ head_of ) ),
inference(pattern_uni,[status(thm)],[3898:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 ))]]) ).
thf(3928,plain,
! [B: $i,A: $i] :
( ( ( A @ head_of )
!= ( sk4 @ head_of ) )
| ( ( B @ tail_of )
!= ( sk3 @ head_of ) )
| ~ ( B @ ( A @ sequential ) ) ),
inference(paramod_ordered,[status(thm)],[56,3899]) ).
thf(3929,plain,
! [A: $i] :
( ( ( A @ tail_of )
!= ( sk3 @ head_of ) )
| ~ ( A @ ( sk4 @ sequential ) ) ),
inference(pattern_uni,[status(thm)],[3928:[bind(A,$thf( sk4 ))]]) ).
thf(3934,plain,
! [A: $i] :
( ( ( A @ tail_of )
!= ( sk3 @ head_of ) )
| ~ ( A @ ( sk4 @ sequential ) ) ),
inference(simp,[status(thm)],[3929]) ).
thf(4136,plain,
! [A: $i] :
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ tail_of )
!= ( A @ tail_of ) )
| ( ( sk3 @ head_of )
!= sk1 )
| ~ ( A @ ( sk4 @ sequential ) ) ),
inference(paramod_ordered,[status(thm)],[4048,3934]) ).
thf(4137,plain,
( ( ( sk3 @ head_of )
!= sk1 )
| ~ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ ( sk4 @ sequential ) ) ),
inference(pattern_uni,[status(thm)],[4136:[bind(A,$thf( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) ))]]) ).
thf(7626,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) )
!= ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) )
| ~ $true
| ( ( empty @ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ path_cons ) )
= sk5 )
| ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of @ ( sk2 @ ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ sk8 ) ) @ edge ) ),
inference(paramod_ordered,[status(thm)],[5765,5908]) ).
thf(7627,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) )
!= ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) )
| ( ( empty @ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ path_cons ) )
= sk5 )
| ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of @ ( sk2 @ ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ sk8 ) ) @ edge ) ),
inference(simp,[status(thm)],[7626]) ).
thf(7628,plain,
( ( ( empty @ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ path_cons ) )
= sk5 )
| ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of @ ( sk2 @ ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ sk8 ) ) @ edge ) ),
inference(pattern_uni,[status(thm)],[7627:[]]) ).
thf(3423,plain,
! [A: $i] :
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ edge )
!= ( A @ edge ) )
| ( A @ head_of @ vertex )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[3354,157]) ).
thf(3424,plain,
! [A: $i] :
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ edge )
!= ( A @ edge ) )
| ( A @ head_of @ vertex ) ),
inference(simp,[status(thm)],[3423]) ).
thf(3425,plain,
sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of @ vertex,
inference(pattern_uni,[status(thm)],[3424:[bind(A,$thf( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) ))]]) ).
thf(27,plain,
! [A: $i] :
( ( ( A @ head_of )
!= ( sk3 @ tail_of ) )
| ( ( A @ tail_of )
!= ( sk4 @ head_of ) )
| ~ ( A @ edge ) ),
inference(cnfConj,[status(thm)],[23]) ).
thf(28,plain,
! [A: $i] :
( ~ ( A @ edge )
| ( ( A @ head_of )
!= ( sk3 @ tail_of ) )
| ( ( A @ tail_of )
!= ( sk4 @ head_of ) ) ),
inference(lifteq,[status(thm)],[27]) ).
thf(3429,plain,
! [A: $i] :
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ edge )
!= ( A @ edge ) )
| ~ $true
| ( ( A @ head_of )
!= ( sk3 @ tail_of ) )
| ( ( A @ tail_of )
!= ( sk4 @ head_of ) ) ),
inference(paramod_ordered,[status(thm)],[3354,28]) ).
thf(3430,plain,
! [A: $i] :
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ edge )
!= ( A @ edge ) )
| ( ( A @ head_of )
!= ( sk3 @ tail_of ) )
| ( ( A @ tail_of )
!= ( sk4 @ head_of ) ) ),
inference(simp,[status(thm)],[3429]) ).
thf(3431,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of )
!= ( sk3 @ tail_of ) )
| ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ tail_of )
!= ( sk4 @ head_of ) ) ),
inference(pattern_uni,[status(thm)],[3430:[bind(A,$thf( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) ))]]) ).
thf(7339,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of )
!= ( sk3 @ tail_of ) )
| ( ( sk4 @ head_of )
!= sk1 ) ),
inference(rewrite,[status(thm)],[3431,4048]) ).
thf(7348,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of )
!= ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of ) )
| ( ( sk3 @ tail_of )
!= sk2 )
| ( ( sk4 @ head_of )
!= sk1 )
| ~ ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) ),
inference(paramod_ordered,[status(thm)],[6610,7339]) ).
thf(7349,plain,
( ( ( sk3 @ tail_of )
!= sk2 )
| ( ( sk4 @ head_of )
!= sk1 )
| ~ ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) ),
inference(pattern_uni,[status(thm)],[7348:[]]) ).
thf(15,axiom,
! [A: $i,B: $i,C: $i] :
( ( A @ ( C @ ( B @ path ) ) )
=> ! [D: $i,E: $i] :
( ( A @ ( E @ ( D @ precedes ) ) )
<= ( ( ? [F: $i] :
( ( A @ ( E @ ( F @ precedes ) ) )
& ( F @ ( D @ sequential ) ) )
| ( E @ ( D @ sequential ) ) )
& ( A @ ( E @ on_path ) )
& ( A @ ( D @ on_path ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',precedes_defn) ).
thf(125,plain,
! [A: $i,B: $i,C: $i] :
( ( A @ ( C @ ( B @ path ) ) )
=> ! [D: $i,E: $i] :
( ( ( ? [F: $i] :
( ( A @ ( E @ ( F @ precedes ) ) )
& ( F @ ( D @ sequential ) ) )
| ( E @ ( D @ sequential ) ) )
& ( A @ ( E @ on_path ) )
& ( A @ ( D @ on_path ) ) )
=> ( A @ ( E @ ( D @ precedes ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[15]) ).
thf(1567,plain,
! [B: $i,A: $i] :
( ( ( sk5 @ ( edges @ number_of_in ) )
!= ( graph @ ( A @ number_of_in ) ) )
| ( sk5 @ length_of @ ( B @ ( A @ number_of_in ) @ less_or_equal ) ) ),
inference(paramod_ordered,[status(thm)],[1434,33]) ).
thf(1570,plain,
! [B: $i,A: $i] :
( ( sk5 != graph )
| ( edges != A )
| ( sk5 @ length_of @ ( B @ ( A @ number_of_in ) @ less_or_equal ) ) ),
inference(simp,[status(thm)],[1567]) ).
thf(1577,plain,
! [A: $i] :
( ( sk5 != graph )
| ( sk5 @ length_of @ ( A @ ( edges @ number_of_in ) @ less_or_equal ) ) ),
inference(simp,[status(thm)],[1570]) ).
thf(10,axiom,
! [A: $i,B: $i,C: $i,D: $i] :
( ( ( C @ ( D @ in_path ) )
& ( C @ ( B @ ( A @ path ) ) ) )
=> ( ? [E: $i] :
( ( ( D
= ( E @ tail_of ) )
| ( D
= ( E @ head_of ) ) )
& ( C @ ( E @ on_path ) ) )
& ( D @ vertex ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',in_path_properties) ).
thf(84,plain,
! [A: $i,B: $i,C: $i,D: $i] :
( ( ( C @ ( D @ in_path ) )
& ( C @ ( B @ ( A @ path ) ) ) )
=> ( ? [E: $i] :
( ( ( D
= ( E @ tail_of ) )
| ( D
= ( E @ head_of ) ) )
& ( C @ ( E @ on_path ) ) )
& ( D @ vertex ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[10]) ).
thf(85,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( D
= ( A @ ( B @ ( C @ ( D @ sk11 ) ) ) @ tail_of ) )
| ( D
= ( A @ ( B @ ( C @ ( D @ sk11 ) ) ) @ head_of ) )
| ~ ( C @ ( D @ in_path ) )
| ~ ( C @ ( B @ ( A @ path ) ) ) )
& ( ( C @ ( A @ ( B @ ( C @ ( D @ sk11 ) ) ) @ on_path ) )
| ~ ( C @ ( D @ in_path ) )
| ~ ( C @ ( B @ ( A @ path ) ) ) )
& ( ( D @ vertex )
| ~ ( C @ ( D @ in_path ) )
| ~ ( C @ ( B @ ( A @ path ) ) ) ) ),
inference(cnf,[status(esa)],[84]) ).
thf(87,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( C @ ( A @ ( B @ ( C @ ( D @ sk11 ) ) ) @ on_path ) )
| ~ ( C @ ( D @ in_path ) )
| ~ ( C @ ( B @ ( A @ path ) ) ) ),
inference(cnfConj,[status(thm)],[85]) ).
thf(7845,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ path ) ) )
!= ( C @ ( B @ ( A @ path ) ) ) )
| ( C @ ( A @ ( B @ ( C @ ( D @ sk11 ) ) ) @ on_path ) )
| ~ ( C @ ( D @ in_path ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1404,87]) ).
thf(7846,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ path ) ) )
!= ( C @ ( B @ ( A @ path ) ) ) )
| ( C @ ( A @ ( B @ ( C @ ( D @ sk11 ) ) ) @ on_path ) )
| ~ ( C @ ( D @ in_path ) ) ),
inference(simp,[status(thm)],[7845]) ).
thf(7847,plain,
! [A: $i] :
( ( sk5 @ ( sk1 @ ( sk2 @ ( sk5 @ ( A @ sk11 ) ) ) @ on_path ) )
| ~ ( sk5 @ ( A @ in_path ) ) ),
inference(pattern_uni,[status(thm)],[7846:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 )),bind(C,$thf( sk5 ))]]) ).
thf(7862,plain,
! [A: $i] :
( ( sk5 @ ( sk1 @ ( sk2 @ ( sk5 @ ( A @ sk11 ) ) ) @ on_path ) )
| ~ ( sk5 @ ( A @ in_path ) ) ),
inference(simp,[status(thm)],[7847]) ).
thf(11,axiom,
! [A: $i,B: $i,C: $i] :
( ( A @ ( C @ ( B @ path ) ) )
=> ! [D: $i,E: $i] :
( ( A @ ( E @ ( D @ precedes ) ) )
=> ( ( ( E @ ( D @ sequential ) )
<~> ? [F: $i] :
( ( A @ ( E @ ( F @ precedes ) ) )
& ( F @ ( D @ sequential ) ) ) )
& ( A @ ( E @ on_path ) )
& ( A @ ( D @ on_path ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',precedes_properties) ).
thf(90,plain,
! [A: $i,B: $i,C: $i] :
( ( A @ ( C @ ( B @ path ) ) )
=> ! [D: $i,E: $i] :
( ( A @ ( E @ ( D @ precedes ) ) )
=> ( ~ ( ( ? [F: $i] :
( ( A @ ( E @ ( F @ precedes ) ) )
& ( F @ ( D @ sequential ) ) )
=> ( E @ ( D @ sequential ) ) )
& ( ( E @ ( D @ sequential ) )
=> ? [F: $i] :
( ( A @ ( E @ ( F @ precedes ) ) )
& ( F @ ( D @ sequential ) ) ) ) )
& ( A @ ( E @ on_path ) )
& ( A @ ( D @ on_path ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[11]) ).
thf(91,plain,
! [A: $i] :
( ? [B: $i,C: $i] : ( A @ ( C @ ( B @ path ) ) )
=> ! [B: $i,C: $i] :
( ( A @ ( C @ ( B @ precedes ) ) )
=> ( ~ ( ( ? [D: $i] :
( ( A @ ( C @ ( D @ precedes ) ) )
& ( D @ ( B @ sequential ) ) )
=> ( C @ ( B @ sequential ) ) )
& ( ( C @ ( B @ sequential ) )
=> ? [D: $i] :
( ( A @ ( C @ ( D @ precedes ) ) )
& ( D @ ( B @ sequential ) ) ) ) )
& ( A @ ( C @ on_path ) )
& ( A @ ( B @ on_path ) ) ) ) ),
inference(miniscope,[status(thm)],[90]) ).
thf(92,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ~ ( E @ ( D @ sequential ) )
| ( A @ ( E @ ( D @ sk12 ) ) )
| ~ ( A @ ( E @ ( D @ precedes ) ) )
| ~ ( A @ ( C @ ( B @ path ) ) ) )
& ( ( A @ ( E @ ( A @ ( D @ ( E @ sk13 ) ) @ precedes ) ) )
| ( A @ ( E @ ( D @ sk12 ) ) )
| ~ ( A @ ( E @ ( D @ precedes ) ) )
| ~ ( A @ ( C @ ( B @ path ) ) ) )
& ( ( A @ ( D @ ( E @ sk13 ) ) @ ( D @ sequential ) )
| ( A @ ( E @ ( D @ sk12 ) ) )
| ~ ( A @ ( E @ ( D @ precedes ) ) )
| ~ ( A @ ( C @ ( B @ path ) ) ) )
& ( ~ ( A @ ( E @ ( D @ sk12 ) ) )
| ~ ( A @ ( E @ ( F @ precedes ) ) )
| ~ ( F @ ( D @ sequential ) )
| ~ ( A @ ( E @ ( D @ precedes ) ) )
| ~ ( A @ ( C @ ( B @ path ) ) ) )
& ( ~ ( A @ ( E @ ( D @ sk12 ) ) )
| ( E @ ( D @ sequential ) )
| ~ ( A @ ( E @ ( D @ precedes ) ) )
| ~ ( A @ ( C @ ( B @ path ) ) ) )
& ( ( A @ ( E @ on_path ) )
| ~ ( A @ ( E @ ( D @ precedes ) ) )
| ~ ( A @ ( C @ ( B @ path ) ) ) )
& ( ( A @ ( D @ on_path ) )
| ~ ( A @ ( E @ ( D @ precedes ) ) )
| ~ ( A @ ( C @ ( B @ path ) ) ) ) ),
inference(cnf,[status(esa)],[91]) ).
thf(93,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ~ ( A @ ( E @ ( D @ sk12 ) ) )
| ~ ( A @ ( E @ ( F @ precedes ) ) )
| ~ ( F @ ( D @ sequential ) )
| ~ ( A @ ( E @ ( D @ precedes ) ) )
| ~ ( A @ ( C @ ( B @ path ) ) ) ),
inference(cnfConj,[status(thm)],[92]) ).
thf(5972,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) )
!= ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) )
| ~ $true
| ( ( empty @ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ path_cons ) )
= sk5 )
| ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ ( sk2 @ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of @ path ) ) ) ),
inference(paramod_ordered,[status(thm)],[3848,5908]) ).
thf(5973,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) )
!= ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) )
| ( ( empty @ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ path_cons ) )
= sk5 )
| ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ ( sk2 @ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of @ path ) ) ) ),
inference(simp,[status(thm)],[5972]) ).
thf(5974,plain,
( ( ( empty @ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ path_cons ) )
= sk5 )
| ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ ( sk2 @ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of @ path ) ) ) ),
inference(pattern_uni,[status(thm)],[5973:[]]) ).
thf(2236,plain,
! [B: $i,A: $i] :
( ( ( sk5 @ ( triangles @ number_of_in ) )
!= ( B @ ( A @ number_of_in ) ) )
| ( graph @ ( A @ number_of_in ) @ ( sk5 @ ( sequential_pairs @ number_of_in ) @ less_or_equal ) )
| ( sk5 @ sk7 @ ( sk5 @ sk6 @ sequential ) ) ),
inference(paramod_ordered,[status(thm)],[1420,33]) ).
thf(2237,plain,
( ( graph @ ( triangles @ number_of_in ) @ ( sk5 @ ( sequential_pairs @ number_of_in ) @ less_or_equal ) )
| ( sk5 @ sk7 @ ( sk5 @ sk6 @ sequential ) ) ),
inference(pattern_uni,[status(thm)],[2236:[bind(A,$thf( triangles )),bind(B,$thf( sk5 ))]]) ).
thf(74,plain,
! [C: $i,B: $i,A: $i] :
( ( C
= ( A @ ( B @ ( C @ sk10 ) ) @ ( A @ ( B @ ( C @ sk8 ) ) @ path_cons ) ) )
| ( A @ ( B @ ( C @ sk9 ) ) )
| ~ ( C @ ( B @ ( A @ path ) ) ) ),
inference(cnfConj,[status(thm)],[67]) ).
thf(79,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( B @ ( C @ sk9 ) ) )
| ~ ( C @ ( B @ ( A @ path ) ) )
| ( ( A @ ( B @ ( C @ sk10 ) ) @ ( A @ ( B @ ( C @ sk8 ) ) @ path_cons ) )
= C ) ),
inference(lifteq,[status(thm)],[74]) ).
thf(4581,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ path ) ) )
!= ( C @ ( B @ ( A @ path ) ) ) )
| ( A @ ( B @ ( C @ sk9 ) ) )
| ~ $true
| ( ( A @ ( B @ ( C @ sk10 ) ) @ ( A @ ( B @ ( C @ sk8 ) ) @ path_cons ) )
= C ) ),
inference(paramod_ordered,[status(thm)],[1404,79]) ).
thf(4582,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ path ) ) )
!= ( C @ ( B @ ( A @ path ) ) ) )
| ( A @ ( B @ ( C @ sk9 ) ) )
| ( ( A @ ( B @ ( C @ sk10 ) ) @ ( A @ ( B @ ( C @ sk8 ) ) @ path_cons ) )
= C ) ),
inference(simp,[status(thm)],[4581]) ).
thf(4583,plain,
( ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) )
| ( ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ path_cons ) )
= sk5 ) ),
inference(pattern_uni,[status(thm)],[4582:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 )),bind(C,$thf( sk5 ))]]) ).
thf(3048,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ shortest_path ) ) )
!= ( sk5 @ ( B @ ( A @ shortest_path ) ) ) )
| ~ $true
| ( ( C @ head_of )
!= ( sk4 @ head_of ) )
| ( ( C @ tail_of )
!= ( sk3 @ tail_of ) ) ),
inference(paramod_ordered,[status(thm)],[25,2732]) ).
thf(3049,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ shortest_path ) ) )
!= ( sk5 @ ( B @ ( A @ shortest_path ) ) ) )
| ( ( C @ head_of )
!= ( sk4 @ head_of ) )
| ( ( C @ tail_of )
!= ( sk3 @ tail_of ) ) ),
inference(simp,[status(thm)],[3048]) ).
thf(3050,plain,
! [A: $i] :
( ( ( A @ head_of )
!= ( sk4 @ head_of ) )
| ( ( A @ tail_of )
!= ( sk3 @ tail_of ) ) ),
inference(pattern_uni,[status(thm)],[3049:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 ))]]) ).
thf(3059,plain,
! [A: $i] :
( ( ( A @ head_of )
!= ( sk4 @ head_of ) )
| ( ( A @ tail_of )
!= ( sk3 @ tail_of ) ) ),
inference(simp,[status(thm)],[3050]) ).
thf(4686,plain,
! [A: $i] :
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ tail_of )
!= ( sk3 @ tail_of ) )
| ( ( A @ head_of )
!= ( sk4 @ head_of ) )
| ( ( A @ tail_of )
!= sk1 ) ),
inference(paramod_ordered,[status(thm)],[4048,3059]) ).
thf(4696,plain,
! [A: $i] :
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ tail_of )
!= ( sk3 @ tail_of ) )
| ( A != sk4 )
| ( ( A @ tail_of )
!= sk1 ) ),
inference(simp,[status(thm)],[4686]) ).
thf(4711,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ tail_of )
!= ( sk3 @ tail_of ) )
| ( ( sk4 @ tail_of )
!= sk1 ) ),
inference(simp,[status(thm)],[4696]) ).
thf(4847,plain,
( ( ( sk3 @ tail_of )
!= sk1 )
| ( ( sk4 @ tail_of )
!= sk1 ) ),
inference(rewrite,[status(thm)],[4711,4048]) ).
thf(20,axiom,
! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ ( A @ triangle ) ) )
<=> ( ( A @ ( C @ sequential ) )
& ( C @ ( B @ sequential ) )
& ( B @ ( A @ sequential ) )
& ( C @ edge )
& ( B @ edge )
& ( A @ edge ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',triangle_defn) ).
thf(159,plain,
! [A: $i,B: $i,C: $i] :
( ( ( ( A @ ( C @ sequential ) )
& ( C @ ( B @ sequential ) )
& ( B @ ( A @ sequential ) )
& ( C @ edge )
& ( B @ edge )
& ( A @ edge ) )
=> ( C @ ( B @ ( A @ triangle ) ) ) )
& ( ( C @ ( B @ ( A @ triangle ) ) )
=> ( ( A @ ( C @ sequential ) )
& ( C @ ( B @ sequential ) )
& ( B @ ( A @ sequential ) )
& ( C @ edge )
& ( B @ edge )
& ( A @ edge ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[20]) ).
thf(160,plain,
( ! [A: $i,B: $i,C: $i] :
( ( ( A @ ( C @ sequential ) )
& ( C @ ( B @ sequential ) )
& ( B @ ( A @ sequential ) )
& ( C @ edge )
& ( B @ edge )
& ( A @ edge ) )
=> ( C @ ( B @ ( A @ triangle ) ) ) )
& ! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ ( A @ triangle ) ) )
=> ( ( A @ ( C @ sequential ) )
& ( C @ ( B @ sequential ) )
& ( B @ ( A @ sequential ) )
& ( C @ edge )
& ( B @ edge )
& ( A @ edge ) ) ) ),
inference(miniscope,[status(thm)],[159]) ).
thf(161,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( F @ ( E @ ( D @ triangle ) ) )
| ~ ( D @ ( F @ sequential ) )
| ~ ( F @ ( E @ sequential ) )
| ~ ( E @ ( D @ sequential ) )
| ~ ( F @ edge )
| ~ ( E @ edge )
| ~ ( D @ edge ) )
& ( ( A @ ( C @ sequential ) )
| ~ ( C @ ( B @ ( A @ triangle ) ) ) )
& ( ( C @ ( B @ sequential ) )
| ~ ( C @ ( B @ ( A @ triangle ) ) ) )
& ( ( B @ ( A @ sequential ) )
| ~ ( C @ ( B @ ( A @ triangle ) ) ) )
& ( ( C @ edge )
| ~ ( C @ ( B @ ( A @ triangle ) ) ) )
& ( ( B @ edge )
| ~ ( C @ ( B @ ( A @ triangle ) ) ) )
& ( ( A @ edge )
| ~ ( C @ ( B @ ( A @ triangle ) ) ) ) ),
inference(cnf,[status(esa)],[160]) ).
thf(164,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ edge )
| ~ ( C @ ( B @ ( A @ triangle ) ) ) ),
inference(cnfConj,[status(thm)],[161]) ).
thf(73,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ vertex )
| ~ ( C @ ( B @ ( A @ path ) ) ) ),
inference(cnfConj,[status(thm)],[67]) ).
thf(1375,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ path ) ) )
!= ( F @ ( E @ ( D @ path ) ) ) )
| ( E @ vertex )
| ~ $true
| ~ ( C @ ( B @ ( A @ shortest_path ) ) ) ),
inference(paramod_ordered,[status(thm)],[115,73]) ).
thf(1376,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ path ) ) )
!= ( F @ ( E @ ( D @ path ) ) ) )
| ( E @ vertex )
| ~ ( C @ ( B @ ( A @ shortest_path ) ) ) ),
inference(simp,[status(thm)],[1375]) ).
thf(1377,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ vertex )
| ~ ( C @ ( B @ ( A @ shortest_path ) ) ) ),
inference(pattern_uni,[status(thm)],[1376:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( A )),bind(E,$thf( B )),bind(F,$thf( C ))]]) ).
thf(88,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D
= ( A @ ( B @ ( C @ ( D @ sk11 ) ) ) @ tail_of ) )
| ( D
= ( A @ ( B @ ( C @ ( D @ sk11 ) ) ) @ head_of ) )
| ~ ( C @ ( D @ in_path ) )
| ~ ( C @ ( B @ ( A @ path ) ) ) ),
inference(cnfConj,[status(thm)],[85]) ).
thf(89,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ ( C @ ( D @ in_path ) )
| ~ ( C @ ( B @ ( A @ path ) ) )
| ( ( A @ ( B @ ( C @ ( D @ sk11 ) ) ) @ tail_of )
= D )
| ( ( A @ ( B @ ( C @ ( D @ sk11 ) ) ) @ head_of )
= D ) ),
inference(lifteq,[status(thm)],[88]) ).
thf(4128,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ tail_of )
!= ( B @ tail_of ) )
| ~ ( B @ ( A @ sequential ) )
| ( ( A @ head_of )
= sk1 ) ),
inference(paramod_ordered,[status(thm)],[4048,56]) ).
thf(4129,plain,
! [A: $i] :
( ~ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ ( A @ sequential ) )
| ( ( A @ head_of )
= sk1 ) ),
inference(pattern_uni,[status(thm)],[4128:[bind(A,$thf( A )),bind(B,$thf( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) ))]]) ).
thf(7352,plain,
! [A: $i] :
( ( ( A @ head_of )
!= ( sk4 @ head_of ) )
| ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of )
!= ( sk3 @ tail_of ) )
| ( sk1 != sk1 )
| ~ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ ( A @ sequential ) ) ),
inference(paramod_ordered,[status(thm)],[4129,7339]) ).
thf(7353,plain,
! [A: $i] :
( ( ( A @ head_of )
!= ( sk4 @ head_of ) )
| ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of )
!= ( sk3 @ tail_of ) )
| ~ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ ( A @ sequential ) ) ),
inference(simp,[status(thm)],[7352]) ).
thf(7354,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of )
!= ( sk3 @ tail_of ) )
| ~ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ ( sk4 @ sequential ) ) ),
inference(pattern_uni,[status(thm)],[7353:[bind(A,$thf( sk4 ))]]) ).
thf(51,plain,
! [B: $i,A: $i] :
( ( A != B )
| ~ ( B @ ( A @ sequential ) ) ),
inference(cnfConj,[status(thm)],[50]) ).
thf(59,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ sequential ) )
| ( A != B ) ),
inference(lifteq,[status(thm)],[51]) ).
thf(60,plain,
! [A: $i] :
~ ( A @ ( A @ sequential ) ),
inference(simp,[status(thm)],[59]) ).
thf(6729,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) )
!= ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) )
| ~ $true
| ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of )
= sk2 )
| ( graph @ ( edges @ number_of_in ) @ ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ length_of @ less_or_equal ) ) ),
inference(paramod_ordered,[status(thm)],[5762,6610]) ).
thf(6730,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) )
!= ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) )
| ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of )
= sk2 )
| ( graph @ ( edges @ number_of_in ) @ ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ length_of @ less_or_equal ) ) ),
inference(simp,[status(thm)],[6729]) ).
thf(6731,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of )
= sk2 )
| ( graph @ ( edges @ number_of_in ) @ ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ length_of @ less_or_equal ) ) ),
inference(pattern_uni,[status(thm)],[6730:[]]) ).
thf(4684,plain,
! [A: $i] :
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ tail_of )
!= ( A @ tail_of ) )
| ( ( A @ head_of )
!= ( sk4 @ head_of ) )
| ( ( sk3 @ tail_of )
!= sk1 ) ),
inference(paramod_ordered,[status(thm)],[4048,3059]) ).
thf(4685,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of )
!= ( sk4 @ head_of ) )
| ( ( sk3 @ tail_of )
!= sk1 ) ),
inference(pattern_uni,[status(thm)],[4684:[bind(A,$thf( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) ))]]) ).
thf(4813,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ tail_of )
!= ( sk3 @ tail_of ) )
| ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of )
!= ( sk4 @ head_of ) )
| ( sk1 != sk1 ) ),
inference(paramod_ordered,[status(thm)],[4048,4685]) ).
thf(4814,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ tail_of )
!= ( sk3 @ tail_of ) )
| ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of )
!= ( sk4 @ head_of ) ) ),
inference(simp,[status(thm)],[4813]) ).
thf(4818,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) )
!= sk3 )
| ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of )
!= ( sk4 @ head_of ) ) ),
inference(simp,[status(thm)],[4814]) ).
thf(6683,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of )
!= ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of ) )
| ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) )
!= sk3 )
| ( ( sk4 @ head_of )
!= sk2 )
| ~ ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) ),
inference(paramod_ordered,[status(thm)],[6610,4818]) ).
thf(6684,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) )
!= sk3 )
| ( ( sk4 @ head_of )
!= sk2 )
| ~ ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) ),
inference(pattern_uni,[status(thm)],[6683:[]]) ).
thf(3011,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( sk5 @ ( B @ ( A @ shortest_path ) ) )
| ( C != sk4 )
| ( ( C @ tail_of )
!= ( sk3 @ tail_of ) ) ),
inference(simp,[status(thm)],[2732]) ).
thf(3053,plain,
! [B: $i,A: $i] :
( ~ ( sk5 @ ( B @ ( A @ shortest_path ) ) )
| ( ( sk4 @ tail_of )
!= ( sk3 @ tail_of ) ) ),
inference(simp,[status(thm)],[3011]) ).
thf(3993,plain,
! [B: $i,A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ shortest_path ) ) )
!= ( sk5 @ ( B @ ( A @ shortest_path ) ) ) )
| ~ $true
| ( ( sk4 @ tail_of )
!= ( sk3 @ tail_of ) ) ),
inference(paramod_ordered,[status(thm)],[25,3053]) ).
thf(3994,plain,
! [B: $i,A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ shortest_path ) ) )
!= ( sk5 @ ( B @ ( A @ shortest_path ) ) ) )
| ( ( sk4 @ tail_of )
!= ( sk3 @ tail_of ) ) ),
inference(simp,[status(thm)],[3993]) ).
thf(3995,plain,
( ( sk4 @ tail_of )
!= ( sk3 @ tail_of ) ),
inference(pattern_uni,[status(thm)],[3994:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 ))]]) ).
thf(4698,plain,
! [A: $i] :
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) )
!= sk3 )
| ( A != sk4 )
| ( ( A @ tail_of )
!= sk1 ) ),
inference(simp,[status(thm)],[4686]) ).
thf(4712,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) )
!= sk3 )
| ( ( sk4 @ tail_of )
!= sk1 ) ),
inference(simp,[status(thm)],[4698]) ).
thf(524,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ shortest_path ) ) )
!= ( E @ ( B @ ( A @ shortest_path ) ) ) )
| ~ ( E @ ( C @ ( D @ precedes ) ) )
| ~ ( E @ ( D @ ( C @ precedes ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[25,64]) ).
thf(525,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ shortest_path ) ) )
!= ( E @ ( B @ ( A @ shortest_path ) ) ) )
| ~ ( E @ ( C @ ( D @ precedes ) ) )
| ~ ( E @ ( D @ ( C @ precedes ) ) ) ),
inference(simp,[status(thm)],[524]) ).
thf(526,plain,
! [B: $i,A: $i] :
( ~ ( sk5 @ ( A @ ( B @ precedes ) ) )
| ~ ( sk5 @ ( B @ ( A @ precedes ) ) ) ),
inference(pattern_uni,[status(thm)],[525:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( sk5 ))]]) ).
thf(536,plain,
! [B: $i,A: $i] :
( ~ ( sk5 @ ( A @ ( B @ precedes ) ) )
| ~ ( sk5 @ ( B @ ( A @ precedes ) ) ) ),
inference(simp,[status(thm)],[526]) ).
thf(743,plain,
! [B: $i,A: $i] :
( ~ $true
| ( ( sk5 @ ( A @ ( B @ precedes ) ) )
!= ( sk5 @ ( B @ ( A @ precedes ) ) ) )
| ~ ( sk5 @ ( B @ ( A @ precedes ) ) ) ),
inference(eqfactor_ordered,[status(thm)],[536]) ).
thf(744,plain,
! [A: $i] :
~ ( sk5 @ ( A @ ( A @ precedes ) ) ),
inference(pattern_uni,[status(thm)],[743:[bind(A,$thf( B ))]]) ).
thf(746,plain,
! [A: $i] :
~ ( sk5 @ ( A @ ( A @ precedes ) ) ),
inference(simp,[status(thm)],[744]) ).
thf(165,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ edge )
| ~ ( C @ ( B @ ( A @ triangle ) ) ) ),
inference(cnfConj,[status(thm)],[161]) ).
thf(2436,plain,
( ( ( sk5 @ ( triangles @ number_of_in ) )
!= ( sk5 @ ( edges @ number_of_in ) ) )
| ( sk5 @ sk7 @ edge )
| ( ( sk5 @ ( sequential_pairs @ number_of_in ) )
= ( sk5 @ length_of ) ) ),
inference(paramod_ordered,[status(thm)],[1434,2254]) ).
thf(2464,plain,
( ( sk5 != sk5 )
| ( triangles != edges )
| ( sk5 @ sk7 @ edge )
| ( ( sk5 @ ( sequential_pairs @ number_of_in ) )
= ( sk5 @ length_of ) ) ),
inference(simp,[status(thm)],[2436]) ).
thf(2467,plain,
( ( triangles != edges )
| ( sk5 @ sk7 @ edge )
| ( ( sk5 @ ( sequential_pairs @ number_of_in ) )
= ( sk5 @ length_of ) ) ),
inference(simp,[status(thm)],[2464]) ).
thf(3681,plain,
! [B: $i,A: $i] :
( ( ( sk5 @ ( sequential_pairs @ number_of_in ) )
!= ( B @ ( A @ number_of_in ) ) )
| ( graph @ ( A @ number_of_in ) @ ( sk5 @ length_of @ less_or_equal ) )
| ( triangles != edges )
| ( sk5 @ sk7 @ edge ) ),
inference(paramod_ordered,[status(thm)],[2467,33]) ).
thf(3682,plain,
( ( graph @ ( sequential_pairs @ number_of_in ) @ ( sk5 @ length_of @ less_or_equal ) )
| ( triangles != edges )
| ( sk5 @ sk7 @ edge ) ),
inference(pattern_uni,[status(thm)],[3681:[bind(A,$thf( sequential_pairs )),bind(B,$thf( sk5 ))]]) ).
thf(1421,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ path ) ) )
!= ( C @ ( B @ ( A @ path ) ) ) )
| ( B @ vertex )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1404,73]) ).
thf(1422,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ path ) ) )
!= ( C @ ( B @ ( A @ path ) ) ) )
| ( B @ vertex ) ),
inference(simp,[status(thm)],[1421]) ).
thf(1423,plain,
sk2 @ vertex,
inference(pattern_uni,[status(thm)],[1422:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 )),bind(C,$thf( sk5 ))]]) ).
thf(86,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ vertex )
| ~ ( C @ ( D @ in_path ) )
| ~ ( C @ ( B @ ( A @ path ) ) ) ),
inference(cnfConj,[status(thm)],[85]) ).
thf(7314,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ path ) ) )
!= ( C @ ( B @ ( A @ path ) ) ) )
| ( D @ vertex )
| ~ ( C @ ( D @ in_path ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1404,86]) ).
thf(7315,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ path ) ) )
!= ( C @ ( B @ ( A @ path ) ) ) )
| ( D @ vertex )
| ~ ( C @ ( D @ in_path ) ) ),
inference(simp,[status(thm)],[7314]) ).
thf(7316,plain,
! [A: $i] :
( ( A @ vertex )
| ~ ( sk5 @ ( A @ in_path ) ) ),
inference(pattern_uni,[status(thm)],[7315:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 )),bind(C,$thf( sk5 ))]]) ).
thf(7325,plain,
! [A: $i] :
( ( A @ vertex )
| ~ ( sk5 @ ( A @ in_path ) ) ),
inference(simp,[status(thm)],[7316]) ).
thf(5526,plain,
! [A: $i] :
( ( ( A @ head_of )
!= ( sk3 @ head_of ) )
| ( sk1 != sk1 )
| ~ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ ( sk4 @ sequential ) )
| ~ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ ( A @ sequential ) ) ),
inference(paramod_ordered,[status(thm)],[4129,4137]) ).
thf(5527,plain,
! [A: $i] :
( ( ( A @ head_of )
!= ( sk3 @ head_of ) )
| ~ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ ( sk4 @ sequential ) )
| ~ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ ( A @ sequential ) ) ),
inference(simp,[status(thm)],[5526]) ).
thf(5528,plain,
( ~ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ ( sk4 @ sequential ) )
| ~ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ ( sk3 @ sequential ) ) ),
inference(pattern_uni,[status(thm)],[5527:[bind(A,$thf( sk3 ))]]) ).
thf(5654,plain,
( ~ $true
| ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ ( sk4 @ sequential ) )
!= ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ ( sk3 @ sequential ) ) )
| ~ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ ( sk3 @ sequential ) ) ),
inference(eqfactor_ordered,[status(thm)],[5528]) ).
thf(5655,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ ( sk4 @ sequential ) )
!= ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ ( sk3 @ sequential ) ) )
| ~ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ ( sk3 @ sequential ) ) ),
inference(simp,[status(thm)],[5654]) ).
thf(97,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ~ ( E @ ( D @ sequential ) )
| ( A @ ( E @ ( D @ sk12 ) ) )
| ~ ( A @ ( E @ ( D @ precedes ) ) )
| ~ ( A @ ( C @ ( B @ path ) ) ) ),
inference(cnfConj,[status(thm)],[92]) ).
thf(96,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( A @ ( D @ on_path ) )
| ~ ( A @ ( E @ ( D @ precedes ) ) )
| ~ ( A @ ( C @ ( B @ path ) ) ) ),
inference(cnfConj,[status(thm)],[92]) ).
thf(11474,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ path ) ) )
!= ( A @ ( C @ ( B @ path ) ) ) )
| ( A @ ( D @ on_path ) )
| ~ ( A @ ( E @ ( D @ precedes ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1404,96]) ).
thf(11475,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ path ) ) )
!= ( A @ ( C @ ( B @ path ) ) ) )
| ( A @ ( D @ on_path ) )
| ~ ( A @ ( E @ ( D @ precedes ) ) ) ),
inference(simp,[status(thm)],[11474]) ).
thf(11476,plain,
! [B: $i,A: $i] :
( ( sk5 @ ( A @ on_path ) )
| ~ ( sk5 @ ( B @ ( A @ precedes ) ) ) ),
inference(pattern_uni,[status(thm)],[11475:[bind(A,$thf( sk5 )),bind(B,$thf( sk1 )),bind(C,$thf( sk2 ))]]) ).
thf(11492,plain,
! [B: $i,A: $i] :
( ( sk5 @ ( A @ on_path ) )
| ~ ( sk5 @ ( B @ ( A @ precedes ) ) ) ),
inference(simp,[status(thm)],[11476]) ).
thf(6727,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of )
!= ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of ) )
| ( ( sk4 @ head_of )
!= sk2 )
| ( ( sk3 @ tail_of )
!= sk1 )
| ~ ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) ),
inference(paramod_ordered,[status(thm)],[6610,4685]) ).
thf(6728,plain,
( ( ( sk4 @ head_of )
!= sk2 )
| ( ( sk3 @ tail_of )
!= sk1 )
| ~ ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) ),
inference(pattern_uni,[status(thm)],[6727:[]]) ).
thf(1452,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ path ) ) )
!= ( graph @ ( B @ ( A @ path ) ) ) )
| ( graph @ length_of @ ( C @ ( edges @ number_of_in ) @ less_or_equal ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1404,500]) ).
thf(1453,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ path ) ) )
!= ( graph @ ( B @ ( A @ path ) ) ) )
| ( graph @ length_of @ ( C @ ( edges @ number_of_in ) @ less_or_equal ) ) ),
inference(simp,[status(thm)],[1452]) ).
thf(1467,plain,
! [C: $i,B: $i,A: $i] :
( ( sk5 != graph )
| ( sk2 != B )
| ( sk1 != A )
| ( graph @ length_of @ ( C @ ( edges @ number_of_in ) @ less_or_equal ) ) ),
inference(simp,[status(thm)],[1453]) ).
thf(1477,plain,
! [A: $i] :
( ( sk5 != graph )
| ( graph @ length_of @ ( A @ ( edges @ number_of_in ) @ less_or_equal ) ) ),
inference(simp,[status(thm)],[1467]) ).
thf(1935,plain,
! [A: $i] :
( ( ( sk5 @ ( edges @ number_of_in ) )
!= ( A @ ( edges @ number_of_in ) ) )
| ( sk5 != graph )
| ( graph @ length_of @ ( sk5 @ length_of @ less_or_equal ) ) ),
inference(paramod_ordered,[status(thm)],[1434,1477]) ).
thf(1936,plain,
( ( sk5 != graph )
| ( graph @ length_of @ ( sk5 @ length_of @ less_or_equal ) ) ),
inference(pattern_uni,[status(thm)],[1935:[bind(A,$thf( sk5 ))]]) ).
thf(53,plain,
! [B: $i,A: $i] :
( ( A @ edge )
| ~ ( B @ ( A @ sequential ) ) ),
inference(cnfConj,[status(thm)],[50]) ).
thf(5685,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ ( sk2 @ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of @ path ) ) )
!= ( C @ ( B @ ( A @ path ) ) ) )
| ~ $true
| ( ( C @ ( edges @ number_of_in ) )
= ( C @ length_of ) )
| ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) ),
inference(paramod_ordered,[status(thm)],[3848,36]) ).
thf(5686,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ ( sk2 @ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of @ path ) ) )
!= ( C @ ( B @ ( A @ path ) ) ) )
| ( ( C @ ( edges @ number_of_in ) )
= ( C @ length_of ) )
| ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) ),
inference(simp,[status(thm)],[5685]) ).
thf(5687,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ ( edges @ number_of_in ) )
= ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ length_of ) )
| ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) ),
inference(pattern_uni,[status(thm)],[5686:[bind(A,$thf( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of )),bind(B,$thf( sk2 )),bind(C,$thf( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) ))]]) ).
thf(840,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( sk1 @ ( sk2 @ ( sk1 @ ( sk2 @ ( sk1 @ ( A @ sk14 ) ) @ sk14 ) ) @ sk14 ) ) @ ( sk1 @ ( sk2 @ path ) ) )
!= ( B @ ( sk1 @ ( sk2 @ path ) ) ) )
| ( sk2 @ ( sk1 @ ( sk2 @ ( sk1 @ ( B @ sk14 ) ) @ sk14 ) ) @ ( sk1 @ ( sk2 @ shortest_path ) ) )
| ( sk2 @ ( sk1 @ ( sk2 @ ( sk1 @ ( sk2 @ ( sk1 @ ( B @ sk14 ) ) @ sk14 ) ) @ sk14 ) ) @ ( sk1 @ ( sk2 @ path ) ) )
| ( sk2 @ ( sk1 @ ( B @ sk14 ) ) @ ( sk1 @ ( sk2 @ shortest_path ) ) )
| ( B @ ( sk1 @ ( sk2 @ shortest_path ) ) )
| ~ $true
| ( sk2 @ ( sk1 @ ( sk2 @ ( sk1 @ ( A @ sk14 ) ) @ sk14 ) ) @ ( sk1 @ ( sk2 @ shortest_path ) ) )
| ( sk2 @ ( sk1 @ ( A @ sk14 ) ) @ ( sk1 @ ( sk2 @ shortest_path ) ) )
| ( A @ ( sk1 @ ( sk2 @ shortest_path ) ) )
| ~ ( A @ ( sk1 @ ( sk2 @ path ) ) ) ),
inference(paramod_ordered,[status(thm)],[760,760]) ).
thf(841,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( sk1 @ ( sk2 @ ( sk1 @ ( sk2 @ ( sk1 @ ( A @ sk14 ) ) @ sk14 ) ) @ sk14 ) ) @ ( sk1 @ ( sk2 @ path ) ) )
!= ( B @ ( sk1 @ ( sk2 @ path ) ) ) )
| ( sk2 @ ( sk1 @ ( sk2 @ ( sk1 @ ( B @ sk14 ) ) @ sk14 ) ) @ ( sk1 @ ( sk2 @ shortest_path ) ) )
| ( sk2 @ ( sk1 @ ( sk2 @ ( sk1 @ ( sk2 @ ( sk1 @ ( B @ sk14 ) ) @ sk14 ) ) @ sk14 ) ) @ ( sk1 @ ( sk2 @ path ) ) )
| ( sk2 @ ( sk1 @ ( B @ sk14 ) ) @ ( sk1 @ ( sk2 @ shortest_path ) ) )
| ( B @ ( sk1 @ ( sk2 @ shortest_path ) ) )
| ( sk2 @ ( sk1 @ ( sk2 @ ( sk1 @ ( A @ sk14 ) ) @ sk14 ) ) @ ( sk1 @ ( sk2 @ shortest_path ) ) )
| ( sk2 @ ( sk1 @ ( A @ sk14 ) ) @ ( sk1 @ ( sk2 @ shortest_path ) ) )
| ( A @ ( sk1 @ ( sk2 @ shortest_path ) ) )
| ~ ( A @ ( sk1 @ ( sk2 @ path ) ) ) ),
inference(simp,[status(thm)],[840]) ).
thf(842,plain,
! [A: $i] :
( ( sk2 @ ( sk1 @ ( sk2 @ ( sk1 @ ( sk2 @ ( sk1 @ ( sk2 @ ( sk1 @ ( sk2 @ ( sk1 @ ( A @ sk14 ) ) @ sk14 ) ) @ sk14 ) ) @ sk14 ) ) @ sk14 ) ) @ ( sk1 @ ( sk2 @ shortest_path ) ) )
| ( sk2 @ ( sk1 @ ( sk2 @ ( sk1 @ ( sk2 @ ( sk1 @ ( sk2 @ ( sk1 @ ( sk2 @ ( sk1 @ ( sk2 @ ( sk1 @ ( A @ sk14 ) ) @ sk14 ) ) @ sk14 ) ) @ sk14 ) ) @ sk14 ) ) @ sk14 ) ) @ ( sk1 @ ( sk2 @ path ) ) )
| ( sk2 @ ( sk1 @ ( sk2 @ ( sk1 @ ( sk2 @ ( sk1 @ ( sk2 @ ( sk1 @ ( A @ sk14 ) ) @ sk14 ) ) @ sk14 ) ) @ sk14 ) ) @ ( sk1 @ ( sk2 @ shortest_path ) ) )
| ( sk2 @ ( sk1 @ ( sk2 @ ( sk1 @ ( sk2 @ ( sk1 @ ( A @ sk14 ) ) @ sk14 ) ) @ sk14 ) ) @ ( sk1 @ ( sk2 @ shortest_path ) ) )
| ( sk2 @ ( sk1 @ ( sk2 @ ( sk1 @ ( A @ sk14 ) ) @ sk14 ) ) @ ( sk1 @ ( sk2 @ shortest_path ) ) )
| ( sk2 @ ( sk1 @ ( A @ sk14 ) ) @ ( sk1 @ ( sk2 @ shortest_path ) ) )
| ( A @ ( sk1 @ ( sk2 @ shortest_path ) ) )
| ~ ( A @ ( sk1 @ ( sk2 @ path ) ) ) ),
inference(pattern_uni,[status(thm)],[841:[bind(A,$thf( I )),bind(B,$thf( sk2 @ ( sk1 @ ( sk2 @ ( sk1 @ ( sk2 @ ( sk1 @ ( I @ sk14 ) ) @ sk14 ) ) @ sk14 ) ) ))]]) ).
thf(857,plain,
! [A: $i] :
( ( sk2 @ ( sk1 @ ( sk2 @ ( sk1 @ ( sk2 @ ( sk1 @ ( sk2 @ ( sk1 @ ( sk2 @ ( sk1 @ ( A @ sk14 ) ) @ sk14 ) ) @ sk14 ) ) @ sk14 ) ) @ sk14 ) ) @ ( sk1 @ ( sk2 @ shortest_path ) ) )
| ( sk2 @ ( sk1 @ ( sk2 @ ( sk1 @ ( sk2 @ ( sk1 @ ( sk2 @ ( sk1 @ ( sk2 @ ( sk1 @ ( sk2 @ ( sk1 @ ( A @ sk14 ) ) @ sk14 ) ) @ sk14 ) ) @ sk14 ) ) @ sk14 ) ) @ sk14 ) ) @ ( sk1 @ ( sk2 @ path ) ) )
| ( sk2 @ ( sk1 @ ( sk2 @ ( sk1 @ ( sk2 @ ( sk1 @ ( sk2 @ ( sk1 @ ( A @ sk14 ) ) @ sk14 ) ) @ sk14 ) ) @ sk14 ) ) @ ( sk1 @ ( sk2 @ shortest_path ) ) )
| ( sk2 @ ( sk1 @ ( sk2 @ ( sk1 @ ( sk2 @ ( sk1 @ ( A @ sk14 ) ) @ sk14 ) ) @ sk14 ) ) @ ( sk1 @ ( sk2 @ shortest_path ) ) )
| ( sk2 @ ( sk1 @ ( sk2 @ ( sk1 @ ( A @ sk14 ) ) @ sk14 ) ) @ ( sk1 @ ( sk2 @ shortest_path ) ) )
| ( sk2 @ ( sk1 @ ( A @ sk14 ) ) @ ( sk1 @ ( sk2 @ shortest_path ) ) )
| ( A @ ( sk1 @ ( sk2 @ shortest_path ) ) )
| ~ ( A @ ( sk1 @ ( sk2 @ path ) ) ) ),
inference(simp,[status(thm)],[842]) ).
thf(5979,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) )
!= ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) )
| ~ $true
| ( ( empty @ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ path_cons ) )
= sk5 )
| ( ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ path_cons ) )
= sk5 ) ),
inference(paramod_ordered,[status(thm)],[4583,5908]) ).
thf(5980,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) )
!= ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) )
| ( ( empty @ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ path_cons ) )
= sk5 )
| ( ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ path_cons ) )
= sk5 ) ),
inference(simp,[status(thm)],[5979]) ).
thf(5981,plain,
( ( ( empty @ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ path_cons ) )
= sk5 )
| ( ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ path_cons ) )
= sk5 ) ),
inference(pattern_uni,[status(thm)],[5980:[]]) ).
thf(9400,plain,
( ( sk5 != sk5 )
| ( ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ path_cons ) )
!= ( empty @ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ path_cons ) ) )
| ( ( empty @ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ path_cons ) )
= sk5 ) ),
inference(eqfactor_ordered,[status(thm)],[5981]) ).
thf(9403,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) )
!= empty )
| ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) )
!= ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) ) )
| ( ( empty @ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ path_cons ) )
= sk5 ) ),
inference(simp,[status(thm)],[9400]) ).
thf(9426,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) )
!= empty )
| ( ( empty @ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ path_cons ) )
= sk5 ) ),
inference(simp,[status(thm)],[9403]) ).
thf(2079,plain,
! [B: $i,A: $i] :
( ( ( sk5 @ ( triangles @ number_of_in ) )
!= ( B @ ( A @ number_of_in ) ) )
| ( graph @ ( A @ number_of_in ) @ ( sk5 @ ( sequential_pairs @ number_of_in ) @ less_or_equal ) )
| ( sk5 @ ( sk5 @ sk7 @ on_path ) ) ),
inference(paramod_ordered,[status(thm)],[1461,33]) ).
thf(2080,plain,
( ( graph @ ( triangles @ number_of_in ) @ ( sk5 @ ( sequential_pairs @ number_of_in ) @ less_or_equal ) )
| ( sk5 @ ( sk5 @ sk7 @ on_path ) ) ),
inference(pattern_uni,[status(thm)],[2079:[bind(A,$thf( triangles )),bind(B,$thf( sk5 ))]]) ).
thf(6706,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of )
!= ( sk4 @ head_of ) )
| ( ( sk3 @ head_of )
!= sk2 )
| ~ ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) ),
inference(paramod_ordered,[status(thm)],[6610,3899]) ).
thf(6788,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) )
!= sk4 )
| ( ( sk3 @ head_of )
!= sk2 )
| ~ ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) ),
inference(simp,[status(thm)],[6706]) ).
thf(4138,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ tail_of )
!= ( sk4 @ tail_of ) )
| ( ( sk3 @ tail_of )
!= sk1 ) ),
inference(paramod_ordered,[status(thm)],[4048,3995]) ).
thf(4152,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) )
!= sk4 )
| ( ( sk3 @ tail_of )
!= sk1 ) ),
inference(simp,[status(thm)],[4138]) ).
thf(2239,plain,
! [B: $i,A: $i] :
( ( ( sk5 @ sk7 @ ( sk5 @ sk6 @ sequential ) )
!= ( B @ ( A @ sequential ) ) )
| ( A @ edge )
| ~ $true
| ( ( sk5 @ ( triangles @ number_of_in ) )
= ( sk5 @ ( sequential_pairs @ number_of_in ) ) ) ),
inference(paramod_ordered,[status(thm)],[1420,53]) ).
thf(2240,plain,
! [B: $i,A: $i] :
( ( ( sk5 @ sk7 @ ( sk5 @ sk6 @ sequential ) )
!= ( B @ ( A @ sequential ) ) )
| ( A @ edge )
| ( ( sk5 @ ( triangles @ number_of_in ) )
= ( sk5 @ ( sequential_pairs @ number_of_in ) ) ) ),
inference(simp,[status(thm)],[2239]) ).
thf(2241,plain,
( ( sk5 @ sk6 @ edge )
| ( ( sk5 @ ( triangles @ number_of_in ) )
= ( sk5 @ ( sequential_pairs @ number_of_in ) ) ) ),
inference(pattern_uni,[status(thm)],[2240:[bind(A,$thf( sk5 @ sk6 )),bind(B,$thf( sk5 @ sk7 ))]]) ).
thf(2356,plain,
( ( ( sk5 @ ( triangles @ number_of_in ) )
!= ( sk5 @ ( edges @ number_of_in ) ) )
| ( sk5 @ sk6 @ edge )
| ( ( sk5 @ ( sequential_pairs @ number_of_in ) )
= ( sk5 @ length_of ) ) ),
inference(paramod_ordered,[status(thm)],[1434,2241]) ).
thf(2372,plain,
( ( sk5 != sk5 )
| ( triangles != edges )
| ( sk5 @ sk6 @ edge )
| ( ( sk5 @ ( sequential_pairs @ number_of_in ) )
= ( sk5 @ length_of ) ) ),
inference(simp,[status(thm)],[2356]) ).
thf(2384,plain,
( ( triangles != edges )
| ( sk5 @ sk6 @ edge )
| ( ( sk5 @ ( sequential_pairs @ number_of_in ) )
= ( sk5 @ length_of ) ) ),
inference(simp,[status(thm)],[2372]) ).
thf(3224,plain,
! [B: $i,A: $i] :
( ( ( sk5 @ ( sequential_pairs @ number_of_in ) )
!= ( B @ ( A @ number_of_in ) ) )
| ( graph @ ( A @ number_of_in ) @ ( sk5 @ length_of @ less_or_equal ) )
| ( triangles != edges )
| ( sk5 @ sk6 @ edge ) ),
inference(paramod_ordered,[status(thm)],[2384,33]) ).
thf(3225,plain,
( ( graph @ ( sequential_pairs @ number_of_in ) @ ( sk5 @ length_of @ less_or_equal ) )
| ( triangles != edges )
| ( sk5 @ sk6 @ edge ) ),
inference(pattern_uni,[status(thm)],[3224:[bind(A,$thf( sequential_pairs )),bind(B,$thf( sk5 ))]]) ).
thf(6258,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) )
!= ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) )
| ~ $true
| ( ( empty @ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ path_cons ) )
= sk5 )
| ( ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ ( edges @ number_of_in ) )
= ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ length_of ) ) ),
inference(paramod_ordered,[status(thm)],[5687,5908]) ).
thf(6259,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) )
!= ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) )
| ( ( empty @ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ path_cons ) )
= sk5 )
| ( ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ ( edges @ number_of_in ) )
= ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ length_of ) ) ),
inference(simp,[status(thm)],[6258]) ).
thf(6260,plain,
( ( ( empty @ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ path_cons ) )
= sk5 )
| ( ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ ( edges @ number_of_in ) )
= ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ length_of ) ) ),
inference(pattern_uni,[status(thm)],[6259:[]]) ).
thf(2351,plain,
! [B: $i,A: $i] :
( ( ( sk5 @ ( triangles @ number_of_in ) )
!= ( B @ ( A @ number_of_in ) ) )
| ( graph @ ( A @ number_of_in ) @ ( sk5 @ ( sequential_pairs @ number_of_in ) @ less_or_equal ) )
| ( sk5 @ sk6 @ edge ) ),
inference(paramod_ordered,[status(thm)],[2241,33]) ).
thf(2352,plain,
( ( graph @ ( triangles @ number_of_in ) @ ( sk5 @ ( sequential_pairs @ number_of_in ) @ less_or_equal ) )
| ( sk5 @ sk6 @ edge ) ),
inference(pattern_uni,[status(thm)],[2351:[bind(A,$thf( triangles )),bind(B,$thf( sk5 ))]]) ).
thf(2634,plain,
( ( ( sk5 @ ( triangles @ number_of_in ) )
!= ( graph @ ( triangles @ number_of_in ) ) )
| ( sk5 @ ( sequential_pairs @ number_of_in ) @ ( sk5 @ ( sequential_pairs @ number_of_in ) @ less_or_equal ) )
| ( sk5 @ sk6 @ edge )
| ( sk5 @ sk6 @ edge ) ),
inference(paramod_ordered,[status(thm)],[2241,2352]) ).
thf(2635,plain,
( ( ( sk5 @ ( triangles @ number_of_in ) )
!= ( graph @ ( triangles @ number_of_in ) ) )
| ( sk5 @ ( sequential_pairs @ number_of_in ) @ ( sk5 @ ( sequential_pairs @ number_of_in ) @ less_or_equal ) )
| ( sk5 @ sk6 @ edge ) ),
inference(simp,[status(thm)],[2634]) ).
thf(2640,plain,
( ( sk5 != graph )
| ( triangles != triangles )
| ( sk5 @ ( sequential_pairs @ number_of_in ) @ ( sk5 @ ( sequential_pairs @ number_of_in ) @ less_or_equal ) )
| ( sk5 @ sk6 @ edge ) ),
inference(simp,[status(thm)],[2635]) ).
thf(2662,plain,
( ( sk5 != graph )
| ( sk5 @ ( sequential_pairs @ number_of_in ) @ ( sk5 @ ( sequential_pairs @ number_of_in ) @ less_or_equal ) )
| ( sk5 @ sk6 @ edge ) ),
inference(simp,[status(thm)],[2640]) ).
thf(2625,plain,
( ( ( sk5 @ ( edges @ number_of_in ) )
!= ( sk5 @ ( sequential_pairs @ number_of_in ) ) )
| ( graph @ ( triangles @ number_of_in ) @ ( sk5 @ length_of @ less_or_equal ) )
| ( sk5 @ sk6 @ edge ) ),
inference(paramod_ordered,[status(thm)],[1434,2352]) ).
thf(2655,plain,
( ( sk5 != sk5 )
| ( edges != sequential_pairs )
| ( graph @ ( triangles @ number_of_in ) @ ( sk5 @ length_of @ less_or_equal ) )
| ( sk5 @ sk6 @ edge ) ),
inference(simp,[status(thm)],[2625]) ).
thf(2677,plain,
( ( edges != sequential_pairs )
| ( graph @ ( triangles @ number_of_in ) @ ( sk5 @ length_of @ less_or_equal ) )
| ( sk5 @ sk6 @ edge ) ),
inference(simp,[status(thm)],[2655]) ).
thf(166,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( A @ sequential ) )
| ~ ( C @ ( B @ ( A @ triangle ) ) ) ),
inference(cnfConj,[status(thm)],[161]) ).
thf(3110,plain,
! [B: $i,A: $i] :
( ( ( sk5 @ ( triangles @ number_of_in ) )
!= ( B @ ( A @ number_of_in ) ) )
| ( graph @ ( A @ number_of_in ) @ ( sk5 @ ( sequential_pairs @ number_of_in ) @ less_or_equal ) )
| ( ( sk5 @ sk6 @ head_of )
= ( sk5 @ sk7 @ tail_of ) ) ),
inference(paramod_ordered,[status(thm)],[2231,33]) ).
thf(3111,plain,
( ( graph @ ( triangles @ number_of_in ) @ ( sk5 @ ( sequential_pairs @ number_of_in ) @ less_or_equal ) )
| ( ( sk5 @ sk6 @ head_of )
= ( sk5 @ sk7 @ tail_of ) ) ),
inference(pattern_uni,[status(thm)],[3110:[bind(A,$thf( triangles )),bind(B,$thf( sk5 ))]]) ).
thf(3495,plain,
! [B: $i,A: $i] :
( ( ( A @ head_of )
!= ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of ) )
| ( B @ tail_of @ vertex )
| ~ ( B @ ( A @ sequential ) ) ),
inference(paramod_ordered,[status(thm)],[56,3425]) ).
thf(3496,plain,
! [A: $i] :
( ( A @ tail_of @ vertex )
| ~ ( A @ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ sequential ) ) ),
inference(pattern_uni,[status(thm)],[3495:[bind(A,$thf( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) )),bind(B,$thf( B ))]]) ).
thf(3504,plain,
! [A: $i] :
( ( A @ tail_of @ vertex )
| ~ ( A @ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ sequential ) ) ),
inference(simp,[status(thm)],[3496]) ).
thf(72,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ vertex )
| ~ ( C @ ( B @ ( A @ path ) ) ) ),
inference(cnfConj,[status(thm)],[67]) ).
thf(1387,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ path ) ) )
!= ( F @ ( E @ ( D @ path ) ) ) )
| ( D @ vertex )
| ~ $true
| ~ ( C @ ( B @ ( A @ shortest_path ) ) ) ),
inference(paramod_ordered,[status(thm)],[115,72]) ).
thf(1388,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ path ) ) )
!= ( F @ ( E @ ( D @ path ) ) ) )
| ( D @ vertex )
| ~ ( C @ ( B @ ( A @ shortest_path ) ) ) ),
inference(simp,[status(thm)],[1387]) ).
thf(1389,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ vertex )
| ~ ( C @ ( B @ ( A @ shortest_path ) ) ) ),
inference(pattern_uni,[status(thm)],[1388:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( A )),bind(E,$thf( B )),bind(F,$thf( C ))]]) ).
thf(7620,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) )
!= ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) )
| ~ $true
| ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of )
= sk2 )
| ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of @ ( sk2 @ ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ sk8 ) ) @ edge ) ),
inference(paramod_ordered,[status(thm)],[5765,6610]) ).
thf(7621,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) )
!= ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) )
| ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of )
= sk2 )
| ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of @ ( sk2 @ ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ sk8 ) ) @ edge ) ),
inference(simp,[status(thm)],[7620]) ).
thf(7622,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of )
= sk2 )
| ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of @ ( sk2 @ ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ sk8 ) ) @ edge ) ),
inference(pattern_uni,[status(thm)],[7621:[]]) ).
thf(1698,plain,
( ( ( sk5 @ ( edges @ number_of_in ) )
!= ( graph @ ( edges @ number_of_in ) ) )
| ( sk5 @ length_of @ ( sk5 @ length_of @ less_or_equal ) ) ),
inference(paramod_ordered,[status(thm)],[1434,1456]) ).
thf(1701,plain,
( ( sk5 != graph )
| ( edges != edges )
| ( sk5 @ length_of @ ( sk5 @ length_of @ less_or_equal ) ) ),
inference(simp,[status(thm)],[1698]) ).
thf(1707,plain,
( ( sk5 != graph )
| ( sk5 @ length_of @ ( sk5 @ length_of @ less_or_equal ) ) ),
inference(simp,[status(thm)],[1701]) ).
thf(6726,plain,
! [A: $i] :
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of )
!= ( sk4 @ head_of ) )
| ( ( A @ head_of )
!= sk2 )
| ( ( A @ tail_of )
!= ( sk3 @ tail_of ) )
| ~ ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) ),
inference(paramod_ordered,[status(thm)],[6610,3059]) ).
thf(6789,plain,
! [A: $i] :
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of )
!= ( sk4 @ head_of ) )
| ( ( A @ head_of )
!= sk2 )
| ( A != sk3 )
| ~ ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) ),
inference(simp,[status(thm)],[6726]) ).
thf(6794,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of )
!= ( sk4 @ head_of ) )
| ( ( sk3 @ head_of )
!= sk2 )
| ~ ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) ),
inference(simp,[status(thm)],[6789]) ).
thf(1462,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ path ) ) )
!= ( C @ ( B @ ( A @ path ) ) ) )
| ( A @ vertex )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1404,72]) ).
thf(1463,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ path ) ) )
!= ( C @ ( B @ ( A @ path ) ) ) )
| ( A @ vertex ) ),
inference(simp,[status(thm)],[1462]) ).
thf(1464,plain,
sk1 @ vertex,
inference(pattern_uni,[status(thm)],[1463:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 )),bind(C,$thf( sk5 ))]]) ).
thf(2234,plain,
! [A: $i] :
( ( ( sk5 @ sk7 @ ( sk5 @ sk6 @ sequential ) )
!= ( A @ ( A @ sequential ) ) )
| ~ $true
| ( ( sk5 @ ( triangles @ number_of_in ) )
= ( sk5 @ ( sequential_pairs @ number_of_in ) ) ) ),
inference(paramod_ordered,[status(thm)],[1420,60]) ).
thf(2235,plain,
! [A: $i] :
( ( ( sk5 @ sk7 @ ( sk5 @ sk6 @ sequential ) )
!= ( A @ ( A @ sequential ) ) )
| ( ( sk5 @ ( triangles @ number_of_in ) )
= ( sk5 @ ( sequential_pairs @ number_of_in ) ) ) ),
inference(simp,[status(thm)],[2234]) ).
thf(2269,plain,
! [A: $i] :
( ( ( sk5 @ sk7 )
!= A )
| ( ( sk5 @ sk6 )
!= A )
| ( ( sk5 @ ( triangles @ number_of_in ) )
= ( sk5 @ ( sequential_pairs @ number_of_in ) ) ) ),
inference(simp,[status(thm)],[2235]) ).
thf(2298,plain,
( ( ( sk5 @ sk7 )
!= ( sk5 @ sk6 ) )
| ( ( sk5 @ ( triangles @ number_of_in ) )
= ( sk5 @ ( sequential_pairs @ number_of_in ) ) ) ),
inference(simp,[status(thm)],[2269]) ).
thf(2536,plain,
( ( ( sk5 @ ( triangles @ number_of_in ) )
!= ( sk5 @ ( edges @ number_of_in ) ) )
| ( ( sk5 @ sk7 )
!= ( sk5 @ sk6 ) )
| ( ( sk5 @ ( sequential_pairs @ number_of_in ) )
= ( sk5 @ length_of ) ) ),
inference(paramod_ordered,[status(thm)],[1434,2298]) ).
thf(2565,plain,
( ( sk5 != sk5 )
| ( triangles != edges )
| ( ( sk5 @ sk7 )
!= ( sk5 @ sk6 ) )
| ( ( sk5 @ ( sequential_pairs @ number_of_in ) )
= ( sk5 @ length_of ) ) ),
inference(simp,[status(thm)],[2536]) ).
thf(2573,plain,
( ( triangles != edges )
| ( ( sk5 @ sk7 )
!= ( sk5 @ sk6 ) )
| ( ( sk5 @ ( sequential_pairs @ number_of_in ) )
= ( sk5 @ length_of ) ) ),
inference(simp,[status(thm)],[2565]) ).
thf(1876,plain,
( ( ( sk5 @ ( triangles @ number_of_in ) )
!= ( sk5 @ ( edges @ number_of_in ) ) )
| ( sk5 @ ( sk5 @ sk6 @ on_path ) )
| ( ( sk5 @ ( sequential_pairs @ number_of_in ) )
= ( sk5 @ length_of ) ) ),
inference(paramod_ordered,[status(thm)],[1434,1426]) ).
thf(1889,plain,
( ( sk5 != sk5 )
| ( triangles != edges )
| ( sk5 @ ( sk5 @ sk6 @ on_path ) )
| ( ( sk5 @ ( sequential_pairs @ number_of_in ) )
= ( sk5 @ length_of ) ) ),
inference(simp,[status(thm)],[1876]) ).
thf(1894,plain,
( ( triangles != edges )
| ( sk5 @ ( sk5 @ sk6 @ on_path ) )
| ( ( sk5 @ ( sequential_pairs @ number_of_in ) )
= ( sk5 @ length_of ) ) ),
inference(simp,[status(thm)],[1889]) ).
thf(76,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ ( A @ ( B @ ( C @ sk9 ) ) )
| ( C
!= ( D @ ( A @ ( B @ ( C @ sk8 ) ) @ path_cons ) ) )
| ~ ( D @ ( B @ ( A @ ( B @ ( C @ sk8 ) ) @ head_of @ path ) ) )
| ~ ( C @ ( B @ ( A @ path ) ) ) ),
inference(cnfConj,[status(thm)],[67]) ).
thf(81,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ ( A @ ( B @ ( C @ sk9 ) ) )
| ~ ( D @ ( B @ ( A @ ( B @ ( C @ sk8 ) ) @ head_of @ path ) ) )
| ~ ( C @ ( B @ ( A @ path ) ) )
| ( ( D @ ( A @ ( B @ ( C @ sk8 ) ) @ path_cons ) )
!= C ) ),
inference(lifteq,[status(thm)],[76]) ).
thf(98,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( A @ ( D @ ( E @ sk13 ) ) @ ( D @ sequential ) )
| ( A @ ( E @ ( D @ sk12 ) ) )
| ~ ( A @ ( E @ ( D @ precedes ) ) )
| ~ ( A @ ( C @ ( B @ path ) ) ) ),
inference(cnfConj,[status(thm)],[92]) ).
thf(13,axiom,
! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ ( A @ path ) ) )
<= ( ? [D: $i] :
( ( ? [E: $i] :
( ( C
= ( E @ ( D @ path_cons ) ) )
& ( E @ ( B @ ( D @ head_of @ path ) ) ) )
| ( ( C
= ( empty @ ( D @ path_cons ) ) )
& ( B
= ( D @ head_of ) ) ) )
& ( A
= ( D @ tail_of ) )
& ( D @ edge ) )
& ( B @ vertex )
& ( A @ vertex ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',path_defn) ).
thf(103,plain,
! [A: $i,B: $i,C: $i] :
( ( ? [D: $i] :
( ( ? [E: $i] :
( ( C
= ( E @ ( D @ path_cons ) ) )
& ( E @ ( B @ ( D @ head_of @ path ) ) ) )
| ( ( C
= ( empty @ ( D @ path_cons ) ) )
& ( B
= ( D @ head_of ) ) ) )
& ( A
= ( D @ tail_of ) )
& ( D @ edge ) )
& ( B @ vertex )
& ( A @ vertex ) )
=> ( C @ ( B @ ( A @ path ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[13]) ).
thf(6690,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) )
!= ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) )
| ~ $true
| ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of )
= sk2 )
| ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ ( sk2 @ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of @ path ) ) ) ),
inference(paramod_ordered,[status(thm)],[3848,6610]) ).
thf(6691,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) )
!= ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) )
| ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of )
= sk2 )
| ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ ( sk2 @ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of @ path ) ) ) ),
inference(simp,[status(thm)],[6690]) ).
thf(6692,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of )
= sk2 )
| ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ ( sk2 @ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of @ path ) ) ) ),
inference(pattern_uni,[status(thm)],[6691:[]]) ).
thf(3190,plain,
( ( ( sk5 @ ( sequential_pairs @ number_of_in ) )
!= ( sk5 @ ( sequential_pairs @ number_of_in ) ) )
| ( graph @ ( triangles @ number_of_in ) @ ( sk5 @ length_of @ less_or_equal ) )
| ( sk5 @ sk6 @ edge )
| ( triangles != edges )
| ( sk5 @ sk6 @ edge ) ),
inference(paramod_ordered,[status(thm)],[2384,2352]) ).
thf(3191,plain,
( ( ( sk5 @ ( sequential_pairs @ number_of_in ) )
!= ( sk5 @ ( sequential_pairs @ number_of_in ) ) )
| ( graph @ ( triangles @ number_of_in ) @ ( sk5 @ length_of @ less_or_equal ) )
| ( triangles != edges )
| ( sk5 @ sk6 @ edge ) ),
inference(simp,[status(thm)],[3190]) ).
thf(3192,plain,
( ( graph @ ( triangles @ number_of_in ) @ ( sk5 @ length_of @ less_or_equal ) )
| ( triangles != edges )
| ( sk5 @ sk6 @ edge ) ),
inference(pattern_uni,[status(thm)],[3191:[]]) ).
thf(16,axiom,
! [A: $i,B: $i,C: $i,D: $i] :
( ( ( C @ ( D @ on_path ) )
& ( C @ ( B @ ( A @ path ) ) ) )
=> ( ( C @ ( D @ tail_of @ in_path ) )
& ( C @ ( D @ head_of @ in_path ) )
& ( D @ edge ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',on_path_properties) ).
thf(130,plain,
! [A: $i,B: $i,C: $i,D: $i] :
( ( ( C @ ( D @ on_path ) )
& ( C @ ( B @ ( A @ path ) ) ) )
=> ( ( C @ ( D @ tail_of @ in_path ) )
& ( C @ ( D @ head_of @ in_path ) )
& ( D @ edge ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[16]) ).
thf(4230,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ tail_of )
!= ( sk3 @ tail_of ) )
| ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) )
!= sk4 )
| ( sk1 != sk1 ) ),
inference(paramod_ordered,[status(thm)],[4048,4152]) ).
thf(4231,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ tail_of )
!= ( sk3 @ tail_of ) )
| ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) )
!= sk4 ) ),
inference(simp,[status(thm)],[4230]) ).
thf(4232,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) )
!= sk3 )
| ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) )
!= sk4 ) ),
inference(simp,[status(thm)],[4231]) ).
thf(71,plain,
! [C: $i,B: $i,A: $i] :
( ( C
!= ( empty @ ( A @ ( B @ ( C @ sk8 ) ) @ path_cons ) ) )
| ( B
!= ( A @ ( B @ ( C @ sk8 ) ) @ head_of ) )
| ( A @ ( B @ ( C @ sk9 ) ) )
| ~ ( C @ ( B @ ( A @ path ) ) ) ),
inference(cnfConj,[status(thm)],[67]) ).
thf(80,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( B @ ( C @ sk9 ) ) )
| ~ ( C @ ( B @ ( A @ path ) ) )
| ( ( empty @ ( A @ ( B @ ( C @ sk8 ) ) @ path_cons ) )
!= C )
| ( ( A @ ( B @ ( C @ sk8 ) ) @ head_of )
!= B ) ),
inference(lifteq,[status(thm)],[71]) ).
thf(167,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ sequential ) )
| ~ ( C @ ( B @ ( A @ triangle ) ) ) ),
inference(cnfConj,[status(thm)],[161]) ).
thf(6702,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) )
!= ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) )
| ~ $true
| ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of )
= sk2 )
| ( ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ path_cons ) )
= sk5 ) ),
inference(paramod_ordered,[status(thm)],[4583,6610]) ).
thf(6703,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) )
!= ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) )
| ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of )
= sk2 )
| ( ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ path_cons ) )
= sk5 ) ),
inference(simp,[status(thm)],[6702]) ).
thf(6704,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of )
= sk2 )
| ( ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ path_cons ) )
= sk5 ) ),
inference(pattern_uni,[status(thm)],[6703:[]]) ).
thf(17,axiom,
! [A: $i,B: $i,C: $i,D: $i,E: $i] :
( ( ( E @ ( D @ ( C @ precedes ) ) )
& ( E @ ( B @ ( A @ shortest_path ) ) ) )
=> ~ ? [F: $i] :
( ( ( F @ head_of )
= ( D @ head_of ) )
& ( ( F @ tail_of )
= ( C @ tail_of ) )
& ( F @ edge ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',no_short_cut_edge) ).
thf(135,plain,
! [A: $i,B: $i,C: $i,D: $i,E: $i] :
( ( ( E @ ( D @ ( C @ precedes ) ) )
& ( E @ ( B @ ( A @ shortest_path ) ) ) )
=> ~ ? [F: $i] :
( ( ( F @ head_of )
= ( D @ head_of ) )
& ( ( F @ tail_of )
= ( C @ tail_of ) )
& ( F @ edge ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[17]) ).
thf(162,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( C @ sequential ) )
| ~ ( C @ ( B @ ( A @ triangle ) ) ) ),
inference(cnfConj,[status(thm)],[161]) ).
thf(7445,plain,
! [A: $i] :
( ( ( A @ head_of )
!= ( sk4 @ head_of ) )
| ( ( sk3 @ tail_of )
!= sk2 )
| ( sk1 != sk1 )
| ~ ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) )
| ~ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ ( A @ sequential ) ) ),
inference(paramod_ordered,[status(thm)],[4129,7349]) ).
thf(7446,plain,
! [A: $i] :
( ( ( A @ head_of )
!= ( sk4 @ head_of ) )
| ( ( sk3 @ tail_of )
!= sk2 )
| ~ ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) )
| ~ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ ( A @ sequential ) ) ),
inference(simp,[status(thm)],[7445]) ).
thf(7447,plain,
( ( ( sk3 @ tail_of )
!= sk2 )
| ~ ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) )
| ~ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ ( sk4 @ sequential ) ) ),
inference(pattern_uni,[status(thm)],[7446:[bind(A,$thf( sk4 ))]]) ).
thf(95,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( A @ ( E @ ( A @ ( D @ ( E @ sk13 ) ) @ precedes ) ) )
| ( A @ ( E @ ( D @ sk12 ) ) )
| ~ ( A @ ( E @ ( D @ precedes ) ) )
| ~ ( A @ ( C @ ( B @ path ) ) ) ),
inference(cnfConj,[status(thm)],[92]) ).
thf(11592,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of )
!= ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of ) )
| ( ( sk4 @ head_of )
!= sk2 )
| ( ( sk3 @ head_of )
!= sk2 )
| ~ ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) )
| ~ ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) ),
inference(paramod_ordered,[status(thm)],[6610,6794]) ).
thf(11593,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of )
!= ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of ) )
| ( ( sk4 @ head_of )
!= sk2 )
| ( ( sk3 @ head_of )
!= sk2 )
| ~ ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) ),
inference(simp,[status(thm)],[11592]) ).
thf(11594,plain,
( ( ( sk4 @ head_of )
!= sk2 )
| ( ( sk3 @ head_of )
!= sk2 )
| ~ ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) ),
inference(pattern_uni,[status(thm)],[11593:[]]) ).
thf(2786,plain,
( ( ( sk5 @ ( edges @ number_of_in ) )
!= ( sk5 @ ( sequential_pairs @ number_of_in ) ) )
| ( graph @ ( triangles @ number_of_in ) @ ( sk5 @ length_of @ less_or_equal ) )
| ( sk5 @ sk7 @ edge ) ),
inference(paramod_ordered,[status(thm)],[1434,2432]) ).
thf(2814,plain,
( ( sk5 != sk5 )
| ( edges != sequential_pairs )
| ( graph @ ( triangles @ number_of_in ) @ ( sk5 @ length_of @ less_or_equal ) )
| ( sk5 @ sk7 @ edge ) ),
inference(simp,[status(thm)],[2786]) ).
thf(2850,plain,
( ( edges != sequential_pairs )
| ( graph @ ( triangles @ number_of_in ) @ ( sk5 @ length_of @ less_or_equal ) )
| ( sk5 @ sk7 @ edge ) ),
inference(simp,[status(thm)],[2814]) ).
thf(11477,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( sk5 @ ( sk4 @ ( sk3 @ precedes ) ) )
!= ( A @ ( E @ ( D @ precedes ) ) ) )
| ( A @ ( D @ on_path ) )
| ~ $true
| ~ ( A @ ( C @ ( B @ path ) ) ) ),
inference(paramod_ordered,[status(thm)],[26,96]) ).
thf(11478,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( sk5 @ ( sk4 @ ( sk3 @ precedes ) ) )
!= ( A @ ( E @ ( D @ precedes ) ) ) )
| ( A @ ( D @ on_path ) )
| ~ ( A @ ( C @ ( B @ path ) ) ) ),
inference(simp,[status(thm)],[11477]) ).
thf(11479,plain,
! [B: $i,A: $i] :
( ( sk5 @ ( sk3 @ on_path ) )
| ~ ( sk5 @ ( B @ ( A @ path ) ) ) ),
inference(pattern_uni,[status(thm)],[11478:[bind(A,$thf( sk5 )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( sk3 )),bind(E,$thf( sk4 ))]]) ).
thf(11493,plain,
! [B: $i,A: $i] :
( ( sk5 @ ( sk3 @ on_path ) )
| ~ ( sk5 @ ( B @ ( A @ path ) ) ) ),
inference(simp,[status(thm)],[11479]) ).
thf(11516,plain,
! [B: $i,A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ path ) ) )
!= ( sk5 @ ( B @ ( A @ path ) ) ) )
| ( sk5 @ ( sk3 @ on_path ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1404,11493]) ).
thf(11517,plain,
! [B: $i,A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ path ) ) )
!= ( sk5 @ ( B @ ( A @ path ) ) ) )
| ( sk5 @ ( sk3 @ on_path ) ) ),
inference(simp,[status(thm)],[11516]) ).
thf(11518,plain,
sk5 @ ( sk3 @ on_path ),
inference(pattern_uni,[status(thm)],[11517:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 ))]]) ).
thf(158,plain,
! [A: $i] :
( ( A @ tail_of @ vertex )
| ~ ( A @ edge ) ),
inference(cnfConj,[status(thm)],[156]) ).
thf(18,axiom,
( complete
=> ! [A: $i,B: $i] :
( ( ( A != B )
& ( B @ vertex )
& ( A @ vertex ) )
=> ? [C: $i] :
( ( ( ( B
= ( C @ tail_of ) )
& ( A
= ( C @ head_of ) ) )
<~> ( ( A
= ( C @ tail_of ) )
& ( B
= ( C @ head_of ) ) ) )
& ( C @ edge ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',complete_properties) ).
thf(139,plain,
( complete
=> ! [A: $i,B: $i] :
( ( ( A != B )
& ( B @ vertex )
& ( A @ vertex ) )
=> ? [C: $i] :
( ~ ( ( ( ( A
= ( C @ tail_of ) )
& ( B
= ( C @ head_of ) ) )
=> ( ( B
= ( C @ tail_of ) )
& ( A
= ( C @ head_of ) ) ) )
& ( ( ( B
= ( C @ tail_of ) )
& ( A
= ( C @ head_of ) ) )
=> ( ( A
= ( C @ tail_of ) )
& ( B
= ( C @ head_of ) ) ) ) )
& ( C @ edge ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[18]) ).
thf(2531,plain,
! [B: $i,A: $i] :
( ( ( sk5 @ ( triangles @ number_of_in ) )
!= ( B @ ( A @ number_of_in ) ) )
| ( graph @ ( A @ number_of_in ) @ ( sk5 @ ( sequential_pairs @ number_of_in ) @ less_or_equal ) )
| ( ( sk5 @ sk7 )
!= ( sk5 @ sk6 ) ) ),
inference(paramod_ordered,[status(thm)],[2298,33]) ).
thf(2532,plain,
( ( graph @ ( triangles @ number_of_in ) @ ( sk5 @ ( sequential_pairs @ number_of_in ) @ less_or_equal ) )
| ( ( sk5 @ sk7 )
!= ( sk5 @ sk6 ) ) ),
inference(pattern_uni,[status(thm)],[2531:[bind(A,$thf( triangles )),bind(B,$thf( sk5 ))]]) ).
thf(54,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ sequential ) )
| ( ( A @ head_of )
!= ( B @ tail_of ) )
| ( A = B )
| ~ ( B @ edge )
| ~ ( A @ edge ) ),
inference(cnfConj,[status(thm)],[50]) ).
thf(57,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ sequential ) )
| ~ ( B @ edge )
| ~ ( A @ edge )
| ( ( A @ head_of )
!= ( B @ tail_of ) )
| ( A = B ) ),
inference(lifteq,[status(thm)],[54]) ).
thf(58,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ sequential ) )
| ~ ( B @ edge )
| ~ ( A @ edge )
| ( ( A @ head_of )
!= ( B @ tail_of ) )
| ( A = B ) ),
inference(simp,[status(thm)],[57]) ).
thf(3434,plain,
! [A: $i] :
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ edge )
!= ( A @ edge ) )
| ( A @ tail_of @ vertex )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[3354,158]) ).
thf(3435,plain,
! [A: $i] :
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ edge )
!= ( A @ edge ) )
| ( A @ tail_of @ vertex ) ),
inference(simp,[status(thm)],[3434]) ).
thf(3436,plain,
sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ tail_of @ vertex,
inference(pattern_uni,[status(thm)],[3435:[bind(A,$thf( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) ))]]) ).
thf(3528,plain,
! [B: $i,A: $i] :
( ( ( B @ tail_of )
!= ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ tail_of ) )
| ( A @ head_of @ vertex )
| ~ ( B @ ( A @ sequential ) ) ),
inference(paramod_ordered,[status(thm)],[56,3436]) ).
thf(3529,plain,
! [A: $i] :
( ( A @ head_of @ vertex )
| ~ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ ( A @ sequential ) ) ),
inference(pattern_uni,[status(thm)],[3528:[bind(A,$thf( A )),bind(B,$thf( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) ))]]) ).
thf(43,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( sequential_pairs @ number_of_in ) )
= ( A @ ( triangles @ number_of_in ) ) )
| ~ ( D @ ( A @ sk7 @ ( A @ sk6 @ triangle ) ) )
| ~ ( A @ ( C @ ( B @ path ) ) ) ),
inference(cnfConj,[status(thm)],[39]) ).
thf(47,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ ( D @ ( A @ sk7 @ ( A @ sk6 @ triangle ) ) )
| ~ ( A @ ( C @ ( B @ path ) ) )
| ( ( A @ ( triangles @ number_of_in ) )
= ( A @ ( sequential_pairs @ number_of_in ) ) ) ),
inference(lifteq,[status(thm)],[43]) ).
thf(1642,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ path ) ) )
!= ( A @ ( C @ ( B @ path ) ) ) )
| ~ ( D @ ( A @ sk7 @ ( A @ sk6 @ triangle ) ) )
| ~ $true
| ( ( A @ ( triangles @ number_of_in ) )
= ( A @ ( sequential_pairs @ number_of_in ) ) ) ),
inference(paramod_ordered,[status(thm)],[1404,47]) ).
thf(1643,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ path ) ) )
!= ( A @ ( C @ ( B @ path ) ) ) )
| ~ ( D @ ( A @ sk7 @ ( A @ sk6 @ triangle ) ) )
| ( ( A @ ( triangles @ number_of_in ) )
= ( A @ ( sequential_pairs @ number_of_in ) ) ) ),
inference(simp,[status(thm)],[1642]) ).
thf(1644,plain,
! [A: $i] :
( ~ ( A @ ( sk5 @ sk7 @ ( sk5 @ sk6 @ triangle ) ) )
| ( ( sk5 @ ( triangles @ number_of_in ) )
= ( sk5 @ ( sequential_pairs @ number_of_in ) ) ) ),
inference(pattern_uni,[status(thm)],[1643:[bind(A,$thf( sk5 )),bind(B,$thf( sk1 )),bind(C,$thf( sk2 ))]]) ).
thf(1661,plain,
! [A: $i] :
( ~ ( A @ ( sk5 @ sk7 @ ( sk5 @ sk6 @ triangle ) ) )
| ( ( sk5 @ ( triangles @ number_of_in ) )
= ( sk5 @ ( sequential_pairs @ number_of_in ) ) ) ),
inference(simp,[status(thm)],[1644]) ).
thf(7990,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk5 @ ( triangles @ number_of_in ) )
!= ( C @ ( B @ number_of_in ) ) )
| ( graph @ ( B @ number_of_in ) @ ( sk5 @ ( sequential_pairs @ number_of_in ) @ less_or_equal ) )
| ~ ( A @ ( sk5 @ sk7 @ ( sk5 @ sk6 @ triangle ) ) ) ),
inference(paramod_ordered,[status(thm)],[1661,33]) ).
thf(7991,plain,
! [A: $i] :
( ( graph @ ( triangles @ number_of_in ) @ ( sk5 @ ( sequential_pairs @ number_of_in ) @ less_or_equal ) )
| ~ ( A @ ( sk5 @ sk7 @ ( sk5 @ sk6 @ triangle ) ) ) ),
inference(pattern_uni,[status(thm)],[7990:[bind(A,$thf( A )),bind(B,$thf( triangles )),bind(C,$thf( sk5 ))]]) ).
thf(7632,plain,
! [A: $i] :
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of @ ( sk2 @ ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ sk8 ) ) @ edge )
!= ( A @ edge ) )
| ( A @ tail_of @ vertex )
| ~ $true
| ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) ),
inference(paramod_ordered,[status(thm)],[5765,158]) ).
thf(7633,plain,
! [A: $i] :
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of @ ( sk2 @ ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ sk8 ) ) @ edge )
!= ( A @ edge ) )
| ( A @ tail_of @ vertex )
| ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) ),
inference(simp,[status(thm)],[7632]) ).
thf(7634,plain,
( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of @ ( sk2 @ ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ sk8 ) ) @ tail_of @ vertex )
| ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) ),
inference(pattern_uni,[status(thm)],[7633:[bind(A,$thf( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of @ ( sk2 @ ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ sk8 ) ) ))]]) ).
thf(3671,plain,
( ( ( sk5 @ ( sequential_pairs @ number_of_in ) )
!= ( sk5 @ ( sequential_pairs @ number_of_in ) ) )
| ( graph @ ( triangles @ number_of_in ) @ ( sk5 @ length_of @ less_or_equal ) )
| ( sk5 @ sk7 @ edge )
| ( triangles != edges )
| ( sk5 @ sk7 @ edge ) ),
inference(paramod_ordered,[status(thm)],[2467,2432]) ).
thf(3672,plain,
( ( ( sk5 @ ( sequential_pairs @ number_of_in ) )
!= ( sk5 @ ( sequential_pairs @ number_of_in ) ) )
| ( graph @ ( triangles @ number_of_in ) @ ( sk5 @ length_of @ less_or_equal ) )
| ( triangles != edges )
| ( sk5 @ sk7 @ edge ) ),
inference(simp,[status(thm)],[3671]) ).
thf(3673,plain,
( ( graph @ ( triangles @ number_of_in ) @ ( sk5 @ length_of @ less_or_equal ) )
| ( triangles != edges )
| ( sk5 @ sk7 @ edge ) ),
inference(pattern_uni,[status(thm)],[3672:[]]) ).
thf(94,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ~ ( A @ ( E @ ( D @ sk12 ) ) )
| ( E @ ( D @ sequential ) )
| ~ ( A @ ( E @ ( D @ precedes ) ) )
| ~ ( A @ ( C @ ( B @ path ) ) ) ),
inference(cnfConj,[status(thm)],[92]) ).
thf(163,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ edge )
| ~ ( C @ ( B @ ( A @ triangle ) ) ) ),
inference(cnfConj,[status(thm)],[161]) ).
thf(1429,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ path ) ) )
!= ( C @ ( B @ ( A @ path ) ) ) )
| ~ $true
| ( ( n1 @ ( C @ length_of @ minus ) )
= ( C @ ( sequential_pairs @ number_of_in ) ) ) ),
inference(paramod_ordered,[status(thm)],[1404,31]) ).
thf(1430,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ path ) ) )
!= ( C @ ( B @ ( A @ path ) ) ) )
| ( ( n1 @ ( C @ length_of @ minus ) )
= ( C @ ( sequential_pairs @ number_of_in ) ) ) ),
inference(simp,[status(thm)],[1429]) ).
thf(1431,plain,
( ( n1 @ ( sk5 @ length_of @ minus ) )
= ( sk5 @ ( sequential_pairs @ number_of_in ) ) ),
inference(pattern_uni,[status(thm)],[1430:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 )),bind(C,$thf( sk5 ))]]) ).
thf(6716,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) )
!= ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) )
| ~ $true
| ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of )
= sk2 )
| ( ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ ( edges @ number_of_in ) )
= ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ length_of ) ) ),
inference(paramod_ordered,[status(thm)],[5687,6610]) ).
thf(6717,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) )
!= ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) )
| ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of )
= sk2 )
| ( ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ ( edges @ number_of_in ) )
= ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ length_of ) ) ),
inference(simp,[status(thm)],[6716]) ).
thf(6718,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of )
= sk2 )
| ( ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ ( edges @ number_of_in ) )
= ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ length_of ) ) ),
inference(pattern_uni,[status(thm)],[6717:[]]) ).
thf(2243,plain,
( ( ( sk5 @ ( triangles @ number_of_in ) )
!= ( sk5 @ ( edges @ number_of_in ) ) )
| ( ( sk5 @ ( sequential_pairs @ number_of_in ) )
= ( sk5 @ length_of ) )
| ( sk5 @ sk7 @ ( sk5 @ sk6 @ sequential ) ) ),
inference(paramod_ordered,[status(thm)],[1420,1434]) ).
thf(2268,plain,
( ( sk5 != sk5 )
| ( triangles != edges )
| ( ( sk5 @ ( sequential_pairs @ number_of_in ) )
= ( sk5 @ length_of ) )
| ( sk5 @ sk7 @ ( sk5 @ sk6 @ sequential ) ) ),
inference(simp,[status(thm)],[2243]) ).
thf(2297,plain,
( ( triangles != edges )
| ( ( sk5 @ ( sequential_pairs @ number_of_in ) )
= ( sk5 @ length_of ) )
| ( sk5 @ sk7 @ ( sk5 @ sk6 @ sequential ) ) ),
inference(simp,[status(thm)],[2268]) ).
thf(1399,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ path ) ) )
!= ( graph @ ( E @ ( D @ path ) ) ) )
| ( graph @ length_of @ ( F @ ( edges @ number_of_in ) @ less_or_equal ) )
| ~ $true
| ~ ( C @ ( B @ ( A @ shortest_path ) ) ) ),
inference(paramod_ordered,[status(thm)],[115,500]) ).
thf(1400,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ path ) ) )
!= ( graph @ ( E @ ( D @ path ) ) ) )
| ( graph @ length_of @ ( F @ ( edges @ number_of_in ) @ less_or_equal ) )
| ~ ( C @ ( B @ ( A @ shortest_path ) ) ) ),
inference(simp,[status(thm)],[1399]) ).
thf(1401,plain,
! [C: $i,B: $i,A: $i] :
( ( graph @ length_of @ ( C @ ( edges @ number_of_in ) @ less_or_equal ) )
| ~ ( graph @ ( B @ ( A @ shortest_path ) ) ) ),
inference(pattern_uni,[status(thm)],[1400:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( graph )),bind(D,$thf( A )),bind(E,$thf( B ))]]) ).
thf(1417,plain,
! [C: $i,B: $i,A: $i] :
( ( graph @ length_of @ ( C @ ( edges @ number_of_in ) @ less_or_equal ) )
| ~ ( graph @ ( B @ ( A @ shortest_path ) ) ) ),
inference(simp,[status(thm)],[1401]) ).
thf(22538,plain,
$false,
inference(e,[status(thm)],[4201,760,4909,6074,555,115,683,2231,120,2114,9003,3848,1426,56,500,1872,7605,2432,24,4137,37,25,7628,5765,3425,7349,125,1577,157,7862,46,93,78,29,5974,2237,4583,3934,4847,2254,1677,84,492,164,1377,61,89,7354,3899,60,6731,6684,3995,102,4712,746,28,70,21,165,33,3682,1423,7325,5655,65,97,11492,6728,1936,4048,53,5687,857,77,1461,9426,2080,96,1456,3059,3354,6788,173,4152,3225,6260,6610,2662,1434,73,2677,4685,5762,166,45,64,3111,32,34,3504,1389,44,7622,1707,5908,6794,1464,2573,86,159,1894,81,362,98,103,4818,155,6692,3192,66,130,4232,1477,7339,80,167,6704,135,5528,162,7447,1420,95,11594,2850,2298,48,5684,31,4106,72,11518,1404,5981,2352,87,158,55,139,2532,26,2384,568,58,3529,1661,536,82,7991,7634,36,79,3673,94,2241,4129,2467,47,163,1431,122,83,6718,2297,100,1417,90,111]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : GRA007+2 : TPTP v9.3.1. Bugfixed v3.2.0.
% 0.00/0.14 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.24/0.50 % Computer : n001.cluster.edu
% 0.24/0.50 % Model : x86_64 x86_64
% 0.24/0.50 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.24/0.50 % Memory : 8046.5625MB
% 0.24/0.50 % OS : Linux 6.8.0-71-generic
% 0.24/0.50 % CPULimit : 300
% 0.24/0.50 % WCLimit : 300
% 0.24/0.50 % DateTime : Fri Sep 25 13:53:25 UTC 2026
% 0.24/0.50 % CPUTime :
% 0.24/0.50 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 1.07/1.13 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 1.74/1.48 % [INFO] Parsing done (346ms).
% 2.07/1.50 % [INFO] Running in sequential loop mode.
% 3.19/2.19 % [INFO] eprover registered as external prover.
% 3.31/2.21 % [INFO] Scanning for conjecture ...
% 3.69/2.40 % [INFO] Found a conjecture (or negated_conjecture) and 18 axioms. Running axiom selection ...
% 3.93/2.54 % [INFO] Axiom selection finished. Selected 18 axioms (removed 0 axioms).
% 4.21/2.65 % [INFO] Problem is first-order (TPTP FOF).
% 4.21/2.67 % [INFO] Type checking passed.
% 4.21/2.68 % [CONFIG] Using configuration: timeout(300) with strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>. Searching for refutation ...
% 105.43/23.81 % External prover 'e' found a proof!
% 105.43/23.81 % [INFO] Killing All external provers ...
% 105.43/23.81 % Time passed: 23150ms (effective reasoning time: 22301ms)
% 105.43/23.81 % Solved by strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>
% 105.43/23.82 % Axioms used in derivation (18): path_defn, sequential_defn, graph_has_them_all, path_properties, sequential_pairs_and_triangles, edge_ends_are_vertices, no_loops, no_short_cut_edge, length_defn, triangle_defn, complete_properties, shortest_path_defn, in_path_properties, precedes_properties, on_path_properties, path_length_sequential_pairs, shortest_path_properties, precedes_defn
% 105.43/23.82 % No. of inferences in proof: 477
% 105.43/23.82 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 23150 ms resp. 22301 ms w/o parsing
% 108.24/24.27 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 108.24/24.27 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------