%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : GRA007+1 : TPTP v9.3.1. Bugfixed v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% Computer : n003.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 149.45s 41.72s
% Output : Refutation 151.54s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 31
% Syntax : Number of formulae : 758 ( 81 unt; 0 typ; 13 def)
% Number of atoms : 3052 (1000 equ; 0 cnn)
% Maximal formula atoms : 43 ( 4 avg)
% Number of connectives : 11246 (1382 ~;1484 |; 241 &;8049 @)
% ( 3 <=>; 82 =>; 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 : 42 ( 39 usr; 14 con; 0-4 aty)
% Number of variables : 1328 ( 20 ^;1246 !; 49 ?;1328 :)
% ( 0 !>; 0 ?*; 0 @-; 13 @+)
% 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(sk15_decl,type,
sk15: $i > $i > $i ).
thf(sk16_decl,type,
sk16: $i > $i > $o ).
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(sk15_def,definition,
( sk15
= ( ^ [A: $i,B: $i] :
@+[C: $i] :
( ~ ( ( ( ( B
= ( C @ tail_of ) )
& ( A
= ( C @ head_of ) ) )
=> ( ( A
= ( C @ tail_of ) )
& ( B
= ( C @ head_of ) ) ) )
& ( ( ( A
= ( C @ tail_of ) )
& ( B
= ( C @ head_of ) ) )
=> ( ( B
= ( C @ tail_of ) )
& ( A
= ( C @ head_of ) ) ) ) )
& ( C @ edge ) ) ) ) ).
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/sandbox2/benchmark/theBenchmark.p',path_properties) ).
thf(65,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(66,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)],[65]) ).
thf(69,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( B @ ( C @ sk8 ) ) @ edge )
| ~ ( C @ ( B @ ( A @ path ) ) ) ),
inference(cnfConj,[status(thm)],[66]) ).
thf(12,axiom,
! [A: $i] :
( ( A @ edge )
=> ( ( A @ head_of )
!= ( A @ tail_of ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',no_loops) ).
thf(99,plain,
! [A: $i] :
( ( A @ edge )
=> ( ( A @ head_of )
!= ( A @ tail_of ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[12]) ).
thf(100,plain,
! [A: $i] :
( ( ( A @ head_of )
!= ( A @ tail_of ) )
| ~ ( A @ edge ) ),
inference(cnf,[status(esa)],[99]) ).
thf(101,plain,
! [A: $i] :
( ~ ( A @ edge )
| ( ( A @ head_of )
!= ( A @ tail_of ) ) ),
inference(lifteq,[status(thm)],[100]) ).
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/sandbox2/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(20,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(21,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)],[20]) ).
thf(22,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)],[21]) ).
thf(24,plain,
sk5 @ ( sk2 @ ( sk1 @ shortest_path ) ),
inference(cnfConj,[status(thm)],[22]) ).
thf(25,plain,
sk5 @ ( sk4 @ ( sk3 @ precedes ) ),
inference(cnfConj,[status(thm)],[22]) ).
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/sandbox2/benchmark/theBenchmark.p',shortest_path_properties) ).
thf(60,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(61,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)],[60]) ).
thf(62,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)],[61]) ).
thf(64,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)],[62]) ).
thf(2696,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)],[25,64]) ).
thf(2697,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)],[2696]) ).
thf(2698,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)],[2697:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( sk3 )),bind(D,$thf( sk4 )),bind(E,$thf( sk5 ))]]) ).
thf(2729,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)],[2698]) ).
thf(3008,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)],[24,2729]) ).
thf(3009,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)],[3008]) ).
thf(3010,plain,
! [A: $i] :
( ( ( A @ head_of )
!= ( sk4 @ head_of ) )
| ( ( A @ tail_of )
!= ( sk3 @ tail_of ) ) ),
inference(pattern_uni,[status(thm)],[3009:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 ))]]) ).
thf(3046,plain,
! [A: $i] :
( ( ( A @ head_of )
!= ( sk4 @ head_of ) )
| ( ( A @ tail_of )
!= ( sk3 @ tail_of ) ) ),
inference(simp,[status(thm)],[3010]) ).
thf(3889,plain,
! [A: $i] :
( ( ( A @ head_of )
!= ( sk4 @ head_of ) )
| ( A != sk3 ) ),
inference(simp,[status(thm)],[3046]) ).
thf(3930,plain,
( ( sk4 @ head_of )
!= ( sk3 @ head_of ) ),
inference(simp,[status(thm)],[3889]) ).
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/sandbox2/benchmark/theBenchmark.p',shortest_path_defn) ).
thf(110,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(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 ) ) ) )
& ! [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)],[110]) ).
thf(112,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)],[111]) ).
thf(114,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ path ) ) )
| ~ ( C @ ( B @ ( A @ shortest_path ) ) ) ),
inference(cnfConj,[status(thm)],[112]) ).
thf(1379,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)],[24,114]) ).
thf(1380,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)],[1379]) ).
thf(1381,plain,
sk5 @ ( sk2 @ ( sk1 @ path ) ),
inference(pattern_uni,[status(thm)],[1380:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 )),bind(C,$thf( sk5 ))]]) ).
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/sandbox2/benchmark/theBenchmark.p',in_path_properties) ).
thf(83,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(84,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)],[83]) ).
thf(86,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)],[84]) ).
thf(8264,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)],[1381,86]) ).
thf(8265,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)],[8264]) ).
thf(8266,plain,
! [A: $i] :
( ( sk5 @ ( sk1 @ ( sk2 @ ( sk5 @ ( A @ sk11 ) ) ) @ on_path ) )
| ~ ( sk5 @ ( A @ in_path ) ) ),
inference(pattern_uni,[status(thm)],[8265:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 )),bind(C,$thf( sk5 ))]]) ).
thf(8283,plain,
! [A: $i] :
( ( sk5 @ ( sk1 @ ( sk2 @ ( sk5 @ ( A @ sk11 ) ) ) @ on_path ) )
| ~ ( sk5 @ ( A @ in_path ) ) ),
inference(simp,[status(thm)],[8266]) ).
thf(113,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ length_of @ ( C @ length_of @ less_or_equal ) )
| ~ ( D @ ( B @ ( A @ path ) ) )
| ~ ( C @ ( B @ ( A @ shortest_path ) ) ) ),
inference(cnfConj,[status(thm)],[112]) ).
thf(14427,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ shortest_path ) ) )
!= ( C @ ( B @ ( A @ shortest_path ) ) ) )
| ( D @ length_of @ ( C @ length_of @ less_or_equal ) )
| ~ ( D @ ( B @ ( A @ path ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[24,113]) ).
thf(14428,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ shortest_path ) ) )
!= ( C @ ( B @ ( A @ shortest_path ) ) ) )
| ( D @ length_of @ ( C @ length_of @ less_or_equal ) )
| ~ ( D @ ( B @ ( A @ path ) ) ) ),
inference(simp,[status(thm)],[14427]) ).
thf(14429,plain,
! [A: $i] :
( ( A @ length_of @ ( sk5 @ length_of @ less_or_equal ) )
| ~ ( A @ ( sk2 @ ( sk1 @ path ) ) ) ),
inference(pattern_uni,[status(thm)],[14428:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 )),bind(C,$thf( sk5 ))]]) ).
thf(14486,plain,
! [A: $i] :
( ( A @ length_of @ ( sk5 @ length_of @ less_or_equal ) )
| ~ ( A @ ( sk2 @ ( sk1 @ path ) ) ) ),
inference(simp,[status(thm)],[14429]) ).
thf(14555,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ path ) ) )
!= ( D @ ( sk2 @ ( sk1 @ path ) ) ) )
| ( D @ length_of @ ( sk5 @ length_of @ less_or_equal ) )
| ~ $true
| ~ ( C @ ( B @ ( A @ shortest_path ) ) ) ),
inference(paramod_ordered,[status(thm)],[114,14486]) ).
thf(14556,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ path ) ) )
!= ( D @ ( sk2 @ ( sk1 @ path ) ) ) )
| ( D @ length_of @ ( sk5 @ length_of @ less_or_equal ) )
| ~ ( C @ ( B @ ( A @ shortest_path ) ) ) ),
inference(simp,[status(thm)],[14555]) ).
thf(14557,plain,
! [A: $i] :
( ( A @ length_of @ ( sk5 @ length_of @ less_or_equal ) )
| ~ ( A @ ( sk2 @ ( sk1 @ shortest_path ) ) ) ),
inference(pattern_uni,[status(thm)],[14556:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 )),bind(C,$thf( C )),bind(D,$thf( C ))]]) ).
thf(14585,plain,
! [A: $i] :
( ( A @ length_of @ ( sk5 @ length_of @ less_or_equal ) )
| ~ ( A @ ( sk2 @ ( sk1 @ shortest_path ) ) ) ),
inference(simp,[status(thm)],[14557]) ).
thf(87,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)],[84]) ).
thf(88,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)],[87]) ).
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/sandbox2/benchmark/theBenchmark.p',precedes_properties) ).
thf(89,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(90,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)],[89]) ).
thf(91,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)],[90]) ).
thf(95,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)],[91]) ).
thf(11231,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)],[25,95]) ).
thf(11232,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)],[11231]) ).
thf(11233,plain,
! [B: $i,A: $i] :
( ( sk5 @ ( sk3 @ on_path ) )
| ~ ( sk5 @ ( B @ ( A @ path ) ) ) ),
inference(pattern_uni,[status(thm)],[11232:[bind(A,$thf( sk5 )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( sk3 )),bind(E,$thf( sk4 ))]]) ).
thf(11264,plain,
! [B: $i,A: $i] :
( ( sk5 @ ( sk3 @ on_path ) )
| ~ ( sk5 @ ( B @ ( A @ path ) ) ) ),
inference(simp,[status(thm)],[11233]) ).
thf(11292,plain,
! [B: $i,A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ path ) ) )
!= ( sk5 @ ( B @ ( A @ path ) ) ) )
| ( sk5 @ ( sk3 @ on_path ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1381,11264]) ).
thf(11293,plain,
! [B: $i,A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ path ) ) )
!= ( sk5 @ ( B @ ( A @ path ) ) ) )
| ( sk5 @ ( sk3 @ on_path ) ) ),
inference(simp,[status(thm)],[11292]) ).
thf(11294,plain,
sk5 @ ( sk3 @ on_path ),
inference(pattern_uni,[status(thm)],[11293:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 ))]]) ).
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/sandbox2/benchmark/theBenchmark.p',on_path_properties) ).
thf(129,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(130,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( D @ tail_of @ in_path ) )
| ~ ( C @ ( D @ on_path ) )
| ~ ( C @ ( B @ ( A @ path ) ) ) )
& ( ( C @ ( D @ head_of @ in_path ) )
| ~ ( C @ ( D @ on_path ) )
| ~ ( C @ ( B @ ( A @ path ) ) ) )
& ( ( D @ edge )
| ~ ( C @ ( D @ on_path ) )
| ~ ( C @ ( B @ ( A @ path ) ) ) ) ),
inference(cnf,[status(esa)],[129]) ).
thf(133,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( C @ ( D @ tail_of @ in_path ) )
| ~ ( C @ ( D @ on_path ) )
| ~ ( C @ ( B @ ( A @ path ) ) ) ),
inference(cnfConj,[status(thm)],[130]) ).
thf(23460,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ path ) ) )
!= ( C @ ( B @ ( A @ path ) ) ) )
| ( C @ ( D @ tail_of @ in_path ) )
| ~ ( C @ ( D @ on_path ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1381,133]) ).
thf(23461,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ path ) ) )
!= ( C @ ( B @ ( A @ path ) ) ) )
| ( C @ ( D @ tail_of @ in_path ) )
| ~ ( C @ ( D @ on_path ) ) ),
inference(simp,[status(thm)],[23460]) ).
thf(23462,plain,
! [A: $i] :
( ( sk5 @ ( A @ tail_of @ in_path ) )
| ~ ( sk5 @ ( A @ on_path ) ) ),
inference(pattern_uni,[status(thm)],[23461:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 )),bind(C,$thf( sk5 ))]]) ).
thf(23512,plain,
! [A: $i] :
( ( sk5 @ ( A @ tail_of @ in_path ) )
| ~ ( sk5 @ ( A @ on_path ) ) ),
inference(simp,[status(thm)],[23462]) ).
thf(27002,plain,
! [A: $i] :
( ( ( sk5 @ ( sk3 @ on_path ) )
!= ( sk5 @ ( A @ on_path ) ) )
| ( sk5 @ ( A @ tail_of @ in_path ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[11294,23512]) ).
thf(27003,plain,
! [A: $i] :
( ( ( sk5 @ ( sk3 @ on_path ) )
!= ( sk5 @ ( A @ on_path ) ) )
| ( sk5 @ ( A @ tail_of @ in_path ) ) ),
inference(simp,[status(thm)],[27002]) ).
thf(27004,plain,
sk5 @ ( sk3 @ tail_of @ in_path ),
inference(pattern_uni,[status(thm)],[27003:[bind(A,$thf( sk3 ))]]) ).
thf(27541,plain,
! [A: $i] :
( ( ( sk5 @ ( sk3 @ tail_of @ in_path ) )
!= ( sk5 @ ( A @ in_path ) ) )
| ( sk5 @ ( sk1 @ ( sk2 @ ( sk5 @ ( A @ sk11 ) ) ) @ on_path ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[27004,8283]) ).
thf(27542,plain,
! [A: $i] :
( ( ( sk5 @ ( sk3 @ tail_of @ in_path ) )
!= ( sk5 @ ( A @ in_path ) ) )
| ( sk5 @ ( sk1 @ ( sk2 @ ( sk5 @ ( A @ sk11 ) ) ) @ on_path ) ) ),
inference(simp,[status(thm)],[27541]) ).
thf(27543,plain,
sk5 @ ( sk1 @ ( sk2 @ ( sk5 @ ( sk3 @ tail_of @ sk11 ) ) ) @ on_path ),
inference(pattern_uni,[status(thm)],[27542:[bind(A,$thf( sk3 @ tail_of ))]]) ).
thf(132,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( C @ ( D @ head_of @ in_path ) )
| ~ ( C @ ( D @ on_path ) )
| ~ ( C @ ( B @ ( A @ path ) ) ) ),
inference(cnfConj,[status(thm)],[130]) ).
thf(22748,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ path ) ) )
!= ( C @ ( B @ ( A @ path ) ) ) )
| ( C @ ( D @ head_of @ in_path ) )
| ~ ( C @ ( D @ on_path ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1381,132]) ).
thf(22749,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ path ) ) )
!= ( C @ ( B @ ( A @ path ) ) ) )
| ( C @ ( D @ head_of @ in_path ) )
| ~ ( C @ ( D @ on_path ) ) ),
inference(simp,[status(thm)],[22748]) ).
thf(22750,plain,
! [A: $i] :
( ( sk5 @ ( A @ head_of @ in_path ) )
| ~ ( sk5 @ ( A @ on_path ) ) ),
inference(pattern_uni,[status(thm)],[22749:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 )),bind(C,$thf( sk5 ))]]) ).
thf(22806,plain,
! [A: $i] :
( ( sk5 @ ( A @ head_of @ in_path ) )
| ~ ( sk5 @ ( A @ on_path ) ) ),
inference(simp,[status(thm)],[22750]) ).
thf(85,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ vertex )
| ~ ( C @ ( D @ in_path ) )
| ~ ( C @ ( B @ ( A @ path ) ) ) ),
inference(cnfConj,[status(thm)],[84]) ).
thf(7774,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)],[1381,85]) ).
thf(7775,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)],[7774]) ).
thf(7776,plain,
! [A: $i] :
( ( A @ vertex )
| ~ ( sk5 @ ( A @ in_path ) ) ),
inference(pattern_uni,[status(thm)],[7775:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 )),bind(C,$thf( sk5 ))]]) ).
thf(7786,plain,
! [A: $i] :
( ( A @ vertex )
| ~ ( sk5 @ ( A @ in_path ) ) ),
inference(simp,[status(thm)],[7776]) ).
thf(24454,plain,
! [B: $i,A: $i] :
( ( ( sk5 @ ( A @ head_of @ in_path ) )
!= ( sk5 @ ( B @ in_path ) ) )
| ( B @ vertex )
| ~ $true
| ~ ( sk5 @ ( A @ on_path ) ) ),
inference(paramod_ordered,[status(thm)],[22806,7786]) ).
thf(24455,plain,
! [B: $i,A: $i] :
( ( ( sk5 @ ( A @ head_of @ in_path ) )
!= ( sk5 @ ( B @ in_path ) ) )
| ( B @ vertex )
| ~ ( sk5 @ ( A @ on_path ) ) ),
inference(simp,[status(thm)],[24454]) ).
thf(24456,plain,
! [A: $i] :
( ( A @ head_of @ vertex )
| ~ ( sk5 @ ( A @ on_path ) ) ),
inference(pattern_uni,[status(thm)],[24455:[bind(A,$thf( C )),bind(B,$thf( C @ head_of ))]]) ).
thf(24533,plain,
! [A: $i] :
( ( A @ head_of @ vertex )
| ~ ( sk5 @ ( A @ on_path ) ) ),
inference(simp,[status(thm)],[24456]) ).
thf(27838,plain,
! [A: $i] :
( ( ( sk5 @ ( sk1 @ ( sk2 @ ( sk5 @ ( sk3 @ tail_of @ sk11 ) ) ) @ on_path ) )
!= ( sk5 @ ( A @ on_path ) ) )
| ( A @ head_of @ vertex )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[27543,24533]) ).
thf(27839,plain,
! [A: $i] :
( ( ( sk5 @ ( sk1 @ ( sk2 @ ( sk5 @ ( sk3 @ tail_of @ sk11 ) ) ) @ on_path ) )
!= ( sk5 @ ( A @ on_path ) ) )
| ( A @ head_of @ vertex ) ),
inference(simp,[status(thm)],[27838]) ).
thf(27840,plain,
sk1 @ ( sk2 @ ( sk5 @ ( sk3 @ tail_of @ sk11 ) ) ) @ head_of @ vertex,
inference(pattern_uni,[status(thm)],[27839:[bind(A,$thf( sk1 @ ( sk2 @ ( sk5 @ ( sk3 @ tail_of @ sk11 ) ) ) ))]]) ).
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/sandbox2/benchmark/theBenchmark.p',sequential_pairs_and_triangles) ).
thf(36,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(37,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)],[36]) ).
thf(38,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)],[37]) ).
thf(41,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)],[38]) ).
thf(45,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)],[41]) ).
thf(1436,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)],[1381,45]) ).
thf(1437,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)],[1436]) ).
thf(1438,plain,
( ( sk5 @ sk7 @ ( sk5 @ sk6 @ sequential ) )
| ( ( sk5 @ ( triangles @ number_of_in ) )
= ( sk5 @ ( sequential_pairs @ number_of_in ) ) ) ),
inference(pattern_uni,[status(thm)],[1437:[bind(A,$thf( sk5 )),bind(B,$thf( sk1 )),bind(C,$thf( sk2 ))]]) ).
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/sandbox2/benchmark/theBenchmark.p',sequential_defn) ).
thf(47,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(48,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)],[47]) ).
thf(49,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)],[48]) ).
thf(54,plain,
! [B: $i,A: $i] :
( ( B @ edge )
| ~ ( B @ ( A @ sequential ) ) ),
inference(cnfConj,[status(thm)],[49]) ).
thf(2235,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)],[1438,54]) ).
thf(2236,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)],[2235]) ).
thf(2237,plain,
( ( sk5 @ sk7 @ edge )
| ( ( sk5 @ ( triangles @ number_of_in ) )
= ( sk5 @ ( sequential_pairs @ number_of_in ) ) ) ),
inference(pattern_uni,[status(thm)],[2236:[bind(A,$thf( sk5 @ sk6 )),bind(B,$thf( sk5 @ sk7 ))]]) ).
thf(4,axiom,
! [A: $i,B: $i] : ( graph @ ( A @ number_of_in ) @ ( B @ ( A @ number_of_in ) @ less_or_equal ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',graph_has_them_all) ).
thf(31,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(32,plain,
! [B: $i,A: $i] : ( graph @ ( A @ number_of_in ) @ ( B @ ( A @ number_of_in ) @ less_or_equal ) ),
inference(cnf,[status(esa)],[31]) ).
thf(2426,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)],[2237,32]) ).
thf(2427,plain,
( ( graph @ ( triangles @ number_of_in ) @ ( sk5 @ ( sequential_pairs @ number_of_in ) @ less_or_equal ) )
| ( sk5 @ sk7 @ edge ) ),
inference(pattern_uni,[status(thm)],[2426:[bind(A,$thf( triangles )),bind(B,$thf( sk5 ))]]) ).
thf(98,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( A @ ( E @ on_path ) )
| ~ ( A @ ( E @ ( D @ precedes ) ) )
| ~ ( A @ ( C @ ( B @ path ) ) ) ),
inference(cnfConj,[status(thm)],[91]) ).
thf(12610,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ path ) ) )
!= ( A @ ( C @ ( B @ path ) ) ) )
| ( A @ ( E @ on_path ) )
| ~ ( A @ ( E @ ( D @ precedes ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1381,98]) ).
thf(12611,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ path ) ) )
!= ( A @ ( C @ ( B @ path ) ) ) )
| ( A @ ( E @ on_path ) )
| ~ ( A @ ( E @ ( D @ precedes ) ) ) ),
inference(simp,[status(thm)],[12610]) ).
thf(12612,plain,
! [B: $i,A: $i] :
( ( sk5 @ ( B @ on_path ) )
| ~ ( sk5 @ ( B @ ( A @ precedes ) ) ) ),
inference(pattern_uni,[status(thm)],[12611:[bind(A,$thf( sk5 )),bind(B,$thf( sk1 )),bind(C,$thf( sk2 ))]]) ).
thf(12629,plain,
! [B: $i,A: $i] :
( ( sk5 @ ( B @ on_path ) )
| ~ ( sk5 @ ( B @ ( A @ precedes ) ) ) ),
inference(simp,[status(thm)],[12612]) ).
thf(52,plain,
! [B: $i,A: $i] :
( ( A @ edge )
| ~ ( B @ ( A @ sequential ) ) ),
inference(cnfConj,[status(thm)],[49]) ).
thf(2210,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)],[1438,52]) ).
thf(2211,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)],[2210]) ).
thf(2212,plain,
( ( sk5 @ sk6 @ edge )
| ( ( sk5 @ ( triangles @ number_of_in ) )
= ( sk5 @ ( sequential_pairs @ number_of_in ) ) ) ),
inference(pattern_uni,[status(thm)],[2211:[bind(A,$thf( sk5 @ sk6 )),bind(B,$thf( sk5 @ sk7 ))]]) ).
thf(2346,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)],[2212,32]) ).
thf(2347,plain,
( ( graph @ ( triangles @ number_of_in ) @ ( sk5 @ ( sequential_pairs @ number_of_in ) @ less_or_equal ) )
| ( sk5 @ sk6 @ edge ) ),
inference(pattern_uni,[status(thm)],[2346:[bind(A,$thf( triangles )),bind(B,$thf( sk5 ))]]) ).
thf(2625,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)],[2212,2347]) ).
thf(2626,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)],[2625]) ).
thf(2638,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)],[2626]) ).
thf(2659,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)],[2638]) ).
thf(50,plain,
! [B: $i,A: $i] :
( ( A != B )
| ~ ( B @ ( A @ sequential ) ) ),
inference(cnfConj,[status(thm)],[49]) ).
thf(57,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ sequential ) )
| ( A != B ) ),
inference(lifteq,[status(thm)],[50]) ).
thf(58,plain,
! [A: $i] :
~ ( A @ ( A @ sequential ) ),
inference(simp,[status(thm)],[57]) ).
thf(2251,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)],[1438,58]) ).
thf(2252,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)],[2251]) ).
thf(2260,plain,
! [A: $i] :
( ( ( sk5 @ sk7 )
!= A )
| ( ( sk5 @ sk6 )
!= A )
| ( ( sk5 @ ( triangles @ number_of_in ) )
= ( sk5 @ ( sequential_pairs @ number_of_in ) ) ) ),
inference(simp,[status(thm)],[2252]) ).
thf(2293,plain,
( ( ( sk5 @ sk7 )
!= ( sk5 @ sk6 ) )
| ( ( sk5 @ ( triangles @ number_of_in ) )
= ( sk5 @ ( sequential_pairs @ number_of_in ) ) ) ),
inference(simp,[status(thm)],[2260]) ).
thf(2526,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)],[2293,32]) ).
thf(2527,plain,
( ( graph @ ( triangles @ number_of_in ) @ ( sk5 @ ( sequential_pairs @ number_of_in ) @ less_or_equal ) )
| ( ( sk5 @ sk7 )
!= ( sk5 @ sk6 ) ) ),
inference(pattern_uni,[status(thm)],[2526:[bind(A,$thf( triangles )),bind(B,$thf( sk5 ))]]) ).
thf(68,plain,
! [C: $i,B: $i,A: $i] :
( ( A
= ( A @ ( B @ ( C @ sk8 ) ) @ tail_of ) )
| ~ ( C @ ( B @ ( A @ path ) ) ) ),
inference(cnfConj,[status(thm)],[66]) ).
thf(82,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( C @ ( B @ ( A @ path ) ) )
| ( ( A @ ( B @ ( C @ sk8 ) ) @ tail_of )
= A ) ),
inference(lifteq,[status(thm)],[68]) ).
thf(7418,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)],[1381,82]) ).
thf(7419,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)],[7418]) ).
thf(7420,plain,
( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ tail_of )
= sk1 ),
inference(pattern_uni,[status(thm)],[7419:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 )),bind(C,$thf( sk5 ))]]) ).
thf(51,plain,
! [B: $i,A: $i] :
( ( ( A @ head_of )
= ( B @ tail_of ) )
| ~ ( B @ ( A @ sequential ) ) ),
inference(cnfConj,[status(thm)],[49]) ).
thf(59,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ sequential ) )
| ( ( A @ head_of )
= ( B @ tail_of ) ) ),
inference(lifteq,[status(thm)],[51]) ).
thf(7509,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)],[7420,59]) ).
thf(7510,plain,
! [A: $i] :
( ~ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ ( A @ sequential ) )
| ( ( A @ head_of )
= sk1 ) ),
inference(pattern_uni,[status(thm)],[7509:[bind(A,$thf( A )),bind(B,$thf( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) ))]]) ).
thf(3948,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)],[59,3930]) ).
thf(3949,plain,
! [A: $i] :
( ( ( A @ tail_of )
!= ( sk3 @ head_of ) )
| ~ ( A @ ( sk4 @ sequential ) ) ),
inference(pattern_uni,[status(thm)],[3948:[bind(A,$thf( sk4 ))]]) ).
thf(3954,plain,
! [A: $i] :
( ( ( A @ tail_of )
!= ( sk3 @ head_of ) )
| ~ ( A @ ( sk4 @ sequential ) ) ),
inference(simp,[status(thm)],[3949]) ).
thf(7503,plain,
! [A: $i] :
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ tail_of )
!= ( A @ tail_of ) )
| ( ( sk3 @ head_of )
!= sk1 )
| ~ ( A @ ( sk4 @ sequential ) ) ),
inference(paramod_ordered,[status(thm)],[7420,3954]) ).
thf(7504,plain,
( ( ( sk3 @ head_of )
!= sk1 )
| ~ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ ( sk4 @ sequential ) ) ),
inference(pattern_uni,[status(thm)],[7503:[bind(A,$thf( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) ))]]) ).
thf(9436,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)],[7510,7504]) ).
thf(9437,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)],[9436]) ).
thf(9438,plain,
( ~ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ ( sk4 @ sequential ) )
| ~ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ ( sk3 @ sequential ) ) ),
inference(pattern_uni,[status(thm)],[9437:[bind(A,$thf( sk3 ))]]) ).
thf(9917,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)],[9438]) ).
thf(9918,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ ( sk4 @ sequential ) )
!= ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ ( sk3 @ sequential ) ) )
| ~ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ ( sk3 @ sequential ) ) ),
inference(simp,[status(thm)],[9917]) ).
thf(131,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ edge )
| ~ ( C @ ( D @ on_path ) )
| ~ ( C @ ( B @ ( A @ path ) ) ) ),
inference(cnfConj,[status(thm)],[130]) ).
thf(22170,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ path ) ) )
!= ( C @ ( B @ ( A @ path ) ) ) )
| ( D @ edge )
| ~ ( C @ ( D @ on_path ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1381,131]) ).
thf(22171,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ path ) ) )
!= ( C @ ( B @ ( A @ path ) ) ) )
| ( D @ edge )
| ~ ( C @ ( D @ on_path ) ) ),
inference(simp,[status(thm)],[22170]) ).
thf(22172,plain,
! [A: $i] :
( ( A @ edge )
| ~ ( sk5 @ ( A @ on_path ) ) ),
inference(pattern_uni,[status(thm)],[22171:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 )),bind(C,$thf( sk5 ))]]) ).
thf(22209,plain,
! [A: $i] :
( ( A @ edge )
| ~ ( sk5 @ ( A @ on_path ) ) ),
inference(simp,[status(thm)],[22172]) ).
thf(27879,plain,
! [A: $i] :
( ( ( sk5 @ ( sk1 @ ( sk2 @ ( sk5 @ ( sk3 @ tail_of @ sk11 ) ) ) @ on_path ) )
!= ( sk5 @ ( A @ on_path ) ) )
| ( A @ edge )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[27543,22209]) ).
thf(27880,plain,
! [A: $i] :
( ( ( sk5 @ ( sk1 @ ( sk2 @ ( sk5 @ ( sk3 @ tail_of @ sk11 ) ) ) @ on_path ) )
!= ( sk5 @ ( A @ on_path ) ) )
| ( A @ edge ) ),
inference(simp,[status(thm)],[27879]) ).
thf(27881,plain,
sk1 @ ( sk2 @ ( sk5 @ ( sk3 @ tail_of @ sk11 ) ) ) @ edge,
inference(pattern_uni,[status(thm)],[27880:[bind(A,$thf( sk1 @ ( sk2 @ ( sk5 @ ( sk3 @ tail_of @ sk11 ) ) ) ))]]) ).
thf(67,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)],[66]) ).
thf(80,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)],[67]) ).
thf(5968,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)],[1381,80]) ).
thf(5969,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)],[5968]) ).
thf(5970,plain,
( ~ ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) )
| ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of )
= sk2 ) ),
inference(pattern_uni,[status(thm)],[5969:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 )),bind(C,$thf( sk5 ))]]) ).
thf(12592,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( sk5 @ ( sk4 @ ( sk3 @ precedes ) ) )
!= ( A @ ( E @ ( D @ precedes ) ) ) )
| ( A @ ( E @ on_path ) )
| ~ $true
| ~ ( A @ ( C @ ( B @ path ) ) ) ),
inference(paramod_ordered,[status(thm)],[25,98]) ).
thf(12593,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( sk5 @ ( sk4 @ ( sk3 @ precedes ) ) )
!= ( A @ ( E @ ( D @ precedes ) ) ) )
| ( A @ ( E @ on_path ) )
| ~ ( A @ ( C @ ( B @ path ) ) ) ),
inference(simp,[status(thm)],[12592]) ).
thf(12594,plain,
! [B: $i,A: $i] :
( ( sk5 @ ( sk4 @ on_path ) )
| ~ ( sk5 @ ( B @ ( A @ path ) ) ) ),
inference(pattern_uni,[status(thm)],[12593:[bind(A,$thf( sk5 )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( sk3 )),bind(E,$thf( sk4 ))]]) ).
thf(12635,plain,
! [B: $i,A: $i] :
( ( sk5 @ ( sk4 @ on_path ) )
| ~ ( sk5 @ ( B @ ( A @ path ) ) ) ),
inference(simp,[status(thm)],[12594]) ).
thf(12657,plain,
! [B: $i,A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ path ) ) )
!= ( sk5 @ ( B @ ( A @ path ) ) ) )
| ( sk5 @ ( sk4 @ on_path ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1381,12635]) ).
thf(12658,plain,
! [B: $i,A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ path ) ) )
!= ( sk5 @ ( B @ ( A @ path ) ) ) )
| ( sk5 @ ( sk4 @ on_path ) ) ),
inference(simp,[status(thm)],[12657]) ).
thf(12659,plain,
sk5 @ ( sk4 @ on_path ),
inference(pattern_uni,[status(thm)],[12658:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 ))]]) ).
thf(22246,plain,
! [A: $i] :
( ( ( sk5 @ ( sk4 @ on_path ) )
!= ( sk5 @ ( A @ on_path ) ) )
| ( A @ edge )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[12659,22209]) ).
thf(22247,plain,
! [A: $i] :
( ( ( sk5 @ ( sk4 @ on_path ) )
!= ( sk5 @ ( A @ on_path ) ) )
| ( A @ edge ) ),
inference(simp,[status(thm)],[22246]) ).
thf(22248,plain,
sk4 @ edge,
inference(pattern_uni,[status(thm)],[22247:[bind(A,$thf( sk4 ))]]) ).
thf(22267,plain,
! [A: $i] :
( ( ( sk4 @ edge )
!= ( A @ edge ) )
| ~ $true
| ( ( A @ head_of )
!= ( A @ tail_of ) ) ),
inference(paramod_ordered,[status(thm)],[22248,101]) ).
thf(22268,plain,
! [A: $i] :
( ( ( sk4 @ edge )
!= ( A @ edge ) )
| ( ( A @ head_of )
!= ( A @ tail_of ) ) ),
inference(simp,[status(thm)],[22267]) ).
thf(22269,plain,
( ( sk4 @ head_of )
!= ( sk4 @ tail_of ) ),
inference(pattern_uni,[status(thm)],[22268:[bind(A,$thf( sk4 ))]]) ).
thf(22399,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of )
!= ( sk4 @ head_of ) )
| ( ( sk4 @ tail_of )
!= sk2 )
| ~ ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) ),
inference(paramod_ordered,[status(thm)],[5970,22269]) ).
thf(22424,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) )
!= sk4 )
| ( ( sk4 @ tail_of )
!= sk2 )
| ~ ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) ),
inference(simp,[status(thm)],[22399]) ).
thf(24530,plain,
! [A: $i] :
( ( ( sk5 @ ( sk3 @ on_path ) )
!= ( sk5 @ ( A @ on_path ) ) )
| ( sk5 @ ( A @ head_of @ in_path ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[11294,22806]) ).
thf(24531,plain,
! [A: $i] :
( ( ( sk5 @ ( sk3 @ on_path ) )
!= ( sk5 @ ( A @ on_path ) ) )
| ( sk5 @ ( A @ head_of @ in_path ) ) ),
inference(simp,[status(thm)],[24530]) ).
thf(24532,plain,
sk5 @ ( sk3 @ head_of @ in_path ),
inference(pattern_uni,[status(thm)],[24531:[bind(A,$thf( sk3 ))]]) ).
thf(24855,plain,
! [A: $i] :
( ( ( sk5 @ ( sk3 @ head_of @ in_path ) )
!= ( sk5 @ ( A @ in_path ) ) )
| ( sk5 @ ( sk1 @ ( sk2 @ ( sk5 @ ( A @ sk11 ) ) ) @ on_path ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[24532,8283]) ).
thf(24856,plain,
! [A: $i] :
( ( ( sk5 @ ( sk3 @ head_of @ in_path ) )
!= ( sk5 @ ( A @ in_path ) ) )
| ( sk5 @ ( sk1 @ ( sk2 @ ( sk5 @ ( A @ sk11 ) ) ) @ on_path ) ) ),
inference(simp,[status(thm)],[24855]) ).
thf(24857,plain,
sk5 @ ( sk1 @ ( sk2 @ ( sk5 @ ( sk3 @ head_of @ sk11 ) ) ) @ on_path ),
inference(pattern_uni,[status(thm)],[24856:[bind(A,$thf( sk3 @ head_of ))]]) ).
thf(25244,plain,
! [A: $i] :
( ( ( sk5 @ ( sk1 @ ( sk2 @ ( sk5 @ ( sk3 @ head_of @ sk11 ) ) ) @ on_path ) )
!= ( sk5 @ ( A @ on_path ) ) )
| ( A @ edge )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[24857,22209]) ).
thf(25245,plain,
! [A: $i] :
( ( ( sk5 @ ( sk1 @ ( sk2 @ ( sk5 @ ( sk3 @ head_of @ sk11 ) ) ) @ on_path ) )
!= ( sk5 @ ( A @ on_path ) ) )
| ( A @ edge ) ),
inference(simp,[status(thm)],[25244]) ).
thf(25246,plain,
sk1 @ ( sk2 @ ( sk5 @ ( sk3 @ head_of @ sk11 ) ) ) @ edge,
inference(pattern_uni,[status(thm)],[25245:[bind(A,$thf( sk1 @ ( sk2 @ ( sk5 @ ( sk3 @ head_of @ sk11 ) ) ) ))]]) ).
thf(5,axiom,
! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ ( A @ path ) ) )
=> ( ( C @ length_of )
= ( C @ ( edges @ number_of_in ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',length_defn) ).
thf(33,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(34,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ length_of )
= ( C @ ( edges @ number_of_in ) ) )
| ~ ( C @ ( B @ ( A @ path ) ) ) ),
inference(cnf,[status(esa)],[33]) ).
thf(35,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( C @ ( B @ ( A @ path ) ) )
| ( ( C @ ( edges @ number_of_in ) )
= ( C @ length_of ) ) ),
inference(lifteq,[status(thm)],[34]) ).
thf(1447,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)],[1381,35]) ).
thf(1448,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)],[1447]) ).
thf(1449,plain,
( ( sk5 @ ( edges @ number_of_in ) )
= ( sk5 @ length_of ) ),
inference(pattern_uni,[status(thm)],[1448:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 )),bind(C,$thf( sk5 ))]]) ).
thf(40,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)],[38]) ).
thf(44,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)],[40]) ).
thf(1439,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)],[1381,44]) ).
thf(1440,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)],[1439]) ).
thf(1441,plain,
( ( sk5 @ ( sk5 @ sk7 @ on_path ) )
| ( ( sk5 @ ( triangles @ number_of_in ) )
= ( sk5 @ ( sequential_pairs @ number_of_in ) ) ) ),
inference(pattern_uni,[status(thm)],[1440:[bind(A,$thf( sk5 )),bind(B,$thf( sk1 )),bind(C,$thf( sk2 ))]]) ).
thf(1879,plain,
( ( ( sk5 @ ( triangles @ number_of_in ) )
!= ( sk5 @ ( edges @ number_of_in ) ) )
| ( sk5 @ ( sk5 @ sk7 @ on_path ) )
| ( ( sk5 @ ( sequential_pairs @ number_of_in ) )
= ( sk5 @ length_of ) ) ),
inference(paramod_ordered,[status(thm)],[1449,1441]) ).
thf(1884,plain,
( ( sk5 != sk5 )
| ( triangles != edges )
| ( sk5 @ ( sk5 @ sk7 @ on_path ) )
| ( ( sk5 @ ( sequential_pairs @ number_of_in ) )
= ( sk5 @ length_of ) ) ),
inference(simp,[status(thm)],[1879]) ).
thf(1902,plain,
( ( triangles != edges )
| ( sk5 @ ( sk5 @ sk7 @ on_path ) )
| ( ( sk5 @ ( sequential_pairs @ number_of_in ) )
= ( sk5 @ length_of ) ) ),
inference(simp,[status(thm)],[1884]) ).
thf(5036,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 @ ( sk5 @ sk7 @ on_path ) ) ),
inference(paramod_ordered,[status(thm)],[1902,32]) ).
thf(5037,plain,
( ( graph @ ( sequential_pairs @ number_of_in ) @ ( sk5 @ length_of @ less_or_equal ) )
| ( triangles != edges )
| ( sk5 @ ( sk5 @ sk7 @ on_path ) ) ),
inference(pattern_uni,[status(thm)],[5036:[bind(A,$thf( sequential_pairs )),bind(B,$thf( sk5 ))]]) ).
thf(53,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ sequential ) )
| ( ( A @ head_of )
!= ( B @ tail_of ) )
| ( A = B )
| ~ ( B @ edge )
| ~ ( A @ edge ) ),
inference(cnfConj,[status(thm)],[49]) ).
thf(55,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ sequential ) )
| ~ ( B @ edge )
| ~ ( A @ edge )
| ( ( A @ head_of )
!= ( B @ tail_of ) )
| ( A = B ) ),
inference(lifteq,[status(thm)],[53]) ).
thf(56,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ sequential ) )
| ~ ( B @ edge )
| ~ ( A @ edge )
| ( ( A @ head_of )
!= ( B @ tail_of ) )
| ( A = B ) ),
inference(simp,[status(thm)],[55]) ).
thf(76,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)],[66]) ).
thf(3824,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)],[1381,76]) ).
thf(3825,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)],[3824]) ).
thf(3826,plain,
( ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ ( sk2 @ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of @ path ) ) )
| ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) ),
inference(pattern_uni,[status(thm)],[3825:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 )),bind(C,$thf( sk5 ))]]) ).
thf(18,axiom,
! [A: $i] :
( ( A @ edge )
=> ( ( A @ tail_of @ vertex )
& ( A @ head_of @ vertex ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',edge_ends_are_vertices) ).
thf(150,plain,
! [A: $i] :
( ( A @ edge )
=> ( ( A @ tail_of @ vertex )
& ( A @ head_of @ vertex ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[18]) ).
thf(151,plain,
! [A: $i] :
( ( ( A @ tail_of @ vertex )
| ~ ( A @ edge ) )
& ( ( A @ head_of @ vertex )
| ~ ( A @ edge ) ) ),
inference(cnf,[status(esa)],[150]) ).
thf(153,plain,
! [A: $i] :
( ( A @ tail_of @ vertex )
| ~ ( A @ edge ) ),
inference(cnfConj,[status(thm)],[151]) ).
thf(39,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)],[38]) ).
thf(43,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)],[39]) ).
thf(1456,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)],[1381,43]) ).
thf(1457,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)],[1456]) ).
thf(1458,plain,
( ( sk5 @ ( sk5 @ sk6 @ on_path ) )
| ( ( sk5 @ ( triangles @ number_of_in ) )
= ( sk5 @ ( sequential_pairs @ number_of_in ) ) ) ),
inference(pattern_uni,[status(thm)],[1457:[bind(A,$thf( sk5 )),bind(B,$thf( sk1 )),bind(C,$thf( sk2 ))]]) ).
thf(63,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)],[61]) ).
thf(522,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)],[25,63]) ).
thf(523,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)],[522]) ).
thf(524,plain,
! [B: $i,A: $i] :
( ~ ( sk5 @ ( sk3 @ ( sk4 @ precedes ) ) )
| ~ ( sk5 @ ( B @ ( A @ shortest_path ) ) ) ),
inference(pattern_uni,[status(thm)],[523:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( sk3 )),bind(D,$thf( sk4 )),bind(E,$thf( sk5 ))]]) ).
thf(548,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)],[24,524]) ).
thf(549,plain,
! [B: $i,A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ shortest_path ) ) )
!= ( sk5 @ ( B @ ( A @ shortest_path ) ) ) )
| ~ ( sk5 @ ( sk3 @ ( sk4 @ precedes ) ) ) ),
inference(simp,[status(thm)],[548]) ).
thf(550,plain,
~ ( sk5 @ ( sk3 @ ( sk4 @ precedes ) ) ),
inference(pattern_uni,[status(thm)],[549:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 ))]]) ).
thf(22403,plain,
! [B: $i,A: $i] :
( ( ( A @ head_of )
!= ( sk4 @ head_of ) )
| ( ( B @ tail_of )
!= ( sk4 @ tail_of ) )
| ~ ( B @ ( A @ sequential ) ) ),
inference(paramod_ordered,[status(thm)],[59,22269]) ).
thf(22404,plain,
! [A: $i] :
( ( ( A @ tail_of )
!= ( sk4 @ tail_of ) )
| ~ ( A @ ( sk4 @ sequential ) ) ),
inference(pattern_uni,[status(thm)],[22403:[bind(A,$thf( sk4 ))]]) ).
thf(22434,plain,
! [A: $i] :
( ( ( A @ tail_of )
!= ( sk4 @ tail_of ) )
| ~ ( A @ ( sk4 @ sequential ) ) ),
inference(simp,[status(thm)],[22404]) ).
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/sandbox2/benchmark/theBenchmark.p',path_length_sequential_pairs) ).
thf(28,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(29,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)],[28]) ).
thf(30,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)],[29]) ).
thf(4470,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)],[3826,30]) ).
thf(4471,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)],[4470]) ).
thf(4472,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)],[4471:[bind(A,$thf( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of )),bind(B,$thf( sk2 )),bind(C,$thf( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) ))]]) ).
thf(74,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)],[66]) ).
thf(77,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)],[74]) ).
thf(4040,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)],[1381,77]) ).
thf(4041,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)],[4040]) ).
thf(4042,plain,
( ~ ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) )
| ( ( empty @ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ path_cons ) )
= sk5 ) ),
inference(pattern_uni,[status(thm)],[4041:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 )),bind(C,$thf( sk5 ))]]) ).
thf(8163,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) )
!= ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) )
| ~ $true
| ( ( empty @ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ path_cons ) )
= sk5 )
| ( ( n1 @ ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ length_of @ minus ) )
= ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ ( sequential_pairs @ number_of_in ) ) ) ),
inference(paramod_ordered,[status(thm)],[4472,4042]) ).
thf(8164,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) )
!= ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) )
| ( ( empty @ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ path_cons ) )
= sk5 )
| ( ( n1 @ ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ length_of @ minus ) )
= ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ ( sequential_pairs @ number_of_in ) ) ) ),
inference(simp,[status(thm)],[8163]) ).
thf(8165,plain,
( ( ( empty @ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ path_cons ) )
= sk5 )
| ( ( n1 @ ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ length_of @ minus ) )
= ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ ( sequential_pairs @ number_of_in ) ) ) ),
inference(pattern_uni,[status(thm)],[8164:[]]) ).
thf(22258,plain,
! [A: $i] :
( ( ( sk5 @ ( sk3 @ on_path ) )
!= ( sk5 @ ( A @ on_path ) ) )
| ( A @ edge )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[11294,22209]) ).
thf(22259,plain,
! [A: $i] :
( ( ( sk5 @ ( sk3 @ on_path ) )
!= ( sk5 @ ( A @ on_path ) ) )
| ( A @ edge ) ),
inference(simp,[status(thm)],[22258]) ).
thf(22260,plain,
sk3 @ edge,
inference(pattern_uni,[status(thm)],[22259:[bind(A,$thf( sk3 ))]]) ).
thf(22305,plain,
! [A: $i] :
( ( ( sk3 @ edge )
!= ( A @ edge ) )
| ~ $true
| ( ( A @ head_of )
!= ( A @ tail_of ) ) ),
inference(paramod_ordered,[status(thm)],[22260,101]) ).
thf(22306,plain,
! [A: $i] :
( ( ( sk3 @ edge )
!= ( A @ edge ) )
| ( ( A @ head_of )
!= ( A @ tail_of ) ) ),
inference(simp,[status(thm)],[22305]) ).
thf(22307,plain,
( ( sk3 @ head_of )
!= ( sk3 @ tail_of ) ),
inference(pattern_uni,[status(thm)],[22306:[bind(A,$thf( sk3 ))]]) ).
thf(22456,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of )
!= ( sk3 @ head_of ) )
| ( ( sk3 @ tail_of )
!= sk2 )
| ~ ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) ),
inference(paramod_ordered,[status(thm)],[5970,22307]) ).
thf(22476,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) )
!= sk3 )
| ( ( sk3 @ tail_of )
!= sk2 )
| ~ ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) ),
inference(simp,[status(thm)],[22456]) ).
thf(152,plain,
! [A: $i] :
( ( A @ head_of @ vertex )
| ~ ( A @ edge ) ),
inference(cnfConj,[status(thm)],[151]) ).
thf(22279,plain,
! [A: $i] :
( ( ( sk4 @ edge )
!= ( A @ edge ) )
| ( A @ head_of @ vertex )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[22248,152]) ).
thf(22280,plain,
! [A: $i] :
( ( ( sk4 @ edge )
!= ( A @ edge ) )
| ( A @ head_of @ vertex ) ),
inference(simp,[status(thm)],[22279]) ).
thf(22281,plain,
sk4 @ head_of @ vertex,
inference(pattern_uni,[status(thm)],[22280:[bind(A,$thf( sk4 ))]]) ).
thf(22522,plain,
! [B: $i,A: $i] :
( ( ( A @ head_of )
!= ( sk4 @ head_of ) )
| ( B @ tail_of @ vertex )
| ~ ( B @ ( A @ sequential ) ) ),
inference(paramod_ordered,[status(thm)],[59,22281]) ).
thf(22523,plain,
! [A: $i] :
( ( A @ tail_of @ vertex )
| ~ ( A @ ( sk4 @ sequential ) ) ),
inference(pattern_uni,[status(thm)],[22522:[bind(A,$thf( sk4 ))]]) ).
thf(22564,plain,
! [A: $i] :
( ( A @ tail_of @ vertex )
| ~ ( A @ ( sk4 @ sequential ) ) ),
inference(simp,[status(thm)],[22523]) ).
thf(14453,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ path ) ) )
!= ( D @ ( B @ ( A @ path ) ) ) )
| ( D @ length_of @ ( C @ length_of @ less_or_equal ) )
| ~ $true
| ~ ( C @ ( B @ ( A @ shortest_path ) ) ) ),
inference(paramod_ordered,[status(thm)],[1381,113]) ).
thf(14454,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ path ) ) )
!= ( D @ ( B @ ( A @ path ) ) ) )
| ( D @ length_of @ ( C @ length_of @ less_or_equal ) )
| ~ ( C @ ( B @ ( A @ shortest_path ) ) ) ),
inference(simp,[status(thm)],[14453]) ).
thf(14455,plain,
! [A: $i] :
( ( sk5 @ length_of @ ( A @ length_of @ less_or_equal ) )
| ~ ( A @ ( sk2 @ ( sk1 @ shortest_path ) ) ) ),
inference(pattern_uni,[status(thm)],[14454:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 )),bind(C,$thf( C )),bind(D,$thf( sk5 ))]]) ).
thf(14483,plain,
! [A: $i] :
( ( sk5 @ length_of @ ( A @ length_of @ less_or_equal ) )
| ~ ( A @ ( sk2 @ ( sk1 @ shortest_path ) ) ) ),
inference(simp,[status(thm)],[14455]) ).
thf(4369,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)],[3826,69]) ).
thf(4370,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)],[4369]) ).
thf(4371,plain,
( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of @ ( sk2 @ ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ sk8 ) ) @ edge )
| ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) ),
inference(pattern_uni,[status(thm)],[4370:[bind(A,$thf( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of )),bind(B,$thf( sk2 )),bind(C,$thf( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) ))]]) ).
thf(26932,plain,
! [A: $i] :
( ( ( sk5 @ ( sk1 @ ( sk2 @ ( sk5 @ ( sk3 @ head_of @ sk11 ) ) ) @ on_path ) )
!= ( sk5 @ ( A @ on_path ) ) )
| ( sk5 @ ( A @ tail_of @ in_path ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[24857,23512]) ).
thf(26933,plain,
! [A: $i] :
( ( ( sk5 @ ( sk1 @ ( sk2 @ ( sk5 @ ( sk3 @ head_of @ sk11 ) ) ) @ on_path ) )
!= ( sk5 @ ( A @ on_path ) ) )
| ( sk5 @ ( A @ tail_of @ in_path ) ) ),
inference(simp,[status(thm)],[26932]) ).
thf(26934,plain,
sk5 @ ( sk1 @ ( sk2 @ ( sk5 @ ( sk3 @ head_of @ sk11 ) ) ) @ tail_of @ in_path ),
inference(pattern_uni,[status(thm)],[26933:[bind(A,$thf( sk1 @ ( sk2 @ ( sk5 @ ( sk3 @ head_of @ sk11 ) ) ) ))]]) ).
thf(72,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ vertex )
| ~ ( C @ ( B @ ( A @ path ) ) ) ),
inference(cnfConj,[status(thm)],[66]) ).
thf(1453,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ path ) ) )
!= ( C @ ( B @ ( A @ path ) ) ) )
| ( B @ vertex )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1381,72]) ).
thf(1454,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ path ) ) )
!= ( C @ ( B @ ( A @ path ) ) ) )
| ( B @ vertex ) ),
inference(simp,[status(thm)],[1453]) ).
thf(1455,plain,
sk2 @ vertex,
inference(pattern_uni,[status(thm)],[1454:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 )),bind(C,$thf( sk5 ))]]) ).
thf(19,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/sandbox2/benchmark/theBenchmark.p',triangle_defn) ).
thf(154,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)],[19]) ).
thf(155,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)],[154]) ).
thf(156,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)],[155]) ).
thf(157,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( C @ sequential ) )
| ~ ( C @ ( B @ ( A @ triangle ) ) ) ),
inference(cnfConj,[status(thm)],[156]) ).
thf(6047,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)],[3826,5970]) ).
thf(6048,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)],[6047]) ).
thf(6049,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)],[6048:[]]) ).
thf(26986,plain,
! [A: $i] :
( ( ( sk5 @ ( sk4 @ on_path ) )
!= ( sk5 @ ( A @ on_path ) ) )
| ( sk5 @ ( A @ tail_of @ in_path ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[12659,23512]) ).
thf(26987,plain,
! [A: $i] :
( ( ( sk5 @ ( sk4 @ on_path ) )
!= ( sk5 @ ( A @ on_path ) ) )
| ( sk5 @ ( A @ tail_of @ in_path ) ) ),
inference(simp,[status(thm)],[26986]) ).
thf(26988,plain,
sk5 @ ( sk4 @ tail_of @ in_path ),
inference(pattern_uni,[status(thm)],[26987:[bind(A,$thf( sk4 ))]]) ).
thf(27026,plain,
! [A: $i] :
( ( ( sk5 @ ( sk4 @ tail_of @ in_path ) )
!= ( sk5 @ ( A @ in_path ) ) )
| ( sk5 @ ( sk1 @ ( sk2 @ ( sk5 @ ( A @ sk11 ) ) ) @ on_path ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[26988,8283]) ).
thf(27027,plain,
! [A: $i] :
( ( ( sk5 @ ( sk4 @ tail_of @ in_path ) )
!= ( sk5 @ ( A @ in_path ) ) )
| ( sk5 @ ( sk1 @ ( sk2 @ ( sk5 @ ( A @ sk11 ) ) ) @ on_path ) ) ),
inference(simp,[status(thm)],[27026]) ).
thf(27028,plain,
sk5 @ ( sk1 @ ( sk2 @ ( sk5 @ ( sk4 @ tail_of @ sk11 ) ) ) @ on_path ),
inference(pattern_uni,[status(thm)],[27027:[bind(A,$thf( sk4 @ tail_of ))]]) ).
thf(42,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)],[38]) ).
thf(46,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)],[42]) ).
thf(93,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)],[91]) ).
thf(486,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)],[35,32]) ).
thf(487,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)],[486:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( edges )),bind(E,$thf( C ))]]) ).
thf(4458,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)],[3826,487]) ).
thf(4459,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)],[4458]) ).
thf(4460,plain,
( ( graph @ ( edges @ number_of_in ) @ ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ length_of @ less_or_equal ) )
| ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) ),
inference(pattern_uni,[status(thm)],[4459:[bind(A,$thf( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of )),bind(B,$thf( sk2 )),bind(C,$thf( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) ))]]) ).
thf(70,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)],[66]) ).
thf(78,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)],[70]) ).
thf(2221,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)],[1438,32]) ).
thf(2222,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)],[2221:[bind(A,$thf( triangles )),bind(B,$thf( sk5 ))]]) ).
thf(17,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/sandbox2/benchmark/theBenchmark.p',complete_properties) ).
thf(134,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)],[17]) ).
thf(135,plain,
! [B: $i,A: $i] :
( ( ( B
!= ( A @ ( B @ sk15 ) @ tail_of ) )
| ( A
!= ( A @ ( B @ sk15 ) @ head_of ) )
| ( A @ ( B @ sk16 ) )
| ( A = B )
| ~ ( B @ vertex )
| ~ ( A @ vertex )
| ~ complete )
& ( ( A
= ( A @ ( B @ sk15 ) @ tail_of ) )
| ( A @ ( B @ sk16 ) )
| ( A = B )
| ~ ( B @ vertex )
| ~ ( A @ vertex )
| ~ complete )
& ( ( B
= ( A @ ( B @ sk15 ) @ head_of ) )
| ( A @ ( B @ sk16 ) )
| ( A = B )
| ~ ( B @ vertex )
| ~ ( A @ vertex )
| ~ complete )
& ( ~ ( A @ ( B @ sk16 ) )
| ( A
!= ( A @ ( B @ sk15 ) @ tail_of ) )
| ( B
!= ( A @ ( B @ sk15 ) @ head_of ) )
| ( A = B )
| ~ ( B @ vertex )
| ~ ( A @ vertex )
| ~ complete )
& ( ~ ( A @ ( B @ sk16 ) )
| ( B
= ( A @ ( B @ sk15 ) @ tail_of ) )
| ( A = B )
| ~ ( B @ vertex )
| ~ ( A @ vertex )
| ~ complete )
& ( ~ ( A @ ( B @ sk16 ) )
| ( A
= ( A @ ( B @ sk15 ) @ head_of ) )
| ( A = B )
| ~ ( B @ vertex )
| ~ ( A @ vertex )
| ~ complete )
& ( ( A @ ( B @ sk15 ) @ edge )
| ( A = B )
| ~ ( B @ vertex )
| ~ ( A @ vertex )
| ~ complete ) ),
inference(cnf,[status(esa)],[134]) ).
thf(139,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ sk15 ) @ edge )
| ( A = B )
| ~ ( B @ vertex )
| ~ ( A @ vertex )
| ~ complete ),
inference(cnfConj,[status(thm)],[135]) ).
thf(148,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ sk15 ) @ edge )
| ~ ( B @ vertex )
| ~ ( A @ vertex )
| ~ complete
| ( A = B ) ),
inference(lifteq,[status(thm)],[139]) ).
thf(23,plain,
complete,
inference(cnfConj,[status(thm)],[22]) ).
thf(29788,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ sk15 ) @ edge )
| ~ ( B @ vertex )
| ~ ( A @ vertex )
| ~ $true
| ( A = B ) ),
inference(rewrite,[status(thm)],[148,23]) ).
thf(29789,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ sk15 ) @ edge )
| ~ ( B @ vertex )
| ~ ( A @ vertex )
| ( A = B ) ),
inference(simp,[status(thm)],[29788]) ).
thf(672,plain,
( ( ( sk5 @ ( sk3 @ ( sk4 @ precedes ) ) )
!= ( sk5 @ ( sk4 @ ( sk3 @ precedes ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[25,550]) ).
thf(673,plain,
( ( sk5 @ ( sk3 @ ( sk4 @ precedes ) ) )
!= ( sk5 @ ( sk4 @ ( sk3 @ precedes ) ) ) ),
inference(simp,[status(thm)],[672]) ).
thf(674,plain,
( ( sk5 != sk5 )
| ( sk4 != sk3 )
| ( sk4 != sk3 ) ),
inference(simp,[status(thm)],[673]) ).
thf(675,plain,
sk4 != sk3,
inference(simp,[status(thm)],[674]) ).
thf(32861,plain,
! [B: $i,A: $i] :
( ( B != sk4 )
| ( A != sk3 )
| ( A @ ( B @ sk15 ) @ edge )
| ~ ( B @ vertex )
| ~ ( A @ vertex ) ),
inference(paramod_ordered,[status(thm)],[29789,675]) ).
thf(32862,plain,
! [A: $i] :
( ( A != sk3 )
| ( A @ ( sk4 @ sk15 ) @ edge )
| ~ ( sk4 @ vertex )
| ~ ( A @ vertex ) ),
inference(pattern_uni,[status(thm)],[32861:[bind(A,$thf( A )),bind(B,$thf( sk4 ))]]) ).
thf(34883,plain,
( ( sk3 @ ( sk4 @ sk15 ) @ edge )
| ~ ( sk4 @ vertex )
| ~ ( sk3 @ vertex ) ),
inference(simp,[status(thm)],[32862]) ).
thf(22314,plain,
! [A: $i] :
( ( ( sk3 @ edge )
!= ( A @ edge ) )
| ( A @ tail_of @ vertex )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[22260,153]) ).
thf(22315,plain,
! [A: $i] :
( ( ( sk3 @ edge )
!= ( A @ edge ) )
| ( A @ tail_of @ vertex ) ),
inference(simp,[status(thm)],[22314]) ).
thf(22316,plain,
sk3 @ tail_of @ vertex,
inference(pattern_uni,[status(thm)],[22315:[bind(A,$thf( sk3 ))]]) ).
thf(27055,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ tail_of )
!= ( sk4 @ tail_of ) )
| ( sk5 @ ( sk1 @ in_path ) ) ),
inference(paramod_ordered,[status(thm)],[7420,26988]) ).
thf(27070,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) )
!= sk4 )
| ( sk5 @ ( sk1 @ in_path ) ) ),
inference(simp,[status(thm)],[27055]) ).
thf(116,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)],[112]) ).
thf(120,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)],[116]) ).
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(simp,[status(thm)],[120]) ).
thf(6052,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)],[4371,5970]) ).
thf(6053,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)],[6052]) ).
thf(6054,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)],[6053:[]]) ).
thf(3298,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)],[1381,69]) ).
thf(3299,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ path ) ) )
!= ( C @ ( B @ ( A @ path ) ) ) )
| ( A @ ( B @ ( C @ sk8 ) ) @ edge ) ),
inference(simp,[status(thm)],[3298]) ).
thf(3300,plain,
sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ edge,
inference(pattern_uni,[status(thm)],[3299:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 )),bind(C,$thf( sk5 ))]]) ).
thf(28107,plain,
! [A: $i] :
( ( ( sk1 @ ( sk2 @ ( sk5 @ ( sk3 @ tail_of @ sk11 ) ) ) @ edge )
!= ( A @ edge ) )
| ( A @ tail_of @ vertex )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[27881,153]) ).
thf(28108,plain,
! [A: $i] :
( ( ( sk1 @ ( sk2 @ ( sk5 @ ( sk3 @ tail_of @ sk11 ) ) ) @ edge )
!= ( A @ edge ) )
| ( A @ tail_of @ vertex ) ),
inference(simp,[status(thm)],[28107]) ).
thf(28109,plain,
sk1 @ ( sk2 @ ( sk5 @ ( sk3 @ tail_of @ sk11 ) ) ) @ tail_of @ vertex,
inference(pattern_uni,[status(thm)],[28108:[bind(A,$thf( sk1 @ ( sk2 @ ( sk5 @ ( sk3 @ tail_of @ sk11 ) ) ) ))]]) ).
thf(141,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ sk16 ) )
| ( A
= ( A @ ( B @ sk15 ) @ head_of ) )
| ( A = B )
| ~ ( B @ vertex )
| ~ ( A @ vertex )
| ~ complete ),
inference(cnfConj,[status(thm)],[135]) ).
thf(146,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ sk16 ) )
| ~ ( B @ vertex )
| ~ ( A @ vertex )
| ~ complete
| ( ( A @ ( B @ sk15 ) @ head_of )
= A )
| ( A = B ) ),
inference(lifteq,[status(thm)],[141]) ).
thf(27086,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ sk16 ) )
| ~ ( B @ vertex )
| ~ ( A @ vertex )
| ~ $true
| ( ( A @ ( B @ sk15 ) @ head_of )
= A )
| ( A = B ) ),
inference(rewrite,[status(thm)],[146,23]) ).
thf(27087,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ sk16 ) )
| ~ ( B @ vertex )
| ~ ( A @ vertex )
| ( ( A @ ( B @ sk15 ) @ head_of )
= A )
| ( A = B ) ),
inference(simp,[status(thm)],[27086]) ).
thf(11249,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)],[1381,95]) ).
thf(11250,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)],[11249]) ).
thf(11251,plain,
! [B: $i,A: $i] :
( ( sk5 @ ( A @ on_path ) )
| ~ ( sk5 @ ( B @ ( A @ precedes ) ) ) ),
inference(pattern_uni,[status(thm)],[11250:[bind(A,$thf( sk5 )),bind(B,$thf( sk1 )),bind(C,$thf( sk2 ))]]) ).
thf(11270,plain,
! [B: $i,A: $i] :
( ( sk5 @ ( A @ on_path ) )
| ~ ( sk5 @ ( B @ ( A @ precedes ) ) ) ),
inference(simp,[status(thm)],[11251]) ).
thf(2087,plain,
( ( ( sk5 @ ( triangles @ number_of_in ) )
!= ( sk5 @ ( edges @ number_of_in ) ) )
| ( ( sk5 @ ( sequential_pairs @ number_of_in ) )
= ( sk5 @ length_of ) )
| ( sk5 @ ( sk5 @ sk6 @ on_path ) ) ),
inference(paramod_ordered,[status(thm)],[1458,1449]) ).
thf(2091,plain,
( ( sk5 != sk5 )
| ( triangles != edges )
| ( ( sk5 @ ( sequential_pairs @ number_of_in ) )
= ( sk5 @ length_of ) )
| ( sk5 @ ( sk5 @ sk6 @ on_path ) ) ),
inference(simp,[status(thm)],[2087]) ).
thf(2103,plain,
( ( triangles != edges )
| ( ( sk5 @ ( sequential_pairs @ number_of_in ) )
= ( sk5 @ length_of ) )
| ( sk5 @ ( sk5 @ sk6 @ on_path ) ) ),
inference(simp,[status(thm)],[2091]) ).
thf(1403,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)],[114,72]) ).
thf(1404,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)],[1403]) ).
thf(1405,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ vertex )
| ~ ( C @ ( B @ ( A @ shortest_path ) ) ) ),
inference(pattern_uni,[status(thm)],[1404:[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(7479,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)],[7420,3046]) ).
thf(7524,plain,
! [A: $i] :
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) )
!= sk3 )
| ( A != sk4 )
| ( ( A @ tail_of )
!= sk1 ) ),
inference(simp,[status(thm)],[7479]) ).
thf(7533,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) )
!= sk3 )
| ( ( sk4 @ tail_of )
!= sk1 ) ),
inference(simp,[status(thm)],[7524]) ).
thf(3344,plain,
! [A: $i] :
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ edge )
!= ( A @ edge ) )
| ~ $true
| ( ( A @ head_of )
!= ( A @ tail_of ) ) ),
inference(paramod_ordered,[status(thm)],[3300,101]) ).
thf(3345,plain,
! [A: $i] :
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ edge )
!= ( A @ edge ) )
| ( ( A @ head_of )
!= ( A @ tail_of ) ) ),
inference(simp,[status(thm)],[3344]) ).
thf(3346,plain,
( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of )
!= ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ tail_of ) ),
inference(pattern_uni,[status(thm)],[3345:[bind(A,$thf( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) ))]]) ).
thf(7471,plain,
( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of )
!= sk1 ),
inference(rewrite,[status(thm)],[3346,7420]) ).
thf(2552,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)],[1449,2293]) ).
thf(2554,plain,
( ( sk5 != sk5 )
| ( triangles != edges )
| ( ( sk5 @ sk7 )
!= ( sk5 @ sk6 ) )
| ( ( sk5 @ ( sequential_pairs @ number_of_in ) )
= ( sk5 @ length_of ) ) ),
inference(simp,[status(thm)],[2552]) ).
thf(2573,plain,
( ( triangles != edges )
| ( ( sk5 @ sk7 )
!= ( sk5 @ sk6 ) )
| ( ( sk5 @ ( sequential_pairs @ number_of_in ) )
= ( sk5 @ length_of ) ) ),
inference(simp,[status(thm)],[2554]) ).
thf(6587,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 )
!= ( sk5 @ sk6 ) ) ),
inference(paramod_ordered,[status(thm)],[2573,32]) ).
thf(6588,plain,
( ( graph @ ( sequential_pairs @ number_of_in ) @ ( sk5 @ length_of @ less_or_equal ) )
| ( triangles != edges )
| ( ( sk5 @ sk7 )
!= ( sk5 @ sk6 ) ) ),
inference(pattern_uni,[status(thm)],[6587:[bind(A,$thf( sequential_pairs )),bind(B,$thf( sk5 ))]]) ).
thf(5611,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)],[4371,152]) ).
thf(5612,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)],[5611]) ).
thf(5613,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)],[5612:[bind(A,$thf( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of @ ( sk2 @ ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ sk8 ) ) ))]]) ).
thf(9586,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 ) ) @ head_of @ vertex ) ),
inference(paramod_ordered,[status(thm)],[5613,4042]) ).
thf(9587,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 ) ) @ head_of @ vertex ) ),
inference(simp,[status(thm)],[9586]) ).
thf(9588,plain,
( ( ( empty @ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ path_cons ) )
= sk5 )
| ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of @ ( sk2 @ ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ sk8 ) ) @ head_of @ vertex ) ),
inference(pattern_uni,[status(thm)],[9587:[]]) ).
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/sandbox2/benchmark/theBenchmark.p',path_defn) ).
thf(102,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(5608,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)],[4371,153]) ).
thf(5609,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)],[5608]) ).
thf(5610,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)],[5609:[bind(A,$thf( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of @ ( sk2 @ ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ sk8 ) ) ))]]) ).
thf(8997,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 ) ) @ tail_of @ vertex ) ),
inference(paramod_ordered,[status(thm)],[5610,5970]) ).
thf(8998,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 ) ) @ tail_of @ vertex ) ),
inference(simp,[status(thm)],[8997]) ).
thf(8999,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of )
= sk2 )
| ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of @ ( sk2 @ ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ sk8 ) ) @ tail_of @ vertex ) ),
inference(pattern_uni,[status(thm)],[8998:[]]) ).
thf(27570,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ tail_of )
!= ( sk3 @ tail_of ) )
| ( sk5 @ ( sk1 @ in_path ) ) ),
inference(paramod_ordered,[status(thm)],[7420,27004]) ).
thf(27585,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) )
!= sk3 )
| ( sk5 @ ( sk1 @ in_path ) ) ),
inference(simp,[status(thm)],[27570]) ).
thf(26935,plain,
! [B: $i,A: $i] :
( ( ( sk5 @ ( A @ tail_of @ in_path ) )
!= ( sk5 @ ( B @ in_path ) ) )
| ( B @ vertex )
| ~ $true
| ~ ( sk5 @ ( A @ on_path ) ) ),
inference(paramod_ordered,[status(thm)],[23512,7786]) ).
thf(26936,plain,
! [B: $i,A: $i] :
( ( ( sk5 @ ( A @ tail_of @ in_path ) )
!= ( sk5 @ ( B @ in_path ) ) )
| ( B @ vertex )
| ~ ( sk5 @ ( A @ on_path ) ) ),
inference(simp,[status(thm)],[26935]) ).
thf(26937,plain,
! [A: $i] :
( ( A @ tail_of @ vertex )
| ~ ( sk5 @ ( A @ on_path ) ) ),
inference(pattern_uni,[status(thm)],[26936:[bind(A,$thf( C )),bind(B,$thf( C @ tail_of ))]]) ).
thf(27022,plain,
! [A: $i] :
( ( A @ tail_of @ vertex )
| ~ ( sk5 @ ( A @ on_path ) ) ),
inference(simp,[status(thm)],[26937]) ).
thf(24510,plain,
! [A: $i] :
( ( ( sk5 @ ( sk4 @ on_path ) )
!= ( sk5 @ ( A @ on_path ) ) )
| ( sk5 @ ( A @ head_of @ in_path ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[12659,22806]) ).
thf(24511,plain,
! [A: $i] :
( ( ( sk5 @ ( sk4 @ on_path ) )
!= ( sk5 @ ( A @ on_path ) ) )
| ( sk5 @ ( A @ head_of @ in_path ) ) ),
inference(simp,[status(thm)],[24510]) ).
thf(24512,plain,
sk5 @ ( sk4 @ head_of @ in_path ),
inference(pattern_uni,[status(thm)],[24511:[bind(A,$thf( sk4 ))]]) ).
thf(24554,plain,
! [A: $i] :
( ( ( sk5 @ ( sk4 @ head_of @ in_path ) )
!= ( sk5 @ ( A @ in_path ) ) )
| ( sk5 @ ( sk1 @ ( sk2 @ ( sk5 @ ( A @ sk11 ) ) ) @ on_path ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[24512,8283]) ).
thf(24555,plain,
! [A: $i] :
( ( ( sk5 @ ( sk4 @ head_of @ in_path ) )
!= ( sk5 @ ( A @ in_path ) ) )
| ( sk5 @ ( sk1 @ ( sk2 @ ( sk5 @ ( A @ sk11 ) ) ) @ on_path ) ) ),
inference(simp,[status(thm)],[24554]) ).
thf(24556,plain,
sk5 @ ( sk1 @ ( sk2 @ ( sk5 @ ( sk4 @ head_of @ sk11 ) ) ) @ on_path ),
inference(pattern_uni,[status(thm)],[24555:[bind(A,$thf( sk4 @ head_of ))]]) ).
thf(24977,plain,
! [A: $i] :
( ( ( sk5 @ ( sk1 @ ( sk2 @ ( sk5 @ ( sk4 @ head_of @ sk11 ) ) ) @ on_path ) )
!= ( sk5 @ ( A @ on_path ) ) )
| ( A @ edge )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[24556,22209]) ).
thf(24978,plain,
! [A: $i] :
( ( ( sk5 @ ( sk1 @ ( sk2 @ ( sk5 @ ( sk4 @ head_of @ sk11 ) ) ) @ on_path ) )
!= ( sk5 @ ( A @ on_path ) ) )
| ( A @ edge ) ),
inference(simp,[status(thm)],[24977]) ).
thf(24979,plain,
sk1 @ ( sk2 @ ( sk5 @ ( sk4 @ head_of @ sk11 ) ) ) @ edge,
inference(pattern_uni,[status(thm)],[24978:[bind(A,$thf( sk1 @ ( sk2 @ ( sk5 @ ( sk4 @ head_of @ sk11 ) ) ) ))]]) ).
thf(4659,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)],[4460,4042]) ).
thf(4660,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)],[4659]) ).
thf(4661,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)],[4660:[]]) ).
thf(160,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ edge )
| ~ ( C @ ( B @ ( A @ triangle ) ) ) ),
inference(cnfConj,[status(thm)],[156]) ).
thf(22276,plain,
! [A: $i] :
( ( ( sk4 @ edge )
!= ( A @ edge ) )
| ( A @ tail_of @ vertex )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[22248,153]) ).
thf(22277,plain,
! [A: $i] :
( ( ( sk4 @ edge )
!= ( A @ edge ) )
| ( A @ tail_of @ vertex ) ),
inference(simp,[status(thm)],[22276]) ).
thf(22278,plain,
sk4 @ tail_of @ vertex,
inference(pattern_uni,[status(thm)],[22277:[bind(A,$thf( sk4 ))]]) ).
thf(97,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)],[91]) ).
thf(488,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)],[35,32]) ).
thf(489,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)],[488:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( graph )),bind(D,$thf( edges ))]]) ).
thf(493,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)],[489]) ).
thf(3890,plain,
! [A: $i] :
( ( A != sk4 )
| ( ( A @ tail_of )
!= ( sk3 @ tail_of ) ) ),
inference(simp,[status(thm)],[3046]) ).
thf(3931,plain,
( ( sk4 @ tail_of )
!= ( sk3 @ tail_of ) ),
inference(simp,[status(thm)],[3890]) ).
thf(22417,plain,
! [A: $i] :
( ( ( A @ head_of )
!= ( sk4 @ head_of ) )
| ( ( sk4 @ tail_of )
!= sk1 )
| ~ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ ( A @ sequential ) ) ),
inference(paramod_ordered,[status(thm)],[7510,22269]) ).
thf(22418,plain,
( ( ( sk4 @ tail_of )
!= sk1 )
| ~ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ ( sk4 @ sequential ) ) ),
inference(pattern_uni,[status(thm)],[22417:[bind(A,$thf( sk4 ))]]) ).
thf(136,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ sk16 ) )
| ( B
= ( A @ ( B @ sk15 ) @ tail_of ) )
| ( A = B )
| ~ ( B @ vertex )
| ~ ( A @ vertex )
| ~ complete ),
inference(cnfConj,[status(thm)],[135]) ).
thf(149,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ sk16 ) )
| ~ ( B @ vertex )
| ~ ( A @ vertex )
| ~ complete
| ( ( A @ ( B @ sk15 ) @ tail_of )
= B )
| ( A = B ) ),
inference(lifteq,[status(thm)],[136]) ).
thf(37711,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ sk16 ) )
| ~ ( B @ vertex )
| ~ ( A @ vertex )
| ~ $true
| ( ( A @ ( B @ sk15 ) @ tail_of )
= B )
| ( A = B ) ),
inference(rewrite,[status(thm)],[149,23]) ).
thf(37712,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ sk16 ) )
| ~ ( B @ vertex )
| ~ ( A @ vertex )
| ( ( A @ ( B @ sk15 ) @ tail_of )
= B )
| ( A = B ) ),
inference(simp,[status(thm)],[37711]) ).
thf(92,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)],[91]) ).
thf(2632,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)],[1449,2347]) ).
thf(2649,plain,
( ( sk5 != sk5 )
| ( edges != sequential_pairs )
| ( graph @ ( triangles @ number_of_in ) @ ( sk5 @ length_of @ less_or_equal ) )
| ( sk5 @ sk6 @ edge ) ),
inference(simp,[status(thm)],[2632]) ).
thf(2670,plain,
( ( edges != sequential_pairs )
| ( graph @ ( triangles @ number_of_in ) @ ( sk5 @ length_of @ less_or_equal ) )
| ( sk5 @ sk6 @ edge ) ),
inference(simp,[status(thm)],[2649]) ).
thf(1450,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)],[1381,487]) ).
thf(1451,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)],[1450]) ).
thf(1452,plain,
graph @ ( edges @ number_of_in ) @ ( sk5 @ length_of @ less_or_equal ),
inference(pattern_uni,[status(thm)],[1451:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 )),bind(C,$thf( sk5 ))]]) ).
thf(1692,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)],[35,1452]) ).
thf(1693,plain,
! [B: $i,A: $i] :
( ( graph @ length_of @ ( sk5 @ length_of @ less_or_equal ) )
| ~ ( graph @ ( B @ ( A @ path ) ) ) ),
inference(pattern_uni,[status(thm)],[1692:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( graph ))]]) ).
thf(4723,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)],[114,1693]) ).
thf(4724,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)],[4723]) ).
thf(4725,plain,
! [B: $i,A: $i] :
( ( graph @ length_of @ ( sk5 @ length_of @ less_or_equal ) )
| ~ ( graph @ ( B @ ( A @ shortest_path ) ) ) ),
inference(pattern_uni,[status(thm)],[4724:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( graph )),bind(D,$thf( A )),bind(E,$thf( B ))]]) ).
thf(3088,plain,
! [B: $i,A: $i] :
( ( ( sk5 @ sk7 @ ( sk5 @ sk6 @ sequential ) )
!= ( B @ ( A @ sequential ) ) )
| ~ $true
| ( ( A @ head_of )
= ( B @ tail_of ) )
| ( graph @ ( triangles @ number_of_in ) @ ( sk5 @ ( sequential_pairs @ number_of_in ) @ less_or_equal ) ) ),
inference(paramod_ordered,[status(thm)],[2222,59]) ).
thf(3089,plain,
! [B: $i,A: $i] :
( ( ( sk5 @ sk7 @ ( sk5 @ sk6 @ sequential ) )
!= ( B @ ( A @ sequential ) ) )
| ( ( A @ head_of )
= ( B @ tail_of ) )
| ( graph @ ( triangles @ number_of_in ) @ ( sk5 @ ( sequential_pairs @ number_of_in ) @ less_or_equal ) ) ),
inference(simp,[status(thm)],[3088]) ).
thf(3090,plain,
( ( ( sk5 @ sk6 @ head_of )
= ( sk5 @ sk7 @ tail_of ) )
| ( graph @ ( triangles @ number_of_in ) @ ( sk5 @ ( sequential_pairs @ number_of_in ) @ less_or_equal ) ) ),
inference(pattern_uni,[status(thm)],[3089:[bind(A,$thf( sk5 @ sk6 )),bind(B,$thf( sk5 @ sk7 ))]]) ).
thf(8143,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)],[4472,5970]) ).
thf(8144,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)],[8143]) ).
thf(8145,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)],[8144:[]]) ).
thf(115,plain,
! [C: $i,B: $i,A: $i] :
( ( A != B )
| ~ ( C @ ( B @ ( A @ shortest_path ) ) ) ),
inference(cnfConj,[status(thm)],[112]) ).
thf(118,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( C @ ( B @ ( A @ shortest_path ) ) )
| ( A != B ) ),
inference(lifteq,[status(thm)],[115]) ).
thf(119,plain,
! [B: $i,A: $i] :
~ ( B @ ( A @ ( A @ shortest_path ) ) ),
inference(simp,[status(thm)],[118]) ).
thf(165,plain,
! [B: $i,A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ shortest_path ) ) )
!= ( B @ ( A @ ( A @ shortest_path ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[24,119]) ).
thf(166,plain,
! [B: $i,A: $i] :
( ( sk5 @ ( sk2 @ ( sk1 @ shortest_path ) ) )
!= ( B @ ( A @ ( A @ shortest_path ) ) ) ),
inference(simp,[status(thm)],[165]) ).
thf(167,plain,
! [B: $i,A: $i] :
( ( sk5 != B )
| ( sk2 != A )
| ( sk1 != A ) ),
inference(simp,[status(thm)],[166]) ).
thf(168,plain,
sk2 != sk1,
inference(simp,[status(thm)],[167]) ).
thf(301,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)],[121,168]) ).
thf(302,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)],[301:[bind(A,$thf( sk2 ))]]) ).
thf(343,plain,
! [A: $i] :
( ( A @ ( sk1 @ ( sk2 @ shortest_path ) ) )
| ( sk2 @ ( sk1 @ ( A @ sk14 ) ) @ ( sk1 @ ( sk2 @ path ) ) )
| ~ ( A @ ( sk1 @ ( sk2 @ path ) ) ) ),
inference(simp,[status(thm)],[302]) ).
thf(414,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( sk1 @ ( A @ sk14 ) ) @ ( sk1 @ ( sk2 @ path ) ) )
!= ( D @ ( C @ ( B @ path ) ) ) )
| ( D @ ( C @ ( B @ shortest_path ) ) )
| ( B @ ( C @ ( D @ sk14 ) ) @ ( C @ ( B @ path ) ) )
| ~ $true
| ( B = C )
| ( A @ ( sk1 @ ( sk2 @ shortest_path ) ) )
| ~ ( A @ ( sk1 @ ( sk2 @ path ) ) ) ),
inference(paramod_ordered,[status(thm)],[343,121]) ).
thf(415,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( sk1 @ ( A @ sk14 ) ) @ ( sk1 @ ( sk2 @ path ) ) )
!= ( D @ ( C @ ( B @ path ) ) ) )
| ( D @ ( C @ ( B @ shortest_path ) ) )
| ( B @ ( C @ ( D @ sk14 ) ) @ ( C @ ( B @ path ) ) )
| ( B = C )
| ( A @ ( sk1 @ ( sk2 @ shortest_path ) ) )
| ~ ( A @ ( sk1 @ ( sk2 @ path ) ) ) ),
inference(simp,[status(thm)],[414]) ).
thf(416,plain,
! [A: $i] :
( ( sk2 @ ( sk1 @ ( A @ sk14 ) ) @ ( sk1 @ ( sk2 @ shortest_path ) ) )
| ( sk2 @ ( sk1 @ ( sk2 @ ( sk1 @ ( A @ sk14 ) ) @ sk14 ) ) @ ( sk1 @ ( sk2 @ path ) ) )
| ( sk2 = sk1 )
| ( A @ ( sk1 @ ( sk2 @ shortest_path ) ) )
| ~ ( A @ ( sk1 @ ( sk2 @ path ) ) ) ),
inference(pattern_uni,[status(thm)],[415:[bind(A,$thf( E )),bind(B,$thf( sk2 )),bind(C,$thf( sk1 )),bind(D,$thf( sk2 @ ( sk1 @ ( E @ sk14 ) ) ))]]) ).
thf(454,plain,
! [A: $i] :
( ( sk2 @ ( sk1 @ ( A @ sk14 ) ) @ ( sk1 @ ( sk2 @ shortest_path ) ) )
| ( sk2 @ ( sk1 @ ( sk2 @ ( sk1 @ ( A @ sk14 ) ) @ sk14 ) ) @ ( sk1 @ ( sk2 @ path ) ) )
| ( sk2 = sk1 )
| ( A @ ( sk1 @ ( sk2 @ shortest_path ) ) )
| ~ ( A @ ( sk1 @ ( sk2 @ path ) ) ) ),
inference(simp,[status(thm)],[416]) ).
thf(563,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)],[454,168]) ).
thf(607,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( C @ sk14 ) ) @ ( B @ ( A @ path ) ) )
!= ( D @ ( sk1 @ ( sk2 @ path ) ) ) )
| ( sk2 @ ( sk1 @ ( D @ sk14 ) ) @ ( sk1 @ ( sk2 @ shortest_path ) ) )
| ( sk2 @ ( sk1 @ ( sk2 @ ( sk1 @ ( D @ sk14 ) ) @ sk14 ) ) @ ( sk1 @ ( sk2 @ path ) ) )
| ( D @ ( sk1 @ ( sk2 @ shortest_path ) ) )
| ~ $true
| ( C @ ( B @ ( A @ shortest_path ) ) )
| ~ ( C @ ( B @ ( A @ path ) ) )
| ( A = B ) ),
inference(paramod_ordered,[status(thm)],[121,563]) ).
thf(608,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( C @ sk14 ) ) @ ( B @ ( A @ path ) ) )
!= ( D @ ( sk1 @ ( sk2 @ path ) ) ) )
| ( sk2 @ ( sk1 @ ( D @ sk14 ) ) @ ( sk1 @ ( sk2 @ shortest_path ) ) )
| ( sk2 @ ( sk1 @ ( sk2 @ ( sk1 @ ( D @ sk14 ) ) @ sk14 ) ) @ ( sk1 @ ( sk2 @ path ) ) )
| ( D @ ( sk1 @ ( sk2 @ shortest_path ) ) )
| ( C @ ( B @ ( A @ shortest_path ) ) )
| ~ ( C @ ( B @ ( A @ path ) ) )
| ( A = B ) ),
inference(simp,[status(thm)],[607]) ).
thf(609,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 ) ) )
| ( sk2 = sk1 ) ),
inference(pattern_uni,[status(thm)],[608:[bind(A,$thf( sk2 )),bind(B,$thf( sk1 )),bind(C,$thf( E )),bind(D,$thf( sk2 @ ( sk1 @ ( E @ sk14 ) ) ))]]) ).
thf(647,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 ) ) )
| ( sk2 = sk1 ) ),
inference(simp,[status(thm)],[609]) ).
thf(755,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)],[647,168]) ).
thf(820,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)],[755,755]) ).
thf(821,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)],[820]) ).
thf(822,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)],[821:[bind(A,$thf( I )),bind(B,$thf( sk2 @ ( sk1 @ ( sk2 @ ( sk1 @ ( sk2 @ ( sk1 @ ( I @ sk14 ) ) @ sk14 ) ) @ sk14 ) ) ))]]) ).
thf(874,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)],[822]) ).
thf(73,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)],[66]) ).
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)],[73]) ).
thf(5185,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)],[1381,79]) ).
thf(5186,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)],[5185]) ).
thf(5187,plain,
( ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) )
| ( ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ path_cons ) )
= sk5 ) ),
inference(pattern_uni,[status(thm)],[5186:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 )),bind(C,$thf( sk5 ))]]) ).
thf(6131,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)],[5187,5970]) ).
thf(6132,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)],[6131]) ).
thf(6133,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of )
= sk2 )
| ( ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ path_cons ) )
= sk5 ) ),
inference(pattern_uni,[status(thm)],[6132:[]]) ).
thf(1400,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ path ) ) )
!= ( F @ ( E @ ( D @ path ) ) ) )
| ( graph @ ( edges @ number_of_in ) @ ( F @ length_of @ less_or_equal ) )
| ~ $true
| ~ ( C @ ( B @ ( A @ shortest_path ) ) ) ),
inference(paramod_ordered,[status(thm)],[114,487]) ).
thf(1401,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ path ) ) )
!= ( F @ ( E @ ( D @ path ) ) ) )
| ( graph @ ( edges @ number_of_in ) @ ( F @ length_of @ less_or_equal ) )
| ~ ( C @ ( B @ ( A @ shortest_path ) ) ) ),
inference(simp,[status(thm)],[1400]) ).
thf(1402,plain,
! [C: $i,B: $i,A: $i] :
( ( graph @ ( edges @ number_of_in ) @ ( C @ length_of @ less_or_equal ) )
| ~ ( C @ ( B @ ( A @ shortest_path ) ) ) ),
inference(pattern_uni,[status(thm)],[1401:[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(7500,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ tail_of )
!= ( sk4 @ tail_of ) )
| ( ( sk3 @ tail_of )
!= sk1 ) ),
inference(paramod_ordered,[status(thm)],[7420,3931]) ).
thf(7519,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) )
!= sk4 )
| ( ( sk3 @ tail_of )
!= sk1 ) ),
inference(simp,[status(thm)],[7500]) ).
thf(7607,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ tail_of )
!= ( sk3 @ tail_of ) )
| ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) )
!= sk4 )
| ( sk1 != sk1 ) ),
inference(paramod_ordered,[status(thm)],[7420,7519]) ).
thf(7608,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ tail_of )
!= ( sk3 @ tail_of ) )
| ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) )
!= sk4 ) ),
inference(simp,[status(thm)],[7607]) ).
thf(7610,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) )
!= sk3 )
| ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) )
!= sk4 ) ),
inference(simp,[status(thm)],[7608]) ).
thf(22317,plain,
! [A: $i] :
( ( ( sk3 @ edge )
!= ( A @ edge ) )
| ( A @ head_of @ vertex )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[22260,152]) ).
thf(22318,plain,
! [A: $i] :
( ( ( sk3 @ edge )
!= ( A @ edge ) )
| ( A @ head_of @ vertex ) ),
inference(simp,[status(thm)],[22317]) ).
thf(22319,plain,
sk3 @ head_of @ vertex,
inference(pattern_uni,[status(thm)],[22318:[bind(A,$thf( sk3 ))]]) ).
thf(103,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ path ) ) )
| ( C
!= ( E @ ( D @ path_cons ) ) )
| ~ ( E @ ( B @ ( D @ head_of @ path ) ) )
| ( A
!= ( D @ tail_of ) )
| ~ ( D @ edge )
| ~ ( B @ vertex )
| ~ ( A @ vertex ) )
& ( ( C @ ( B @ ( A @ path ) ) )
| ( C
!= ( empty @ ( D @ path_cons ) ) )
| ( B
!= ( D @ head_of ) )
| ( A
!= ( D @ tail_of ) )
| ~ ( D @ edge )
| ~ ( B @ vertex )
| ~ ( A @ vertex ) ) ),
inference(cnf,[status(esa)],[102]) ).
thf(105,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ path ) ) )
| ( C
!= ( E @ ( D @ path_cons ) ) )
| ~ ( E @ ( B @ ( D @ head_of @ path ) ) )
| ( A
!= ( D @ tail_of ) )
| ~ ( D @ edge )
| ~ ( B @ vertex )
| ~ ( A @ vertex ) ),
inference(cnfConj,[status(thm)],[103]) ).
thf(108,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ path ) ) )
| ~ ( E @ ( B @ ( D @ head_of @ path ) ) )
| ~ ( D @ edge )
| ~ ( B @ vertex )
| ~ ( A @ vertex )
| ( C
!= ( E @ ( D @ path_cons ) ) )
| ( A
!= ( D @ tail_of ) ) ),
inference(lifteq,[status(thm)],[105]) ).
thf(109,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ path_cons ) @ ( A @ ( B @ tail_of @ path ) ) )
| ~ ( C @ ( A @ ( B @ head_of @ path ) ) )
| ~ ( B @ edge )
| ~ ( A @ vertex )
| ~ ( B @ tail_of @ vertex ) ),
inference(simp,[status(thm)],[108]) ).
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/sandbox2/benchmark/theBenchmark.p',precedes_defn) ).
thf(124,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(1459,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)],[1381,30]) ).
thf(1460,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)],[1459]) ).
thf(1461,plain,
( ( n1 @ ( sk5 @ length_of @ minus ) )
= ( sk5 @ ( sequential_pairs @ number_of_in ) ) ),
inference(pattern_uni,[status(thm)],[1460:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 )),bind(C,$thf( sk5 ))]]) ).
thf(26,plain,
! [A: $i] :
( ( ( A @ head_of )
!= ( sk3 @ tail_of ) )
| ( ( A @ tail_of )
!= ( sk4 @ head_of ) )
| ~ ( A @ edge ) ),
inference(cnfConj,[status(thm)],[22]) ).
thf(27,plain,
! [A: $i] :
( ~ ( A @ edge )
| ( ( A @ head_of )
!= ( sk3 @ tail_of ) )
| ( ( A @ tail_of )
!= ( sk4 @ head_of ) ) ),
inference(lifteq,[status(thm)],[26]) ).
thf(3381,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)],[3300,27]) ).
thf(3382,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)],[3381]) ).
thf(3383,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of )
!= ( sk3 @ tail_of ) )
| ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ tail_of )
!= ( sk4 @ head_of ) ) ),
inference(pattern_uni,[status(thm)],[3382:[bind(A,$thf( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) ))]]) ).
thf(7472,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of )
!= ( sk3 @ tail_of ) )
| ( ( sk4 @ head_of )
!= sk1 ) ),
inference(rewrite,[status(thm)],[3383,7420]) ).
thf(9417,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)],[7510,7472]) ).
thf(9418,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)],[9417]) ).
thf(9419,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of )
!= ( sk3 @ tail_of ) )
| ~ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ ( sk4 @ sequential ) ) ),
inference(pattern_uni,[status(thm)],[9418:[bind(A,$thf( sk4 ))]]) ).
thf(24972,plain,
! [A: $i] :
( ( ( sk5 @ ( sk1 @ ( sk2 @ ( sk5 @ ( sk4 @ head_of @ sk11 ) ) ) @ on_path ) )
!= ( sk5 @ ( A @ on_path ) ) )
| ( sk5 @ ( A @ head_of @ in_path ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[24556,22806]) ).
thf(24973,plain,
! [A: $i] :
( ( ( sk5 @ ( sk1 @ ( sk2 @ ( sk5 @ ( sk4 @ head_of @ sk11 ) ) ) @ on_path ) )
!= ( sk5 @ ( A @ on_path ) ) )
| ( sk5 @ ( A @ head_of @ in_path ) ) ),
inference(simp,[status(thm)],[24972]) ).
thf(24974,plain,
sk5 @ ( sk1 @ ( sk2 @ ( sk5 @ ( sk4 @ head_of @ sk11 ) ) ) @ head_of @ in_path ),
inference(pattern_uni,[status(thm)],[24973:[bind(A,$thf( sk1 @ ( sk2 @ ( sk5 @ ( sk4 @ head_of @ sk11 ) ) ) ))]]) ).
thf(5385,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)],[5187,4042]) ).
thf(5386,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)],[5385]) ).
thf(5387,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)],[5386:[]]) ).
thf(96,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)],[91]) ).
thf(4455,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)],[3826,35]) ).
thf(4456,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)],[4455]) ).
thf(4457,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ ( edges @ number_of_in ) )
= ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ length_of ) )
| ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) ),
inference(pattern_uni,[status(thm)],[4456:[bind(A,$thf( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of )),bind(B,$thf( sk2 )),bind(C,$thf( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) ))]]) ).
thf(32859,plain,
! [B: $i,A: $i] :
( ( A != sk4 )
| ( B != sk3 )
| ( A @ ( B @ sk15 ) @ edge )
| ~ ( B @ vertex )
| ~ ( A @ vertex ) ),
inference(paramod_ordered,[status(thm)],[29789,675]) ).
thf(32860,plain,
! [A: $i] :
( ( A != sk3 )
| ( sk4 @ ( A @ sk15 ) @ edge )
| ~ ( A @ vertex )
| ~ ( sk4 @ vertex ) ),
inference(pattern_uni,[status(thm)],[32859:[bind(A,$thf( sk4 ))]]) ).
thf(34882,plain,
( ( sk4 @ ( sk3 @ sk15 ) @ edge )
| ~ ( sk3 @ vertex )
| ~ ( sk4 @ vertex ) ),
inference(simp,[status(thm)],[32860]) ).
thf(71,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ vertex )
| ~ ( C @ ( B @ ( A @ path ) ) ) ),
inference(cnfConj,[status(thm)],[66]) ).
thf(1391,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)],[114,71]) ).
thf(1392,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)],[1391]) ).
thf(1393,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ vertex )
| ~ ( C @ ( B @ ( A @ shortest_path ) ) ) ),
inference(pattern_uni,[status(thm)],[1392:[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(6531,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 )
!= ( sk5 @ sk6 ) )
| ( triangles != edges )
| ( ( sk5 @ sk7 )
!= ( sk5 @ sk6 ) ) ),
inference(paramod_ordered,[status(thm)],[2573,2527]) ).
thf(6532,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 )
!= ( sk5 @ sk6 ) ) ),
inference(simp,[status(thm)],[6531]) ).
thf(6533,plain,
( ( graph @ ( triangles @ number_of_in ) @ ( sk5 @ length_of @ less_or_equal ) )
| ( triangles != edges )
| ( ( sk5 @ sk7 )
!= ( sk5 @ sk6 ) ) ),
inference(pattern_uni,[status(thm)],[6532:[]]) ).
thf(2365,plain,
( ( ( sk5 @ ( triangles @ number_of_in ) )
!= ( sk5 @ ( edges @ number_of_in ) ) )
| ( ( sk5 @ ( sequential_pairs @ number_of_in ) )
= ( sk5 @ length_of ) )
| ( sk5 @ sk6 @ edge ) ),
inference(paramod_ordered,[status(thm)],[2212,1449]) ).
thf(2372,plain,
( ( sk5 != sk5 )
| ( triangles != edges )
| ( ( sk5 @ ( sequential_pairs @ number_of_in ) )
= ( sk5 @ length_of ) )
| ( sk5 @ sk6 @ edge ) ),
inference(simp,[status(thm)],[2365]) ).
thf(2379,plain,
( ( triangles != edges )
| ( ( sk5 @ ( sequential_pairs @ number_of_in ) )
= ( sk5 @ length_of ) )
| ( sk5 @ sk6 @ edge ) ),
inference(simp,[status(thm)],[2372]) ).
thf(3172,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)],[2379,32]) ).
thf(3173,plain,
( ( graph @ ( sequential_pairs @ number_of_in ) @ ( sk5 @ length_of @ less_or_equal ) )
| ( triangles != edges )
| ( sk5 @ sk6 @ edge ) ),
inference(pattern_uni,[status(thm)],[3172:[bind(A,$thf( sequential_pairs )),bind(B,$thf( sk5 ))]]) ).
thf(2451,plain,
( ( ( sk5 @ ( triangles @ number_of_in ) )
!= ( sk5 @ ( edges @ number_of_in ) ) )
| ( ( sk5 @ ( sequential_pairs @ number_of_in ) )
= ( sk5 @ length_of ) )
| ( sk5 @ sk7 @ edge ) ),
inference(paramod_ordered,[status(thm)],[2237,1449]) ).
thf(2454,plain,
( ( sk5 != sk5 )
| ( triangles != edges )
| ( ( sk5 @ ( sequential_pairs @ number_of_in ) )
= ( sk5 @ length_of ) )
| ( sk5 @ sk7 @ edge ) ),
inference(simp,[status(thm)],[2451]) ).
thf(2467,plain,
( ( triangles != edges )
| ( ( sk5 @ ( sequential_pairs @ number_of_in ) )
= ( sk5 @ length_of ) )
| ( sk5 @ sk7 @ edge ) ),
inference(simp,[status(thm)],[2454]) ).
thf(3674,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,32]) ).
thf(3675,plain,
( ( graph @ ( sequential_pairs @ number_of_in ) @ ( sk5 @ length_of @ less_or_equal ) )
| ( triangles != edges )
| ( sk5 @ sk7 @ edge ) ),
inference(pattern_uni,[status(thm)],[3674:[bind(A,$thf( sequential_pairs )),bind(B,$thf( sk5 ))]]) ).
thf(125,plain,
! [A: $i] :
( ? [B: $i,C: $i] : ( A @ ( C @ ( B @ path ) ) )
=> ! [B: $i,C: $i] :
( ( ( ? [D: $i] :
( ( A @ ( C @ ( D @ precedes ) ) )
& ( D @ ( B @ sequential ) ) )
| ( C @ ( B @ sequential ) ) )
& ( A @ ( C @ on_path ) )
& ( A @ ( B @ on_path ) ) )
=> ( A @ ( C @ ( B @ precedes ) ) ) ) ),
inference(miniscope,[status(thm)],[124]) ).
thf(126,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( E @ ( D @ precedes ) ) )
| ~ ( A @ ( E @ ( F @ precedes ) ) )
| ~ ( F @ ( D @ sequential ) )
| ~ ( A @ ( E @ on_path ) )
| ~ ( A @ ( D @ on_path ) )
| ~ ( A @ ( C @ ( B @ path ) ) ) )
& ( ( A @ ( E @ ( D @ precedes ) ) )
| ~ ( E @ ( D @ sequential ) )
| ~ ( A @ ( E @ on_path ) )
| ~ ( A @ ( D @ on_path ) )
| ~ ( A @ ( C @ ( B @ path ) ) ) ) ),
inference(cnf,[status(esa)],[125]) ).
thf(128,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( A @ ( E @ ( D @ precedes ) ) )
| ~ ( A @ ( E @ ( F @ precedes ) ) )
| ~ ( F @ ( D @ sequential ) )
| ~ ( A @ ( E @ on_path ) )
| ~ ( A @ ( D @ on_path ) )
| ~ ( A @ ( C @ ( B @ path ) ) ) ),
inference(cnfConj,[status(thm)],[126]) ).
thf(22474,plain,
! [A: $i] :
( ( ( A @ head_of )
!= ( sk3 @ head_of ) )
| ( ( sk3 @ tail_of )
!= sk1 )
| ~ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ ( A @ sequential ) ) ),
inference(paramod_ordered,[status(thm)],[7510,22307]) ).
thf(22475,plain,
( ( ( sk3 @ tail_of )
!= sk1 )
| ~ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ ( sk3 @ sequential ) ) ),
inference(pattern_uni,[status(thm)],[22474:[bind(A,$thf( sk3 ))]]) ).
thf(22972,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ tail_of )
!= ( sk3 @ tail_of ) )
| ( sk1 != sk1 )
| ~ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ ( sk3 @ sequential ) ) ),
inference(paramod_ordered,[status(thm)],[7420,22475]) ).
thf(22973,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ tail_of )
!= ( sk3 @ tail_of ) )
| ~ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ ( sk3 @ sequential ) ) ),
inference(simp,[status(thm)],[22972]) ).
thf(23012,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) )
!= sk3 )
| ~ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ ( sk3 @ sequential ) ) ),
inference(simp,[status(thm)],[22973]) ).
thf(7522,plain,
! [A: $i] :
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ tail_of )
!= ( sk3 @ tail_of ) )
| ( A != sk4 )
| ( ( A @ tail_of )
!= sk1 ) ),
inference(simp,[status(thm)],[7479]) ).
thf(7532,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ tail_of )
!= ( sk3 @ tail_of ) )
| ( ( sk4 @ tail_of )
!= sk1 ) ),
inference(simp,[status(thm)],[7522]) ).
thf(8195,plain,
( ( ( sk3 @ tail_of )
!= sk1 )
| ( ( sk4 @ tail_of )
!= sk1 ) ),
inference(rewrite,[status(thm)],[7532,7420]) ).
thf(25089,plain,
! [A: $i] :
( ( ( sk1 @ ( sk2 @ ( sk5 @ ( sk4 @ head_of @ sk11 ) ) ) @ edge )
!= ( A @ edge ) )
| ( A @ head_of @ vertex )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[24979,152]) ).
thf(25090,plain,
! [A: $i] :
( ( ( sk1 @ ( sk2 @ ( sk5 @ ( sk4 @ head_of @ sk11 ) ) ) @ edge )
!= ( A @ edge ) )
| ( A @ head_of @ vertex ) ),
inference(simp,[status(thm)],[25089]) ).
thf(25091,plain,
sk1 @ ( sk2 @ ( sk5 @ ( sk4 @ head_of @ sk11 ) ) ) @ head_of @ vertex,
inference(pattern_uni,[status(thm)],[25090:[bind(A,$thf( sk1 @ ( sk2 @ ( sk5 @ ( sk4 @ head_of @ sk11 ) ) ) ))]]) ).
thf(161,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( A @ sequential ) )
| ~ ( C @ ( B @ ( A @ triangle ) ) ) ),
inference(cnfConj,[status(thm)],[156]) ).
thf(6057,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)],[5970,3046]) ).
thf(6139,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)],[6057]) ).
thf(6166,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of )
!= ( sk4 @ head_of ) )
| ( ( sk3 @ head_of )
!= sk2 )
| ~ ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) ),
inference(simp,[status(thm)],[6139]) ).
thf(11394,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)],[5970,6166]) ).
thf(11395,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)],[11394]) ).
thf(11396,plain,
( ( ( sk4 @ head_of )
!= sk2 )
| ( ( sk3 @ head_of )
!= sk2 )
| ~ ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) ),
inference(pattern_uni,[status(thm)],[11395:[]]) ).
thf(25504,plain,
! [A: $i] :
( ( ( sk1 @ ( sk2 @ ( sk5 @ ( sk3 @ head_of @ sk11 ) ) ) @ edge )
!= ( A @ edge ) )
| ( A @ tail_of @ vertex )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[25246,153]) ).
thf(25505,plain,
! [A: $i] :
( ( ( sk1 @ ( sk2 @ ( sk5 @ ( sk3 @ head_of @ sk11 ) ) ) @ edge )
!= ( A @ edge ) )
| ( A @ tail_of @ vertex ) ),
inference(simp,[status(thm)],[25504]) ).
thf(25506,plain,
sk1 @ ( sk2 @ ( sk5 @ ( sk3 @ head_of @ sk11 ) ) ) @ tail_of @ vertex,
inference(pattern_uni,[status(thm)],[25505:[bind(A,$thf( sk1 @ ( sk2 @ ( sk5 @ ( sk3 @ head_of @ sk11 ) ) ) ))]]) ).
thf(25239,plain,
! [A: $i] :
( ( ( sk5 @ ( sk1 @ ( sk2 @ ( sk5 @ ( sk3 @ head_of @ sk11 ) ) ) @ on_path ) )
!= ( sk5 @ ( A @ on_path ) ) )
| ( sk5 @ ( A @ head_of @ in_path ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[24857,22806]) ).
thf(25240,plain,
! [A: $i] :
( ( ( sk5 @ ( sk1 @ ( sk2 @ ( sk5 @ ( sk3 @ head_of @ sk11 ) ) ) @ on_path ) )
!= ( sk5 @ ( A @ on_path ) ) )
| ( sk5 @ ( A @ head_of @ in_path ) ) ),
inference(simp,[status(thm)],[25239]) ).
thf(25241,plain,
sk5 @ ( sk1 @ ( sk2 @ ( sk5 @ ( sk3 @ head_of @ sk11 ) ) ) @ head_of @ in_path ),
inference(pattern_uni,[status(thm)],[25240:[bind(A,$thf( sk1 @ ( sk2 @ ( sk5 @ ( sk3 @ head_of @ sk11 ) ) ) ))]]) ).
thf(75,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)],[66]) ).
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)],[75]) ).
thf(6798,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( empty @ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ path_cons ) )
!= ( D @ ( A @ ( B @ ( C @ sk8 ) ) @ path_cons ) ) )
| ~ ( A @ ( B @ ( C @ sk9 ) ) )
| ~ ( D @ ( B @ ( A @ ( B @ ( C @ sk8 ) ) @ head_of @ path ) ) )
| ~ ( C @ ( B @ ( A @ path ) ) )
| ( sk5 != C )
| ~ ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) ),
inference(paramod_ordered,[status(thm)],[4042,81]) ).
thf(6799,plain,
( ~ ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) )
| ~ ( empty @ ( sk2 @ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of @ path ) ) )
| ~ ( sk5 @ ( sk2 @ ( sk1 @ path ) ) )
| ( sk5 != sk5 )
| ~ ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) ),
inference(pattern_uni,[status(thm)],[6798:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 )),bind(C,$thf( sk5 )),bind(D,$thf( empty ))]]) ).
thf(6838,plain,
( ~ ( empty @ ( sk2 @ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of @ path ) ) )
| ~ ( sk5 @ ( sk2 @ ( sk1 @ path ) ) )
| ~ ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) ),
inference(simp,[status(thm)],[6799]) ).
thf(29360,plain,
( ~ ( empty @ ( sk2 @ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of @ path ) ) )
| ~ $true
| ~ ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) ),
inference(rewrite,[status(thm)],[6838,1381]) ).
thf(29361,plain,
( ~ ( empty @ ( sk2 @ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of @ path ) ) )
| ~ ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) ),
inference(simp,[status(thm)],[29360]) ).
thf(29426,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of )
!= ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of ) )
| ~ ( empty @ ( sk2 @ ( sk2 @ path ) ) )
| ~ ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) )
| ~ ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) ),
inference(paramod_ordered,[status(thm)],[5970,29361]) ).
thf(29427,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of )
!= ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of ) )
| ~ ( empty @ ( sk2 @ ( sk2 @ path ) ) )
| ~ ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) ),
inference(simp,[status(thm)],[29426]) ).
thf(29428,plain,
( ~ ( empty @ ( sk2 @ ( sk2 @ path ) ) )
| ~ ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) ),
inference(pattern_uni,[status(thm)],[29427:[]]) ).
thf(27642,plain,
! [A: $i] :
( ( ( sk5 @ ( sk1 @ ( sk2 @ ( sk5 @ ( sk4 @ tail_of @ sk11 ) ) ) @ on_path ) )
!= ( sk5 @ ( A @ on_path ) ) )
| ( A @ edge )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[27028,22209]) ).
thf(27643,plain,
! [A: $i] :
( ( ( sk5 @ ( sk1 @ ( sk2 @ ( sk5 @ ( sk4 @ tail_of @ sk11 ) ) ) @ on_path ) )
!= ( sk5 @ ( A @ on_path ) ) )
| ( A @ edge ) ),
inference(simp,[status(thm)],[27642]) ).
thf(27644,plain,
sk1 @ ( sk2 @ ( sk5 @ ( sk4 @ tail_of @ sk11 ) ) ) @ edge,
inference(pattern_uni,[status(thm)],[27643:[bind(A,$thf( sk1 @ ( sk2 @ ( sk5 @ ( sk4 @ tail_of @ sk11 ) ) ) ))]]) ).
thf(27731,plain,
! [A: $i] :
( ( ( sk1 @ ( sk2 @ ( sk5 @ ( sk4 @ tail_of @ sk11 ) ) ) @ edge )
!= ( A @ edge ) )
| ~ $true
| ( ( A @ head_of )
!= ( A @ tail_of ) ) ),
inference(paramod_ordered,[status(thm)],[27644,101]) ).
thf(27732,plain,
! [A: $i] :
( ( ( sk1 @ ( sk2 @ ( sk5 @ ( sk4 @ tail_of @ sk11 ) ) ) @ edge )
!= ( A @ edge ) )
| ( ( A @ head_of )
!= ( A @ tail_of ) ) ),
inference(simp,[status(thm)],[27731]) ).
thf(27733,plain,
( ( sk1 @ ( sk2 @ ( sk5 @ ( sk4 @ tail_of @ sk11 ) ) ) @ head_of )
!= ( sk1 @ ( sk2 @ ( sk5 @ ( sk4 @ tail_of @ sk11 ) ) ) @ tail_of ) ),
inference(pattern_uni,[status(thm)],[27732:[bind(A,$thf( sk1 @ ( sk2 @ ( sk5 @ ( sk4 @ tail_of @ sk11 ) ) ) ))]]) ).
thf(159,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ edge )
| ~ ( C @ ( B @ ( A @ triangle ) ) ) ),
inference(cnfConj,[status(thm)],[156]) ).
thf(6042,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of )
!= ( sk4 @ head_of ) )
| ( ( sk3 @ head_of )
!= sk2 )
| ~ ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) ),
inference(paramod_ordered,[status(thm)],[5970,3930]) ).
thf(6144,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) )
!= sk4 )
| ( ( sk3 @ head_of )
!= sk2 )
| ~ ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) ),
inference(simp,[status(thm)],[6042]) ).
thf(1428,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)],[1381,493]) ).
thf(1429,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)],[1428]) ).
thf(1463,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)],[1429]) ).
thf(1474,plain,
! [A: $i] :
( ( sk5 != graph )
| ( graph @ length_of @ ( A @ ( edges @ number_of_in ) @ less_or_equal ) ) ),
inference(simp,[status(thm)],[1463]) ).
thf(1932,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)],[1449,1474]) ).
thf(1933,plain,
( ( sk5 != graph )
| ( graph @ length_of @ ( sk5 @ length_of @ less_or_equal ) ) ),
inference(pattern_uni,[status(thm)],[1932:[bind(A,$thf( sk5 ))]]) ).
thf(6055,plain,
! [A: $i] :
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of )
!= ( A @ head_of ) )
| ( ( sk4 @ head_of )
!= sk2 )
| ( ( A @ tail_of )
!= ( sk3 @ tail_of ) )
| ~ ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) ),
inference(paramod_ordered,[status(thm)],[5970,3046]) ).
thf(6056,plain,
( ( ( sk4 @ head_of )
!= sk2 )
| ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ tail_of )
!= ( sk3 @ tail_of ) )
| ~ ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) ),
inference(pattern_uni,[status(thm)],[6055:[bind(A,$thf( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) ))]]) ).
thf(7470,plain,
( ( ( sk4 @ head_of )
!= sk2 )
| ( ( sk3 @ tail_of )
!= sk1 )
| ~ ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) ),
inference(rewrite,[status(thm)],[6056,7420]) ).
thf(25494,plain,
! [A: $i] :
( ( ( sk1 @ ( sk2 @ ( sk5 @ ( sk3 @ head_of @ sk11 ) ) ) @ edge )
!= ( A @ edge ) )
| ~ $true
| ( ( A @ head_of )
!= ( A @ tail_of ) ) ),
inference(paramod_ordered,[status(thm)],[25246,101]) ).
thf(25495,plain,
! [A: $i] :
( ( ( sk1 @ ( sk2 @ ( sk5 @ ( sk3 @ head_of @ sk11 ) ) ) @ edge )
!= ( A @ edge ) )
| ( ( A @ head_of )
!= ( A @ tail_of ) ) ),
inference(simp,[status(thm)],[25494]) ).
thf(25496,plain,
( ( sk1 @ ( sk2 @ ( sk5 @ ( sk3 @ head_of @ sk11 ) ) ) @ head_of )
!= ( sk1 @ ( sk2 @ ( sk5 @ ( sk3 @ head_of @ sk11 ) ) ) @ tail_of ) ),
inference(pattern_uni,[status(thm)],[25495:[bind(A,$thf( sk1 @ ( sk2 @ ( sk5 @ ( sk3 @ head_of @ sk11 ) ) ) ))]]) ).
thf(1861,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)],[1441,32]) ).
thf(1862,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)],[1861:[bind(A,$thf( triangles )),bind(B,$thf( sk5 ))]]) ).
thf(3140,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)],[2379,2347]) ).
thf(3141,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)],[3140]) ).
thf(3142,plain,
( ( graph @ ( triangles @ number_of_in ) @ ( sk5 @ length_of @ less_or_equal ) )
| ( triangles != edges )
| ( sk5 @ sk6 @ edge ) ),
inference(pattern_uni,[status(thm)],[3141:[]]) ).
thf(7895,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)],[5970,7472]) ).
thf(7896,plain,
( ( ( sk3 @ tail_of )
!= sk2 )
| ( ( sk4 @ head_of )
!= sk1 )
| ~ ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) ),
inference(pattern_uni,[status(thm)],[7895:[]]) ).
thf(7561,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)],[59,7471]) ).
thf(7562,plain,
! [A: $i] :
( ( ( A @ tail_of )
!= sk1 )
| ~ ( A @ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ sequential ) ) ),
inference(pattern_uni,[status(thm)],[7561:[bind(A,$thf( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) )),bind(B,$thf( B ))]]) ).
thf(7571,plain,
! [A: $i] :
( ( ( A @ tail_of )
!= sk1 )
| ~ ( A @ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ sequential ) ) ),
inference(simp,[status(thm)],[7562]) ).
thf(2232,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)],[1438,59]) ).
thf(2233,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)],[2232]) ).
thf(2234,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)],[2233:[bind(A,$thf( sk5 @ sk6 )),bind(B,$thf( sk5 @ sk7 ))]]) ).
thf(27740,plain,
! [A: $i] :
( ( ( sk1 @ ( sk2 @ ( sk5 @ ( sk4 @ tail_of @ sk11 ) ) ) @ edge )
!= ( A @ edge ) )
| ( A @ tail_of @ vertex )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[27644,153]) ).
thf(27741,plain,
! [A: $i] :
( ( ( sk1 @ ( sk2 @ ( sk5 @ ( sk4 @ tail_of @ sk11 ) ) ) @ edge )
!= ( A @ edge ) )
| ( A @ tail_of @ vertex ) ),
inference(simp,[status(thm)],[27740]) ).
thf(27742,plain,
sk1 @ ( sk2 @ ( sk5 @ ( sk4 @ tail_of @ sk11 ) ) ) @ tail_of @ vertex,
inference(pattern_uni,[status(thm)],[27741:[bind(A,$thf( sk1 @ ( sk2 @ ( sk5 @ ( sk4 @ tail_of @ sk11 ) ) ) ))]]) ).
thf(2750,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 @ sk7 @ edge )
| ( sk5 @ sk7 @ edge ) ),
inference(paramod_ordered,[status(thm)],[2237,2427]) ).
thf(2751,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 @ sk7 @ edge ) ),
inference(simp,[status(thm)],[2750]) ).
thf(2811,plain,
( ( sk5 != graph )
| ( triangles != triangles )
| ( sk5 @ ( sequential_pairs @ number_of_in ) @ ( sk5 @ ( sequential_pairs @ number_of_in ) @ less_or_equal ) )
| ( sk5 @ sk7 @ edge ) ),
inference(simp,[status(thm)],[2751]) ).
thf(2846,plain,
( ( sk5 != graph )
| ( sk5 @ ( sequential_pairs @ number_of_in ) @ ( sk5 @ ( sequential_pairs @ number_of_in ) @ less_or_equal ) )
| ( sk5 @ sk7 @ edge ) ),
inference(simp,[status(thm)],[2811]) ).
thf(27601,plain,
! [A: $i] :
( ( ( sk5 @ ( sk1 @ ( sk2 @ ( sk5 @ ( sk4 @ tail_of @ sk11 ) ) ) @ on_path ) )
!= ( sk5 @ ( A @ on_path ) ) )
| ( A @ head_of @ vertex )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[27028,24533]) ).
thf(27602,plain,
! [A: $i] :
( ( ( sk5 @ ( sk1 @ ( sk2 @ ( sk5 @ ( sk4 @ tail_of @ sk11 ) ) ) @ on_path ) )
!= ( sk5 @ ( A @ on_path ) ) )
| ( A @ head_of @ vertex ) ),
inference(simp,[status(thm)],[27601]) ).
thf(27603,plain,
sk1 @ ( sk2 @ ( sk5 @ ( sk4 @ tail_of @ sk11 ) ) ) @ head_of @ vertex,
inference(pattern_uni,[status(thm)],[27602:[bind(A,$thf( sk1 @ ( sk2 @ ( sk5 @ ( sk4 @ tail_of @ sk11 ) ) ) ))]]) ).
thf(138,plain,
! [B: $i,A: $i] :
( ( B
!= ( A @ ( B @ sk15 ) @ tail_of ) )
| ( A
!= ( A @ ( B @ sk15 ) @ head_of ) )
| ( A @ ( B @ sk16 ) )
| ( A = B )
| ~ ( B @ vertex )
| ~ ( A @ vertex )
| ~ complete ),
inference(cnfConj,[status(thm)],[135]) ).
thf(143,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ sk16 ) )
| ~ ( B @ vertex )
| ~ ( A @ vertex )
| ~ complete
| ( ( A @ ( B @ sk15 ) @ tail_of )
!= B )
| ( ( A @ ( B @ sk15 ) @ head_of )
!= A )
| ( A = B ) ),
inference(lifteq,[status(thm)],[138]) ).
thf(23942,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ sk16 ) )
| ~ ( B @ vertex )
| ~ ( A @ vertex )
| ~ $true
| ( ( A @ ( B @ sk15 ) @ tail_of )
!= B )
| ( ( A @ ( B @ sk15 ) @ head_of )
!= A )
| ( A = B ) ),
inference(rewrite,[status(thm)],[143,23]) ).
thf(23943,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ sk16 ) )
| ~ ( B @ vertex )
| ~ ( A @ vertex )
| ( ( A @ ( B @ sk15 ) @ tail_of )
!= B )
| ( ( A @ ( B @ sk15 ) @ head_of )
!= A )
| ( A = B ) ),
inference(simp,[status(thm)],[23942]) ).
thf(162,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ sequential ) )
| ~ ( C @ ( B @ ( A @ triangle ) ) ) ),
inference(cnfConj,[status(thm)],[156]) ).
thf(519,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)],[24,63]) ).
thf(520,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)],[519]) ).
thf(521,plain,
! [B: $i,A: $i] :
( ~ ( sk5 @ ( A @ ( B @ precedes ) ) )
| ~ ( sk5 @ ( B @ ( A @ precedes ) ) ) ),
inference(pattern_uni,[status(thm)],[520:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( sk5 ))]]) ).
thf(531,plain,
! [B: $i,A: $i] :
( ~ ( sk5 @ ( A @ ( B @ precedes ) ) )
| ~ ( sk5 @ ( B @ ( A @ precedes ) ) ) ),
inference(simp,[status(thm)],[521]) ).
thf(117,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ shortest_path ) ) )
| ~ ( A @ ( B @ ( C @ sk14 ) ) @ length_of @ ( C @ length_of @ less_or_equal ) )
| ( A = B )
| ~ ( C @ ( B @ ( A @ path ) ) ) ),
inference(cnfConj,[status(thm)],[112]) ).
thf(122,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ shortest_path ) ) )
| ~ ( A @ ( B @ ( C @ sk14 ) ) @ length_of @ ( C @ length_of @ less_or_equal ) )
| ~ ( C @ ( B @ ( A @ path ) ) )
| ( A = B ) ),
inference(lifteq,[status(thm)],[117]) ).
thf(123,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ shortest_path ) ) )
| ~ ( A @ ( B @ ( C @ sk14 ) ) @ length_of @ ( C @ length_of @ less_or_equal ) )
| ~ ( C @ ( B @ ( A @ path ) ) )
| ( A = B ) ),
inference(simp,[status(thm)],[122]) ).
thf(25508,plain,
! [A: $i] :
( ( ( sk1 @ ( sk2 @ ( sk5 @ ( sk3 @ head_of @ sk11 ) ) ) @ edge )
!= ( A @ edge ) )
| ( A @ head_of @ vertex )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[25246,152]) ).
thf(25509,plain,
! [A: $i] :
( ( ( sk1 @ ( sk2 @ ( sk5 @ ( sk3 @ head_of @ sk11 ) ) ) @ edge )
!= ( A @ edge ) )
| ( A @ head_of @ vertex ) ),
inference(simp,[status(thm)],[25508]) ).
thf(25510,plain,
sk1 @ ( sk2 @ ( sk5 @ ( sk3 @ head_of @ sk11 ) ) ) @ head_of @ vertex,
inference(pattern_uni,[status(thm)],[25509:[bind(A,$thf( sk1 @ ( sk2 @ ( sk5 @ ( sk3 @ head_of @ sk11 ) ) ) ))]]) ).
thf(22631,plain,
! [B: $i,A: $i] :
( ( ( A @ head_of )
!= ( sk3 @ head_of ) )
| ( B @ tail_of @ vertex )
| ~ ( B @ ( A @ sequential ) ) ),
inference(paramod_ordered,[status(thm)],[59,22319]) ).
thf(22632,plain,
! [A: $i] :
( ( A @ tail_of @ vertex )
| ~ ( A @ ( sk3 @ sequential ) ) ),
inference(pattern_uni,[status(thm)],[22631:[bind(A,$thf( sk3 ))]]) ).
thf(22670,plain,
! [A: $i] :
( ( A @ tail_of @ vertex )
| ~ ( A @ ( sk3 @ sequential ) ) ),
inference(simp,[status(thm)],[22632]) ).
thf(4467,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)],[3826,4042]) ).
thf(4468,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)],[4467]) ).
thf(4469,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)],[4468:[]]) ).
thf(2791,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)],[1449,2427]) ).
thf(2796,plain,
( ( sk5 != sk5 )
| ( edges != sequential_pairs )
| ( graph @ ( triangles @ number_of_in ) @ ( sk5 @ length_of @ less_or_equal ) )
| ( sk5 @ sk7 @ edge ) ),
inference(simp,[status(thm)],[2791]) ).
thf(2831,plain,
( ( edges != sequential_pairs )
| ( graph @ ( triangles @ number_of_in ) @ ( sk5 @ length_of @ less_or_equal ) )
| ( sk5 @ sk7 @ edge ) ),
inference(simp,[status(thm)],[2796]) ).
thf(4903,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)],[4457,4042]) ).
thf(4904,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)],[4903]) ).
thf(4905,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)],[4904:[]]) ).
thf(127,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( A @ ( E @ ( D @ precedes ) ) )
| ~ ( E @ ( D @ sequential ) )
| ~ ( A @ ( E @ on_path ) )
| ~ ( A @ ( D @ on_path ) )
| ~ ( A @ ( C @ ( B @ path ) ) ) ),
inference(cnfConj,[status(thm)],[126]) ).
thf(9443,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)],[7510,7896]) ).
thf(9444,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)],[9443]) ).
thf(9445,plain,
( ( ( sk3 @ tail_of )
!= sk2 )
| ~ ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) )
| ~ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ ( sk4 @ sequential ) ) ),
inference(pattern_uni,[status(thm)],[9444:[bind(A,$thf( sk4 ))]]) ).
thf(142,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ sk16 ) )
| ( A
!= ( A @ ( B @ sk15 ) @ tail_of ) )
| ( B
!= ( A @ ( B @ sk15 ) @ head_of ) )
| ( A = B )
| ~ ( B @ vertex )
| ~ ( A @ vertex )
| ~ complete ),
inference(cnfConj,[status(thm)],[135]) ).
thf(144,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ sk16 ) )
| ~ ( B @ vertex )
| ~ ( A @ vertex )
| ~ complete
| ( ( A @ ( B @ sk15 ) @ tail_of )
!= A )
| ( ( A @ ( B @ sk15 ) @ head_of )
!= B )
| ( A = B ) ),
inference(lifteq,[status(thm)],[142]) ).
thf(24632,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ sk16 ) )
| ~ ( B @ vertex )
| ~ ( A @ vertex )
| ~ $true
| ( ( A @ ( B @ sk15 ) @ tail_of )
!= A )
| ( ( A @ ( B @ sk15 ) @ head_of )
!= B )
| ( A = B ) ),
inference(rewrite,[status(thm)],[144,23]) ).
thf(24633,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ sk16 ) )
| ~ ( B @ vertex )
| ~ ( A @ vertex )
| ( ( A @ ( B @ sk15 ) @ tail_of )
!= A )
| ( ( A @ ( B @ sk15 ) @ head_of )
!= B )
| ( A = B ) ),
inference(simp,[status(thm)],[24632]) ).
thf(22460,plain,
! [B: $i,A: $i] :
( ( ( A @ head_of )
!= ( sk3 @ head_of ) )
| ( ( B @ tail_of )
!= ( sk3 @ tail_of ) )
| ~ ( B @ ( A @ sequential ) ) ),
inference(paramod_ordered,[status(thm)],[59,22307]) ).
thf(22461,plain,
! [A: $i] :
( ( ( A @ tail_of )
!= ( sk3 @ tail_of ) )
| ~ ( A @ ( sk3 @ sequential ) ) ),
inference(pattern_uni,[status(thm)],[22460:[bind(A,$thf( sk3 ))]]) ).
thf(22501,plain,
! [A: $i] :
( ( ( A @ tail_of )
!= ( sk3 @ tail_of ) )
| ~ ( A @ ( sk3 @ sequential ) ) ),
inference(simp,[status(thm)],[22461]) ).
thf(6103,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)],[4457,5970]) ).
thf(6104,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)],[6103]) ).
thf(6105,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)],[6104:[]]) ).
thf(1608,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)],[1381,46]) ).
thf(1609,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)],[1608]) ).
thf(1610,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)],[1609:[bind(A,$thf( sk5 )),bind(B,$thf( sk1 )),bind(C,$thf( sk2 ))]]) ).
thf(1653,plain,
! [A: $i] :
( ~ ( A @ ( sk5 @ sk7 @ ( sk5 @ sk6 @ triangle ) ) )
| ( ( sk5 @ ( triangles @ number_of_in ) )
= ( sk5 @ ( sequential_pairs @ number_of_in ) ) ) ),
inference(simp,[status(thm)],[1610]) ).
thf(5489,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)],[1653,32]) ).
thf(5490,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)],[5489:[bind(A,$thf( A )),bind(B,$thf( triangles )),bind(C,$thf( sk5 ))]]) ).
thf(7007,plain,
( ( ( sk4 @ head_of )
!= sk2 )
| ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) )
!= sk3 )
| ~ ( sk1 @ ( sk2 @ ( sk5 @ sk9 ) ) ) ),
inference(simp,[status(thm)],[6056]) ).
thf(1370,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)],[114,493]) ).
thf(1371,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)],[1370]) ).
thf(1372,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)],[1371:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( graph )),bind(D,$thf( A )),bind(E,$thf( B ))]]) ).
thf(1412,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)],[1372]) ).
thf(2944,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 )
!= ( sk5 @ sk6 ) ) ),
inference(paramod_ordered,[status(thm)],[1449,2527]) ).
thf(2965,plain,
( ( sk5 != sk5 )
| ( edges != sequential_pairs )
| ( ( sk5 @ sk7 )
!= ( sk5 @ sk6 ) )
| ( graph @ ( triangles @ number_of_in ) @ ( sk5 @ length_of @ less_or_equal ) ) ),
inference(simp,[status(thm)],[2944]) ).
thf(2988,plain,
( ( edges != sequential_pairs )
| ( ( sk5 @ sk7 )
!= ( sk5 @ sk6 ) )
| ( graph @ ( triangles @ number_of_in ) @ ( sk5 @ length_of @ less_or_equal ) ) ),
inference(simp,[status(thm)],[2965]) ).
thf(137,plain,
! [B: $i,A: $i] :
( ( A
= ( A @ ( B @ sk15 ) @ tail_of ) )
| ( A @ ( B @ sk16 ) )
| ( A = B )
| ~ ( B @ vertex )
| ~ ( A @ vertex )
| ~ complete ),
inference(cnfConj,[status(thm)],[135]) ).
thf(145,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ sk16 ) )
| ~ ( B @ vertex )
| ~ ( A @ vertex )
| ~ complete
| ( ( A @ ( B @ sk15 ) @ tail_of )
= A )
| ( A = B ) ),
inference(lifteq,[status(thm)],[137]) ).
thf(25822,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ sk16 ) )
| ~ ( B @ vertex )
| ~ ( A @ vertex )
| ~ $true
| ( ( A @ ( B @ sk15 ) @ tail_of )
= A )
| ( A = B ) ),
inference(rewrite,[status(thm)],[145,23]) ).
thf(25823,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ sk16 ) )
| ~ ( B @ vertex )
| ~ ( A @ vertex )
| ( ( A @ ( B @ sk15 ) @ tail_of )
= A )
| ( A = B ) ),
inference(simp,[status(thm)],[25822]) ).
thf(158,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ edge )
| ~ ( C @ ( B @ ( A @ triangle ) ) ) ),
inference(cnfConj,[status(thm)],[156]) ).
thf(28098,plain,
! [A: $i] :
( ( ( sk1 @ ( sk2 @ ( sk5 @ ( sk3 @ tail_of @ sk11 ) ) ) @ edge )
!= ( A @ edge ) )
| ~ $true
| ( ( A @ head_of )
!= ( A @ tail_of ) ) ),
inference(paramod_ordered,[status(thm)],[27881,101]) ).
thf(28099,plain,
! [A: $i] :
( ( ( sk1 @ ( sk2 @ ( sk5 @ ( sk3 @ tail_of @ sk11 ) ) ) @ edge )
!= ( A @ edge ) )
| ( ( A @ head_of )
!= ( A @ tail_of ) ) ),
inference(simp,[status(thm)],[28098]) ).
thf(28100,plain,
( ( sk1 @ ( sk2 @ ( sk5 @ ( sk3 @ tail_of @ sk11 ) ) ) @ head_of )
!= ( sk1 @ ( sk2 @ ( sk5 @ ( sk3 @ tail_of @ sk11 ) ) ) @ tail_of ) ),
inference(pattern_uni,[status(thm)],[28099:[bind(A,$thf( sk1 @ ( sk2 @ ( sk5 @ ( sk3 @ tail_of @ sk11 ) ) ) ))]]) ).
thf(25075,plain,
! [A: $i] :
( ( ( sk1 @ ( sk2 @ ( sk5 @ ( sk4 @ head_of @ sk11 ) ) ) @ edge )
!= ( A @ edge ) )
| ~ $true
| ( ( A @ head_of )
!= ( A @ tail_of ) ) ),
inference(paramod_ordered,[status(thm)],[24979,101]) ).
thf(25076,plain,
! [A: $i] :
( ( ( sk1 @ ( sk2 @ ( sk5 @ ( sk4 @ head_of @ sk11 ) ) ) @ edge )
!= ( A @ edge ) )
| ( ( A @ head_of )
!= ( A @ tail_of ) ) ),
inference(simp,[status(thm)],[25075]) ).
thf(25077,plain,
( ( sk1 @ ( sk2 @ ( sk5 @ ( sk4 @ head_of @ sk11 ) ) ) @ head_of )
!= ( sk1 @ ( sk2 @ ( sk5 @ ( sk4 @ head_of @ sk11 ) ) ) @ tail_of ) ),
inference(pattern_uni,[status(thm)],[25076:[bind(A,$thf( sk1 @ ( sk2 @ ( sk5 @ ( sk4 @ head_of @ sk11 ) ) ) ))]]) ).
thf(6060,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)],[4460,5970]) ).
thf(6061,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)],[6060]) ).
thf(6062,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)],[6061:[]]) ).
thf(1442,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ path ) ) )
!= ( C @ ( B @ ( A @ path ) ) ) )
| ( A @ vertex )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1381,71]) ).
thf(1443,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ path ) ) )
!= ( C @ ( B @ ( A @ path ) ) ) )
| ( A @ vertex ) ),
inference(simp,[status(thm)],[1442]) ).
thf(1444,plain,
sk1 @ vertex,
inference(pattern_uni,[status(thm)],[1443:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 )),bind(C,$thf( sk5 ))]]) ).
thf(2255,plain,
( ( ( sk5 @ ( triangles @ number_of_in ) )
!= ( sk5 @ ( edges @ number_of_in ) ) )
| ( sk5 @ sk7 @ ( sk5 @ sk6 @ sequential ) )
| ( ( sk5 @ ( sequential_pairs @ number_of_in ) )
= ( sk5 @ length_of ) ) ),
inference(paramod_ordered,[status(thm)],[1449,1438]) ).
thf(2261,plain,
( ( sk5 != sk5 )
| ( triangles != edges )
| ( sk5 @ sk7 @ ( sk5 @ sk6 @ sequential ) )
| ( ( sk5 @ ( sequential_pairs @ number_of_in ) )
= ( sk5 @ length_of ) ) ),
inference(simp,[status(thm)],[2255]) ).
thf(2294,plain,
( ( triangles != edges )
| ( sk5 @ sk7 @ ( sk5 @ sk6 @ sequential ) )
| ( ( sk5 @ ( sequential_pairs @ number_of_in ) )
= ( sk5 @ length_of ) ) ),
inference(simp,[status(thm)],[2261]) ).
thf(3643,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,2427]) ).
thf(3644,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)],[3643]) ).
thf(3645,plain,
( ( graph @ ( triangles @ number_of_in ) @ ( sk5 @ length_of @ less_or_equal ) )
| ( triangles != edges )
| ( sk5 @ sk7 @ edge ) ),
inference(pattern_uni,[status(thm)],[3644:[]]) ).
thf(9549,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 ) ) @ head_of @ vertex ) ),
inference(paramod_ordered,[status(thm)],[5613,5970]) ).
thf(9550,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 ) ) @ head_of @ vertex ) ),
inference(simp,[status(thm)],[9549]) ).
thf(9551,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of )
= sk2 )
| ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of @ ( sk2 @ ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ sk8 ) ) @ head_of @ vertex ) ),
inference(pattern_uni,[status(thm)],[9550:[]]) ).
thf(9032,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 ) ) @ tail_of @ vertex ) ),
inference(paramod_ordered,[status(thm)],[5610,4042]) ).
thf(9033,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 ) ) @ tail_of @ vertex ) ),
inference(simp,[status(thm)],[9032]) ).
thf(9034,plain,
( ( ( empty @ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ path_cons ) )
= sk5 )
| ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of @ ( sk2 @ ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) @ sk8 ) ) @ tail_of @ vertex ) ),
inference(pattern_uni,[status(thm)],[9033:[]]) ).
thf(14488,plain,
! [A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ shortest_path ) ) )
!= ( A @ ( sk2 @ ( sk1 @ shortest_path ) ) ) )
| ( sk5 @ length_of @ ( A @ length_of @ less_or_equal ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[24,14483]) ).
thf(14489,plain,
! [A: $i] :
( ( ( sk5 @ ( sk2 @ ( sk1 @ shortest_path ) ) )
!= ( A @ ( sk2 @ ( sk1 @ shortest_path ) ) ) )
| ( sk5 @ length_of @ ( A @ length_of @ less_or_equal ) ) ),
inference(simp,[status(thm)],[14488]) ).
thf(14490,plain,
sk5 @ length_of @ ( sk5 @ length_of @ less_or_equal ),
inference(pattern_uni,[status(thm)],[14489:[bind(A,$thf( sk5 ))]]) ).
thf(25085,plain,
! [A: $i] :
( ( ( sk1 @ ( sk2 @ ( sk5 @ ( sk4 @ head_of @ sk11 ) ) ) @ edge )
!= ( A @ edge ) )
| ( A @ tail_of @ vertex )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[24979,153]) ).
thf(25086,plain,
! [A: $i] :
( ( ( sk1 @ ( sk2 @ ( sk5 @ ( sk4 @ head_of @ sk11 ) ) ) @ edge )
!= ( A @ edge ) )
| ( A @ tail_of @ vertex ) ),
inference(simp,[status(thm)],[25085]) ).
thf(25087,plain,
sk1 @ ( sk2 @ ( sk5 @ ( sk4 @ head_of @ sk11 ) ) ) @ tail_of @ vertex,
inference(pattern_uni,[status(thm)],[25086:[bind(A,$thf( sk1 @ ( sk2 @ ( sk5 @ ( sk4 @ head_of @ sk11 ) ) ) ))]]) ).
thf(104,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ path ) ) )
| ( C
!= ( empty @ ( D @ path_cons ) ) )
| ( B
!= ( D @ head_of ) )
| ( A
!= ( D @ tail_of ) )
| ~ ( D @ edge )
| ~ ( B @ vertex )
| ~ ( A @ vertex ) ),
inference(cnfConj,[status(thm)],[103]) ).
thf(106,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ path ) ) )
| ~ ( D @ edge )
| ~ ( B @ vertex )
| ~ ( A @ vertex )
| ( C
!= ( empty @ ( D @ path_cons ) ) )
| ( B
!= ( D @ head_of ) )
| ( A
!= ( D @ tail_of ) ) ),
inference(lifteq,[status(thm)],[104]) ).
thf(107,plain,
! [A: $i] :
( ( empty @ ( A @ path_cons ) @ ( A @ head_of @ ( A @ tail_of @ path ) ) )
| ~ ( A @ edge )
| ~ ( A @ head_of @ vertex )
| ~ ( A @ tail_of @ vertex ) ),
inference(simp,[status(thm)],[106]) ).
thf(140,plain,
! [B: $i,A: $i] :
( ( B
= ( A @ ( B @ sk15 ) @ head_of ) )
| ( A @ ( B @ sk16 ) )
| ( A = B )
| ~ ( B @ vertex )
| ~ ( A @ vertex )
| ~ complete ),
inference(cnfConj,[status(thm)],[135]) ).
thf(147,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ sk16 ) )
| ~ ( B @ vertex )
| ~ ( A @ vertex )
| ~ complete
| ( ( A @ ( B @ sk15 ) @ head_of )
= B )
| ( A = B ) ),
inference(lifteq,[status(thm)],[140]) ).
thf(28315,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ sk16 ) )
| ~ ( B @ vertex )
| ~ ( A @ vertex )
| ~ $true
| ( ( A @ ( B @ sk15 ) @ head_of )
= B )
| ( A = B ) ),
inference(rewrite,[status(thm)],[147,23]) ).
thf(28316,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ sk16 ) )
| ~ ( B @ vertex )
| ~ ( A @ vertex )
| ( ( A @ ( B @ sk15 ) @ head_of )
= B )
| ( A = B ) ),
inference(simp,[status(thm)],[28315]) ).
thf(3360,plain,
! [A: $i] :
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ edge )
!= ( A @ edge ) )
| ( A @ head_of @ vertex )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[3300,152]) ).
thf(3361,plain,
! [A: $i] :
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ edge )
!= ( A @ edge ) )
| ( A @ head_of @ vertex ) ),
inference(simp,[status(thm)],[3360]) ).
thf(3362,plain,
sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of @ vertex,
inference(pattern_uni,[status(thm)],[3361:[bind(A,$thf( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) ))]]) ).
thf(3468,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)],[59,3362]) ).
thf(3469,plain,
! [A: $i] :
( ( A @ tail_of @ vertex )
| ~ ( A @ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ sequential ) ) ),
inference(pattern_uni,[status(thm)],[3468:[bind(A,$thf( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) )),bind(B,$thf( B ))]]) ).
thf(3479,plain,
! [A: $i] :
( ( A @ tail_of @ vertex )
| ~ ( A @ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ sequential ) ) ),
inference(simp,[status(thm)],[3469]) ).
thf(8496,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)],[5387]) ).
thf(8499,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)],[8496]) ).
thf(8516,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk10 ) ) )
!= empty )
| ( ( empty @ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ path_cons ) )
= sk5 ) ),
inference(simp,[status(thm)],[8499]) ).
thf(94,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)],[91]) ).
thf(2069,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)],[1458,32]) ).
thf(2070,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)],[2069:[bind(A,$thf( triangles )),bind(B,$thf( sk5 ))]]) ).
thf(738,plain,
! [B: $i,A: $i] :
( ~ $true
| ( ( sk5 @ ( A @ ( B @ precedes ) ) )
!= ( sk5 @ ( B @ ( A @ precedes ) ) ) )
| ~ ( sk5 @ ( B @ ( A @ precedes ) ) ) ),
inference(eqfactor_ordered,[status(thm)],[531]) ).
thf(739,plain,
! [A: $i] :
~ ( sk5 @ ( A @ ( A @ precedes ) ) ),
inference(pattern_uni,[status(thm)],[738:[bind(A,$thf( B ))]]) ).
thf(740,plain,
! [A: $i] :
~ ( sk5 @ ( A @ ( A @ precedes ) ) ),
inference(simp,[status(thm)],[739]) ).
thf(7477,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)],[7420,3046]) ).
thf(7478,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of )
!= ( sk4 @ head_of ) )
| ( ( sk3 @ tail_of )
!= sk1 ) ),
inference(pattern_uni,[status(thm)],[7477:[bind(A,$thf( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) ))]]) ).
thf(7973,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)],[7420,7478]) ).
thf(7974,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ tail_of )
!= ( sk3 @ tail_of ) )
| ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of )
!= ( sk4 @ head_of ) ) ),
inference(simp,[status(thm)],[7973]) ).
thf(7987,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) )
!= sk3 )
| ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ head_of )
!= ( sk4 @ head_of ) ) ),
inference(simp,[status(thm)],[7974]) ).
thf(1554,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)],[1449,32]) ).
thf(1565,plain,
! [B: $i,A: $i] :
( ( sk5 != graph )
| ( edges != A )
| ( sk5 @ length_of @ ( B @ ( A @ number_of_in ) @ less_or_equal ) ) ),
inference(simp,[status(thm)],[1554]) ).
thf(1582,plain,
! [A: $i] :
( ( sk5 != graph )
| ( sk5 @ length_of @ ( A @ ( edges @ number_of_in ) @ less_or_equal ) ) ),
inference(simp,[status(thm)],[1565]) ).
thf(5679,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)],[4371,4042]) ).
thf(5680,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)],[5679]) ).
thf(5681,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)],[5680:[]]) ).
thf(22861,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ tail_of )
!= ( sk4 @ tail_of ) )
| ( sk1 != sk1 )
| ~ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ ( sk4 @ sequential ) ) ),
inference(paramod_ordered,[status(thm)],[7420,22418]) ).
thf(22862,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ tail_of )
!= ( sk4 @ tail_of ) )
| ~ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ ( sk4 @ sequential ) ) ),
inference(simp,[status(thm)],[22861]) ).
thf(22897,plain,
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) )
!= sk4 )
| ~ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ ( sk4 @ sequential ) ) ),
inference(simp,[status(thm)],[22862]) ).
thf(5767,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 @ ( sk5 @ sk6 @ on_path ) ) ),
inference(paramod_ordered,[status(thm)],[2103,32]) ).
thf(5768,plain,
( ( graph @ ( sequential_pairs @ number_of_in ) @ ( sk5 @ length_of @ less_or_equal ) )
| ( triangles != edges )
| ( sk5 @ ( sk5 @ sk6 @ on_path ) ) ),
inference(pattern_uni,[status(thm)],[5767:[bind(A,$thf( sequential_pairs )),bind(B,$thf( sk5 ))]]) ).
thf(3353,plain,
! [A: $i] :
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ edge )
!= ( A @ edge ) )
| ( A @ tail_of @ vertex )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[3300,153]) ).
thf(3354,plain,
! [A: $i] :
( ( ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ edge )
!= ( A @ edge ) )
| ( A @ tail_of @ vertex ) ),
inference(simp,[status(thm)],[3353]) ).
thf(3355,plain,
sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ tail_of @ vertex,
inference(pattern_uni,[status(thm)],[3354:[bind(A,$thf( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) ))]]) ).
thf(3436,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)],[59,3355]) ).
thf(3437,plain,
! [A: $i] :
( ( A @ head_of @ vertex )
| ~ ( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) @ ( A @ sequential ) ) ),
inference(pattern_uni,[status(thm)],[3436:[bind(A,$thf( A )),bind(B,$thf( sk1 @ ( sk2 @ ( sk5 @ sk8 ) ) ))]]) ).
thf(43072,plain,
$false,
inference(e,[status(thm)],[69,101,3930,8283,14585,88,27840,2427,12629,2659,2527,9918,27881,22424,25246,5037,56,3826,153,1458,550,22434,24,8165,22476,22564,25,24533,14483,4371,1441,52,3046,110,26934,1455,24857,157,6049,20,27028,46,93,152,4460,78,2222,2237,7786,34883,22316,27070,121,6054,22307,3300,28109,27087,132,27543,11270,5970,89,133,2103,1405,7533,7471,1438,85,6588,9588,102,60,8999,22806,27585,28,27022,24979,4661,33,160,22260,22278,97,493,3931,22418,22269,37712,92,65,2670,4725,3090,8145,874,6133,22209,1402,29789,7610,22319,109,3954,124,77,1461,9419,24974,5387,96,4457,34882,129,1393,134,6533,3173,3675,128,343,23012,8195,32,25091,45,161,64,24512,22248,11396,44,25506,25241,59,7472,27,29428,71,54,2293,27733,2573,86,159,6144,7519,113,81,1933,76,5610,29361,98,7470,25496,7504,1862,1381,24556,1474,2212,563,23512,3142,35,80,27004,675,7896,7571,2234,487,27742,2846,27603,23943,162,531,7420,123,63,25510,150,95,22670,4469,2831,12659,4905,1452,127,9445,31,24633,22475,2379,5613,72,154,22501,6105,43,5490,99,9438,7007,2347,1412,2988,25823,158,4042,114,23,28100,25077,27644,6062,6166,1444,82,119,58,2294,3645,5187,9551,9034,4472,168,30,24532,14490,36,25087,7510,107,28316,79,3479,8516,94,1693,2070,740,3362,7987,1582,2467,5681,14486,22281,1902,22897,47,131,5768,3437,1653,83,7478,755,26988,1449,11294]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : GRA007+1 : TPTP v9.3.1. Bugfixed v3.2.0.
% 0.00/0.12 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 0.25/5.52 % Computer : n003.cluster.edu
% 0.25/5.52 % Model : x86_64 x86_64
% 0.25/5.52 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.25/5.52 % Memory : 8046.5625MB
% 0.25/5.52 % OS : Linux 6.8.0-71-generic
% 0.25/5.52 % CPULimit : 300
% 0.25/5.52 % WCLimit : 300
% 0.25/5.52 % DateTime : Fri Sep 25 13:49:43 UTC 2026
% 0.25/5.53 % CPUTime :
% 0.25/5.53 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 1.41/6.34 % [INFO] Parsing problem /export/starexec/sandbox2/benchmark/theBenchmark.p ...
% 1.96/6.65 % [INFO] Parsing done (301ms).
% 1.96/6.67 % [INFO] Running in sequential loop mode.
% 3.15/7.26 % [INFO] eprover registered as external prover.
% 3.15/7.28 % [INFO] Scanning for conjecture ...
% 3.61/7.44 % [INFO] Found a conjecture (or negated_conjecture) and 17 axioms. Running axiom selection ...
% 3.78/7.56 % [INFO] Axiom selection finished. Selected 17 axioms (removed 0 axioms).
% 4.00/7.66 % [INFO] Problem is first-order (TPTP FOF).
% 4.00/7.67 % [INFO] Type checking passed.
% 4.00/7.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 ...
% 149.45/41.71 % External prover 'e' found a proof!
% 149.45/41.71 % [INFO] Killing All external provers ...
% 149.45/41.72 % Time passed: 35962ms (effective reasoning time: 35036ms)
% 149.45/41.72 % 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)>
% 149.45/41.72 % Axioms used in derivation (17): path_defn, sequential_defn, graph_has_them_all, path_properties, sequential_pairs_and_triangles, edge_ends_are_vertices, no_loops, 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
% 149.45/41.72 % No. of inferences in proof: 745
% 149.45/41.72 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p : 35962 ms resp. 35036 ms w/o parsing
% 151.54/42.18 % SZS output start Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 151.54/42.19 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------