Harry is round. Green, kind things are white. Round things are white. If something is white and round then it is green. All kind, green things are quiet. If Harry is round and Harry is green then Harry is young. If something is round and not green then it is rough.
Harry is round.
("Harry" "is" "round" "+")
Green, kind things are white.
((("something" "is" "green" "+") ("something" "is" "kind" "+")) -> ("something" "is" "white" "+"))
Round things are white.
((("something" "is" "round" "+")) -> ("something" "is" "white" "+"))
If something is white and round then it is green.
((("something" "is" "white" "+") ("something" "is" "round" "+")) -> ("something" "is" "green" "+"))
All kind, green things are quiet.
((("something" "is" "kind" "+") ("something" "is" "green" "+")) -> ("something" "is" "quiet" "+"))
If Harry is round and Harry is green then Harry is young.
((("Harry" "is" "round" "+") ("Harry" "is" "green" "+")) -> ("Harry" "is" "young" "+"))
If something is round and not green then it is rough.
((("something" "is" "round" "+") ("something" "is" "green" "~")) -> ("something" "is" "rough" "+"))
Harry is round.
True
1
proof
[(triple1)]
("Harry" "is" "round" "+")
triple1
Harry is not round.
False
1
inv-proof
[(triple1)]
("Harry" "is" "round" "-")
triple1
Harry is white.
True
2
proof
[(((triple1) -> rule2))]
("Harry" "is" "white" "+")
((triple1) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is not white.
False
2
inv-proof
[(((triple1) -> rule2))]
("Harry" "is" "white" "-")
((triple1) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is green.
True
4
proof
[(((((triple1) -> rule2) triple1) -> rule3))]
("Harry" "is" "green" "+")
((((triple1) -> (rule2 % int2)) triple1) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is not green.
False
4
inv-proof
[(((((triple1) -> rule2) triple1) -> rule3))]
("Harry" "is" "green" "-")
((((triple1) -> (rule2 % int2)) triple1) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is young.
True
6
proof
[(((triple1 ((((triple1) -> rule2) triple1) -> rule3)) -> rule5))]
("Harry" "is" "young" "+")
((triple1 ((((triple1) -> (rule2 % int3)) triple1) -> (rule3 % int2))) -> (rule5 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is not young.
False
6
inv-proof
[(((triple1 ((((triple1) -> rule2) triple1) -> rule3)) -> rule5))]
("Harry" "is" "young" "-")
((triple1 ((((triple1) -> (rule2 % int3)) triple1) -> (rule3 % int2))) -> (rule5 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is not quiet.
Unknown
inv-rconc
[@1: Harry is quiet.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Harry" "is" "quiet" "-")
Harry is rough.
Unknown
rconc
[@1: Harry is rough.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "rough" "+")
@0: Harry is round.[(triple1)] @1: Harry is white.[(((triple1) -> rule2))] @2: Harry is green.[(((((triple1) -> rule2) triple1) -> rule3))] @3: Harry is young.[(((triple1 ((((triple1) -> rule2) triple1) -> rule3)) -> rule5))]
Harry is round.
("Harry" "is" "round" "+")
triple1
Harry is white.
("Harry" "is" "white" "+")
((triple1) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
((((triple1) -> (rule2 % int2)) triple1) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
((triple1 ((((triple1) -> (rule2 % int3)) triple1) -> (rule3 % int2))) -> (rule5 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3