Dave is furry. Fiona is red. Harry is red. All red, green people are nice. If Dave is white and Dave is kind then Dave is furry. Furry people are nice. If someone is nice then they are kind. If someone is kind then they are furry. All round, kind people are white.
Dave is furry.
("Dave" "is" "furry" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Harry is red.
("Harry" "is" "red" "+")
All red, green people are nice.
((("someone" "is" "red" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "nice" "+"))
If Dave is white and Dave is kind then Dave is furry.
((("Dave" "is" "white" "+") ("Dave" "is" "kind" "+")) -> ("Dave" "is" "furry" "+"))
Furry people are nice.
((("someone" "is" "furry" "+")) -> ("someone" "is" "nice" "+"))
If someone is nice then they are kind.
((("someone" "is" "nice" "+")) -> ("someone" "is" "kind" "+"))
If someone is kind then they are furry.
((("someone" "is" "kind" "+")) -> ("someone" "is" "furry" "+"))
All round, kind people are white.
((("someone" "is" "round" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "white" "+"))
Dave is furry.
True
1
proof
[(triple1)]
("Dave" "is" "furry" "+")
triple1
Harry is not red.
False
1
inv-proof
[(triple3)]
("Harry" "is" "red" "-")
triple3
Dave is nice.
True
2
proof
[(((triple1) -> rule3))]
("Dave" "is" "nice" "+")
((triple1) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is not nice.
False
2
inv-proof
[(((triple1) -> rule3))]
("Dave" "is" "nice" "-")
((triple1) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is kind.
True
3
proof
[(((((triple1) -> rule3)) -> rule4))]
("Dave" "is" "kind" "+")
((((triple1) -> (rule3 % int2))) -> (rule4 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is not kind.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule4))]
("Dave" "is" "kind" "-")
((((triple1) -> (rule3 % int2))) -> (rule4 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Harry is not white.
Unknown
inv-rconc
[@1: Harry is white.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "white" "-")
Harry is nice.
Unknown
rconc
[@4: Harry is nice.[CWA. Example of deepest failure = (rule3 <- rule5 <- rule4 <- rule1 <- FAIL)]]
("Harry" "is" "nice" "+")
Harry is not furry.
Unknown
inv-rconc
[@3: Harry is furry.[CWA. Example of deepest failure = (rule5 <- rule4 <- rule1 <- FAIL)]]
("Harry" "is" "furry" "-")
Harry is round.
Unknown
random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "+")
Harry is not green.
Unknown
inv-random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "-")
Dave is red.
Unknown
random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "+")
@0: Dave is furry.[(triple1)] Fiona is red.[(triple2)] Harry is red.[(triple3)] @1: Dave is nice.[(((triple1) -> rule3))] @2: Dave is kind.[(((((triple1) -> rule3)) -> rule4))]
Dave is furry.
("Dave" "is" "furry" "+")
triple1
Fiona is red.
("Fiona" "is" "red" "+")
triple2
Harry is red.
("Harry" "is" "red" "+")
triple3
Dave is nice.
("Dave" "is" "nice" "+")
((triple1) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
((((triple1) -> (rule3 % int2))) -> (rule4 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2