Bob is blue. Bob is quiet. Bob is white. Bob is young. Harry is not blue. Harry is kind. Harry is white. If someone is blue and not green then they are young. Blue people are young. If Harry is blue then Harry is young. All young people are not kind. If Harry is not young then Harry is quiet. If someone is green and not kind then they are quiet. All white people are quiet. If someone is quiet and kind then they are white.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is white.
("Bob" "is" "white" "+")
Bob is young.
("Bob" "is" "young" "+")
Harry is not blue.
("Harry" "is" "blue" "-")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is white.
("Harry" "is" "white" "+")
If someone is blue and not green then they are young.
((("someone" "is" "blue" "+") ("someone" "is" "green" "~")) -> ("someone" "is" "young" "+"))
Blue people are young.
((("someone" "is" "blue" "+")) -> ("someone" "is" "young" "+"))
If Harry is blue then Harry is young.
((("Harry" "is" "blue" "+")) -> ("Harry" "is" "young" "+"))
All young people are not kind.
((("someone" "is" "young" "+")) -> ("someone" "is" "kind" "-"))
If Harry is not young then Harry is quiet.
((("Harry" "is" "young" "~")) -> ("Harry" "is" "quiet" "+"))
If someone is green and not kind then they are quiet.
((("someone" "is" "green" "+") ("someone" "is" "kind" "~")) -> ("someone" "is" "quiet" "+"))
All white people are quiet.
((("someone" "is" "white" "+")) -> ("someone" "is" "quiet" "+"))
If someone is quiet and kind then they are white.
((("someone" "is" "quiet" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "white" "+"))
Bob is white.
True
1
proof
[(triple3)]
("Bob" "is" "white" "+")
triple3
Bob is not young.
False
1
inv-proof
[(triple4 OR ((triple1) -> rule2))]
("Bob" "is" "young" "-")
triple4
((triple1) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Harry is quiet.
True
2
proof
[(((triple7) -> rule7))]
("Harry" "is" "quiet" "+")
((triple7) -> (rule7 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Bob is kind.
False
2
inv-proof
[(((triple4) -> rule4) OR ((((triple1) -> rule2)) -> rule4))]
("Bob" "is" "kind" "+")
((triple4) -> (rule4 % int1))
Bob is not kind.
("Bob" "is" "kind" "-")
int1
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Bob is not kind.
("Bob" "is" "kind" "-")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Harry is not young.
Unknown
inv-rconc
[@1: Harry is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "young" "-")
Harry is green.
Unknown
random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "+")
Bob is not green.
Unknown
inv-random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "-")
Harry is cold.
Unknown
random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "+")
@0: Bob is blue.[(triple1)] Bob is quiet.[(triple2 OR ((triple3) -> rule7))] Bob is white.[(triple3)] Bob is young.[(triple4 OR ((triple1) -> rule2))] Harry is kind.[(triple6)] Harry is not blue.[(triple5)] Harry is white.[(triple7)] @1: Bob is not kind.[(((triple4) -> rule4) OR ((((triple1) -> rule2)) -> rule4))] Harry is quiet.[(((triple7) -> rule7))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple2
((triple3) -> (rule7 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
triple3
Bob is young.
("Bob" "is" "young" "+")
triple4
((triple1) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
triple6
Harry is not blue.
("Harry" "is" "blue" "-")
triple5
Harry is white.
("Harry" "is" "white" "+")
triple7
Bob is not kind.
("Bob" "is" "kind" "-")
((triple4) -> (rule4 % int1))
Bob is not kind.
("Bob" "is" "kind" "-")
int1
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Bob is not kind.
("Bob" "is" "kind" "-")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple7) -> (rule7 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1