Harry is nice. If Harry is nice and Harry is quiet then Harry is smart. Furry, round things are smart. Quiet things are smart. If Harry is green then Harry is quiet. Nice things are green. If Harry is furry and Harry is nice then Harry is green.
Harry is nice.
("Harry" "is" "nice" "+")
If Harry is nice and Harry is quiet then Harry is smart.
((("Harry" "is" "nice" "+") ("Harry" "is" "quiet" "+")) -> ("Harry" "is" "smart" "+"))
Furry, round things are smart.
((("something" "is" "furry" "+") ("something" "is" "round" "+")) -> ("something" "is" "smart" "+"))
Quiet things are smart.
((("something" "is" "quiet" "+")) -> ("something" "is" "smart" "+"))
If Harry is green then Harry is quiet.
((("Harry" "is" "green" "+")) -> ("Harry" "is" "quiet" "+"))
Nice things are green.
((("something" "is" "nice" "+")) -> ("something" "is" "green" "+"))
If Harry is furry and Harry is nice then Harry is green.
((("Harry" "is" "furry" "+") ("Harry" "is" "nice" "+")) -> ("Harry" "is" "green" "+"))
Harry is nice.
True
1
proof
[(triple1)]
("Harry" "is" "nice" "+")
triple1
Harry is not nice.
False
1
inv-proof
[(triple1)]
("Harry" "is" "nice" "-")
triple1
Harry is green.
True
2
proof
[(((triple1) -> rule5))]
("Harry" "is" "green" "+")
((triple1) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is not green.
False
2
inv-proof
[(((triple1) -> rule5))]
("Harry" "is" "green" "-")
((triple1) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is not round.
Unknown
inv-random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "-")
Harry is furry.
Unknown
random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "+")
@0: Harry is nice.[(triple1)] @1: Harry is green.[(((triple1) -> rule5))] @2: Harry is quiet.[(((((triple1) -> rule5)) -> rule4))] @3: Harry is smart.[(((((((triple1) -> rule5)) -> rule4)) -> rule3) OR ((triple1 ((((triple1) -> rule5)) -> rule4)) -> rule1))]
Harry is nice.
("Harry" "is" "nice" "+")
triple1
Harry is green.
("Harry" "is" "green" "+")
((triple1) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((((triple1) -> (rule5 % int2))) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
((((((triple1) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
((triple1 ((((triple1) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3