Harry is kind. Rough, green people are kind. All kind, green people are not cold. All kind people are green. If Harry is white then Harry is round. If Harry is green and Harry is not cold then Harry is white. If someone is round and not green then they are white.
Harry is kind.
("Harry" "is" "kind" "+")
Rough, green people are kind.
((("someone" "is" "rough" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "kind" "+"))
All kind, green people are not cold.
((("someone" "is" "kind" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "cold" "-"))
All kind people are green.
((("someone" "is" "kind" "+")) -> ("someone" "is" "green" "+"))
If Harry is white then Harry is round.
((("Harry" "is" "white" "+")) -> ("Harry" "is" "round" "+"))
If Harry is green and Harry is not cold then Harry is white.
((("Harry" "is" "green" "+") ("Harry" "is" "cold" "~")) -> ("Harry" "is" "white" "+"))
If someone is round and not green then they are white.
((("someone" "is" "round" "+") ("someone" "is" "green" "~")) -> ("someone" "is" "white" "+"))
Harry is kind.
True
1
proof
[(triple1)]
("Harry" "is" "kind" "+")
triple1
Harry is not kind.
False
1
inv-proof
[(triple1)]
("Harry" "is" "kind" "-")
triple1
Harry is green.
True
2
proof
[(((triple1) -> rule3))]
("Harry" "is" "green" "+")
((triple1) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is not green.
False
2
inv-proof
[(((triple1) -> rule3))]
("Harry" "is" "green" "-")
((triple1) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is not cold.
True
4
proof
[(((triple1 ((triple1) -> rule3)) -> rule2))]
("Harry" "is" "cold" "-")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Harry is not cold.
("Harry" "is" "cold" "-")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is cold.
False
4
inv-proof
[(((triple1 ((triple1) -> rule3)) -> rule2))]
("Harry" "is" "cold" "+")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Harry is not cold.
("Harry" "is" "cold" "-")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is white.
True
7
proof
[(((((triple1) -> rule3) ((triple1 ((triple1) -> rule3)) -> rule2)) -> rule5))]
("Harry" "is" "white" "+")
((((triple1) -> (rule3 % int3)) ((triple1 ((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is not cold.
("Harry" "is" "cold" "-")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is not white.
False
7
inv-proof
[(((((triple1) -> rule3) ((triple1 ((triple1) -> rule3)) -> rule2)) -> rule5))]
("Harry" "is" "white" "-")
((((triple1) -> (rule3 % int3)) ((triple1 ((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is not cold.
("Harry" "is" "cold" "-")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is not rough.
Unknown
inv-random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "-")
Harry is quiet.
Unknown
random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "+")
@0: Harry is kind.[(triple1)] @1: Harry is green.[(((triple1) -> rule3))] @2: Harry is not cold.[(((triple1 ((triple1) -> rule3)) -> rule2))] @3: Harry is white.[(((((triple1) -> rule3) ((triple1 ((triple1) -> rule3)) -> rule2)) -> rule5))] @4: Harry is round.[(((((((triple1) -> rule3) ((triple1 ((triple1) -> rule3)) -> rule2)) -> rule5)) -> rule4))]
Harry is kind.
("Harry" "is" "kind" "+")
triple1
Harry is green.
("Harry" "is" "green" "+")
((triple1) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is not cold.
("Harry" "is" "cold" "-")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Harry is not cold.
("Harry" "is" "cold" "-")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
((((triple1) -> (rule3 % int3)) ((triple1 ((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is not cold.
("Harry" "is" "cold" "-")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is round.
("Harry" "is" "round" "+")
((((((triple1) -> (rule3 % int4)) ((triple1 ((triple1) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is not cold.
("Harry" "is" "cold" "-")
int3
Harry is green.
("Harry" "is" "green" "+")
int4