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