Bob is cold. Bob is kind. Bob is nice. Bob is smart. Erin is cold. Erin is smart. Fiona is blue. Green things are red. If something is red and cold then it is green.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Green things are red.
((("something" "is" "green" "+")) -> ("something" "is" "red" "+"))
If something is red and cold then it is green.
((("something" "is" "red" "+") ("something" "is" "cold" "+")) -> ("something" "is" "green" "+"))
Bob is cold.
True
1
proof
[(triple1)]
("Bob" "is" "cold" "+")
triple1
Erin is not cold.
False
1
inv-proof
[(triple5)]
("Erin" "is" "cold" "-")
triple5
Bob is not green.
Unknown
inv-rconc
[@2: Bob is green.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Bob" "is" "green" "-")
Fiona is cold.
Unknown
random
[@0: Fiona is cold.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "cold" "+")
@0: Bob is cold.[(triple1)] Bob is kind.[(triple2)] Bob is nice.[(triple3)] Bob is smart.[(triple4)] Erin is cold.[(triple5)] Erin is smart.[(triple6)] Fiona is blue.[(triple7)]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is kind.
("Bob" "is" "kind" "+")
triple2
Bob is nice.
("Bob" "is" "nice" "+")
triple3
Bob is smart.
("Bob" "is" "smart" "+")
triple4
Erin is cold.
("Erin" "is" "cold" "+")
triple5
Erin is smart.
("Erin" "is" "smart" "+")
triple6
Fiona is blue.
("Fiona" "is" "blue" "+")
triple7