The cat chases the mouse. The cat is green. The cat is kind. The cat is not red. The cat is round. The cat is young. The cat visits the mouse. The mouse chases the cat. The mouse is green. The mouse is kind. The mouse is red. The mouse is round. The mouse is young. The mouse needs the cat. The mouse does not visit the cat. If the cat visits the mouse then the cat is kind. If something is red then it chases the cat. If something is kind and it visits the cat then the cat chases the mouse. If something is young and not round then it is kind. If the cat needs the mouse and the mouse does not need the cat then the mouse does not chase the cat. If something needs the cat then the cat visits the mouse.
The cat chases the mouse.
("cat" "chases" "mouse" "+")
The cat is green.
("cat" "is" "green" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat is not red.
("cat" "is" "red" "-")
The cat is round.
("cat" "is" "round" "+")
The cat is young.
("cat" "is" "young" "+")
The cat visits the mouse.
("cat" "visits" "mouse" "+")
The mouse chases the cat.
("mouse" "chases" "cat" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse is round.
("mouse" "is" "round" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse needs the cat.
("mouse" "needs" "cat" "+")
The mouse does not visit the cat.
("mouse" "visits" "cat" "-")
If the cat visits the mouse then the cat is kind.
((("cat" "visits" "mouse" "+")) -> ("cat" "is" "kind" "+"))
If something is red then it chases the cat.
((("something" "is" "red" "+")) -> ("something" "chases" "cat" "+"))
If something is kind and it visits the cat then the cat chases the mouse.
((("something" "is" "kind" "+") ("something" "visits" "cat" "+")) -> ("cat" "chases" "mouse" "+"))
If something is young and not round then it is kind.
((("something" "is" "young" "+") ("something" "is" "round" "~")) -> ("something" "is" "kind" "+"))
If the cat needs the mouse and the mouse does not need the cat then the mouse does not chase the cat.
((("cat" "needs" "mouse" "+") ("mouse" "needs" "cat" "~")) -> ("mouse" "chases" "cat" "-"))
If something needs the cat then the cat visits the mouse.
((("something" "needs" "cat" "+")) -> ("cat" "visits" "mouse" "+"))
The cat is round.
True
1
proof
[(triple5)]
("cat" "is" "round" "+")
triple5
The mouse is not green.
False
1
inv-proof
[(triple9)]
("mouse" "is" "green" "-")
triple9
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 mouse needs the mouse.
Unknown
random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "+")
@0: The cat chases the mouse.[(triple1)] The cat is green.[(triple2)] The cat is kind.[(triple3 OR ((triple7) -> rule1) OR ((((triple14) -> rule6)) -> rule1))] The cat is not red.[(triple4)] The cat is round.[(triple5)] The cat is young.[(triple6)] The cat visits the mouse.[(triple7 OR ((triple14) -> rule6))] The mouse chases the cat.[(triple8 OR ((triple11) -> rule2))] The mouse does not visit the cat.[(triple15)] The mouse is green.[(triple9)] The mouse is kind.[(triple10)] The mouse is red.[(triple11)] The mouse is round.[(triple12)] The mouse is young.[(triple13)] The mouse needs the cat.[(triple14)]
The cat chases the mouse.
("cat" "chases" "mouse" "+")
triple1
The cat is green.
("cat" "is" "green" "+")
triple2
The cat is kind.
("cat" "is" "kind" "+")
triple3
((triple7) -> (rule1 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
((((triple14) -> (rule6 % int2))) -> (rule1 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int2
The cat is not red.
("cat" "is" "red" "-")
triple4
The cat is round.
("cat" "is" "round" "+")
triple5
The cat is young.
("cat" "is" "young" "+")
triple6
The cat visits the mouse.
("cat" "visits" "mouse" "+")
triple7
((triple14) -> (rule6 % int1))
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int1
The mouse chases the cat.
("mouse" "chases" "cat" "+")
triple8
((triple11) -> (rule2 % int1))
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int1
The mouse does not visit the cat.
("mouse" "visits" "cat" "-")
triple15
The mouse is green.
("mouse" "is" "green" "+")
triple9
The mouse is kind.
("mouse" "is" "kind" "+")
triple10
The mouse is red.
("mouse" "is" "red" "+")
triple11
The mouse is round.
("mouse" "is" "round" "+")
triple12
The mouse is young.
("mouse" "is" "young" "+")
triple13
The mouse needs the cat.
("mouse" "needs" "cat" "+")
triple14