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