The cat sees the mouse. The mouse is round. The tiger sees the mouse. If someone needs the mouse and the mouse likes the cat then the cat sees the mouse. If someone sees the tiger then the tiger is kind. If someone needs the tiger then the tiger is rough. If someone sees the tiger then they are round. If someone is rough then they do not need the mouse. If someone is round and they see the cat then the cat is round. If someone sees the mouse then they need the tiger. If the cat likes the mouse and the cat does not need the mouse then the mouse is kind.
The cat sees the mouse.
("cat" "sees" "mouse" "+")
The mouse is round.
("mouse" "is" "round" "+")
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
If someone needs the mouse and the mouse likes the cat then the cat sees the mouse.
((("someone" "needs" "mouse" "+") ("mouse" "likes" "cat" "+")) -> ("cat" "sees" "mouse" "+"))
If someone sees the tiger then the tiger is kind.
((("someone" "sees" "tiger" "+")) -> ("tiger" "is" "kind" "+"))
If someone needs the tiger then the tiger is rough.
((("someone" "needs" "tiger" "+")) -> ("tiger" "is" "rough" "+"))
If someone sees the tiger then they are round.
((("someone" "sees" "tiger" "+")) -> ("someone" "is" "round" "+"))
If someone is rough then they do not need the mouse.
((("someone" "is" "rough" "+")) -> ("someone" "needs" "mouse" "-"))
If someone is round and they see the cat then the cat is round.
((("someone" "is" "round" "+") ("someone" "sees" "cat" "+")) -> ("cat" "is" "round" "+"))
If someone sees the mouse then they need the tiger.
((("someone" "sees" "mouse" "+")) -> ("someone" "needs" "tiger" "+"))
If the cat likes the mouse and the cat does not need the mouse then the mouse is kind.
((("cat" "likes" "mouse" "+") ("cat" "needs" "mouse" "~")) -> ("mouse" "is" "kind" "+"))
The tiger sees the mouse.
True
1
proof
[(triple3)]
("tiger" "sees" "mouse" "+")
triple3
The cat does not see the mouse.
False
1
inv-proof
[(triple1)]
("cat" "sees" "mouse" "-")
triple1
The tiger needs the tiger.
True
2
proof
[(((triple3) -> rule7))]
("tiger" "needs" "tiger" "+")
((triple3) -> (rule7 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The cat does not need the tiger.
False
2
inv-proof
[(((triple1) -> rule7))]
("cat" "needs" "tiger" "-")
((triple1) -> (rule7 % int1))
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int1
The tiger is rough.
True
3
proof
[(((((triple1) -> rule7)) -> rule3) OR ((((triple3) -> rule7)) -> rule3))]
("tiger" "is" "rough" "+")
((((triple1) -> (rule7 % int2))) -> (rule3 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int2
((((triple3) -> (rule7 % int2))) -> (rule3 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int2
The tiger is not rough.
False
3
inv-proof
[(((((triple1) -> rule7)) -> rule3) OR ((((triple3) -> rule7)) -> rule3))]
("tiger" "is" "rough" "-")
((((triple1) -> (rule7 % int2))) -> (rule3 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int2
((((triple3) -> (rule7 % int2))) -> (rule3 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int2
The tiger does not need the mouse.
True
4
proof
[(((((((triple1) -> rule7)) -> rule3)) -> rule5) OR ((((((triple3) -> rule7)) -> rule3)) -> rule5))]
("tiger" "needs" "mouse" "-")
((((((triple1) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The tiger does not need the mouse.
("tiger" "needs" "mouse" "-")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
int2
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int3
((((((triple3) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The tiger does not need the mouse.
("tiger" "needs" "mouse" "-")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
int2
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int3
The tiger needs the mouse.
False
4
inv-proof
[(((((((triple1) -> rule7)) -> rule3)) -> rule5) OR ((((((triple3) -> rule7)) -> rule3)) -> rule5))]
("tiger" "needs" "mouse" "+")
((((((triple1) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The tiger does not need the mouse.
("tiger" "needs" "mouse" "-")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
int2
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int3
((((((triple3) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The tiger does not need the mouse.
("tiger" "needs" "mouse" "-")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
int2
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int3
The tiger is not kind.
Unknown
inv-rconc
[@1: The tiger is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "is" "kind" "-")
The mouse needs the tiger.
Unknown
rconc
[@1: The mouse needs the tiger.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("mouse" "needs" "tiger" "+")
The mouse is not kind.
Unknown
inv-rconc
[@1: The mouse is kind.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("mouse" "is" "kind" "-")
The tiger is round.
Unknown
rconc
[@1: The tiger is round.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("tiger" "is" "round" "+")
The mouse does not like the cat.
Unknown
inv-random
[@0: The mouse likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "cat" "-")
The cat likes the cat.
Unknown
random
[@0: The cat likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "cat" "+")
The tiger does not like the mouse.
Unknown
inv-random
[@0: The tiger likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "mouse" "-")
The mouse needs the mouse.
Unknown
random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "+")
@0: The cat sees the mouse.[(triple1)] The mouse is round.[(triple2)] The tiger sees the mouse.[(triple3)] @1: The cat needs the tiger.[(((triple1) -> rule7))] The tiger needs the tiger.[(((triple3) -> rule7))] @2: The tiger is rough.[(((((triple1) -> rule7)) -> rule3) OR ((((triple3) -> rule7)) -> rule3))] @3: The tiger does not need the mouse.[(((((((triple1) -> rule7)) -> rule3)) -> rule5) OR ((((((triple3) -> rule7)) -> rule3)) -> rule5))]
The cat sees the mouse.
("cat" "sees" "mouse" "+")
triple1
The mouse is round.
("mouse" "is" "round" "+")
triple2
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
triple3
The cat needs the tiger.
("cat" "needs" "tiger" "+")
((triple1) -> (rule7 % int1))
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int1
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
((triple3) -> (rule7 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
((((triple1) -> (rule7 % int2))) -> (rule3 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int2
((((triple3) -> (rule7 % int2))) -> (rule3 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int2
The tiger does not need the mouse.
("tiger" "needs" "mouse" "-")
((((((triple1) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The tiger does not need the mouse.
("tiger" "needs" "mouse" "-")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
int2
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int3
((((((triple3) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The tiger does not need the mouse.
("tiger" "needs" "mouse" "-")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
int2
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int3