Dave is nice. If Dave is furry and Dave is round then Dave is blue. Quiet, furry people are round. Smart, white people are furry. If Dave is furry then Dave is round. All round, nice people are smart. If someone is nice then they are furry.
Dave is nice.
("Dave" "is" "nice" "+")
If Dave is furry and Dave is round then Dave is blue.
((("Dave" "is" "furry" "+") ("Dave" "is" "round" "+")) -> ("Dave" "is" "blue" "+"))
Quiet, furry people are round.
((("someone" "is" "quiet" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "round" "+"))
Smart, white people are furry.
((("someone" "is" "smart" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "furry" "+"))
If Dave is furry then Dave is round.
((("Dave" "is" "furry" "+")) -> ("Dave" "is" "round" "+"))
All round, nice people are smart.
((("someone" "is" "round" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "smart" "+"))
If someone is nice then they are furry.
((("someone" "is" "nice" "+")) -> ("someone" "is" "furry" "+"))
Dave is nice.
True
1
proof
[(triple1)]
("Dave" "is" "nice" "+")
triple1
Dave is not nice.
False
1
inv-proof
[(triple1)]
("Dave" "is" "nice" "-")
triple1
Dave is furry.
True
2
proof
[(((triple1) -> rule6))]
("Dave" "is" "furry" "+")
((triple1) -> (rule6 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is not furry.
False
2
inv-proof
[(((triple1) -> rule6))]
("Dave" "is" "furry" "-")
((triple1) -> (rule6 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is round.
True
3
proof
[(((((triple1) -> rule6)) -> rule4))]
("Dave" "is" "round" "+")
((((triple1) -> (rule6 % int2))) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is not round.
False
3
inv-proof
[(((((triple1) -> rule6)) -> rule4))]
("Dave" "is" "round" "-")
((((triple1) -> (rule6 % int2))) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is blue.
True
6
proof
[(((((triple1) -> rule6) ((((triple1) -> rule6)) -> rule4)) -> rule1))]
("Dave" "is" "blue" "+")
((((triple1) -> (rule6 % int3)) ((((triple1) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is not blue.
False
6
inv-proof
[(((((triple1) -> rule6) ((((triple1) -> rule6)) -> rule4)) -> rule1))]
("Dave" "is" "blue" "-")
((((triple1) -> (rule6 % int3)) ((((triple1) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is not white.
Unknown
inv-random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "-")
Dave is quiet.
Unknown
random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "+")
@0: Dave is nice.[(triple1)] @1: Dave is furry.[(((triple1) -> rule6))] @2: Dave is round.[(((((triple1) -> rule6)) -> rule4))] @3: Dave is blue.[(((((triple1) -> rule6) ((((triple1) -> rule6)) -> rule4)) -> rule1))] Dave is smart.[(((((((triple1) -> rule6)) -> rule4) triple1) -> rule5))]
Dave is nice.
("Dave" "is" "nice" "+")
triple1
Dave is furry.
("Dave" "is" "furry" "+")
((triple1) -> (rule6 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
((((triple1) -> (rule6 % int2))) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
((((triple1) -> (rule6 % int3)) ((((triple1) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
((((((triple1) -> (rule6 % int3))) -> (rule4 % int2)) triple1) -> (rule5 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3