The cow chases the mouse. The cow is cold. The cow is green. The cow is kind. The cow is nice. The cow is rough. The cow needs the mouse. The cow visits the mouse. The mouse is green. The mouse is rough. The mouse needs the cow. The mouse visits the cow. If something is rough and green then it chases the mouse. If something is nice then it visits the mouse. If the cow chases the mouse then the cow is green.
The cow chases the mouse.
("cow" "chases" "mouse" "+")
The cow is cold.
("cow" "is" "cold" "+")
The cow is green.
("cow" "is" "green" "+")
The cow is kind.
("cow" "is" "kind" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow is rough.
("cow" "is" "rough" "+")
The cow needs the mouse.
("cow" "needs" "mouse" "+")
The cow visits the mouse.
("cow" "visits" "mouse" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse needs the cow.
("mouse" "needs" "cow" "+")
The mouse visits the cow.
("mouse" "visits" "cow" "+")
If something is rough and green then it chases the mouse.
((("something" "is" "rough" "+") ("something" "is" "green" "+")) -> ("something" "chases" "mouse" "+"))
If something is nice then it visits the mouse.
((("something" "is" "nice" "+")) -> ("something" "visits" "mouse" "+"))
If the cow chases the mouse then the cow is green.
((("cow" "chases" "mouse" "+")) -> ("cow" "is" "green" "+"))
The cow chases the mouse.
True
1
proof
[(triple1 OR ((triple6 triple3) -> rule1))]
("cow" "chases" "mouse" "+")
triple1
((triple6 triple3) -> (rule1 % int1))
The cow chases the mouse.
("cow" "chases" "mouse" "+")
int1
The mouse is not green.
False
1
inv-proof
[(triple9)]
("mouse" "is" "green" "-")
triple9
The mouse chases the mouse.
True
3
proof
[(((triple10 triple9) -> rule1))]
("mouse" "chases" "mouse" "+")
((triple10 triple9) -> (rule1 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse does not chase the mouse.
False
3
inv-proof
[(((triple10 triple9) -> rule1))]
("mouse" "chases" "mouse" "-")
((triple10 triple9) -> (rule1 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse does not visit the mouse.
Unknown
inv-rconc
[@1: The mouse visits the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "visits" "mouse" "-")
The mouse is kind.
Unknown
random
[@0: The mouse is kind.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "kind" "+")
The cow does not need the cow.
Unknown
inv-random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (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 chases the mouse.[(triple1 OR ((triple6 triple3) -> rule1))] The cow is cold.[(triple2)] The cow is green.[(triple3 OR ((triple1) -> rule3))] The cow is kind.[(triple4)] The cow is nice.[(triple5)] The cow is rough.[(triple6)] The cow needs the mouse.[(triple7)] The cow visits the mouse.[(triple8 OR ((triple5) -> rule2))] The mouse is green.[(triple9)] The mouse is rough.[(triple10)] The mouse needs the cow.[(triple11)] The mouse visits the cow.[(triple12)] @1: The mouse chases the mouse.[(((triple10 triple9) -> rule1))]
The cow chases the mouse.
("cow" "chases" "mouse" "+")
triple1
((triple6 triple3) -> (rule1 % int1))
The cow chases the mouse.
("cow" "chases" "mouse" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
triple2
The cow is green.
("cow" "is" "green" "+")
triple3
((triple1) -> (rule3 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow is kind.
("cow" "is" "kind" "+")
triple4
The cow is nice.
("cow" "is" "nice" "+")
triple5
The cow is rough.
("cow" "is" "rough" "+")
triple6
The cow needs the mouse.
("cow" "needs" "mouse" "+")
triple7
The cow visits the mouse.
("cow" "visits" "mouse" "+")
triple8
((triple5) -> (rule2 % int1))
The cow visits the mouse.
("cow" "visits" "mouse" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
triple9
The mouse is rough.
("mouse" "is" "rough" "+")
triple10
The mouse needs the cow.
("mouse" "needs" "cow" "+")
triple11
The mouse visits the cow.
("mouse" "visits" "cow" "+")
triple12
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
((triple10 triple9) -> (rule1 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1