The bear chases the tiger. The bear eats the tiger. The bear is blue. The bear is nice. The bear is not red. The bear is round. The bear is young. The bear visits the tiger. The tiger chases the bear. The tiger does not eat the bear. The tiger is blue. The tiger is nice. The tiger is round. The tiger is young. The tiger does not visit the bear. If someone chases the bear and the bear does not chase the tiger then the bear is not red. If someone visits the tiger then the tiger is blue. If someone visits the tiger then they visit the bear. If the bear does not chase the tiger then the bear does not visit the tiger. If the bear chases the tiger then the bear visits the tiger. If the bear does not eat the tiger then the tiger visits the bear. If someone visits the bear then they eat the bear. If the bear visits the tiger and the tiger does not chase the bear then the tiger is nice.
The bear chases the tiger.
("bear" "chases" "tiger" "+")
The bear eats the tiger.
("bear" "eats" "tiger" "+")
The bear is blue.
("bear" "is" "blue" "+")
The bear is nice.
("bear" "is" "nice" "+")
The bear is not red.
("bear" "is" "red" "-")
The bear is round.
("bear" "is" "round" "+")
The bear is young.
("bear" "is" "young" "+")
The bear visits the tiger.
("bear" "visits" "tiger" "+")
The tiger chases the bear.
("tiger" "chases" "bear" "+")
The tiger does not eat the bear.
("tiger" "eats" "bear" "-")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger does not visit the bear.
("tiger" "visits" "bear" "-")
If someone chases the bear and the bear does not chase the tiger then the bear is not red.
((("someone" "chases" "bear" "+") ("bear" "chases" "tiger" "~")) -> ("bear" "is" "red" "-"))
If someone visits the tiger then the tiger is blue.
((("someone" "visits" "tiger" "+")) -> ("tiger" "is" "blue" "+"))
If someone visits the tiger then they visit the bear.
((("someone" "visits" "tiger" "+")) -> ("someone" "visits" "bear" "+"))
If the bear does not chase the tiger then the bear does not visit the tiger.
((("bear" "chases" "tiger" "~")) -> ("bear" "visits" "tiger" "-"))
If the bear chases the tiger then the bear visits the tiger.
((("bear" "chases" "tiger" "+")) -> ("bear" "visits" "tiger" "+"))
If the bear does not eat the tiger then the tiger visits the bear.
((("bear" "eats" "tiger" "~")) -> ("tiger" "visits" "bear" "+"))
If someone visits the bear then they eat the bear.
((("someone" "visits" "bear" "+")) -> ("someone" "eats" "bear" "+"))
If the bear visits the tiger and the tiger does not chase the bear then the tiger is nice.
((("bear" "visits" "tiger" "+") ("tiger" "chases" "bear" "~")) -> ("tiger" "is" "nice" "+"))
The bear is nice.
True
1
proof
[(triple4)]
("bear" "is" "nice" "+")
triple4
The tiger is not blue.
False
1
inv-proof
[(triple11 OR ((triple8) -> rule2) OR ((((triple1) -> rule5)) -> rule2))]
("tiger" "is" "blue" "-")
triple11
((triple8) -> (rule2 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The bear visits the tiger.
("bear" "visits" "tiger" "+")
int2
The bear visits the bear.
True
2
proof
[(((triple8) -> rule3) OR ((((triple1) -> rule5)) -> rule3))]
("bear" "visits" "bear" "+")
((triple8) -> (rule3 % int1))
The bear visits the bear.
("bear" "visits" "bear" "+")
int1
((((triple1) -> (rule5 % int2))) -> (rule3 % int1))
The bear visits the bear.
("bear" "visits" "bear" "+")
int1
The bear visits the tiger.
("bear" "visits" "tiger" "+")
int2
The bear does not visit the bear.
False
2
inv-proof
[(((triple8) -> rule3) OR ((((triple1) -> rule5)) -> rule3))]
("bear" "visits" "bear" "-")
((triple8) -> (rule3 % int1))
The bear visits the bear.
("bear" "visits" "bear" "+")
int1
((((triple1) -> (rule5 % int2))) -> (rule3 % int1))
The bear visits the bear.
("bear" "visits" "bear" "+")
int1
The bear visits the tiger.
("bear" "visits" "tiger" "+")
int2
The bear eats the bear.
True
3
proof
[(((((triple8) -> rule3)) -> rule7) OR ((((((triple1) -> rule5)) -> rule3)) -> rule7))]
("bear" "eats" "bear" "+")
((((triple8) -> (rule3 % int2))) -> (rule7 % int1))
The bear eats the bear.
("bear" "eats" "bear" "+")
int1
The bear visits the bear.
("bear" "visits" "bear" "+")
int2
((((((triple1) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The bear eats the bear.
("bear" "eats" "bear" "+")
int1
The bear visits the bear.
("bear" "visits" "bear" "+")
int2
The bear visits the tiger.
("bear" "visits" "tiger" "+")
int3
The bear does not eat the bear.
False
3
inv-proof
[(((((triple8) -> rule3)) -> rule7) OR ((((((triple1) -> rule5)) -> rule3)) -> rule7))]
("bear" "eats" "bear" "-")
((((triple8) -> (rule3 % int2))) -> (rule7 % int1))
The bear eats the bear.
("bear" "eats" "bear" "+")
int1
The bear visits the bear.
("bear" "visits" "bear" "+")
int2
((((((triple1) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The bear eats the bear.
("bear" "eats" "bear" "+")
int1
The bear visits the bear.
("bear" "visits" "bear" "+")
int2
The bear visits the tiger.
("bear" "visits" "tiger" "+")
int3
The bear does not chase the bear.
Unknown
inv-random
[@0: The bear chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "bear" "-")
The tiger visits the tiger.
Unknown
random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "+")
The tiger does not chase the tiger.
Unknown
inv-random
[@0: The tiger chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "tiger" "-")
The tiger is red.
Unknown
random
[@0: The tiger is red.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "red" "+")
@0: The bear chases the tiger.[(triple1)] The bear eats the tiger.[(triple2)] The bear is blue.[(triple3)] The bear is nice.[(triple4)] The bear is not red.[(triple5)] The bear is round.[(triple6)] The bear is young.[(triple7)] The bear visits the tiger.[(triple8 OR ((triple1) -> rule5))] The tiger chases the bear.[(triple9)] The tiger does not eat the bear.[(triple10)] The tiger does not visit the bear.[(triple15)] The tiger is blue.[(triple11 OR ((triple8) -> rule2) OR ((((triple1) -> rule5)) -> rule2))] The tiger is nice.[(triple12)] The tiger is round.[(triple13)] The tiger is young.[(triple14)] @1: The bear visits the bear.[(((triple8) -> rule3) OR ((((triple1) -> rule5)) -> rule3))] @2: The bear eats the bear.[(((((triple8) -> rule3)) -> rule7) OR ((((((triple1) -> rule5)) -> rule3)) -> rule7))]
The bear chases the tiger.
("bear" "chases" "tiger" "+")
triple1
The bear eats the tiger.
("bear" "eats" "tiger" "+")
triple2
The bear is blue.
("bear" "is" "blue" "+")
triple3
The bear is nice.
("bear" "is" "nice" "+")
triple4
The bear is not red.
("bear" "is" "red" "-")
triple5
The bear is round.
("bear" "is" "round" "+")
triple6
The bear is young.
("bear" "is" "young" "+")
triple7
The bear visits the tiger.
("bear" "visits" "tiger" "+")
triple8
((triple1) -> (rule5 % int1))
The bear visits the tiger.
("bear" "visits" "tiger" "+")
int1
The tiger chases the bear.
("tiger" "chases" "bear" "+")
triple9
The tiger does not eat the bear.
("tiger" "eats" "bear" "-")
triple10
The tiger does not visit the bear.
("tiger" "visits" "bear" "-")
triple15
The tiger is blue.
("tiger" "is" "blue" "+")
triple11
((triple8) -> (rule2 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The bear visits the tiger.
("bear" "visits" "tiger" "+")
int2
The tiger is nice.
("tiger" "is" "nice" "+")
triple12
The tiger is round.
("tiger" "is" "round" "+")
triple13
The tiger is young.
("tiger" "is" "young" "+")
triple14
The bear visits the bear.
("bear" "visits" "bear" "+")
((triple8) -> (rule3 % int1))
The bear visits the bear.
("bear" "visits" "bear" "+")
int1
((((triple1) -> (rule5 % int2))) -> (rule3 % int1))
The bear visits the bear.
("bear" "visits" "bear" "+")
int1
The bear visits the tiger.
("bear" "visits" "tiger" "+")
int2
The bear eats the bear.
("bear" "eats" "bear" "+")
((((triple8) -> (rule3 % int2))) -> (rule7 % int1))
The bear eats the bear.
("bear" "eats" "bear" "+")
int1
The bear visits the bear.
("bear" "visits" "bear" "+")
int2
((((((triple1) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The bear eats the bear.
("bear" "eats" "bear" "+")
int1
The bear visits the bear.
("bear" "visits" "bear" "+")
int2
The bear visits the tiger.
("bear" "visits" "tiger" "+")
int3