Bob is blue. Bob is furry. Bob is kind. Bob is not round. Gary is blue. Gary is furry. Gary is kind. Gary is not quiet. Gary is red. Gary is not round. Harry is kind. Harry is young. All furry people are kind. If someone is young and kind then they are not round. All round people are not quiet. If Gary is quiet then Gary is blue. If someone is round and not kind then they are young. If Harry is young and Harry is not round then Harry is not blue. If someone is red and not young then they are not blue. If someone is young and furry then they are not blue.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is not round.
("Bob" "is" "round" "-")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is not quiet.
("Gary" "is" "quiet" "-")
Gary is red.
("Gary" "is" "red" "+")
Gary is not round.
("Gary" "is" "round" "-")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is young.
("Harry" "is" "young" "+")
All furry people are kind.
((("someone" "is" "furry" "+")) -> ("someone" "is" "kind" "+"))
If someone is young and kind then they are not round.
((("someone" "is" "young" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "round" "-"))
All round people are not quiet.
((("someone" "is" "round" "+")) -> ("someone" "is" "quiet" "-"))
If Gary is quiet then Gary is blue.
((("Gary" "is" "quiet" "+")) -> ("Gary" "is" "blue" "+"))
If someone is round and not kind then they are young.
((("someone" "is" "round" "+") ("someone" "is" "kind" "~")) -> ("someone" "is" "young" "+"))
If Harry is young and Harry is not round then Harry is not blue.
((("Harry" "is" "young" "+") ("Harry" "is" "round" "~")) -> ("Harry" "is" "blue" "-"))
If someone is red and not young then they are not blue.
((("someone" "is" "red" "+") ("someone" "is" "young" "~")) -> ("someone" "is" "blue" "-"))
If someone is young and furry then they are not blue.
((("someone" "is" "young" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "blue" "-"))
Bob is furry.
True
1
proof
[(triple2)]
("Bob" "is" "furry" "+")
triple2
Gary is round.
False
1
inv-proof
[(triple10)]
("Gary" "is" "round" "+")
triple10
Harry is not round.
True
3
proof
[(((triple12 triple11) -> rule2))]
("Harry" "is" "round" "-")
((triple12 triple11) -> (rule2 % int1))
Harry is not round.
("Harry" "is" "round" "-")
int1
Harry is round.
False
3
inv-proof
[(((triple12 triple11) -> rule2))]
("Harry" "is" "round" "+")
((triple12 triple11) -> (rule2 % int1))
Harry is not round.
("Harry" "is" "round" "-")
int1
Harry is not blue.
True
5
proof
[(((triple12 ((triple12 triple11) -> rule2)) -> rule6))]
("Harry" "is" "blue" "-")
((triple12 ((triple12 triple11) -> (rule2 % int2))) -> (rule6 % int1))
Harry is not blue.
("Harry" "is" "blue" "-")
int1
Harry is not round.
("Harry" "is" "round" "-")
int2
Harry is blue.
False
5
inv-proof
[(((triple12 ((triple12 triple11) -> rule2)) -> rule6))]
("Harry" "is" "blue" "+")
((triple12 ((triple12 triple11) -> (rule2 % int2))) -> (rule6 % int1))
Harry is not blue.
("Harry" "is" "blue" "-")
int1
Harry is not round.
("Harry" "is" "round" "-")
int2
Bob is not young.
Unknown
inv-rconc
[@1: Bob is young.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "young" "-")
Gary is young.
Unknown
rconc
[@1: Gary is young.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Gary" "is" "young" "+")
Harry is not red.
Unknown
inv-random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "-")
Harry is furry.
Unknown
random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "+")
Bob is not quiet.
Unknown
inv-random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "-")
Harry is quiet.
Unknown
random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "+")
@0: Bob is blue.[(triple1)] Bob is furry.[(triple2)] Bob is kind.[(triple3 OR ((triple2) -> rule1))] Bob is not round.[(triple4)] Gary is blue.[(triple5)] Gary is furry.[(triple6)] Gary is kind.[(triple7 OR ((triple6) -> rule1))] Gary is not quiet.[(triple8)] Gary is not round.[(triple10)] Gary is red.[(triple9)] Harry is kind.[(triple11)] Harry is young.[(triple12)] @1: Harry is not round.[(((triple12 triple11) -> rule2))] @2: Harry is not blue.[(((triple12 ((triple12 triple11) -> rule2)) -> rule6))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Bob is kind.
("Bob" "is" "kind" "+")
triple3
((triple2) -> (rule1 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is not round.
("Bob" "is" "round" "-")
triple4
Gary is blue.
("Gary" "is" "blue" "+")
triple5
Gary is furry.
("Gary" "is" "furry" "+")
triple6
Gary is kind.
("Gary" "is" "kind" "+")
triple7
((triple6) -> (rule1 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is not quiet.
("Gary" "is" "quiet" "-")
triple8
Gary is not round.
("Gary" "is" "round" "-")
triple10
Gary is red.
("Gary" "is" "red" "+")
triple9
Harry is kind.
("Harry" "is" "kind" "+")
triple11
Harry is young.
("Harry" "is" "young" "+")
triple12
Harry is not round.
("Harry" "is" "round" "-")
((triple12 triple11) -> (rule2 % int1))
Harry is not round.
("Harry" "is" "round" "-")
int1
Harry is not blue.
("Harry" "is" "blue" "-")
((triple12 ((triple12 triple11) -> (rule2 % int2))) -> (rule6 % int1))
Harry is not blue.
("Harry" "is" "blue" "-")
int1
Harry is not round.
("Harry" "is" "round" "-")
int2