The cat is rough. The dog sees the mouse. The mouse is young. The rabbit sees the cat. If the rabbit is not rough then the rabbit is green. If something eats the cat and it likes the mouse then the mouse eats the rabbit. If the dog is big then the dog does not eat the mouse. If something is rough then it likes the cat. If something likes the cat then it is not big. If something eats the cat and it is not rough then it is big. If something likes the dog then it sees the rabbit. If the cat is not big then the cat likes the dog.
The cat is rough.
("cat" "is" "rough" "+")
The dog sees the mouse.
("dog" "sees" "mouse" "+")
The mouse is young.
("mouse" "is" "young" "+")
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
If the rabbit is not rough then the rabbit is green.
((("rabbit" "is" "rough" "~")) -> ("rabbit" "is" "green" "+"))
If something eats the cat and it likes the mouse then the mouse eats the rabbit.
((("something" "eats" "cat" "+") ("something" "likes" "mouse" "+")) -> ("mouse" "eats" "rabbit" "+"))
If the dog is big then the dog does not eat the mouse.
((("dog" "is" "big" "+")) -> ("dog" "eats" "mouse" "-"))
If something is rough then it likes the cat.
((("something" "is" "rough" "+")) -> ("something" "likes" "cat" "+"))
If something likes the cat then it is not big.
((("something" "likes" "cat" "+")) -> ("something" "is" "big" "-"))
If something eats the cat and it is not rough then it is big.
((("something" "eats" "cat" "+") ("something" "is" "rough" "~")) -> ("something" "is" "big" "+"))
If something likes the dog then it sees the rabbit.
((("something" "likes" "dog" "+")) -> ("something" "sees" "rabbit" "+"))
If the cat is not big then the cat likes the dog.
((("cat" "is" "big" "~")) -> ("cat" "likes" "dog" "+"))
The dog sees the mouse.
True
1
proof
[(triple2)]
("dog" "sees" "mouse" "+")
triple2
The cat is not rough.
False
1
inv-proof
[(triple1)]
("cat" "is" "rough" "-")
triple1
The cat likes the cat.
True
2
proof
[(((triple1) -> rule4))]
("cat" "likes" "cat" "+")
((triple1) -> (rule4 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat does not like the cat.
False
2
inv-proof
[(((triple1) -> rule4))]
("cat" "likes" "cat" "-")
((triple1) -> (rule4 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat is not big.
True
3
proof
[(((((triple1) -> rule4)) -> rule5))]
("cat" "is" "big" "-")
((((triple1) -> (rule4 % int2))) -> (rule5 % int1))
The cat is not big.
("cat" "is" "big" "-")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2
The cat is big.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule5))]
("cat" "is" "big" "+")
((((triple1) -> (rule4 % int2))) -> (rule5 % int1))
The cat is not big.
("cat" "is" "big" "-")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2
The cat likes the dog.
True
4
proof
[(((((((triple1) -> rule4)) -> rule5)) -> rule8))]
("cat" "likes" "dog" "+")
((((((triple1) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
The cat likes the dog.
("cat" "likes" "dog" "+")
int1
The cat is not big.
("cat" "is" "big" "-")
int2
The cat likes the cat.
("cat" "likes" "cat" "+")
int3
The cat does not like the dog.
False
4
inv-proof
[(((((((triple1) -> rule4)) -> rule5)) -> rule8))]
("cat" "likes" "dog" "-")
((((((triple1) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
The cat likes the dog.
("cat" "likes" "dog" "+")
int1
The cat is not big.
("cat" "is" "big" "-")
int2
The cat likes the cat.
("cat" "likes" "cat" "+")
int3
The mouse does not like the cat.
Unknown
inv-rconc
[@1: The mouse likes the cat.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "likes" "cat" "-")
The rabbit is green.
Unknown
rconc
[@1: The rabbit is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "is" "green" "+")
The mouse is not big.
Unknown
inv-rconc
[@1: The mouse is big.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("mouse" "is" "big" "-")
The dog sees the rabbit.
Unknown
rconc
[@1: The dog sees the rabbit.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("dog" "sees" "rabbit" "+")
The cat does not eat the dog.
Unknown
inv-random
[@0: The cat eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "dog" "-")
The dog sees the cat.
Unknown
random
[@0: The dog sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "cat" "+")
The dog does not eat the dog.
Unknown
inv-random
[@0: The dog eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "dog" "-")
The dog eats the rabbit.
Unknown
random
[@0: The dog eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "rabbit" "+")
@0: The cat is rough.[(triple1)] The dog sees the mouse.[(triple2)] The mouse is young.[(triple3)] The rabbit sees the cat.[(triple4)] @1: The cat likes the cat.[(((triple1) -> rule4))] @2: The cat is not big.[(((((triple1) -> rule4)) -> rule5))] @3: The cat likes the dog.[(((((((triple1) -> rule4)) -> rule5)) -> rule8))] @4: The cat sees the rabbit.[(((((((((triple1) -> rule4)) -> rule5)) -> rule8)) -> rule7))]
The cat is rough.
("cat" "is" "rough" "+")
triple1
The dog sees the mouse.
("dog" "sees" "mouse" "+")
triple2
The mouse is young.
("mouse" "is" "young" "+")
triple3
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
triple4
The cat likes the cat.
("cat" "likes" "cat" "+")
((triple1) -> (rule4 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat is not big.
("cat" "is" "big" "-")
((((triple1) -> (rule4 % int2))) -> (rule5 % int1))
The cat is not big.
("cat" "is" "big" "-")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2
The cat likes the dog.
("cat" "likes" "dog" "+")
((((((triple1) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
The cat likes the dog.
("cat" "likes" "dog" "+")
int1
The cat is not big.
("cat" "is" "big" "-")
int2
The cat likes the cat.
("cat" "likes" "cat" "+")
int3
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
((((((((triple1) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int1
The cat likes the dog.
("cat" "likes" "dog" "+")
int2
The cat is not big.
("cat" "is" "big" "-")
int3
The cat likes the cat.
("cat" "likes" "cat" "+")
int4