Bob is blue. All white people are kind. If someone is smart then they are green. Young people are kind. If Bob is green and Bob is young then Bob is smart. If someone is blue then they are kind. Blue people are smart.
Bob is blue.
("Bob" "is" "blue" "+")
All white people are kind.
((("someone" "is" "white" "+")) -> ("someone" "is" "kind" "+"))
If someone is smart then they are green.
((("someone" "is" "smart" "+")) -> ("someone" "is" "green" "+"))
Young people are kind.
((("someone" "is" "young" "+")) -> ("someone" "is" "kind" "+"))
If Bob is green and Bob is young then Bob is smart.
((("Bob" "is" "green" "+") ("Bob" "is" "young" "+")) -> ("Bob" "is" "smart" "+"))
If someone is blue then they are kind.
((("someone" "is" "blue" "+")) -> ("someone" "is" "kind" "+"))
Blue people are smart.
((("someone" "is" "blue" "+")) -> ("someone" "is" "smart" "+"))
Bob is blue.
True
1
proof
[(triple1)]
("Bob" "is" "blue" "+")
triple1
Bob is not blue.
False
1
inv-proof
[(triple1)]
("Bob" "is" "blue" "-")
triple1
Bob is kind.
True
2
proof
[(((triple1) -> rule5))]
("Bob" "is" "kind" "+")
((triple1) -> (rule5 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is not kind.
False
2
inv-proof
[(((triple1) -> rule5))]
("Bob" "is" "kind" "-")
((triple1) -> (rule5 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is green.
True
3
proof
[(((((triple1) -> rule6)) -> rule2))]
("Bob" "is" "green" "+")
((((triple1) -> (rule6 % int2))) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is not green.
False
3
inv-proof
[(((((triple1) -> rule6)) -> rule2))]
("Bob" "is" "green" "-")
((((triple1) -> (rule6 % int2))) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is not white.
Unknown
inv-random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "-")
Bob is young.
Unknown
random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "+")
@0: Bob is blue.[(triple1)] @1: Bob is kind.[(((triple1) -> rule5))] Bob is smart.[(((triple1) -> rule6))] @2: Bob is green.[(((((triple1) -> rule6)) -> rule2))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is kind.
("Bob" "is" "kind" "+")
((triple1) -> (rule5 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
((triple1) -> (rule6 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
((((triple1) -> (rule6 % int2))) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2