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