Anne is not big. Anne is green. Anne is kind. Anne is quiet. Anne is rough. Bob is blue. Bob is green. Bob is rough. Bob is not white. Gary is blue. Gary is green. Gary is rough. Gary is white. Harry is kind. Harry is quiet. Harry is rough. Green things are kind. If Harry is kind then Harry is white. All quiet things are rough. All big things are rough. All rough, big things are not white. Blue, quiet things are white. All big things are blue. If Harry is green then Harry is big.
Anne is not big.
("Anne" "is" "big" "-")
Anne is green.
("Anne" "is" "green" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is not white.
("Bob" "is" "white" "-")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is white.
("Gary" "is" "white" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Green things are kind.
((("something" "is" "green" "+")) -> ("something" "is" "kind" "+"))
If Harry is kind then Harry is white.
((("Harry" "is" "kind" "+")) -> ("Harry" "is" "white" "+"))
All quiet things are rough.
((("something" "is" "quiet" "+")) -> ("something" "is" "rough" "+"))
All big things are rough.
((("something" "is" "big" "+")) -> ("something" "is" "rough" "+"))
All rough, big things are not white.
((("something" "is" "rough" "+") ("something" "is" "big" "+")) -> ("something" "is" "white" "-"))
Blue, quiet things are white.
((("something" "is" "blue" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "white" "+"))
All big things are blue.
((("something" "is" "big" "+")) -> ("something" "is" "blue" "+"))
If Harry is green then Harry is big.
((("Harry" "is" "green" "+")) -> ("Harry" "is" "big" "+"))
Gary is blue.
True
1
proof
[(triple10)]
("Gary" "is" "blue" "+")
triple10
Anne is not kind.
False
1
inv-proof
[(triple3 OR ((triple2) -> rule1))]
("Anne" "is" "kind" "-")
triple3
((triple2) -> (rule1 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is not blue.
Unknown
inv-rconc
[@1: Anne is blue.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Anne" "is" "blue" "-")
Bob is quiet.
Unknown
random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "+")
@0: Anne is green.[(triple2)] Anne is kind.[(triple3 OR ((triple2) -> rule1))] Anne is not big.[(triple1)] Anne is quiet.[(triple4)] Anne is rough.[(triple5 OR ((triple4) -> rule3))] Bob is blue.[(triple6)] Bob is green.[(triple7)] Bob is not white.[(triple9)] Bob is rough.[(triple8)] Gary is blue.[(triple10)] Gary is green.[(triple11)] Gary is rough.[(triple12)] Gary is white.[(triple13)] Harry is kind.[(triple14)] Harry is quiet.[(triple15)] Harry is rough.[(triple16 OR ((triple15) -> rule3))] @1: Bob is kind.[(((triple7) -> rule1))] Gary is kind.[(((triple11) -> rule1))] Harry is white.[(((triple14) -> rule2))]
Anne is green.
("Anne" "is" "green" "+")
triple2
Anne is kind.
("Anne" "is" "kind" "+")
triple3
((triple2) -> (rule1 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is not big.
("Anne" "is" "big" "-")
triple1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple4
Anne is rough.
("Anne" "is" "rough" "+")
triple5
((triple4) -> (rule3 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
triple6
Bob is green.
("Bob" "is" "green" "+")
triple7
Bob is not white.
("Bob" "is" "white" "-")
triple9
Bob is rough.
("Bob" "is" "rough" "+")
triple8
Gary is blue.
("Gary" "is" "blue" "+")
triple10
Gary is green.
("Gary" "is" "green" "+")
triple11
Gary is rough.
("Gary" "is" "rough" "+")
triple12
Gary is white.
("Gary" "is" "white" "+")
triple13
Harry is kind.
("Harry" "is" "kind" "+")
triple14
Harry is quiet.
("Harry" "is" "quiet" "+")
triple15
Harry is rough.
("Harry" "is" "rough" "+")
triple16
((triple15) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
((triple7) -> (rule1 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
((triple11) -> (rule1 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
((triple14) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1