The bear is rough. The bear is not young. The tiger is round. If something is rough then it eats the bear. If something sees the bear and the bear visits the tiger then it eats the bear. If something visits the tiger then the tiger eats the bear. If something sees the tiger then the tiger does not eat the bear. If something is round then it visits the bear. If something eats the bear then it sees the tiger.
The bear is rough.
("bear" "is" "rough" "+")
The bear is not young.
("bear" "is" "young" "-")
The tiger is round.
("tiger" "is" "round" "+")
If something is rough then it eats the bear.
((("something" "is" "rough" "+")) -> ("something" "eats" "bear" "+"))
If something sees the bear and the bear visits the tiger then it eats the bear.
((("something" "sees" "bear" "+") ("bear" "visits" "tiger" "+")) -> ("something" "eats" "bear" "+"))
If something visits the tiger then the tiger eats the bear.
((("something" "visits" "tiger" "+")) -> ("tiger" "eats" "bear" "+"))
If something sees the tiger then the tiger does not eat the bear.
((("something" "sees" "tiger" "+")) -> ("tiger" "eats" "bear" "-"))
If something is round then it visits the bear.
((("something" "is" "round" "+")) -> ("something" "visits" "bear" "+"))
If something eats the bear then it sees the tiger.
((("something" "eats" "bear" "+")) -> ("something" "sees" "tiger" "+"))
The bear is not young.
True
1
proof
[(triple2)]
("bear" "is" "young" "-")
triple2
The bear is young.
False
1
inv-proof
[(triple2)]
("bear" "is" "young" "+")
triple2
The tiger visits the bear.
True
2
proof
[(((triple3) -> rule5))]
("tiger" "visits" "bear" "+")
((triple3) -> (rule5 % int1))
The tiger visits the bear.
("tiger" "visits" "bear" "+")
int1
The bear does not eat the bear.
False
2
inv-proof
[(((triple1) -> rule1))]
("bear" "eats" "bear" "-")
((triple1) -> (rule1 % int1))
The bear eats the bear.
("bear" "eats" "bear" "+")
int1
The bear sees the tiger.
True
3
proof
[(((((triple1) -> rule1)) -> rule6))]
("bear" "sees" "tiger" "+")
((((triple1) -> (rule1 % int2))) -> (rule6 % int1))
The bear sees the tiger.
("bear" "sees" "tiger" "+")
int1
The bear eats the bear.
("bear" "eats" "bear" "+")
int2
The bear does not see the tiger.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule6))]
("bear" "sees" "tiger" "-")
((((triple1) -> (rule1 % int2))) -> (rule6 % int1))
The bear sees the tiger.
("bear" "sees" "tiger" "+")
int1
The bear eats the bear.
("bear" "eats" "bear" "+")
int2
The tiger does not eat the bear.
True
4
proof
[(((((((triple1) -> rule1)) -> rule6)) -> rule4))]
("tiger" "eats" "bear" "-")
((((((triple1) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The tiger does not eat the bear.
("tiger" "eats" "bear" "-")
int1
The bear sees the tiger.
("bear" "sees" "tiger" "+")
int2
The bear eats the bear.
("bear" "eats" "bear" "+")
int3
The tiger eats the bear.
False
4
inv-proof
[(((((((triple1) -> rule1)) -> rule6)) -> rule4))]
("tiger" "eats" "bear" "+")
((((((triple1) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The tiger does not eat the bear.
("tiger" "eats" "bear" "-")
int1
The bear sees the tiger.
("bear" "sees" "tiger" "+")
int2
The bear eats the bear.
("bear" "eats" "bear" "+")
int3
The bear does not visit the bear.
Unknown
inv-rconc
[@1: The bear visits the bear.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bear" "visits" "bear" "-")
The tiger sees the tiger.
Unknown
rconc
[@1: The tiger sees the tiger.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "sees" "tiger" "+")
The tiger is not young.
Unknown
inv-random
[@0: The tiger is young.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "young" "-")
The tiger is nice.
Unknown
random
[@0: The tiger is nice.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "nice" "+")
The tiger does not visit the tiger.
Unknown
inv-random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "-")
The tiger is green.
Unknown
random
[@0: The tiger is green.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "green" "+")
The bear is not nice.
Unknown
inv-random
[@0: The bear is nice.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "nice" "-")
The tiger eats the tiger.
Unknown
random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "+")
@0: The bear is not young.[(triple2)] The bear is rough.[(triple1)] The tiger is round.[(triple3)] @1: The bear eats the bear.[(((triple1) -> rule1))] The tiger visits the bear.[(((triple3) -> rule5))] @2: The bear sees the tiger.[(((((triple1) -> rule1)) -> rule6))] @3: The tiger does not eat the bear.[(((((((triple1) -> rule1)) -> rule6)) -> rule4))]
The bear is not young.
("bear" "is" "young" "-")
triple2
The bear is rough.
("bear" "is" "rough" "+")
triple1
The tiger is round.
("tiger" "is" "round" "+")
triple3
The bear eats the bear.
("bear" "eats" "bear" "+")
((triple1) -> (rule1 % int1))
The bear eats the bear.
("bear" "eats" "bear" "+")
int1
The tiger visits the bear.
("tiger" "visits" "bear" "+")
((triple3) -> (rule5 % int1))
The tiger visits the bear.
("tiger" "visits" "bear" "+")
int1
The bear sees the tiger.
("bear" "sees" "tiger" "+")
((((triple1) -> (rule1 % int2))) -> (rule6 % int1))
The bear sees the tiger.
("bear" "sees" "tiger" "+")
int1
The bear eats the bear.
("bear" "eats" "bear" "+")
int2
The tiger does not eat the bear.
("tiger" "eats" "bear" "-")
((((((triple1) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The tiger does not eat the bear.
("tiger" "eats" "bear" "-")
int1
The bear sees the tiger.
("bear" "sees" "tiger" "+")
int2
The bear eats the bear.
("bear" "eats" "bear" "+")
int3