The bear is big. The dog is red. The lion sees the mouse. The mouse eats the dog. If someone is big then they like the dog. If someone is rough then they eat the mouse. If someone eats the lion then they see the mouse. If the dog likes the mouse then the mouse is red. If the dog eats the lion then the dog eats the mouse. If someone likes the dog then they are nice. If someone is nice then they see the bear. If someone is rough and they see the bear then they like the bear.
The bear is big.
("bear" "is" "big" "+")
The dog is red.
("dog" "is" "red" "+")
The lion sees the mouse.
("lion" "sees" "mouse" "+")
The mouse eats the dog.
("mouse" "eats" "dog" "+")
If someone is big then they like the dog.
((("someone" "is" "big" "+")) -> ("someone" "likes" "dog" "+"))
If someone is rough then they eat the mouse.
((("someone" "is" "rough" "+")) -> ("someone" "eats" "mouse" "+"))
If someone eats the lion then they see the mouse.
((("someone" "eats" "lion" "+")) -> ("someone" "sees" "mouse" "+"))
If the dog likes the mouse then the mouse is red.
((("dog" "likes" "mouse" "+")) -> ("mouse" "is" "red" "+"))
If the dog eats the lion then the dog eats the mouse.
((("dog" "eats" "lion" "+")) -> ("dog" "eats" "mouse" "+"))
If someone likes the dog then they are nice.
((("someone" "likes" "dog" "+")) -> ("someone" "is" "nice" "+"))
If someone is nice then they see the bear.
((("someone" "is" "nice" "+")) -> ("someone" "sees" "bear" "+"))
If someone is rough and they see the bear then they like the bear.
((("someone" "is" "rough" "+") ("someone" "sees" "bear" "+")) -> ("someone" "likes" "bear" "+"))
The lion sees the mouse.
True
1
proof
[(triple3)]
("lion" "sees" "mouse" "+")
triple3
The dog is not red.
False
1
inv-proof
[(triple2)]
("dog" "is" "red" "-")
triple2
The bear likes the dog.
True
2
proof
[(((triple1) -> rule1))]
("bear" "likes" "dog" "+")
((triple1) -> (rule1 % int1))
The bear likes the dog.
("bear" "likes" "dog" "+")
int1
The bear does not like the dog.
False
2
inv-proof
[(((triple1) -> rule1))]
("bear" "likes" "dog" "-")
((triple1) -> (rule1 % int1))
The bear likes the dog.
("bear" "likes" "dog" "+")
int1
The bear is nice.
True
3
proof
[(((((triple1) -> rule1)) -> rule6))]
("bear" "is" "nice" "+")
((((triple1) -> (rule1 % int2))) -> (rule6 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear likes the dog.
("bear" "likes" "dog" "+")
int2
The bear is not nice.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule6))]
("bear" "is" "nice" "-")
((((triple1) -> (rule1 % int2))) -> (rule6 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear likes the dog.
("bear" "likes" "dog" "+")
int2
The bear sees the bear.
True
4
proof
[(((((((triple1) -> rule1)) -> rule6)) -> rule7))]
("bear" "sees" "bear" "+")
((((((triple1) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
The bear sees the bear.
("bear" "sees" "bear" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
int2
The bear likes the dog.
("bear" "likes" "dog" "+")
int3
The bear does not see the bear.
False
4
inv-proof
[(((((((triple1) -> rule1)) -> rule6)) -> rule7))]
("bear" "sees" "bear" "-")
((((((triple1) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
The bear sees the bear.
("bear" "sees" "bear" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
int2
The bear likes the dog.
("bear" "likes" "dog" "+")
int3
The lion does not see the bear.
Unknown
inv-rconc
[@3: The lion sees the bear.[CWA. Example of deepest failure = (rule7 <- rule6 <- rule1 <- FAIL)]]
("lion" "sees" "bear" "-")
The mouse is red.
Unknown
rconc
[@1: The mouse is red.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "is" "red" "+")
The dog does not see the mouse.
Unknown
inv-rconc
[@1: The dog sees the mouse.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "sees" "mouse" "-")
The bear eats the mouse.
Unknown
rconc
[@1: The bear eats the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "eats" "mouse" "+")
The dog is not round.
Unknown
inv-random
[@0: The dog is round.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "round" "-")
The mouse is big.
Unknown
random
[@0: The mouse is big.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "big" "+")
The bear is not round.
Unknown
inv-random
[@0: The bear is round.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "round" "-")
The lion eats the bear.
Unknown
random
[@0: The lion eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "bear" "+")
@0: The bear is big.[(triple1)] The dog is red.[(triple2)] The lion sees the mouse.[(triple3)] The mouse eats the dog.[(triple4)] @1: The bear likes the dog.[(((triple1) -> rule1))] @2: The bear is nice.[(((((triple1) -> rule1)) -> rule6))] @3: The bear sees the bear.[(((((((triple1) -> rule1)) -> rule6)) -> rule7))]
The bear is big.
("bear" "is" "big" "+")
triple1
The dog is red.
("dog" "is" "red" "+")
triple2
The lion sees the mouse.
("lion" "sees" "mouse" "+")
triple3
The mouse eats the dog.
("mouse" "eats" "dog" "+")
triple4
The bear likes the dog.
("bear" "likes" "dog" "+")
((triple1) -> (rule1 % int1))
The bear likes the dog.
("bear" "likes" "dog" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
((((triple1) -> (rule1 % int2))) -> (rule6 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear likes the dog.
("bear" "likes" "dog" "+")
int2
The bear sees the bear.
("bear" "sees" "bear" "+")
((((((triple1) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
The bear sees the bear.
("bear" "sees" "bear" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
int2
The bear likes the dog.
("bear" "likes" "dog" "+")
int3