The cat chases the mouse. The dog is not round. The mouse visits the dog. If someone needs the mouse then the mouse does not chase the dog. If someone is big and they chase the dog then the dog chases the cat. If someone is kind and they visit the cat then the cat does not visit the dog. If someone visits the dog then the dog chases the mouse. If someone chases the mouse then they do not chase the dog. If someone is big then they chase the cat.
The cat chases the mouse.
("cat" "chases" "mouse" "+")
The dog is not round.
("dog" "is" "round" "-")
The mouse visits the dog.
("mouse" "visits" "dog" "+")
If someone needs the mouse then the mouse does not chase the dog.
((("someone" "needs" "mouse" "+")) -> ("mouse" "chases" "dog" "-"))
If someone is big and they chase the dog then the dog chases the cat.
((("someone" "is" "big" "+") ("someone" "chases" "dog" "+")) -> ("dog" "chases" "cat" "+"))
If someone is kind and they visit the cat then the cat does not visit the dog.
((("someone" "is" "kind" "+") ("someone" "visits" "cat" "+")) -> ("cat" "visits" "dog" "-"))
If someone visits the dog then the dog chases the mouse.
((("someone" "visits" "dog" "+")) -> ("dog" "chases" "mouse" "+"))
If someone chases the mouse then they do not chase the dog.
((("someone" "chases" "mouse" "+")) -> ("someone" "chases" "dog" "-"))
If someone is big then they chase the cat.
((("someone" "is" "big" "+")) -> ("someone" "chases" "cat" "+"))
The dog is not round.
True
1
proof
[(triple2)]
("dog" "is" "round" "-")
triple2
The dog is round.
False
1
inv-proof
[(triple2)]
("dog" "is" "round" "+")
triple2
The dog chases the mouse.
True
2
proof
[(((triple3) -> rule4))]
("dog" "chases" "mouse" "+")
((triple3) -> (rule4 % int1))
The dog chases the mouse.
("dog" "chases" "mouse" "+")
int1
The dog does not chase the mouse.
False
2
inv-proof
[(((triple3) -> rule4))]
("dog" "chases" "mouse" "-")
((triple3) -> (rule4 % int1))
The dog chases the mouse.
("dog" "chases" "mouse" "+")
int1
The dog does not chase the dog.
True
3
proof
[(((((triple3) -> rule4)) -> rule5))]
("dog" "chases" "dog" "-")
((((triple3) -> (rule4 % int2))) -> (rule5 % int1))
The dog does not chase the dog.
("dog" "chases" "dog" "-")
int1
The dog chases the mouse.
("dog" "chases" "mouse" "+")
int2
The dog chases the dog.
False
3
inv-proof
[(((((triple3) -> rule4)) -> rule5))]
("dog" "chases" "dog" "+")
((((triple3) -> (rule4 % int2))) -> (rule5 % int1))
The dog does not chase the dog.
("dog" "chases" "dog" "-")
int1
The dog chases the mouse.
("dog" "chases" "mouse" "+")
int2
The dog does not chase the cat.
Unknown
inv-rconc
[@1: The dog chases the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "chases" "cat" "-")
The cat chases the cat.
Unknown
rconc
[@1: The cat chases the cat.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cat" "chases" "cat" "+")
The mouse does not chase the cat.
Unknown
inv-rconc
[@1: The mouse chases the cat.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("mouse" "chases" "cat" "-")
The cat needs the mouse.
Unknown
random
[@0: The cat needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "mouse" "+")
The dog is not kind.
Unknown
inv-random
[@0: The dog is kind.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "kind" "-")
The cat needs the dog.
Unknown
random
[@0: The cat needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "dog" "+")
@0: The cat chases the mouse.[(triple1)] The dog is not round.[(triple2)] The mouse visits the dog.[(triple3)] @1: The cat does not chase the dog.[(((triple1) -> rule5))] The dog chases the mouse.[(((triple3) -> rule4))] @2: The dog does not chase the dog.[(((((triple3) -> rule4)) -> rule5))]
The cat chases the mouse.
("cat" "chases" "mouse" "+")
triple1
The dog is not round.
("dog" "is" "round" "-")
triple2
The mouse visits the dog.
("mouse" "visits" "dog" "+")
triple3
The cat does not chase the dog.
("cat" "chases" "dog" "-")
((triple1) -> (rule5 % int1))
The cat does not chase the dog.
("cat" "chases" "dog" "-")
int1
The dog chases the mouse.
("dog" "chases" "mouse" "+")
((triple3) -> (rule4 % int1))
The dog chases the mouse.
("dog" "chases" "mouse" "+")
int1
The dog does not chase the dog.
("dog" "chases" "dog" "-")
((((triple3) -> (rule4 % int2))) -> (rule5 % int1))
The dog does not chase the dog.
("dog" "chases" "dog" "-")
int1
The dog chases the mouse.
("dog" "chases" "mouse" "+")
int2