Dave is kind. Dave is round. Fiona is not big. Fiona is cold. Fiona is young. Gary is blue. Harry is big. If Gary is young then Gary is not round. If someone is big then they are cold. All kind, young people are furry. All young, furry people are blue. Young, furry people are not blue. If someone is round then they are kind.
Dave is kind.
("Dave" "is" "kind" "+")
Dave is round.
("Dave" "is" "round" "+")
Fiona is not big.
("Fiona" "is" "big" "-")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Harry is big.
("Harry" "is" "big" "+")
If Gary is young then Gary is not round.
((("Gary" "is" "young" "+")) -> ("Gary" "is" "round" "-"))
If someone is big then they are cold.
((("someone" "is" "big" "+")) -> ("someone" "is" "cold" "+"))
All kind, young people are furry.
((("someone" "is" "kind" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "furry" "+"))
All young, furry people are blue.
((("someone" "is" "young" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "blue" "+"))
Young, furry people are not blue.
((("someone" "is" "young" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "blue" "-"))
If someone is round then they are kind.
((("someone" "is" "round" "+")) -> ("someone" "is" "kind" "+"))
Dave is kind.
True
1
proof
[(triple1 OR ((triple2) -> rule6))]
("Dave" "is" "kind" "+")
triple1
((triple2) -> (rule6 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Fiona is not cold.
False
1
inv-proof
[(triple4)]
("Fiona" "is" "cold" "-")
triple4
Harry is cold.
True
2
proof
[(((triple7) -> rule2))]
("Harry" "is" "cold" "+")
((triple7) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is not cold.
False
2
inv-proof
[(((triple7) -> rule2))]
("Harry" "is" "cold" "-")
((triple7) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is not furry.
Unknown
inv-rconc
[@1: Harry is furry.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "furry" "-")
Gary is cold.
Unknown
rconc
[@1: Gary is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "cold" "+")
Gary is not round.
Unknown
inv-random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "-")
Dave is young.
Unknown
random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "+")
@0: Dave is kind.[(triple1 OR ((triple2) -> rule6))] Dave is round.[(triple2)] Fiona is cold.[(triple4)] Fiona is not big.[(triple3)] Fiona is young.[(triple5)] Gary is blue.[(triple6)] Harry is big.[(triple7)] @1: Harry is cold.[(((triple7) -> rule2))]
Dave is kind.
("Dave" "is" "kind" "+")
triple1
((triple2) -> (rule6 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
triple2
Fiona is cold.
("Fiona" "is" "cold" "+")
triple4
Fiona is not big.
("Fiona" "is" "big" "-")
triple3
Fiona is young.
("Fiona" "is" "young" "+")
triple5
Gary is blue.
("Gary" "is" "blue" "+")
triple6
Harry is big.
("Harry" "is" "big" "+")
triple7
Harry is cold.
("Harry" "is" "cold" "+")
((triple7) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1