Harry is quiet. All quiet, young things are round. If Harry is quiet and Harry is red then Harry is rough. All young things are round. All rough things are quiet. All quiet things are young. If Harry is young and Harry is round then Harry is blue. If something is blue and red then it is quiet. All rough, red things are quiet.
Harry is quiet.
("Harry" "is" "quiet" "+")
All quiet, young things are round.
((("something" "is" "quiet" "+") ("something" "is" "young" "+")) -> ("something" "is" "round" "+"))
If Harry is quiet and Harry is red then Harry is rough.
((("Harry" "is" "quiet" "+") ("Harry" "is" "red" "+")) -> ("Harry" "is" "rough" "+"))
All young things are round.
((("something" "is" "young" "+")) -> ("something" "is" "round" "+"))
All rough things are quiet.
((("something" "is" "rough" "+")) -> ("something" "is" "quiet" "+"))
All quiet things are young.
((("something" "is" "quiet" "+")) -> ("something" "is" "young" "+"))
If Harry is young and Harry is round then Harry is blue.
((("Harry" "is" "young" "+") ("Harry" "is" "round" "+")) -> ("Harry" "is" "blue" "+"))
If something is blue and red then it is quiet.
((("something" "is" "blue" "+") ("something" "is" "red" "+")) -> ("something" "is" "quiet" "+"))
All rough, red things are quiet.
((("something" "is" "rough" "+") ("something" "is" "red" "+")) -> ("something" "is" "quiet" "+"))
Harry is quiet.
True
1
proof
[(triple1)]
("Harry" "is" "quiet" "+")
triple1
Harry is not quiet.
False
1
inv-proof
[(triple1)]
("Harry" "is" "quiet" "-")
triple1
Harry is young.
True
2
proof
[(((triple1) -> rule5))]
("Harry" "is" "young" "+")
((triple1) -> (rule5 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is not young.
False
2
inv-proof
[(((triple1) -> rule5))]
("Harry" "is" "young" "-")
((triple1) -> (rule5 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is not rough.
Unknown
inv-rconc
[@1: Harry is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "rough" "-")
Harry is smart.
Unknown
random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "+")
@0: Harry is quiet.[(triple1)] @1: Harry is young.[(((triple1) -> rule5))] @2: Harry is round.[(((((triple1) -> rule5)) -> rule3) OR ((triple1 ((triple1) -> rule5)) -> rule1))] @3: Harry is blue.[(((((triple1) -> rule5) ((((triple1) -> rule5)) -> rule3)) -> rule6) OR ((((triple1) -> rule5) ((triple1 ((triple1) -> rule5)) -> rule1)) -> rule6))]
Harry is quiet.
("Harry" "is" "quiet" "+")
triple1
Harry is young.
("Harry" "is" "young" "+")
((triple1) -> (rule5 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
((((triple1) -> (rule5 % int2))) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
((triple1 ((triple1) -> (rule5 % int2))) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
((((triple1) -> (rule5 % int3)) ((((triple1) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
((((triple1) -> (rule5 % int3)) ((triple1 ((triple1) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3