The dog likes the mouse. The mouse eats the tiger. The squirrel eats the dog. The tiger is round. If someone eats the tiger then they eat the squirrel. If someone eats the squirrel then the squirrel eats the tiger.
The dog likes the mouse.
("dog" "likes" "mouse" "+")
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
The tiger is round.
("tiger" "is" "round" "+")
If someone eats the tiger then they eat the squirrel.
((("someone" "eats" "tiger" "+")) -> ("someone" "eats" "squirrel" "+"))
If someone eats the squirrel then the squirrel eats the tiger.
((("someone" "eats" "squirrel" "+")) -> ("squirrel" "eats" "tiger" "+"))
The squirrel eats the dog.
True
1
proof
[(triple3)]
("squirrel" "eats" "dog" "+")
triple3
The tiger is not round.
False
1
inv-proof
[(triple4)]
("tiger" "is" "round" "-")
triple4
The mouse eats the squirrel.
True
2
proof
[(((triple2) -> rule1))]
("mouse" "eats" "squirrel" "+")
((triple2) -> (rule1 % int1))
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
int1
The mouse does not eat the squirrel.
False
2
inv-proof
[(((triple2) -> rule1))]
("mouse" "eats" "squirrel" "-")
((triple2) -> (rule1 % int1))
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
int1
The squirrel eats the tiger.
True
3
proof
[(((((triple2) -> rule1)) -> rule2))]
("squirrel" "eats" "tiger" "+")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
int1
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
int2
The squirrel does not eat the tiger.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule2))]
("squirrel" "eats" "tiger" "-")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
int1
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
int2
The squirrel eats the squirrel.
True
4
proof
[(((((((triple2) -> rule1)) -> rule2)) -> rule1))]
("squirrel" "eats" "squirrel" "+")
((((((triple2) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int1
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
int2
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
int3
The squirrel does not eat the squirrel.
False
4
inv-proof
[(((((((triple2) -> rule1)) -> rule2)) -> rule1))]
("squirrel" "eats" "squirrel" "-")
((((((triple2) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int1
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
int2
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
int3
The dog does not eat the squirrel.
Unknown
inv-rconc
[@1: The dog eats the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "eats" "squirrel" "-")
The tiger eats the squirrel.
Unknown
rconc
[@1: The tiger eats the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "eats" "squirrel" "+")
The dog is not big.
Unknown
inv-random
[@0: The dog is big.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "big" "-")
The dog is round.
Unknown
random
[@0: The dog is round.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "round" "+")
The squirrel does not see the dog.
Unknown
inv-random
[@0: The squirrel sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "dog" "-")
The dog likes the tiger.
Unknown
random
[@0: The dog likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "tiger" "+")
The dog does not like the dog.
Unknown
inv-random
[@0: The dog likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "dog" "-")
The tiger likes the tiger.
Unknown
random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "+")
@0: The dog likes the mouse.[(triple1)] The mouse eats the tiger.[(triple2)] The squirrel eats the dog.[(triple3)] The tiger is round.[(triple4)] @1: The mouse eats the squirrel.[(((triple2) -> rule1))] @2: The squirrel eats the tiger.[(((((triple2) -> rule1)) -> rule2))] @3: The squirrel eats the squirrel.[(((((((triple2) -> rule1)) -> rule2)) -> rule1))]
The dog likes the mouse.
("dog" "likes" "mouse" "+")
triple1
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
triple2
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
triple3
The tiger is round.
("tiger" "is" "round" "+")
triple4
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
((triple2) -> (rule1 % int1))
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
int1
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
int1
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
int2
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
((((((triple2) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int1
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
int2
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
int3