Charlie is cold. Charlie is red. Dave is furry. Dave is not kind. Dave is red. Gary is not furry. Gary is green. Harry is cold. Harry is furry. Harry is red. All furry, red people are not green. All cold people are furry. If someone is cold and not white then they are not kind.
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is not kind.
("Dave" "is" "kind" "-")
Dave is red.
("Dave" "is" "red" "+")
Gary is not furry.
("Gary" "is" "furry" "-")
Gary is green.
("Gary" "is" "green" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is red.
("Harry" "is" "red" "+")
All furry, red people are not green.
((("someone" "is" "furry" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "green" "-"))
All cold people are furry.
((("someone" "is" "cold" "+")) -> ("someone" "is" "furry" "+"))
If someone is cold and not white then they are not kind.
((("someone" "is" "cold" "+") ("someone" "is" "white" "~")) -> ("someone" "is" "kind" "-"))
Harry is furry.
True
1
proof
[(triple9 OR ((triple8) -> rule2))]
("Harry" "is" "furry" "+")
triple9
((triple8) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Gary is not green.
False
1
inv-proof
[(triple7)]
("Gary" "is" "green" "-")
triple7
Charlie is furry.
True
2
proof
[(((triple1) -> rule2))]
("Charlie" "is" "furry" "+")
((triple1) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is not furry.
False
2
inv-proof
[(((triple1) -> rule2))]
("Charlie" "is" "furry" "-")
((triple1) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is not green.
True
4
proof
[(((((triple1) -> rule2) triple2) -> rule1))]
("Charlie" "is" "green" "-")
((((triple1) -> (rule2 % int2)) triple2) -> (rule1 % int1))
Charlie is not green.
("Charlie" "is" "green" "-")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is green.
False
4
inv-proof
[(((((triple1) -> rule2) triple2) -> rule1))]
("Charlie" "is" "green" "+")
((((triple1) -> (rule2 % int2)) triple2) -> (rule1 % int1))
Charlie is not green.
("Charlie" "is" "green" "-")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Gary is not big.
Unknown
inv-random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "-")
Harry is kind.
Unknown
random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "+")
Harry is not white.
Unknown
inv-random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "-")
Charlie is big.
Unknown
random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "+")
Dave is not white.
Unknown
inv-random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "-")
Charlie is kind.
Unknown
random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "+")
@0: Charlie is cold.[(triple1)] Charlie is red.[(triple2)] Dave is furry.[(triple3)] Dave is not kind.[(triple4)] Dave is red.[(triple5)] Gary is green.[(triple7)] Gary is not furry.[(triple6)] Harry is cold.[(triple8)] Harry is furry.[(triple9 OR ((triple8) -> rule2))] Harry is red.[(triple10)] @1: Charlie is furry.[(((triple1) -> rule2))] Dave is not green.[(((triple3 triple5) -> rule1))] Harry is not green.[(((triple9 triple10) -> rule1) OR ((((triple8) -> rule2) triple10) -> rule1))] @2: Charlie is not green.[(((((triple1) -> rule2) triple2) -> rule1))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
Charlie is red.
("Charlie" "is" "red" "+")
triple2
Dave is furry.
("Dave" "is" "furry" "+")
triple3
Dave is not kind.
("Dave" "is" "kind" "-")
triple4
Dave is red.
("Dave" "is" "red" "+")
triple5
Gary is green.
("Gary" "is" "green" "+")
triple7
Gary is not furry.
("Gary" "is" "furry" "-")
triple6
Harry is cold.
("Harry" "is" "cold" "+")
triple8
Harry is furry.
("Harry" "is" "furry" "+")
triple9
((triple8) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
triple10
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple1) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Dave is not green.
("Dave" "is" "green" "-")
((triple3 triple5) -> (rule1 % int1))
Dave is not green.
("Dave" "is" "green" "-")
int1
Harry is not green.
("Harry" "is" "green" "-")
((triple9 triple10) -> (rule1 % int1))
Harry is not green.
("Harry" "is" "green" "-")
int1
((((triple8) -> (rule2 % int2)) triple10) -> (rule1 % int1))
Harry is not green.
("Harry" "is" "green" "-")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Charlie is not green.
("Charlie" "is" "green" "-")
((((triple1) -> (rule2 % int2)) triple2) -> (rule1 % int1))
Charlie is not green.
("Charlie" "is" "green" "-")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2