The dog chases the tiger. The mouse chases the rabbit. The rabbit is blue. The tiger is not nice. If someone chases the tiger then they chase the mouse. If someone chases the mouse then the mouse chases the tiger. If someone is green then they do not chase the tiger. If the rabbit needs the mouse and the rabbit does not like the mouse then the rabbit is blue. If someone likes the rabbit and the rabbit likes the mouse then the mouse is not blue. If someone likes the tiger then the tiger is nice.
The dog chases the tiger.
("dog" "chases" "tiger" "+")
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The tiger is not nice.
("tiger" "is" "nice" "-")
If someone chases the tiger then they chase the mouse.
((("someone" "chases" "tiger" "+")) -> ("someone" "chases" "mouse" "+"))
If someone chases the mouse then the mouse chases the tiger.
((("someone" "chases" "mouse" "+")) -> ("mouse" "chases" "tiger" "+"))
If someone is green then they do not chase the tiger.
((("someone" "is" "green" "+")) -> ("someone" "chases" "tiger" "-"))
If the rabbit needs the mouse and the rabbit does not like the mouse then the rabbit is blue.
((("rabbit" "needs" "mouse" "+") ("rabbit" "likes" "mouse" "~")) -> ("rabbit" "is" "blue" "+"))
If someone likes the rabbit and the rabbit likes the mouse then the mouse is not blue.
((("someone" "likes" "rabbit" "+") ("rabbit" "likes" "mouse" "+")) -> ("mouse" "is" "blue" "-"))
If someone likes the tiger then the tiger is nice.
((("someone" "likes" "tiger" "+")) -> ("tiger" "is" "nice" "+"))
The rabbit is blue.
True
1
proof
[(triple3)]
("rabbit" "is" "blue" "+")
triple3
The tiger is nice.
False
1
inv-proof
[(triple4)]
("tiger" "is" "nice" "+")
triple4
The dog chases the mouse.
True
2
proof
[(((triple1) -> rule1))]
("dog" "chases" "mouse" "+")
((triple1) -> (rule1 % int1))
The dog chases the mouse.
("dog" "chases" "mouse" "+")
int1
The dog does not chase the mouse.
False
2
inv-proof
[(((triple1) -> rule1))]
("dog" "chases" "mouse" "-")
((triple1) -> (rule1 % int1))
The dog chases the mouse.
("dog" "chases" "mouse" "+")
int1
The mouse chases the tiger.
True
3
proof
[(((((triple1) -> rule1)) -> rule2))]
("mouse" "chases" "tiger" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
int1
The dog chases the mouse.
("dog" "chases" "mouse" "+")
int2
The mouse does not chase the tiger.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule2))]
("mouse" "chases" "tiger" "-")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
int1
The dog chases the mouse.
("dog" "chases" "mouse" "+")
int2
The mouse chases the mouse.
True
4
proof
[(((((((triple1) -> rule1)) -> rule2)) -> rule1))]
("mouse" "chases" "mouse" "+")
((((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
int2
The dog chases the mouse.
("dog" "chases" "mouse" "+")
int3
The mouse does not chase the mouse.
False
4
inv-proof
[(((((((triple1) -> rule1)) -> rule2)) -> rule1))]
("mouse" "chases" "mouse" "-")
((((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
int2
The dog chases the mouse.
("dog" "chases" "mouse" "+")
int3
The tiger does not chase the mouse.
Unknown
inv-rconc
[@1: The tiger chases the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "chases" "mouse" "-")
The rabbit chases the mouse.
Unknown
rconc
[@1: The rabbit chases the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "chases" "mouse" "+")
The dog is not blue.
Unknown
inv-random
[@0: The dog is blue.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "blue" "-")
The tiger is big.
Unknown
random
[@0: The tiger is big.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "big" "+")
The tiger does not need the dog.
Unknown
inv-random
[@0: The tiger needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "dog" "-")
The mouse is blue.
Unknown
random
[@0: The mouse is blue.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "blue" "+")
The rabbit does not chase the tiger.
Unknown
inv-random
[@0: The rabbit chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "tiger" "-")
The mouse chases the dog.
Unknown
random
[@0: The mouse chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "dog" "+")
@0: The dog chases the tiger.[(triple1)] The mouse chases the rabbit.[(triple2)] The rabbit is blue.[(triple3)] The tiger is not nice.[(triple4)] @1: The dog chases the mouse.[(((triple1) -> rule1))] @2: The mouse chases the tiger.[(((((triple1) -> rule1)) -> rule2))] @3: The mouse chases the mouse.[(((((((triple1) -> rule1)) -> rule2)) -> rule1))]
The dog chases the tiger.
("dog" "chases" "tiger" "+")
triple1
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
triple2
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple3
The tiger is not nice.
("tiger" "is" "nice" "-")
triple4
The dog chases the mouse.
("dog" "chases" "mouse" "+")
((triple1) -> (rule1 % int1))
The dog chases the mouse.
("dog" "chases" "mouse" "+")
int1
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
int1
The dog chases the mouse.
("dog" "chases" "mouse" "+")
int2
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
((((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
int2
The dog chases the mouse.
("dog" "chases" "mouse" "+")
int3