Charlie is cold. Dave is white. Cold, quiet people are white. If someone is green then they are white. All white people are smart. If Dave is cold and Dave is white then Dave is green. All big people are not quiet. If someone is smart and big then they are not green. All big people are green. If someone is quiet and not red then they are big.
Charlie is cold.
("Charlie" "is" "cold" "+")
Dave is white.
("Dave" "is" "white" "+")
Cold, quiet people are white.
((("someone" "is" "cold" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "white" "+"))
If someone is green then they are white.
((("someone" "is" "green" "+")) -> ("someone" "is" "white" "+"))
All white people are smart.
((("someone" "is" "white" "+")) -> ("someone" "is" "smart" "+"))
If Dave is cold and Dave is white then Dave is green.
((("Dave" "is" "cold" "+") ("Dave" "is" "white" "+")) -> ("Dave" "is" "green" "+"))
All big people are not quiet.
((("someone" "is" "big" "+")) -> ("someone" "is" "quiet" "-"))
If someone is smart and big then they are not green.
((("someone" "is" "smart" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "green" "-"))
All big people are green.
((("someone" "is" "big" "+")) -> ("someone" "is" "green" "+"))
If someone is quiet and not red then they are big.
((("someone" "is" "quiet" "+") ("someone" "is" "red" "~")) -> ("someone" "is" "big" "+"))
Dave is white.
True
1
proof
[(triple2)]
("Dave" "is" "white" "+")
triple2
Dave is not white.
False
1
inv-proof
[(triple2)]
("Dave" "is" "white" "-")
triple2
Dave is smart.
True
2
proof
[(((triple2) -> rule3))]
("Dave" "is" "smart" "+")
((triple2) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is not smart.
False
2
inv-proof
[(((triple2) -> rule3))]
("Dave" "is" "smart" "-")
((triple2) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is not big.
Unknown
inv-rconc
[@1: Dave is big.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Dave" "is" "big" "-")
Charlie is big.
Unknown
rconc
[@1: Charlie is big.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Charlie" "is" "big" "+")
Dave is not red.
Unknown
inv-random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "-")
Dave is quiet.
Unknown
random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "+")
@0: Charlie is cold.[(triple1)] Dave is white.[(triple2)] @1: Dave is smart.[(((triple2) -> rule3))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
Dave is white.
("Dave" "is" "white" "+")
triple2
Dave is smart.
("Dave" "is" "smart" "+")
((triple2) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1