Harry is white. All white people are kind. If someone is nice then they are not young. Furry people are not nice. All kind people are green. If someone is nice then they are green. Green people are not furry.
Harry is white.
("Harry" "is" "white" "+")
All white people are kind.
((("someone" "is" "white" "+")) -> ("someone" "is" "kind" "+"))
If someone is nice then they are not young.
((("someone" "is" "nice" "+")) -> ("someone" "is" "young" "-"))
Furry people are not nice.
((("someone" "is" "furry" "+")) -> ("someone" "is" "nice" "-"))
All kind people are green.
((("someone" "is" "kind" "+")) -> ("someone" "is" "green" "+"))
If someone is nice then they are green.
((("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
Green people are not furry.
((("someone" "is" "green" "+")) -> ("someone" "is" "furry" "-"))
Harry is white.
True
1
proof
[(triple1)]
("Harry" "is" "white" "+")
triple1
Harry is not white.
False
1
inv-proof
[(triple1)]
("Harry" "is" "white" "-")
triple1
Harry is kind.
True
2
proof
[(((triple1) -> rule1))]
("Harry" "is" "kind" "+")
((triple1) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is not kind.
False
2
inv-proof
[(((triple1) -> rule1))]
("Harry" "is" "kind" "-")
((triple1) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is green.
True
3
proof
[(((((triple1) -> rule1)) -> rule4))]
("Harry" "is" "green" "+")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is not green.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule4))]
("Harry" "is" "green" "-")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is not furry.
True
4
proof
[(((((((triple1) -> rule1)) -> rule4)) -> rule6))]
("Harry" "is" "furry" "-")
((((((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Harry is not furry.
("Harry" "is" "furry" "-")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is furry.
False
4
inv-proof
[(((((((triple1) -> rule1)) -> rule4)) -> rule6))]
("Harry" "is" "furry" "+")
((((((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Harry is not furry.
("Harry" "is" "furry" "-")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is not young.
Unknown
inv-random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "-")
Harry is cold.
Unknown
random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "+")
@0: Harry is white.[(triple1)] @1: Harry is kind.[(((triple1) -> rule1))] @2: Harry is green.[(((((triple1) -> rule1)) -> rule4))] @3: Harry is not furry.[(((((((triple1) -> rule1)) -> rule4)) -> rule6))]
Harry is white.
("Harry" "is" "white" "+")
triple1
Harry is kind.
("Harry" "is" "kind" "+")
((triple1) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is not furry.
("Harry" "is" "furry" "-")
((((((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Harry is not furry.
("Harry" "is" "furry" "-")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3