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