The cat chases the tiger. The mouse is big. The squirrel needs the mouse. The tiger chases the squirrel. If someone eats the mouse then they eat the cat. If someone chases the tiger then the tiger eats the squirrel. If someone eats the squirrel then the squirrel does not chase the tiger.
The cat chases the tiger.
("cat" "chases" "tiger" "+")
The mouse is big.
("mouse" "is" "big" "+")
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
If someone eats the mouse then they eat the cat.
((("someone" "eats" "mouse" "+")) -> ("someone" "eats" "cat" "+"))
If someone chases the tiger then the tiger eats the squirrel.
((("someone" "chases" "tiger" "+")) -> ("tiger" "eats" "squirrel" "+"))
If someone eats the squirrel then the squirrel does not chase the tiger.
((("someone" "eats" "squirrel" "+")) -> ("squirrel" "chases" "tiger" "-"))
The squirrel needs the mouse.
True
1
proof
[(triple3)]
("squirrel" "needs" "mouse" "+")
triple3
The cat does not chase the tiger.
False
1
inv-proof
[(triple1)]
("cat" "chases" "tiger" "-")
triple1
The tiger eats the squirrel.
True
2
proof
[(((triple1) -> rule2))]
("tiger" "eats" "squirrel" "+")
((triple1) -> (rule2 % int1))
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int1
The tiger does not eat the squirrel.
False
2
inv-proof
[(((triple1) -> rule2))]
("tiger" "eats" "squirrel" "-")
((triple1) -> (rule2 % int1))
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int1
The squirrel does not chase the tiger.
True
3
proof
[(((((triple1) -> rule2)) -> rule3))]
("squirrel" "chases" "tiger" "-")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The squirrel does not chase the tiger.
("squirrel" "chases" "tiger" "-")
int1
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int2
The squirrel chases the tiger.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule3))]
("squirrel" "chases" "tiger" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The squirrel does not chase the tiger.
("squirrel" "chases" "tiger" "-")
int1
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int2
The cat does not eat the cat.
Unknown
inv-rconc
[@1: The cat eats the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "eats" "cat" "-")
The mouse eats the cat.
Unknown
rconc
[@1: The mouse eats the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "eats" "cat" "+")
The tiger does not eat the cat.
Unknown
inv-rconc
[@1: The tiger eats the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "eats" "cat" "-")
The tiger eats the mouse.
Unknown
random
[@0: The tiger eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "mouse" "+")
The cat is not big.
Unknown
inv-random
[@0: The cat is big.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "big" "-")
The tiger is young.
Unknown
random
[@0: The tiger is young.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "young" "+")
@0: The cat chases the tiger.[(triple1)] The mouse is big.[(triple2)] The squirrel needs the mouse.[(triple3)] The tiger chases the squirrel.[(triple4)] @1: The tiger eats the squirrel.[(((triple1) -> rule2))] @2: The squirrel does not chase the tiger.[(((((triple1) -> rule2)) -> rule3))]
The cat chases the tiger.
("cat" "chases" "tiger" "+")
triple1
The mouse is big.
("mouse" "is" "big" "+")
triple2
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
triple3
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
triple4
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
((triple1) -> (rule2 % int1))
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int1
The squirrel does not chase the tiger.
("squirrel" "chases" "tiger" "-")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The squirrel does not chase the tiger.
("squirrel" "chases" "tiger" "-")
int1
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int2