The cat is kind. The dog visits the cat. The mouse chases the dog. If something visits the cat and it is kind then the cat eats the dog. If something eats the dog and it visits the dog then the dog is kind. If something is blue and kind then it chases the mouse. If the mouse eats the cat and the mouse chases the cat then the mouse is round. If something visits the dog then it eats the dog. If something chases the dog then it visits the dog.
The cat is kind.
("cat" "is" "kind" "+")
The dog visits the cat.
("dog" "visits" "cat" "+")
The mouse chases the dog.
("mouse" "chases" "dog" "+")
If something visits the cat and it is kind then the cat eats the dog.
((("something" "visits" "cat" "+") ("something" "is" "kind" "+")) -> ("cat" "eats" "dog" "+"))
If something eats the dog and it visits the dog then the dog is kind.
((("something" "eats" "dog" "+") ("something" "visits" "dog" "+")) -> ("dog" "is" "kind" "+"))
If something is blue and kind then it chases the mouse.
((("something" "is" "blue" "+") ("something" "is" "kind" "+")) -> ("something" "chases" "mouse" "+"))
If the mouse eats the cat and the mouse chases the cat then the mouse is round.
((("mouse" "eats" "cat" "+") ("mouse" "chases" "cat" "+")) -> ("mouse" "is" "round" "+"))
If something visits the dog then it eats the dog.
((("something" "visits" "dog" "+")) -> ("something" "eats" "dog" "+"))
If something chases the dog then it visits the dog.
((("something" "chases" "dog" "+")) -> ("something" "visits" "dog" "+"))
The cat is kind.
True
1
proof
[(triple1)]
("cat" "is" "kind" "+")
triple1
The dog does not visit the cat.
False
1
inv-proof
[(triple2)]
("dog" "visits" "cat" "-")
triple2
The mouse visits the dog.
True
2
proof
[(((triple3) -> rule6))]
("mouse" "visits" "dog" "+")
((triple3) -> (rule6 % int1))
The mouse visits the dog.
("mouse" "visits" "dog" "+")
int1
The mouse does not visit the dog.
False
2
inv-proof
[(((triple3) -> rule6))]
("mouse" "visits" "dog" "-")
((triple3) -> (rule6 % int1))
The mouse visits the dog.
("mouse" "visits" "dog" "+")
int1
The mouse eats the dog.
True
3
proof
[(((((triple3) -> rule6)) -> rule5))]
("mouse" "eats" "dog" "+")
((((triple3) -> (rule6 % int2))) -> (rule5 % int1))
The mouse eats the dog.
("mouse" "eats" "dog" "+")
int1
The mouse visits the dog.
("mouse" "visits" "dog" "+")
int2
The mouse does not eat the dog.
False
3
inv-proof
[(((((triple3) -> rule6)) -> rule5))]
("mouse" "eats" "dog" "-")
((((triple3) -> (rule6 % int2))) -> (rule5 % int1))
The mouse eats the dog.
("mouse" "eats" "dog" "+")
int1
The mouse visits the dog.
("mouse" "visits" "dog" "+")
int2
The dog is kind.
True
6
proof
[(((((((triple3) -> rule6)) -> rule5) ((triple3) -> rule6)) -> rule2))]
("dog" "is" "kind" "+")
((((((triple3) -> (rule6 % int3))) -> (rule5 % int2)) ((triple3) -> (rule6 % int3))) -> (rule2 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The mouse eats the dog.
("mouse" "eats" "dog" "+")
int2
The mouse visits the dog.
("mouse" "visits" "dog" "+")
int3
The dog is not kind.
False
6
inv-proof
[(((((((triple3) -> rule6)) -> rule5) ((triple3) -> rule6)) -> rule2))]
("dog" "is" "kind" "-")
((((((triple3) -> (rule6 % int3))) -> (rule5 % int2)) ((triple3) -> (rule6 % int3))) -> (rule2 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The mouse eats the dog.
("mouse" "eats" "dog" "+")
int2
The mouse visits the dog.
("mouse" "visits" "dog" "+")
int3
The dog does not chase the mouse.
Unknown
inv-rconc
[@1: The dog chases the mouse.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "chases" "mouse" "-")
The mouse is round.
Unknown
rconc
[@1: The mouse is round.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "is" "round" "+")
The mouse does not chase the mouse.
Unknown
inv-rconc
[@1: The mouse chases the mouse.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "chases" "mouse" "-")
The dog visits the dog.
Unknown
rconc
[@1: The dog visits the dog.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "visits" "dog" "+")
The cat does not eat the mouse.
Unknown
inv-random
[@0: The cat eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "mouse" "-")
The dog visits the mouse.
Unknown
random
[@0: The dog visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "mouse" "+")
The dog does not eat the mouse.
Unknown
inv-random
[@0: The dog eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "mouse" "-")
The mouse chases the cat.
Unknown
random
[@0: The mouse chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "cat" "+")
@0: The cat is kind.[(triple1)] The dog visits the cat.[(triple2)] The mouse chases the dog.[(triple3)] @1: The mouse visits the dog.[(((triple3) -> rule6))] @2: The mouse eats the dog.[(((((triple3) -> rule6)) -> rule5))] @3: The dog is kind.[(((((((triple3) -> rule6)) -> rule5) ((triple3) -> rule6)) -> rule2))] @4: The cat eats the dog.[(((triple2 ((((((triple3) -> rule6)) -> rule5) ((triple3) -> rule6)) -> rule2)) -> rule1))]
The cat is kind.
("cat" "is" "kind" "+")
triple1
The dog visits the cat.
("dog" "visits" "cat" "+")
triple2
The mouse chases the dog.
("mouse" "chases" "dog" "+")
triple3
The mouse visits the dog.
("mouse" "visits" "dog" "+")
((triple3) -> (rule6 % int1))
The mouse visits the dog.
("mouse" "visits" "dog" "+")
int1
The mouse eats the dog.
("mouse" "eats" "dog" "+")
((((triple3) -> (rule6 % int2))) -> (rule5 % int1))
The mouse eats the dog.
("mouse" "eats" "dog" "+")
int1
The mouse visits the dog.
("mouse" "visits" "dog" "+")
int2
The dog is kind.
("dog" "is" "kind" "+")
((((((triple3) -> (rule6 % int3))) -> (rule5 % int2)) ((triple3) -> (rule6 % int3))) -> (rule2 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The mouse eats the dog.
("mouse" "eats" "dog" "+")
int2
The mouse visits the dog.
("mouse" "visits" "dog" "+")
int3
The cat eats the dog.
("cat" "eats" "dog" "+")
((triple2 ((((((triple3) -> (rule6 % int4))) -> (rule5 % int3)) ((triple3) -> (rule6 % int4))) -> (rule2 % int2))) -> (rule1 % int1))
The cat eats the dog.
("cat" "eats" "dog" "+")
int1
The dog is kind.
("dog" "is" "kind" "+")
int2
The mouse eats the dog.
("mouse" "eats" "dog" "+")
int3
The mouse visits the dog.
("mouse" "visits" "dog" "+")
int4