The bear chases the lion. The bear is young. The bear likes the lion. The lion is kind. The lion likes the bear. The lion sees the bear. The lion sees the mouse. The mouse is kind. The mouse is young. The mouse sees the lion. If something is young then it sees the bear. If something sees the bear then it is kind. If something sees the bear then it likes the bear.
The bear chases the lion.
("bear" "chases" "lion" "+")
The bear is young.
("bear" "is" "young" "+")
The bear likes the lion.
("bear" "likes" "lion" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion likes the bear.
("lion" "likes" "bear" "+")
The lion sees the bear.
("lion" "sees" "bear" "+")
The lion sees the mouse.
("lion" "sees" "mouse" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse sees the lion.
("mouse" "sees" "lion" "+")
If something is young then it sees the bear.
((("something" "is" "young" "+")) -> ("something" "sees" "bear" "+"))
If something sees the bear then it is kind.
((("something" "sees" "bear" "+")) -> ("something" "is" "kind" "+"))
If something sees the bear then it likes the bear.
((("something" "sees" "bear" "+")) -> ("something" "likes" "bear" "+"))
The lion likes the bear.
True
1
proof
[(triple5 OR ((triple6) -> rule3))]
("lion" "likes" "bear" "+")
triple5
((triple6) -> (rule3 % int1))
The lion likes the bear.
("lion" "likes" "bear" "+")
int1
The mouse is not young.
False
1
inv-proof
[(triple9)]
("mouse" "is" "young" "-")
triple9
The bear sees the bear.
True
2
proof
[(((triple2) -> rule1))]
("bear" "sees" "bear" "+")
((triple2) -> (rule1 % int1))
The bear sees the bear.
("bear" "sees" "bear" "+")
int1
The bear does not see the bear.
False
2
inv-proof
[(((triple2) -> rule1))]
("bear" "sees" "bear" "-")
((triple2) -> (rule1 % int1))
The bear sees the bear.
("bear" "sees" "bear" "+")
int1
The mouse likes the bear.
True
3
proof
[(((((triple9) -> rule1)) -> rule3))]
("mouse" "likes" "bear" "+")
((((triple9) -> (rule1 % int2))) -> (rule3 % int1))
The mouse likes the bear.
("mouse" "likes" "bear" "+")
int1
The mouse sees the bear.
("mouse" "sees" "bear" "+")
int2
The mouse does not like the bear.
False
3
inv-proof
[(((((triple9) -> rule1)) -> rule3))]
("mouse" "likes" "bear" "-")
((((triple9) -> (rule1 % int2))) -> (rule3 % int1))
The mouse likes the bear.
("mouse" "likes" "bear" "+")
int1
The mouse sees the bear.
("mouse" "sees" "bear" "+")
int2
The bear does not chase the bear.
Unknown
inv-random
[@0: The bear chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "bear" "-")
The lion likes the mouse.
Unknown
random
[@0: The lion likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "mouse" "+")
The bear is not nice.
Unknown
inv-random
[@0: The bear is nice.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "nice" "-")
The mouse chases the bear.
Unknown
random
[@0: The mouse chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "bear" "+")
The mouse is not red.
Unknown
inv-random
[@0: The mouse is red.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "red" "-")
The lion is nice.
Unknown
random
[@0: The lion is nice.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "nice" "+")
@0: The bear chases the lion.[(triple1)] The bear is young.[(triple2)] The bear likes the lion.[(triple3)] The lion is kind.[(triple4 OR ((triple6) -> rule2))] The lion likes the bear.[(triple5 OR ((triple6) -> rule3))] The lion sees the bear.[(triple6)] The lion sees the mouse.[(triple7)] The mouse is kind.[(triple8 OR ((((triple9) -> rule1)) -> rule2))] The mouse is young.[(triple9)] The mouse sees the lion.[(triple10)] @1: The bear sees the bear.[(((triple2) -> rule1))] The mouse sees the bear.[(((triple9) -> rule1))] @2: The bear is kind.[(((((triple2) -> rule1)) -> rule2))] The bear likes the bear.[(((((triple2) -> rule1)) -> rule3))] The mouse likes the bear.[(((((triple9) -> rule1)) -> rule3))]
The bear chases the lion.
("bear" "chases" "lion" "+")
triple1
The bear is young.
("bear" "is" "young" "+")
triple2
The bear likes the lion.
("bear" "likes" "lion" "+")
triple3
The lion is kind.
("lion" "is" "kind" "+")
triple4
((triple6) -> (rule2 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion likes the bear.
("lion" "likes" "bear" "+")
triple5
((triple6) -> (rule3 % int1))
The lion likes the bear.
("lion" "likes" "bear" "+")
int1
The lion sees the bear.
("lion" "sees" "bear" "+")
triple6
The lion sees the mouse.
("lion" "sees" "mouse" "+")
triple7
The mouse is kind.
("mouse" "is" "kind" "+")
triple8
((((triple9) -> (rule1 % int2))) -> (rule2 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The mouse sees the bear.
("mouse" "sees" "bear" "+")
int2
The mouse is young.
("mouse" "is" "young" "+")
triple9
The mouse sees the lion.
("mouse" "sees" "lion" "+")
triple10
The bear sees the bear.
("bear" "sees" "bear" "+")
((triple2) -> (rule1 % int1))
The bear sees the bear.
("bear" "sees" "bear" "+")
int1
The mouse sees the bear.
("mouse" "sees" "bear" "+")
((triple9) -> (rule1 % int1))
The mouse sees the bear.
("mouse" "sees" "bear" "+")
int1
The bear is kind.
("bear" "is" "kind" "+")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The bear sees the bear.
("bear" "sees" "bear" "+")
int2
The bear likes the bear.
("bear" "likes" "bear" "+")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
The bear likes the bear.
("bear" "likes" "bear" "+")
int1
The bear sees the bear.
("bear" "sees" "bear" "+")
int2
The mouse likes the bear.
("mouse" "likes" "bear" "+")
((((triple9) -> (rule1 % int2))) -> (rule3 % int1))
The mouse likes the bear.
("mouse" "likes" "bear" "+")
int1
The mouse sees the bear.
("mouse" "sees" "bear" "+")
int2