The bear needs the dog. The bear visits the dog. The dog eats the bear. The dog is not rough. The dog is young. The dog needs the bear. The dog visits the bear. If the dog visits the bear then the bear is not young. If the dog is cold then the dog does not need the bear. If something visits the dog and the dog visits the bear then it needs the bear. If something is rough and it eats the dog then it needs the bear. If something visits the bear then it visits the dog. If something needs the bear then it eats the bear.
The bear needs the dog.
("bear" "needs" "dog" "+")
The bear visits the dog.
("bear" "visits" "dog" "+")
The dog eats the bear.
("dog" "eats" "bear" "+")
The dog is not rough.
("dog" "is" "rough" "-")
The dog is young.
("dog" "is" "young" "+")
The dog needs the bear.
("dog" "needs" "bear" "+")
The dog visits the bear.
("dog" "visits" "bear" "+")
If the dog visits the bear then the bear is not young.
((("dog" "visits" "bear" "+")) -> ("bear" "is" "young" "-"))
If the dog is cold then the dog does not need the bear.
((("dog" "is" "cold" "+")) -> ("dog" "needs" "bear" "-"))
If something visits the dog and the dog visits the bear then it needs the bear.
((("something" "visits" "dog" "+") ("dog" "visits" "bear" "+")) -> ("something" "needs" "bear" "+"))
If something is rough and it eats the dog then it needs the bear.
((("something" "is" "rough" "+") ("something" "eats" "dog" "+")) -> ("something" "needs" "bear" "+"))
If something visits the bear then it visits the dog.
((("something" "visits" "bear" "+")) -> ("something" "visits" "dog" "+"))
If something needs the bear then it eats the bear.
((("something" "needs" "bear" "+")) -> ("something" "eats" "bear" "+"))
The dog is not rough.
True
1
proof
[(triple4)]
("dog" "is" "rough" "-")
triple4
The dog does not visit the bear.
False
1
inv-proof
[(triple7)]
("dog" "visits" "bear" "-")
triple7
The bear needs the bear.
True
3
proof
[(((triple2 triple7) -> rule3))]
("bear" "needs" "bear" "+")
((triple2 triple7) -> (rule3 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The bear does not need the bear.
False
3
inv-proof
[(((triple2 triple7) -> rule3))]
("bear" "needs" "bear" "-")
((triple2 triple7) -> (rule3 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The bear eats the bear.
True
4
proof
[(((((triple2 triple7) -> rule3)) -> rule6))]
("bear" "eats" "bear" "+")
((((triple2 triple7) -> (rule3 % int2))) -> (rule6 % int1))
The bear eats the bear.
("bear" "eats" "bear" "+")
int1
The bear needs the bear.
("bear" "needs" "bear" "+")
int2
The bear does not eat the bear.
False
4
inv-proof
[(((((triple2 triple7) -> rule3)) -> rule6))]
("bear" "eats" "bear" "-")
((((triple2 triple7) -> (rule3 % int2))) -> (rule6 % int1))
The bear eats the bear.
("bear" "eats" "bear" "+")
int1
The bear needs the bear.
("bear" "needs" "bear" "+")
int2
The dog is not big.
Unknown
inv-random
[@0: The dog is big.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "big" "-")
The dog needs the dog.
Unknown
random
[@0: The dog needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "dog" "+")
The dog is not cold.
Unknown
inv-random
[@0: The dog is cold.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "cold" "-")
The bear is nice.
Unknown
random
[@0: The bear is nice.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "nice" "+")
The dog is not nice.
Unknown
inv-random
[@0: The dog is nice.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "nice" "-")
The bear is rough.
Unknown
random
[@0: The bear is rough.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "rough" "+")
@0: The bear needs the dog.[(triple1)] The bear visits the dog.[(triple2)] The dog eats the bear.[(triple3 OR ((triple6) -> rule6) OR ((((((triple7) -> rule5) triple7) -> rule3)) -> rule6))] The dog is not rough.[(triple4)] The dog is young.[(triple5)] The dog needs the bear.[(triple6 OR ((((triple7) -> rule5) triple7) -> rule3))] The dog visits the bear.[(triple7)] @1: The bear is not young.[(((triple7) -> rule1))] The bear needs the bear.[(((triple2 triple7) -> rule3))] The dog visits the dog.[(((triple7) -> rule5))] @2: The bear eats the bear.[(((((triple2 triple7) -> rule3)) -> rule6))]
The bear needs the dog.
("bear" "needs" "dog" "+")
triple1
The bear visits the dog.
("bear" "visits" "dog" "+")
triple2
The dog eats the bear.
("dog" "eats" "bear" "+")
triple3
((triple6) -> (rule6 % int1))
The dog eats the bear.
("dog" "eats" "bear" "+")
int1
((((((triple7) -> (rule5 % int3)) triple7) -> (rule3 % int2))) -> (rule6 % int1))
The dog eats the bear.
("dog" "eats" "bear" "+")
int1
The dog needs the bear.
("dog" "needs" "bear" "+")
int2
The dog visits the dog.
("dog" "visits" "dog" "+")
int3
The dog is not rough.
("dog" "is" "rough" "-")
triple4
The dog is young.
("dog" "is" "young" "+")
triple5
The dog needs the bear.
("dog" "needs" "bear" "+")
triple6
((((triple7) -> (rule5 % int2)) triple7) -> (rule3 % int1))
The dog needs the bear.
("dog" "needs" "bear" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
int2
The dog visits the bear.
("dog" "visits" "bear" "+")
triple7
The bear is not young.
("bear" "is" "young" "-")
((triple7) -> (rule1 % int1))
The bear is not young.
("bear" "is" "young" "-")
int1
The bear needs the bear.
("bear" "needs" "bear" "+")
((triple2 triple7) -> (rule3 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
((triple7) -> (rule5 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The bear eats the bear.
("bear" "eats" "bear" "+")
((((triple2 triple7) -> (rule3 % int2))) -> (rule6 % int1))
The bear eats the bear.
("bear" "eats" "bear" "+")
int1
The bear needs the bear.
("bear" "needs" "bear" "+")
int2