1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
|
%------------------------------------------------------------------------------
% File : SYN000+2 : TPTP v5.5.0. Bugfixed v4.1.1.
% Domain : Syntactic
% Problem : Advanced TPTP FOF syntax
% Version : Biased.
% English : Advanced TPTP FOF syntax that you will encounter some time.
% Refs :
% Source : [TPTP]
% Names :
% Status : Satisfiable
% Rating : 0.50 v5.5.0, 0.67 v5.2.0, 1.00 v5.0.0
% Syntax : Number of formulae : 20 ( 16 unit)
% Number of atoms : 31 ( 2 equality)
% Maximal formula depth : 7 ( 2 average)
% Number of connectives : 13 ( 2 ~; 9 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% ( 1 ~|; 1 ~&)
% Number of predicates : 8 ( 3 propositional; 0-3 arity)
% Number of functors : 22 ( 20 constant; 0-3 arity)
% Number of variables : 8 ( 0 sgn; 8 !; 0 ?)
% Maximal term depth : 2 ( 1 average)
% Arithmetic symbols : 12 ( 0 pred; 0 func; 12 numbers)
% SPC : FOF_SAT_RFO_SEQ
% Comments :
% Bugfixes : v4.0.1 - Added more numbers, particularly rationals.
% : v4.1.1 - Removed rationals with negative denominators.
%------------------------------------------------------------------------------
%----Quoted symbols
fof(distinct_object,axiom,(
"An Apple" != "A \"Microsoft \\ escape\"" )).
%----Numbers
fof(integers,axiom,
( p(12)
| p(-12) )).
fof(rationals,axiom,
( p(123/456)
| p(-123/456)
| p(+123/456) )).
fof(reals,axiom,
( p(123.456 )
| p(-123.456 )
| p(123.456E789 )
| p(123.456e789 )
| p(-123.456E789 )
| p(123.456E-789 )
| p(-123.456E-789 ) )).
%----Connectives - seen |, &, =>, ~ already
fof(never_used_connectives,axiom,(
! [X] :
( ( p(X)
~| ~ q(X,a) )
~& p(X) ) )).
%----Roles
fof(role_definition,definition,(
! [X] : f(d) = f(X) )).
fof(role_assumption,assumption,(
p(a) )).
fof(role_lemma,lemma,(
p(l) )).
fof(role_theorem,theorem,(
p(t) )).
fof(role_unknown,unknown,(
p(u) )).
%----Selective include directive
include('Axioms/SYN000+0.ax',[ia1,ia3]).
%----Source
fof(source_unknown,axiom,(
! [X] : p(X) ),
unknown).
fof(source,axiom,(
! [X] : p(X) ),
file('SYN000-1.p')).
fof(source_name,axiom,(
! [X] : p(X) ),
file('SYN000-1.p',source_unknown)).
fof(source_copy,axiom,(
! [X] : p(X) ),
source_unknown).
fof(source_introduced_assumption,axiom,(
! [X] : p(X) ),
introduced(assumption,[from,the,world])).
fof(source_inference,plain,(
p(a) ),
inference(magic,
[status(thm),assumptions([source_introduced_assumption])],
[theory(equality),source_unknown])).
fof(source_inference_with_bind,plain,(
p(a) ),
inference(magic,
[status(thm)],
[theory(equality),source_unknown:[bind(X,$fot(a))]])).
%----Useful info
fof(useful_info,axiom,(
! [X] : p(X) ),
unknown,
[simple,
prolog(like,Data,[nested,12.2]),
AVariable,
12.2,
"A distinct object",
$fof(p(X) | ~ q(X,a) | r(X,f(Y),g(X,f(Y),Z)) | ~ s(f(f(f(b))))),
data(name):[colon,list,2],
[simple,prolog(like,Data,[nested,12.2]),AVariable,12.2]
]).
%------------------------------------------------------------------------------
|
