The bear eats the mouse. The bear is kind. The bear is red. The bear needs the cat. The bear sees the cat. The cat eats the mouse. The cat is red. The cat needs the mouse. The cat sees the bear. The mouse is round. If someone sees the mouse then they need the bear. If someone needs the bear then they eat the bear. If someone eats the mouse then the mouse needs the bear.
The bear eats the mouse.
("bear" "eats" "mouse" "+")
The bear is kind.
("bear" "is" "kind" "+")
The bear is red.
("bear" "is" "red" "+")
The bear needs the cat.
("bear" "needs" "cat" "+")
The bear sees the cat.
("bear" "sees" "cat" "+")
The cat eats the mouse.
("cat" "eats" "mouse" "+")
The cat is red.
("cat" "is" "red" "+")
The cat needs the mouse.
("cat" "needs" "mouse" "+")
The cat sees the bear.
("cat" "sees" "bear" "+")
The mouse is round.
("mouse" "is" "round" "+")
If someone sees the mouse then they need the bear.
((("someone" "sees" "mouse" "+")) -> ("someone" "needs" "bear" "+"))
If someone needs the bear then they eat the bear.
((("someone" "needs" "bear" "+")) -> ("someone" "eats" "bear" "+"))
If someone eats the mouse then the mouse needs the bear.
((("someone" "eats" "mouse" "+")) -> ("mouse" "needs" "bear" "+"))
The bear is red.
True
1
proof
[(triple3)]
("bear" "is" "red" "+")
triple3
The bear is not red.
False
1
inv-proof
[(triple3)]
("bear" "is" "red" "-")
triple3
The mouse needs the bear.
True
2
proof
[(((triple1) -> rule3) OR ((triple6) -> rule3))]
("mouse" "needs" "bear" "+")
((triple1) -> (rule3 % int1))
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int1
((triple6) -> (rule3 % int1))
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int1
The mouse does not need the bear.
False
2
inv-proof
[(((triple1) -> rule3) OR ((triple6) -> rule3))]
("mouse" "needs" "bear" "-")
((triple1) -> (rule3 % int1))
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int1
((triple6) -> (rule3 % int1))
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int1
The mouse eats the bear.
True
3
proof
[(((((triple1) -> rule3)) -> rule2) OR ((((triple6) -> rule3)) -> rule2))]
("mouse" "eats" "bear" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The mouse eats the bear.
("mouse" "eats" "bear" "+")
int1
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int2
((((triple6) -> (rule3 % int2))) -> (rule2 % int1))
The mouse eats the bear.
("mouse" "eats" "bear" "+")
int1
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int2
The mouse does not eat the bear.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule2) OR ((((triple6) -> rule3)) -> rule2))]
("mouse" "eats" "bear" "-")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The mouse eats the bear.
("mouse" "eats" "bear" "+")
int1
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int2
((((triple6) -> (rule3 % int2))) -> (rule2 % int1))
The mouse eats the bear.
("mouse" "eats" "bear" "+")
int1
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int2
The bear does not need the bear.
Unknown
inv-rconc
[@1: The bear needs the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "needs" "bear" "-")
The bear eats the bear.
Unknown
rconc
[@2: The bear eats the bear.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("bear" "eats" "bear" "+")
The cat does not need the bear.
Unknown
inv-rconc
[@1: The cat needs the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "needs" "bear" "-")
The bear needs the mouse.
Unknown
random
[@0: The bear needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "mouse" "+")
The bear does not eat the cat.
Unknown
inv-random
[@0: The bear eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "cat" "-")
The cat sees the cat.
Unknown
random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "+")
@0: The bear eats the mouse.[(triple1)] The bear is kind.[(triple2)] The bear is red.[(triple3)] The bear needs the cat.[(triple4)] The bear sees the cat.[(triple5)] The cat eats the mouse.[(triple6)] The cat is red.[(triple7)] The cat needs the mouse.[(triple8)] The cat sees the bear.[(triple9)] The mouse is round.[(triple10)] @1: The mouse needs the bear.[(((triple1) -> rule3) OR ((triple6) -> rule3))] @2: The mouse eats the bear.[(((((triple1) -> rule3)) -> rule2) OR ((((triple6) -> rule3)) -> rule2))]
The bear eats the mouse.
("bear" "eats" "mouse" "+")
triple1
The bear is kind.
("bear" "is" "kind" "+")
triple2
The bear is red.
("bear" "is" "red" "+")
triple3
The bear needs the cat.
("bear" "needs" "cat" "+")
triple4
The bear sees the cat.
("bear" "sees" "cat" "+")
triple5
The cat eats the mouse.
("cat" "eats" "mouse" "+")
triple6
The cat is red.
("cat" "is" "red" "+")
triple7
The cat needs the mouse.
("cat" "needs" "mouse" "+")
triple8
The cat sees the bear.
("cat" "sees" "bear" "+")
triple9
The mouse is round.
("mouse" "is" "round" "+")
triple10
The mouse needs the bear.
("mouse" "needs" "bear" "+")
((triple1) -> (rule3 % int1))
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int1
((triple6) -> (rule3 % int1))
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int1
The mouse eats the bear.
("mouse" "eats" "bear" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The mouse eats the bear.
("mouse" "eats" "bear" "+")
int1
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int2
((((triple6) -> (rule3 % int2))) -> (rule2 % int1))
The mouse eats the bear.
("mouse" "eats" "bear" "+")
int1
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int2