The lion is cold. The lion likes the rabbit. The rabbit is big. The rabbit is cold. The squirrel eats the lion. The squirrel eats the rabbit. The squirrel is round. The squirrel is young. The squirrel likes the lion. The squirrel likes the rabbit. The squirrel sees the lion. The squirrel sees the rabbit. If something eats the lion then it likes the squirrel. If something eats the squirrel and the squirrel sees the lion then the squirrel eats the rabbit. If something eats the rabbit and it eats the lion then the lion is nice. If something eats the lion and it sees the lion then the lion eats the rabbit. If the squirrel sees the lion and the lion likes the rabbit then the squirrel eats the lion. If something eats the squirrel and it eats the lion then it likes the lion. If something likes the rabbit then the rabbit likes the lion. If something eats the rabbit and the rabbit is round then the rabbit eats the lion.
The lion is cold.
("lion" "is" "cold" "+")
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
The squirrel is round.
("squirrel" "is" "round" "+")
The squirrel is young.
("squirrel" "is" "young" "+")
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
If something eats the lion then it likes the squirrel.
((("something" "eats" "lion" "+")) -> ("something" "likes" "squirrel" "+"))
If something eats the squirrel and the squirrel sees the lion then the squirrel eats the rabbit.
((("something" "eats" "squirrel" "+") ("squirrel" "sees" "lion" "+")) -> ("squirrel" "eats" "rabbit" "+"))
If something eats the rabbit and it eats the lion then the lion is nice.
((("something" "eats" "rabbit" "+") ("something" "eats" "lion" "+")) -> ("lion" "is" "nice" "+"))
If something eats the lion and it sees the lion then the lion eats the rabbit.
((("something" "eats" "lion" "+") ("something" "sees" "lion" "+")) -> ("lion" "eats" "rabbit" "+"))
If the squirrel sees the lion and the lion likes the rabbit then the squirrel eats the lion.
((("squirrel" "sees" "lion" "+") ("lion" "likes" "rabbit" "+")) -> ("squirrel" "eats" "lion" "+"))
If something eats the squirrel and it eats the lion then it likes the lion.
((("something" "eats" "squirrel" "+") ("something" "eats" "lion" "+")) -> ("something" "likes" "lion" "+"))
If something likes the rabbit then the rabbit likes the lion.
((("something" "likes" "rabbit" "+")) -> ("rabbit" "likes" "lion" "+"))
If something eats the rabbit and the rabbit is round then the rabbit eats the lion.
((("something" "eats" "rabbit" "+") ("rabbit" "is" "round" "+")) -> ("rabbit" "eats" "lion" "+"))
The squirrel likes the lion.
True
1
proof
[(triple9)]
("squirrel" "likes" "lion" "+")
triple9
The squirrel does not like the lion.
False
1
inv-proof
[(triple9)]
("squirrel" "likes" "lion" "-")
triple9
The squirrel likes the squirrel.
True
2
proof
[(((triple5) -> rule1) OR ((((triple11 triple2) -> rule5)) -> rule1))]
("squirrel" "likes" "squirrel" "+")
((triple5) -> (rule1 % int1))
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int1
((((triple11 triple2) -> (rule5 % int2))) -> (rule1 % int1))
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int1
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
int2
The rabbit does not like the lion.
False
2
inv-proof
[(((triple10) -> rule7) OR ((triple2) -> rule7))]
("rabbit" "likes" "lion" "-")
((triple10) -> (rule7 % int1))
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
int1
((triple2) -> (rule7 % int1))
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
int1
The rabbit does not eat the lion.
Unknown
inv-rconc
[@1: The rabbit eats the lion.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("rabbit" "eats" "lion" "-")
The rabbit likes the squirrel.
Unknown
rconc
[@2: The rabbit likes the squirrel.[CWA. Example of deepest failure = (rule1 <- rule8 <- FAIL)]]
("rabbit" "likes" "squirrel" "+")
The rabbit does not like the rabbit.
Unknown
inv-random
[@0: The rabbit likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "rabbit" "-")
The lion is young.
Unknown
random
[@0: The lion is young.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "young" "+")
@0: The lion is cold.[(triple1)] The lion likes the rabbit.[(triple2)] The rabbit is big.[(triple3)] The rabbit is cold.[(triple4)] The squirrel eats the lion.[(triple5 OR ((triple11 triple2) -> rule5))] The squirrel eats the rabbit.[(triple6)] The squirrel is round.[(triple7)] The squirrel is young.[(triple8)] The squirrel likes the lion.[(triple9)] The squirrel likes the rabbit.[(triple10)] The squirrel sees the lion.[(triple11)] The squirrel sees the rabbit.[(triple12)] @1: The lion eats the rabbit.[(((triple5 triple11) -> rule4) OR ((((triple11 triple2) -> rule5) triple11) -> rule4))] The lion is nice.[(((triple6 triple5) -> rule3) OR ((triple6 ((triple11 triple2) -> rule5)) -> rule3))] The rabbit likes the lion.[(((triple10) -> rule7) OR ((triple2) -> rule7))] The squirrel likes the squirrel.[(((triple5) -> rule1) OR ((((triple11 triple2) -> rule5)) -> rule1))]
The lion is cold.
("lion" "is" "cold" "+")
triple1
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
triple2
The rabbit is big.
("rabbit" "is" "big" "+")
triple3
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple4
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
triple5
((triple11 triple2) -> (rule5 % int1))
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
int1
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
triple6
The squirrel is round.
("squirrel" "is" "round" "+")
triple7
The squirrel is young.
("squirrel" "is" "young" "+")
triple8
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
triple9
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
triple10
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
triple11
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
triple12
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
((triple5 triple11) -> (rule4 % int1))
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
int1
((((triple11 triple2) -> (rule5 % int2)) triple11) -> (rule4 % int1))
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
int1
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
int2
The lion is nice.
("lion" "is" "nice" "+")
((triple6 triple5) -> (rule3 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
((triple6 ((triple11 triple2) -> (rule5 % int2))) -> (rule3 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
int2
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
((triple10) -> (rule7 % int1))
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
int1
((triple2) -> (rule7 % int1))
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
int1
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
((triple5) -> (rule1 % int1))
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int1
((((triple11 triple2) -> (rule5 % int2))) -> (rule1 % int1))
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int1
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
int2