The cat is red. The cat needs the cow. The cat sees the rabbit. The cat visits the cow. The cat visits the rabbit. The cow is green. The cow is kind. The cow is nice. The cow needs the rabbit. The cow sees the rabbit. The dog needs the rabbit. The dog sees the cow. The dog visits the cat. The rabbit needs the cow. The rabbit visits the cow. If the cat is nice and the cat is red then the cat visits the rabbit. If the cat sees the cow and the cat needs the cow then the cow visits the dog. If the dog needs the rabbit then the dog visits the cat. If the rabbit needs the cat and the rabbit is kind then the rabbit is nice. If something is green then it is red. If the cat sees the rabbit and the cat needs the rabbit then the rabbit is nice. If something needs the cat and the cat visits the cow then the cat visits the dog. If the rabbit is green then the rabbit is rough.
The cat is red.
("cat" "is" "red" "+")
The cat needs the cow.
("cat" "needs" "cow" "+")
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
The cat visits the cow.
("cat" "visits" "cow" "+")
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
The cow is green.
("cow" "is" "green" "+")
The cow is kind.
("cow" "is" "kind" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
The dog sees the cow.
("dog" "sees" "cow" "+")
The dog visits the cat.
("dog" "visits" "cat" "+")
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
If the cat is nice and the cat is red then the cat visits the rabbit.
((("cat" "is" "nice" "+") ("cat" "is" "red" "+")) -> ("cat" "visits" "rabbit" "+"))
If the cat sees the cow and the cat needs the cow then the cow visits the dog.
((("cat" "sees" "cow" "+") ("cat" "needs" "cow" "+")) -> ("cow" "visits" "dog" "+"))
If the dog needs the rabbit then the dog visits the cat.
((("dog" "needs" "rabbit" "+")) -> ("dog" "visits" "cat" "+"))
If the rabbit needs the cat and the rabbit is kind then the rabbit is nice.
((("rabbit" "needs" "cat" "+") ("rabbit" "is" "kind" "+")) -> ("rabbit" "is" "nice" "+"))
If something is green then it is red.
((("something" "is" "green" "+")) -> ("something" "is" "red" "+"))
If the cat sees the rabbit and the cat needs the rabbit then the rabbit is nice.
((("cat" "sees" "rabbit" "+") ("cat" "needs" "rabbit" "+")) -> ("rabbit" "is" "nice" "+"))
If something needs the cat and the cat visits the cow then the cat visits the dog.
((("something" "needs" "cat" "+") ("cat" "visits" "cow" "+")) -> ("cat" "visits" "dog" "+"))
If the rabbit is green then the rabbit is rough.
((("rabbit" "is" "green" "+")) -> ("rabbit" "is" "rough" "+"))
The cow sees the rabbit.
True
1
proof
[(triple10)]
("cow" "sees" "rabbit" "+")
triple10
The cat is not red.
False
1
inv-proof
[(triple1)]
("cat" "is" "red" "-")
triple1
The cow is red.
True
2
proof
[(((triple6) -> rule5))]
("cow" "is" "red" "+")
((triple6) -> (rule5 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow is not red.
False
2
inv-proof
[(((triple6) -> rule5))]
("cow" "is" "red" "-")
((triple6) -> (rule5 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The dog is not red.
Unknown
inv-rconc
[@1: The dog is red.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "is" "red" "-")
The rabbit is nice.
Unknown
rconc
[@1: The rabbit is nice.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("rabbit" "is" "nice" "+")
The dog does not need the cow.
Unknown
inv-random
[@0: The dog needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "cow" "-")
The cat is nice.
Unknown
random
[@0: The cat is nice.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "nice" "+")
@0: The cat is red.[(triple1)] The cat needs the cow.[(triple2)] The cat sees the rabbit.[(triple3)] The cat visits the cow.[(triple4)] The cat visits the rabbit.[(triple5)] The cow is green.[(triple6)] The cow is kind.[(triple7)] The cow is nice.[(triple8)] The cow needs the rabbit.[(triple9)] The cow sees the rabbit.[(triple10)] The dog needs the rabbit.[(triple11)] The dog sees the cow.[(triple12)] The dog visits the cat.[(triple13 OR ((triple11) -> rule3))] The rabbit needs the cow.[(triple14)] The rabbit visits the cow.[(triple15)] @1: The cow is red.[(((triple6) -> rule5))]
The cat is red.
("cat" "is" "red" "+")
triple1
The cat needs the cow.
("cat" "needs" "cow" "+")
triple2
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
triple3
The cat visits the cow.
("cat" "visits" "cow" "+")
triple4
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
triple5
The cow is green.
("cow" "is" "green" "+")
triple6
The cow is kind.
("cow" "is" "kind" "+")
triple7
The cow is nice.
("cow" "is" "nice" "+")
triple8
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
triple9
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
triple10
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
triple11
The dog sees the cow.
("dog" "sees" "cow" "+")
triple12
The dog visits the cat.
("dog" "visits" "cat" "+")
triple13
((triple11) -> (rule3 % int1))
The dog visits the cat.
("dog" "visits" "cat" "+")
int1
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
triple14
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
triple15
The cow is red.
("cow" "is" "red" "+")
((triple6) -> (rule5 % int1))
The cow is red.
("cow" "is" "red" "+")
int1