The bear chases the tiger. The bear is big. The bear is blue. The bear likes the tiger. The bear visits the cat. The cat chases the bear. The cat chases the tiger. The cat is blue. The cat is cold. The cat visits the bear. The tiger is blue. The tiger is green. The tiger is rough. The tiger likes the cat. The tiger visits the bear. If the bear is rough and the bear likes the tiger then the bear likes the cat. If the bear visits the tiger and the tiger visits the bear then the bear likes the cat. If something likes the bear then the bear visits the tiger. If the cat is green and the cat likes the tiger then the tiger is green. If something is blue then it likes the bear. If something chases the tiger then it visits the bear.
The bear chases the tiger.
("bear" "chases" "tiger" "+")
The bear is big.
("bear" "is" "big" "+")
The bear is blue.
("bear" "is" "blue" "+")
The bear likes the tiger.
("bear" "likes" "tiger" "+")
The bear visits the cat.
("bear" "visits" "cat" "+")
The cat chases the bear.
("cat" "chases" "bear" "+")
The cat chases the tiger.
("cat" "chases" "tiger" "+")
The cat is blue.
("cat" "is" "blue" "+")
The cat is cold.
("cat" "is" "cold" "+")
The cat visits the bear.
("cat" "visits" "bear" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger likes the cat.
("tiger" "likes" "cat" "+")
The tiger visits the bear.
("tiger" "visits" "bear" "+")
If the bear is rough and the bear likes the tiger then the bear likes the cat.
((("bear" "is" "rough" "+") ("bear" "likes" "tiger" "+")) -> ("bear" "likes" "cat" "+"))
If the bear visits the tiger and the tiger visits the bear then the bear likes the cat.
((("bear" "visits" "tiger" "+") ("tiger" "visits" "bear" "+")) -> ("bear" "likes" "cat" "+"))
If something likes the bear then the bear visits the tiger.
((("something" "likes" "bear" "+")) -> ("bear" "visits" "tiger" "+"))
If the cat is green and the cat likes the tiger then the tiger is green.
((("cat" "is" "green" "+") ("cat" "likes" "tiger" "+")) -> ("tiger" "is" "green" "+"))
If something is blue then it likes the bear.
((("something" "is" "blue" "+")) -> ("something" "likes" "bear" "+"))
If something chases the tiger then it visits the bear.
((("something" "chases" "tiger" "+")) -> ("something" "visits" "bear" "+"))
The tiger is rough.
True
1
proof
[(triple13)]
("tiger" "is" "rough" "+")
triple13
The cat does not chase the tiger.
False
1
inv-proof
[(triple7)]
("cat" "chases" "tiger" "-")
triple7
The bear likes the bear.
True
2
proof
[(((triple3) -> rule5))]
("bear" "likes" "bear" "+")
((triple3) -> (rule5 % int1))
The bear likes the bear.
("bear" "likes" "bear" "+")
int1
The bear does not visit the bear.
False
2
inv-proof
[(((triple1) -> rule6))]
("bear" "visits" "bear" "-")
((triple1) -> (rule6 % int1))
The bear visits the bear.
("bear" "visits" "bear" "+")
int1
The bear visits the tiger.
True
3
proof
[(((((triple11) -> rule5)) -> rule3) OR ((((triple3) -> rule5)) -> rule3) OR ((((triple8) -> rule5)) -> rule3))]
("bear" "visits" "tiger" "+")
((((triple11) -> (rule5 % int2))) -> (rule3 % int1))
The bear visits the tiger.
("bear" "visits" "tiger" "+")
int1
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int2
((((triple3) -> (rule5 % int2))) -> (rule3 % int1))
The bear visits the tiger.
("bear" "visits" "tiger" "+")
int1
The bear likes the bear.
("bear" "likes" "bear" "+")
int2
((((triple8) -> (rule5 % int2))) -> (rule3 % int1))
The bear visits the tiger.
("bear" "visits" "tiger" "+")
int1
The cat likes the bear.
("cat" "likes" "bear" "+")
int2
The bear does not visit the tiger.
False
3
inv-proof
[(((((triple11) -> rule5)) -> rule3) OR ((((triple3) -> rule5)) -> rule3) OR ((((triple8) -> rule5)) -> rule3))]
("bear" "visits" "tiger" "-")
((((triple11) -> (rule5 % int2))) -> (rule3 % int1))
The bear visits the tiger.
("bear" "visits" "tiger" "+")
int1
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int2
((((triple3) -> (rule5 % int2))) -> (rule3 % int1))
The bear visits the tiger.
("bear" "visits" "tiger" "+")
int1
The bear likes the bear.
("bear" "likes" "bear" "+")
int2
((((triple8) -> (rule5 % int2))) -> (rule3 % int1))
The bear visits the tiger.
("bear" "visits" "tiger" "+")
int1
The cat likes the bear.
("cat" "likes" "bear" "+")
int2
The bear likes the cat.
True
5
proof
[(((((((triple11) -> rule5)) -> rule3) triple15) -> rule2) OR ((((((triple3) -> rule5)) -> rule3) triple15) -> rule2) OR ((((((triple8) -> rule5)) -> rule3) triple15) -> rule2))]
("bear" "likes" "cat" "+")
((((((triple11) -> (rule5 % int3))) -> (rule3 % int2)) triple15) -> (rule2 % int1))
The bear likes the cat.
("bear" "likes" "cat" "+")
int1
The bear visits the tiger.
("bear" "visits" "tiger" "+")
int2
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int3
((((((triple3) -> (rule5 % int3))) -> (rule3 % int2)) triple15) -> (rule2 % int1))
The bear likes the cat.
("bear" "likes" "cat" "+")
int1
The bear visits the tiger.
("bear" "visits" "tiger" "+")
int2
The bear likes the bear.
("bear" "likes" "bear" "+")
int3
((((((triple8) -> (rule5 % int3))) -> (rule3 % int2)) triple15) -> (rule2 % int1))
The bear likes the cat.
("bear" "likes" "cat" "+")
int1
The bear visits the tiger.
("bear" "visits" "tiger" "+")
int2
The cat likes the bear.
("cat" "likes" "bear" "+")
int3
The bear does not like the cat.
False
5
inv-proof
[(((((((triple11) -> rule5)) -> rule3) triple15) -> rule2) OR ((((((triple3) -> rule5)) -> rule3) triple15) -> rule2) OR ((((((triple8) -> rule5)) -> rule3) triple15) -> rule2))]
("bear" "likes" "cat" "-")
((((((triple11) -> (rule5 % int3))) -> (rule3 % int2)) triple15) -> (rule2 % int1))
The bear likes the cat.
("bear" "likes" "cat" "+")
int1
The bear visits the tiger.
("bear" "visits" "tiger" "+")
int2
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int3
((((((triple3) -> (rule5 % int3))) -> (rule3 % int2)) triple15) -> (rule2 % int1))
The bear likes the cat.
("bear" "likes" "cat" "+")
int1
The bear visits the tiger.
("bear" "visits" "tiger" "+")
int2
The bear likes the bear.
("bear" "likes" "bear" "+")
int3
((((((triple8) -> (rule5 % int3))) -> (rule3 % int2)) triple15) -> (rule2 % int1))
The bear likes the cat.
("bear" "likes" "cat" "+")
int1
The bear visits the tiger.
("bear" "visits" "tiger" "+")
int2
The cat likes the bear.
("cat" "likes" "bear" "+")
int3
The tiger is not cold.
Unknown
inv-random
[@0: The tiger is cold.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "cold" "-")
The tiger likes the tiger.
Unknown
random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "+")
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 chases the tiger.
Unknown
random
[@0: The tiger chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "tiger" "+")
The bear is not green.
Unknown
inv-random
[@0: The bear is green.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "green" "-")
The bear is cold.
Unknown
random
[@0: The bear is cold.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "cold" "+")
The cat is not big.
Unknown
inv-random
[@0: The cat is big.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "big" "-")
The cat visits the cat.
Unknown
random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "+")
@0: The bear chases the tiger.[(triple1)] The bear is big.[(triple2)] The bear is blue.[(triple3)] The bear likes the tiger.[(triple4)] The bear visits the cat.[(triple5)] The cat chases the bear.[(triple6)] The cat chases the tiger.[(triple7)] The cat is blue.[(triple8)] The cat is cold.[(triple9)] The cat visits the bear.[(triple10 OR ((triple7) -> rule6))] The tiger is blue.[(triple11)] The tiger is green.[(triple12)] The tiger is rough.[(triple13)] The tiger likes the cat.[(triple14)] The tiger visits the bear.[(triple15)] @1: The bear likes the bear.[(((triple3) -> rule5))] The bear visits the bear.[(((triple1) -> rule6))] The cat likes the bear.[(((triple8) -> rule5))] The tiger likes the bear.[(((triple11) -> rule5))] @2: The bear visits the tiger.[(((((triple11) -> rule5)) -> rule3) OR ((((triple3) -> rule5)) -> rule3) OR ((((triple8) -> rule5)) -> rule3))] @3: The bear likes the cat.[(((((((triple11) -> rule5)) -> rule3) triple15) -> rule2) OR ((((((triple3) -> rule5)) -> rule3) triple15) -> rule2) OR ((((((triple8) -> rule5)) -> rule3) triple15) -> rule2))]
The bear chases the tiger.
("bear" "chases" "tiger" "+")
triple1
The bear is big.
("bear" "is" "big" "+")
triple2
The bear is blue.
("bear" "is" "blue" "+")
triple3
The bear likes the tiger.
("bear" "likes" "tiger" "+")
triple4
The bear visits the cat.
("bear" "visits" "cat" "+")
triple5
The cat chases the bear.
("cat" "chases" "bear" "+")
triple6
The cat chases the tiger.
("cat" "chases" "tiger" "+")
triple7
The cat is blue.
("cat" "is" "blue" "+")
triple8
The cat is cold.
("cat" "is" "cold" "+")
triple9
The cat visits the bear.
("cat" "visits" "bear" "+")
triple10
((triple7) -> (rule6 % int1))
The cat visits the bear.
("cat" "visits" "bear" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
triple11
The tiger is green.
("tiger" "is" "green" "+")
triple12
The tiger is rough.
("tiger" "is" "rough" "+")
triple13
The tiger likes the cat.
("tiger" "likes" "cat" "+")
triple14
The tiger visits the bear.
("tiger" "visits" "bear" "+")
triple15
The bear likes the bear.
("bear" "likes" "bear" "+")
((triple3) -> (rule5 % int1))
The bear likes the bear.
("bear" "likes" "bear" "+")
int1
The bear visits the bear.
("bear" "visits" "bear" "+")
((triple1) -> (rule6 % int1))
The bear visits the bear.
("bear" "visits" "bear" "+")
int1
The cat likes the bear.
("cat" "likes" "bear" "+")
((triple8) -> (rule5 % int1))
The cat likes the bear.
("cat" "likes" "bear" "+")
int1
The tiger likes the bear.
("tiger" "likes" "bear" "+")
((triple11) -> (rule5 % int1))
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int1
The bear visits the tiger.
("bear" "visits" "tiger" "+")
((((triple11) -> (rule5 % int2))) -> (rule3 % int1))
The bear visits the tiger.
("bear" "visits" "tiger" "+")
int1
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int2
((((triple3) -> (rule5 % int2))) -> (rule3 % int1))
The bear visits the tiger.
("bear" "visits" "tiger" "+")
int1
The bear likes the bear.
("bear" "likes" "bear" "+")
int2
((((triple8) -> (rule5 % int2))) -> (rule3 % int1))
The bear visits the tiger.
("bear" "visits" "tiger" "+")
int1
The cat likes the bear.
("cat" "likes" "bear" "+")
int2
The bear likes the cat.
("bear" "likes" "cat" "+")
((((((triple11) -> (rule5 % int3))) -> (rule3 % int2)) triple15) -> (rule2 % int1))
The bear likes the cat.
("bear" "likes" "cat" "+")
int1
The bear visits the tiger.
("bear" "visits" "tiger" "+")
int2
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int3
((((((triple3) -> (rule5 % int3))) -> (rule3 % int2)) triple15) -> (rule2 % int1))
The bear likes the cat.
("bear" "likes" "cat" "+")
int1
The bear visits the tiger.
("bear" "visits" "tiger" "+")
int2
The bear likes the bear.
("bear" "likes" "bear" "+")
int3
((((((triple8) -> (rule5 % int3))) -> (rule3 % int2)) triple15) -> (rule2 % int1))
The bear likes the cat.
("bear" "likes" "cat" "+")
int1
The bear visits the tiger.
("bear" "visits" "tiger" "+")
int2
The cat likes the bear.
("cat" "likes" "bear" "+")
int3