Harry is kind. If Harry is kind then Harry is quiet. If something is white then it is round. Furry things are quiet. Quiet things are kind. If something is furry then it is white. If Harry is kind then Harry is round. If Harry is young then Harry is white. If something is quiet then it is young.
Harry is kind.
("Harry" "is" "kind" "+")
If Harry is kind then Harry is quiet.
((("Harry" "is" "kind" "+")) -> ("Harry" "is" "quiet" "+"))
If something is white then it is round.
((("something" "is" "white" "+")) -> ("something" "is" "round" "+"))
Furry things are quiet.
((("something" "is" "furry" "+")) -> ("something" "is" "quiet" "+"))
Quiet things are kind.
((("something" "is" "quiet" "+")) -> ("something" "is" "kind" "+"))
If something is furry then it is white.
((("something" "is" "furry" "+")) -> ("something" "is" "white" "+"))
If Harry is kind then Harry is round.
((("Harry" "is" "kind" "+")) -> ("Harry" "is" "round" "+"))
If Harry is young then Harry is white.
((("Harry" "is" "young" "+")) -> ("Harry" "is" "white" "+"))
If something is quiet then it is young.
((("something" "is" "quiet" "+")) -> ("something" "is" "young" "+"))
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 round.
True
2
proof
[(((triple1) -> rule6) OR ((((((((triple1) -> rule1)) -> rule8)) -> rule7)) -> rule2))]
("Harry" "is" "round" "+")
((triple1) -> (rule6 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
((((((((triple1) -> (rule1 % int4))) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Harry is quiet.
("Harry" "is" "quiet" "+")
int4
Harry is not round.
False
2
inv-proof
[(((triple1) -> rule6) OR ((((((((triple1) -> rule1)) -> rule8)) -> rule7)) -> rule2))]
("Harry" "is" "round" "-")
((triple1) -> (rule6 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
((((((((triple1) -> (rule1 % int4))) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Harry is quiet.
("Harry" "is" "quiet" "+")
int4
Harry is young.
True
3
proof
[(((((triple1) -> rule1)) -> rule8))]
("Harry" "is" "young" "+")
((((triple1) -> (rule1 % int2))) -> (rule8 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is not young.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule8))]
("Harry" "is" "young" "-")
((((triple1) -> (rule1 % int2))) -> (rule8 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is white.
True
4
proof
[(((((((triple1) -> rule1)) -> rule8)) -> rule7))]
("Harry" "is" "white" "+")
((((((triple1) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is not white.
False
4
inv-proof
[(((((((triple1) -> rule1)) -> rule8)) -> rule7))]
("Harry" "is" "white" "-")
((((((triple1) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is not smart.
Unknown
inv-random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "-")
Harry is furry.
Unknown
random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "+")
@0: Harry is kind.[(triple1)] @1: Harry is quiet.[(((triple1) -> rule1))] Harry is round.[(((triple1) -> rule6) OR ((((((((triple1) -> rule1)) -> rule8)) -> rule7)) -> rule2))] @2: Harry is young.[(((((triple1) -> rule1)) -> rule8))] @3: Harry is white.[(((((((triple1) -> rule1)) -> rule8)) -> rule7))]
Harry is kind.
("Harry" "is" "kind" "+")
triple1
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple1) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
((triple1) -> (rule6 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
((((((((triple1) -> (rule1 % int4))) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Harry is quiet.
("Harry" "is" "quiet" "+")
int4
Harry is young.
("Harry" "is" "young" "+")
((((triple1) -> (rule1 % int2))) -> (rule8 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
((((((triple1) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3