The lion is green. The lion sees the squirrel. The mouse is not red. The rabbit does not visit the mouse. The squirrel chases the lion. The squirrel chases the rabbit. The squirrel is kind. If something is nice then it does not see the squirrel. If something chases the mouse then the mouse is nice. If something sees the mouse then it chases the mouse. If something is kind then it sees the mouse. If something is nice then it sees the mouse. If something chases the mouse and it is red then the mouse sees the lion. If something visits the rabbit then it sees the rabbit. If the rabbit is blue and the rabbit chases the mouse then the mouse chases the squirrel. If something visits the lion and it sees the lion then the lion is green.
The lion is green.
("lion" "is" "green" "+")
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
The mouse is not red.
("mouse" "is" "red" "-")
The rabbit does not visit the mouse.
("rabbit" "visits" "mouse" "-")
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
If something is nice then it does not see the squirrel.
((("something" "is" "nice" "+")) -> ("something" "sees" "squirrel" "-"))
If something chases the mouse then the mouse is nice.
((("something" "chases" "mouse" "+")) -> ("mouse" "is" "nice" "+"))
If something sees the mouse then it chases the mouse.
((("something" "sees" "mouse" "+")) -> ("something" "chases" "mouse" "+"))
If something is kind then it sees the mouse.
((("something" "is" "kind" "+")) -> ("something" "sees" "mouse" "+"))
If something is nice then it sees the mouse.
((("something" "is" "nice" "+")) -> ("something" "sees" "mouse" "+"))
If something chases the mouse and it is red then the mouse sees the lion.
((("something" "chases" "mouse" "+") ("something" "is" "red" "+")) -> ("mouse" "sees" "lion" "+"))
If something visits the rabbit then it sees the rabbit.
((("something" "visits" "rabbit" "+")) -> ("something" "sees" "rabbit" "+"))
If the rabbit is blue and the rabbit chases the mouse then the mouse chases the squirrel.
((("rabbit" "is" "blue" "+") ("rabbit" "chases" "mouse" "+")) -> ("mouse" "chases" "squirrel" "+"))
If something visits the lion and it sees the lion then the lion is green.
((("something" "visits" "lion" "+") ("something" "sees" "lion" "+")) -> ("lion" "is" "green" "+"))
The squirrel chases the lion.
True
1
proof
[(triple5)]
("squirrel" "chases" "lion" "+")
triple5
The rabbit visits the mouse.
False
1
inv-proof
[(triple4)]
("rabbit" "visits" "mouse" "+")
triple4
The squirrel sees the mouse.
True
2
proof
[(((triple7) -> rule4))]
("squirrel" "sees" "mouse" "+")
((triple7) -> (rule4 % int1))
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
int1
The squirrel does not see the mouse.
False
2
inv-proof
[(((triple7) -> rule4))]
("squirrel" "sees" "mouse" "-")
((triple7) -> (rule4 % int1))
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
int1
The squirrel chases the mouse.
True
3
proof
[(((((triple7) -> rule4)) -> rule3))]
("squirrel" "chases" "mouse" "+")
((((triple7) -> (rule4 % int2))) -> (rule3 % int1))
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
int1
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
int2
The squirrel does not chase the mouse.
False
3
inv-proof
[(((((triple7) -> rule4)) -> rule3))]
("squirrel" "chases" "mouse" "-")
((((triple7) -> (rule4 % int2))) -> (rule3 % int1))
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
int1
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
int2
The mouse is nice.
True
4
proof
[(((((((triple7) -> rule4)) -> rule3)) -> rule2))]
("mouse" "is" "nice" "+")
((((((triple7) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
int2
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
int3
The mouse is not nice.
False
4
inv-proof
[(((((((triple7) -> rule4)) -> rule3)) -> rule2))]
("mouse" "is" "nice" "-")
((((((triple7) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
int2
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
int3
The mouse does not see the squirrel.
True
5
proof
[(((((((((triple7) -> rule4)) -> rule3)) -> rule2)) -> rule1))]
("mouse" "sees" "squirrel" "-")
((((((((triple7) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The mouse does not see the squirrel.
("mouse" "sees" "squirrel" "-")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
int3
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
int4
The mouse does not see the mouse.
False
5
inv-proof
[(((((((((triple7) -> rule4)) -> rule3)) -> rule2)) -> rule5))]
("mouse" "sees" "mouse" "-")
((((((((triple7) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
int3
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
int4
The mouse chases the mouse.
True
6
proof
[(((((((((((triple7) -> rule4)) -> rule3)) -> rule2)) -> rule5)) -> rule3))]
("mouse" "chases" "mouse" "+")
((((((((((triple7) -> (rule4 % int5))) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int2
The mouse is nice.
("mouse" "is" "nice" "+")
int3
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
int4
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
int5
The mouse does not chase the mouse.
False
6
inv-proof
[(((((((((((triple7) -> rule4)) -> rule3)) -> rule2)) -> rule5)) -> rule3))]
("mouse" "chases" "mouse" "-")
((((((((((triple7) -> (rule4 % int5))) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int2
The mouse is nice.
("mouse" "is" "nice" "+")
int3
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
int4
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
int5
The rabbit does not see the mouse.
Unknown
inv-rconc
[@1: The rabbit sees the mouse.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("rabbit" "sees" "mouse" "-")
The lion sees the rabbit.
Unknown
rconc
[@1: The lion sees the rabbit.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("lion" "sees" "rabbit" "+")
The lion does not chase the mouse.
Unknown
inv-rconc
[@2: The lion chases the mouse.[CWA. Example of deepest failure = (rule3 <- rule4 <- FAIL)]]
("lion" "chases" "mouse" "-")
The squirrel sees the rabbit.
Unknown
rconc
[@1: The squirrel sees the rabbit.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("squirrel" "sees" "rabbit" "+")
The rabbit does not chase the mouse.
Unknown
inv-rconc
[@2: The rabbit chases the mouse.[CWA. Example of deepest failure = (rule3 <- rule4 <- FAIL)]]
("rabbit" "chases" "mouse" "-")
The mouse chases the squirrel.
Unknown
rconc
[@1: The mouse chases the squirrel.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("mouse" "chases" "squirrel" "+")
The lion does not visit the mouse.
Unknown
inv-random
[@0: The lion visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "mouse" "-")
The rabbit chases the squirrel.
Unknown
random
[@0: The rabbit chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "squirrel" "+")
The lion does not chase the rabbit.
Unknown
inv-random
[@0: The lion chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "rabbit" "-")
The squirrel is nice.
Unknown
random
[@0: The squirrel is nice.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "nice" "+")
The rabbit does not visit the squirrel.
Unknown
inv-random
[@0: The rabbit visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "squirrel" "-")
The rabbit visits the lion.
Unknown
random
[@0: The rabbit visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "lion" "+")
@0: The lion is green.[(triple1)] The lion sees the squirrel.[(triple2)] The mouse is not red.[(triple3)] The rabbit does not visit the mouse.[(triple4)] The squirrel chases the lion.[(triple5)] The squirrel chases the rabbit.[(triple6)] The squirrel is kind.[(triple7)] @1: The squirrel sees the mouse.[(((triple7) -> rule4))] @2: The squirrel chases the mouse.[(((((triple7) -> rule4)) -> rule3))] @3: The mouse is nice.[(((((((triple7) -> rule4)) -> rule3)) -> rule2))] @4: The mouse does not see the squirrel.[(((((((((triple7) -> rule4)) -> rule3)) -> rule2)) -> rule1))] The mouse sees the mouse.[(((((((((triple7) -> rule4)) -> rule3)) -> rule2)) -> rule5))] @5: The mouse chases the mouse.[(((((((((((triple7) -> rule4)) -> rule3)) -> rule2)) -> rule5)) -> rule3))]
The lion is green.
("lion" "is" "green" "+")
triple1
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
triple2
The mouse is not red.
("mouse" "is" "red" "-")
triple3
The rabbit does not visit the mouse.
("rabbit" "visits" "mouse" "-")
triple4
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
triple5
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
triple6
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple7
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
((triple7) -> (rule4 % int1))
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
int1
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
((((triple7) -> (rule4 % int2))) -> (rule3 % int1))
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
int1
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
int2
The mouse is nice.
("mouse" "is" "nice" "+")
((((((triple7) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
int2
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
int3
The mouse does not see the squirrel.
("mouse" "sees" "squirrel" "-")
((((((((triple7) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The mouse does not see the squirrel.
("mouse" "sees" "squirrel" "-")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
int3
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
int4
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
((((((((triple7) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
int3
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
int4
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
((((((((((triple7) -> (rule4 % int5))) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int2
The mouse is nice.
("mouse" "is" "nice" "+")
int3
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
int4
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
int5