The dog is rough. The dog is young. The dog needs the lion. The dog needs the tiger. The dog sees the lion. The lion visits the tiger. The rabbit is red. The rabbit needs the dog. The rabbit sees the lion. The tiger needs the lion. If the dog is rough then the dog visits the lion. If someone visits the rabbit then the rabbit needs the tiger.
The dog is rough.
("dog" "is" "rough" "+")
The dog is young.
("dog" "is" "young" "+")
The dog needs the lion.
("dog" "needs" "lion" "+")
The dog needs the tiger.
("dog" "needs" "tiger" "+")
The dog sees the lion.
("dog" "sees" "lion" "+")
The lion visits the tiger.
("lion" "visits" "tiger" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
The tiger needs the lion.
("tiger" "needs" "lion" "+")
If the dog is rough then the dog visits the lion.
((("dog" "is" "rough" "+")) -> ("dog" "visits" "lion" "+"))
If someone visits the rabbit then the rabbit needs the tiger.
((("someone" "visits" "rabbit" "+")) -> ("rabbit" "needs" "tiger" "+"))
The tiger needs the lion.
True
1
proof
[(triple10)]
("tiger" "needs" "lion" "+")
triple10
The rabbit does not see the lion.
False
1
inv-proof
[(triple9)]
("rabbit" "sees" "lion" "-")
triple9
The dog visits the lion.
True
2
proof
[(((triple1) -> rule1))]
("dog" "visits" "lion" "+")
((triple1) -> (rule1 % int1))
The dog visits the lion.
("dog" "visits" "lion" "+")
int1
The dog does not visit the lion.
False
2
inv-proof
[(((triple1) -> rule1))]
("dog" "visits" "lion" "-")
((triple1) -> (rule1 % int1))
The dog visits the lion.
("dog" "visits" "lion" "+")
int1
The rabbit does not need the tiger.
Unknown
inv-rconc
[@1: The rabbit needs the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "needs" "tiger" "-")
The rabbit is nice.
Unknown
random
[@0: The rabbit is nice.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "nice" "+")
The lion does not visit the rabbit.
Unknown
inv-random
[@0: The lion visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "rabbit" "-")
The rabbit needs the lion.
Unknown
random
[@0: The rabbit needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "lion" "+")
@0: The dog is rough.[(triple1)] The dog is young.[(triple2)] The dog needs the lion.[(triple3)] The dog needs the tiger.[(triple4)] The dog sees the lion.[(triple5)] The lion visits the tiger.[(triple6)] The rabbit is red.[(triple7)] The rabbit needs the dog.[(triple8)] The rabbit sees the lion.[(triple9)] The tiger needs the lion.[(triple10)] @1: The dog visits the lion.[(((triple1) -> rule1))]
The dog is rough.
("dog" "is" "rough" "+")
triple1
The dog is young.
("dog" "is" "young" "+")
triple2
The dog needs the lion.
("dog" "needs" "lion" "+")
triple3
The dog needs the tiger.
("dog" "needs" "tiger" "+")
triple4
The dog sees the lion.
("dog" "sees" "lion" "+")
triple5
The lion visits the tiger.
("lion" "visits" "tiger" "+")
triple6
The rabbit is red.
("rabbit" "is" "red" "+")
triple7
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
triple8
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
triple9
The tiger needs the lion.
("tiger" "needs" "lion" "+")
triple10
The dog visits the lion.
("dog" "visits" "lion" "+")
((triple1) -> (rule1 % int1))
The dog visits the lion.
("dog" "visits" "lion" "+")
int1