The cow eats the mouse. The mouse visits the cow. If someone visits the cow then the cow visits the mouse. If someone likes the mouse then the mouse eats the cow. If someone is blue and they eat the mouse then they visit the cow. If the mouse visits the cow then the mouse is blue. If someone visits the cow then the cow is cold. If the cow visits the mouse then the cow likes the mouse.
The cow eats the mouse.
("cow" "eats" "mouse" "+")
The mouse visits the cow.
("mouse" "visits" "cow" "+")
If someone visits the cow then the cow visits the mouse.
((("someone" "visits" "cow" "+")) -> ("cow" "visits" "mouse" "+"))
If someone likes the mouse then the mouse eats the cow.
((("someone" "likes" "mouse" "+")) -> ("mouse" "eats" "cow" "+"))
If someone is blue and they eat the mouse then they visit the cow.
((("someone" "is" "blue" "+") ("someone" "eats" "mouse" "+")) -> ("someone" "visits" "cow" "+"))
If the mouse visits the cow then the mouse is blue.
((("mouse" "visits" "cow" "+")) -> ("mouse" "is" "blue" "+"))
If someone visits the cow then the cow is cold.
((("someone" "visits" "cow" "+")) -> ("cow" "is" "cold" "+"))
If the cow visits the mouse then the cow likes the mouse.
((("cow" "visits" "mouse" "+")) -> ("cow" "likes" "mouse" "+"))
The cow eats the mouse.
True
1
proof
[(triple1)]
("cow" "eats" "mouse" "+")
triple1
The mouse does not visit the cow.
False
1
inv-proof
[(triple2)]
("mouse" "visits" "cow" "-")
triple2
The cow is cold.
True
2
proof
[(((triple2) -> rule5))]
("cow" "is" "cold" "+")
((triple2) -> (rule5 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The mouse is not blue.
False
2
inv-proof
[(((triple2) -> rule4))]
("mouse" "is" "blue" "-")
((triple2) -> (rule4 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The cow likes the mouse.
True
3
proof
[(((((triple2) -> rule1)) -> rule6))]
("cow" "likes" "mouse" "+")
((((triple2) -> (rule1 % int2))) -> (rule6 % int1))
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int1
The cow visits the mouse.
("cow" "visits" "mouse" "+")
int2
The cow does not like the mouse.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule6))]
("cow" "likes" "mouse" "-")
((((triple2) -> (rule1 % int2))) -> (rule6 % int1))
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int1
The cow visits the mouse.
("cow" "visits" "mouse" "+")
int2
The mouse eats the cow.
True
4
proof
[(((((((triple2) -> rule1)) -> rule6)) -> rule2))]
("mouse" "eats" "cow" "+")
((((((triple2) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The mouse eats the cow.
("mouse" "eats" "cow" "+")
int1
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int2
The cow visits the mouse.
("cow" "visits" "mouse" "+")
int3
The mouse does not eat the cow.
False
4
inv-proof
[(((((((triple2) -> rule1)) -> rule6)) -> rule2))]
("mouse" "eats" "cow" "-")
((((((triple2) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The mouse eats the cow.
("mouse" "eats" "cow" "+")
int1
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int2
The cow visits the mouse.
("cow" "visits" "mouse" "+")
int3
The cow does not visit the cow.
Unknown
inv-rconc
[@1: The cow visits the cow.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "visits" "cow" "-")
The mouse is red.
Unknown
random
[@0: The mouse is red.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "red" "+")
The cow is not big.
Unknown
inv-random
[@0: The cow is big.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "big" "-")
The mouse visits the mouse.
Unknown
random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "+")
The cow does not eat the cow.
Unknown
inv-random
[@0: The cow eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "cow" "-")
The mouse likes the mouse.
Unknown
random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "+")
The cow is not green.
Unknown
inv-random
[@0: The cow is green.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "green" "-")
The cow likes the cow.
Unknown
random
[@0: The cow likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "cow" "+")
@0: The cow eats the mouse.[(triple1)] The mouse visits the cow.[(triple2)] @1: The cow is cold.[(((triple2) -> rule5))] The cow visits the mouse.[(((triple2) -> rule1))] The mouse is blue.[(((triple2) -> rule4))] @2: The cow likes the mouse.[(((((triple2) -> rule1)) -> rule6))] @3: The mouse eats the cow.[(((((((triple2) -> rule1)) -> rule6)) -> rule2))]
The cow eats the mouse.
("cow" "eats" "mouse" "+")
triple1
The mouse visits the cow.
("mouse" "visits" "cow" "+")
triple2
The cow is cold.
("cow" "is" "cold" "+")
((triple2) -> (rule5 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow visits the mouse.
("cow" "visits" "mouse" "+")
((triple2) -> (rule1 % int1))
The cow visits the mouse.
("cow" "visits" "mouse" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
((triple2) -> (rule4 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The cow likes the mouse.
("cow" "likes" "mouse" "+")
((((triple2) -> (rule1 % int2))) -> (rule6 % int1))
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int1
The cow visits the mouse.
("cow" "visits" "mouse" "+")
int2
The mouse eats the cow.
("mouse" "eats" "cow" "+")
((((((triple2) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The mouse eats the cow.
("mouse" "eats" "cow" "+")
int1
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int2
The cow visits the mouse.
("cow" "visits" "mouse" "+")
int3