-
Notifications
You must be signed in to change notification settings - Fork 0
/
x16AssRC.txt
32 lines (32 loc) · 1.75 KB
/
x16AssRC.txt
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
assign(max_weight, 15).
set(prolog_style_variables).
assign(max_given, 100).
set(raw).
set(binary_resolution).
assign(order, kbo).
assign(literal_selection, none).
clear(predicate_elim).
list(kbo_weights).
s = 3.
end_of_list.
formulas(sos).
( S1(0) <-> ( ( B1(0) <-> ( - ( ( - (A1(0) <-> A2(0) ) ) <-> C1(0)) ) & C1(s(0)) <-> (A1(0) & A2(0) | C1(0) & A1(0) | C1(0) & A2(0)) ) ) ) .
( S1(s(X)) <-> ( S1(X) & ( ( B1(X) <-> ( - ( ( - (A1(X) <-> A2(X) ) ) <-> C1(X)) ) & C1(s(X)) <-> (A1(X) & A2(X) | C1(X) & A1(X) | C1(X) & A2(X)) ) ) ) ) .
( N(X) | - S1(X) ) .
-C1(0) .
( S2(0) <-> ( ( S(0) <-> ( - ( ( - (B1(0) <-> A3(0) ) ) <-> C1'(0)) ) & C1'(s(0)) <-> (B1(0) & A3(0) | C1'(0) & B1(0) | C1'(0) & A3(0)) ) ) ) .
( S2(s(X)) <-> ( S2(X) & ( ( S(X) <-> ( - ( ( - (B1(X) <-> A3(X) ) ) <-> C1'(X)) ) & C1'(s(X)) <-> (B1(X) & A3(X) | C1'(X) & B1(X) | C1'(X) & A3(X)) ) ) ) ) .
( N(X) | - S2(X) ) .
-C1'(0) .
( S3(0) <-> ( ( S'(0) <-> ( - ( ( - (A1(0) <-> B2(0) ) ) <-> C2'(0)) ) & C2'(s(0)) <-> (A1(0) & B2(0) | C2'(0) & A1(0) | C2'(0) & B2(0)) ) ) ) .
( S3(s(X)) <-> ( S3(X) & ( ( S'(X) <-> ( - ( ( - (A1(X) <-> B2(X) ) ) <-> C2'(X)) ) & C2'(s(X)) <-> (A1(X) & B2(X) | C2'(X) & A1(X) | C2'(X) & B2(X)) ) ) ) ) .
( N(X) | - S3(X) ) .
-C2'(0) .
( S4(0) <-> ( ( B2(0) <-> ( - ( ( - (A2(0) <-> A3(0) ) ) <-> C2(0)) ) & C2(s(0)) <-> (A2(0) & A3(0) | C2(0) & A2(0) | C2(0) & A3(0)) ) ) ) .
( S4(s(X)) <-> ( S4(X) & ( ( B2(X) <-> ( - ( ( - (A2(X) <-> A3(X) ) ) <-> C2(X)) ) & C2(s(X)) <-> (A2(X) & A3(X) | C2(X) & A2(X) | C2(X) & A3(X)) ) ) ) ) .
( N(X) | - S4(X) ) .
-C2(0) .
( S5(0) <-> ( ( - (S(0) <-> S'(0)) ) ) ) .
( S5(s(X)) <-> ( S5(X) | ( ( - (S(X) <-> S'(X)) ) ) ) ) .
( N(X) | - S5(X) ) .
end_of_list.