Erin is rough. Harry is green. Harry is red. Furry, round things are quiet. If something is green then it is furry. If Harry is furry then Harry is round.
Erin is rough.
("Erin" "is" "rough" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is red.
("Harry" "is" "red" "+")
Furry, round things are quiet.
((("something" "is" "furry" "+") ("something" "is" "round" "+")) -> ("something" "is" "quiet" "+"))
If something is green then it is furry.
((("something" "is" "green" "+")) -> ("something" "is" "furry" "+"))
If Harry is furry then Harry is round.
((("Harry" "is" "furry" "+")) -> ("Harry" "is" "round" "+"))
Harry is green.
True
1
proof
[(triple2)]
("Harry" "is" "green" "+")
triple2
Harry is not green.
False
1
inv-proof
[(triple2)]
("Harry" "is" "green" "-")
triple2
Harry is furry.
True
2
proof
[(((triple2) -> rule2))]
("Harry" "is" "furry" "+")
((triple2) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is not furry.
False
2
inv-proof
[(((triple2) -> rule2))]
("Harry" "is" "furry" "-")
((triple2) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is round.
True
3
proof
[(((((triple2) -> rule2)) -> rule3))]
("Harry" "is" "round" "+")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is not round.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule3))]
("Harry" "is" "round" "-")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is quiet.
True
6
proof
[(((((triple2) -> rule2) ((((triple2) -> rule2)) -> rule3)) -> rule1))]
("Harry" "is" "quiet" "+")
((((triple2) -> (rule2 % int3)) ((((triple2) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is not quiet.
False
6
inv-proof
[(((((triple2) -> rule2) ((((triple2) -> rule2)) -> rule3)) -> rule1))]
("Harry" "is" "quiet" "-")
((((triple2) -> (rule2 % int3)) ((((triple2) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Erin is not quiet.
Unknown
inv-rconc
[@1: Erin is quiet.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "quiet" "-")
Erin is furry.
Unknown
rconc
[@1: Erin is furry.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "furry" "+")
Erin is not round.
Unknown
inv-random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "-")
Erin is big.
Unknown
random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "+")
Harry is not rough.
Unknown
inv-random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "-")
Harry is big.
Unknown
random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "+")
Erin is not green.
Unknown
inv-random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "-")
Erin is red.
Unknown
random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "+")
@0: Erin is rough.[(triple1)] Harry is green.[(triple2)] Harry is red.[(triple3)] @1: Harry is furry.[(((triple2) -> rule2))] @2: Harry is round.[(((((triple2) -> rule2)) -> rule3))] @3: Harry is quiet.[(((((triple2) -> rule2) ((((triple2) -> rule2)) -> rule3)) -> rule1))]
Erin is rough.
("Erin" "is" "rough" "+")
triple1
Harry is green.
("Harry" "is" "green" "+")
triple2
Harry is red.
("Harry" "is" "red" "+")
triple3
Harry is furry.
("Harry" "is" "furry" "+")
((triple2) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
((((triple2) -> (rule2 % int3)) ((((triple2) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3