The cat eats the tiger. The cat is not big. The cat is blue. The cat is cold. The cat is red. The cat sees the tiger. The cat visits the tiger. The tiger is blue. The tiger is cold. The tiger is kind. The tiger sees the cat. The tiger visits the cat. If someone is red and they eat the tiger then they see the cat.
The cat eats the tiger.
("cat" "eats" "tiger" "+")
The cat is not big.
("cat" "is" "big" "-")
The cat is blue.
("cat" "is" "blue" "+")
The cat is cold.
("cat" "is" "cold" "+")
The cat is red.
("cat" "is" "red" "+")
The cat sees the tiger.
("cat" "sees" "tiger" "+")
The cat visits the tiger.
("cat" "visits" "tiger" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger sees the cat.
("tiger" "sees" "cat" "+")
The tiger visits the cat.
("tiger" "visits" "cat" "+")
If someone is red and they eat the tiger then they see the cat.
((("someone" "is" "red" "+") ("someone" "eats" "tiger" "+")) -> ("someone" "sees" "cat" "+"))
The cat visits the tiger.
True
1
proof
[(triple7)]
("cat" "visits" "tiger" "+")
triple7
The tiger is not kind.
False
1
inv-proof
[(triple10)]
("tiger" "is" "kind" "-")
triple10
The cat sees the cat.
True
3
proof
[(((triple5 triple1) -> rule1))]
("cat" "sees" "cat" "+")
((triple5 triple1) -> (rule1 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat does not see the cat.
False
3
inv-proof
[(((triple5 triple1) -> rule1))]
("cat" "sees" "cat" "-")
((triple5 triple1) -> (rule1 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The tiger does not eat the tiger.
Unknown
inv-random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "-")
The tiger visits the tiger.
Unknown
random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "+")
The cat does not eat the cat.
Unknown
inv-random
[@0: The cat eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cat" "-")
The tiger sees the tiger.
Unknown
random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "+")
@0: The cat eats the tiger.[(triple1)] The cat is blue.[(triple3)] The cat is cold.[(triple4)] The cat is not big.[(triple2)] The cat is red.[(triple5)] The cat sees the tiger.[(triple6)] The cat visits the tiger.[(triple7)] The tiger is blue.[(triple8)] The tiger is cold.[(triple9)] The tiger is kind.[(triple10)] The tiger sees the cat.[(triple11)] The tiger visits the cat.[(triple12)] @1: The cat sees the cat.[(((triple5 triple1) -> rule1))]
The cat eats the tiger.
("cat" "eats" "tiger" "+")
triple1
The cat is blue.
("cat" "is" "blue" "+")
triple3
The cat is cold.
("cat" "is" "cold" "+")
triple4
The cat is not big.
("cat" "is" "big" "-")
triple2
The cat is red.
("cat" "is" "red" "+")
triple5
The cat sees the tiger.
("cat" "sees" "tiger" "+")
triple6
The cat visits the tiger.
("cat" "visits" "tiger" "+")
triple7
The tiger is blue.
("tiger" "is" "blue" "+")
triple8
The tiger is cold.
("tiger" "is" "cold" "+")
triple9
The tiger is kind.
("tiger" "is" "kind" "+")
triple10
The tiger sees the cat.
("tiger" "sees" "cat" "+")
triple11
The tiger visits the cat.
("tiger" "visits" "cat" "+")
triple12
The cat sees the cat.
("cat" "sees" "cat" "+")
((triple5 triple1) -> (rule1 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1