-
Notifications
You must be signed in to change notification settings - Fork 0
/
result.txt
78 lines (74 loc) · 3.6 KB
/
result.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
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
--------------------------SPASS-START-----------------------------
Input Problem:
1[0:Inp] || ElectronicSurveillance* -> .
2[0:Inp] || -> Intentional(Acquisition)*.
3[0:Inp] || -> Surv(Device)*.
4[0:Inp] || -> Surv_US(Device)*.
5[0:Inp] || -> USP(Person)*.
6[0:Inp] || -> ReceiveUS(Contents)*.
7[0:Inp] || -> SentUS(Contents)*.
8[0:Inp] || -> REP_LE(Person)*.
9[0:Inp] || Consent* -> .
10[0:Inp] || -> Tres(Contents)*.
11[0:Inp] || Wire(Contents)* -> .
12[0:Inp] || Radio(Contents)* -> .
13[0:Inp] || Target(Person)* -> .
14[0:Inp] || Wire(Contents)* -> SkC0.
15[0:Inp] || Radio(Contents)* -> SkC0.
16[0:Inp] || Surv_US(Device) Surv(Device)* REP_LE(Contents) -> Radio(Contents) Wire(Contents) ElectronicSurveillance.
17[0:Inp] || SentUS(Contents) Surv(Device)* Wire(Contents) Surv_US(Device) -> Consent Tres(Contents) ElectronicSurveillance.
18[0:Inp] || ReceiveUS(Contents) Surv(Device)* Wire(Contents) Surv_US(Device) -> Consent Tres(Contents) ElectronicSurveillance.
19[0:Inp] || SentUS(Contents) Surv(Device)* USP(Person) Target(Person) REP_LE(Person) SkC0 -> ElectronicSurveillance.
20[0:Inp] || ReceiveUS(Contents) Surv(Device)* USP(Person) Target(Person) REP_LE(Person) SkC0 -> ElectronicSurveillance.
21[0:Inp] || Intentional(Acquisition)* Surv(Device) Radio(Contents) REP_LE(Contents) SentUS(Contents) ReceiveUS(Contents) -> ElectronicSurveillance.
This is a propositional Non-Horn problem.
The following monadic predicates have finite extensions: REP_LE, SentUS, ReceiveUS, USP, Surv_US, Surv, Intentional.
Axiom clauses: 20 Conjecture clauses: 1
Inferences:
Reductions: RFMRR=1 RBMRR=1 RObv=1 RUnC=1 RTaut=1 RFSub=1 RBSub=1
Extras : Input Saturation, Always Selection, Full Splitting, Full Reduction, Ratio: 5, FuncWeight: 1, VarWeight: 1
Precedence: ElectronicSurveillance > Intentional > Tres > Consent > SkC0 > Wire > Radio > Surv > Surv_US > USP > Target > SentUS > ReceiveUS > REP_LE > Person > Contents > Device > Acquisition
Ordering : KBO
Processed Problem:
Worked Off Clauses:
Usable Clauses:
10[0:Inp] || -> Tres(Contents)*.
7[0:Inp] || -> SentUS(Contents)*.
6[0:Inp] || -> ReceiveUS(Contents)*.
5[0:Inp] || -> USP(Person)*.
4[0:Inp] || -> Surv_US(Device)*.
3[0:Inp] || -> Surv(Device)*.
2[0:Inp] || -> Intentional(Acquisition)*.
8[0:Inp] || -> REP_LE(Person)*.
9[0:Inp] || Consent* -> .
1[0:Inp] || ElectronicSurveillance* -> .
13[0:Inp] || Target(Person)* -> .
12[0:Inp] || Radio(Contents)* -> .
11[0:Inp] || Wire(Contents)* -> .
16[0:Inp] || REP_LE(Contents)* -> .
Given clause: 10[0:Inp] || -> Tres(Contents)*.
Given clause: 7[0:Inp] || -> SentUS(Contents)*.
Given clause: 6[0:Inp] || -> ReceiveUS(Contents)*.
Given clause: 5[0:Inp] || -> USP(Person)*.
Given clause: 4[0:Inp] || -> Surv_US(Device)*.
Given clause: 3[0:Inp] || -> Surv(Device)*.
Given clause: 2[0:Inp] || -> Intentional(Acquisition)*.
Given clause: 8[0:Inp] || -> REP_LE(Person)*.
Given clause: 9[0:Inp] || Consent*+ -> .
Given clause: 1[0:Inp] || ElectronicSurveillance*+ -> .
Given clause: 13[0:Inp] || Target(Person)*+ -> .
Given clause: 12[0:Inp] || Radio(Contents)*+ -> .
Given clause: 11[0:Inp] || Wire(Contents)*+ -> .
Given clause: 16[0:Inp] || REP_LE(Contents)*+ -> .
SPASS V 3.9
SPASS beiseite: Completion found.
Problem: spass.txt
SPASS derived 0 clauses, backtracked 0 clauses, performed 0 splits and kept 14 clauses.
SPASS allocated 72635 KBytes.
SPASS spent 0:00:00.04 on the problem.
0:00:00.02 for the input.
0:00:00.01 for the FLOTTER CNF translation.
0:00:00.00 for inferences.
0:00:00.00 for the backtracking.
0:00:00.00 for the reduction.
--------------------------SPASS-STOP------------------------------