The bear visits the dog. The dog does not chase the bear. The dog eats the bear. If something visits the dog then it visits the bear. If something visits the dog and the dog eats the bear then the dog is rough. If something visits the bear and it does not eat the bear then the bear does not chase the dog. If something eats the dog and it eats the bear then it chases the bear. If something is rough then it visits the dog. If something eats the bear then the bear visits the dog.
The bear visits the dog.
("bear" "visits" "dog" "+")
The dog does not chase the bear.
("dog" "chases" "bear" "-")
The dog eats the bear.
("dog" "eats" "bear" "+")
If something visits the dog then it visits the bear.
((("something" "visits" "dog" "+")) -> ("something" "visits" "bear" "+"))
If something visits the dog and the dog eats the bear then the dog is rough.
((("something" "visits" "dog" "+") ("dog" "eats" "bear" "+")) -> ("dog" "is" "rough" "+"))
If something visits the bear and it does not eat the bear then the bear does not chase the dog.
((("something" "visits" "bear" "+") ("something" "eats" "bear" "~")) -> ("bear" "chases" "dog" "-"))
If something eats the dog and it eats the bear then it chases the bear.
((("something" "eats" "dog" "+") ("something" "eats" "bear" "+")) -> ("something" "chases" "bear" "+"))
If something is rough then it visits the dog.
((("something" "is" "rough" "+")) -> ("something" "visits" "dog" "+"))
If something eats the bear then the bear visits the dog.
((("something" "eats" "bear" "+")) -> ("bear" "visits" "dog" "+"))
The dog does not chase the bear.
True
1
proof
[(triple2)]
("dog" "chases" "bear" "-")
triple2
The dog does not eat the bear.
False
1
inv-proof
[(triple3)]
("dog" "eats" "bear" "-")
triple3
The bear visits the bear.
True
2
proof
[(((triple1) -> rule1) OR ((((triple3) -> rule6)) -> rule1))]
("bear" "visits" "bear" "+")
((triple1) -> (rule1 % int1))
The bear visits the bear.
("bear" "visits" "bear" "+")
int1
((((triple3) -> (rule6 % int2))) -> (rule1 % int1))
The bear visits the bear.
("bear" "visits" "bear" "+")
int1
The bear visits the dog.
("bear" "visits" "dog" "+")
int2
The dog is not rough.
False
3
inv-proof
[(((triple1 triple3) -> rule2) OR ((((triple3) -> rule6) triple3) -> rule2))]
("dog" "is" "rough" "-")
((triple1 triple3) -> (rule2 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
((((triple3) -> (rule6 % int2)) triple3) -> (rule2 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The bear visits the dog.
("bear" "visits" "dog" "+")
int2
The dog visits the dog.
True
4
proof
[(((((triple1 triple3) -> rule2)) -> rule5) OR ((((((triple3) -> rule6) triple3) -> rule2)) -> rule5))]
("dog" "visits" "dog" "+")
((((triple1 triple3) -> (rule2 % int2))) -> (rule5 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog is rough.
("dog" "is" "rough" "+")
int2
((((((triple3) -> (rule6 % int3)) triple3) -> (rule2 % int2))) -> (rule5 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog is rough.
("dog" "is" "rough" "+")
int2
The bear visits the dog.
("bear" "visits" "dog" "+")
int3
The dog does not visit the dog.
False
4
inv-proof
[(((((triple1 triple3) -> rule2)) -> rule5) OR ((((((triple3) -> rule6) triple3) -> rule2)) -> rule5))]
("dog" "visits" "dog" "-")
((((triple1 triple3) -> (rule2 % int2))) -> (rule5 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog is rough.
("dog" "is" "rough" "+")
int2
((((((triple3) -> (rule6 % int3)) triple3) -> (rule2 % int2))) -> (rule5 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog is rough.
("dog" "is" "rough" "+")
int2
The bear visits the dog.
("bear" "visits" "dog" "+")
int3
The dog visits the bear.
True
5
proof
[(((((((triple1 triple3) -> rule2)) -> rule5)) -> rule1) OR ((((((((triple3) -> rule6) triple3) -> rule2)) -> rule5)) -> rule1))]
("dog" "visits" "bear" "+")
((((((triple1 triple3) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The dog visits the bear.
("dog" "visits" "bear" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
int2
The dog is rough.
("dog" "is" "rough" "+")
int3
((((((((triple3) -> (rule6 % int4)) triple3) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The dog visits the bear.
("dog" "visits" "bear" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
int2
The dog is rough.
("dog" "is" "rough" "+")
int3
The bear visits the dog.
("bear" "visits" "dog" "+")
int4
The dog does not visit the bear.
False
5
inv-proof
[(((((((triple1 triple3) -> rule2)) -> rule5)) -> rule1) OR ((((((((triple3) -> rule6) triple3) -> rule2)) -> rule5)) -> rule1))]
("dog" "visits" "bear" "-")
((((((triple1 triple3) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The dog visits the bear.
("dog" "visits" "bear" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
int2
The dog is rough.
("dog" "is" "rough" "+")
int3
((((((((triple3) -> (rule6 % int4)) triple3) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The dog visits the bear.
("dog" "visits" "bear" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
int2
The dog is rough.
("dog" "is" "rough" "+")
int3
The bear visits the dog.
("bear" "visits" "dog" "+")
int4
The bear does not chase the bear.
Unknown
inv-rconc
[@1: The bear chases the bear.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bear" "chases" "bear" "-")
The bear is big.
Unknown
random
[@0: The bear is big.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "big" "+")
The bear is not kind.
Unknown
inv-random
[@0: The bear is kind.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "kind" "-")
The dog eats the dog.
Unknown
random
[@0: The dog eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "dog" "+")
The dog is not kind.
Unknown
inv-random
[@0: The dog is kind.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "kind" "-")
The dog chases the dog.
Unknown
random
[@0: The dog chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "dog" "+")
The bear does not eat the bear.
Unknown
inv-random
[@0: The bear eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "bear" "-")
The dog is big.
Unknown
random
[@0: The dog is big.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "big" "+")
@0: The bear visits the dog.[(triple1 OR ((triple3) -> rule6))] The dog does not chase the bear.[(triple2)] The dog eats the bear.[(triple3)] @1: The bear visits the bear.[(((triple1) -> rule1) OR ((((triple3) -> rule6)) -> rule1))] The dog is rough.[(((triple1 triple3) -> rule2) OR ((((triple3) -> rule6) triple3) -> rule2))] @2: The dog visits the dog.[(((((triple1 triple3) -> rule2)) -> rule5) OR ((((((triple3) -> rule6) triple3) -> rule2)) -> rule5))] @3: The dog visits the bear.[(((((((triple1 triple3) -> rule2)) -> rule5)) -> rule1) OR ((((((((triple3) -> rule6) triple3) -> rule2)) -> rule5)) -> rule1))]
The bear visits the dog.
("bear" "visits" "dog" "+")
triple1
((triple3) -> (rule6 % int1))
The bear visits the dog.
("bear" "visits" "dog" "+")
int1
The dog does not chase the bear.
("dog" "chases" "bear" "-")
triple2
The dog eats the bear.
("dog" "eats" "bear" "+")
triple3
The bear visits the bear.
("bear" "visits" "bear" "+")
((triple1) -> (rule1 % int1))
The bear visits the bear.
("bear" "visits" "bear" "+")
int1
((((triple3) -> (rule6 % int2))) -> (rule1 % int1))
The bear visits the bear.
("bear" "visits" "bear" "+")
int1
The bear visits the dog.
("bear" "visits" "dog" "+")
int2
The dog is rough.
("dog" "is" "rough" "+")
((triple1 triple3) -> (rule2 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
((((triple3) -> (rule6 % int2)) triple3) -> (rule2 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The bear visits the dog.
("bear" "visits" "dog" "+")
int2
The dog visits the dog.
("dog" "visits" "dog" "+")
((((triple1 triple3) -> (rule2 % int2))) -> (rule5 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog is rough.
("dog" "is" "rough" "+")
int2
((((((triple3) -> (rule6 % int3)) triple3) -> (rule2 % int2))) -> (rule5 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog is rough.
("dog" "is" "rough" "+")
int2
The bear visits the dog.
("bear" "visits" "dog" "+")
int3
The dog visits the bear.
("dog" "visits" "bear" "+")
((((((triple1 triple3) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The dog visits the bear.
("dog" "visits" "bear" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
int2
The dog is rough.
("dog" "is" "rough" "+")
int3
((((((((triple3) -> (rule6 % int4)) triple3) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The dog visits the bear.
("dog" "visits" "bear" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
int2
The dog is rough.
("dog" "is" "rough" "+")
int3
The bear visits the dog.
("bear" "visits" "dog" "+")
int4