The cat needs the mouse. The dog chases the cat. The mouse chases the cat. If something visits the dog then it does not need the cat. If something chases the cat then the cat chases the mouse. If something chases the mouse and the mouse is big then the mouse visits the dog. If something chases the mouse then the mouse visits the dog. If something chases the mouse and it needs the dog then the mouse chases the cat. If something visits the mouse and it is big then it chases the cat. If something is red and it needs the cat then the cat does not need the dog. If something chases the cat then the cat does not visit the dog.
The cat needs the mouse.
("cat" "needs" "mouse" "+")
The dog chases the cat.
("dog" "chases" "cat" "+")
The mouse chases the cat.
("mouse" "chases" "cat" "+")
If something visits the dog then it does not need the cat.
((("something" "visits" "dog" "+")) -> ("something" "needs" "cat" "-"))
If something chases the cat then the cat chases the mouse.
((("something" "chases" "cat" "+")) -> ("cat" "chases" "mouse" "+"))
If something chases the mouse and the mouse is big then the mouse visits the dog.
((("something" "chases" "mouse" "+") ("mouse" "is" "big" "+")) -> ("mouse" "visits" "dog" "+"))
If something chases the mouse then the mouse visits the dog.
((("something" "chases" "mouse" "+")) -> ("mouse" "visits" "dog" "+"))
If something chases the mouse and it needs the dog then the mouse chases the cat.
((("something" "chases" "mouse" "+") ("something" "needs" "dog" "+")) -> ("mouse" "chases" "cat" "+"))
If something visits the mouse and it is big then it chases the cat.
((("something" "visits" "mouse" "+") ("something" "is" "big" "+")) -> ("something" "chases" "cat" "+"))
If something is red and it needs the cat then the cat does not need the dog.
((("something" "is" "red" "+") ("something" "needs" "cat" "+")) -> ("cat" "needs" "dog" "-"))
If something chases the cat then the cat does not visit the dog.
((("something" "chases" "cat" "+")) -> ("cat" "visits" "dog" "-"))
The cat needs the mouse.
True
1
proof
[(triple1)]
("cat" "needs" "mouse" "+")
triple1
The mouse does not chase the cat.
False
1
inv-proof
[(triple3)]
("mouse" "chases" "cat" "-")
triple3
The cat chases the mouse.
True
2
proof
[(((triple2) -> rule2) OR ((triple3) -> rule2))]
("cat" "chases" "mouse" "+")
((triple2) -> (rule2 % int1))
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int1
((triple3) -> (rule2 % int1))
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int1
The cat visits the dog.
False
2
inv-proof
[(((triple2) -> rule8) OR ((triple3) -> rule8))]
("cat" "visits" "dog" "+")
((triple2) -> (rule8 % int1))
The cat does not visit the dog.
("cat" "visits" "dog" "-")
int1
((triple3) -> (rule8 % int1))
The cat does not visit the dog.
("cat" "visits" "dog" "-")
int1
The mouse visits the dog.
True
3
proof
[(((((triple2) -> rule2)) -> rule4) OR ((((triple3) -> rule2)) -> rule4))]
("mouse" "visits" "dog" "+")
((((triple2) -> (rule2 % int2))) -> (rule4 % int1))
The mouse visits the dog.
("mouse" "visits" "dog" "+")
int1
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int2
((((triple3) -> (rule2 % int2))) -> (rule4 % int1))
The mouse visits the dog.
("mouse" "visits" "dog" "+")
int1
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int2
The mouse does not visit the dog.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule4) OR ((((triple3) -> rule2)) -> rule4))]
("mouse" "visits" "dog" "-")
((((triple2) -> (rule2 % int2))) -> (rule4 % int1))
The mouse visits the dog.
("mouse" "visits" "dog" "+")
int1
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int2
((((triple3) -> (rule2 % int2))) -> (rule4 % int1))
The mouse visits the dog.
("mouse" "visits" "dog" "+")
int1
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int2
The mouse does not need the cat.
True
4
proof
[(((((((triple2) -> rule2)) -> rule4)) -> rule1) OR ((((((triple3) -> rule2)) -> rule4)) -> rule1))]
("mouse" "needs" "cat" "-")
((((((triple2) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The mouse does not need the cat.
("mouse" "needs" "cat" "-")
int1
The mouse visits the dog.
("mouse" "visits" "dog" "+")
int2
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int3
((((((triple3) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The mouse does not need the cat.
("mouse" "needs" "cat" "-")
int1
The mouse visits the dog.
("mouse" "visits" "dog" "+")
int2
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int3
The mouse needs the cat.
False
4
inv-proof
[(((((((triple2) -> rule2)) -> rule4)) -> rule1) OR ((((((triple3) -> rule2)) -> rule4)) -> rule1))]
("mouse" "needs" "cat" "+")
((((((triple2) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The mouse does not need the cat.
("mouse" "needs" "cat" "-")
int1
The mouse visits the dog.
("mouse" "visits" "dog" "+")
int2
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int3
((((((triple3) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The mouse does not need the cat.
("mouse" "needs" "cat" "-")
int1
The mouse visits the dog.
("mouse" "visits" "dog" "+")
int2
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int3
The cat does not chase the cat.
Unknown
inv-rconc
[@1: The cat chases the cat.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cat" "chases" "cat" "-")
The dog chases the dog.
Unknown
random
[@0: The dog chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "dog" "+")
The cat is not red.
Unknown
inv-random
[@0: The cat is red.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "red" "-")
The cat is young.
Unknown
random
[@0: The cat is young.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "young" "+")
The mouse does not chase the dog.
Unknown
inv-random
[@0: The mouse chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "dog" "-")
The dog needs the dog.
Unknown
random
[@0: The dog needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "dog" "+")
The dog is not big.
Unknown
inv-random
[@0: The dog is big.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "big" "-")
The dog needs the mouse.
Unknown
random
[@0: The dog needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "mouse" "+")
@0: The cat needs the mouse.[(triple1)] The dog chases the cat.[(triple2)] The mouse chases the cat.[(triple3)] @1: The cat chases the mouse.[(((triple2) -> rule2) OR ((triple3) -> rule2))] The cat does not visit the dog.[(((triple2) -> rule8) OR ((triple3) -> rule8))] @2: The mouse visits the dog.[(((((triple2) -> rule2)) -> rule4) OR ((((triple3) -> rule2)) -> rule4))] @3: The mouse does not need the cat.[(((((((triple2) -> rule2)) -> rule4)) -> rule1) OR ((((((triple3) -> rule2)) -> rule4)) -> rule1))]
The cat needs the mouse.
("cat" "needs" "mouse" "+")
triple1
The dog chases the cat.
("dog" "chases" "cat" "+")
triple2
The mouse chases the cat.
("mouse" "chases" "cat" "+")
triple3
The cat chases the mouse.
("cat" "chases" "mouse" "+")
((triple2) -> (rule2 % int1))
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int1
((triple3) -> (rule2 % int1))
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int1
The cat does not visit the dog.
("cat" "visits" "dog" "-")
((triple2) -> (rule8 % int1))
The cat does not visit the dog.
("cat" "visits" "dog" "-")
int1
((triple3) -> (rule8 % int1))
The cat does not visit the dog.
("cat" "visits" "dog" "-")
int1
The mouse visits the dog.
("mouse" "visits" "dog" "+")
((((triple2) -> (rule2 % int2))) -> (rule4 % int1))
The mouse visits the dog.
("mouse" "visits" "dog" "+")
int1
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int2
((((triple3) -> (rule2 % int2))) -> (rule4 % int1))
The mouse visits the dog.
("mouse" "visits" "dog" "+")
int1
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int2
The mouse does not need the cat.
("mouse" "needs" "cat" "-")
((((((triple2) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The mouse does not need the cat.
("mouse" "needs" "cat" "-")
int1
The mouse visits the dog.
("mouse" "visits" "dog" "+")
int2
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int3
((((((triple3) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The mouse does not need the cat.
("mouse" "needs" "cat" "-")
int1
The mouse visits the dog.
("mouse" "visits" "dog" "+")
int2
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int3