The lion chases the squirrel. The lion is green. The lion is young. The lion sees the squirrel. The lion visits the squirrel. The squirrel is young. The squirrel visits the lion. If something is young then it visits the squirrel. If something is cold then it visits the squirrel. If something chases the lion then it sees the squirrel. If something chases the lion then the lion sees the squirrel. If something sees the lion then it is cold. If something visits the squirrel then it chases the lion.
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
The lion is green.
("lion" "is" "green" "+")
The lion is young.
("lion" "is" "young" "+")
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
The squirrel is young.
("squirrel" "is" "young" "+")
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
If something is young then it visits the squirrel.
((("something" "is" "young" "+")) -> ("something" "visits" "squirrel" "+"))
If something is cold then it visits the squirrel.
((("something" "is" "cold" "+")) -> ("something" "visits" "squirrel" "+"))
If something chases the lion then it sees the squirrel.
((("something" "chases" "lion" "+")) -> ("something" "sees" "squirrel" "+"))
If something chases the lion then the lion sees the squirrel.
((("something" "chases" "lion" "+")) -> ("lion" "sees" "squirrel" "+"))
If something sees the lion then it is cold.
((("something" "sees" "lion" "+")) -> ("something" "is" "cold" "+"))
If something visits the squirrel then it chases the lion.
((("something" "visits" "squirrel" "+")) -> ("something" "chases" "lion" "+"))
The lion is young.
True
1
proof
[(triple3)]
("lion" "is" "young" "+")
triple3
The squirrel is not young.
False
1
inv-proof
[(triple6)]
("squirrel" "is" "young" "-")
triple6
The lion chases the lion.
True
2
proof
[(((triple5) -> rule6) OR ((((triple3) -> rule1)) -> rule6))]
("lion" "chases" "lion" "+")
((triple5) -> (rule6 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
((((triple3) -> (rule1 % int2))) -> (rule6 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int2
The lion does not chase the lion.
False
2
inv-proof
[(((triple5) -> rule6) OR ((((triple3) -> rule1)) -> rule6))]
("lion" "chases" "lion" "-")
((triple5) -> (rule6 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
((((triple3) -> (rule1 % int2))) -> (rule6 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int2
The squirrel chases the lion.
True
3
proof
[(((((triple6) -> rule1)) -> rule6))]
("squirrel" "chases" "lion" "+")
((((triple6) -> (rule1 % int2))) -> (rule6 % int1))
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
int1
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int2
The squirrel does not chase the lion.
False
3
inv-proof
[(((((triple6) -> rule1)) -> rule6))]
("squirrel" "chases" "lion" "-")
((((triple6) -> (rule1 % int2))) -> (rule6 % int1))
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
int1
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int2
The squirrel sees the squirrel.
True
4
proof
[(((((((triple6) -> rule1)) -> rule6)) -> rule3))]
("squirrel" "sees" "squirrel" "+")
((((((triple6) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
int2
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int3
The squirrel does not see the squirrel.
False
4
inv-proof
[(((((((triple6) -> rule1)) -> rule6)) -> rule3))]
("squirrel" "sees" "squirrel" "-")
((((((triple6) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
int2
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int3
The lion is not cold.
Unknown
inv-rconc
[@1: The lion is cold.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("lion" "is" "cold" "-")
The squirrel is cold.
Unknown
rconc
[@1: The squirrel is cold.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("squirrel" "is" "cold" "+")
The squirrel does not chase the squirrel.
Unknown
inv-random
[@0: The squirrel chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "squirrel" "-")
The lion is big.
Unknown
random
[@0: The lion is big.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "big" "+")
The squirrel is not big.
Unknown
inv-random
[@0: The squirrel is big.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "big" "-")
The squirrel is kind.
Unknown
random
[@0: The squirrel is kind.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "kind" "+")
The squirrel is not green.
Unknown
inv-random
[@0: The squirrel is green.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "green" "-")
The lion sees the lion.
Unknown
random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "+")
@0: The lion chases the squirrel.[(triple1)] The lion is green.[(triple2)] The lion is young.[(triple3)] The lion sees the squirrel.[(triple4 OR ((((triple5) -> rule6)) -> rule3) OR ((((triple5) -> rule6)) -> rule4) OR ((((((triple3) -> rule1)) -> rule6)) -> rule3) OR ((((((triple3) -> rule1)) -> rule6)) -> rule4) OR ((((((triple6) -> rule1)) -> rule6)) -> rule4))] The lion visits the squirrel.[(triple5 OR ((triple3) -> rule1))] The squirrel is young.[(triple6)] The squirrel visits the lion.[(triple7)] @1: The lion chases the lion.[(((triple5) -> rule6) OR ((((triple3) -> rule1)) -> rule6))] The squirrel visits the squirrel.[(((triple6) -> rule1))] @2: The squirrel chases the lion.[(((((triple6) -> rule1)) -> rule6))] @3: The squirrel sees the squirrel.[(((((((triple6) -> rule1)) -> rule6)) -> rule3))]
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
triple1
The lion is green.
("lion" "is" "green" "+")
triple2
The lion is young.
("lion" "is" "young" "+")
triple3
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
triple4
((((triple5) -> (rule6 % int2))) -> (rule3 % int1))
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int1
The lion chases the lion.
("lion" "chases" "lion" "+")
int2
((((triple5) -> (rule6 % int2))) -> (rule4 % int1))
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int1
The lion chases the lion.
("lion" "chases" "lion" "+")
int2
((((((triple3) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int1
The lion chases the lion.
("lion" "chases" "lion" "+")
int2
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int3
((((((triple3) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int1
The lion chases the lion.
("lion" "chases" "lion" "+")
int2
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int3
((((((triple6) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int1
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
int2
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int3
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
triple5
((triple3) -> (rule1 % int1))
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int1
The squirrel is young.
("squirrel" "is" "young" "+")
triple6
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
triple7
The lion chases the lion.
("lion" "chases" "lion" "+")
((triple5) -> (rule6 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
((((triple3) -> (rule1 % int2))) -> (rule6 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int2
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
((triple6) -> (rule1 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
((((triple6) -> (rule1 % int2))) -> (rule6 % int1))
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
int1
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int2
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
((((((triple6) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
int2
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int3