The bear is red. The bear likes the tiger. The bear sees the tiger. The bear visits the tiger. The tiger is cold. The tiger is green. The tiger is nice. The tiger is red. The tiger is round. The tiger likes the bear. The tiger sees the bear. The tiger visits the bear. If someone is round then they visit the bear. If someone likes the bear then they see the bear. All red people are nice. If someone visits the bear and the bear visits the tiger then they are green. If someone is nice then they visit the bear. If someone is round then they are nice.
The bear is red.
("bear" "is" "red" "+")
The bear likes the tiger.
("bear" "likes" "tiger" "+")
The bear sees the tiger.
("bear" "sees" "tiger" "+")
The bear visits the tiger.
("bear" "visits" "tiger" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger likes the bear.
("tiger" "likes" "bear" "+")
The tiger sees the bear.
("tiger" "sees" "bear" "+")
The tiger visits the bear.
("tiger" "visits" "bear" "+")
If someone is round then they visit the bear.
((("someone" "is" "round" "+")) -> ("someone" "visits" "bear" "+"))
If someone likes the bear then they see the bear.
((("someone" "likes" "bear" "+")) -> ("someone" "sees" "bear" "+"))
All red people are nice.
((("someone" "is" "red" "+")) -> ("someone" "is" "nice" "+"))
If someone visits the bear and the bear visits the tiger then they are green.
((("someone" "visits" "bear" "+") ("bear" "visits" "tiger" "+")) -> ("someone" "is" "green" "+"))
If someone is nice then they visit the bear.
((("someone" "is" "nice" "+")) -> ("someone" "visits" "bear" "+"))
If someone is round then they are nice.
((("someone" "is" "round" "+")) -> ("someone" "is" "nice" "+"))
The tiger visits the bear.
True
1
proof
[(triple12 OR ((triple7) -> rule5) OR ((triple9) -> rule1) OR ((((triple8) -> rule3)) -> rule5) OR ((((triple9) -> rule6)) -> rule5))]
("tiger" "visits" "bear" "+")
triple12
((triple7) -> (rule5 % int1))
The tiger visits the bear.
("tiger" "visits" "bear" "+")
int1
((triple9) -> (rule1 % int1))
The tiger visits the bear.
("tiger" "visits" "bear" "+")
int1
((((triple8) -> (rule3 % int2))) -> (rule5 % int1))
The tiger visits the bear.
("tiger" "visits" "bear" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
((((triple9) -> (rule6 % int2))) -> (rule5 % int1))
The tiger visits the bear.
("tiger" "visits" "bear" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
The bear does not visit the tiger.
False
1
inv-proof
[(triple4)]
("bear" "visits" "tiger" "-")
triple4
The bear is nice.
True
2
proof
[(((triple1) -> rule3))]
("bear" "is" "nice" "+")
((triple1) -> (rule3 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear is not nice.
False
2
inv-proof
[(((triple1) -> rule3))]
("bear" "is" "nice" "-")
((triple1) -> (rule3 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear visits the bear.
True
3
proof
[(((((triple1) -> rule3)) -> rule5))]
("bear" "visits" "bear" "+")
((((triple1) -> (rule3 % int2))) -> (rule5 % int1))
The bear visits the bear.
("bear" "visits" "bear" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
int2
The bear does not visit the bear.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule5))]
("bear" "visits" "bear" "-")
((((triple1) -> (rule3 % int2))) -> (rule5 % int1))
The bear visits the bear.
("bear" "visits" "bear" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
int2
The bear is green.
True
5
proof
[(((((((triple1) -> rule3)) -> rule5) triple4) -> rule4))]
("bear" "is" "green" "+")
((((((triple1) -> (rule3 % int3))) -> (rule5 % int2)) triple4) -> (rule4 % int1))
The bear is green.
("bear" "is" "green" "+")
int1
The bear visits the bear.
("bear" "visits" "bear" "+")
int2
The bear is nice.
("bear" "is" "nice" "+")
int3
The bear is not green.
False
5
inv-proof
[(((((((triple1) -> rule3)) -> rule5) triple4) -> rule4))]
("bear" "is" "green" "-")
((((((triple1) -> (rule3 % int3))) -> (rule5 % int2)) triple4) -> (rule4 % int1))
The bear is green.
("bear" "is" "green" "+")
int1
The bear visits the bear.
("bear" "visits" "bear" "+")
int2
The bear is nice.
("bear" "is" "nice" "+")
int3
The bear does not see the bear.
Unknown
inv-rconc
[@1: The bear sees the bear.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "sees" "bear" "-")
The bear likes the bear.
Unknown
random
[@0: The bear likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "bear" "+")
The bear is not round.
Unknown
inv-random
[@0: The bear is round.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "round" "-")
The tiger likes the tiger.
Unknown
random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "+")
The bear is not cold.
Unknown
inv-random
[@0: The bear is cold.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "cold" "-")
The tiger visits the tiger.
Unknown
random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "+")
@0: The bear is red.[(triple1)] The bear likes the tiger.[(triple2)] The bear sees the tiger.[(triple3)] The bear visits the tiger.[(triple4)] The tiger is cold.[(triple5)] The tiger is green.[(triple6 OR ((triple12 triple4) -> rule4) OR ((((triple7) -> rule5) triple4) -> rule4) OR ((((triple9) -> rule1) triple4) -> rule4) OR ((((((triple8) -> rule3)) -> rule5) triple4) -> rule4) OR ((((((triple9) -> rule6)) -> rule5) triple4) -> rule4))] The tiger is nice.[(triple7 OR ((triple8) -> rule3) OR ((triple9) -> rule6))] The tiger is red.[(triple8)] The tiger is round.[(triple9)] The tiger likes the bear.[(triple10)] The tiger sees the bear.[(triple11 OR ((triple10) -> rule2))] The tiger visits the bear.[(triple12 OR ((triple7) -> rule5) OR ((triple9) -> rule1) OR ((((triple8) -> rule3)) -> rule5) OR ((((triple9) -> rule6)) -> rule5))] @1: The bear is nice.[(((triple1) -> rule3))] @2: The bear visits the bear.[(((((triple1) -> rule3)) -> rule5))] @3: The bear is green.[(((((((triple1) -> rule3)) -> rule5) triple4) -> rule4))]
The bear is red.
("bear" "is" "red" "+")
triple1
The bear likes the tiger.
("bear" "likes" "tiger" "+")
triple2
The bear sees the tiger.
("bear" "sees" "tiger" "+")
triple3
The bear visits the tiger.
("bear" "visits" "tiger" "+")
triple4
The tiger is cold.
("tiger" "is" "cold" "+")
triple5
The tiger is green.
("tiger" "is" "green" "+")
triple6
((triple12 triple4) -> (rule4 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
((((triple7) -> (rule5 % int2)) triple4) -> (rule4 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger visits the bear.
("tiger" "visits" "bear" "+")
int2
((((triple9) -> (rule1 % int2)) triple4) -> (rule4 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger visits the bear.
("tiger" "visits" "bear" "+")
int2
((((((triple8) -> (rule3 % int3))) -> (rule5 % int2)) triple4) -> (rule4 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger visits the bear.
("tiger" "visits" "bear" "+")
int2
The tiger is nice.
("tiger" "is" "nice" "+")
int3
((((((triple9) -> (rule6 % int3))) -> (rule5 % int2)) triple4) -> (rule4 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger visits the bear.
("tiger" "visits" "bear" "+")
int2
The tiger is nice.
("tiger" "is" "nice" "+")
int3
The tiger is nice.
("tiger" "is" "nice" "+")
triple7
((triple8) -> (rule3 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
((triple9) -> (rule6 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
triple8
The tiger is round.
("tiger" "is" "round" "+")
triple9
The tiger likes the bear.
("tiger" "likes" "bear" "+")
triple10
The tiger sees the bear.
("tiger" "sees" "bear" "+")
triple11
((triple10) -> (rule2 % int1))
The tiger sees the bear.
("tiger" "sees" "bear" "+")
int1
The tiger visits the bear.
("tiger" "visits" "bear" "+")
triple12
((triple7) -> (rule5 % int1))
The tiger visits the bear.
("tiger" "visits" "bear" "+")
int1
((triple9) -> (rule1 % int1))
The tiger visits the bear.
("tiger" "visits" "bear" "+")
int1
((((triple8) -> (rule3 % int2))) -> (rule5 % int1))
The tiger visits the bear.
("tiger" "visits" "bear" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
((((triple9) -> (rule6 % int2))) -> (rule5 % int1))
The tiger visits the bear.
("tiger" "visits" "bear" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
The bear is nice.
("bear" "is" "nice" "+")
((triple1) -> (rule3 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear visits the bear.
("bear" "visits" "bear" "+")
((((triple1) -> (rule3 % int2))) -> (rule5 % int1))
The bear visits the bear.
("bear" "visits" "bear" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
int2
The bear is green.
("bear" "is" "green" "+")
((((((triple1) -> (rule3 % int3))) -> (rule5 % int2)) triple4) -> (rule4 % int1))
The bear is green.
("bear" "is" "green" "+")
int1
The bear visits the bear.
("bear" "visits" "bear" "+")
int2
The bear is nice.
("bear" "is" "nice" "+")
int3