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