The cat is big. The cat is blue. The cat is cold. The cat is nice. The cat likes the rabbit. The cat needs the rabbit. The cat visits the rabbit. The rabbit is big. The rabbit is blue. The rabbit is cold. The rabbit is nice. The rabbit is young. The rabbit likes the cat. The rabbit needs the cat. The rabbit visits the cat. If someone likes the rabbit and the rabbit visits the cat then the rabbit is big. If someone is nice and they like the cat then the cat is nice. If someone visits the cat and the cat is blue then the cat needs the rabbit. If someone likes the cat and the cat visits the rabbit then the cat is cold. If the cat is blue and the cat is nice then the cat needs the rabbit. If someone is cold then they visit the rabbit.
The cat is big.
("cat" "is" "big" "+")
The cat is blue.
("cat" "is" "blue" "+")
The cat is cold.
("cat" "is" "cold" "+")
The cat is nice.
("cat" "is" "nice" "+")
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
If someone likes the rabbit and the rabbit visits the cat then the rabbit is big.
((("someone" "likes" "rabbit" "+") ("rabbit" "visits" "cat" "+")) -> ("rabbit" "is" "big" "+"))
If someone is nice and they like the cat then the cat is nice.
((("someone" "is" "nice" "+") ("someone" "likes" "cat" "+")) -> ("cat" "is" "nice" "+"))
If someone visits the cat and the cat is blue then the cat needs the rabbit.
((("someone" "visits" "cat" "+") ("cat" "is" "blue" "+")) -> ("cat" "needs" "rabbit" "+"))
If someone likes the cat and the cat visits the rabbit then the cat is cold.
((("someone" "likes" "cat" "+") ("cat" "visits" "rabbit" "+")) -> ("cat" "is" "cold" "+"))
If the cat is blue and the cat is nice then the cat needs the rabbit.
((("cat" "is" "blue" "+") ("cat" "is" "nice" "+")) -> ("cat" "needs" "rabbit" "+"))
If someone is cold then they visit the rabbit.
((("someone" "is" "cold" "+")) -> ("someone" "visits" "rabbit" "+"))
The rabbit is big.
True
1
proof
[(triple8 OR ((triple5 triple15) -> rule1))]
("rabbit" "is" "big" "+")
triple8
((triple5 triple15) -> (rule1 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The cat does not like the rabbit.
False
1
inv-proof
[(triple5)]
("cat" "likes" "rabbit" "-")
triple5
The rabbit visits the rabbit.
True
2
proof
[(((triple10) -> rule6))]
("rabbit" "visits" "rabbit" "+")
((triple10) -> (rule6 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit does not visit the rabbit.
False
2
inv-proof
[(((triple10) -> rule6))]
("rabbit" "visits" "rabbit" "-")
((triple10) -> (rule6 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit does not like the rabbit.
Unknown
inv-random
[@0: The rabbit likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "rabbit" "-")
The cat needs the cat.
Unknown
random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "+")
The rabbit does not need the rabbit.
Unknown
inv-random
[@0: The rabbit needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "rabbit" "-")
The cat visits the cat.
Unknown
random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "+")
@0: The cat is big.[(triple1)] The cat is blue.[(triple2)] The cat is cold.[(triple3 OR ((triple13 triple7) -> rule4))] The cat is nice.[(triple4 OR ((triple11 triple13) -> rule2))] The cat likes the rabbit.[(triple5)] The cat needs the rabbit.[(triple6 OR ((triple15 triple2) -> rule3) OR ((triple2 triple4) -> rule5) OR ((triple2 ((triple11 triple13) -> rule2)) -> rule5))] The cat visits the rabbit.[(triple7 OR ((triple3) -> rule6))] The rabbit is big.[(triple8 OR ((triple5 triple15) -> rule1))] The rabbit is blue.[(triple9)] The rabbit is cold.[(triple10)] The rabbit is nice.[(triple11)] The rabbit is young.[(triple12)] The rabbit likes the cat.[(triple13)] The rabbit needs the cat.[(triple14)] The rabbit visits the cat.[(triple15)] @1: The rabbit visits the rabbit.[(((triple10) -> rule6))]
The cat is big.
("cat" "is" "big" "+")
triple1
The cat is blue.
("cat" "is" "blue" "+")
triple2
The cat is cold.
("cat" "is" "cold" "+")
triple3
((triple13 triple7) -> (rule4 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
triple4
((triple11 triple13) -> (rule2 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
triple5
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
triple6
((triple15 triple2) -> (rule3 % int1))
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
int1
((triple2 triple4) -> (rule5 % int1))
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
int1
((triple2 ((triple11 triple13) -> (rule2 % int2))) -> (rule5 % int1))
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
triple7
((triple3) -> (rule6 % int1))
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
triple8
((triple5 triple15) -> (rule1 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple9
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple10
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple11
The rabbit is young.
("rabbit" "is" "young" "+")
triple12
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
triple13
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
triple14
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
triple15
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
((triple10) -> (rule6 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1