The cat eats the squirrel. The cow sees the rabbit. The rabbit is kind. The squirrel is cold. If something is cold then it is nice. If something chases the squirrel then it sees the cow.
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
If something is cold then it is nice.
((("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
If something chases the squirrel then it sees the cow.
((("something" "chases" "squirrel" "+")) -> ("something" "sees" "cow" "+"))
The cow sees the rabbit.
True
1
proof
[(triple2)]
("cow" "sees" "rabbit" "+")
triple2
The rabbit is not kind.
False
1
inv-proof
[(triple3)]
("rabbit" "is" "kind" "-")
triple3
The cow is not nice.
Unknown
inv-rconc
[@1: The cow is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "is" "nice" "-")
The cat is cold.
Unknown
random
[@0: The cat is cold.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "cold" "+")
@0: The cat eats the squirrel.[(triple1)] The cow sees the rabbit.[(triple2)] The rabbit is kind.[(triple3)] The squirrel is cold.[(triple4)] @1: The squirrel is nice.[(((triple4) -> rule1))]
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
triple1
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
triple2
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple3
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple4
The squirrel is nice.
("squirrel" "is" "nice" "+")
((triple4) -> (rule1 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1