Dave is not kind. Dave is nice. Erin is kind. Erin is round. Erin is young. Gary is cold. Gary is nice. Gary is young. Harry is cold. Harry is round. If someone is young and not nice then they are round. All big, nice people are round. Round people are young.
Dave is not kind.
("Dave" "is" "kind" "-")
Dave is nice.
("Dave" "is" "nice" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is young.
("Erin" "is" "young" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is young.
("Gary" "is" "young" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is round.
("Harry" "is" "round" "+")
If someone is young and not nice then they are round.
((("someone" "is" "young" "+") ("someone" "is" "nice" "~")) -> ("someone" "is" "round" "+"))
All big, nice people are round.
((("someone" "is" "big" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "round" "+"))
Round people are young.
((("someone" "is" "round" "+")) -> ("someone" "is" "young" "+"))
Erin is young.
True
1
proof
[(triple5 OR ((triple4) -> rule3))]
("Erin" "is" "young" "+")
triple5
((triple4) -> (rule3 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Gary is not cold.
False
1
inv-proof
[(triple6)]
("Gary" "is" "cold" "-")
triple6
Dave is not round.
Unknown
inv-rconc
[@1: Dave is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "round" "-")
Erin is big.
Unknown
random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "+")
@0: Dave is nice.[(triple2)] Dave is not kind.[(triple1)] Erin is kind.[(triple3)] Erin is round.[(triple4)] Erin is young.[(triple5 OR ((triple4) -> rule3))] Gary is cold.[(triple6)] Gary is nice.[(triple7)] Gary is young.[(triple8)] Harry is cold.[(triple9)] Harry is round.[(triple10)] @1: Harry is young.[(((triple10) -> rule3))]
Dave is nice.
("Dave" "is" "nice" "+")
triple2
Dave is not kind.
("Dave" "is" "kind" "-")
triple1
Erin is kind.
("Erin" "is" "kind" "+")
triple3
Erin is round.
("Erin" "is" "round" "+")
triple4
Erin is young.
("Erin" "is" "young" "+")
triple5
((triple4) -> (rule3 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
triple6
Gary is nice.
("Gary" "is" "nice" "+")
triple7
Gary is young.
("Gary" "is" "young" "+")
triple8
Harry is cold.
("Harry" "is" "cold" "+")
triple9
Harry is round.
("Harry" "is" "round" "+")
triple10
Harry is young.
("Harry" "is" "young" "+")
((triple10) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1