Anne is smart. Charlie is cold. Charlie is green. Charlie is kind. Charlie is smart. Gary is cold. Gary is furry. Gary is not green. Gary is kind. Gary is not round. Gary is smart. Gary is young. Harry is not cold. Harry is furry. Harry is not young. Kind people are young.
Anne is smart.
("Anne" "is" "smart" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is not green.
("Gary" "is" "green" "-")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is not round.
("Gary" "is" "round" "-")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is young.
("Gary" "is" "young" "+")
Harry is not cold.
("Harry" "is" "cold" "-")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is not young.
("Harry" "is" "young" "-")
Kind people are young.
((("someone" "is" "kind" "+")) -> ("someone" "is" "young" "+"))
Anne is smart.
True
1
proof
[(triple1)]
("Anne" "is" "smart" "+")
triple1
Charlie is not cold.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "cold" "-")
triple2
Charlie is young.
True
2
proof
[(((triple4) -> rule1))]
("Charlie" "is" "young" "+")
((triple4) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is not young.
False
2
inv-proof
[(((triple4) -> rule1))]
("Charlie" "is" "young" "-")
((triple4) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Anne is not young.
Unknown
inv-rconc
[@1: Anne is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "young" "-")
Harry is round.
Unknown
random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "+")
Harry is not smart.
Unknown
inv-random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "-")
Anne is cold.
Unknown
random
[@0: Anne is cold.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "cold" "+")
@0: Anne is smart.[(triple1)] Charlie is cold.[(triple2)] Charlie is green.[(triple3)] Charlie is kind.[(triple4)] Charlie is smart.[(triple5)] Gary is cold.[(triple6)] Gary is furry.[(triple7)] Gary is kind.[(triple9)] Gary is not green.[(triple8)] Gary is not round.[(triple10)] Gary is smart.[(triple11)] Gary is young.[(triple12 OR ((triple9) -> rule1))] Harry is furry.[(triple14)] Harry is not cold.[(triple13)] Harry is not young.[(triple15)] @1: Charlie is young.[(((triple4) -> rule1))]
Anne is smart.
("Anne" "is" "smart" "+")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
Charlie is green.
("Charlie" "is" "green" "+")
triple3
Charlie is kind.
("Charlie" "is" "kind" "+")
triple4
Charlie is smart.
("Charlie" "is" "smart" "+")
triple5
Gary is cold.
("Gary" "is" "cold" "+")
triple6
Gary is furry.
("Gary" "is" "furry" "+")
triple7
Gary is kind.
("Gary" "is" "kind" "+")
triple9
Gary is not green.
("Gary" "is" "green" "-")
triple8
Gary is not round.
("Gary" "is" "round" "-")
triple10
Gary is smart.
("Gary" "is" "smart" "+")
triple11
Gary is young.
("Gary" "is" "young" "+")
triple12
((triple9) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
triple14
Harry is not cold.
("Harry" "is" "cold" "-")
triple13
Harry is not young.
("Harry" "is" "young" "-")
triple15
Charlie is young.
("Charlie" "is" "young" "+")
((triple4) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1