The bear chases the cat. The bear is big. The bear is blue. The bear is kind. The bear is rough. The bear likes the cat. The bear visits the cat. The cat chases the bear. The cat is red. The cat is rough. The cat likes the bear. The cat visits the bear. If the bear is blue and the bear chases the cat then the bear visits the cat. If something is kind then it likes the bear. If something chases the bear and the bear chases the cat then it chases the cat. If the cat visits the bear then the bear is blue. If the bear chases the cat and the cat is rough then the cat is kind. If the bear likes the cat then the bear is red. If something likes the cat and it is big then the cat is blue. If something visits the cat and it likes the bear then the bear likes the cat.
The bear chases the cat.
("bear" "chases" "cat" "+")
The bear is big.
("bear" "is" "big" "+")
The bear is blue.
("bear" "is" "blue" "+")
The bear is kind.
("bear" "is" "kind" "+")
The bear is rough.
("bear" "is" "rough" "+")
The bear likes the cat.
("bear" "likes" "cat" "+")
The bear visits the cat.
("bear" "visits" "cat" "+")
The cat chases the bear.
("cat" "chases" "bear" "+")
The cat is red.
("cat" "is" "red" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat likes the bear.
("cat" "likes" "bear" "+")
The cat visits the bear.
("cat" "visits" "bear" "+")
If the bear is blue and the bear chases the cat then the bear visits the cat.
((("bear" "is" "blue" "+") ("bear" "chases" "cat" "+")) -> ("bear" "visits" "cat" "+"))
If something is kind then it likes the bear.
((("something" "is" "kind" "+")) -> ("something" "likes" "bear" "+"))
If something chases the bear and the bear chases the cat then it chases the cat.
((("something" "chases" "bear" "+") ("bear" "chases" "cat" "+")) -> ("something" "chases" "cat" "+"))
If the cat visits the bear then the bear is blue.
((("cat" "visits" "bear" "+")) -> ("bear" "is" "blue" "+"))
If the bear chases the cat and the cat is rough then the cat is kind.
((("bear" "chases" "cat" "+") ("cat" "is" "rough" "+")) -> ("cat" "is" "kind" "+"))
If the bear likes the cat then the bear is red.
((("bear" "likes" "cat" "+")) -> ("bear" "is" "red" "+"))
If something likes the cat and it is big then the cat is blue.
((("something" "likes" "cat" "+") ("something" "is" "big" "+")) -> ("cat" "is" "blue" "+"))
If something visits the cat and it likes the bear then the bear likes the cat.
((("something" "visits" "cat" "+") ("something" "likes" "bear" "+")) -> ("bear" "likes" "cat" "+"))
The bear is rough.
True
1
proof
[(triple5)]
("bear" "is" "rough" "+")
triple5
The bear is not kind.
False
1
inv-proof
[(triple4)]
("bear" "is" "kind" "-")
triple4
The cat is blue.
True
3
proof
[(((triple6 triple2) -> rule7) OR ((((triple7 ((triple4) -> rule2)) -> rule8) triple2) -> rule7) OR ((((((triple3 triple1) -> rule1) ((triple4) -> rule2)) -> rule8) triple2) -> rule7) OR ((((((((triple12) -> rule4) triple1) -> rule1) ((triple4) -> rule2)) -> rule8) triple2) -> rule7))]
("cat" "is" "blue" "+")
((triple6 triple2) -> (rule7 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
((((triple7 ((triple4) -> (rule2 % int3))) -> (rule8 % int2)) triple2) -> (rule7 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The bear likes the cat.
("bear" "likes" "cat" "+")
int2
The bear likes the bear.
("bear" "likes" "bear" "+")
int3
((((((triple3 triple1) -> (rule1 % int4)) ((triple4) -> (rule2 % int3))) -> (rule8 % int2)) triple2) -> (rule7 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The bear likes the cat.
("bear" "likes" "cat" "+")
int2
The bear likes the bear.
("bear" "likes" "bear" "+")
int3
The bear visits the cat.
("bear" "visits" "cat" "+")
int4
((((((((triple12) -> (rule4 % int5)) triple1) -> (rule1 % int4)) ((triple4) -> (rule2 % int3))) -> (rule8 % int2)) triple2) -> (rule7 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The bear likes the cat.
("bear" "likes" "cat" "+")
int2
The bear likes the bear.
("bear" "likes" "bear" "+")
int3
The bear visits the cat.
("bear" "visits" "cat" "+")
int4
The bear is blue.
("bear" "is" "blue" "+")
int5
The cat does not chase the cat.
False
3
inv-proof
[(((triple8 triple1) -> rule3))]
("cat" "chases" "cat" "-")
((triple8 triple1) -> (rule3 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The bear does not visit the bear.
Unknown
inv-random
[@0: The bear visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "bear" "-")
The bear chases the bear.
Unknown
random
[@0: The bear chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "bear" "+")
The cat does not visit the cat.
Unknown
inv-random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "-")
The cat is big.
Unknown
random
[@0: The cat is big.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "big" "+")
@0: The bear chases the cat.[(triple1)] The bear is big.[(triple2)] The bear is blue.[(triple3 OR ((triple12) -> rule4))] The bear is kind.[(triple4)] The bear is rough.[(triple5)] The bear likes the cat.[(triple6 OR ((triple7 ((triple4) -> rule2)) -> rule8) OR ((((triple3 triple1) -> rule1) ((triple4) -> rule2)) -> rule8) OR ((((((triple12) -> rule4) triple1) -> rule1) ((triple4) -> rule2)) -> rule8))] The bear visits the cat.[(triple7 OR ((triple3 triple1) -> rule1) OR ((((triple12) -> rule4) triple1) -> rule1))] The cat chases the bear.[(triple8)] The cat is red.[(triple9)] The cat is rough.[(triple10)] The cat likes the bear.[(triple11 OR ((((triple1 triple10) -> rule5)) -> rule2))] The cat visits the bear.[(triple12)] @1: The bear is red.[(((triple6) -> rule6) OR ((((triple7 ((triple4) -> rule2)) -> rule8)) -> rule6) OR ((((((triple3 triple1) -> rule1) ((triple4) -> rule2)) -> rule8)) -> rule6) OR ((((((((triple12) -> rule4) triple1) -> rule1) ((triple4) -> rule2)) -> rule8)) -> rule6))] The bear likes the bear.[(((triple4) -> rule2))] The cat chases the cat.[(((triple8 triple1) -> rule3))] The cat is blue.[(((triple6 triple2) -> rule7) OR ((((triple7 ((triple4) -> rule2)) -> rule8) triple2) -> rule7) OR ((((((triple3 triple1) -> rule1) ((triple4) -> rule2)) -> rule8) triple2) -> rule7) OR ((((((((triple12) -> rule4) triple1) -> rule1) ((triple4) -> rule2)) -> rule8) triple2) -> rule7))] The cat is kind.[(((triple1 triple10) -> rule5))]
The bear chases the cat.
("bear" "chases" "cat" "+")
triple1
The bear is big.
("bear" "is" "big" "+")
triple2
The bear is blue.
("bear" "is" "blue" "+")
triple3
((triple12) -> (rule4 % int1))
The bear is blue.
("bear" "is" "blue" "+")
int1
The bear is kind.
("bear" "is" "kind" "+")
triple4
The bear is rough.
("bear" "is" "rough" "+")
triple5
The bear likes the cat.
("bear" "likes" "cat" "+")
triple6
((triple7 ((triple4) -> (rule2 % int2))) -> (rule8 % int1))
The bear likes the cat.
("bear" "likes" "cat" "+")
int1
The bear likes the bear.
("bear" "likes" "bear" "+")
int2
((((triple3 triple1) -> (rule1 % int3)) ((triple4) -> (rule2 % int2))) -> (rule8 % int1))
The bear likes the cat.
("bear" "likes" "cat" "+")
int1
The bear likes the bear.
("bear" "likes" "bear" "+")
int2
The bear visits the cat.
("bear" "visits" "cat" "+")
int3
((((((triple12) -> (rule4 % int4)) triple1) -> (rule1 % int3)) ((triple4) -> (rule2 % int2))) -> (rule8 % int1))
The bear likes the cat.
("bear" "likes" "cat" "+")
int1
The bear likes the bear.
("bear" "likes" "bear" "+")
int2
The bear visits the cat.
("bear" "visits" "cat" "+")
int3
The bear is blue.
("bear" "is" "blue" "+")
int4
The bear visits the cat.
("bear" "visits" "cat" "+")
triple7
((triple3 triple1) -> (rule1 % int1))
The bear visits the cat.
("bear" "visits" "cat" "+")
int1
((((triple12) -> (rule4 % int2)) triple1) -> (rule1 % int1))
The bear visits the cat.
("bear" "visits" "cat" "+")
int1
The bear is blue.
("bear" "is" "blue" "+")
int2
The cat chases the bear.
("cat" "chases" "bear" "+")
triple8
The cat is red.
("cat" "is" "red" "+")
triple9
The cat is rough.
("cat" "is" "rough" "+")
triple10
The cat likes the bear.
("cat" "likes" "bear" "+")
triple11
((((triple1 triple10) -> (rule5 % int2))) -> (rule2 % int1))
The cat likes the bear.
("cat" "likes" "bear" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
The cat visits the bear.
("cat" "visits" "bear" "+")
triple12
The bear is red.
("bear" "is" "red" "+")
((triple6) -> (rule6 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
((((triple7 ((triple4) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The bear likes the cat.
("bear" "likes" "cat" "+")
int2
The bear likes the bear.
("bear" "likes" "bear" "+")
int3
((((((triple3 triple1) -> (rule1 % int4)) ((triple4) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The bear likes the cat.
("bear" "likes" "cat" "+")
int2
The bear likes the bear.
("bear" "likes" "bear" "+")
int3
The bear visits the cat.
("bear" "visits" "cat" "+")
int4
((((((((triple12) -> (rule4 % int5)) triple1) -> (rule1 % int4)) ((triple4) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The bear likes the cat.
("bear" "likes" "cat" "+")
int2
The bear likes the bear.
("bear" "likes" "bear" "+")
int3
The bear visits the cat.
("bear" "visits" "cat" "+")
int4
The bear is blue.
("bear" "is" "blue" "+")
int5
The bear likes the bear.
("bear" "likes" "bear" "+")
((triple4) -> (rule2 % int1))
The bear likes the bear.
("bear" "likes" "bear" "+")
int1
The cat chases the cat.
("cat" "chases" "cat" "+")
((triple8 triple1) -> (rule3 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat is blue.
("cat" "is" "blue" "+")
((triple6 triple2) -> (rule7 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
((((triple7 ((triple4) -> (rule2 % int3))) -> (rule8 % int2)) triple2) -> (rule7 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The bear likes the cat.
("bear" "likes" "cat" "+")
int2
The bear likes the bear.
("bear" "likes" "bear" "+")
int3
((((((triple3 triple1) -> (rule1 % int4)) ((triple4) -> (rule2 % int3))) -> (rule8 % int2)) triple2) -> (rule7 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The bear likes the cat.
("bear" "likes" "cat" "+")
int2
The bear likes the bear.
("bear" "likes" "bear" "+")
int3
The bear visits the cat.
("bear" "visits" "cat" "+")
int4
((((((((triple12) -> (rule4 % int5)) triple1) -> (rule1 % int4)) ((triple4) -> (rule2 % int3))) -> (rule8 % int2)) triple2) -> (rule7 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The bear likes the cat.
("bear" "likes" "cat" "+")
int2
The bear likes the bear.
("bear" "likes" "bear" "+")
int3
The bear visits the cat.
("bear" "visits" "cat" "+")
int4
The bear is blue.
("bear" "is" "blue" "+")
int5
The cat is kind.
("cat" "is" "kind" "+")
((triple1 triple10) -> (rule5 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1