Dave is blue. Fiona is round. Harry is furry. All red, furry things are green. If Harry is furry then Harry is red. If Fiona is green and Fiona is red then Fiona is nice. All green things are nice. If something is blue and round then it is not nice. If something is round and not green then it is not nice.
Dave is blue.
("Dave" "is" "blue" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Harry is furry.
("Harry" "is" "furry" "+")
All red, furry things are green.
((("something" "is" "red" "+") ("something" "is" "furry" "+")) -> ("something" "is" "green" "+"))
If Harry is furry then Harry is red.
((("Harry" "is" "furry" "+")) -> ("Harry" "is" "red" "+"))
If Fiona is green and Fiona is red then Fiona is nice.
((("Fiona" "is" "green" "+") ("Fiona" "is" "red" "+")) -> ("Fiona" "is" "nice" "+"))
All green things are nice.
((("something" "is" "green" "+")) -> ("something" "is" "nice" "+"))
If something is blue and round then it is not nice.
((("something" "is" "blue" "+") ("something" "is" "round" "+")) -> ("something" "is" "nice" "-"))
If something is round and not green then it is not nice.
((("something" "is" "round" "+") ("something" "is" "green" "~")) -> ("something" "is" "nice" "-"))
Dave is blue.
True
1
proof
[(triple1)]
("Dave" "is" "blue" "+")
triple1
Dave is not blue.
False
1
inv-proof
[(triple1)]
("Dave" "is" "blue" "-")
triple1
Harry is red.
True
2
proof
[(((triple3) -> rule2))]
("Harry" "is" "red" "+")
((triple3) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is not red.
False
2
inv-proof
[(((triple3) -> rule2))]
("Harry" "is" "red" "-")
((triple3) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is green.
True
4
proof
[(((((triple3) -> rule2) triple3) -> rule1))]
("Harry" "is" "green" "+")
((((triple3) -> (rule2 % int2)) triple3) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is not green.
False
4
inv-proof
[(((((triple3) -> rule2) triple3) -> rule1))]
("Harry" "is" "green" "-")
((((triple3) -> (rule2 % int2)) triple3) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is nice.
True
5
proof
[(((((((triple3) -> rule2) triple3) -> rule1)) -> rule4))]
("Harry" "is" "nice" "+")
((((((triple3) -> (rule2 % int3)) triple3) -> (rule1 % int2))) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Harry is not nice.
False
5
inv-proof
[(((((((triple3) -> rule2) triple3) -> rule1)) -> rule4))]
("Harry" "is" "nice" "-")
((((((triple3) -> (rule2 % int3)) triple3) -> (rule1 % int2))) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Fiona is not green.
Unknown
inv-rconc
[@1: Fiona is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "green" "-")
Fiona is nice.
Unknown
rconc
[@2: Fiona is nice.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("Fiona" "is" "nice" "+")
Dave is not nice.
Unknown
inv-rconc
[@2: Dave is nice.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("Dave" "is" "nice" "-")
Dave is green.
Unknown
rconc
[@1: Dave is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "green" "+")
Dave is not red.
Unknown
inv-random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "-")
Dave is quiet.
Unknown
random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "+")
Fiona is not blue.
Unknown
inv-random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "-")
Dave is furry.
Unknown
random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "+")
@0: Dave is blue.[(triple1)] Fiona is round.[(triple2)] Harry is furry.[(triple3)] @1: Harry is red.[(((triple3) -> rule2))] @2: Harry is green.[(((((triple3) -> rule2) triple3) -> rule1))] @3: Harry is nice.[(((((((triple3) -> rule2) triple3) -> rule1)) -> rule4))]
Dave is blue.
("Dave" "is" "blue" "+")
triple1
Fiona is round.
("Fiona" "is" "round" "+")
triple2
Harry is furry.
("Harry" "is" "furry" "+")
triple3
Harry is red.
("Harry" "is" "red" "+")
((triple3) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
((((triple3) -> (rule2 % int2)) triple3) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
((((((triple3) -> (rule2 % int3)) triple3) -> (rule1 % int2))) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3