Bob is blue. Bob is kind. Bob is nice. Bob is quiet. Bob is young. Charlie is furry. Charlie is kind. Charlie is not nice. Charlie is not round. Harry is young. All furry, quiet things are blue. If Harry is kind and Harry is not furry then Harry is not quiet. Furry things are quiet.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is young.
("Bob" "is" "young" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is not nice.
("Charlie" "is" "nice" "-")
Charlie is not round.
("Charlie" "is" "round" "-")
Harry is young.
("Harry" "is" "young" "+")
All furry, quiet things are blue.
((("something" "is" "furry" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "blue" "+"))
If Harry is kind and Harry is not furry then Harry is not quiet.
((("Harry" "is" "kind" "+") ("Harry" "is" "furry" "~")) -> ("Harry" "is" "quiet" "-"))
Furry things are quiet.
((("something" "is" "furry" "+")) -> ("something" "is" "quiet" "+"))
Charlie is not round.
True
1
proof
[(triple9)]
("Charlie" "is" "round" "-")
triple9
Harry is not young.
False
1
inv-proof
[(triple10)]
("Harry" "is" "young" "-")
triple10
Charlie is quiet.
True
2
proof
[(((triple6) -> rule3))]
("Charlie" "is" "quiet" "+")
((triple6) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is not quiet.
False
2
inv-proof
[(((triple6) -> rule3))]
("Charlie" "is" "quiet" "-")
((triple6) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is blue.
True
4
proof
[(((triple6 ((triple6) -> rule3)) -> rule1))]
("Charlie" "is" "blue" "+")
((triple6 ((triple6) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is not blue.
False
4
inv-proof
[(((triple6 ((triple6) -> rule3)) -> rule1))]
("Charlie" "is" "blue" "-")
((triple6 ((triple6) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Harry is not quiet.
Unknown
inv-rconc
[@1: Harry is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "quiet" "-")
Harry is blue.
Unknown
rconc
[@1: Harry is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "blue" "+")
Bob is not round.
Unknown
inv-random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "-")
Harry is nice.
Unknown
random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "+")
Charlie is not young.
Unknown
inv-random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "-")
Bob is furry.
Unknown
random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "+")
@0: Bob is blue.[(triple1)] Bob is kind.[(triple2)] Bob is nice.[(triple3)] Bob is quiet.[(triple4)] Bob is young.[(triple5)] Charlie is furry.[(triple6)] Charlie is kind.[(triple7)] Charlie is not nice.[(triple8)] Charlie is not round.[(triple9)] Harry is young.[(triple10)] @1: Charlie is quiet.[(((triple6) -> rule3))] @2: Charlie is blue.[(((triple6 ((triple6) -> rule3)) -> rule1))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is kind.
("Bob" "is" "kind" "+")
triple2
Bob is nice.
("Bob" "is" "nice" "+")
triple3
Bob is quiet.
("Bob" "is" "quiet" "+")
triple4
Bob is young.
("Bob" "is" "young" "+")
triple5
Charlie is furry.
("Charlie" "is" "furry" "+")
triple6
Charlie is kind.
("Charlie" "is" "kind" "+")
triple7
Charlie is not nice.
("Charlie" "is" "nice" "-")
triple8
Charlie is not round.
("Charlie" "is" "round" "-")
triple9
Harry is young.
("Harry" "is" "young" "+")
triple10
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple6) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple6 ((triple6) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2