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