Bob is cold. Bob is round. Bob is young. Erin is cold. Erin is young. Harry is big. Harry is kind. If something is round then it is cold. Cold, round things are white.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is young.
("Bob" "is" "young" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is young.
("Erin" "is" "young" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is kind.
("Harry" "is" "kind" "+")
If something is round then it is cold.
((("something" "is" "round" "+")) -> ("something" "is" "cold" "+"))
Cold, round things are white.
((("something" "is" "cold" "+") ("something" "is" "round" "+")) -> ("something" "is" "white" "+"))
Harry is big.
True
1
proof
[(triple6)]
("Harry" "is" "big" "+")
triple6
Bob is not round.
False
1
inv-proof
[(triple2)]
("Bob" "is" "round" "-")
triple2
Harry is not cold.
Unknown
inv-rconc
[@1: Harry is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "cold" "-")
Erin is kind.
Unknown
random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "+")
@0: Bob is cold.[(triple1 OR ((triple2) -> rule1))] Bob is round.[(triple2)] Bob is young.[(triple3)] Erin is cold.[(triple4)] Erin is young.[(triple5)] Harry is big.[(triple6)] Harry is kind.[(triple7)] @1: Bob is white.[(((triple1 triple2) -> rule2) OR ((((triple2) -> rule1) triple2) -> rule2))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
((triple2) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
triple2
Bob is young.
("Bob" "is" "young" "+")
triple3
Erin is cold.
("Erin" "is" "cold" "+")
triple4
Erin is young.
("Erin" "is" "young" "+")
triple5
Harry is big.
("Harry" "is" "big" "+")
triple6
Harry is kind.
("Harry" "is" "kind" "+")
triple7
Bob is white.
("Bob" "is" "white" "+")
((triple1 triple2) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
((((triple2) -> (rule1 % int2)) triple2) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2