The cat chases the cow. The cat sees the cow. The cow is cold. The cow is round. The cow needs the mouse. The cow sees the cat. The cow sees the mouse. The mouse chases the cat. The mouse chases the cow. The mouse is cold. The mouse is round. The mouse needs the cat. The mouse needs the cow. The mouse sees the cat. The mouse sees the cow. If someone needs the mouse and the mouse sees the cow then the cow sees the mouse. If someone sees the mouse then they chase the cat.
The cat chases the cow.
("cat" "chases" "cow" "+")
The cat sees the cow.
("cat" "sees" "cow" "+")
The cow is cold.
("cow" "is" "cold" "+")
The cow is round.
("cow" "is" "round" "+")
The cow needs the mouse.
("cow" "needs" "mouse" "+")
The cow sees the cat.
("cow" "sees" "cat" "+")
The cow sees the mouse.
("cow" "sees" "mouse" "+")
The mouse chases the cat.
("mouse" "chases" "cat" "+")
The mouse chases the cow.
("mouse" "chases" "cow" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is round.
("mouse" "is" "round" "+")
The mouse needs the cat.
("mouse" "needs" "cat" "+")
The mouse needs the cow.
("mouse" "needs" "cow" "+")
The mouse sees the cat.
("mouse" "sees" "cat" "+")
The mouse sees the cow.
("mouse" "sees" "cow" "+")
If someone needs the mouse and the mouse sees the cow then the cow sees the mouse.
((("someone" "needs" "mouse" "+") ("mouse" "sees" "cow" "+")) -> ("cow" "sees" "mouse" "+"))
If someone sees the mouse then they chase the cat.
((("someone" "sees" "mouse" "+")) -> ("someone" "chases" "cat" "+"))
The cow sees the mouse.
True
1
proof
[(triple7 OR ((triple5 triple15) -> rule1))]
("cow" "sees" "mouse" "+")
triple7
((triple5 triple15) -> (rule1 % int1))
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int1
The mouse does not need the cat.
False
1
inv-proof
[(triple12)]
("mouse" "needs" "cat" "-")
triple12
The cat does not chase the cat.
Unknown
inv-rconc
[@1: The cat chases the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "chases" "cat" "-")
The cat is red.
Unknown
random
[@0: The cat is red.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "red" "+")
@0: The cat chases the cow.[(triple1)] The cat sees the cow.[(triple2)] The cow is cold.[(triple3)] The cow is round.[(triple4)] The cow needs the mouse.[(triple5)] The cow sees the cat.[(triple6)] The cow sees the mouse.[(triple7 OR ((triple5 triple15) -> rule1))] The mouse chases the cat.[(triple8)] The mouse chases the cow.[(triple9)] The mouse is cold.[(triple10)] The mouse is round.[(triple11)] The mouse needs the cat.[(triple12)] The mouse needs the cow.[(triple13)] The mouse sees the cat.[(triple14)] The mouse sees the cow.[(triple15)] @1: The cow chases the cat.[(((triple7) -> rule2) OR ((((triple5 triple15) -> rule1)) -> rule2))]
The cat chases the cow.
("cat" "chases" "cow" "+")
triple1
The cat sees the cow.
("cat" "sees" "cow" "+")
triple2
The cow is cold.
("cow" "is" "cold" "+")
triple3
The cow is round.
("cow" "is" "round" "+")
triple4
The cow needs the mouse.
("cow" "needs" "mouse" "+")
triple5
The cow sees the cat.
("cow" "sees" "cat" "+")
triple6
The cow sees the mouse.
("cow" "sees" "mouse" "+")
triple7
((triple5 triple15) -> (rule1 % int1))
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int1
The mouse chases the cat.
("mouse" "chases" "cat" "+")
triple8
The mouse chases the cow.
("mouse" "chases" "cow" "+")
triple9
The mouse is cold.
("mouse" "is" "cold" "+")
triple10
The mouse is round.
("mouse" "is" "round" "+")
triple11
The mouse needs the cat.
("mouse" "needs" "cat" "+")
triple12
The mouse needs the cow.
("mouse" "needs" "cow" "+")
triple13
The mouse sees the cat.
("mouse" "sees" "cat" "+")
triple14
The mouse sees the cow.
("mouse" "sees" "cow" "+")
triple15
The cow chases the cat.
("cow" "chases" "cat" "+")
((triple7) -> (rule2 % int1))
The cow chases the cat.
("cow" "chases" "cat" "+")
int1
((((triple5 triple15) -> (rule1 % int2))) -> (rule2 % int1))
The cow chases the cat.
("cow" "chases" "cat" "+")
int1
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int2