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