The cat does not chase the mouse. The cat is nice. The cat needs the cow. The cat sees the cow. The cat sees the mouse. The cow is blue. The cow is nice. The cow needs the cat. The cow needs the mouse. The mouse chases the cat. The mouse chases the cow. The mouse is big. The mouse is blue. The mouse is red. The mouse needs the cow. The mouse sees the cat. If the cat is not nice then the cat sees the cow. If something is kind then it is blue. If something is kind then it does not see the cow. If the mouse sees the cow then the mouse is kind. If the cat is kind then the cat does not see the mouse. If something is red and it chases the mouse then it chases the cow. If something needs the cow then it does not chase the mouse. If something chases the cow and it does not see the cow then it chases the mouse.
The cat does not chase the mouse.
("cat" "chases" "mouse" "-")
The cat is nice.
("cat" "is" "nice" "+")
The cat needs the cow.
("cat" "needs" "cow" "+")
The cat sees the cow.
("cat" "sees" "cow" "+")
The cat sees the mouse.
("cat" "sees" "mouse" "+")
The cow is blue.
("cow" "is" "blue" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow needs the cat.
("cow" "needs" "cat" "+")
The cow needs the mouse.
("cow" "needs" "mouse" "+")
The mouse chases the cat.
("mouse" "chases" "cat" "+")
The mouse chases the cow.
("mouse" "chases" "cow" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse needs the cow.
("mouse" "needs" "cow" "+")
The mouse sees the cat.
("mouse" "sees" "cat" "+")
If the cat is not nice then the cat sees the cow.
((("cat" "is" "nice" "~")) -> ("cat" "sees" "cow" "+"))
If something is kind then it is blue.
((("something" "is" "kind" "+")) -> ("something" "is" "blue" "+"))
If something is kind then it does not see the cow.
((("something" "is" "kind" "+")) -> ("something" "sees" "cow" "-"))
If the mouse sees the cow then the mouse is kind.
((("mouse" "sees" "cow" "+")) -> ("mouse" "is" "kind" "+"))
If the cat is kind then the cat does not see the mouse.
((("cat" "is" "kind" "+")) -> ("cat" "sees" "mouse" "-"))
If something is red and it chases the mouse then it chases the cow.
((("something" "is" "red" "+") ("something" "chases" "mouse" "+")) -> ("something" "chases" "cow" "+"))
If something needs the cow then it does not chase the mouse.
((("something" "needs" "cow" "+")) -> ("something" "chases" "mouse" "-"))
If something chases the cow and it does not see the cow then it chases the mouse.
((("something" "chases" "cow" "+") ("something" "sees" "cow" "~")) -> ("something" "chases" "mouse" "+"))
The mouse is big.
True
1
proof
[(triple12)]
("mouse" "is" "big" "+")
triple12
The cat does not see the mouse.
False
1
inv-proof
[(triple5)]
("cat" "sees" "mouse" "-")
triple5
The mouse does not chase the mouse.
True
2
proof
[(((triple15) -> rule7))]
("mouse" "chases" "mouse" "-")
((triple15) -> (rule7 % int1))
The mouse does not chase the mouse.
("mouse" "chases" "mouse" "-")
int1
The mouse chases the mouse.
False
2
inv-proof
[(((triple15) -> rule7))]
("mouse" "chases" "mouse" "+")
((triple15) -> (rule7 % int1))
The mouse does not chase the mouse.
("mouse" "chases" "mouse" "-")
int1
The cow does not chase the mouse.
Unknown
inv-rconc
[@1: The cow chases the mouse.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("cow" "chases" "mouse" "-")
The cat chases the cow.
Unknown
rconc
[@1: The cat chases the cow.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cat" "chases" "cow" "+")
The cat does not chase the cat.
Unknown
inv-random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cat" "-")
The mouse needs the cat.
Unknown
random
[@0: The mouse needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "cat" "+")
@0: The cat does not chase the mouse.[(triple1 OR ((triple3) -> rule7))] The cat is nice.[(triple2)] The cat needs the cow.[(triple3)] The cat sees the cow.[(triple4)] The cat sees the mouse.[(triple5)] The cow is blue.[(triple6)] The cow is nice.[(triple7)] The cow needs the cat.[(triple8)] The cow needs the mouse.[(triple9)] The mouse chases the cat.[(triple10)] The mouse chases the cow.[(triple11)] The mouse is big.[(triple12)] The mouse is blue.[(triple13)] The mouse is red.[(triple14)] The mouse needs the cow.[(triple15)] The mouse sees the cat.[(triple16)] @1: The mouse does not chase the mouse.[(((triple15) -> rule7))]
The cat does not chase the mouse.
("cat" "chases" "mouse" "-")
triple1
((triple3) -> (rule7 % int1))
The cat does not chase the mouse.
("cat" "chases" "mouse" "-")
int1
The cat is nice.
("cat" "is" "nice" "+")
triple2
The cat needs the cow.
("cat" "needs" "cow" "+")
triple3
The cat sees the cow.
("cat" "sees" "cow" "+")
triple4
The cat sees the mouse.
("cat" "sees" "mouse" "+")
triple5
The cow is blue.
("cow" "is" "blue" "+")
triple6
The cow is nice.
("cow" "is" "nice" "+")
triple7
The cow needs the cat.
("cow" "needs" "cat" "+")
triple8
The cow needs the mouse.
("cow" "needs" "mouse" "+")
triple9
The mouse chases the cat.
("mouse" "chases" "cat" "+")
triple10
The mouse chases the cow.
("mouse" "chases" "cow" "+")
triple11
The mouse is big.
("mouse" "is" "big" "+")
triple12
The mouse is blue.
("mouse" "is" "blue" "+")
triple13
The mouse is red.
("mouse" "is" "red" "+")
triple14
The mouse needs the cow.
("mouse" "needs" "cow" "+")
triple15
The mouse sees the cat.
("mouse" "sees" "cat" "+")
triple16
The mouse does not chase the mouse.
("mouse" "chases" "mouse" "-")
((triple15) -> (rule7 % int1))
The mouse does not chase the mouse.
("mouse" "chases" "mouse" "-")
int1