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