Bob is smart. Erin is blue. Gary is young. Young things are smart. All white things are cold. If Erin is green and Erin is young then Erin is cold.
Bob is smart.
("Bob" "is" "smart" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Gary is young.
("Gary" "is" "young" "+")
Young things are smart.
((("something" "is" "young" "+")) -> ("something" "is" "smart" "+"))
All white things are cold.
((("something" "is" "white" "+")) -> ("something" "is" "cold" "+"))
If Erin is green and Erin is young then Erin is cold.
((("Erin" "is" "green" "+") ("Erin" "is" "young" "+")) -> ("Erin" "is" "cold" "+"))
Bob is smart.
True
1
proof
[(triple1)]
("Bob" "is" "smart" "+")
triple1
Gary is not young.
False
1
inv-proof
[(triple3)]
("Gary" "is" "young" "-")
triple3
Gary is smart.
True
2
proof
[(((triple3) -> rule1))]
("Gary" "is" "smart" "+")
((triple3) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is not smart.
False
2
inv-proof
[(((triple3) -> rule1))]
("Gary" "is" "smart" "-")
((triple3) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Bob is not cold.
Unknown
inv-rconc
[@1: Bob is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "cold" "-")
Erin is cold.
Unknown
rconc
[@1: Erin is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "cold" "+")
Gary is not green.
Unknown
inv-random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "-")
Gary is white.
Unknown
random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "+")
@0: Bob is smart.[(triple1)] Erin is blue.[(triple2)] Gary is young.[(triple3)] @1: Gary is smart.[(((triple3) -> rule1))]
Bob is smart.
("Bob" "is" "smart" "+")
triple1
Erin is blue.
("Erin" "is" "blue" "+")
triple2
Gary is young.
("Gary" "is" "young" "+")
triple3
Gary is smart.
("Gary" "is" "smart" "+")
((triple3) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1