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