The bear sees the tiger. The tiger is cold. The tiger is kind. If something sees the tiger then it likes the bear. If the tiger sees the bear and the bear is blue then the bear is green. If something likes the bear then it likes the tiger. If something needs the tiger and the tiger is blue then it likes the tiger. If something sees the tiger then it does not see the bear. If the bear needs the tiger then the bear sees the tiger. If something is kind then it sees the tiger. If the tiger does not see the bear then the tiger is not green.
The bear sees the tiger.
("bear" "sees" "tiger" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
If something sees the tiger then it likes the bear.
((("something" "sees" "tiger" "+")) -> ("something" "likes" "bear" "+"))
If the tiger sees the bear and the bear is blue then the bear is green.
((("tiger" "sees" "bear" "+") ("bear" "is" "blue" "+")) -> ("bear" "is" "green" "+"))
If something likes the bear then it likes the tiger.
((("something" "likes" "bear" "+")) -> ("something" "likes" "tiger" "+"))
If something needs the tiger and the tiger is blue then it likes the tiger.
((("something" "needs" "tiger" "+") ("tiger" "is" "blue" "+")) -> ("something" "likes" "tiger" "+"))
If something sees the tiger then it does not see the bear.
((("something" "sees" "tiger" "+")) -> ("something" "sees" "bear" "-"))
If the bear needs the tiger then the bear sees the tiger.
((("bear" "needs" "tiger" "+")) -> ("bear" "sees" "tiger" "+"))
If something is kind then it sees the tiger.
((("something" "is" "kind" "+")) -> ("something" "sees" "tiger" "+"))
If the tiger does not see the bear then the tiger is not green.
((("tiger" "sees" "bear" "~")) -> ("tiger" "is" "green" "-"))
The bear sees the tiger.
True
1
proof
[(triple1)]
("bear" "sees" "tiger" "+")
triple1
The bear does not see the tiger.
False
1
inv-proof
[(triple1)]
("bear" "sees" "tiger" "-")
triple1
The bear does not see the bear.
True
2
proof
[(((triple1) -> rule5))]
("bear" "sees" "bear" "-")
((triple1) -> (rule5 % int1))
The bear does not see the bear.
("bear" "sees" "bear" "-")
int1
The tiger does not see the tiger.
False
2
inv-proof
[(((triple3) -> rule7))]
("tiger" "sees" "tiger" "-")
((triple3) -> (rule7 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger does not see the bear.
True
3
proof
[(((((triple3) -> rule7)) -> rule5))]
("tiger" "sees" "bear" "-")
((((triple3) -> (rule7 % int2))) -> (rule5 % int1))
The tiger does not see the bear.
("tiger" "sees" "bear" "-")
int1
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int2
The bear does not like the tiger.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule3))]
("bear" "likes" "tiger" "-")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The bear likes the tiger.
("bear" "likes" "tiger" "+")
int1
The bear likes the bear.
("bear" "likes" "bear" "+")
int2
The tiger likes the tiger.
True
4
proof
[(((((((triple3) -> rule7)) -> rule1)) -> rule3))]
("tiger" "likes" "tiger" "+")
((((((triple3) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int2
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int3
The tiger is green.
False
4
inv-proof
[(((((((triple3) -> rule7)) -> rule5)) -> rule8))]
("tiger" "is" "green" "+")
((((((triple3) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
The tiger is not green.
("tiger" "is" "green" "-")
int1
The tiger does not see the bear.
("tiger" "sees" "bear" "-")
int2
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int3
The bear is not green.
Unknown
inv-rconc
[@1: The bear is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "is" "green" "-")
The tiger is round.
Unknown
random
[@0: The tiger is round.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "round" "+")
The bear is not kind.
Unknown
inv-random
[@0: The bear is kind.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "kind" "-")
The bear is round.
Unknown
random
[@0: The bear is round.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "round" "+")
The tiger does not need the tiger.
Unknown
inv-random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "-")
The bear is blue.
Unknown
random
[@0: The bear is blue.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "blue" "+")
The tiger is not blue.
Unknown
inv-random
[@0: The tiger is blue.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "blue" "-")
The bear is cold.
Unknown
random
[@0: The bear is cold.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "cold" "+")
@0: The bear sees the tiger.[(triple1)] The tiger is cold.[(triple2)] The tiger is kind.[(triple3)] @1: The bear does not see the bear.[(((triple1) -> rule5))] The bear likes the bear.[(((triple1) -> rule1))] The tiger sees the tiger.[(((triple3) -> rule7))] @2: The bear likes the tiger.[(((((triple1) -> rule1)) -> rule3))] The tiger does not see the bear.[(((((triple3) -> rule7)) -> rule5))] The tiger likes the bear.[(((((triple3) -> rule7)) -> rule1))] @3: The tiger is not green.[(((((((triple3) -> rule7)) -> rule5)) -> rule8))] The tiger likes the tiger.[(((((((triple3) -> rule7)) -> rule1)) -> rule3))]
The bear sees the tiger.
("bear" "sees" "tiger" "+")
triple1
The tiger is cold.
("tiger" "is" "cold" "+")
triple2
The tiger is kind.
("tiger" "is" "kind" "+")
triple3
The bear does not see the bear.
("bear" "sees" "bear" "-")
((triple1) -> (rule5 % int1))
The bear does not see the bear.
("bear" "sees" "bear" "-")
int1
The bear likes the bear.
("bear" "likes" "bear" "+")
((triple1) -> (rule1 % int1))
The bear likes the bear.
("bear" "likes" "bear" "+")
int1
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
((triple3) -> (rule7 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The bear likes the tiger.
("bear" "likes" "tiger" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The bear likes the tiger.
("bear" "likes" "tiger" "+")
int1
The bear likes the bear.
("bear" "likes" "bear" "+")
int2
The tiger does not see the bear.
("tiger" "sees" "bear" "-")
((((triple3) -> (rule7 % int2))) -> (rule5 % int1))
The tiger does not see the bear.
("tiger" "sees" "bear" "-")
int1
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int2
The tiger likes the bear.
("tiger" "likes" "bear" "+")
((((triple3) -> (rule7 % int2))) -> (rule1 % int1))
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int1
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int2
The tiger is not green.
("tiger" "is" "green" "-")
((((((triple3) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
The tiger is not green.
("tiger" "is" "green" "-")
int1
The tiger does not see the bear.
("tiger" "sees" "bear" "-")
int2
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int3
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
((((((triple3) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int2
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int3