The cat sees the lion. The cat visits the dog. The dog is big. The dog sees the rabbit. The dog visits the cat. The lion is big. The lion needs the cat. The lion needs the dog. The lion needs the rabbit. The rabbit is green. The rabbit needs the cat. The rabbit visits the lion. If someone visits the dog then the dog visits the rabbit.
The cat sees the lion.
("cat" "sees" "lion" "+")
The cat visits the dog.
("cat" "visits" "dog" "+")
The dog is big.
("dog" "is" "big" "+")
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
The dog visits the cat.
("dog" "visits" "cat" "+")
The lion is big.
("lion" "is" "big" "+")
The lion needs the cat.
("lion" "needs" "cat" "+")
The lion needs the dog.
("lion" "needs" "dog" "+")
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
If someone visits the dog then the dog visits the rabbit.
((("someone" "visits" "dog" "+")) -> ("dog" "visits" "rabbit" "+"))
The lion needs the rabbit.
True
1
proof
[(triple9)]
("lion" "needs" "rabbit" "+")
triple9
The dog does not see the rabbit.
False
1
inv-proof
[(triple4)]
("dog" "sees" "rabbit" "-")
triple4
The dog is not kind.
Unknown
inv-random
[@0: The dog is kind.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "kind" "-")
The lion sees the rabbit.
Unknown
random
[@0: The lion sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "rabbit" "+")
@0: The cat sees the lion.[(triple1)] The cat visits the dog.[(triple2)] The dog is big.[(triple3)] The dog sees the rabbit.[(triple4)] The dog visits the cat.[(triple5)] The lion is big.[(triple6)] The lion needs the cat.[(triple7)] The lion needs the dog.[(triple8)] The lion needs the rabbit.[(triple9)] The rabbit is green.[(triple10)] The rabbit needs the cat.[(triple11)] The rabbit visits the lion.[(triple12)] @1: The dog visits the rabbit.[(((triple2) -> rule1))]
The cat sees the lion.
("cat" "sees" "lion" "+")
triple1
The cat visits the dog.
("cat" "visits" "dog" "+")
triple2
The dog is big.
("dog" "is" "big" "+")
triple3
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
triple4
The dog visits the cat.
("dog" "visits" "cat" "+")
triple5
The lion is big.
("lion" "is" "big" "+")
triple6
The lion needs the cat.
("lion" "needs" "cat" "+")
triple7
The lion needs the dog.
("lion" "needs" "dog" "+")
triple8
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
triple9
The rabbit is green.
("rabbit" "is" "green" "+")
triple10
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
triple11
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
triple12
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
((triple2) -> (rule1 % int1))
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
int1