The bear eats the lion. The bear is cold. The bear is round. The bear likes the lion. The lion is round. The lion likes the bear. The lion sees the bear. Round people are cold. If the bear is green and the bear is not round then the bear eats the lion. If someone likes the lion then they are not green. If someone sees the bear then they see the lion. If someone sees the bear and they are cold then they like the lion. If someone is green and they do not like the lion then the lion eats the bear.
The bear eats the lion.
("bear" "eats" "lion" "+")
The bear is cold.
("bear" "is" "cold" "+")
The bear is round.
("bear" "is" "round" "+")
The bear likes the lion.
("bear" "likes" "lion" "+")
The lion is round.
("lion" "is" "round" "+")
The lion likes the bear.
("lion" "likes" "bear" "+")
The lion sees the bear.
("lion" "sees" "bear" "+")
Round people are cold.
((("someone" "is" "round" "+")) -> ("someone" "is" "cold" "+"))
If the bear is green and the bear is not round then the bear eats the lion.
((("bear" "is" "green" "+") ("bear" "is" "round" "~")) -> ("bear" "eats" "lion" "+"))
If someone likes the lion then they are not green.
((("someone" "likes" "lion" "+")) -> ("someone" "is" "green" "-"))
If someone sees the bear then they see the lion.
((("someone" "sees" "bear" "+")) -> ("someone" "sees" "lion" "+"))
If someone sees the bear and they are cold then they like the lion.
((("someone" "sees" "bear" "+") ("someone" "is" "cold" "+")) -> ("someone" "likes" "lion" "+"))
If someone is green and they do not like the lion then the lion eats the bear.
((("someone" "is" "green" "+") ("someone" "likes" "lion" "~")) -> ("lion" "eats" "bear" "+"))
The bear is round.
True
1
proof
[(triple3)]
("bear" "is" "round" "+")
triple3
The bear does not like the lion.
False
1
inv-proof
[(triple4)]
("bear" "likes" "lion" "-")
triple4
The lion sees the lion.
True
2
proof
[(((triple7) -> rule4))]
("lion" "sees" "lion" "+")
((triple7) -> (rule4 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The bear is green.
False
2
inv-proof
[(((triple4) -> rule3))]
("bear" "is" "green" "+")
((triple4) -> (rule3 % int1))
The bear is not green.
("bear" "is" "green" "-")
int1
The lion likes the lion.
True
4
proof
[(((triple7 ((triple5) -> rule1)) -> rule5))]
("lion" "likes" "lion" "+")
((triple7 ((triple5) -> (rule1 % int2))) -> (rule5 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
The lion does not like the lion.
False
4
inv-proof
[(((triple7 ((triple5) -> rule1)) -> rule5))]
("lion" "likes" "lion" "-")
((triple7 ((triple5) -> (rule1 % int2))) -> (rule5 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
The lion is not green.
True
5
proof
[(((((triple7 ((triple5) -> rule1)) -> rule5)) -> rule3))]
("lion" "is" "green" "-")
((((triple7 ((triple5) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The lion is not green.
("lion" "is" "green" "-")
int1
The lion likes the lion.
("lion" "likes" "lion" "+")
int2
The lion is cold.
("lion" "is" "cold" "+")
int3
The lion is green.
False
5
inv-proof
[(((((triple7 ((triple5) -> rule1)) -> rule5)) -> rule3))]
("lion" "is" "green" "+")
((((triple7 ((triple5) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The lion is not green.
("lion" "is" "green" "-")
int1
The lion likes the lion.
("lion" "likes" "lion" "+")
int2
The lion is cold.
("lion" "is" "cold" "+")
int3
The bear does not see the lion.
Unknown
inv-rconc
[@1: The bear sees the lion.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bear" "sees" "lion" "-")
The lion eats the bear.
Unknown
rconc
[@1: The lion eats the bear.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "eats" "bear" "+")
The bear is not nice.
Unknown
inv-random
[@0: The bear is nice.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "nice" "-")
The bear eats the bear.
Unknown
random
[@0: The bear eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "bear" "+")
The lion is not nice.
Unknown
inv-random
[@0: The lion is nice.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "nice" "-")
The lion eats the lion.
Unknown
random
[@0: The lion eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "lion" "+")
The bear does not see the bear.
Unknown
inv-random
[@0: The bear sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "bear" "-")
The lion is young.
Unknown
random
[@0: The lion is young.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "young" "+")
@0: The bear eats the lion.[(triple1)] The bear is cold.[(triple2 OR ((triple3) -> rule1))] The bear is round.[(triple3)] The bear likes the lion.[(triple4)] The lion is round.[(triple5)] The lion likes the bear.[(triple6)] The lion sees the bear.[(triple7)] @1: The bear is not green.[(((triple4) -> rule3))] The lion is cold.[(((triple5) -> rule1))] The lion sees the lion.[(((triple7) -> rule4))] @2: The lion likes the lion.[(((triple7 ((triple5) -> rule1)) -> rule5))] @3: The lion is not green.[(((((triple7 ((triple5) -> rule1)) -> rule5)) -> rule3))]
The bear eats the lion.
("bear" "eats" "lion" "+")
triple1
The bear is cold.
("bear" "is" "cold" "+")
triple2
((triple3) -> (rule1 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear is round.
("bear" "is" "round" "+")
triple3
The bear likes the lion.
("bear" "likes" "lion" "+")
triple4
The lion is round.
("lion" "is" "round" "+")
triple5
The lion likes the bear.
("lion" "likes" "bear" "+")
triple6
The lion sees the bear.
("lion" "sees" "bear" "+")
triple7
The bear is not green.
("bear" "is" "green" "-")
((triple4) -> (rule3 % int1))
The bear is not green.
("bear" "is" "green" "-")
int1
The lion is cold.
("lion" "is" "cold" "+")
((triple5) -> (rule1 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion sees the lion.
("lion" "sees" "lion" "+")
((triple7) -> (rule4 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The lion likes the lion.
("lion" "likes" "lion" "+")
((triple7 ((triple5) -> (rule1 % int2))) -> (rule5 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
The lion is not green.
("lion" "is" "green" "-")
((((triple7 ((triple5) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The lion is not green.
("lion" "is" "green" "-")
int1
The lion likes the lion.
("lion" "likes" "lion" "+")
int2
The lion is cold.
("lion" "is" "cold" "+")
int3