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