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