The bear likes the cat. The bear needs the cat. The cat is big. The cat is round. The lion is red. The lion likes the bear. The lion likes the cat. The lion needs the cat. The lion sees the bear. The lion sees the cat. If the bear sees the cat and the cat likes the bear then the bear needs the cat. Cold people are round. If someone sees the cat then they like the bear. If the bear is green then the bear is red. If someone sees the cat and the cat needs the bear then they see the bear. If the cat likes the lion then the lion likes the bear. If someone sees the cat then they are cold. If someone sees the bear then the bear sees the cat.
The bear likes the cat.
("bear" "likes" "cat" "+")
The bear needs the cat.
("bear" "needs" "cat" "+")
The cat is big.
("cat" "is" "big" "+")
The cat is round.
("cat" "is" "round" "+")
The lion is red.
("lion" "is" "red" "+")
The lion likes the bear.
("lion" "likes" "bear" "+")
The lion likes the cat.
("lion" "likes" "cat" "+")
The lion needs the cat.
("lion" "needs" "cat" "+")
The lion sees the bear.
("lion" "sees" "bear" "+")
The lion sees the cat.
("lion" "sees" "cat" "+")
If the bear sees the cat and the cat likes the bear then the bear needs the cat.
((("bear" "sees" "cat" "+") ("cat" "likes" "bear" "+")) -> ("bear" "needs" "cat" "+"))
Cold people are round.
((("someone" "is" "cold" "+")) -> ("someone" "is" "round" "+"))
If someone sees the cat then they like the bear.
((("someone" "sees" "cat" "+")) -> ("someone" "likes" "bear" "+"))
If the bear is green then the bear is red.
((("bear" "is" "green" "+")) -> ("bear" "is" "red" "+"))
If someone sees the cat and the cat needs the bear then they see the bear.
((("someone" "sees" "cat" "+") ("cat" "needs" "bear" "+")) -> ("someone" "sees" "bear" "+"))
If the cat likes the lion then the lion likes the bear.
((("cat" "likes" "lion" "+")) -> ("lion" "likes" "bear" "+"))
If someone sees the cat then they are cold.
((("someone" "sees" "cat" "+")) -> ("someone" "is" "cold" "+"))
If someone sees the bear then the bear sees the cat.
((("someone" "sees" "bear" "+")) -> ("bear" "sees" "cat" "+"))
The lion is red.
True
1
proof
[(triple5)]
("lion" "is" "red" "+")
triple5
The bear does not need the cat.
False
1
inv-proof
[(triple2)]
("bear" "needs" "cat" "-")
triple2
The lion is cold.
True
2
proof
[(((triple10) -> rule7))]
("lion" "is" "cold" "+")
((triple10) -> (rule7 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion is not cold.
False
2
inv-proof
[(((triple10) -> rule7))]
("lion" "is" "cold" "-")
((triple10) -> (rule7 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion is round.
True
3
proof
[(((((triple10) -> rule7)) -> rule2))]
("lion" "is" "round" "+")
((((triple10) -> (rule7 % int2))) -> (rule2 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
The bear is not cold.
False
3
inv-proof
[(((((triple9) -> rule8)) -> rule7))]
("bear" "is" "cold" "-")
((((triple9) -> (rule8 % int2))) -> (rule7 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear sees the cat.
("bear" "sees" "cat" "+")
int2
The bear is round.
True
4
proof
[(((((((triple9) -> rule8)) -> rule7)) -> rule2))]
("bear" "is" "round" "+")
((((((triple9) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
The bear is round.
("bear" "is" "round" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The bear sees the cat.
("bear" "sees" "cat" "+")
int3
The bear is not round.
False
4
inv-proof
[(((((((triple9) -> rule8)) -> rule7)) -> rule2))]
("bear" "is" "round" "-")
((((((triple9) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
The bear is round.
("bear" "is" "round" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The bear sees the cat.
("bear" "sees" "cat" "+")
int3
The cat does not see the bear.
Unknown
inv-rconc
[@1: The cat sees the bear.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "sees" "bear" "-")
The bear sees the bear.
Unknown
rconc
[@1: The bear sees the bear.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bear" "sees" "bear" "+")
The bear is not red.
Unknown
inv-rconc
[@1: The bear is red.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bear" "is" "red" "-")
The cat is cold.
Unknown
rconc
[@1: The cat is cold.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("cat" "is" "cold" "+")
The bear does not like the lion.
Unknown
inv-random
[@0: The bear likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "lion" "-")
The bear needs the bear.
Unknown
random
[@0: The bear needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "bear" "+")
The cat does not see the lion.
Unknown
inv-random
[@0: The cat sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "lion" "-")
The lion needs the lion.
Unknown
random
[@0: The lion needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "lion" "+")
@0: The bear likes the cat.[(triple1)] The bear needs the cat.[(triple2)] The cat is big.[(triple3)] The cat is round.[(triple4)] The lion is red.[(triple5)] The lion likes the bear.[(triple6 OR ((triple10) -> rule3))] The lion likes the cat.[(triple7)] The lion needs the cat.[(triple8)] The lion sees the bear.[(triple9)] The lion sees the cat.[(triple10)] @1: The bear sees the cat.[(((triple9) -> rule8))] The lion is cold.[(((triple10) -> rule7))] @2: The bear is cold.[(((((triple9) -> rule8)) -> rule7))] The bear likes the bear.[(((((triple9) -> rule8)) -> rule3))] The lion is round.[(((((triple10) -> rule7)) -> rule2))] @3: The bear is round.[(((((((triple9) -> rule8)) -> rule7)) -> rule2))]
The bear likes the cat.
("bear" "likes" "cat" "+")
triple1
The bear needs the cat.
("bear" "needs" "cat" "+")
triple2
The cat is big.
("cat" "is" "big" "+")
triple3
The cat is round.
("cat" "is" "round" "+")
triple4
The lion is red.
("lion" "is" "red" "+")
triple5
The lion likes the bear.
("lion" "likes" "bear" "+")
triple6
((triple10) -> (rule3 % int1))
The lion likes the bear.
("lion" "likes" "bear" "+")
int1
The lion likes the cat.
("lion" "likes" "cat" "+")
triple7
The lion needs the cat.
("lion" "needs" "cat" "+")
triple8
The lion sees the bear.
("lion" "sees" "bear" "+")
triple9
The lion sees the cat.
("lion" "sees" "cat" "+")
triple10
The bear sees the cat.
("bear" "sees" "cat" "+")
((triple9) -> (rule8 % int1))
The bear sees the cat.
("bear" "sees" "cat" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
((triple10) -> (rule7 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
((((triple9) -> (rule8 % int2))) -> (rule7 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear sees the cat.
("bear" "sees" "cat" "+")
int2
The bear likes the bear.
("bear" "likes" "bear" "+")
((((triple9) -> (rule8 % int2))) -> (rule3 % int1))
The bear likes the bear.
("bear" "likes" "bear" "+")
int1
The bear sees the cat.
("bear" "sees" "cat" "+")
int2
The lion is round.
("lion" "is" "round" "+")
((((triple10) -> (rule7 % int2))) -> (rule2 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
The bear is round.
("bear" "is" "round" "+")
((((((triple9) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
The bear is round.
("bear" "is" "round" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The bear sees the cat.
("bear" "sees" "cat" "+")
int3