The dog chases the tiger. The mouse eats the tiger. The squirrel eats the tiger. The tiger is round. If someone needs the tiger then the tiger is cold. If someone is round then they eat the mouse. If someone is round then they do not eat the squirrel. If someone is rough then they are kind. If the tiger eats the mouse then the tiger is kind. If someone chases the mouse then the mouse needs the squirrel. If someone chases the squirrel then the squirrel is not round. If someone is kind and round then they do not need the dog.
The dog chases the tiger.
("dog" "chases" "tiger" "+")
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
The tiger is round.
("tiger" "is" "round" "+")
If someone needs the tiger then the tiger is cold.
((("someone" "needs" "tiger" "+")) -> ("tiger" "is" "cold" "+"))
If someone is round then they eat the mouse.
((("someone" "is" "round" "+")) -> ("someone" "eats" "mouse" "+"))
If someone is round then they do not eat the squirrel.
((("someone" "is" "round" "+")) -> ("someone" "eats" "squirrel" "-"))
If someone is rough then they are kind.
((("someone" "is" "rough" "+")) -> ("someone" "is" "kind" "+"))
If the tiger eats the mouse then the tiger is kind.
((("tiger" "eats" "mouse" "+")) -> ("tiger" "is" "kind" "+"))
If someone chases the mouse then the mouse needs the squirrel.
((("someone" "chases" "mouse" "+")) -> ("mouse" "needs" "squirrel" "+"))
If someone chases the squirrel then the squirrel is not round.
((("someone" "chases" "squirrel" "+")) -> ("squirrel" "is" "round" "-"))
If someone is kind and round then they do not need the dog.
((("someone" "is" "kind" "+") ("someone" "is" "round" "+")) -> ("someone" "needs" "dog" "-"))
The mouse eats the tiger.
True
1
proof
[(triple2)]
("mouse" "eats" "tiger" "+")
triple2
The tiger is not round.
False
1
inv-proof
[(triple4)]
("tiger" "is" "round" "-")
triple4
The tiger eats the mouse.
True
2
proof
[(((triple4) -> rule2))]
("tiger" "eats" "mouse" "+")
((triple4) -> (rule2 % int1))
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int1
The tiger does not eat the mouse.
False
2
inv-proof
[(((triple4) -> rule2))]
("tiger" "eats" "mouse" "-")
((triple4) -> (rule2 % int1))
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int1
The tiger is kind.
True
3
proof
[(((((triple4) -> rule2)) -> rule5))]
("tiger" "is" "kind" "+")
((((triple4) -> (rule2 % int2))) -> (rule5 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int2
The tiger is not kind.
False
3
inv-proof
[(((((triple4) -> rule2)) -> rule5))]
("tiger" "is" "kind" "-")
((((triple4) -> (rule2 % int2))) -> (rule5 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int2
The tiger does not need the dog.
True
5
proof
[(((((((triple4) -> rule2)) -> rule5) triple4) -> rule8))]
("tiger" "needs" "dog" "-")
((((((triple4) -> (rule2 % int3))) -> (rule5 % int2)) triple4) -> (rule8 % int1))
The tiger does not need the dog.
("tiger" "needs" "dog" "-")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
int2
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int3
The tiger needs the dog.
False
5
inv-proof
[(((((((triple4) -> rule2)) -> rule5) triple4) -> rule8))]
("tiger" "needs" "dog" "+")
((((((triple4) -> (rule2 % int3))) -> (rule5 % int2)) triple4) -> (rule8 % int1))
The tiger does not need the dog.
("tiger" "needs" "dog" "-")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
int2
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int3
The mouse is not kind.
Unknown
inv-rconc
[@1: The mouse is kind.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "is" "kind" "-")
The squirrel eats the mouse.
Unknown
rconc
[@1: The squirrel eats the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "eats" "mouse" "+")
The squirrel is not kind.
Unknown
inv-rconc
[@1: The squirrel is kind.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("squirrel" "is" "kind" "-")
The tiger is cold.
Unknown
rconc
[@1: The tiger is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "is" "cold" "+")
The dog does not eat the squirrel.
Unknown
inv-random
[@0: The dog eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "squirrel" "-")
The tiger needs the tiger.
Unknown
random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "+")
The dog is not rough.
Unknown
inv-random
[@0: The dog is rough.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "rough" "-")
The mouse needs the dog.
Unknown
random
[@0: The mouse needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "dog" "+")
@0: The dog chases the tiger.[(triple1)] The mouse eats the tiger.[(triple2)] The squirrel eats the tiger.[(triple3)] The tiger is round.[(triple4)] @1: The tiger does not eat the squirrel.[(((triple4) -> rule3))] The tiger eats the mouse.[(((triple4) -> rule2))] @2: The tiger is kind.[(((((triple4) -> rule2)) -> rule5))] @3: The tiger does not need the dog.[(((((((triple4) -> rule2)) -> rule5) triple4) -> rule8))]
The dog chases the tiger.
("dog" "chases" "tiger" "+")
triple1
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
triple2
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
triple3
The tiger is round.
("tiger" "is" "round" "+")
triple4
The tiger does not eat the squirrel.
("tiger" "eats" "squirrel" "-")
((triple4) -> (rule3 % int1))
The tiger does not eat the squirrel.
("tiger" "eats" "squirrel" "-")
int1
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
((triple4) -> (rule2 % int1))
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
((((triple4) -> (rule2 % int2))) -> (rule5 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int2
The tiger does not need the dog.
("tiger" "needs" "dog" "-")
((((((triple4) -> (rule2 % int3))) -> (rule5 % int2)) triple4) -> (rule8 % int1))
The tiger does not need the dog.
("tiger" "needs" "dog" "-")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
int2
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int3