The bear is big. The bear is cold. The bear is green. The bear sees the tiger. The bear visits the tiger. The tiger eats the bear. The tiger visits the bear. If something sees the tiger and the tiger eats the bear then it visits the bear. If something eats the tiger then it is not big. If the bear sees the tiger and the bear eats the tiger then the bear visits the tiger. If the bear eats the tiger and the bear sees the tiger then the tiger sees the bear. If the bear sees the tiger and the tiger eats the bear then the tiger sees the bear. If something sees the bear then it eats the tiger.
The bear is big.
("bear" "is" "big" "+")
The bear is cold.
("bear" "is" "cold" "+")
The bear is green.
("bear" "is" "green" "+")
The bear sees the tiger.
("bear" "sees" "tiger" "+")
The bear visits the tiger.
("bear" "visits" "tiger" "+")
The tiger eats the bear.
("tiger" "eats" "bear" "+")
The tiger visits the bear.
("tiger" "visits" "bear" "+")
If something sees the tiger and the tiger eats the bear then it visits the bear.
((("something" "sees" "tiger" "+") ("tiger" "eats" "bear" "+")) -> ("something" "visits" "bear" "+"))
If something eats the tiger then it is not big.
((("something" "eats" "tiger" "+")) -> ("something" "is" "big" "-"))
If the bear sees the tiger and the bear eats the tiger then the bear visits the tiger.
((("bear" "sees" "tiger" "+") ("bear" "eats" "tiger" "+")) -> ("bear" "visits" "tiger" "+"))
If the bear eats the tiger and the bear sees the tiger then the tiger sees the bear.
((("bear" "eats" "tiger" "+") ("bear" "sees" "tiger" "+")) -> ("tiger" "sees" "bear" "+"))
If the bear sees the tiger and the tiger eats the bear then the tiger sees the bear.
((("bear" "sees" "tiger" "+") ("tiger" "eats" "bear" "+")) -> ("tiger" "sees" "bear" "+"))
If something sees the bear then it eats the tiger.
((("something" "sees" "bear" "+")) -> ("something" "eats" "tiger" "+"))
The bear is cold.
True
1
proof
[(triple2)]
("bear" "is" "cold" "+")
triple2
The bear is not big.
False
1
inv-proof
[(triple1)]
("bear" "is" "big" "-")
triple1
The tiger sees the bear.
True
3
proof
[(((triple4 triple6) -> rule5))]
("tiger" "sees" "bear" "+")
((triple4 triple6) -> (rule5 % int1))
The tiger sees the bear.
("tiger" "sees" "bear" "+")
int1
The bear does not visit the bear.
False
3
inv-proof
[(((triple4 triple6) -> rule1))]
("bear" "visits" "bear" "-")
((triple4 triple6) -> (rule1 % int1))
The bear visits the bear.
("bear" "visits" "bear" "+")
int1
The tiger eats the tiger.
True
4
proof
[(((((triple4 triple6) -> rule5)) -> rule6))]
("tiger" "eats" "tiger" "+")
((((triple4 triple6) -> (rule5 % int2))) -> (rule6 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger sees the bear.
("tiger" "sees" "bear" "+")
int2
The tiger does not eat the tiger.
False
4
inv-proof
[(((((triple4 triple6) -> rule5)) -> rule6))]
("tiger" "eats" "tiger" "-")
((((triple4 triple6) -> (rule5 % int2))) -> (rule6 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger sees the bear.
("tiger" "sees" "bear" "+")
int2
The tiger is not big.
True
5
proof
[(((((((triple4 triple6) -> rule5)) -> rule6)) -> rule2))]
("tiger" "is" "big" "-")
((((((triple4 triple6) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The tiger is not big.
("tiger" "is" "big" "-")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int2
The tiger sees the bear.
("tiger" "sees" "bear" "+")
int3
The tiger is big.
False
5
inv-proof
[(((((((triple4 triple6) -> rule5)) -> rule6)) -> rule2))]
("tiger" "is" "big" "+")
((((((triple4 triple6) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The tiger is not big.
("tiger" "is" "big" "-")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int2
The tiger sees the bear.
("tiger" "sees" "bear" "+")
int3
The bear does not eat the tiger.
Unknown
inv-rconc
[@1: The bear eats the tiger.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bear" "eats" "tiger" "-")
The tiger visits the tiger.
Unknown
random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "+")
The bear is not nice.
Unknown
inv-random
[@0: The bear is nice.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "nice" "-")
The tiger is kind.
Unknown
random
[@0: The tiger is kind.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "kind" "+")
The bear is not kind.
Unknown
inv-random
[@0: The bear is kind.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "kind" "-")
The tiger is green.
Unknown
random
[@0: The tiger is green.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "green" "+")
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 tiger sees the tiger.
Unknown
random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "+")
@0: The bear is big.[(triple1)] The bear is cold.[(triple2)] The bear is green.[(triple3)] The bear sees the tiger.[(triple4)] The bear visits the tiger.[(triple5)] The tiger eats the bear.[(triple6)] The tiger visits the bear.[(triple7)] @1: The bear visits the bear.[(((triple4 triple6) -> rule1))] The tiger sees the bear.[(((triple4 triple6) -> rule5))] @2: The tiger eats the tiger.[(((((triple4 triple6) -> rule5)) -> rule6))] @3: The tiger is not big.[(((((((triple4 triple6) -> rule5)) -> rule6)) -> rule2))]
The bear is big.
("bear" "is" "big" "+")
triple1
The bear is cold.
("bear" "is" "cold" "+")
triple2
The bear is green.
("bear" "is" "green" "+")
triple3
The bear sees the tiger.
("bear" "sees" "tiger" "+")
triple4
The bear visits the tiger.
("bear" "visits" "tiger" "+")
triple5
The tiger eats the bear.
("tiger" "eats" "bear" "+")
triple6
The tiger visits the bear.
("tiger" "visits" "bear" "+")
triple7
The bear visits the bear.
("bear" "visits" "bear" "+")
((triple4 triple6) -> (rule1 % int1))
The bear visits the bear.
("bear" "visits" "bear" "+")
int1
The tiger sees the bear.
("tiger" "sees" "bear" "+")
((triple4 triple6) -> (rule5 % int1))
The tiger sees the bear.
("tiger" "sees" "bear" "+")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
((((triple4 triple6) -> (rule5 % int2))) -> (rule6 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger sees the bear.
("tiger" "sees" "bear" "+")
int2
The tiger is not big.
("tiger" "is" "big" "-")
((((((triple4 triple6) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The tiger is not big.
("tiger" "is" "big" "-")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int2
The tiger sees the bear.
("tiger" "sees" "bear" "+")
int3