Harry is big. Harry is kind. Harry is young. If something is white and not red then it is not cold. If something is kind then it is round. If something is white then it is kind. All round things are not white. If Harry is not round then Harry is not young. If Harry is red and Harry is not big then Harry is not young.
Harry is big.
("Harry" "is" "big" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is young.
("Harry" "is" "young" "+")
If something is white and not red then it is not cold.
((("something" "is" "white" "+") ("something" "is" "red" "~")) -> ("something" "is" "cold" "-"))
If something is kind then it is round.
((("something" "is" "kind" "+")) -> ("something" "is" "round" "+"))
If something is white then it is kind.
((("something" "is" "white" "+")) -> ("something" "is" "kind" "+"))
All round things are not white.
((("something" "is" "round" "+")) -> ("something" "is" "white" "-"))
If Harry is not round then Harry is not young.
((("Harry" "is" "round" "~")) -> ("Harry" "is" "young" "-"))
If Harry is red and Harry is not big then Harry is not young.
((("Harry" "is" "red" "+") ("Harry" "is" "big" "~")) -> ("Harry" "is" "young" "-"))
Harry is young.
True
1
proof
[(triple3)]
("Harry" "is" "young" "+")
triple3
Harry is not kind.
False
1
inv-proof
[(triple2)]
("Harry" "is" "kind" "-")
triple2
Harry is round.
True
2
proof
[(((triple2) -> rule2))]
("Harry" "is" "round" "+")
((triple2) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is not round.
False
2
inv-proof
[(((triple2) -> rule2))]
("Harry" "is" "round" "-")
((triple2) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is not white.
True
3
proof
[(((((triple2) -> rule2)) -> rule4))]
("Harry" "is" "white" "-")
((((triple2) -> (rule2 % int2))) -> (rule4 % int1))
Harry is not white.
("Harry" "is" "white" "-")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is white.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule4))]
("Harry" "is" "white" "+")
((((triple2) -> (rule2 % int2))) -> (rule4 % int1))
Harry is not white.
("Harry" "is" "white" "-")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is not cold.
Unknown
inv-random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "-")
Harry is red.
Unknown
random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "+")
@0: Harry is big.[(triple1)] Harry is kind.[(triple2)] Harry is young.[(triple3)] @1: Harry is round.[(((triple2) -> rule2))] @2: Harry is not white.[(((((triple2) -> rule2)) -> rule4))]
Harry is big.
("Harry" "is" "big" "+")
triple1
Harry is kind.
("Harry" "is" "kind" "+")
triple2
Harry is young.
("Harry" "is" "young" "+")
triple3
Harry is round.
("Harry" "is" "round" "+")
((triple2) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is not white.
("Harry" "is" "white" "-")
((((triple2) -> (rule2 % int2))) -> (rule4 % int1))
Harry is not white.
("Harry" "is" "white" "-")
int1
Harry is round.
("Harry" "is" "round" "+")
int2