Gary is not furry. Harry is round. If Harry is round then Harry is blue. If Gary is round and Gary is blue then Gary is furry. All blue people are quiet. Red, quiet people are not white. If someone is white and not quiet then they are red. If someone is green and blue then they are not red. All quiet people are green. White people are green.
Gary is not furry.
("Gary" "is" "furry" "-")
Harry is round.
("Harry" "is" "round" "+")
If Harry is round then Harry is blue.
((("Harry" "is" "round" "+")) -> ("Harry" "is" "blue" "+"))
If Gary is round and Gary is blue then Gary is furry.
((("Gary" "is" "round" "+") ("Gary" "is" "blue" "+")) -> ("Gary" "is" "furry" "+"))
All blue people are quiet.
((("someone" "is" "blue" "+")) -> ("someone" "is" "quiet" "+"))
Red, quiet people are not white.
((("someone" "is" "red" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "white" "-"))
If someone is white and not quiet then they are red.
((("someone" "is" "white" "+") ("someone" "is" "quiet" "~")) -> ("someone" "is" "red" "+"))
If someone is green and blue then they are not red.
((("someone" "is" "green" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "red" "-"))
All quiet people are green.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "green" "+"))
White people are green.
((("someone" "is" "white" "+")) -> ("someone" "is" "green" "+"))
Gary is not furry.
True
1
proof
[(triple1)]
("Gary" "is" "furry" "-")
triple1
Harry is not round.
False
1
inv-proof
[(triple2)]
("Harry" "is" "round" "-")
triple2
Harry is blue.
True
2
proof
[(((triple2) -> rule1))]
("Harry" "is" "blue" "+")
((triple2) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is not blue.
False
2
inv-proof
[(((triple2) -> rule1))]
("Harry" "is" "blue" "-")
((triple2) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is quiet.
True
3
proof
[(((((triple2) -> rule1)) -> rule3))]
("Harry" "is" "quiet" "+")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is not quiet.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule3))]
("Harry" "is" "quiet" "-")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is green.
True
4
proof
[(((((((triple2) -> rule1)) -> rule3)) -> rule7))]
("Harry" "is" "green" "+")
((((((triple2) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is not green.
False
4
inv-proof
[(((((((triple2) -> rule1)) -> rule3)) -> rule7))]
("Harry" "is" "green" "-")
((((((triple2) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Gary is not quiet.
Unknown
inv-rconc
[@1: Gary is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "quiet" "-")
Gary is green.
Unknown
rconc
[@2: Gary is green.[CWA. Example of deepest failure = (rule7 <- rule3 <- FAIL)]]
("Gary" "is" "green" "+")
Gary is not red.
Unknown
inv-rconc
[@1: Gary is red.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Gary" "is" "red" "-")
Gary is blue.
Unknown
random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "+")
Harry is not white.
Unknown
inv-random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "-")
Gary is white.
Unknown
random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "+")
Gary is not round.
Unknown
inv-random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "-")
Harry is furry.
Unknown
random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "+")
@0: Gary is not furry.[(triple1)] Harry is round.[(triple2)] @1: Harry is blue.[(((triple2) -> rule1))] @2: Harry is quiet.[(((((triple2) -> rule1)) -> rule3))] @3: Harry is green.[(((((((triple2) -> rule1)) -> rule3)) -> rule7))] @4: Harry is not red.[(((((((((triple2) -> rule1)) -> rule3)) -> rule7) ((triple2) -> rule1)) -> rule6))]
Gary is not furry.
("Gary" "is" "furry" "-")
triple1
Harry is round.
("Harry" "is" "round" "+")
triple2
Harry is blue.
("Harry" "is" "blue" "+")
((triple2) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
((((((triple2) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is not red.
("Harry" "is" "red" "-")
((((((((triple2) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule7 % int2)) ((triple2) -> (rule1 % int4))) -> (rule6 % int1))
Harry is not red.
("Harry" "is" "red" "-")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is blue.
("Harry" "is" "blue" "+")
int4