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