Dave is red. If something is smart and red then it is blue. If Dave is red then Dave is blue. If something is red then it is quiet. If Dave is round and Dave is green then Dave is quiet. If Dave is quiet and Dave is red then Dave is not furry. If something is red and not blue then it is round.
Dave is red.
("Dave" "is" "red" "+")
If something is smart and red then it is blue.
((("something" "is" "smart" "+") ("something" "is" "red" "+")) -> ("something" "is" "blue" "+"))
If Dave is red then Dave is blue.
((("Dave" "is" "red" "+")) -> ("Dave" "is" "blue" "+"))
If something is red then it is quiet.
((("something" "is" "red" "+")) -> ("something" "is" "quiet" "+"))
If Dave is round and Dave is green then Dave is quiet.
((("Dave" "is" "round" "+") ("Dave" "is" "green" "+")) -> ("Dave" "is" "quiet" "+"))
If Dave is quiet and Dave is red then Dave is not furry.
((("Dave" "is" "quiet" "+") ("Dave" "is" "red" "+")) -> ("Dave" "is" "furry" "-"))
If something is red and not blue then it is round.
((("something" "is" "red" "+") ("something" "is" "blue" "~")) -> ("something" "is" "round" "+"))
Dave is red.
True
1
proof
[(triple1)]
("Dave" "is" "red" "+")
triple1
Dave is not red.
False
1
inv-proof
[(triple1)]
("Dave" "is" "red" "-")
triple1
Dave is blue.
True
2
proof
[(((triple1) -> rule2))]
("Dave" "is" "blue" "+")
((triple1) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is not blue.
False
2
inv-proof
[(((triple1) -> rule2))]
("Dave" "is" "blue" "-")
((triple1) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is not furry.
True
4
proof
[(((((triple1) -> rule3) triple1) -> rule5))]
("Dave" "is" "furry" "-")
((((triple1) -> (rule3 % int2)) triple1) -> (rule5 % int1))
Dave is not furry.
("Dave" "is" "furry" "-")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is furry.
False
4
inv-proof
[(((((triple1) -> rule3) triple1) -> rule5))]
("Dave" "is" "furry" "+")
((((triple1) -> (rule3 % int2)) triple1) -> (rule5 % int1))
Dave is not furry.
("Dave" "is" "furry" "-")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is not round.
Unknown
inv-rconc
[@1: Dave is round.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Dave" "is" "round" "-")
Dave is smart.
Unknown
random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "+")
@0: Dave is red.[(triple1)] @1: Dave is blue.[(((triple1) -> rule2))] Dave is quiet.[(((triple1) -> rule3))] @2: Dave is not furry.[(((((triple1) -> rule3) triple1) -> rule5))]
Dave is red.
("Dave" "is" "red" "+")
triple1
Dave is blue.
("Dave" "is" "blue" "+")
((triple1) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple1) -> (rule3 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is not furry.
("Dave" "is" "furry" "-")
((((triple1) -> (rule3 % int2)) triple1) -> (rule5 % int1))
Dave is not furry.
("Dave" "is" "furry" "-")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2