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