Bob is smart. Quiet people are red. If Bob is cold then Bob is green. Cold, quiet people are green. Smart people are quiet. All nice people are red. If someone is quiet then they are red. Cold people are smart. Smart people are kind.
Bob is smart.
("Bob" "is" "smart" "+")
Quiet people are red.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "red" "+"))
If Bob is cold then Bob is green.
((("Bob" "is" "cold" "+")) -> ("Bob" "is" "green" "+"))
Cold, quiet people are green.
((("someone" "is" "cold" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "green" "+"))
Smart people are quiet.
((("someone" "is" "smart" "+")) -> ("someone" "is" "quiet" "+"))
All nice people are red.
((("someone" "is" "nice" "+")) -> ("someone" "is" "red" "+"))
If someone is quiet then they are red.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "red" "+"))
Cold people are smart.
((("someone" "is" "cold" "+")) -> ("someone" "is" "smart" "+"))
Smart people are kind.
((("someone" "is" "smart" "+")) -> ("someone" "is" "kind" "+"))
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 kind.
True
2
proof
[(((triple1) -> rule8))]
("Bob" "is" "kind" "+")
((triple1) -> (rule8 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is not quiet.
False
2
inv-proof
[(((triple1) -> rule4))]
("Bob" "is" "quiet" "-")
((triple1) -> (rule4 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is not green.
Unknown
inv-rconc
[@1: Bob is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "green" "-")
Bob is cold.
Unknown
random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "+")
@0: Bob is smart.[(triple1)] @1: Bob is kind.[(((triple1) -> rule8))] Bob is quiet.[(((triple1) -> rule4))] @2: Bob is red.[(((((triple1) -> rule4)) -> rule1) OR ((((triple1) -> rule4)) -> rule6))]
Bob is smart.
("Bob" "is" "smart" "+")
triple1
Bob is kind.
("Bob" "is" "kind" "+")
((triple1) -> (rule8 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple1) -> (rule4 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
((((triple1) -> (rule4 % int2))) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
((((triple1) -> (rule4 % int2))) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2