The cat is cold. The cat is red. The cat likes the tiger. The cat visits the rabbit. The rabbit is nice. The rabbit is red. The rabbit likes the cat. The rabbit visits the cat. The rabbit visits the tiger. The tiger is not blue. The tiger is nice. The tiger likes the cat. The tiger likes the rabbit. The tiger does not see the rabbit. The tiger visits the cat. Cold things are not blue.
The cat is cold.
("cat" "is" "cold" "+")
The cat is red.
("cat" "is" "red" "+")
The cat likes the tiger.
("cat" "likes" "tiger" "+")
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
The tiger is not blue.
("tiger" "is" "blue" "-")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger likes the cat.
("tiger" "likes" "cat" "+")
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
The tiger does not see the rabbit.
("tiger" "sees" "rabbit" "-")
The tiger visits the cat.
("tiger" "visits" "cat" "+")
Cold things are not blue.
((("something" "is" "cold" "+")) -> ("something" "is" "blue" "-"))
The rabbit visits the cat.
True
1
proof
[(triple8)]
("rabbit" "visits" "cat" "+")
triple8
The rabbit is not nice.
False
1
inv-proof
[(triple5)]
("rabbit" "is" "nice" "-")
triple5
The cat is not blue.
True
2
proof
[(((triple1) -> rule1))]
("cat" "is" "blue" "-")
((triple1) -> (rule1 % int1))
The cat is not blue.
("cat" "is" "blue" "-")
int1
The cat is blue.
False
2
inv-proof
[(((triple1) -> rule1))]
("cat" "is" "blue" "+")
((triple1) -> (rule1 % int1))
The cat is not blue.
("cat" "is" "blue" "-")
int1
The cat does not see the tiger.
Unknown
inv-random
[@0: The cat sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "tiger" "-")
The cat sees the rabbit.
Unknown
random
[@0: The cat sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "rabbit" "+")
The rabbit does not see the tiger.
Unknown
inv-random
[@0: The rabbit sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "tiger" "-")
The tiger is cold.
Unknown
random
[@0: The tiger is cold.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "cold" "+")
@0: The cat is cold.[(triple1)] The cat is red.[(triple2)] The cat likes the tiger.[(triple3)] The cat visits the rabbit.[(triple4)] The rabbit is nice.[(triple5)] The rabbit is red.[(triple6)] The rabbit likes the cat.[(triple7)] The rabbit visits the cat.[(triple8)] The rabbit visits the tiger.[(triple9)] The tiger does not see the rabbit.[(triple14)] The tiger is nice.[(triple11)] The tiger is not blue.[(triple10)] The tiger likes the cat.[(triple12)] The tiger likes the rabbit.[(triple13)] The tiger visits the cat.[(triple15)] @1: The cat is not blue.[(((triple1) -> rule1))]
The cat is cold.
("cat" "is" "cold" "+")
triple1
The cat is red.
("cat" "is" "red" "+")
triple2
The cat likes the tiger.
("cat" "likes" "tiger" "+")
triple3
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
triple4
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple5
The rabbit is red.
("rabbit" "is" "red" "+")
triple6
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
triple7
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
triple8
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
triple9
The tiger does not see the rabbit.
("tiger" "sees" "rabbit" "-")
triple14
The tiger is nice.
("tiger" "is" "nice" "+")
triple11
The tiger is not blue.
("tiger" "is" "blue" "-")
triple10
The tiger likes the cat.
("tiger" "likes" "cat" "+")
triple12
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
triple13
The tiger visits the cat.
("tiger" "visits" "cat" "+")
triple15
The cat is not blue.
("cat" "is" "blue" "-")
((triple1) -> (rule1 % int1))
The cat is not blue.
("cat" "is" "blue" "-")
int1