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