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