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