The bear is cold. The tiger likes the bear. If someone is big and they like the bear then they like the tiger. If someone is blue then they see the tiger. If someone is cold and they see the tiger then they see the bear. Cold people are blue. All nice people are blue. Big, blue people are cold.
The bear is cold.
("bear" "is" "cold" "+")
The tiger likes the bear.
("tiger" "likes" "bear" "+")
If someone is big and they like the bear then they like the tiger.
((("someone" "is" "big" "+") ("someone" "likes" "bear" "+")) -> ("someone" "likes" "tiger" "+"))
If someone is blue then they see the tiger.
((("someone" "is" "blue" "+")) -> ("someone" "sees" "tiger" "+"))
If someone is cold and they see the tiger then they see the bear.
((("someone" "is" "cold" "+") ("someone" "sees" "tiger" "+")) -> ("someone" "sees" "bear" "+"))
Cold people are blue.
((("someone" "is" "cold" "+")) -> ("someone" "is" "blue" "+"))
All nice people are blue.
((("someone" "is" "nice" "+")) -> ("someone" "is" "blue" "+"))
Big, blue people are cold.
((("someone" "is" "big" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "cold" "+"))
The bear is cold.
True
1
proof
[(triple1)]
("bear" "is" "cold" "+")
triple1
The bear is not cold.
False
1
inv-proof
[(triple1)]
("bear" "is" "cold" "-")
triple1
The bear is blue.
True
2
proof
[(((triple1) -> rule4))]
("bear" "is" "blue" "+")
((triple1) -> (rule4 % int1))
The bear is blue.
("bear" "is" "blue" "+")
int1
The bear is not blue.
False
2
inv-proof
[(((triple1) -> rule4))]
("bear" "is" "blue" "-")
((triple1) -> (rule4 % int1))
The bear is blue.
("bear" "is" "blue" "+")
int1
The bear sees the tiger.
True
3
proof
[(((((triple1) -> rule4)) -> rule2))]
("bear" "sees" "tiger" "+")
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
The bear sees the tiger.
("bear" "sees" "tiger" "+")
int1
The bear is blue.
("bear" "is" "blue" "+")
int2
The bear does not see the tiger.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule2))]
("bear" "sees" "tiger" "-")
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
The bear sees the tiger.
("bear" "sees" "tiger" "+")
int1
The bear is blue.
("bear" "is" "blue" "+")
int2
The bear sees the bear.
True
5
proof
[(((triple1 ((((triple1) -> rule4)) -> rule2)) -> rule3))]
("bear" "sees" "bear" "+")
((triple1 ((((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The bear sees the bear.
("bear" "sees" "bear" "+")
int1
The bear sees the tiger.
("bear" "sees" "tiger" "+")
int2
The bear is blue.
("bear" "is" "blue" "+")
int3
The bear does not see the bear.
False
5
inv-proof
[(((triple1 ((((triple1) -> rule4)) -> rule2)) -> rule3))]
("bear" "sees" "bear" "-")
((triple1 ((((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The bear sees the bear.
("bear" "sees" "bear" "+")
int1
The bear sees the tiger.
("bear" "sees" "tiger" "+")
int2
The bear is blue.
("bear" "is" "blue" "+")
int3
The bear does not like the tiger.
Unknown
inv-rconc
[@1: The bear likes the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "likes" "tiger" "-")
The tiger sees the bear.
Unknown
rconc
[@2: The tiger sees the bear.[CWA. Example of deepest failure = (rule3 <- rule6 <- FAIL)]]
("tiger" "sees" "bear" "+")
The tiger does not see the tiger.
Unknown
inv-rconc
[@3: The tiger sees the tiger.[CWA. Example of deepest failure = (rule2 <- rule4 <- rule6 <- FAIL)]]
("tiger" "sees" "tiger" "-")
The tiger is blue.
Unknown
rconc
[@2: The tiger is blue.[CWA. Example of deepest failure = (rule4 <- rule6 <- FAIL)]]
("tiger" "is" "blue" "+")
The bear is not big.
Unknown
inv-random
[@0: The bear is big.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "big" "-")
The tiger visits the tiger.
Unknown
random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "+")
The bear does not visit the tiger.
Unknown
inv-random
[@0: The bear visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "tiger" "-")
The bear likes the bear.
Unknown
random
[@0: The bear likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "bear" "+")
@0: The bear is cold.[(triple1)] The tiger likes the bear.[(triple2)] @1: The bear is blue.[(((triple1) -> rule4))] @2: The bear sees the tiger.[(((((triple1) -> rule4)) -> rule2))] @3: The bear sees the bear.[(((triple1 ((((triple1) -> rule4)) -> rule2)) -> rule3))]
The bear is cold.
("bear" "is" "cold" "+")
triple1
The tiger likes the bear.
("tiger" "likes" "bear" "+")
triple2
The bear is blue.
("bear" "is" "blue" "+")
((triple1) -> (rule4 % int1))
The bear is blue.
("bear" "is" "blue" "+")
int1
The bear sees the tiger.
("bear" "sees" "tiger" "+")
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
The bear sees the tiger.
("bear" "sees" "tiger" "+")
int1
The bear is blue.
("bear" "is" "blue" "+")
int2
The bear sees the bear.
("bear" "sees" "bear" "+")
((triple1 ((((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The bear sees the bear.
("bear" "sees" "bear" "+")
int1
The bear sees the tiger.
("bear" "sees" "tiger" "+")
int2
The bear is blue.
("bear" "is" "blue" "+")
int3