Bob is blue. Gary is white. Harry is green. If someone is green and blue then they are round. Nice, round people are white. If Gary is nice then Gary is white. If Bob is white and Bob is green then Bob is round. Round people are quiet. If someone is green then they are rough. If Gary is nice and Gary is rough then Gary is white. All white people are green.
Bob is blue.
("Bob" "is" "blue" "+")
Gary is white.
("Gary" "is" "white" "+")
Harry is green.
("Harry" "is" "green" "+")
If someone is green and blue then they are round.
((("someone" "is" "green" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "round" "+"))
Nice, round people are white.
((("someone" "is" "nice" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "white" "+"))
If Gary is nice then Gary is white.
((("Gary" "is" "nice" "+")) -> ("Gary" "is" "white" "+"))
If Bob is white and Bob is green then Bob is round.
((("Bob" "is" "white" "+") ("Bob" "is" "green" "+")) -> ("Bob" "is" "round" "+"))
Round people are quiet.
((("someone" "is" "round" "+")) -> ("someone" "is" "quiet" "+"))
If someone is green then they are rough.
((("someone" "is" "green" "+")) -> ("someone" "is" "rough" "+"))
If Gary is nice and Gary is rough then Gary is white.
((("Gary" "is" "nice" "+") ("Gary" "is" "rough" "+")) -> ("Gary" "is" "white" "+"))
All white people are green.
((("someone" "is" "white" "+")) -> ("someone" "is" "green" "+"))
Bob is blue.
True
1
proof
[(triple1)]
("Bob" "is" "blue" "+")
triple1
Bob is not blue.
False
1
inv-proof
[(triple1)]
("Bob" "is" "blue" "-")
triple1
Gary is green.
True
2
proof
[(((triple2) -> rule8))]
("Gary" "is" "green" "+")
((triple2) -> (rule8 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is not green.
False
2
inv-proof
[(((triple2) -> rule8))]
("Gary" "is" "green" "-")
((triple2) -> (rule8 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is rough.
True
3
proof
[(((((triple2) -> rule8)) -> rule6))]
("Gary" "is" "rough" "+")
((((triple2) -> (rule8 % int2))) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is not rough.
False
3
inv-proof
[(((((triple2) -> rule8)) -> rule6))]
("Gary" "is" "rough" "-")
((((triple2) -> (rule8 % int2))) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Bob is not round.
Unknown
inv-rconc
[@3: Bob is round.[CWA. Example of deepest failure = (rule1 <- rule8 <- rule2 <- FAIL)]]
("Bob" "is" "round" "-")
Harry is white.
Unknown
rconc
[@1: Harry is white.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "white" "+")
Gary is not quiet.
Unknown
inv-rconc
[@2: Gary is quiet.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("Gary" "is" "quiet" "-")
Gary is blue.
Unknown
random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "+")
Gary is not nice.
Unknown
inv-random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "-")
Bob is nice.
Unknown
random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "+")
@0: Bob is blue.[(triple1)] Gary is white.[(triple2)] Harry is green.[(triple3)] @1: Gary is green.[(((triple2) -> rule8))] Harry is rough.[(((triple3) -> rule6))] @2: Gary is rough.[(((((triple2) -> rule8)) -> rule6))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Gary is white.
("Gary" "is" "white" "+")
triple2
Harry is green.
("Harry" "is" "green" "+")
triple3
Gary is green.
("Gary" "is" "green" "+")
((triple2) -> (rule8 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
((triple3) -> (rule6 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
((((triple2) -> (rule8 % int2))) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2