Anne is nice. Dave is kind. Harry is green. If Anne is blue and Anne is nice then Anne is kind. If Dave is blue and Dave is furry then Dave is cold. Blue, furry people are not cold. If someone is kind then they are green. Blue, nice people are furry. Green, kind people are big.
Anne is nice.
("Anne" "is" "nice" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Harry is green.
("Harry" "is" "green" "+")
If Anne is blue and Anne is nice then Anne is kind.
((("Anne" "is" "blue" "+") ("Anne" "is" "nice" "+")) -> ("Anne" "is" "kind" "+"))
If Dave is blue and Dave is furry then Dave is cold.
((("Dave" "is" "blue" "+") ("Dave" "is" "furry" "+")) -> ("Dave" "is" "cold" "+"))
Blue, furry people are not cold.
((("someone" "is" "blue" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "cold" "-"))
If someone is kind then they are green.
((("someone" "is" "kind" "+")) -> ("someone" "is" "green" "+"))
Blue, nice people are furry.
((("someone" "is" "blue" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "furry" "+"))
Green, kind people are big.
((("someone" "is" "green" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "big" "+"))
Dave is kind.
True
1
proof
[(triple2)]
("Dave" "is" "kind" "+")
triple2
Anne is not nice.
False
1
inv-proof
[(triple1)]
("Anne" "is" "nice" "-")
triple1
Dave is green.
True
2
proof
[(((triple2) -> rule4))]
("Dave" "is" "green" "+")
((triple2) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is not green.
False
2
inv-proof
[(((triple2) -> rule4))]
("Dave" "is" "green" "-")
((triple2) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is big.
True
4
proof
[(((((triple2) -> rule4) triple2) -> rule6))]
("Dave" "is" "big" "+")
((((triple2) -> (rule4 % int2)) triple2) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is not big.
False
4
inv-proof
[(((((triple2) -> rule4) triple2) -> rule6))]
("Dave" "is" "big" "-")
((((triple2) -> (rule4 % int2)) triple2) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is not cold.
Unknown
inv-rconc
[@1: Dave is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "cold" "-")
Anne is kind.
Unknown
rconc
[@1: Anne is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "kind" "+")
Harry is not big.
Unknown
inv-rconc
[@1: Harry is big.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "big" "-")
Harry is blue.
Unknown
random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "+")
Harry is not nice.
Unknown
inv-random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
@0: Anne is nice.[(triple1)] Dave is kind.[(triple2)] Harry is green.[(triple3)] @1: Dave is green.[(((triple2) -> rule4))] @2: Dave is big.[(((((triple2) -> rule4) triple2) -> rule6))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Dave is kind.
("Dave" "is" "kind" "+")
triple2
Harry is green.
("Harry" "is" "green" "+")
triple3
Dave is green.
("Dave" "is" "green" "+")
((triple2) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
((((triple2) -> (rule4 % int2)) triple2) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2