The cat eats the rabbit. The cat is cold. The cat is kind. The cat needs the dog. The cat needs the rabbit. The dog chases the cat. The dog is kind. The dog is rough. The dog needs the cat. The rabbit chases the cat. The rabbit eats the cat. The rabbit is cold. If someone needs the cat and they eat the cat then the cat is kind. If someone is young then they eat the rabbit. If the dog chases the rabbit and the rabbit eats the cat then the cat needs the rabbit. If the dog is nice and the dog needs the rabbit then the rabbit is young. If someone needs the cat and the cat is cold then they are rough. If someone eats the cat then they need the rabbit.
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
The cat is cold.
("cat" "is" "cold" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat needs the dog.
("cat" "needs" "dog" "+")
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
The dog chases the cat.
("dog" "chases" "cat" "+")
The dog is kind.
("dog" "is" "kind" "+")
The dog is rough.
("dog" "is" "rough" "+")
The dog needs the cat.
("dog" "needs" "cat" "+")
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
If someone needs the cat and they eat the cat then the cat is kind.
((("someone" "needs" "cat" "+") ("someone" "eats" "cat" "+")) -> ("cat" "is" "kind" "+"))
If someone is young then they eat the rabbit.
((("someone" "is" "young" "+")) -> ("someone" "eats" "rabbit" "+"))
If the dog chases the rabbit and the rabbit eats the cat then the cat needs the rabbit.
((("dog" "chases" "rabbit" "+") ("rabbit" "eats" "cat" "+")) -> ("cat" "needs" "rabbit" "+"))
If the dog is nice and the dog needs the rabbit then the rabbit is young.
((("dog" "is" "nice" "+") ("dog" "needs" "rabbit" "+")) -> ("rabbit" "is" "young" "+"))
If someone needs the cat and the cat is cold then they are rough.
((("someone" "needs" "cat" "+") ("cat" "is" "cold" "+")) -> ("someone" "is" "rough" "+"))
If someone eats the cat then they need the rabbit.
((("someone" "eats" "cat" "+")) -> ("someone" "needs" "rabbit" "+"))
The cat needs the rabbit.
True
1
proof
[(triple5)]
("cat" "needs" "rabbit" "+")
triple5
The dog is not rough.
False
1
inv-proof
[(triple8 OR ((triple9 triple2) -> rule5))]
("dog" "is" "rough" "-")
triple8
((triple9 triple2) -> (rule5 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The rabbit is not young.
Unknown
inv-rconc
[@1: The rabbit is young.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("rabbit" "is" "young" "-")
The cat eats the cat.
Unknown
random
[@0: The cat eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cat" "+")
@0: The cat eats the rabbit.[(triple1)] The cat is cold.[(triple2)] The cat is kind.[(triple3)] The cat needs the dog.[(triple4)] The cat needs the rabbit.[(triple5)] The dog chases the cat.[(triple6)] The dog is kind.[(triple7)] The dog is rough.[(triple8 OR ((triple9 triple2) -> rule5))] The dog needs the cat.[(triple9)] The rabbit chases the cat.[(triple10)] The rabbit eats the cat.[(triple11)] The rabbit is cold.[(triple12)] @1: The rabbit needs the rabbit.[(((triple11) -> rule6))]
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
triple1
The cat is cold.
("cat" "is" "cold" "+")
triple2
The cat is kind.
("cat" "is" "kind" "+")
triple3
The cat needs the dog.
("cat" "needs" "dog" "+")
triple4
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
triple5
The dog chases the cat.
("dog" "chases" "cat" "+")
triple6
The dog is kind.
("dog" "is" "kind" "+")
triple7
The dog is rough.
("dog" "is" "rough" "+")
triple8
((triple9 triple2) -> (rule5 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The dog needs the cat.
("dog" "needs" "cat" "+")
triple9
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
triple10
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
triple11
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple12
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
((triple11) -> (rule6 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1