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