Anne is cold. Anne is furry. Anne is nice. Anne is smart. Charlie is furry. Charlie is kind. Charlie is nice. Charlie is round. Charlie is smart. Dave is blue. Dave is cold. Dave is furry. Dave is kind. Dave is round. Gary is kind. If something is kind then it is furry.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is round.
("Dave" "is" "round" "+")
Gary is kind.
("Gary" "is" "kind" "+")
If something is kind then it is furry.
((("something" "is" "kind" "+")) -> ("something" "is" "furry" "+"))
Charlie is round.
True
1
proof
[(triple8)]
("Charlie" "is" "round" "+")
triple8
Charlie is not round.
False
1
inv-proof
[(triple8)]
("Charlie" "is" "round" "-")
triple8
Gary is furry.
True
2
proof
[(((triple15) -> rule1))]
("Gary" "is" "furry" "+")
((triple15) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is not furry.
False
2
inv-proof
[(((triple15) -> rule1))]
("Gary" "is" "furry" "-")
((triple15) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is not cold.
Unknown
inv-random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "-")
Anne is kind.
Unknown
random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "+")
Anne is not blue.
Unknown
inv-random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "-")
Gary is nice.
Unknown
random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "+")
@0: Anne is cold.[(triple1)] Anne is furry.[(triple2)] Anne is nice.[(triple3)] Anne is smart.[(triple4)] Charlie is furry.[(triple5 OR ((triple6) -> rule1))] Charlie is kind.[(triple6)] Charlie is nice.[(triple7)] Charlie is round.[(triple8)] Charlie is smart.[(triple9)] Dave is blue.[(triple10)] Dave is cold.[(triple11)] Dave is furry.[(triple12 OR ((triple13) -> rule1))] Dave is kind.[(triple13)] Dave is round.[(triple14)] Gary is kind.[(triple15)] @1: Gary is furry.[(((triple15) -> rule1))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is furry.
("Anne" "is" "furry" "+")
triple2
Anne is nice.
("Anne" "is" "nice" "+")
triple3
Anne is smart.
("Anne" "is" "smart" "+")
triple4
Charlie is furry.
("Charlie" "is" "furry" "+")
triple5
((triple6) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple6
Charlie is nice.
("Charlie" "is" "nice" "+")
triple7
Charlie is round.
("Charlie" "is" "round" "+")
triple8
Charlie is smart.
("Charlie" "is" "smart" "+")
triple9
Dave is blue.
("Dave" "is" "blue" "+")
triple10
Dave is cold.
("Dave" "is" "cold" "+")
triple11
Dave is furry.
("Dave" "is" "furry" "+")
triple12
((triple13) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
triple13
Dave is round.
("Dave" "is" "round" "+")
triple14
Gary is kind.
("Gary" "is" "kind" "+")
triple15
Gary is furry.
("Gary" "is" "furry" "+")
((triple15) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1