The cat chases the cow. The cat eats the cow. The cow chases the cat. If someone visits the cat then the cat chases the cow. If someone chases the cow then the cow eats the cat. If the cat eats the cow then the cow is cold. If someone is blue and they visit the cow then the cow is cold. If someone eats the cat and they visit the cow then the cow eats the cat. If the cat is young then the cat chases the cow. If someone is round and they visit the cat then the cat chases the cow. If someone chases the cat and they are cold then they chase the cow.
The cat chases the cow.
("cat" "chases" "cow" "+")
The cat eats the cow.
("cat" "eats" "cow" "+")
The cow chases the cat.
("cow" "chases" "cat" "+")
If someone visits the cat then the cat chases the cow.
((("someone" "visits" "cat" "+")) -> ("cat" "chases" "cow" "+"))
If someone chases the cow then the cow eats the cat.
((("someone" "chases" "cow" "+")) -> ("cow" "eats" "cat" "+"))
If the cat eats the cow then the cow is cold.
((("cat" "eats" "cow" "+")) -> ("cow" "is" "cold" "+"))
If someone is blue and they visit the cow then the cow is cold.
((("someone" "is" "blue" "+") ("someone" "visits" "cow" "+")) -> ("cow" "is" "cold" "+"))
If someone eats the cat and they visit the cow then the cow eats the cat.
((("someone" "eats" "cat" "+") ("someone" "visits" "cow" "+")) -> ("cow" "eats" "cat" "+"))
If the cat is young then the cat chases the cow.
((("cat" "is" "young" "+")) -> ("cat" "chases" "cow" "+"))
If someone is round and they visit the cat then the cat chases the cow.
((("someone" "is" "round" "+") ("someone" "visits" "cat" "+")) -> ("cat" "chases" "cow" "+"))
If someone chases the cat and they are cold then they chase the cow.
((("someone" "chases" "cat" "+") ("someone" "is" "cold" "+")) -> ("someone" "chases" "cow" "+"))
The cat eats the cow.
True
1
proof
[(triple2)]
("cat" "eats" "cow" "+")
triple2
The cat does not chase the cow.
False
1
inv-proof
[(triple1)]
("cat" "chases" "cow" "-")
triple1
The cow eats the cat.
True
2
proof
[(((triple1) -> rule2) OR ((((triple3 ((triple2) -> rule3)) -> rule8)) -> rule2))]
("cow" "eats" "cat" "+")
((triple1) -> (rule2 % int1))
The cow eats the cat.
("cow" "eats" "cat" "+")
int1
((((triple3 ((triple2) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The cow eats the cat.
("cow" "eats" "cat" "+")
int1
The cow chases the cow.
("cow" "chases" "cow" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3
The cow is not cold.
False
2
inv-proof
[(((triple2) -> rule3))]
("cow" "is" "cold" "-")
((triple2) -> (rule3 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow is not round.
Unknown
inv-random
[@0: The cow is round.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "round" "-")
The cow visits the cow.
Unknown
random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cow" "+")
The cow is not blue.
Unknown
inv-random
[@0: The cow is blue.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "blue" "-")
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 chases the cow.[(triple1)] The cat eats the cow.[(triple2)] The cow chases the cat.[(triple3)] @1: The cow eats the cat.[(((triple1) -> rule2) OR ((((triple3 ((triple2) -> rule3)) -> rule8)) -> rule2))] The cow is cold.[(((triple2) -> rule3))] @2: The cow chases the cow.[(((triple3 ((triple2) -> rule3)) -> rule8))]
The cat chases the cow.
("cat" "chases" "cow" "+")
triple1
The cat eats the cow.
("cat" "eats" "cow" "+")
triple2
The cow chases the cat.
("cow" "chases" "cat" "+")
triple3
The cow eats the cat.
("cow" "eats" "cat" "+")
((triple1) -> (rule2 % int1))
The cow eats the cat.
("cow" "eats" "cat" "+")
int1
((((triple3 ((triple2) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The cow eats the cat.
("cow" "eats" "cat" "+")
int1
The cow chases the cow.
("cow" "chases" "cow" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3
The cow is cold.
("cow" "is" "cold" "+")
((triple2) -> (rule3 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow chases the cow.
("cow" "chases" "cow" "+")
((triple3 ((triple2) -> (rule3 % int2))) -> (rule8 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2