Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Removed some incorrect axioms.
authormengj
Fri, 30 Jun 2006 12:22:29 +0200
changeset 19969 c72e2110c026
parent 19968 2180f0f443af
child 19970 d6e238c46d1b
Removed some incorrect axioms.
src/HOL/Tools/atp-inputs/const_comb_inclS.dfg file | annotate | diff | comparison | revisions
src/HOL/Tools/atp-inputs/const_comb_inclS.tptp file | annotate | diff | comparison | revisions
src/HOL/Tools/atp-inputs/const_comb_noS.dfg file | annotate | diff | comparison | revisions
src/HOL/Tools/atp-inputs/const_comb_noS.tptp file | annotate | diff | comparison | revisions
src/HOL/Tools/atp-inputs/full_comb_inclS.dfg file | annotate | diff | comparison | revisions
src/HOL/Tools/atp-inputs/full_comb_inclS.tptp file | annotate | diff | comparison | revisions
src/HOL/Tools/atp-inputs/full_comb_noS.dfg file | annotate | diff | comparison | revisions
src/HOL/Tools/atp-inputs/full_comb_noS.tptp file | annotate | diff | comparison | revisions
src/HOL/Tools/atp-inputs/par_comb_inclS.dfg file | annotate | diff | comparison | revisions
src/HOL/Tools/atp-inputs/par_comb_inclS.tptp file | annotate | diff | comparison | revisions
src/HOL/Tools/atp-inputs/par_comb_noS.dfg file | annotate | diff | comparison | revisions
src/HOL/Tools/atp-inputs/par_comb_noS.tptp file | annotate | diff | comparison | revisions
src/HOL/Tools/atp-inputs/u_comb_inclS.dfg file | annotate | diff | comparison | revisions
src/HOL/Tools/atp-inputs/u_comb_inclS.tptp file | annotate | diff | comparison | revisions
src/HOL/Tools/atp-inputs/u_comb_noS.dfg file | annotate | diff | comparison | revisions
src/HOL/Tools/atp-inputs/u_comb_noS.tptp file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/atp-inputs/const_comb_inclS.dfg	Fri Jun 30 12:04:17 2006 +0200
+++ b/src/HOL/Tools/atp-inputs/const_comb_inclS.dfg	Fri Jun 30 12:22:29 2006 +0200
@@ -28,64 +28,14 @@
 a5 ).
 
 clause(
-forall([A, B, T],
-or( not(equal(c_COMBI(T),c_COMBK(A,B))))),
-a6 ).
-
-clause(
-forall([A, B, C, T],
-or( not(equal(c_COMBI(T),c_COMBS(A,B,C))))),
-a7 ).
-
-clause(
-forall([A, B, C, T],
-or( not(equal(c_COMBI(T),c_COMBB(A,B,C))))),
-a8 ).
-
-clause(
-forall([A, B, C, T],
-or( not(equal(c_COMBI(T),c_COMBC(A,B,C))))),
-a9 ).
-
-clause(
-forall([A, A3, B, B3, C3],
-or( not(equal(c_COMBK(A,B),c_COMBS(A3,B3,C3))))),
-a10 ).
-
-clause(
-forall([A, A1, B, B1, C1],
-or( not(equal(c_COMBK(A,B),c_COMBB(A1,B1,C1))))),
-a11 ).
-
-clause(
-forall([A, A2, B, B2, C2],
-or( not(equal(c_COMBK(A,B),c_COMBC(A2,B2,C2))))),
-a12 ).
-
-clause(
-forall([A1, A3, B1, B3, C1, C3],
-or( not(equal(c_COMBS(A3,B3,C3),c_COMBB(A1,B1,C1))))),
-a13 ).
-
-clause(
-forall([A2, A3, B2, B3, C2, C3],
-or( not(equal(c_COMBS(A3,B3,C3),c_COMBC(A2,B2,C2))))),
-a14 ).
-
-clause(
-forall([A1, A2, B1, B2, C1, C2],
-or( not(equal(c_COMBB(A1,B1,C1),c_COMBC(A2,B2,C2))))),
-a15 ).
-
-clause(
 forall([A, X, Y],
 or( not(hBOOL(hAPP(hAPP(fequal(A),X),Y))),
     equal(X,Y))),
-a16 ).
+a6 ).
 
 clause(
 forall([A, X, Y],
 or( not(equal(X,Y)),
     hBOOL(hAPP(hAPP(fequal(A),X),Y)))),
-a17 ).
+a7 ).
 
--- a/src/HOL/Tools/atp-inputs/const_comb_inclS.tptp	Fri Jun 30 12:04:17 2006 +0200
+++ b/src/HOL/Tools/atp-inputs/const_comb_inclS.tptp	Fri Jun 30 12:22:29 2006 +0200
@@ -24,41 +24,10 @@
 input_clause(a5,axiom,
 [++equal(hAPP(hAPP(hAPP(c_COMBC(A,B,C),P),Q),R),hAPP(hAPP(P,R),Q))]).
 
-%the combinators are all different
 input_clause(a6,axiom,
-[--equal(c_COMBI(T),c_COMBK(A,B))]).
+[--hBOOL(hAPP(hAPP(fequal(A),X),Y)),++equal(X,Y)]).
 
 input_clause(a7,axiom,
-[--equal(c_COMBI(T),c_COMBS(A,B,C))]).
-
-input_clause(a8,axiom,
-[--equal(c_COMBI(T),c_COMBB(A,B,C))]).
-
-input_clause(a9,axiom,
-[--equal(c_COMBI(T),c_COMBC(A,B,C))]).
-
-input_clause(a10,axiom,
-[--equal(c_COMBK(A,B),c_COMBS(A3,B3,C3))]).
-
-input_clause(a11,axiom,
-[--equal(c_COMBK(A,B),c_COMBB(A1,B1,C1))]).
-
-input_clause(a12,axiom,
-[--equal(c_COMBK(A,B),c_COMBC(A2,B2,C2))]).
-
-input_clause(a13,axiom,
-[--equal(c_COMBS(A3,B3,C3),c_COMBB(A1,B1,C1))]).
-
-input_clause(a14,axiom,
-[--equal(c_COMBS(A3,B3,C3),c_COMBC(A2,B2,C2))]).
-
-input_clause(a15,axiom,
-[--equal(c_COMBB(A1,B1,C1),c_COMBC(A2,B2,C2))]).
-
-input_clause(a16,axiom,
-[--hBOOL(hAPP(hAPP(fequal(A),X),Y)),++equal(X,Y)]).
-
-input_clause(a17,axiom,
 [++hBOOL(hAPP(hAPP(fequal(A),X),Y)),--equal(X,Y)]).
 
 
--- a/src/HOL/Tools/atp-inputs/const_comb_noS.dfg	Fri Jun 30 12:04:17 2006 +0200
+++ b/src/HOL/Tools/atp-inputs/const_comb_noS.dfg	Fri Jun 30 12:22:29 2006 +0200
@@ -23,45 +23,15 @@
 a5 ).
 
 clause(
-forall([A, B, T],
-or( not(equal(c_COMBI(T),c_COMBK(A,B))))),
-a6 ).
-
-clause(
-forall([A, B, C, T],
-or( not(equal(c_COMBI(T),c_COMBB(A,B,C))))),
-a8 ).
-
-clause(
-forall([A, B, C, T],
-or( not(equal(c_COMBI(T),c_COMBC(A,B,C))))),
-a9 ).
-
-clause(
-forall([A, A1, B, B1, C1],
-or( not(equal(c_COMBK(A,B),c_COMBB(A1,B1,C1))))),
-a11 ).
-
-clause(
-forall([A, A2, B, B2, C2],
-or( not(equal(c_COMBK(A,B),c_COMBC(A2,B2,C2))))),
-a12 ).
-
-clause(
-forall([A1, A2, B1, B2, C1, C2],
-or( not(equal(c_COMBB(A1,B1,C1),c_COMBC(A2,B2,C2))))),
-a15 ).
-
-clause(
 forall([A, X, Y],
 or( not(hBOOL(hAPP(hAPP(fequal(A),X),Y))),
     equal(X,Y))),
-a16 ).
+a6 ).
 
 clause(
 forall([A, X, Y],
 or( not(equal(X,Y)),
     hBOOL(hAPP(hAPP(fequal(A),X),Y)))),
-a17 ).
+a7 ).
 
 
--- a/src/HOL/Tools/atp-inputs/const_comb_noS.tptp	Fri Jun 30 12:04:17 2006 +0200
+++ b/src/HOL/Tools/atp-inputs/const_comb_noS.tptp	Fri Jun 30 12:22:29 2006 +0200
@@ -19,29 +19,10 @@
 input_clause(a5,axiom,
 [++equal(hAPP(hAPP(hAPP(c_COMBC(A,B,C),P),Q),R),hAPP(hAPP(P,R),Q))]).
 
-%the combinators are all different
 input_clause(a6,axiom,
-[--equal(c_COMBI(T),c_COMBK(A,B))]).
-
-input_clause(a8,axiom,
-[--equal(c_COMBI(T),c_COMBB(A,B,C))]).
-
-input_clause(a9,axiom,
-[--equal(c_COMBI(T),c_COMBC(A,B,C))]).
-
-input_clause(a11,axiom,
-[--equal(c_COMBK(A,B),c_COMBB(A1,B1,C1))]).
-
-input_clause(a12,axiom,
-[--equal(c_COMBK(A,B),c_COMBC(A2,B2,C2))]).
-
-input_clause(a15,axiom,
-[--equal(c_COMBB(A1,B1,C1),c_COMBC(A2,B2,C2))]).
-
-input_clause(a16,axiom,
 [--hBOOL(hAPP(hAPP(fequal(A),X),Y)),++equal(X,Y)]).
 
-input_clause(a17,axiom,
+input_clause(a7,axiom,
 [++hBOOL(hAPP(hAPP(fequal(A),X),Y)),--equal(X,Y)]).
 
 
--- a/src/HOL/Tools/atp-inputs/full_comb_inclS.dfg	Fri Jun 30 12:04:17 2006 +0200
+++ b/src/HOL/Tools/atp-inputs/full_comb_inclS.dfg	Fri Jun 30 12:22:29 2006 +0200
@@ -28,64 +28,14 @@
 a5 ).
 
 clause(
-forall([A, B, T],
-or( not(equal(typeinfo(c_COMBI,tc_fun(T,T)),typeinfo(c_COMBK,tc_fun(A,tc_fun(B,A))))))),
-a6 ).
-
-clause(
-forall([A, B, C, T],
-or( not(equal(typeinfo(c_COMBI,tc_fun(T,T)),typeinfo(c_COMBS,tc_fun(tc_fun(A,tc_fun(B,C)),tc_fun(tc_fun(A,B),tc_fun(A,C)))))))),
-a7 ).
-
-clause(
-forall([A, B, C, T],
-or( not(equal(typeinfo(c_COMBI,tc_fun(T,T)),typeinfo(c_COMBB,tc_fun(tc_fun(A,B),tc_fun(tc_fun(C,A),tc_fun(C,B)))))))),
-a8 ).
-
-clause(
-forall([A, B, C, T],
-or( not(equal(typeinfo(c_COMBI,tc_fun(T,T)),typeinfo(c_COMBC,tc_fun(tc_fun(A,tc_fun(B,C)),tc_fun(B,tc_fun(A,C)))))))),
-a9 ).
-
-clause(
-forall([A, A3, B, B3, C3],
-or( not(equal(typeinfo(c_COMBK,tc_fun(A,tc_fun(B,A))),typeinfo(c_COMBS,tc_fun(tc_fun(A3,tc_fun(B3,C3)),tc_fun(tc_fun(A3,B3),tc_fun(A3,C3)))))))),
-a10 ).
-
-clause(
-forall([A, A1, B, B1, C1],
-or( not(equal(typeinfo(c_COMBK,tc_fun(A,tc_fun(B,A))),typeinfo(c_COMBB,tc_fun(tc_fun(A1,B1),tc_fun(tc_fun(C1,A1),tc_fun(C1,B1)))))))),
-a11 ).
-
-clause(
-forall([A, A2, B, B2, C2],
-or( not(equal(typeinfo(c_COMBK,tc_fun(A,tc_fun(B,A))),typeinfo(c_COMBC,tc_fun(tc_fun(A2,tc_fun(B2,C2)),tc_fun(B2,tc_fun(A2,C2)))))))),
-a12 ).
-
-clause(
-forall([A1, A3, B1, B3, C1, C3],
-or( not(equal(typeinfo(c_COMBS,tc_fun(tc_fun(A3,tc_fun(B3,C3)),tc_fun(tc_fun(A3,B3),tc_fun(A3,C3)))),typeinfo(c_COMBB,tc_fun(tc_fun(A1,B1),tc_fun(tc_fun(C1,A1),tc_fun(C1,B1)))))))),
-a13 ).
-
-clause(
-forall([A2, A3, B2, B3, C2, C3],
-or( not(equal(typeinfo(c_COMBS,tc_fun(tc_fun(A3,tc_fun(B3,C3)),tc_fun(tc_fun(A3,B3),tc_fun(A3,C3)))),typeinfo(c_COMBC,tc_fun(tc_fun(A2,tc_fun(B2,C2)),tc_fun(B2,tc_fun(A2,C2)))))))),
-a14 ).
-
-clause(
-forall([A1, A2, B1, B2, C1, C2],
-or( not(equal(typeinfo(c_COMBB,tc_fun(tc_fun(A1,B1),tc_fun(tc_fun(C1,A1),tc_fun(C1,B1)))),typeinfo(c_COMBC,tc_fun(tc_fun(A2,tc_fun(B2,C2)),tc_fun(B2,tc_fun(A2,C2)))))))),
-a15 ).
-
-clause(
 forall([A, X, Y],
 or( not(hBOOL(typeinfo(hAPP(typeinfo(hAPP(typeinfo(fequal,tc_fun(A,tc_fun(A,tc_bool))),typeinfo(X,A)),tc_fun(A,tc_bool)),typeinfo(Y,A)),tc_bool))),
     equal(typeinfo(X,A),typeinfo(Y,A)))),
-a16 ).
+a6 ).
 
 clause(
 forall([A, X, Y],
 or( not(equal(typeinfo(X,A),typeinfo(Y,A))),
     hBOOL(typeinfo(hAPP(typeinfo(hAPP(typeinfo(fequal,tc_fun(A,tc_fun(A,tc_bool))),typeinfo(X,A)),tc_fun(A,tc_bool)),typeinfo(Y,A)),tc_bool)))),
-a17 ).
+a7 ).
 
--- a/src/HOL/Tools/atp-inputs/full_comb_inclS.tptp	Fri Jun 30 12:04:17 2006 +0200
+++ b/src/HOL/Tools/atp-inputs/full_comb_inclS.tptp	Fri Jun 30 12:22:29 2006 +0200
@@ -23,48 +23,11 @@
 input_clause(a5,axiom,
 [++equal(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(c_COMBC,tc_fun(tc_fun(A,tc_fun(B,C)),tc_fun(B,tc_fun(A,C)))),typeinfo(P,tc_fun(A,tc_fun(B,C)))),tc_fun(B,tc_fun(A,C))),typeinfo(Q,B)),tc_fun(A,C)),typeinfo(R,A)),C),typeinfo(hAPP(typeinfo(hAPP(typeinfo(P,tc_fun(A,tc_fun(B,C))),typeinfo(R,A)),tc_fun(B,C)),typeinfo(Q,B)),C))]).
 
-%the combinators are all different
 input_clause(a6,axiom,
-[--equal(typeinfo(c_COMBI,tc_fun(T,T)),typeinfo(c_COMBK,tc_fun(A,tc_fun(B,A))))]).
-
-input_clause(a7,axiom,
-[--equal(typeinfo(c_COMBI,tc_fun(T,T)),typeinfo(c_COMBS,tc_fun(tc_fun(A,tc_fun(B,C)),tc_fun(tc_fun(A,B),tc_fun(A,C)))))]).
-
-
-input_clause(a8,axiom,
-[--equal(typeinfo(c_COMBI,tc_fun(T,T)),typeinfo(c_COMBB,tc_fun(tc_fun(A,B),tc_fun(tc_fun(C,A),tc_fun(C,B)))))]).
-
-
-input_clause(a9,axiom,
-[--equal(typeinfo(c_COMBI,tc_fun(T,T)),typeinfo(c_COMBC,tc_fun(tc_fun(A,tc_fun(B,C)),tc_fun(B,tc_fun(A,C)))))]).
-
-
-input_clause(a10,axiom,
-[--equal(typeinfo(c_COMBK,tc_fun(A,tc_fun(B,A))),typeinfo(c_COMBS,tc_fun(tc_fun(A3,tc_fun(B3,C3)),tc_fun(tc_fun(A3,B3),tc_fun(A3,C3)))))]).
-
-input_clause(a11,axiom,
-[--equal(typeinfo(c_COMBK,tc_fun(A,tc_fun(B,A))),typeinfo(c_COMBB,tc_fun(tc_fun(A1,B1),tc_fun(tc_fun(C1,A1),tc_fun(C1,B1)))))]).
-
-
-input_clause(a12,axiom,
-[--equal(typeinfo(c_COMBK,tc_fun(A,tc_fun(B,A))),typeinfo(c_COMBC,tc_fun(tc_fun(A2,tc_fun(B2,C2)),tc_fun(B2,tc_fun(A2,C2)))))]).
-
-
-input_clause(a13,axiom,
-[--equal(typeinfo(c_COMBS,tc_fun(tc_fun(A3,tc_fun(B3,C3)),tc_fun(tc_fun(A3,B3),tc_fun(A3,C3)))),typeinfo(c_COMBB,tc_fun(tc_fun(A1,B1),tc_fun(tc_fun(C1,A1),tc_fun(C1,B1)))))]).
-
-
-input_clause(a14,axiom,
-[--equal(typeinfo(c_COMBS,tc_fun(tc_fun(A3,tc_fun(B3,C3)),tc_fun(tc_fun(A3,B3),tc_fun(A3,C3)))),typeinfo(c_COMBC,tc_fun(tc_fun(A2,tc_fun(B2,C2)),tc_fun(B2,tc_fun(A2,C2)))))]).
-
-input_clause(a15,axiom,
-[--equal(typeinfo(c_COMBB,tc_fun(tc_fun(A1,B1),tc_fun(tc_fun(C1,A1),tc_fun(C1,B1)))),typeinfo(c_COMBC,tc_fun(tc_fun(A2,tc_fun(B2,C2)),tc_fun(B2,tc_fun(A2,C2)))))]).
-
-input_clause(a16,axiom,
 [--hBOOL(typeinfo(hAPP(typeinfo(hAPP(typeinfo(fequal,tc_fun(A,tc_fun(A,tc_bool))),typeinfo(X,A)),tc_fun(A,tc_bool)),typeinfo(Y,A)),tc_bool)),
 ++equal(typeinfo(X,A),typeinfo(Y,A))]).
 
-input_clause(a17,axiom,
+input_clause(a7,axiom,
 [++hBOOL(typeinfo(hAPP(typeinfo(hAPP(typeinfo(fequal,tc_fun(A,tc_fun(A,tc_bool))),typeinfo(X,A)),tc_fun(A,tc_bool)),typeinfo(Y,A)),tc_bool)),
 --equal(typeinfo(X,A),typeinfo(Y,A))]).
 
--- a/src/HOL/Tools/atp-inputs/full_comb_noS.dfg	Fri Jun 30 12:04:17 2006 +0200
+++ b/src/HOL/Tools/atp-inputs/full_comb_noS.dfg	Fri Jun 30 12:22:29 2006 +0200
@@ -23,44 +23,14 @@
 a5 ).
 
 clause(
-forall([A, B, T],
-or( not(equal(typeinfo(c_COMBI,tc_fun(T,T)),typeinfo(c_COMBK,tc_fun(A,tc_fun(B,A))))))),
-a6 ).
-
-clause(
-forall([A, B, C, T],
-or( not(equal(typeinfo(c_COMBI,tc_fun(T,T)),typeinfo(c_COMBB,tc_fun(tc_fun(A,B),tc_fun(tc_fun(C,A),tc_fun(C,B)))))))),
-a8 ).
-
-clause(
-forall([A, B, C, T],
-or( not(equal(typeinfo(c_COMBI,tc_fun(T,T)),typeinfo(c_COMBC,tc_fun(tc_fun(A,tc_fun(B,C)),tc_fun(B,tc_fun(A,C)))))))),
-a9 ).
-
-clause(
-forall([A, A1, B, B1, C1],
-or( not(equal(typeinfo(c_COMBK,tc_fun(A,tc_fun(B,A))),typeinfo(c_COMBB,tc_fun(tc_fun(A1,B1),tc_fun(tc_fun(C1,A1),tc_fun(C1,B1)))))))),
-a11 ).
-
-clause(
-forall([A, A2, B, B2, C2],
-or( not(equal(typeinfo(c_COMBK,tc_fun(A,tc_fun(B,A))),typeinfo(c_COMBC,tc_fun(tc_fun(A2,tc_fun(B2,C2)),tc_fun(B2,tc_fun(A2,C2)))))))),
-a12 ).
-
-clause(
-forall([A1, A2, B1, B2, C1, C2],
-or( not(equal(typeinfo(c_COMBB,tc_fun(tc_fun(A1,B1),tc_fun(tc_fun(C1,A1),tc_fun(C1,B1)))),typeinfo(c_COMBC,tc_fun(tc_fun(A2,tc_fun(B2,C2)),tc_fun(B2,tc_fun(A2,C2)))))))),
-a15 ).
-
-clause(
 forall([A, X, Y],
 or( not(hBOOL(typeinfo(hAPP(typeinfo(hAPP(typeinfo(fequal,tc_fun(A,tc_fun(A,tc_bool))),typeinfo(X,A)),tc_fun(A,tc_bool)),typeinfo(Y,A)),tc_bool))),
     equal(typeinfo(X,A),typeinfo(Y,A)))),
-a16 ).
+a6 ).
 
 clause(
 forall([A, X, Y],
 or( not(equal(typeinfo(X,A),typeinfo(Y,A))),
     hBOOL(typeinfo(hAPP(typeinfo(hAPP(typeinfo(fequal,tc_fun(A,tc_fun(A,tc_bool))),typeinfo(X,A)),tc_fun(A,tc_bool)),typeinfo(Y,A)),tc_bool)))),
-a17 ).
+a7 ).
 
--- a/src/HOL/Tools/atp-inputs/full_comb_noS.tptp	Fri Jun 30 12:04:17 2006 +0200
+++ b/src/HOL/Tools/atp-inputs/full_comb_noS.tptp	Fri Jun 30 12:22:29 2006 +0200
@@ -19,33 +19,11 @@
 input_clause(a5,axiom,
 [++equal(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(c_COMBC,tc_fun(tc_fun(A,tc_fun(B,C)),tc_fun(B,tc_fun(A,C)))),typeinfo(P,tc_fun(A,tc_fun(B,C)))),tc_fun(B,tc_fun(A,C))),typeinfo(Q,B)),tc_fun(A,C)),typeinfo(R,A)),C),typeinfo(hAPP(typeinfo(hAPP(typeinfo(P,tc_fun(A,tc_fun(B,C))),typeinfo(R,A)),tc_fun(B,C)),typeinfo(Q,B)),C))]).
 
-%the combinators are all different
 input_clause(a6,axiom,
-[--equal(typeinfo(c_COMBI,tc_fun(T,T)),typeinfo(c_COMBK,tc_fun(A,tc_fun(B,A))))]).
-
-input_clause(a8,axiom,
-[--equal(typeinfo(c_COMBI,tc_fun(T,T)),typeinfo(c_COMBB,tc_fun(tc_fun(A,B),tc_fun(tc_fun(C,A),tc_fun(C,B)))))]).
-
-
-input_clause(a9,axiom,
-[--equal(typeinfo(c_COMBI,tc_fun(T,T)),typeinfo(c_COMBC,tc_fun(tc_fun(A,tc_fun(B,C)),tc_fun(B,tc_fun(A,C)))))]).
-
-input_clause(a11,axiom,
-[--equal(typeinfo(c_COMBK,tc_fun(A,tc_fun(B,A))),typeinfo(c_COMBB,tc_fun(tc_fun(A1,B1),tc_fun(tc_fun(C1,A1),tc_fun(C1,B1)))))]).
-
-
-input_clause(a12,axiom,
-[--equal(typeinfo(c_COMBK,tc_fun(A,tc_fun(B,A))),typeinfo(c_COMBC,tc_fun(tc_fun(A2,tc_fun(B2,C2)),tc_fun(B2,tc_fun(A2,C2)))))]).
-
-
-input_clause(a15,axiom,
-[--equal(typeinfo(c_COMBB,tc_fun(tc_fun(A1,B1),tc_fun(tc_fun(C1,A1),tc_fun(C1,B1)))),typeinfo(c_COMBC,tc_fun(tc_fun(A2,tc_fun(B2,C2)),tc_fun(B2,tc_fun(A2,C2)))))]).
-
-input_clause(a16,axiom,
 [--hBOOL(typeinfo(hAPP(typeinfo(hAPP(typeinfo(fequal,tc_fun(A,tc_fun(A,tc_bool))),typeinfo(X,A)),tc_fun(A,tc_bool)),typeinfo(Y,A)),tc_bool)),
 ++equal(typeinfo(X,A),typeinfo(Y,A))]).
 
-input_clause(a17,axiom,
+input_clause(a7,axiom,
 [++hBOOL(typeinfo(hAPP(typeinfo(hAPP(typeinfo(fequal,tc_fun(A,tc_fun(A,tc_bool))),typeinfo(X,A)),tc_fun(A,tc_bool)),typeinfo(Y,A)),tc_bool)),
 --equal(typeinfo(X,A),typeinfo(Y,A))]).
 
--- a/src/HOL/Tools/atp-inputs/par_comb_inclS.dfg	Fri Jun 30 12:04:17 2006 +0200
+++ b/src/HOL/Tools/atp-inputs/par_comb_inclS.dfg	Fri Jun 30 12:22:29 2006 +0200
@@ -28,54 +28,14 @@
 a5 ).
 
 clause(
-or( not(equal(c_COMBI,c_COMBK))),
-a6 ).
-
-clause(
-or( not(equal(c_COMBI,c_COMBS))),
-a7 ).
-
-clause(
-or( not(equal(c_COMBI,c_COMBB))),
-a8 ).
-
-clause(
-or( not(equal(c_COMBI,c_COMBC))),
-a9 ).
-
-clause(
-or( not(equal(c_COMBK,c_COMBS))),
-a10 ).
-
-clause(
-or( not(equal(c_COMBK,c_COMBB))),
-a11 ).
-
-clause(
-or( not(equal(c_COMBK,c_COMBC))),
-a12 ).
-
-clause(
-or( not(equal(c_COMBS,c_COMBB))),
-a13 ).
-
-clause(
-or( not(equal(c_COMBS,c_COMBC))),
-a14 ).
-
-clause(
-or( not(equal(c_COMBB,c_COMBC))),
-a15 ).
-
-clause(
 forall([A, X, Y],
 or( not(hBOOL(hAPP(hAPP(fequal,X,tc_fun(A,tc_fun(A,tc_bool))),Y,tc_fun(A,tc_bool)))),
     equal(X,Y))),
-a16 ).
+a6 ).
 
 clause(
 forall([A, X, Y],
 or( not(equal(X,Y)),
     hBOOL(hAPP(hAPP(fequal,X,tc_fun(A,tc_fun(A,tc_bool))),Y,tc_fun(A,tc_bool))))),
-a17 ).
+a7 ).
 
--- a/src/HOL/Tools/atp-inputs/par_comb_inclS.tptp	Fri Jun 30 12:04:17 2006 +0200
+++ b/src/HOL/Tools/atp-inputs/par_comb_inclS.tptp	Fri Jun 30 12:22:29 2006 +0200
@@ -25,42 +25,11 @@
 input_clause(a5,axiom,
 [++equal(hAPP(hAPP(hAPP(c_COMBC,P,tc_fun(tc_fun(A,tc_fun(B,C)),tc_fun(B,tc_fun(A,C)))),Q,tc_fun(B,tc_fun(A,C))),R,tc_fun(A,C)),hAPP(hAPP(P,R,tc_fun(A,tc_fun(B,C))),Q,tc_fun(B,C)))]).
 
-%the combinators are all different
 input_clause(a6,axiom,
-[--equal(c_COMBI,c_COMBK)]).
-
-input_clause(a7,axiom,
-[--equal(c_COMBI,c_COMBS)]).
-
-input_clause(a8,axiom,
-[--equal(c_COMBI,c_COMBB)]).
-
-input_clause(a9,axiom,
-[--equal(c_COMBI,c_COMBC)]).
-
-input_clause(a10,axiom,
-[--equal(c_COMBK,c_COMBS)]).
-
-input_clause(a11,axiom,
-[--equal(c_COMBK,c_COMBB)]).
-
-input_clause(a12,axiom,
-[--equal(c_COMBK,c_COMBC)]).
-
-input_clause(a13,axiom,
-[--equal(c_COMBS,c_COMBB)]).
-
-input_clause(a14,axiom,
-[--equal(c_COMBS,c_COMBC)]).
-
-input_clause(a15,axiom,
-[--equal(c_COMBB,c_COMBC)]).
-
-input_clause(a16,axiom,
 [--hBOOL(hAPP(hAPP(fequal,X,tc_fun(A,tc_fun(A,tc_bool))),Y,tc_fun(A,tc_bool))),
 ++equal(X,Y)]).
 
-input_clause(a17,axiom,
+input_clause(a7,axiom,
 [++hBOOL(hAPP(hAPP(fequal,X,tc_fun(A,tc_fun(A,tc_bool))),Y,tc_fun(A,tc_bool))),
 --equal(X,Y)]).
 
--- a/src/HOL/Tools/atp-inputs/par_comb_noS.dfg	Fri Jun 30 12:04:17 2006 +0200
+++ b/src/HOL/Tools/atp-inputs/par_comb_noS.dfg	Fri Jun 30 12:22:29 2006 +0200
@@ -23,38 +23,14 @@
 a5 ).
 
 clause(
-or( not(equal(c_COMBI,c_COMBK))),
-a6 ).
-
-clause(
-or( not(equal(c_COMBI,c_COMBB))),
-a8 ).
-
-clause(
-or( not(equal(c_COMBI,c_COMBC))),
-a9 ).
-
-clause(
-or( not(equal(c_COMBK,c_COMBB))),
-a11 ).
-
-clause(
-or( not(equal(c_COMBK,c_COMBC))),
-a12 ).
-
-clause(
-or( not(equal(c_COMBB,c_COMBC))),
-a15 ).
-
-clause(
 forall([A, X, Y],
 or( not(hBOOL(hAPP(hAPP(fequal,X,tc_fun(A,tc_fun(A,tc_bool))),Y,tc_fun(A,tc_bool)))),
     equal(X,Y))),
-a16 ).
+a6 ).
 
 clause(
 forall([A, X, Y],
 or( not(equal(X,Y)),
     hBOOL(hAPP(hAPP(fequal,X,tc_fun(A,tc_fun(A,tc_bool))),Y,tc_fun(A,tc_bool))))),
-a17 ).
+a7 ).
 
--- a/src/HOL/Tools/atp-inputs/par_comb_noS.tptp	Fri Jun 30 12:04:17 2006 +0200
+++ b/src/HOL/Tools/atp-inputs/par_comb_noS.tptp	Fri Jun 30 12:22:29 2006 +0200
@@ -20,30 +20,11 @@
 input_clause(a5,axiom,
 [++equal(hAPP(hAPP(hAPP(c_COMBC,P,tc_fun(tc_fun(A,tc_fun(B,C)),tc_fun(B,tc_fun(A,C)))),Q,tc_fun(B,tc_fun(A,C))),R,tc_fun(A,C)),hAPP(hAPP(P,R,tc_fun(A,tc_fun(B,C))),Q,tc_fun(B,C)))]).
 
-%the combinators are all different
 input_clause(a6,axiom,
-[--equal(c_COMBI,c_COMBK)]).
-
-input_clause(a8,axiom,
-[--equal(c_COMBI,c_COMBB)]).
-
-input_clause(a9,axiom,
-[--equal(c_COMBI,c_COMBC)]).
-
-input_clause(a11,axiom,
-[--equal(c_COMBK,c_COMBB)]).
-
-input_clause(a12,axiom,
-[--equal(c_COMBK,c_COMBC)]).
-
-input_clause(a15,axiom,
-[--equal(c_COMBB,c_COMBC)]).
-
-input_clause(a16,axiom,
 [--hBOOL(hAPP(hAPP(fequal,X,tc_fun(A,tc_fun(A,tc_bool))),Y,tc_fun(A,tc_bool))),
 ++equal(X,Y)]).
 
-input_clause(a17,axiom,
+input_clause(a7,axiom,
 [++hBOOL(hAPP(hAPP(fequal,X,tc_fun(A,tc_fun(A,tc_bool))),Y,tc_fun(A,tc_bool))),
 --equal(X,Y)]).
 
--- a/src/HOL/Tools/atp-inputs/u_comb_inclS.dfg	Fri Jun 30 12:04:17 2006 +0200
+++ b/src/HOL/Tools/atp-inputs/u_comb_inclS.dfg	Fri Jun 30 12:22:29 2006 +0200
@@ -28,54 +28,14 @@
 a5 ).
 
 clause(
-or( not(equal(c_COMBI,c_COMBK))),
-a6 ).
-
-clause(
-or( not(equal(c_COMBI,c_COMBS))),
-a7 ).
-
-clause(
-or( not(equal(c_COMBI,c_COMBB))),
-a8 ).
-
-clause(
-or( not(equal(c_COMBI,c_COMBC))),
-a9 ).
-
-clause(
-or( not(equal(c_COMBK,c_COMBS))),
-a10 ).
-
-clause(
-or( not(equal(c_COMBK,c_COMBB))),
-a11 ).
-
-clause(
-or( not(equal(c_COMBK,c_COMBC))),
-a12 ).
-
-clause(
-or( not(equal(c_COMBS,c_COMBB))),
-a13 ).
-
-clause(
-or( not(equal(c_COMBS,c_COMBC))),
-a14 ).
-
-clause(
-or( not(equal(c_COMBB,c_COMBC))),
-a15 ).
-
-clause(
 forall([X, Y],
 or( not(hBOOL(hAPP(hAPP(fequal,X),Y))),
     equal(X,Y))),
-a16 ).
+a6 ).
 
 clause(
 forall([X, Y],
 or( not(equal(X,Y)),
     hBOOL(hAPP(hAPP(fequal,X),Y)))),
-a17 ).
+a7 ).
 
--- a/src/HOL/Tools/atp-inputs/u_comb_inclS.tptp	Fri Jun 30 12:04:17 2006 +0200
+++ b/src/HOL/Tools/atp-inputs/u_comb_inclS.tptp	Fri Jun 30 12:22:29 2006 +0200
@@ -20,41 +20,10 @@
 input_clause(a5,axiom,
 [++equal(hAPP(hAPP(hAPP(c_COMBC,P),Q),R),hAPP(hAPP(P,R),Q))]).
 
-%the combinators are all different
 input_clause(a6,axiom,
-[--equal(c_COMBI,c_COMBK)]).
+[--hBOOL(hAPP(hAPP(fequal,X),Y)),++equal(X,Y)]).
 
 input_clause(a7,axiom,
-[--equal(c_COMBI,c_COMBS)]).
-
-input_clause(a8,axiom,
-[--equal(c_COMBI,c_COMBB)]).
-
-input_clause(a9,axiom,
-[--equal(c_COMBI,c_COMBC)]).
-
-input_clause(a10,axiom,
-[--equal(c_COMBK,c_COMBS)]).
-
-input_clause(a11,axiom,
-[--equal(c_COMBK,c_COMBB)]).
-
-input_clause(a12,axiom,
-[--equal(c_COMBK,c_COMBC)]).
-
-input_clause(a13,axiom,
-[--equal(c_COMBS,c_COMBB)]).
-
-input_clause(a14,axiom,
-[--equal(c_COMBS,c_COMBC)]).
-
-input_clause(a15,axiom,
-[--equal(c_COMBB,c_COMBC)]).
-
-input_clause(a16,axiom,
-[--hBOOL(hAPP(hAPP(fequal,X),Y)),++equal(X,Y)]).
-
-input_clause(a17,axiom,
 [++hBOOL(hAPP(hAPP(fequal,X),Y)),--equal(X,Y)]).
 
 
--- a/src/HOL/Tools/atp-inputs/u_comb_noS.dfg	Fri Jun 30 12:04:17 2006 +0200
+++ b/src/HOL/Tools/atp-inputs/u_comb_noS.dfg	Fri Jun 30 12:22:29 2006 +0200
@@ -23,38 +23,14 @@
 a5 ).
 
 clause(
-or( not(equal(c_COMBI,c_COMBK))),
-a6 ).
-
-clause(
-or( not(equal(c_COMBI,c_COMBB))),
-a8 ).
-
-clause(
-or( not(equal(c_COMBI,c_COMBC))),
-a9 ).
-
-clause(
-or( not(equal(c_COMBK,c_COMBB))),
-a11 ).
-
-clause(
-or( not(equal(c_COMBK,c_COMBC))),
-a12 ).
-
-clause(
-or( not(equal(c_COMBB,c_COMBC))),
-a15 ).
-
-clause(
 forall([X, Y],
 or( not(hBOOL(hAPP(hAPP(fequal,X),Y))),
     equal(X,Y))),
-a16 ).
+a6 ).
 
 clause(
 forall([X, Y],
 or( not(equal(X,Y)),
     hBOOL(hAPP(hAPP(fequal,X),Y)))),
-a17 ).
+a7 ).
 
--- a/src/HOL/Tools/atp-inputs/u_comb_noS.tptp	Fri Jun 30 12:04:17 2006 +0200
+++ b/src/HOL/Tools/atp-inputs/u_comb_noS.tptp	Fri Jun 30 12:22:29 2006 +0200
@@ -16,29 +16,10 @@
 input_clause(a5,axiom,
 [++equal(hAPP(hAPP(hAPP(c_COMBC,P),Q),R),hAPP(hAPP(P,R),Q))]).
 
-%the combinators are all different
 input_clause(a6,axiom,
-[--equal(c_COMBI,c_COMBK)]).
-
-input_clause(a8,axiom,
-[--equal(c_COMBI,c_COMBB)]).
-
-input_clause(a9,axiom,
-[--equal(c_COMBI,c_COMBC)]).
-
-input_clause(a11,axiom,
-[--equal(c_COMBK,c_COMBB)]).
-
-input_clause(a12,axiom,
-[--equal(c_COMBK,c_COMBC)]).
-
-input_clause(a15,axiom,
-[--equal(c_COMBB,c_COMBC)]).
-
-input_clause(a16,axiom,
 [--hBOOL(hAPP(hAPP(fequal,X),Y)),++equal(X,Y)]).
 
-input_clause(a17,axiom,
+input_clause(a7,axiom,
 [++hBOOL(hAPP(hAPP(fequal,X),Y)),--equal(X,Y)]).
isabelle