The dog eats the lion. The dog visits the lion. The lion eats the dog. The lion is red. The lion is rough. The lion does not need the rabbit. The lion visits the dog. The lion does not visit the rabbit. The rabbit does not eat the dog. The rabbit eats the lion. The rabbit is blue. The rabbit is kind. The rabbit is red. The rabbit needs the dog. The rabbit needs the lion. The rabbit visits the dog. If the lion is red then the lion needs the dog. If something eats the rabbit and the rabbit needs the dog then the rabbit is blue. If the lion needs the dog and the dog visits the rabbit then the rabbit needs the dog.
The dog eats the lion.
("dog" "eats" "lion" "+")
The dog visits the lion.
("dog" "visits" "lion" "+")
The lion eats the dog.
("lion" "eats" "dog" "+")
The lion is red.
("lion" "is" "red" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion does not need the rabbit.
("lion" "needs" "rabbit" "-")
The lion visits the dog.
("lion" "visits" "dog" "+")
The lion does not visit the rabbit.
("lion" "visits" "rabbit" "-")
The rabbit does not eat the dog.
("rabbit" "eats" "dog" "-")
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
If the lion is red then the lion needs the dog.
((("lion" "is" "red" "+")) -> ("lion" "needs" "dog" "+"))
If something eats the rabbit and the rabbit needs the dog then the rabbit is blue.
((("something" "eats" "rabbit" "+") ("rabbit" "needs" "dog" "+")) -> ("rabbit" "is" "blue" "+"))
If the lion needs the dog and the dog visits the rabbit then the rabbit needs the dog.
((("lion" "needs" "dog" "+") ("dog" "visits" "rabbit" "+")) -> ("rabbit" "needs" "dog" "+"))
The dog eats the lion.
True
1
proof
[(triple1)]
("dog" "eats" "lion" "+")
triple1
The rabbit does not need the dog.
False
1
inv-proof
[(triple14)]
("rabbit" "needs" "dog" "-")
triple14
The lion needs the dog.
True
2
proof
[(((triple4) -> rule1))]
("lion" "needs" "dog" "+")
((triple4) -> (rule1 % int1))
The lion needs the dog.
("lion" "needs" "dog" "+")
int1
The lion does not need the dog.
False
2
inv-proof
[(((triple4) -> rule1))]
("lion" "needs" "dog" "-")
((triple4) -> (rule1 % int1))
The lion needs the dog.
("lion" "needs" "dog" "+")
int1
The dog does not need the lion.
Unknown
inv-random
[@0: The dog needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "lion" "-")
The rabbit visits the rabbit.
Unknown
random
[@0: The rabbit visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "rabbit" "+")
The dog is not red.
Unknown
inv-random
[@0: The dog is red.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "red" "-")
The lion is blue.
Unknown
random
[@0: The lion is blue.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "blue" "+")
@0: The dog eats the lion.[(triple1)] The dog visits the lion.[(triple2)] The lion does not need the rabbit.[(triple6)] The lion does not visit the rabbit.[(triple8)] The lion eats the dog.[(triple3)] The lion is red.[(triple4)] The lion is rough.[(triple5)] The lion visits the dog.[(triple7)] The rabbit does not eat the dog.[(triple9)] The rabbit eats the lion.[(triple10)] The rabbit is blue.[(triple11)] The rabbit is kind.[(triple12)] The rabbit is red.[(triple13)] The rabbit needs the dog.[(triple14)] The rabbit needs the lion.[(triple15)] The rabbit visits the dog.[(triple16)] @1: The lion needs the dog.[(((triple4) -> rule1))]
The dog eats the lion.
("dog" "eats" "lion" "+")
triple1
The dog visits the lion.
("dog" "visits" "lion" "+")
triple2
The lion does not need the rabbit.
("lion" "needs" "rabbit" "-")
triple6
The lion does not visit the rabbit.
("lion" "visits" "rabbit" "-")
triple8
The lion eats the dog.
("lion" "eats" "dog" "+")
triple3
The lion is red.
("lion" "is" "red" "+")
triple4
The lion is rough.
("lion" "is" "rough" "+")
triple5
The lion visits the dog.
("lion" "visits" "dog" "+")
triple7
The rabbit does not eat the dog.
("rabbit" "eats" "dog" "-")
triple9
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
triple10
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple11
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple12
The rabbit is red.
("rabbit" "is" "red" "+")
triple13
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
triple14
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
triple15
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
triple16
The lion needs the dog.
("lion" "needs" "dog" "+")
((triple4) -> (rule1 % int1))
The lion needs the dog.
("lion" "needs" "dog" "+")
int1