The dog is big. The dog visits the rabbit. The lion chases the mouse. The lion is not cold. The mouse chases the lion. The mouse does not chase the rabbit. The mouse visits the dog. The rabbit is cold. The rabbit sees the lion. The rabbit visits the lion. All cold things are kind. If the lion sees the rabbit and the rabbit visits the mouse then the lion chases the dog.
The dog is big.
("dog" "is" "big" "+")
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
The lion chases the mouse.
("lion" "chases" "mouse" "+")
The lion is not cold.
("lion" "is" "cold" "-")
The mouse chases the lion.
("mouse" "chases" "lion" "+")
The mouse does not chase the rabbit.
("mouse" "chases" "rabbit" "-")
The mouse visits the dog.
("mouse" "visits" "dog" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
All cold things are kind.
((("something" "is" "cold" "+")) -> ("something" "is" "kind" "+"))
If the lion sees the rabbit and the rabbit visits the mouse then the lion chases the dog.
((("lion" "sees" "rabbit" "+") ("rabbit" "visits" "mouse" "+")) -> ("lion" "chases" "dog" "+"))
The rabbit is cold.
True
1
proof
[(triple8)]
("rabbit" "is" "cold" "+")
triple8
The dog is not big.
False
1
inv-proof
[(triple1)]
("dog" "is" "big" "-")
triple1
The rabbit is kind.
True
2
proof
[(((triple8) -> rule1))]
("rabbit" "is" "kind" "+")
((triple8) -> (rule1 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The rabbit is not kind.
False
2
inv-proof
[(((triple8) -> rule1))]
("rabbit" "is" "kind" "-")
((triple8) -> (rule1 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The lion is not kind.
Unknown
inv-rconc
[@1: The lion is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "is" "kind" "-")
The mouse is kind.
Unknown
rconc
[@1: The mouse is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "is" "kind" "+")
The dog does not chase the mouse.
Unknown
inv-random
[@0: The dog chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "mouse" "-")
The lion visits the mouse.
Unknown
random
[@0: The lion visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "mouse" "+")
@0: The dog is big.[(triple1)] The dog visits the rabbit.[(triple2)] The lion chases the mouse.[(triple3)] The lion is not cold.[(triple4)] The mouse chases the lion.[(triple5)] The mouse does not chase the rabbit.[(triple6)] The mouse visits the dog.[(triple7)] The rabbit is cold.[(triple8)] The rabbit sees the lion.[(triple9)] The rabbit visits the lion.[(triple10)] @1: The rabbit is kind.[(((triple8) -> rule1))]
The dog is big.
("dog" "is" "big" "+")
triple1
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
triple2
The lion chases the mouse.
("lion" "chases" "mouse" "+")
triple3
The lion is not cold.
("lion" "is" "cold" "-")
triple4
The mouse chases the lion.
("mouse" "chases" "lion" "+")
triple5
The mouse does not chase the rabbit.
("mouse" "chases" "rabbit" "-")
triple6
The mouse visits the dog.
("mouse" "visits" "dog" "+")
triple7
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple8
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
triple9
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
triple10
The rabbit is kind.
("rabbit" "is" "kind" "+")
((triple8) -> (rule1 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1