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