The dog does not chase the lion. The lion is rough. The mouse is cold. The squirrel does not eat the dog. If something is rough and it sees the mouse then it chases the dog. If something sees the dog then the dog is not red. If the squirrel is kind and the squirrel eats the dog then the dog is kind. If the mouse eats the squirrel and the squirrel is nice then the squirrel is kind. If something chases the mouse then it is kind. Cold things are kind. Kind things are nice. If the mouse is nice then the mouse sees the lion.
The dog does not chase the lion.
("dog" "chases" "lion" "-")
The lion is rough.
("lion" "is" "rough" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The squirrel does not eat the dog.
("squirrel" "eats" "dog" "-")
If something is rough and it sees the mouse then it chases the dog.
((("something" "is" "rough" "+") ("something" "sees" "mouse" "+")) -> ("something" "chases" "dog" "+"))
If something sees the dog then the dog is not red.
((("something" "sees" "dog" "+")) -> ("dog" "is" "red" "-"))
If the squirrel is kind and the squirrel eats the dog then the dog is kind.
((("squirrel" "is" "kind" "+") ("squirrel" "eats" "dog" "+")) -> ("dog" "is" "kind" "+"))
If the mouse eats the squirrel and the squirrel is nice then the squirrel is kind.
((("mouse" "eats" "squirrel" "+") ("squirrel" "is" "nice" "+")) -> ("squirrel" "is" "kind" "+"))
If something chases the mouse then it is kind.
((("something" "chases" "mouse" "+")) -> ("something" "is" "kind" "+"))
Cold things are kind.
((("something" "is" "cold" "+")) -> ("something" "is" "kind" "+"))
Kind things are nice.
((("something" "is" "kind" "+")) -> ("something" "is" "nice" "+"))
If the mouse is nice then the mouse sees the lion.
((("mouse" "is" "nice" "+")) -> ("mouse" "sees" "lion" "+"))
The mouse is cold.
True
1
proof
[(triple3)]
("mouse" "is" "cold" "+")
triple3
The mouse is not cold.
False
1
inv-proof
[(triple3)]
("mouse" "is" "cold" "-")
triple3
The mouse is kind.
True
2
proof
[(((triple3) -> rule6))]
("mouse" "is" "kind" "+")
((triple3) -> (rule6 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The mouse is not kind.
False
2
inv-proof
[(((triple3) -> rule6))]
("mouse" "is" "kind" "-")
((triple3) -> (rule6 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The mouse is nice.
True
3
proof
[(((((triple3) -> rule6)) -> rule7))]
("mouse" "is" "nice" "+")
((((triple3) -> (rule6 % int2))) -> (rule7 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
The mouse is not nice.
False
3
inv-proof
[(((((triple3) -> rule6)) -> rule7))]
("mouse" "is" "nice" "-")
((((triple3) -> (rule6 % int2))) -> (rule7 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
The mouse sees the lion.
True
4
proof
[(((((((triple3) -> rule6)) -> rule7)) -> rule8))]
("mouse" "sees" "lion" "+")
((((((triple3) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The mouse is kind.
("mouse" "is" "kind" "+")
int3
The mouse does not see the lion.
False
4
inv-proof
[(((((((triple3) -> rule6)) -> rule7)) -> rule8))]
("mouse" "sees" "lion" "-")
((((((triple3) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The mouse is kind.
("mouse" "is" "kind" "+")
int3
The lion is not nice.
Unknown
inv-rconc
[@2: The lion is nice.[CWA. Example of deepest failure = (rule7 <- rule5 <- FAIL)]]
("lion" "is" "nice" "-")
The squirrel is nice.
Unknown
rconc
[@2: The squirrel is nice.[CWA. Example of deepest failure = (rule7 <- rule4 <- FAIL)]]
("squirrel" "is" "nice" "+")
The lion is not kind.
Unknown
inv-rconc
[@1: The lion is kind.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("lion" "is" "kind" "-")
The squirrel is kind.
Unknown
rconc
[@1: The squirrel is kind.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("squirrel" "is" "kind" "+")
The mouse does not eat the mouse.
Unknown
inv-random
[@0: The mouse eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "mouse" "-")
The dog chases the mouse.
Unknown
random
[@0: The dog chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "mouse" "+")
The squirrel does not eat the mouse.
Unknown
inv-random
[@0: The squirrel eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "mouse" "-")
The lion chases the lion.
Unknown
random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "+")
@0: The dog does not chase the lion.[(triple1)] The lion is rough.[(triple2)] The mouse is cold.[(triple3)] The squirrel does not eat the dog.[(triple4)] @1: The mouse is kind.[(((triple3) -> rule6))] @2: The mouse is nice.[(((((triple3) -> rule6)) -> rule7))] @3: The mouse sees the lion.[(((((((triple3) -> rule6)) -> rule7)) -> rule8))]
The dog does not chase the lion.
("dog" "chases" "lion" "-")
triple1
The lion is rough.
("lion" "is" "rough" "+")
triple2
The mouse is cold.
("mouse" "is" "cold" "+")
triple3
The squirrel does not eat the dog.
("squirrel" "eats" "dog" "-")
triple4
The mouse is kind.
("mouse" "is" "kind" "+")
((triple3) -> (rule6 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
((((triple3) -> (rule6 % int2))) -> (rule7 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
The mouse sees the lion.
("mouse" "sees" "lion" "+")
((((((triple3) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The mouse is kind.
("mouse" "is" "kind" "+")
int3