Bob is kind. Bob is smart. Harry is kind. If someone is kind and furry then they are round. All kind people are young. If Harry is young then Harry is furry.
Bob is kind.
("Bob" "is" "kind" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Harry is kind.
("Harry" "is" "kind" "+")
If someone is kind and furry then they are round.
((("someone" "is" "kind" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "round" "+"))
All kind people are young.
((("someone" "is" "kind" "+")) -> ("someone" "is" "young" "+"))
If Harry is young then Harry is furry.
((("Harry" "is" "young" "+")) -> ("Harry" "is" "furry" "+"))
Bob is kind.
True
1
proof
[(triple1)]
("Bob" "is" "kind" "+")
triple1
Bob is not kind.
False
1
inv-proof
[(triple1)]
("Bob" "is" "kind" "-")
triple1
Bob is young.
True
2
proof
[(((triple1) -> rule2))]
("Bob" "is" "young" "+")
((triple1) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is not young.
False
2
inv-proof
[(((triple1) -> rule2))]
("Bob" "is" "young" "-")
((triple1) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Harry is furry.
True
3
proof
[(((((triple3) -> rule2)) -> rule3))]
("Harry" "is" "furry" "+")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is not furry.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule3))]
("Harry" "is" "furry" "-")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is round.
True
5
proof
[(((triple3 ((((triple3) -> rule2)) -> rule3)) -> rule1))]
("Harry" "is" "round" "+")
((triple3 ((((triple3) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Harry is not round.
False
5
inv-proof
[(((triple3 ((((triple3) -> rule2)) -> rule3)) -> rule1))]
("Harry" "is" "round" "-")
((triple3 ((((triple3) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Bob is not round.
Unknown
inv-rconc
[@1: Bob is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "round" "-")
Harry is big.
Unknown
random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "+")
Bob is not big.
Unknown
inv-random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "-")
Bob is furry.
Unknown
random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "+")
Harry is not blue.
Unknown
inv-random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "-")
Harry is smart.
Unknown
random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "+")
@0: Bob is kind.[(triple1)] Bob is smart.[(triple2)] Harry is kind.[(triple3)] @1: Bob is young.[(((triple1) -> rule2))] Harry is young.[(((triple3) -> rule2))] @2: Harry is furry.[(((((triple3) -> rule2)) -> rule3))] @3: Harry is round.[(((triple3 ((((triple3) -> rule2)) -> rule3)) -> rule1))]
Bob is kind.
("Bob" "is" "kind" "+")
triple1
Bob is smart.
("Bob" "is" "smart" "+")
triple2
Harry is kind.
("Harry" "is" "kind" "+")
triple3
Bob is young.
("Bob" "is" "young" "+")
((triple1) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
((triple3) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
((triple3 ((((triple3) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3