Charlie is nice. Dave is not furry. Dave is nice. Dave is rough. Fiona is furry. Gary is not blue. Gary is kind. If someone is rough then they are not blue. If someone is nice and not kind then they are blue. All furry people are nice. If someone is kind then they are nice. If someone is rough then they are not furry. If someone is blue and not green then they are not rough.
Charlie is nice.
("Charlie" "is" "nice" "+")
Dave is not furry.
("Dave" "is" "furry" "-")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Gary is not blue.
("Gary" "is" "blue" "-")
Gary is kind.
("Gary" "is" "kind" "+")
If someone is rough then they are not blue.
((("someone" "is" "rough" "+")) -> ("someone" "is" "blue" "-"))
If someone is nice and not kind then they are blue.
((("someone" "is" "nice" "+") ("someone" "is" "kind" "~")) -> ("someone" "is" "blue" "+"))
All furry people are nice.
((("someone" "is" "furry" "+")) -> ("someone" "is" "nice" "+"))
If someone is kind then they are nice.
((("someone" "is" "kind" "+")) -> ("someone" "is" "nice" "+"))
If someone is rough then they are not furry.
((("someone" "is" "rough" "+")) -> ("someone" "is" "furry" "-"))
If someone is blue and not green then they are not rough.
((("someone" "is" "blue" "+") ("someone" "is" "green" "~")) -> ("someone" "is" "rough" "-"))
Dave is not furry.
True
1
proof
[(triple2 OR ((triple4) -> rule5))]
("Dave" "is" "furry" "-")
triple2
((triple4) -> (rule5 % int1))
Dave is not furry.
("Dave" "is" "furry" "-")
int1
Gary is not kind.
False
1
inv-proof
[(triple7)]
("Gary" "is" "kind" "-")
triple7
Dave is not blue.
True
2
proof
[(((triple4) -> rule1))]
("Dave" "is" "blue" "-")
((triple4) -> (rule1 % int1))
Dave is not blue.
("Dave" "is" "blue" "-")
int1
Gary is not nice.
False
2
inv-proof
[(((triple7) -> rule4))]
("Gary" "is" "nice" "-")
((triple7) -> (rule4 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Fiona is not blue.
Unknown
inv-rconc
[@1: Fiona is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "blue" "-")
Charlie is blue.
Unknown
rconc
[@1: Charlie is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "blue" "+")
Dave is not green.
Unknown
inv-random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "-")
Dave is kind.
Unknown
random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "+")
@0: Charlie is nice.[(triple1)] Dave is nice.[(triple3)] Dave is not furry.[(triple2 OR ((triple4) -> rule5))] Dave is rough.[(triple4)] Fiona is furry.[(triple5)] Gary is kind.[(triple7)] Gary is not blue.[(triple6)] @1: Dave is not blue.[(((triple4) -> rule1))] Fiona is nice.[(((triple5) -> rule3))] Gary is nice.[(((triple7) -> rule4))]
Charlie is nice.
("Charlie" "is" "nice" "+")
triple1
Dave is nice.
("Dave" "is" "nice" "+")
triple3
Dave is not furry.
("Dave" "is" "furry" "-")
triple2
((triple4) -> (rule5 % int1))
Dave is not furry.
("Dave" "is" "furry" "-")
int1
Dave is rough.
("Dave" "is" "rough" "+")
triple4
Fiona is furry.
("Fiona" "is" "furry" "+")
triple5
Gary is kind.
("Gary" "is" "kind" "+")
triple7
Gary is not blue.
("Gary" "is" "blue" "-")
triple6
Dave is not blue.
("Dave" "is" "blue" "-")
((triple4) -> (rule1 % int1))
Dave is not blue.
("Dave" "is" "blue" "-")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
((triple5) -> (rule3 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
((triple7) -> (rule4 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1