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