The cow eats the mouse. The cow is nice. The cow is round. The cow likes the mouse. The cow needs the mouse. The mouse eats the cow. The mouse is cold. The mouse is not green. The mouse is rough. The mouse is not round. The mouse does not like the cow. The mouse needs the cow. If something is cold and it needs the mouse then it is round. If something is rough and it needs the mouse then it needs the cow. If something eats the cow and the cow does not eat the mouse then the mouse is nice. If something likes the cow and the cow eats the mouse then it eats the cow. If something likes the cow and it eats the mouse then the mouse does not like the cow. If the cow is nice and the cow does not eat the mouse then the cow needs the mouse. If the mouse eats the cow then the mouse needs the cow. If something needs the mouse then it likes the cow.
The cow eats the mouse.
("cow" "eats" "mouse" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow is round.
("cow" "is" "round" "+")
The cow likes the mouse.
("cow" "likes" "mouse" "+")
The cow needs the mouse.
("cow" "needs" "mouse" "+")
The mouse eats the cow.
("mouse" "eats" "cow" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is not green.
("mouse" "is" "green" "-")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse is not round.
("mouse" "is" "round" "-")
The mouse does not like the cow.
("mouse" "likes" "cow" "-")
The mouse needs the cow.
("mouse" "needs" "cow" "+")
If something is cold and it needs the mouse then it is round.
((("something" "is" "cold" "+") ("something" "needs" "mouse" "+")) -> ("something" "is" "round" "+"))
If something is rough and it needs the mouse then it needs the cow.
((("something" "is" "rough" "+") ("something" "needs" "mouse" "+")) -> ("something" "needs" "cow" "+"))
If something eats the cow and the cow does not eat the mouse then the mouse is nice.
((("something" "eats" "cow" "+") ("cow" "eats" "mouse" "~")) -> ("mouse" "is" "nice" "+"))
If something likes the cow and the cow eats the mouse then it eats the cow.
((("something" "likes" "cow" "+") ("cow" "eats" "mouse" "+")) -> ("something" "eats" "cow" "+"))
If something likes the cow and it eats the mouse then the mouse does not like the cow.
((("something" "likes" "cow" "+") ("something" "eats" "mouse" "+")) -> ("mouse" "likes" "cow" "-"))
If the cow is nice and the cow does not eat the mouse then the cow needs the mouse.
((("cow" "is" "nice" "+") ("cow" "eats" "mouse" "~")) -> ("cow" "needs" "mouse" "+"))
If the mouse eats the cow then the mouse needs the cow.
((("mouse" "eats" "cow" "+")) -> ("mouse" "needs" "cow" "+"))
If something needs the mouse then it likes the cow.
((("something" "needs" "mouse" "+")) -> ("something" "likes" "cow" "+"))
The mouse is rough.
True
1
proof
[(triple9)]
("mouse" "is" "rough" "+")
triple9
The cow does not need the mouse.
False
1
inv-proof
[(triple5)]
("cow" "needs" "mouse" "-")
triple5
The cow does not need the cow.
Unknown
inv-rconc
[@1: The cow needs the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "needs" "cow" "-")
The mouse needs the mouse.
Unknown
random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "+")
@0: The cow eats the mouse.[(triple1)] The cow is nice.[(triple2)] The cow is round.[(triple3)] The cow likes the mouse.[(triple4)] The cow needs the mouse.[(triple5)] The mouse does not like the cow.[(triple11 OR ((((triple5) -> rule8) triple1) -> rule5))] The mouse eats the cow.[(triple6)] The mouse is cold.[(triple7)] The mouse is not green.[(triple8)] The mouse is not round.[(triple10)] The mouse is rough.[(triple9)] The mouse needs the cow.[(triple12 OR ((triple6) -> rule7))] @1: The cow likes the cow.[(((triple5) -> rule8))] @2: The cow eats the cow.[(((((triple5) -> rule8) triple1) -> rule4))]
The cow eats the mouse.
("cow" "eats" "mouse" "+")
triple1
The cow is nice.
("cow" "is" "nice" "+")
triple2
The cow is round.
("cow" "is" "round" "+")
triple3
The cow likes the mouse.
("cow" "likes" "mouse" "+")
triple4
The cow needs the mouse.
("cow" "needs" "mouse" "+")
triple5
The mouse does not like the cow.
("mouse" "likes" "cow" "-")
triple11
((((triple5) -> (rule8 % int2)) triple1) -> (rule5 % int1))
The mouse does not like the cow.
("mouse" "likes" "cow" "-")
int1
The cow likes the cow.
("cow" "likes" "cow" "+")
int2
The mouse eats the cow.
("mouse" "eats" "cow" "+")
triple6
The mouse is cold.
("mouse" "is" "cold" "+")
triple7
The mouse is not green.
("mouse" "is" "green" "-")
triple8
The mouse is not round.
("mouse" "is" "round" "-")
triple10
The mouse is rough.
("mouse" "is" "rough" "+")
triple9
The mouse needs the cow.
("mouse" "needs" "cow" "+")
triple12
((triple6) -> (rule7 % int1))
The mouse needs the cow.
("mouse" "needs" "cow" "+")
int1
The cow likes the cow.
("cow" "likes" "cow" "+")
((triple5) -> (rule8 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The cow eats the cow.
("cow" "eats" "cow" "+")
((((triple5) -> (rule8 % int2)) triple1) -> (rule4 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The cow likes the cow.
("cow" "likes" "cow" "+")
int2