Dave is nice. Dave is red. Dave is smart. If Dave is furry and Dave is red then Dave is cold. Nice people are furry.
Dave is nice.
("Dave" "is" "nice" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is smart.
("Dave" "is" "smart" "+")
If Dave is furry and Dave is red then Dave is cold.
((("Dave" "is" "furry" "+") ("Dave" "is" "red" "+")) -> ("Dave" "is" "cold" "+"))
Nice people are furry.
((("someone" "is" "nice" "+")) -> ("someone" "is" "furry" "+"))
Dave is nice.
True
1
proof
[(triple1)]
("Dave" "is" "nice" "+")
triple1
Dave is not red.
False
1
inv-proof
[(triple2)]
("Dave" "is" "red" "-")
triple2
Dave is furry.
True
2
proof
[(((triple1) -> rule2))]
("Dave" "is" "furry" "+")
((triple1) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is not furry.
False
2
inv-proof
[(((triple1) -> rule2))]
("Dave" "is" "furry" "-")
((triple1) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is cold.
True
4
proof
[(((((triple1) -> rule2) triple2) -> rule1))]
("Dave" "is" "cold" "+")
((((triple1) -> (rule2 % int2)) triple2) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is not cold.
False
4
inv-proof
[(((((triple1) -> rule2) triple2) -> rule1))]
("Dave" "is" "cold" "-")
((((triple1) -> (rule2 % int2)) triple2) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is not round.
Unknown
inv-random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
@0: Dave is nice.[(triple1)] Dave is red.[(triple2)] Dave is smart.[(triple3)] @1: Dave is furry.[(((triple1) -> rule2))] @2: Dave is cold.[(((((triple1) -> rule2) triple2) -> rule1))]
Dave is nice.
("Dave" "is" "nice" "+")
triple1
Dave is red.
("Dave" "is" "red" "+")
triple2
Dave is smart.
("Dave" "is" "smart" "+")
triple3
Dave is furry.
("Dave" "is" "furry" "+")
((triple1) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
((((triple1) -> (rule2 % int2)) triple2) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2