Anne is cold. Anne is furry. Anne is green. Anne is kind. Anne is smart. Anne is white. Bob is cold. Bob is furry. Bob is round. Bob is smart. Charlie is furry. Charlie is green. Charlie is kind. Charlie is round. Charlie is white. If something is kind and round then it is green. All smart things are furry. If something is cold then it is kind.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is white.
("Anne" "is" "white" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is white.
("Charlie" "is" "white" "+")
If something is kind and round then it is green.
((("something" "is" "kind" "+") ("something" "is" "round" "+")) -> ("something" "is" "green" "+"))
All smart things are furry.
((("something" "is" "smart" "+")) -> ("something" "is" "furry" "+"))
If something is cold then it is kind.
((("something" "is" "cold" "+")) -> ("something" "is" "kind" "+"))
Charlie is kind.
True
1
proof
[(triple13)]
("Charlie" "is" "kind" "+")
triple13
Charlie is not green.
False
1
inv-proof
[(triple12 OR ((triple13 triple14) -> rule1))]
("Charlie" "is" "green" "-")
triple12
((triple13 triple14) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Bob is kind.
True
2
proof
[(((triple7) -> rule3))]
("Bob" "is" "kind" "+")
((triple7) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is not kind.
False
2
inv-proof
[(((triple7) -> rule3))]
("Bob" "is" "kind" "-")
((triple7) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is green.
True
4
proof
[(((((triple7) -> rule3) triple9) -> rule1))]
("Bob" "is" "green" "+")
((((triple7) -> (rule3 % int2)) triple9) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is not green.
False
4
inv-proof
[(((((triple7) -> rule3) triple9) -> rule1))]
("Bob" "is" "green" "-")
((((triple7) -> (rule3 % int2)) triple9) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Charlie is not cold.
Unknown
inv-random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "-")
Charlie is smart.
Unknown
random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "+")
Bob is not white.
Unknown
inv-random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "-")
Anne is round.
Unknown
random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "+")
@0: Anne is cold.[(triple1)] Anne is furry.[(triple2 OR ((triple5) -> rule2))] Anne is green.[(triple3)] Anne is kind.[(triple4 OR ((triple1) -> rule3))] Anne is smart.[(triple5)] Anne is white.[(triple6)] Bob is cold.[(triple7)] Bob is furry.[(triple8 OR ((triple10) -> rule2))] Bob is round.[(triple9)] Bob is smart.[(triple10)] Charlie is furry.[(triple11)] Charlie is green.[(triple12 OR ((triple13 triple14) -> rule1))] Charlie is kind.[(triple13)] Charlie is round.[(triple14)] Charlie is white.[(triple15)] @1: Bob is kind.[(((triple7) -> rule3))] @2: Bob is green.[(((((triple7) -> rule3) triple9) -> rule1))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is furry.
("Anne" "is" "furry" "+")
triple2
((triple5) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
triple3
Anne is kind.
("Anne" "is" "kind" "+")
triple4
((triple1) -> (rule3 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
triple5
Anne is white.
("Anne" "is" "white" "+")
triple6
Bob is cold.
("Bob" "is" "cold" "+")
triple7
Bob is furry.
("Bob" "is" "furry" "+")
triple8
((triple10) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
triple9
Bob is smart.
("Bob" "is" "smart" "+")
triple10
Charlie is furry.
("Charlie" "is" "furry" "+")
triple11
Charlie is green.
("Charlie" "is" "green" "+")
triple12
((triple13 triple14) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple13
Charlie is round.
("Charlie" "is" "round" "+")
triple14
Charlie is white.
("Charlie" "is" "white" "+")
triple15
Bob is kind.
("Bob" "is" "kind" "+")
((triple7) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
((((triple7) -> (rule3 % int2)) triple9) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2