The dog eats the mouse. The dog needs the tiger. The mouse is blue. The mouse needs the tiger. The tiger eats the dog. The tiger eats the mouse. The tiger likes the dog. The tiger likes the mouse. The tiger needs the dog. The tiger needs the mouse. If someone needs the mouse and they eat the dog then the mouse needs the dog. If someone likes the tiger then the tiger is nice. If someone is blue then they like the tiger.
The dog eats the mouse.
("dog" "eats" "mouse" "+")
The dog needs the tiger.
("dog" "needs" "tiger" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
The tiger eats the dog.
("tiger" "eats" "dog" "+")
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
The tiger likes the dog.
("tiger" "likes" "dog" "+")
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
The tiger needs the dog.
("tiger" "needs" "dog" "+")
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
If someone needs the mouse and they eat the dog then the mouse needs the dog.
((("someone" "needs" "mouse" "+") ("someone" "eats" "dog" "+")) -> ("mouse" "needs" "dog" "+"))
If someone likes the tiger then the tiger is nice.
((("someone" "likes" "tiger" "+")) -> ("tiger" "is" "nice" "+"))
If someone is blue then they like the tiger.
((("someone" "is" "blue" "+")) -> ("someone" "likes" "tiger" "+"))
The dog eats the mouse.
True
1
proof
[(triple1)]
("dog" "eats" "mouse" "+")
triple1
The tiger does not like the mouse.
False
1
inv-proof
[(triple8)]
("tiger" "likes" "mouse" "-")
triple8
The mouse likes the tiger.
True
2
proof
[(((triple3) -> rule3))]
("mouse" "likes" "tiger" "+")
((triple3) -> (rule3 % int1))
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int1
The mouse does not like the tiger.
False
2
inv-proof
[(((triple3) -> rule3))]
("mouse" "likes" "tiger" "-")
((triple3) -> (rule3 % int1))
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int1
The tiger is nice.
True
3
proof
[(((((triple3) -> rule3)) -> rule2))]
("tiger" "is" "nice" "+")
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int2
The tiger is not nice.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule2))]
("tiger" "is" "nice" "-")
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int2
The tiger does not like the tiger.
Unknown
inv-rconc
[@1: The tiger likes the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "likes" "tiger" "-")
The dog likes the tiger.
Unknown
rconc
[@1: The dog likes the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "likes" "tiger" "+")
The dog does not need the mouse.
Unknown
inv-random
[@0: The dog needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "mouse" "-")
The mouse is round.
Unknown
random
[@0: The mouse is round.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "round" "+")
The dog is not blue.
Unknown
inv-random
[@0: The dog is blue.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "blue" "-")
The mouse eats the tiger.
Unknown
random
[@0: The mouse eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "tiger" "+")
@0: The dog eats the mouse.[(triple1)] The dog needs the tiger.[(triple2)] The mouse is blue.[(triple3)] The mouse needs the tiger.[(triple4)] The tiger eats the dog.[(triple5)] The tiger eats the mouse.[(triple6)] The tiger likes the dog.[(triple7)] The tiger likes the mouse.[(triple8)] The tiger needs the dog.[(triple9)] The tiger needs the mouse.[(triple10)] @1: The mouse likes the tiger.[(((triple3) -> rule3))] The mouse needs the dog.[(((triple10 triple5) -> rule1))] @2: The tiger is nice.[(((((triple3) -> rule3)) -> rule2))]
The dog eats the mouse.
("dog" "eats" "mouse" "+")
triple1
The dog needs the tiger.
("dog" "needs" "tiger" "+")
triple2
The mouse is blue.
("mouse" "is" "blue" "+")
triple3
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
triple4
The tiger eats the dog.
("tiger" "eats" "dog" "+")
triple5
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
triple6
The tiger likes the dog.
("tiger" "likes" "dog" "+")
triple7
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
triple8
The tiger needs the dog.
("tiger" "needs" "dog" "+")
triple9
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
triple10
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
((triple3) -> (rule3 % int1))
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int1
The mouse needs the dog.
("mouse" "needs" "dog" "+")
((triple10 triple5) -> (rule1 % int1))
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int2