The cow chases the mouse. The mouse is blue. The squirrel does not see the mouse. If something is nice and it does not eat the mouse then the mouse sees the cow. If something sees the cow and the cow is red then it eats the squirrel. If something sees the cow then the cow sees the mouse. If something is nice then it sees the cow. If something is round then it chases the squirrel. All blue things are nice.
The cow chases the mouse.
("cow" "chases" "mouse" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The squirrel does not see the mouse.
("squirrel" "sees" "mouse" "-")
If something is nice and it does not eat the mouse then the mouse sees the cow.
((("something" "is" "nice" "+") ("something" "eats" "mouse" "~")) -> ("mouse" "sees" "cow" "+"))
If something sees the cow and the cow is red then it eats the squirrel.
((("something" "sees" "cow" "+") ("cow" "is" "red" "+")) -> ("something" "eats" "squirrel" "+"))
If something sees the cow then the cow sees the mouse.
((("something" "sees" "cow" "+")) -> ("cow" "sees" "mouse" "+"))
If something is nice then it sees the cow.
((("something" "is" "nice" "+")) -> ("something" "sees" "cow" "+"))
If something is round then it chases the squirrel.
((("something" "is" "round" "+")) -> ("something" "chases" "squirrel" "+"))
All blue things are nice.
((("something" "is" "blue" "+")) -> ("something" "is" "nice" "+"))
The cow chases the mouse.
True
1
proof
[(triple1)]
("cow" "chases" "mouse" "+")
triple1
The squirrel sees the mouse.
False
1
inv-proof
[(triple3)]
("squirrel" "sees" "mouse" "+")
triple3
The mouse is nice.
True
2
proof
[(((triple2) -> rule6))]
("mouse" "is" "nice" "+")
((triple2) -> (rule6 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse is not nice.
False
2
inv-proof
[(((triple2) -> rule6))]
("mouse" "is" "nice" "-")
((triple2) -> (rule6 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse sees the cow.
True
3
proof
[(((((triple2) -> rule6)) -> rule4))]
("mouse" "sees" "cow" "+")
((((triple2) -> (rule6 % int2))) -> (rule4 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The mouse does not see the cow.
False
3
inv-proof
[(((((triple2) -> rule6)) -> rule4))]
("mouse" "sees" "cow" "-")
((((triple2) -> (rule6 % int2))) -> (rule4 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The cow sees the mouse.
True
4
proof
[(((((((triple2) -> rule6)) -> rule4)) -> rule3))]
("cow" "sees" "mouse" "+")
((((((triple2) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int1
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int2
The mouse is nice.
("mouse" "is" "nice" "+")
int3
The cow does not see the mouse.
False
4
inv-proof
[(((((((triple2) -> rule6)) -> rule4)) -> rule3))]
("cow" "sees" "mouse" "-")
((((((triple2) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int1
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int2
The mouse is nice.
("mouse" "is" "nice" "+")
int3
The mouse does not eat the squirrel.
Unknown
inv-rconc
[@1: The mouse eats the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "eats" "squirrel" "-")
The cow chases the squirrel.
Unknown
rconc
[@1: The cow chases the squirrel.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cow" "chases" "squirrel" "+")
The cow does not see the cow.
Unknown
inv-rconc
[@2: The cow sees the cow.[CWA. Example of deepest failure = (rule4 <- rule6 <- FAIL)]]
("cow" "sees" "cow" "-")
The cow eats the squirrel.
Unknown
rconc
[@1: The cow eats the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "eats" "squirrel" "+")
The mouse does not chase the cow.
Unknown
inv-random
[@0: The mouse chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "cow" "-")
The cow chases the cow.
Unknown
random
[@0: The cow chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cow" "+")
The cow is not round.
Unknown
inv-random
[@0: The cow is round.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "round" "-")
The mouse eats the cow.
Unknown
random
[@0: The mouse eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "cow" "+")
@0: The cow chases the mouse.[(triple1)] The mouse is blue.[(triple2)] The squirrel does not see the mouse.[(triple3)] @1: The mouse is nice.[(((triple2) -> rule6))] @2: The mouse sees the cow.[(((((triple2) -> rule6)) -> rule4))] @3: The cow sees the mouse.[(((((((triple2) -> rule6)) -> rule4)) -> rule3))]
The cow chases the mouse.
("cow" "chases" "mouse" "+")
triple1
The mouse is blue.
("mouse" "is" "blue" "+")
triple2
The squirrel does not see the mouse.
("squirrel" "sees" "mouse" "-")
triple3
The mouse is nice.
("mouse" "is" "nice" "+")
((triple2) -> (rule6 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse sees the cow.
("mouse" "sees" "cow" "+")
((((triple2) -> (rule6 % int2))) -> (rule4 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The cow sees the mouse.
("cow" "sees" "mouse" "+")
((((((triple2) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int1
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int2
The mouse is nice.
("mouse" "is" "nice" "+")
int3