Anne is kind. Anne is smart. Charlie is blue. Charlie is kind. Charlie is smart. Charlie is white. Charlie is young. Gary is big. Gary is kind. Gary is rough. Gary is young. Harry is big. Harry is kind. Harry is smart. Harry is white. Harry is young. If Harry is big and Harry is kind then Harry is blue. If someone is white then they are big.
Anne is kind.
("Anne" "is" "kind" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is young.
("Gary" "is" "young" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is white.
("Harry" "is" "white" "+")
Harry is young.
("Harry" "is" "young" "+")
If Harry is big and Harry is kind then Harry is blue.
((("Harry" "is" "big" "+") ("Harry" "is" "kind" "+")) -> ("Harry" "is" "blue" "+"))
If someone is white then they are big.
((("someone" "is" "white" "+")) -> ("someone" "is" "big" "+"))
Charlie is blue.
True
1
proof
[(triple3)]
("Charlie" "is" "blue" "+")
triple3
Anne is not smart.
False
1
inv-proof
[(triple2)]
("Anne" "is" "smart" "-")
triple2
Harry is blue.
True
3
proof
[(((triple12 triple13) -> rule1) OR ((((triple15) -> rule2) triple13) -> rule1))]
("Harry" "is" "blue" "+")
((triple12 triple13) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((((triple15) -> (rule2 % int2)) triple13) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is not blue.
False
3
inv-proof
[(((triple12 triple13) -> rule1) OR ((((triple15) -> rule2) triple13) -> rule1))]
("Harry" "is" "blue" "-")
((triple12 triple13) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((((triple15) -> (rule2 % int2)) triple13) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Anne is not big.
Unknown
inv-rconc
[@1: Anne is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "big" "-")
Gary is white.
Unknown
random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "+")
Anne is not blue.
Unknown
inv-random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "-")
Gary is smart.
Unknown
random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "+")
@0: Anne is kind.[(triple1)] Anne is smart.[(triple2)] Charlie is blue.[(triple3)] Charlie is kind.[(triple4)] Charlie is smart.[(triple5)] Charlie is white.[(triple6)] Charlie is young.[(triple7)] Gary is big.[(triple8)] Gary is kind.[(triple9)] Gary is rough.[(triple10)] Gary is young.[(triple11)] Harry is big.[(triple12 OR ((triple15) -> rule2))] Harry is kind.[(triple13)] Harry is smart.[(triple14)] Harry is white.[(triple15)] Harry is young.[(triple16)] @1: Charlie is big.[(((triple6) -> rule2))] Harry is blue.[(((triple12 triple13) -> rule1) OR ((((triple15) -> rule2) triple13) -> rule1))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Anne is smart.
("Anne" "is" "smart" "+")
triple2
Charlie is blue.
("Charlie" "is" "blue" "+")
triple3
Charlie is kind.
("Charlie" "is" "kind" "+")
triple4
Charlie is smart.
("Charlie" "is" "smart" "+")
triple5
Charlie is white.
("Charlie" "is" "white" "+")
triple6
Charlie is young.
("Charlie" "is" "young" "+")
triple7
Gary is big.
("Gary" "is" "big" "+")
triple8
Gary is kind.
("Gary" "is" "kind" "+")
triple9
Gary is rough.
("Gary" "is" "rough" "+")
triple10
Gary is young.
("Gary" "is" "young" "+")
triple11
Harry is big.
("Harry" "is" "big" "+")
triple12
((triple15) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
triple13
Harry is smart.
("Harry" "is" "smart" "+")
triple14
Harry is white.
("Harry" "is" "white" "+")
triple15
Harry is young.
("Harry" "is" "young" "+")
triple16
Charlie is big.
("Charlie" "is" "big" "+")
((triple6) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((triple12 triple13) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((((triple15) -> (rule2 % int2)) triple13) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2