The cow is blue. The cow sees the mouse. The cow visits the mouse. The mouse is young. The mouse needs the cow. The mouse sees the cow. The mouse visits the cow. If something sees the mouse then the mouse visits the cow. If something is blue and it needs the mouse then it is cold. If something needs the cow and it visits the mouse then it visits the cow. If something needs the mouse and it sees the mouse then the mouse visits the cow. If something is rough and round then it needs the mouse. If something is young and round then it is rough. If something visits the cow then the cow visits the mouse. If something visits the cow then the cow is cold.
The cow is blue.
("cow" "is" "blue" "+")
The cow sees the mouse.
("cow" "sees" "mouse" "+")
The cow visits the mouse.
("cow" "visits" "mouse" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse needs the cow.
("mouse" "needs" "cow" "+")
The mouse sees the cow.
("mouse" "sees" "cow" "+")
The mouse visits the cow.
("mouse" "visits" "cow" "+")
If something sees the mouse then the mouse visits the cow.
((("something" "sees" "mouse" "+")) -> ("mouse" "visits" "cow" "+"))
If something is blue and it needs the mouse then it is cold.
((("something" "is" "blue" "+") ("something" "needs" "mouse" "+")) -> ("something" "is" "cold" "+"))
If something needs the cow and it visits the mouse then it visits the cow.
((("something" "needs" "cow" "+") ("something" "visits" "mouse" "+")) -> ("something" "visits" "cow" "+"))
If something needs the mouse and it sees the mouse then the mouse visits the cow.
((("something" "needs" "mouse" "+") ("something" "sees" "mouse" "+")) -> ("mouse" "visits" "cow" "+"))
If something is rough and round then it needs the mouse.
((("something" "is" "rough" "+") ("something" "is" "round" "+")) -> ("something" "needs" "mouse" "+"))
If something is young and round then it is rough.
((("something" "is" "young" "+") ("something" "is" "round" "+")) -> ("something" "is" "rough" "+"))
If something visits the cow then the cow visits the mouse.
((("something" "visits" "cow" "+")) -> ("cow" "visits" "mouse" "+"))
If something visits the cow then the cow is cold.
((("something" "visits" "cow" "+")) -> ("cow" "is" "cold" "+"))
The mouse sees the cow.
True
1
proof
[(triple6)]
("mouse" "sees" "cow" "+")
triple6
The cow does not see the mouse.
False
1
inv-proof
[(triple2)]
("cow" "sees" "mouse" "-")
triple2
The mouse is not rough.
Unknown
inv-rconc
[@1: The mouse is rough.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("mouse" "is" "rough" "-")
The cow sees the cow.
Unknown
random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "+")
@0: The cow is blue.[(triple1)] The cow sees the mouse.[(triple2)] The cow visits the mouse.[(triple3 OR ((triple7) -> rule7) OR ((((triple2) -> rule1)) -> rule7))] The mouse is young.[(triple4)] The mouse needs the cow.[(triple5)] The mouse sees the cow.[(triple6)] The mouse visits the cow.[(triple7 OR ((triple2) -> rule1))] @1: The cow is cold.[(((triple7) -> rule8) OR ((((triple2) -> rule1)) -> rule8))]
The cow is blue.
("cow" "is" "blue" "+")
triple1
The cow sees the mouse.
("cow" "sees" "mouse" "+")
triple2
The cow visits the mouse.
("cow" "visits" "mouse" "+")
triple3
((triple7) -> (rule7 % int1))
The cow visits the mouse.
("cow" "visits" "mouse" "+")
int1
((((triple2) -> (rule1 % int2))) -> (rule7 % int1))
The cow visits the mouse.
("cow" "visits" "mouse" "+")
int1
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int2
The mouse is young.
("mouse" "is" "young" "+")
triple4
The mouse needs the cow.
("mouse" "needs" "cow" "+")
triple5
The mouse sees the cow.
("mouse" "sees" "cow" "+")
triple6
The mouse visits the cow.
("mouse" "visits" "cow" "+")
triple7
((triple2) -> (rule1 % int1))
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
((triple7) -> (rule8 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
((((triple2) -> (rule1 % int2))) -> (rule8 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int2