The cat does not eat the dog. The dog sees the rabbit. The mouse is big. The mouse is round. The rabbit eats the cat. The rabbit is round. The rabbit likes the dog. If the cat sees the dog and the cat is rough then the cat likes the mouse. If someone likes the rabbit then they see the mouse. If someone sees the cat and they like the dog then the cat likes the rabbit. If someone eats the cat then the cat is blue. If someone is round then they see the cat. If someone likes the mouse then the mouse eats the dog. If someone sees the mouse then the mouse likes the rabbit. If the cat likes the mouse then the mouse likes the rabbit.
The cat does not eat the dog.
("cat" "eats" "dog" "-")
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse is round.
("mouse" "is" "round" "+")
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
If the cat sees the dog and the cat is rough then the cat likes the mouse.
((("cat" "sees" "dog" "+") ("cat" "is" "rough" "+")) -> ("cat" "likes" "mouse" "+"))
If someone likes the rabbit then they see the mouse.
((("someone" "likes" "rabbit" "+")) -> ("someone" "sees" "mouse" "+"))
If someone sees the cat and they like the dog then the cat likes the rabbit.
((("someone" "sees" "cat" "+") ("someone" "likes" "dog" "+")) -> ("cat" "likes" "rabbit" "+"))
If someone eats the cat then the cat is blue.
((("someone" "eats" "cat" "+")) -> ("cat" "is" "blue" "+"))
If someone is round then they see the cat.
((("someone" "is" "round" "+")) -> ("someone" "sees" "cat" "+"))
If someone likes the mouse then the mouse eats the dog.
((("someone" "likes" "mouse" "+")) -> ("mouse" "eats" "dog" "+"))
If someone sees the mouse then the mouse likes the rabbit.
((("someone" "sees" "mouse" "+")) -> ("mouse" "likes" "rabbit" "+"))
If the cat likes the mouse then the mouse likes the rabbit.
((("cat" "likes" "mouse" "+")) -> ("mouse" "likes" "rabbit" "+"))
The mouse is big.
True
1
proof
[(triple3)]
("mouse" "is" "big" "+")
triple3
The rabbit does not eat the cat.
False
1
inv-proof
[(triple5)]
("rabbit" "eats" "cat" "-")
triple5
The mouse sees the cat.
True
2
proof
[(((triple4) -> rule5))]
("mouse" "sees" "cat" "+")
((triple4) -> (rule5 % int1))
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int1
The cat is not blue.
False
2
inv-proof
[(((triple5) -> rule4))]
("cat" "is" "blue" "-")
((triple5) -> (rule4 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The cat likes the rabbit.
True
4
proof
[(((((triple6) -> rule5) triple7) -> rule3))]
("cat" "likes" "rabbit" "+")
((((triple6) -> (rule5 % int2)) triple7) -> (rule3 % int1))
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
int1
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int2
The cat does not like the rabbit.
False
4
inv-proof
[(((((triple6) -> rule5) triple7) -> rule3))]
("cat" "likes" "rabbit" "-")
((((triple6) -> (rule5 % int2)) triple7) -> (rule3 % int1))
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
int1
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int2
The cat sees the mouse.
True
5
proof
[(((((((triple6) -> rule5) triple7) -> rule3)) -> rule2))]
("cat" "sees" "mouse" "+")
((((((triple6) -> (rule5 % int3)) triple7) -> (rule3 % int2))) -> (rule2 % int1))
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int1
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
int2
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int3
The cat does not see the mouse.
False
5
inv-proof
[(((((((triple6) -> rule5) triple7) -> rule3)) -> rule2))]
("cat" "sees" "mouse" "-")
((((((triple6) -> (rule5 % int3)) triple7) -> (rule3 % int2))) -> (rule2 % int1))
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int1
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
int2
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int3
The mouse likes the rabbit.
True
6
proof
[(((((((((triple6) -> rule5) triple7) -> rule3)) -> rule2)) -> rule7))]
("mouse" "likes" "rabbit" "+")
((((((((triple6) -> (rule5 % int4)) triple7) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int1
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int2
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
int3
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int4
The mouse does not like the rabbit.
False
6
inv-proof
[(((((((((triple6) -> rule5) triple7) -> rule3)) -> rule2)) -> rule7))]
("mouse" "likes" "rabbit" "-")
((((((((triple6) -> (rule5 % int4)) triple7) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int1
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int2
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
int3
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int4
The mouse sees the mouse.
True
7
proof
[(((((((((((triple6) -> rule5) triple7) -> rule3)) -> rule2)) -> rule7)) -> rule2))]
("mouse" "sees" "mouse" "+")
((((((((((triple6) -> (rule5 % int5)) triple7) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int2
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int3
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
int4
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int5
The mouse does not see the mouse.
False
7
inv-proof
[(((((((((((triple6) -> rule5) triple7) -> rule3)) -> rule2)) -> rule7)) -> rule2))]
("mouse" "sees" "mouse" "-")
((((((((((triple6) -> (rule5 % int5)) triple7) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int2
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int3
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
int4
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int5
The cat does not like the mouse.
Unknown
inv-rconc
[@1: The cat likes the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "likes" "mouse" "-")
The dog sees the mouse.
Unknown
rconc
[@1: The dog sees the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "sees" "mouse" "+")
The rabbit does not see the mouse.
Unknown
inv-rconc
[@1: The rabbit sees the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "sees" "mouse" "-")
The cat sees the cat.
Unknown
rconc
[@1: The cat sees the cat.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "sees" "cat" "+")
The mouse does not eat the dog.
Unknown
inv-rconc
[@2: The mouse eats the dog.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("mouse" "eats" "dog" "-")
The dog sees the cat.
Unknown
rconc
[@1: The dog sees the cat.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "sees" "cat" "+")
The rabbit does not eat the dog.
Unknown
inv-random
[@0: The rabbit eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "dog" "-")
The cat eats the cat.
Unknown
random
[@0: The cat eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cat" "+")
The cat is not big.
Unknown
inv-random
[@0: The cat is big.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "big" "-")
The mouse eats the mouse.
Unknown
random
[@0: The mouse eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "mouse" "+")
The dog does not see the dog.
Unknown
inv-random
[@0: The dog sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "dog" "-")
The dog is round.
Unknown
random
[@0: The dog is round.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "round" "+")
@0: The cat does not eat the dog.[(triple1)] The dog sees the rabbit.[(triple2)] The mouse is big.[(triple3)] The mouse is round.[(triple4)] The rabbit eats the cat.[(triple5)] The rabbit is round.[(triple6)] The rabbit likes the dog.[(triple7)] @1: The cat is blue.[(((triple5) -> rule4))] The mouse sees the cat.[(((triple4) -> rule5))] The rabbit sees the cat.[(((triple6) -> rule5))] @2: The cat likes the rabbit.[(((((triple6) -> rule5) triple7) -> rule3))] @3: The cat sees the mouse.[(((((((triple6) -> rule5) triple7) -> rule3)) -> rule2))] @4: The mouse likes the rabbit.[(((((((((triple6) -> rule5) triple7) -> rule3)) -> rule2)) -> rule7))] @5: The mouse sees the mouse.[(((((((((((triple6) -> rule5) triple7) -> rule3)) -> rule2)) -> rule7)) -> rule2))]
The cat does not eat the dog.
("cat" "eats" "dog" "-")
triple1
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
triple2
The mouse is big.
("mouse" "is" "big" "+")
triple3
The mouse is round.
("mouse" "is" "round" "+")
triple4
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
triple5
The rabbit is round.
("rabbit" "is" "round" "+")
triple6
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
triple7
The cat is blue.
("cat" "is" "blue" "+")
((triple5) -> (rule4 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The mouse sees the cat.
("mouse" "sees" "cat" "+")
((triple4) -> (rule5 % int1))
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int1
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
((triple6) -> (rule5 % int1))
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int1
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
((((triple6) -> (rule5 % int2)) triple7) -> (rule3 % int1))
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
int1
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int2
The cat sees the mouse.
("cat" "sees" "mouse" "+")
((((((triple6) -> (rule5 % int3)) triple7) -> (rule3 % int2))) -> (rule2 % int1))
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int1
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
int2
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int3
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
((((((((triple6) -> (rule5 % int4)) triple7) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int1
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int2
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
int3
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int4
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
((((((((((triple6) -> (rule5 % int5)) triple7) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int2
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int3
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
int4
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int5