Bob is smart. If Bob is round then Bob is young. All smart things are cold. All green things are cold. If something is smart and kind then it is red. If Bob is young and Bob is not kind then Bob is not red. If something is red and cold then it is round.
Bob is smart.
("Bob" "is" "smart" "+")
If Bob is round then Bob is young.
((("Bob" "is" "round" "+")) -> ("Bob" "is" "young" "+"))
All smart things are cold.
((("something" "is" "smart" "+")) -> ("something" "is" "cold" "+"))
All green things are cold.
((("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
If something is smart and kind then it is red.
((("something" "is" "smart" "+") ("something" "is" "kind" "+")) -> ("something" "is" "red" "+"))
If Bob is young and Bob is not kind then Bob is not red.
((("Bob" "is" "young" "+") ("Bob" "is" "kind" "~")) -> ("Bob" "is" "red" "-"))
If something is red and cold then it is round.
((("something" "is" "red" "+") ("something" "is" "cold" "+")) -> ("something" "is" "round" "+"))
Bob is smart.
True
1
proof
[(triple1)]
("Bob" "is" "smart" "+")
triple1
Bob is not smart.
False
1
inv-proof
[(triple1)]
("Bob" "is" "smart" "-")
triple1
Bob is cold.
True
2
proof
[(((triple1) -> rule2))]
("Bob" "is" "cold" "+")
((triple1) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is not cold.
False
2
inv-proof
[(((triple1) -> rule2))]
("Bob" "is" "cold" "-")
((triple1) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is not round.
Unknown
inv-rconc
[@2: Bob is round.[CWA. Example of deepest failure = (rule6 <- rule4 <- FAIL)]]
("Bob" "is" "round" "-")
Bob is red.
Unknown
rconc
[@1: Bob is red.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Bob" "is" "red" "+")
Bob is not green.
Unknown
inv-random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "-")
Bob is kind.
Unknown
random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "+")
@0: Bob is smart.[(triple1)] @1: Bob is cold.[(((triple1) -> rule2))]
Bob is smart.
("Bob" "is" "smart" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
((triple1) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1