Harry is not cold. Harry is quiet. Harry is round. All round people are not young. All cold people are round. If Harry is not young then Harry is not rough.
Harry is not cold.
("Harry" "is" "cold" "-")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is round.
("Harry" "is" "round" "+")
All round people are not young.
((("someone" "is" "round" "+")) -> ("someone" "is" "young" "-"))
All cold people are round.
((("someone" "is" "cold" "+")) -> ("someone" "is" "round" "+"))
If Harry is not young then Harry is not rough.
((("Harry" "is" "young" "~")) -> ("Harry" "is" "rough" "-"))
Harry is quiet.
True
1
proof
[(triple2)]
("Harry" "is" "quiet" "+")
triple2
Harry is not quiet.
False
1
inv-proof
[(triple2)]
("Harry" "is" "quiet" "-")
triple2
Harry is not young.
True
2
proof
[(((triple3) -> rule1))]
("Harry" "is" "young" "-")
((triple3) -> (rule1 % int1))
Harry is not young.
("Harry" "is" "young" "-")
int1
Harry is young.
False
2
inv-proof
[(((triple3) -> rule1))]
("Harry" "is" "young" "+")
((triple3) -> (rule1 % int1))
Harry is not young.
("Harry" "is" "young" "-")
int1
Harry is not rough.
True
3
proof
[(((((triple3) -> rule1)) -> rule3))]
("Harry" "is" "rough" "-")
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
Harry is not rough.
("Harry" "is" "rough" "-")
int1
Harry is not young.
("Harry" "is" "young" "-")
int2
Harry is rough.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule3))]
("Harry" "is" "rough" "+")
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
Harry is not rough.
("Harry" "is" "rough" "-")
int1
Harry is not young.
("Harry" "is" "young" "-")
int2
Harry is not red.
Unknown
inv-random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "-")
Harry is smart.
Unknown
random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "+")
@0: Harry is not cold.[(triple1)] Harry is quiet.[(triple2)] Harry is round.[(triple3)] @1: Harry is not young.[(((triple3) -> rule1))] @2: Harry is not rough.[(((((triple3) -> rule1)) -> rule3))]
Harry is not cold.
("Harry" "is" "cold" "-")
triple1
Harry is quiet.
("Harry" "is" "quiet" "+")
triple2
Harry is round.
("Harry" "is" "round" "+")
triple3
Harry is not young.
("Harry" "is" "young" "-")
((triple3) -> (rule1 % int1))
Harry is not young.
("Harry" "is" "young" "-")
int1
Harry is not rough.
("Harry" "is" "rough" "-")
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
Harry is not rough.
("Harry" "is" "rough" "-")
int1
Harry is not young.
("Harry" "is" "young" "-")
int2