Dave is nice. Dave is not round. Dave is young. If Dave is cold then Dave is not furry. If Dave is round and Dave is not young then Dave is nice. If someone is round and not cold then they are furry. Nice people are not furry. Cold, young people are round. Furry, round people are red. If someone is cold and not nice then they are not red. If someone is nice then they are not red.
Dave is nice.
("Dave" "is" "nice" "+")
Dave is not round.
("Dave" "is" "round" "-")
Dave is young.
("Dave" "is" "young" "+")
If Dave is cold then Dave is not furry.
((("Dave" "is" "cold" "+")) -> ("Dave" "is" "furry" "-"))
If Dave is round and Dave is not young then Dave is nice.
((("Dave" "is" "round" "+") ("Dave" "is" "young" "~")) -> ("Dave" "is" "nice" "+"))
If someone is round and not cold then they are furry.
((("someone" "is" "round" "+") ("someone" "is" "cold" "~")) -> ("someone" "is" "furry" "+"))
Nice people are not furry.
((("someone" "is" "nice" "+")) -> ("someone" "is" "furry" "-"))
Cold, young people are round.
((("someone" "is" "cold" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "round" "+"))
Furry, round people are red.
((("someone" "is" "furry" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "red" "+"))
If someone is cold and not nice then they are not red.
((("someone" "is" "cold" "+") ("someone" "is" "nice" "~")) -> ("someone" "is" "red" "-"))
If someone is nice then they are not red.
((("someone" "is" "nice" "+")) -> ("someone" "is" "red" "-"))
Dave is not round.
True
1
proof
[(triple2)]
("Dave" "is" "round" "-")
triple2
Dave is not young.
False
1
inv-proof
[(triple3)]
("Dave" "is" "young" "-")
triple3
Dave is not furry.
True
2
proof
[(((triple1) -> rule4))]
("Dave" "is" "furry" "-")
((triple1) -> (rule4 % int1))
Dave is not furry.
("Dave" "is" "furry" "-")
int1
Dave is red.
False
2
inv-proof
[(((triple1) -> rule8))]
("Dave" "is" "red" "+")
((triple1) -> (rule8 % int1))
Dave is not red.
("Dave" "is" "red" "-")
int1
Dave is not cold.
Unknown
inv-random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "-")
Dave is green.
Unknown
random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "+")
@0: Dave is nice.[(triple1)] Dave is not round.[(triple2)] Dave is young.[(triple3)] @1: Dave is not furry.[(((triple1) -> rule4))] Dave is not red.[(((triple1) -> rule8))]
Dave is nice.
("Dave" "is" "nice" "+")
triple1
Dave is not round.
("Dave" "is" "round" "-")
triple2
Dave is young.
("Dave" "is" "young" "+")
triple3
Dave is not furry.
("Dave" "is" "furry" "-")
((triple1) -> (rule4 % int1))
Dave is not furry.
("Dave" "is" "furry" "-")
int1
Dave is not red.
("Dave" "is" "red" "-")
((triple1) -> (rule8 % int1))
Dave is not red.
("Dave" "is" "red" "-")
int1