Bob is smart. Red people are white. If Bob is furry and Bob is red then Bob is smart. If Bob is red and Bob is smart then Bob is white. If Bob is furry then Bob is cold. If someone is smart then they are young. All white, cold people are smart.
Bob is smart.
("Bob" "is" "smart" "+")
Red people are white.
((("someone" "is" "red" "+")) -> ("someone" "is" "white" "+"))
If Bob is furry and Bob is red then Bob is smart.
((("Bob" "is" "furry" "+") ("Bob" "is" "red" "+")) -> ("Bob" "is" "smart" "+"))
If Bob is red and Bob is smart then Bob is white.
((("Bob" "is" "red" "+") ("Bob" "is" "smart" "+")) -> ("Bob" "is" "white" "+"))
If Bob is furry then Bob is cold.
((("Bob" "is" "furry" "+")) -> ("Bob" "is" "cold" "+"))
If someone is smart then they are young.
((("someone" "is" "smart" "+")) -> ("someone" "is" "young" "+"))
All white, cold people are smart.
((("someone" "is" "white" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "smart" "+"))
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 young.
True
2
proof
[(((triple1) -> rule5))]
("Bob" "is" "young" "+")
((triple1) -> (rule5 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is not young.
False
2
inv-proof
[(((triple1) -> rule5))]
("Bob" "is" "young" "-")
((triple1) -> (rule5 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is not cold.
Unknown
inv-rconc
[@1: Bob is cold.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Bob" "is" "cold" "-")
Bob is white.
Unknown
rconc
[@1: Bob is white.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "white" "+")
Bob is not furry.
Unknown
inv-random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "-")
Bob is red.
Unknown
random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "+")
@0: Bob is smart.[(triple1)] @1: Bob is young.[(((triple1) -> rule5))]
Bob is smart.
("Bob" "is" "smart" "+")
triple1
Bob is young.
("Bob" "is" "young" "+")
((triple1) -> (rule5 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1