The cat does not need the squirrel. The mouse sees the squirrel. The squirrel sees the cat. If something is nice and it eats the mouse then it is rough. If something sees the cat then the cat eats the squirrel. If the mouse does not eat the squirrel then the mouse is round. If something needs the mouse then it eats the cat. If something is big then it needs the mouse. If something eats the squirrel then it needs the mouse. If something eats the mouse then it is green. If something eats the squirrel and it is not green then it is round.
The cat does not need the squirrel.
("cat" "needs" "squirrel" "-")
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
If something is nice and it eats the mouse then it is rough.
((("something" "is" "nice" "+") ("something" "eats" "mouse" "+")) -> ("something" "is" "rough" "+"))
If something sees the cat then the cat eats the squirrel.
((("something" "sees" "cat" "+")) -> ("cat" "eats" "squirrel" "+"))
If the mouse does not eat the squirrel then the mouse is round.
((("mouse" "eats" "squirrel" "~")) -> ("mouse" "is" "round" "+"))
If something needs the mouse then it eats the cat.
((("something" "needs" "mouse" "+")) -> ("something" "eats" "cat" "+"))
If something is big then it needs the mouse.
((("something" "is" "big" "+")) -> ("something" "needs" "mouse" "+"))
If something eats the squirrel then it needs the mouse.
((("something" "eats" "squirrel" "+")) -> ("something" "needs" "mouse" "+"))
If something eats the mouse then it is green.
((("something" "eats" "mouse" "+")) -> ("something" "is" "green" "+"))
If something eats the squirrel and it is not green then it is round.
((("something" "eats" "squirrel" "+") ("something" "is" "green" "~")) -> ("something" "is" "round" "+"))
The mouse sees the squirrel.
True
1
proof
[(triple2)]
("mouse" "sees" "squirrel" "+")
triple2
The mouse does not see the squirrel.
False
1
inv-proof
[(triple2)]
("mouse" "sees" "squirrel" "-")
triple2
The cat eats the squirrel.
True
2
proof
[(((triple3) -> rule2))]
("cat" "eats" "squirrel" "+")
((triple3) -> (rule2 % int1))
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
int1
The cat does not eat the squirrel.
False
2
inv-proof
[(((triple3) -> rule2))]
("cat" "eats" "squirrel" "-")
((triple3) -> (rule2 % int1))
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
int1
The cat needs the mouse.
True
3
proof
[(((((triple3) -> rule2)) -> rule6))]
("cat" "needs" "mouse" "+")
((((triple3) -> (rule2 % int2))) -> (rule6 % int1))
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int1
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
int2
The cat does not need the mouse.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule6))]
("cat" "needs" "mouse" "-")
((((triple3) -> (rule2 % int2))) -> (rule6 % int1))
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int1
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
int2
The cat eats the cat.
True
4
proof
[(((((((triple3) -> rule2)) -> rule6)) -> rule4))]
("cat" "eats" "cat" "+")
((((((triple3) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int2
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
int3
The cat does not eat the cat.
False
4
inv-proof
[(((((((triple3) -> rule2)) -> rule6)) -> rule4))]
("cat" "eats" "cat" "-")
((((((triple3) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int2
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
int3
The cat is not green.
Unknown
inv-rconc
[@1: The cat is green.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("cat" "is" "green" "-")
The cat is rough.
Unknown
rconc
[@1: The cat is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "is" "rough" "+")
The cat is not round.
Unknown
inv-rconc
[@1: The cat is round.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("cat" "is" "round" "-")
The squirrel needs the mouse.
Unknown
rconc
[@1: The squirrel needs the mouse.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("squirrel" "needs" "mouse" "+")
The squirrel does not eat the squirrel.
Unknown
inv-random
[@0: The squirrel eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "squirrel" "-")
The mouse eats the squirrel.
Unknown
random
[@0: The mouse eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "squirrel" "+")
The mouse does not see the cat.
Unknown
inv-random
[@0: The mouse sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "cat" "-")
The mouse is big.
Unknown
random
[@0: The mouse is big.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "big" "+")
@0: The cat does not need the squirrel.[(triple1)] The mouse sees the squirrel.[(triple2)] The squirrel sees the cat.[(triple3)] @1: The cat eats the squirrel.[(((triple3) -> rule2))] @2: The cat needs the mouse.[(((((triple3) -> rule2)) -> rule6))] @3: The cat eats the cat.[(((((((triple3) -> rule2)) -> rule6)) -> rule4))]
The cat does not need the squirrel.
("cat" "needs" "squirrel" "-")
triple1
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
triple2
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
triple3
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
((triple3) -> (rule2 % int1))
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
int1
The cat needs the mouse.
("cat" "needs" "mouse" "+")
((((triple3) -> (rule2 % int2))) -> (rule6 % int1))
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int1
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
int2
The cat eats the cat.
("cat" "eats" "cat" "+")
((((((triple3) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int2
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
int3