The bear chases the rabbit. The bear is young. The cat is round. The mouse is not cold. The mouse needs the cat. The rabbit does not chase the mouse. The rabbit needs the bear. If something needs the bear and the bear is cold then it sees the bear. If something needs the mouse and the mouse chases the bear then it sees the cat. If something needs the cat and it is not kind then it sees the mouse. If something is round then it chases the mouse. If something chases the mouse then the mouse is round. If something chases the bear and it is kind then it needs the cat.
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
The bear is young.
("bear" "is" "young" "+")
The cat is round.
("cat" "is" "round" "+")
The mouse is not cold.
("mouse" "is" "cold" "-")
The mouse needs the cat.
("mouse" "needs" "cat" "+")
The rabbit does not chase the mouse.
("rabbit" "chases" "mouse" "-")
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
If something needs the bear and the bear is cold then it sees the bear.
((("something" "needs" "bear" "+") ("bear" "is" "cold" "+")) -> ("something" "sees" "bear" "+"))
If something needs the mouse and the mouse chases the bear then it sees the cat.
((("something" "needs" "mouse" "+") ("mouse" "chases" "bear" "+")) -> ("something" "sees" "cat" "+"))
If something needs the cat and it is not kind then it sees the mouse.
((("something" "needs" "cat" "+") ("something" "is" "kind" "~")) -> ("something" "sees" "mouse" "+"))
If something is round then it chases the mouse.
((("something" "is" "round" "+")) -> ("something" "chases" "mouse" "+"))
If something chases the mouse then the mouse is round.
((("something" "chases" "mouse" "+")) -> ("mouse" "is" "round" "+"))
If something chases the bear and it is kind then it needs the cat.
((("something" "chases" "bear" "+") ("something" "is" "kind" "+")) -> ("something" "needs" "cat" "+"))
The bear is young.
True
1
proof
[(triple2)]
("bear" "is" "young" "+")
triple2
The bear does not chase the rabbit.
False
1
inv-proof
[(triple1)]
("bear" "chases" "rabbit" "-")
triple1
The cat chases the mouse.
True
2
proof
[(((triple3) -> rule4))]
("cat" "chases" "mouse" "+")
((triple3) -> (rule4 % int1))
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int1
The cat does not chase the mouse.
False
2
inv-proof
[(((triple3) -> rule4))]
("cat" "chases" "mouse" "-")
((triple3) -> (rule4 % int1))
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int1
The mouse is round.
True
3
proof
[(((((triple3) -> rule4)) -> rule5))]
("mouse" "is" "round" "+")
((((triple3) -> (rule4 % int2))) -> (rule5 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int2
The mouse is not round.
False
3
inv-proof
[(((((triple3) -> rule4)) -> rule5))]
("mouse" "is" "round" "-")
((((triple3) -> (rule4 % int2))) -> (rule5 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int2
The mouse chases the mouse.
True
4
proof
[(((((((triple3) -> rule4)) -> rule5)) -> rule4))]
("mouse" "chases" "mouse" "+")
((((((triple3) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int3
The mouse does not chase the mouse.
False
4
inv-proof
[(((((((triple3) -> rule4)) -> rule5)) -> rule4))]
("mouse" "chases" "mouse" "-")
((((((triple3) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int3
The cat does not see the cat.
Unknown
inv-rconc
[@1: The cat sees the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "sees" "cat" "-")
The bear sees the bear.
Unknown
rconc
[@1: The bear sees the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "sees" "bear" "+")
The rabbit does not see the cat.
Unknown
inv-rconc
[@1: The rabbit sees the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "sees" "cat" "-")
The mouse sees the bear.
Unknown
rconc
[@1: The mouse sees the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "sees" "bear" "+")
The mouse does not chase the cat.
Unknown
inv-random
[@0: The mouse chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "cat" "-")
The bear needs the mouse.
Unknown
random
[@0: The bear needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "mouse" "+")
The cat is not cold.
Unknown
inv-random
[@0: The cat is cold.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "cold" "-")
The mouse is nice.
Unknown
random
[@0: The mouse is nice.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "nice" "+")
@0: The bear chases the rabbit.[(triple1)] The bear is young.[(triple2)] The cat is round.[(triple3)] The mouse is not cold.[(triple4)] The mouse needs the cat.[(triple5)] The rabbit does not chase the mouse.[(triple6)] The rabbit needs the bear.[(triple7)] @1: The cat chases the mouse.[(((triple3) -> rule4))] @2: The mouse is round.[(((((triple3) -> rule4)) -> rule5))] @3: The mouse chases the mouse.[(((((((triple3) -> rule4)) -> rule5)) -> rule4))]
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
triple1
The bear is young.
("bear" "is" "young" "+")
triple2
The cat is round.
("cat" "is" "round" "+")
triple3
The mouse is not cold.
("mouse" "is" "cold" "-")
triple4
The mouse needs the cat.
("mouse" "needs" "cat" "+")
triple5
The rabbit does not chase the mouse.
("rabbit" "chases" "mouse" "-")
triple6
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
triple7
The cat chases the mouse.
("cat" "chases" "mouse" "+")
((triple3) -> (rule4 % int1))
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
((((triple3) -> (rule4 % int2))) -> (rule5 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int2
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
((((((triple3) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int3