Bob is kind. Bob is smart. Erin is young. All young, round people are nice. Smart people are cold. Round people are cold. All nice, round people are smart. Cold, round people are blue. If Erin is blue and Erin is smart then Erin is young.
Bob is kind.
("Bob" "is" "kind" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Erin is young.
("Erin" "is" "young" "+")
All young, round people are nice.
((("someone" "is" "young" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "nice" "+"))
Smart people are cold.
((("someone" "is" "smart" "+")) -> ("someone" "is" "cold" "+"))
Round people are cold.
((("someone" "is" "round" "+")) -> ("someone" "is" "cold" "+"))
All nice, round people are smart.
((("someone" "is" "nice" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "smart" "+"))
Cold, round people are blue.
((("someone" "is" "cold" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "blue" "+"))
If Erin is blue and Erin is smart then Erin is young.
((("Erin" "is" "blue" "+") ("Erin" "is" "smart" "+")) -> ("Erin" "is" "young" "+"))
Bob is smart.
True
1
proof
[(triple2)]
("Bob" "is" "smart" "+")
triple2
Erin is not young.
False
1
inv-proof
[(triple3)]
("Erin" "is" "young" "-")
triple3
Erin is not smart.
Unknown
inv-rconc
[@1: Erin is smart.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Erin" "is" "smart" "-")
Bob is round.
Unknown
random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "+")
@0: Bob is kind.[(triple1)] Bob is smart.[(triple2)] Erin is young.[(triple3)] @1: Bob is cold.[(((triple2) -> rule2))]
Bob is kind.
("Bob" "is" "kind" "+")
triple1
Bob is smart.
("Bob" "is" "smart" "+")
triple2
Erin is young.
("Erin" "is" "young" "+")
triple3
Bob is cold.
("Bob" "is" "cold" "+")
((triple2) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1