The cat is young. The mouse sees the cat. The rabbit is round. If the rabbit chases the cat then the rabbit chases the mouse. If someone sees the rabbit then the rabbit is green. If someone is round and they chase the mouse then they eat the cat. If someone sees the rabbit and the rabbit chases the cat then they eat the mouse. If someone sees the cat then the cat eats the mouse. If someone sees the rabbit then they eat the rabbit. If someone is round then they chase the cat. If someone is red and round then they see the cat.
The cat is young.
("cat" "is" "young" "+")
The mouse sees the cat.
("mouse" "sees" "cat" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
If the rabbit chases the cat then the rabbit chases the mouse.
((("rabbit" "chases" "cat" "+")) -> ("rabbit" "chases" "mouse" "+"))
If someone sees the rabbit then the rabbit is green.
((("someone" "sees" "rabbit" "+")) -> ("rabbit" "is" "green" "+"))
If someone is round and they chase the mouse then they eat the cat.
((("someone" "is" "round" "+") ("someone" "chases" "mouse" "+")) -> ("someone" "eats" "cat" "+"))
If someone sees the rabbit and the rabbit chases the cat then they eat the mouse.
((("someone" "sees" "rabbit" "+") ("rabbit" "chases" "cat" "+")) -> ("someone" "eats" "mouse" "+"))
If someone sees the cat then the cat eats the mouse.
((("someone" "sees" "cat" "+")) -> ("cat" "eats" "mouse" "+"))
If someone sees the rabbit then they eat the rabbit.
((("someone" "sees" "rabbit" "+")) -> ("someone" "eats" "rabbit" "+"))
If someone is round then they chase the cat.
((("someone" "is" "round" "+")) -> ("someone" "chases" "cat" "+"))
If someone is red and round then they see the cat.
((("someone" "is" "red" "+") ("someone" "is" "round" "+")) -> ("someone" "sees" "cat" "+"))
The mouse sees the cat.
True
1
proof
[(triple2)]
("mouse" "sees" "cat" "+")
triple2
The rabbit is not round.
False
1
inv-proof
[(triple3)]
("rabbit" "is" "round" "-")
triple3
The rabbit chases the cat.
True
2
proof
[(((triple3) -> rule7))]
("rabbit" "chases" "cat" "+")
((triple3) -> (rule7 % int1))
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
int1
The cat does not eat the mouse.
False
2
inv-proof
[(((triple2) -> rule5))]
("cat" "eats" "mouse" "-")
((triple2) -> (rule5 % int1))
The cat eats the mouse.
("cat" "eats" "mouse" "+")
int1
The rabbit chases the mouse.
True
3
proof
[(((((triple3) -> rule7)) -> rule1))]
("rabbit" "chases" "mouse" "+")
((((triple3) -> (rule7 % int2))) -> (rule1 % int1))
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
int1
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
int2
The rabbit does not chase the mouse.
False
3
inv-proof
[(((((triple3) -> rule7)) -> rule1))]
("rabbit" "chases" "mouse" "-")
((((triple3) -> (rule7 % int2))) -> (rule1 % int1))
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
int1
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
int2
The rabbit eats the cat.
True
5
proof
[(((triple3 ((((triple3) -> rule7)) -> rule1)) -> rule3))]
("rabbit" "eats" "cat" "+")
((triple3 ((((triple3) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
int1
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
int2
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
int3
The rabbit does not eat the cat.
False
5
inv-proof
[(((triple3 ((((triple3) -> rule7)) -> rule1)) -> rule3))]
("rabbit" "eats" "cat" "-")
((triple3 ((((triple3) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
int1
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
int2
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
int3
The cat does not eat the cat.
Unknown
inv-rconc
[@1: The cat eats the cat.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "eats" "cat" "-")
The mouse eats the mouse.
Unknown
rconc
[@1: The mouse eats the mouse.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "eats" "mouse" "+")
The cat does not chase the cat.
Unknown
inv-rconc
[@1: The cat chases the cat.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("cat" "chases" "cat" "-")
The rabbit is green.
Unknown
rconc
[@1: The rabbit is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "is" "green" "+")
The cat does not see the mouse.
Unknown
inv-random
[@0: The cat sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "mouse" "-")
The rabbit is red.
Unknown
random
[@0: The rabbit is red.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "red" "+")
The rabbit does not see the rabbit.
Unknown
inv-random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "-")
The mouse is round.
Unknown
random
[@0: The mouse is round.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "round" "+")
@0: The cat is young.[(triple1)] The mouse sees the cat.[(triple2)] The rabbit is round.[(triple3)] @1: The cat eats the mouse.[(((triple2) -> rule5))] The rabbit chases the cat.[(((triple3) -> rule7))] @2: The rabbit chases the mouse.[(((((triple3) -> rule7)) -> rule1))] @3: The rabbit eats the cat.[(((triple3 ((((triple3) -> rule7)) -> rule1)) -> rule3))]
The cat is young.
("cat" "is" "young" "+")
triple1
The mouse sees the cat.
("mouse" "sees" "cat" "+")
triple2
The rabbit is round.
("rabbit" "is" "round" "+")
triple3
The cat eats the mouse.
("cat" "eats" "mouse" "+")
((triple2) -> (rule5 % int1))
The cat eats the mouse.
("cat" "eats" "mouse" "+")
int1
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
((triple3) -> (rule7 % int1))
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
int1
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
((((triple3) -> (rule7 % int2))) -> (rule1 % int1))
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
int1
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
int2
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
((triple3 ((((triple3) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
int1
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
int2
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
int3