Charlie is blue. Dave is quiet. Erin is white. Harry is smart. All red people are quiet. Blue people are white. If someone is nice and blue then they are green.
Charlie is blue.
("Charlie" "is" "blue" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Erin is white.
("Erin" "is" "white" "+")
Harry is smart.
("Harry" "is" "smart" "+")
All red people are quiet.
((("someone" "is" "red" "+")) -> ("someone" "is" "quiet" "+"))
Blue people are white.
((("someone" "is" "blue" "+")) -> ("someone" "is" "white" "+"))
If someone is nice and blue then they are green.
((("someone" "is" "nice" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "green" "+"))
Charlie is blue.
True
1
proof
[(triple1)]
("Charlie" "is" "blue" "+")
triple1
Erin is not white.
False
1
inv-proof
[(triple3)]
("Erin" "is" "white" "-")
triple3
Charlie is white.
True
2
proof
[(((triple1) -> rule2))]
("Charlie" "is" "white" "+")
((triple1) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is not white.
False
2
inv-proof
[(((triple1) -> rule2))]
("Charlie" "is" "white" "-")
((triple1) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Dave is not green.
Unknown
inv-rconc
[@1: Dave is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "green" "-")
Charlie is green.
Unknown
rconc
[@1: Charlie is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "green" "+")
Dave is not nice.
Unknown
inv-random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "-")
Harry is nice.
Unknown
random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "+")
@0: Charlie is blue.[(triple1)] Dave is quiet.[(triple2)] Erin is white.[(triple3)] Harry is smart.[(triple4)] @1: Charlie is white.[(((triple1) -> rule2))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple2
Erin is white.
("Erin" "is" "white" "+")
triple3
Harry is smart.
("Harry" "is" "smart" "+")
triple4
Charlie is white.
("Charlie" "is" "white" "+")
((triple1) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1