The cat eats the mouse. The cat is blue. The cat is kind. The cat is red. The cat needs the mouse. The cat sees the mouse. The mouse eats the cat. If something sees the cat and the cat eats the mouse then the mouse needs the cat. If something is red then it sees the cat. If the mouse is red and the mouse is green then the mouse needs the cat.
The cat eats the mouse.
("cat" "eats" "mouse" "+")
The cat is blue.
("cat" "is" "blue" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat is red.
("cat" "is" "red" "+")
The cat needs the mouse.
("cat" "needs" "mouse" "+")
The cat sees the mouse.
("cat" "sees" "mouse" "+")
The mouse eats the cat.
("mouse" "eats" "cat" "+")
If something sees the cat and the cat eats the mouse then the mouse needs the cat.
((("something" "sees" "cat" "+") ("cat" "eats" "mouse" "+")) -> ("mouse" "needs" "cat" "+"))
If something is red then it sees the cat.
((("something" "is" "red" "+")) -> ("something" "sees" "cat" "+"))
If the mouse is red and the mouse is green then the mouse needs the cat.
((("mouse" "is" "red" "+") ("mouse" "is" "green" "+")) -> ("mouse" "needs" "cat" "+"))
The cat is kind.
True
1
proof
[(triple3)]
("cat" "is" "kind" "+")
triple3
The cat is not kind.
False
1
inv-proof
[(triple3)]
("cat" "is" "kind" "-")
triple3
The cat sees the cat.
True
2
proof
[(((triple4) -> rule2))]
("cat" "sees" "cat" "+")
((triple4) -> (rule2 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat does not see the cat.
False
2
inv-proof
[(((triple4) -> rule2))]
("cat" "sees" "cat" "-")
((triple4) -> (rule2 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The mouse needs the cat.
True
4
proof
[(((((triple4) -> rule2) triple1) -> rule1))]
("mouse" "needs" "cat" "+")
((((triple4) -> (rule2 % int2)) triple1) -> (rule1 % int1))
The mouse needs the cat.
("mouse" "needs" "cat" "+")
int1
The cat sees the cat.
("cat" "sees" "cat" "+")
int2
The mouse does not need the cat.
False
4
inv-proof
[(((((triple4) -> rule2) triple1) -> rule1))]
("mouse" "needs" "cat" "-")
((((triple4) -> (rule2 % int2)) triple1) -> (rule1 % int1))
The mouse needs the cat.
("mouse" "needs" "cat" "+")
int1
The cat sees the cat.
("cat" "sees" "cat" "+")
int2
The mouse does not see the cat.
Unknown
inv-rconc
[@1: The mouse sees the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "sees" "cat" "-")
The mouse sees the mouse.
Unknown
random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "+")
The mouse is not round.
Unknown
inv-random
[@0: The mouse is round.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "round" "-")
The mouse is kind.
Unknown
random
[@0: The mouse is kind.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "kind" "+")
The cat does not eat the cat.
Unknown
inv-random
[@0: The cat eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cat" "-")
The mouse is green.
Unknown
random
[@0: The mouse is green.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "green" "+")
@0: The cat eats the mouse.[(triple1)] The cat is blue.[(triple2)] The cat is kind.[(triple3)] The cat is red.[(triple4)] The cat needs the mouse.[(triple5)] The cat sees the mouse.[(triple6)] The mouse eats the cat.[(triple7)] @1: The cat sees the cat.[(((triple4) -> rule2))] @2: The mouse needs the cat.[(((((triple4) -> rule2) triple1) -> rule1))]
The cat eats the mouse.
("cat" "eats" "mouse" "+")
triple1
The cat is blue.
("cat" "is" "blue" "+")
triple2
The cat is kind.
("cat" "is" "kind" "+")
triple3
The cat is red.
("cat" "is" "red" "+")
triple4
The cat needs the mouse.
("cat" "needs" "mouse" "+")
triple5
The cat sees the mouse.
("cat" "sees" "mouse" "+")
triple6
The mouse eats the cat.
("mouse" "eats" "cat" "+")
triple7
The cat sees the cat.
("cat" "sees" "cat" "+")
((triple4) -> (rule2 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The mouse needs the cat.
("mouse" "needs" "cat" "+")
((((triple4) -> (rule2 % int2)) triple1) -> (rule1 % int1))
The mouse needs the cat.
("mouse" "needs" "cat" "+")
int1
The cat sees the cat.
("cat" "sees" "cat" "+")
int2