Anne is round. Bob is rough. Gary is white. Harry is white. All blue people are red. If Harry is rough then Harry is blue. All red, white people are round. White people are blue. If Bob is round and Bob is blue then Bob is kind. If someone is blue and not white then they are quiet.
Anne is round.
("Anne" "is" "round" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Gary is white.
("Gary" "is" "white" "+")
Harry is white.
("Harry" "is" "white" "+")
All blue people are red.
((("someone" "is" "blue" "+")) -> ("someone" "is" "red" "+"))
If Harry is rough then Harry is blue.
((("Harry" "is" "rough" "+")) -> ("Harry" "is" "blue" "+"))
All red, white people are round.
((("someone" "is" "red" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "round" "+"))
White people are blue.
((("someone" "is" "white" "+")) -> ("someone" "is" "blue" "+"))
If Bob is round and Bob is blue then Bob is kind.
((("Bob" "is" "round" "+") ("Bob" "is" "blue" "+")) -> ("Bob" "is" "kind" "+"))
If someone is blue and not white then they are quiet.
((("someone" "is" "blue" "+") ("someone" "is" "white" "~")) -> ("someone" "is" "quiet" "+"))
Bob is rough.
True
1
proof
[(triple2)]
("Bob" "is" "rough" "+")
triple2
Gary is not white.
False
1
inv-proof
[(triple3)]
("Gary" "is" "white" "-")
triple3
Harry is blue.
True
2
proof
[(((triple4) -> rule4))]
("Harry" "is" "blue" "+")
((triple4) -> (rule4 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is not blue.
False
2
inv-proof
[(((triple4) -> rule4))]
("Harry" "is" "blue" "-")
((triple4) -> (rule4 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is red.
True
3
proof
[(((((triple4) -> rule4)) -> rule1))]
("Harry" "is" "red" "+")
((((triple4) -> (rule4 % int2))) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is not red.
False
3
inv-proof
[(((((triple4) -> rule4)) -> rule1))]
("Harry" "is" "red" "-")
((((triple4) -> (rule4 % int2))) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Gary is round.
True
5
proof
[(((((((triple3) -> rule4)) -> rule1) triple3) -> rule3))]
("Gary" "is" "round" "+")
((((((triple3) -> (rule4 % int3))) -> (rule1 % int2)) triple3) -> (rule3 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Harry is not round.
False
5
inv-proof
[(((((((triple4) -> rule4)) -> rule1) triple4) -> rule3))]
("Harry" "is" "round" "-")
((((((triple4) -> (rule4 % int3))) -> (rule1 % int2)) triple4) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Anne is not red.
Unknown
inv-rconc
[@2: Anne is red.[CWA. Example of deepest failure = (rule1 <- rule4 <- FAIL)]]
("Anne" "is" "red" "-")
Bob is blue.
Unknown
rconc
[@1: Bob is blue.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Bob" "is" "blue" "+")
Harry is not quiet.
Unknown
inv-rconc
[@1: Harry is quiet.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "quiet" "-")
Gary is quiet.
Unknown
rconc
[@1: Gary is quiet.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Gary" "is" "quiet" "+")
Gary is not kind.
Unknown
inv-random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "-")
Anne is rough.
Unknown
random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "+")
Anne is not white.
Unknown
inv-random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "-")
Bob is white.
Unknown
random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "+")
@0: Anne is round.[(triple1)] Bob is rough.[(triple2)] Gary is white.[(triple3)] Harry is white.[(triple4)] @1: Gary is blue.[(((triple3) -> rule4))] Harry is blue.[(((triple4) -> rule4))] @2: Gary is red.[(((((triple3) -> rule4)) -> rule1))] Harry is red.[(((((triple4) -> rule4)) -> rule1))] @3: Gary is round.[(((((((triple3) -> rule4)) -> rule1) triple3) -> rule3))] Harry is round.[(((((((triple4) -> rule4)) -> rule1) triple4) -> rule3))]
Anne is round.
("Anne" "is" "round" "+")
triple1
Bob is rough.
("Bob" "is" "rough" "+")
triple2
Gary is white.
("Gary" "is" "white" "+")
triple3
Harry is white.
("Harry" "is" "white" "+")
triple4
Gary is blue.
("Gary" "is" "blue" "+")
((triple3) -> (rule4 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((triple4) -> (rule4 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
((((triple3) -> (rule4 % int2))) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
((((triple4) -> (rule4 % int2))) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
((((((triple3) -> (rule4 % int3))) -> (rule1 % int2)) triple3) -> (rule3 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Harry is round.
("Harry" "is" "round" "+")
((((((triple4) -> (rule4 % int3))) -> (rule1 % int2)) triple4) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3