The lion chases the squirrel. The lion is cold. The lion is rough. The lion is round. The lion likes the squirrel. The lion sees the squirrel. The squirrel chases the lion. The squirrel is cold. The squirrel is kind. The squirrel is rough. The squirrel likes the lion. The squirrel sees the lion. If someone is young then they like the squirrel. If someone sees the lion and the lion chases the squirrel then the squirrel is round. If someone likes the squirrel and the squirrel chases the lion then they chase the squirrel. If someone likes the squirrel then they see the squirrel. If someone chases the squirrel then they chase the lion. If someone chases the lion and the lion likes the squirrel then they like the lion. If someone sees the lion and they see the squirrel then they like the lion. If the lion sees the squirrel then the lion is young.
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion is round.
("lion" "is" "round" "+")
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
The squirrel is rough.
("squirrel" "is" "rough" "+")
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
If someone is young then they like the squirrel.
((("someone" "is" "young" "+")) -> ("someone" "likes" "squirrel" "+"))
If someone sees the lion and the lion chases the squirrel then the squirrel is round.
((("someone" "sees" "lion" "+") ("lion" "chases" "squirrel" "+")) -> ("squirrel" "is" "round" "+"))
If someone likes the squirrel and the squirrel chases the lion then they chase the squirrel.
((("someone" "likes" "squirrel" "+") ("squirrel" "chases" "lion" "+")) -> ("someone" "chases" "squirrel" "+"))
If someone likes the squirrel then they see the squirrel.
((("someone" "likes" "squirrel" "+")) -> ("someone" "sees" "squirrel" "+"))
If someone chases the squirrel then they chase the lion.
((("someone" "chases" "squirrel" "+")) -> ("someone" "chases" "lion" "+"))
If someone chases the lion and the lion likes the squirrel then they like the lion.
((("someone" "chases" "lion" "+") ("lion" "likes" "squirrel" "+")) -> ("someone" "likes" "lion" "+"))
If someone sees the lion and they see the squirrel then they like the lion.
((("someone" "sees" "lion" "+") ("someone" "sees" "squirrel" "+")) -> ("someone" "likes" "lion" "+"))
If the lion sees the squirrel then the lion is young.
((("lion" "sees" "squirrel" "+")) -> ("lion" "is" "young" "+"))
The lion is cold.
True
1
proof
[(triple2)]
("lion" "is" "cold" "+")
triple2
The lion is not round.
False
1
inv-proof
[(triple4)]
("lion" "is" "round" "-")
triple4
The lion is young.
True
2
proof
[(((triple6) -> rule8) OR ((((triple5) -> rule4)) -> rule8))]
("lion" "is" "young" "+")
((triple6) -> (rule8 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
((((triple5) -> (rule4 % int2))) -> (rule8 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int2
The lion does not chase the lion.
False
2
inv-proof
[(((triple1) -> rule5) OR ((((triple5 triple7) -> rule3)) -> rule5) OR ((((((((triple6) -> rule8)) -> rule1) triple7) -> rule3)) -> rule5))]
("lion" "chases" "lion" "-")
((triple1) -> (rule5 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
((((triple5 triple7) -> (rule3 % int2))) -> (rule5 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int2
((((((((triple6) -> (rule8 % int4))) -> (rule1 % int3)) triple7) -> (rule3 % int2))) -> (rule5 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int2
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
int3
The lion is young.
("lion" "is" "young" "+")
int4
The lion likes the lion.
True
4
proof
[(((((triple1) -> rule5) triple5) -> rule6) OR ((((((triple5 triple7) -> rule3)) -> rule5) triple5) -> rule6) OR ((((triple1) -> rule5) ((((triple6) -> rule8)) -> rule1)) -> rule6) OR ((((((triple5 triple7) -> rule3)) -> rule5) ((((triple6) -> rule8)) -> rule1)) -> rule6) OR ((((((((((triple6) -> rule8)) -> rule1) triple7) -> rule3)) -> rule5) triple5) -> rule6) OR ((((((((((triple6) -> rule8)) -> rule1) triple7) -> rule3)) -> rule5) ((((triple6) -> rule8)) -> rule1)) -> rule6))]
("lion" "likes" "lion" "+")
((((triple1) -> (rule5 % int2)) triple5) -> (rule6 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion chases the lion.
("lion" "chases" "lion" "+")
int2
((((((triple5 triple7) -> (rule3 % int3))) -> (rule5 % int2)) triple5) -> (rule6 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion chases the lion.
("lion" "chases" "lion" "+")
int2
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int3
((((triple1) -> (rule5 % int4)) ((((triple6) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
int2
The lion is young.
("lion" "is" "young" "+")
int3
The lion chases the lion.
("lion" "chases" "lion" "+")
int4
((((((triple5 triple7) -> (rule3 % int5))) -> (rule5 % int4)) ((((triple6) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
int2
The lion is young.
("lion" "is" "young" "+")
int3
The lion chases the lion.
("lion" "chases" "lion" "+")
int4
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int5
((((((((((triple6) -> (rule8 % int5))) -> (rule1 % int4)) triple7) -> (rule3 % int3))) -> (rule5 % int2)) triple5) -> (rule6 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion chases the lion.
("lion" "chases" "lion" "+")
int2
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int3
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
int4
The lion is young.
("lion" "is" "young" "+")
int5
((((((((((triple6) -> (rule8 % int5))) -> (rule1 % int4)) triple7) -> (rule3 % int3))) -> (rule5 % int2)) ((((triple6) -> (rule8 % int5))) -> (rule1 % int4))) -> (rule6 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion chases the lion.
("lion" "chases" "lion" "+")
int2
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int3
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
int4
The lion is young.
("lion" "is" "young" "+")
int5
The lion does not like the lion.
False
4
inv-proof
[(((((triple1) -> rule5) triple5) -> rule6) OR ((((((triple5 triple7) -> rule3)) -> rule5) triple5) -> rule6) OR ((((triple1) -> rule5) ((((triple6) -> rule8)) -> rule1)) -> rule6) OR ((((((triple5 triple7) -> rule3)) -> rule5) ((((triple6) -> rule8)) -> rule1)) -> rule6) OR ((((((((((triple6) -> rule8)) -> rule1) triple7) -> rule3)) -> rule5) triple5) -> rule6) OR ((((((((((triple6) -> rule8)) -> rule1) triple7) -> rule3)) -> rule5) ((((triple6) -> rule8)) -> rule1)) -> rule6))]
("lion" "likes" "lion" "-")
((((triple1) -> (rule5 % int2)) triple5) -> (rule6 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion chases the lion.
("lion" "chases" "lion" "+")
int2
((((((triple5 triple7) -> (rule3 % int3))) -> (rule5 % int2)) triple5) -> (rule6 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion chases the lion.
("lion" "chases" "lion" "+")
int2
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int3
((((triple1) -> (rule5 % int4)) ((((triple6) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
int2
The lion is young.
("lion" "is" "young" "+")
int3
The lion chases the lion.
("lion" "chases" "lion" "+")
int4
((((((triple5 triple7) -> (rule3 % int5))) -> (rule5 % int4)) ((((triple6) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
int2
The lion is young.
("lion" "is" "young" "+")
int3
The lion chases the lion.
("lion" "chases" "lion" "+")
int4
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int5
((((((((((triple6) -> (rule8 % int5))) -> (rule1 % int4)) triple7) -> (rule3 % int3))) -> (rule5 % int2)) triple5) -> (rule6 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion chases the lion.
("lion" "chases" "lion" "+")
int2
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int3
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
int4
The lion is young.
("lion" "is" "young" "+")
int5
((((((((((triple6) -> (rule8 % int5))) -> (rule1 % int4)) triple7) -> (rule3 % int3))) -> (rule5 % int2)) ((((triple6) -> (rule8 % int5))) -> (rule1 % int4))) -> (rule6 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion chases the lion.
("lion" "chases" "lion" "+")
int2
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int3
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
int4
The lion is young.
("lion" "is" "young" "+")
int5
The squirrel does not like the squirrel.
Unknown
inv-rconc
[@1: The squirrel likes the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "likes" "squirrel" "-")
The squirrel chases the squirrel.
Unknown
rconc
[@2: The squirrel chases the squirrel.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("squirrel" "chases" "squirrel" "+")
The squirrel does not see the squirrel.
Unknown
inv-rconc
[@2: The squirrel sees the squirrel.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("squirrel" "sees" "squirrel" "-")
The lion sees the lion.
Unknown
random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "+")
The squirrel is not young.
Unknown
inv-random
[@0: The squirrel is young.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "young" "-")
The lion is kind.
Unknown
random
[@0: The lion is kind.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "kind" "+")
@0: The lion chases the squirrel.[(triple1 OR ((triple5 triple7) -> rule3) OR ((((((triple6) -> rule8)) -> rule1) triple7) -> rule3))] The lion is cold.[(triple2)] The lion is rough.[(triple3)] The lion is round.[(triple4)] The lion likes the squirrel.[(triple5 OR ((((triple6) -> rule8)) -> rule1))] The lion sees the squirrel.[(triple6 OR ((triple5) -> rule4))] The squirrel chases the lion.[(triple7)] The squirrel is cold.[(triple8)] The squirrel is kind.[(triple9)] The squirrel is rough.[(triple10)] The squirrel likes the lion.[(triple11 OR ((triple7 triple5) -> rule6) OR ((triple7 ((((triple6) -> rule8)) -> rule1)) -> rule6))] The squirrel sees the lion.[(triple12)] @1: The lion chases the lion.[(((triple1) -> rule5) OR ((((triple5 triple7) -> rule3)) -> rule5) OR ((((((((triple6) -> rule8)) -> rule1) triple7) -> rule3)) -> rule5))] The lion is young.[(((triple6) -> rule8) OR ((((triple5) -> rule4)) -> rule8))] The squirrel is round.[(((triple12 triple1) -> rule2) OR ((triple12 ((triple5 triple7) -> rule3)) -> rule2) OR ((triple12 ((((((triple6) -> rule8)) -> rule1) triple7) -> rule3)) -> rule2))] @2: The lion likes the lion.[(((((triple1) -> rule5) triple5) -> rule6) OR ((((((triple5 triple7) -> rule3)) -> rule5) triple5) -> rule6) OR ((((triple1) -> rule5) ((((triple6) -> rule8)) -> rule1)) -> rule6) OR ((((((triple5 triple7) -> rule3)) -> rule5) ((((triple6) -> rule8)) -> rule1)) -> rule6) OR ((((((((((triple6) -> rule8)) -> rule1) triple7) -> rule3)) -> rule5) triple5) -> rule6) OR ((((((((((triple6) -> rule8)) -> rule1) triple7) -> rule3)) -> rule5) ((((triple6) -> rule8)) -> rule1)) -> rule6))]
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
triple1
((triple5 triple7) -> (rule3 % int1))
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int1
((((((triple6) -> (rule8 % int3))) -> (rule1 % int2)) triple7) -> (rule3 % int1))
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int1
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
int2
The lion is young.
("lion" "is" "young" "+")
int3
The lion is cold.
("lion" "is" "cold" "+")
triple2
The lion is rough.
("lion" "is" "rough" "+")
triple3
The lion is round.
("lion" "is" "round" "+")
triple4
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
triple5
((((triple6) -> (rule8 % int2))) -> (rule1 % int1))
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
triple6
((triple5) -> (rule4 % int1))
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int1
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
triple7
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple8
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple9
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple10
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
triple11
((triple7 triple5) -> (rule6 % int1))
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
int1
((triple7 ((((triple6) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
int1
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
int2
The lion is young.
("lion" "is" "young" "+")
int3
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
triple12
The lion chases the lion.
("lion" "chases" "lion" "+")
((triple1) -> (rule5 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
((((triple5 triple7) -> (rule3 % int2))) -> (rule5 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int2
((((((((triple6) -> (rule8 % int4))) -> (rule1 % int3)) triple7) -> (rule3 % int2))) -> (rule5 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int2
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
int3
The lion is young.
("lion" "is" "young" "+")
int4
The lion is young.
("lion" "is" "young" "+")
((triple6) -> (rule8 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
((((triple5) -> (rule4 % int2))) -> (rule8 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int2
The squirrel is round.
("squirrel" "is" "round" "+")
((triple12 triple1) -> (rule2 % int1))
The squirrel is round.
("squirrel" "is" "round" "+")
int1
((triple12 ((triple5 triple7) -> (rule3 % int2))) -> (rule2 % int1))
The squirrel is round.
("squirrel" "is" "round" "+")
int1
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int2
((triple12 ((((((triple6) -> (rule8 % int4))) -> (rule1 % int3)) triple7) -> (rule3 % int2))) -> (rule2 % int1))
The squirrel is round.
("squirrel" "is" "round" "+")
int1
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int2
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
int3
The lion is young.
("lion" "is" "young" "+")
int4
The lion likes the lion.
("lion" "likes" "lion" "+")
((((triple1) -> (rule5 % int2)) triple5) -> (rule6 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion chases the lion.
("lion" "chases" "lion" "+")
int2
((((((triple5 triple7) -> (rule3 % int3))) -> (rule5 % int2)) triple5) -> (rule6 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion chases the lion.
("lion" "chases" "lion" "+")
int2
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int3
((((triple1) -> (rule5 % int4)) ((((triple6) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
int2
The lion is young.
("lion" "is" "young" "+")
int3
The lion chases the lion.
("lion" "chases" "lion" "+")
int4
((((((triple5 triple7) -> (rule3 % int5))) -> (rule5 % int4)) ((((triple6) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
int2
The lion is young.
("lion" "is" "young" "+")
int3
The lion chases the lion.
("lion" "chases" "lion" "+")
int4
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int5
((((((((((triple6) -> (rule8 % int5))) -> (rule1 % int4)) triple7) -> (rule3 % int3))) -> (rule5 % int2)) triple5) -> (rule6 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion chases the lion.
("lion" "chases" "lion" "+")
int2
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int3
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
int4
The lion is young.
("lion" "is" "young" "+")
int5
((((((((((triple6) -> (rule8 % int5))) -> (rule1 % int4)) triple7) -> (rule3 % int3))) -> (rule5 % int2)) ((((triple6) -> (rule8 % int5))) -> (rule1 % int4))) -> (rule6 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion chases the lion.
("lion" "chases" "lion" "+")
int2
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int3
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
int4
The lion is young.
("lion" "is" "young" "+")
int5