The bear eats the dog. The bear is nice. The bear needs the dog. The bear visits the dog. The dog is red. The dog is round. The dog visits the bear. If someone needs the bear and the bear eats the dog then they are rough. If someone needs the dog then they eat the bear. If someone needs the dog then the dog needs the bear. If the bear needs the dog and the bear is rough then the dog is red. If the bear visits the dog and the dog eats the bear then the bear is rough. If someone visits the dog then the dog needs the bear. If someone is red and they visit the bear then they need the dog. If someone eats the dog and they visit the bear then the bear eats the dog.
The bear eats the dog.
("bear" "eats" "dog" "+")
The bear is nice.
("bear" "is" "nice" "+")
The bear needs the dog.
("bear" "needs" "dog" "+")
The bear visits the dog.
("bear" "visits" "dog" "+")
The dog is red.
("dog" "is" "red" "+")
The dog is round.
("dog" "is" "round" "+")
The dog visits the bear.
("dog" "visits" "bear" "+")
If someone needs the bear and the bear eats the dog then they are rough.
((("someone" "needs" "bear" "+") ("bear" "eats" "dog" "+")) -> ("someone" "is" "rough" "+"))
If someone needs the dog then they eat the bear.
((("someone" "needs" "dog" "+")) -> ("someone" "eats" "bear" "+"))
If someone needs the dog then the dog needs the bear.
((("someone" "needs" "dog" "+")) -> ("dog" "needs" "bear" "+"))
If the bear needs the dog and the bear is rough then the dog is red.
((("bear" "needs" "dog" "+") ("bear" "is" "rough" "+")) -> ("dog" "is" "red" "+"))
If the bear visits the dog and the dog eats the bear then the bear is rough.
((("bear" "visits" "dog" "+") ("dog" "eats" "bear" "+")) -> ("bear" "is" "rough" "+"))
If someone visits the dog then the dog needs the bear.
((("someone" "visits" "dog" "+")) -> ("dog" "needs" "bear" "+"))
If someone is red and they visit the bear then they need the dog.
((("someone" "is" "red" "+") ("someone" "visits" "bear" "+")) -> ("someone" "needs" "dog" "+"))
If someone eats the dog and they visit the bear then the bear eats the dog.
((("someone" "eats" "dog" "+") ("someone" "visits" "bear" "+")) -> ("bear" "eats" "dog" "+"))
The bear is nice.
True
1
proof
[(triple2)]
("bear" "is" "nice" "+")
triple2
The bear is not nice.
False
1
inv-proof
[(triple2)]
("bear" "is" "nice" "-")
triple2
The dog needs the bear.
True
2
proof
[(((triple3) -> rule3) OR ((triple4) -> rule6) OR ((((triple5 triple7) -> rule7)) -> rule3))]
("dog" "needs" "bear" "+")
((triple3) -> (rule3 % int1))
The dog needs the bear.
("dog" "needs" "bear" "+")
int1
((triple4) -> (rule6 % int1))
The dog needs the bear.
("dog" "needs" "bear" "+")
int1
((((triple5 triple7) -> (rule7 % int2))) -> (rule3 % int1))
The dog needs the bear.
("dog" "needs" "bear" "+")
int1
The dog needs the dog.
("dog" "needs" "dog" "+")
int2
The dog does not need the dog.
False
3
inv-proof
[(((triple5 triple7) -> rule7))]
("dog" "needs" "dog" "-")
((triple5 triple7) -> (rule7 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog eats the bear.
True
4
proof
[(((((triple5 triple7) -> rule7)) -> rule2))]
("dog" "eats" "bear" "+")
((((triple5 triple7) -> (rule7 % int2))) -> (rule2 % int1))
The dog eats the bear.
("dog" "eats" "bear" "+")
int1
The dog needs the dog.
("dog" "needs" "dog" "+")
int2
The dog is not rough.
False
4
inv-proof
[(((((triple3) -> rule3) triple1) -> rule1) OR ((((triple4) -> rule6) triple1) -> rule1) OR ((((((triple5 triple7) -> rule7)) -> rule3) triple1) -> rule1))]
("dog" "is" "rough" "-")
((((triple3) -> (rule3 % int2)) triple1) -> (rule1 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The dog needs the bear.
("dog" "needs" "bear" "+")
int2
((((triple4) -> (rule6 % int2)) triple1) -> (rule1 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The dog needs the bear.
("dog" "needs" "bear" "+")
int2
((((((triple5 triple7) -> (rule7 % int3))) -> (rule3 % int2)) triple1) -> (rule1 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The dog needs the bear.
("dog" "needs" "bear" "+")
int2
The dog needs the dog.
("dog" "needs" "dog" "+")
int3
The bear is rough.
True
6
proof
[(((triple4 ((((triple5 triple7) -> rule7)) -> rule2)) -> rule5))]
("bear" "is" "rough" "+")
((triple4 ((((triple5 triple7) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
The dog eats the bear.
("dog" "eats" "bear" "+")
int2
The dog needs the dog.
("dog" "needs" "dog" "+")
int3
The bear is not rough.
False
6
inv-proof
[(((triple4 ((((triple5 triple7) -> rule7)) -> rule2)) -> rule5))]
("bear" "is" "rough" "-")
((triple4 ((((triple5 triple7) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
The dog eats the bear.
("dog" "eats" "bear" "+")
int2
The dog needs the dog.
("dog" "needs" "dog" "+")
int3
The bear does not need the bear.
Unknown
inv-random
[@0: The bear needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "bear" "-")
The dog visits the dog.
Unknown
random
[@0: The dog visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "dog" "+")
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 dog is cold.
Unknown
random
[@0: The dog is cold.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "cold" "+")
The bear is not round.
Unknown
inv-random
[@0: The bear is round.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "round" "-")
The dog is nice.
Unknown
random
[@0: The dog is nice.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "nice" "+")
The dog does not eat the dog.
Unknown
inv-random
[@0: The dog eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "dog" "-")
The bear is red.
Unknown
random
[@0: The bear is red.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "red" "+")
@0: The bear eats the dog.[(triple1)] The bear is nice.[(triple2)] The bear needs the dog.[(triple3)] The bear visits the dog.[(triple4)] The dog is red.[(triple5)] The dog is round.[(triple6)] The dog visits the bear.[(triple7)] @1: The bear eats the bear.[(((triple3) -> rule2))] The dog needs the bear.[(((triple3) -> rule3) OR ((triple4) -> rule6) OR ((((triple5 triple7) -> rule7)) -> rule3))] The dog needs the dog.[(((triple5 triple7) -> rule7))] @2: The dog eats the bear.[(((((triple5 triple7) -> rule7)) -> rule2))] The dog is rough.[(((((triple3) -> rule3) triple1) -> rule1) OR ((((triple4) -> rule6) triple1) -> rule1) OR ((((((triple5 triple7) -> rule7)) -> rule3) triple1) -> rule1))] @3: The bear is rough.[(((triple4 ((((triple5 triple7) -> rule7)) -> rule2)) -> rule5))]
The bear eats the dog.
("bear" "eats" "dog" "+")
triple1
The bear is nice.
("bear" "is" "nice" "+")
triple2
The bear needs the dog.
("bear" "needs" "dog" "+")
triple3
The bear visits the dog.
("bear" "visits" "dog" "+")
triple4
The dog is red.
("dog" "is" "red" "+")
triple5
The dog is round.
("dog" "is" "round" "+")
triple6
The dog visits the bear.
("dog" "visits" "bear" "+")
triple7
The bear eats the bear.
("bear" "eats" "bear" "+")
((triple3) -> (rule2 % int1))
The bear eats the bear.
("bear" "eats" "bear" "+")
int1
The dog needs the bear.
("dog" "needs" "bear" "+")
((triple3) -> (rule3 % int1))
The dog needs the bear.
("dog" "needs" "bear" "+")
int1
((triple4) -> (rule6 % int1))
The dog needs the bear.
("dog" "needs" "bear" "+")
int1
((((triple5 triple7) -> (rule7 % int2))) -> (rule3 % int1))
The dog needs the bear.
("dog" "needs" "bear" "+")
int1
The dog needs the dog.
("dog" "needs" "dog" "+")
int2
The dog needs the dog.
("dog" "needs" "dog" "+")
((triple5 triple7) -> (rule7 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog eats the bear.
("dog" "eats" "bear" "+")
((((triple5 triple7) -> (rule7 % int2))) -> (rule2 % int1))
The dog eats the bear.
("dog" "eats" "bear" "+")
int1
The dog needs the dog.
("dog" "needs" "dog" "+")
int2
The dog is rough.
("dog" "is" "rough" "+")
((((triple3) -> (rule3 % int2)) triple1) -> (rule1 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The dog needs the bear.
("dog" "needs" "bear" "+")
int2
((((triple4) -> (rule6 % int2)) triple1) -> (rule1 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The dog needs the bear.
("dog" "needs" "bear" "+")
int2
((((((triple5 triple7) -> (rule7 % int3))) -> (rule3 % int2)) triple1) -> (rule1 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The dog needs the bear.
("dog" "needs" "bear" "+")
int2
The dog needs the dog.
("dog" "needs" "dog" "+")
int3
The bear is rough.
("bear" "is" "rough" "+")
((triple4 ((((triple5 triple7) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
The dog eats the bear.
("dog" "eats" "bear" "+")
int2
The dog needs the dog.
("dog" "needs" "dog" "+")
int3