The cow likes the mouse. The mouse eats the cow. The mouse likes the cow. If someone is blue then they like the mouse. If someone eats the mouse and the mouse chases the cow then the cow chases the mouse. If someone likes the mouse then the mouse is blue. If someone is cold and they eat the mouse then they like the cow. If the mouse likes the cow and the cow eats the mouse then the cow likes the mouse. If someone chases the cow then the cow eats the mouse. If the mouse is nice and the mouse chases the cow then the mouse is big. If someone eats the cow then they like the cow.
The cow likes the mouse.
("cow" "likes" "mouse" "+")
The mouse eats the cow.
("mouse" "eats" "cow" "+")
The mouse likes the cow.
("mouse" "likes" "cow" "+")
If someone is blue then they like the mouse.
((("someone" "is" "blue" "+")) -> ("someone" "likes" "mouse" "+"))
If someone eats the mouse and the mouse chases the cow then the cow chases the mouse.
((("someone" "eats" "mouse" "+") ("mouse" "chases" "cow" "+")) -> ("cow" "chases" "mouse" "+"))
If someone likes the mouse then the mouse is blue.
((("someone" "likes" "mouse" "+")) -> ("mouse" "is" "blue" "+"))
If someone is cold and they eat the mouse then they like the cow.
((("someone" "is" "cold" "+") ("someone" "eats" "mouse" "+")) -> ("someone" "likes" "cow" "+"))
If the mouse likes the cow and the cow eats the mouse then the cow likes the mouse.
((("mouse" "likes" "cow" "+") ("cow" "eats" "mouse" "+")) -> ("cow" "likes" "mouse" "+"))
If someone chases the cow then the cow eats the mouse.
((("someone" "chases" "cow" "+")) -> ("cow" "eats" "mouse" "+"))
If the mouse is nice and the mouse chases the cow then the mouse is big.
((("mouse" "is" "nice" "+") ("mouse" "chases" "cow" "+")) -> ("mouse" "is" "big" "+"))
If someone eats the cow then they like the cow.
((("someone" "eats" "cow" "+")) -> ("someone" "likes" "cow" "+"))
The cow likes the mouse.
True
1
proof
[(triple1)]
("cow" "likes" "mouse" "+")
triple1
The cow does not like the mouse.
False
1
inv-proof
[(triple1)]
("cow" "likes" "mouse" "-")
triple1
The mouse is blue.
True
2
proof
[(((triple1) -> rule3))]
("mouse" "is" "blue" "+")
((triple1) -> (rule3 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse is not blue.
False
2
inv-proof
[(((triple1) -> rule3))]
("mouse" "is" "blue" "-")
((triple1) -> (rule3 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse likes the mouse.
True
3
proof
[(((((triple1) -> rule3)) -> rule1))]
("mouse" "likes" "mouse" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The mouse does not like the mouse.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule1))]
("mouse" "likes" "mouse" "-")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The cow does not chase the mouse.
Unknown
inv-rconc
[@1: The cow chases the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "chases" "mouse" "-")
The mouse is big.
Unknown
rconc
[@1: The mouse is big.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("mouse" "is" "big" "+")
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 cow eats the cow.
Unknown
random
[@0: The cow eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "cow" "+")
The cow is not big.
Unknown
inv-random
[@0: The cow is big.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "big" "-")
The mouse is nice.
Unknown
random
[@0: The mouse is nice.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "nice" "+")
@0: The cow likes the mouse.[(triple1)] The mouse eats the cow.[(triple2)] The mouse likes the cow.[(triple3 OR ((triple2) -> rule8))] @1: The mouse is blue.[(((triple1) -> rule3))] @2: The mouse likes the mouse.[(((((triple1) -> rule3)) -> rule1))]
The cow likes the mouse.
("cow" "likes" "mouse" "+")
triple1
The mouse eats the cow.
("mouse" "eats" "cow" "+")
triple2
The mouse likes the cow.
("mouse" "likes" "cow" "+")
triple3
((triple2) -> (rule8 % int1))
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
((triple1) -> (rule3 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2