Bob is young. Harry is furry. If someone is furry and round then they are smart. Furry, round people are quiet. All young, furry people are quiet. If Harry is rough and Harry is furry then Harry is round. If Harry is smart then Harry is young. If someone is furry then they are rough.
Bob is young.
("Bob" "is" "young" "+")
Harry is furry.
("Harry" "is" "furry" "+")
If someone is furry and round then they are smart.
((("someone" "is" "furry" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "smart" "+"))
Furry, round people are quiet.
((("someone" "is" "furry" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "quiet" "+"))
All young, furry people are quiet.
((("someone" "is" "young" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "quiet" "+"))
If Harry is rough and Harry is furry then Harry is round.
((("Harry" "is" "rough" "+") ("Harry" "is" "furry" "+")) -> ("Harry" "is" "round" "+"))
If Harry is smart then Harry is young.
((("Harry" "is" "smart" "+")) -> ("Harry" "is" "young" "+"))
If someone is furry then they are rough.
((("someone" "is" "furry" "+")) -> ("someone" "is" "rough" "+"))
Bob is young.
True
1
proof
[(triple1)]
("Bob" "is" "young" "+")
triple1
Bob is not young.
False
1
inv-proof
[(triple1)]
("Bob" "is" "young" "-")
triple1
Harry is rough.
True
2
proof
[(((triple2) -> rule6))]
("Harry" "is" "rough" "+")
((triple2) -> (rule6 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is not rough.
False
2
inv-proof
[(((triple2) -> rule6))]
("Harry" "is" "rough" "-")
((triple2) -> (rule6 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is round.
True
4
proof
[(((((triple2) -> rule6) triple2) -> rule4))]
("Harry" "is" "round" "+")
((((triple2) -> (rule6 % int2)) triple2) -> (rule4 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is not round.
False
4
inv-proof
[(((((triple2) -> rule6) triple2) -> rule4))]
("Harry" "is" "round" "-")
((((triple2) -> (rule6 % int2)) triple2) -> (rule4 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Bob is not smart.
Unknown
inv-rconc
[@1: Bob is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "smart" "-")
Bob is rough.
Unknown
rconc
[@1: Bob is rough.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "rough" "+")
Bob is not quiet.
Unknown
inv-rconc
[@1: Bob is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "quiet" "-")
Bob is furry.
Unknown
random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "+")
Harry is not white.
Unknown
inv-random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "-")
Bob is round.
Unknown
random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "+")
@0: Bob is young.[(triple1)] Harry is furry.[(triple2)] @1: Harry is rough.[(((triple2) -> rule6))] @2: Harry is round.[(((((triple2) -> rule6) triple2) -> rule4))] @3: Harry is quiet.[(((triple2 ((((triple2) -> rule6) triple2) -> rule4)) -> rule2) OR ((((((triple2 ((((triple2) -> rule6) triple2) -> rule4)) -> rule1)) -> rule5) triple2) -> rule3))] Harry is smart.[(((triple2 ((((triple2) -> rule6) triple2) -> rule4)) -> rule1))] @4: Harry is young.[(((((triple2 ((((triple2) -> rule6) triple2) -> rule4)) -> rule1)) -> rule5))]
Bob is young.
("Bob" "is" "young" "+")
triple1
Harry is furry.
("Harry" "is" "furry" "+")
triple2
Harry is rough.
("Harry" "is" "rough" "+")
((triple2) -> (rule6 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
((((triple2) -> (rule6 % int2)) triple2) -> (rule4 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple2 ((((triple2) -> (rule6 % int3)) triple2) -> (rule4 % int2))) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
((((((triple2 ((((triple2) -> (rule6 % int5)) triple2) -> (rule4 % int4))) -> (rule1 % int3))) -> (rule5 % int2)) triple2) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Harry is round.
("Harry" "is" "round" "+")
int4
Harry is rough.
("Harry" "is" "rough" "+")
int5
Harry is smart.
("Harry" "is" "smart" "+")
((triple2 ((((triple2) -> (rule6 % int3)) triple2) -> (rule4 % int2))) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is young.
("Harry" "is" "young" "+")
((((triple2 ((((triple2) -> (rule6 % int4)) triple2) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
int4