The bear eats the lion. The bear eats the squirrel. The lion eats the bear. The lion eats the squirrel. The squirrel eats the bear. The squirrel eats the lion. The squirrel is big. The squirrel is green. The squirrel sees the bear. The squirrel sees the lion. If something eats the squirrel and the squirrel visits the lion then the squirrel sees the lion. If the bear eats the squirrel then the bear is round. If something visits the squirrel and the squirrel eats the lion then it is big. If something visits the lion then the lion eats the squirrel. If something sees the bear and the bear sees the squirrel then it visits the bear. If something sees the lion and the lion is big then it visits the squirrel. If something eats the lion then the lion visits the squirrel. If the lion sees the bear and the lion sees the squirrel then the squirrel visits the lion.
The bear eats the lion.
("bear" "eats" "lion" "+")
The bear eats the squirrel.
("bear" "eats" "squirrel" "+")
The lion eats the bear.
("lion" "eats" "bear" "+")
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
If something eats the squirrel and the squirrel visits the lion then the squirrel sees the lion.
((("something" "eats" "squirrel" "+") ("squirrel" "visits" "lion" "+")) -> ("squirrel" "sees" "lion" "+"))
If the bear eats the squirrel then the bear is round.
((("bear" "eats" "squirrel" "+")) -> ("bear" "is" "round" "+"))
If something visits the squirrel and the squirrel eats the lion then it is big.
((("something" "visits" "squirrel" "+") ("squirrel" "eats" "lion" "+")) -> ("something" "is" "big" "+"))
If something visits the lion then the lion eats the squirrel.
((("something" "visits" "lion" "+")) -> ("lion" "eats" "squirrel" "+"))
If something sees the bear and the bear sees the squirrel then it visits the bear.
((("something" "sees" "bear" "+") ("bear" "sees" "squirrel" "+")) -> ("something" "visits" "bear" "+"))
If something sees the lion and the lion is big then it visits the squirrel.
((("something" "sees" "lion" "+") ("lion" "is" "big" "+")) -> ("something" "visits" "squirrel" "+"))
If something eats the lion then the lion visits the squirrel.
((("something" "eats" "lion" "+")) -> ("lion" "visits" "squirrel" "+"))
If the lion sees the bear and the lion sees the squirrel then the squirrel visits the lion.
((("lion" "sees" "bear" "+") ("lion" "sees" "squirrel" "+")) -> ("squirrel" "visits" "lion" "+"))
The squirrel sees the lion.
True
1
proof
[(triple10)]
("squirrel" "sees" "lion" "+")
triple10
The lion does not eat the bear.
False
1
inv-proof
[(triple3)]
("lion" "eats" "bear" "-")
triple3
The bear is round.
True
2
proof
[(((triple2) -> rule2))]
("bear" "is" "round" "+")
((triple2) -> (rule2 % int1))
The bear is round.
("bear" "is" "round" "+")
int1
The bear is not round.
False
2
inv-proof
[(((triple2) -> rule2))]
("bear" "is" "round" "-")
((triple2) -> (rule2 % int1))
The bear is round.
("bear" "is" "round" "+")
int1
The lion is big.
True
4
proof
[(((((triple1) -> rule7) triple6) -> rule3) OR ((((triple6) -> rule7) triple6) -> rule3))]
("lion" "is" "big" "+")
((((triple1) -> (rule7 % int2)) triple6) -> (rule3 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int2
((((triple6) -> (rule7 % int2)) triple6) -> (rule3 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int2
The lion is not big.
False
4
inv-proof
[(((((triple1) -> rule7) triple6) -> rule3) OR ((((triple6) -> rule7) triple6) -> rule3))]
("lion" "is" "big" "-")
((((triple1) -> (rule7 % int2)) triple6) -> (rule3 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int2
((((triple6) -> (rule7 % int2)) triple6) -> (rule3 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int2
The squirrel visits the squirrel.
True
6
proof
[(((triple10 ((((triple1) -> rule7) triple6) -> rule3)) -> rule6) OR ((triple10 ((((triple6) -> rule7) triple6) -> rule3)) -> rule6))]
("squirrel" "visits" "squirrel" "+")
((triple10 ((((triple1) -> (rule7 % int3)) triple6) -> (rule3 % int2))) -> (rule6 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int3
((triple10 ((((triple6) -> (rule7 % int3)) triple6) -> (rule3 % int2))) -> (rule6 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int3
The squirrel does not visit the squirrel.
False
6
inv-proof
[(((triple10 ((((triple1) -> rule7) triple6) -> rule3)) -> rule6) OR ((triple10 ((((triple6) -> rule7) triple6) -> rule3)) -> rule6))]
("squirrel" "visits" "squirrel" "-")
((triple10 ((((triple1) -> (rule7 % int3)) triple6) -> (rule3 % int2))) -> (rule6 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int3
((triple10 ((((triple6) -> (rule7 % int3)) triple6) -> (rule3 % int2))) -> (rule6 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int3
The bear does not visit the squirrel.
Unknown
inv-rconc
[@1: The bear visits the squirrel.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bear" "visits" "squirrel" "-")
The squirrel visits the lion.
Unknown
rconc
[@1: The squirrel visits the lion.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("squirrel" "visits" "lion" "+")
The bear does not visit the bear.
Unknown
inv-rconc
[@1: The bear visits the bear.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bear" "visits" "bear" "-")
The lion visits the bear.
Unknown
rconc
[@1: The lion visits the bear.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("lion" "visits" "bear" "+")
The bear does not eat the bear.
Unknown
inv-random
[@0: The bear eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "bear" "-")
The bear is red.
Unknown
random
[@0: The bear is red.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "red" "+")
The lion is not green.
Unknown
inv-random
[@0: The lion is green.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "green" "-")
The bear visits the lion.
Unknown
random
[@0: The bear visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "lion" "+")
@0: The bear eats the lion.[(triple1)] The bear eats the squirrel.[(triple2)] The lion eats the bear.[(triple3)] The lion eats the squirrel.[(triple4)] The squirrel eats the bear.[(triple5)] The squirrel eats the lion.[(triple6)] The squirrel is big.[(triple7 OR ((((triple10 ((((triple1) -> rule7) triple6) -> rule3)) -> rule6) triple6) -> rule3) OR ((((triple10 ((((triple6) -> rule7) triple6) -> rule3)) -> rule6) triple6) -> rule3))] The squirrel is green.[(triple8)] The squirrel sees the bear.[(triple9)] The squirrel sees the lion.[(triple10)] @1: The bear is round.[(((triple2) -> rule2))] The lion visits the squirrel.[(((triple1) -> rule7) OR ((triple6) -> rule7))] @2: The lion is big.[(((((triple1) -> rule7) triple6) -> rule3) OR ((((triple6) -> rule7) triple6) -> rule3))] @3: The squirrel visits the squirrel.[(((triple10 ((((triple1) -> rule7) triple6) -> rule3)) -> rule6) OR ((triple10 ((((triple6) -> rule7) triple6) -> rule3)) -> rule6))]
The bear eats the lion.
("bear" "eats" "lion" "+")
triple1
The bear eats the squirrel.
("bear" "eats" "squirrel" "+")
triple2
The lion eats the bear.
("lion" "eats" "bear" "+")
triple3
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
triple4
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
triple5
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
triple6
The squirrel is big.
("squirrel" "is" "big" "+")
triple7
((((triple10 ((((triple1) -> (rule7 % int4)) triple6) -> (rule3 % int3))) -> (rule6 % int2)) triple6) -> (rule3 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int2
The lion is big.
("lion" "is" "big" "+")
int3
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int4
((((triple10 ((((triple6) -> (rule7 % int4)) triple6) -> (rule3 % int3))) -> (rule6 % int2)) triple6) -> (rule3 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int2
The lion is big.
("lion" "is" "big" "+")
int3
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int4
The squirrel is green.
("squirrel" "is" "green" "+")
triple8
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
triple9
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
triple10
The bear is round.
("bear" "is" "round" "+")
((triple2) -> (rule2 % int1))
The bear is round.
("bear" "is" "round" "+")
int1
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
((triple1) -> (rule7 % int1))
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int1
((triple6) -> (rule7 % int1))
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int1
The lion is big.
("lion" "is" "big" "+")
((((triple1) -> (rule7 % int2)) triple6) -> (rule3 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int2
((((triple6) -> (rule7 % int2)) triple6) -> (rule3 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int2
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
((triple10 ((((triple1) -> (rule7 % int3)) triple6) -> (rule3 % int2))) -> (rule6 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int3
((triple10 ((((triple6) -> (rule7 % int3)) triple6) -> (rule3 % int2))) -> (rule6 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int3