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