Charlie is blue. Charlie is cold. Charlie is furry. Charlie is not nice. Gary is blue. Gary is not rough. Gary is not white. If Charlie is cold then Charlie is white. If something is cold and white then it is not smart. If something is cold and not smart then it is rough.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is not nice.
("Charlie" "is" "nice" "-")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is not rough.
("Gary" "is" "rough" "-")
Gary is not white.
("Gary" "is" "white" "-")
If Charlie is cold then Charlie is white.
((("Charlie" "is" "cold" "+")) -> ("Charlie" "is" "white" "+"))
If something is cold and white then it is not smart.
((("something" "is" "cold" "+") ("something" "is" "white" "+")) -> ("something" "is" "smart" "-"))
If something is cold and not smart then it is rough.
((("something" "is" "cold" "+") ("something" "is" "smart" "~")) -> ("something" "is" "rough" "+"))
Gary is not white.
True
1
proof
[(triple7)]
("Gary" "is" "white" "-")
triple7
Charlie is not furry.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "furry" "-")
triple3
Charlie is white.
True
2
proof
[(((triple2) -> rule1))]
("Charlie" "is" "white" "+")
((triple2) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is not white.
False
2
inv-proof
[(((triple2) -> rule1))]
("Charlie" "is" "white" "-")
((triple2) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is not smart.
True
4
proof
[(((triple2 ((triple2) -> rule1)) -> rule2))]
("Charlie" "is" "smart" "-")
((triple2 ((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is not smart.
("Charlie" "is" "smart" "-")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is smart.
False
4
inv-proof
[(((triple2 ((triple2) -> rule1)) -> rule2))]
("Charlie" "is" "smart" "+")
((triple2 ((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is not smart.
("Charlie" "is" "smart" "-")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is rough.
True
6
proof
[(((triple2 ((triple2 ((triple2) -> rule1)) -> rule2)) -> rule3))]
("Charlie" "is" "rough" "+")
((triple2 ((triple2 ((triple2) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is not smart.
("Charlie" "is" "smart" "-")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Charlie is not rough.
False
6
inv-proof
[(((triple2 ((triple2 ((triple2) -> rule1)) -> rule2)) -> rule3))]
("Charlie" "is" "rough" "-")
((triple2 ((triple2 ((triple2) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is not smart.
("Charlie" "is" "smart" "-")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Gary is not smart.
Unknown
inv-random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "-")
Gary is cold.
Unknown
random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "+")
Gary is not nice.
Unknown
inv-random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "-")
Gary is furry.
Unknown
random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "+")
@0: Charlie is blue.[(triple1)] Charlie is cold.[(triple2)] Charlie is furry.[(triple3)] Charlie is not nice.[(triple4)] Gary is blue.[(triple5)] Gary is not rough.[(triple6)] Gary is not white.[(triple7)] @1: Charlie is white.[(((triple2) -> rule1))] @2: Charlie is not smart.[(((triple2 ((triple2) -> rule1)) -> rule2))] @3: Charlie is rough.[(((triple2 ((triple2 ((triple2) -> rule1)) -> rule2)) -> rule3))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
Charlie is furry.
("Charlie" "is" "furry" "+")
triple3
Charlie is not nice.
("Charlie" "is" "nice" "-")
triple4
Gary is blue.
("Gary" "is" "blue" "+")
triple5
Gary is not rough.
("Gary" "is" "rough" "-")
triple6
Gary is not white.
("Gary" "is" "white" "-")
triple7
Charlie is white.
("Charlie" "is" "white" "+")
((triple2) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is not smart.
("Charlie" "is" "smart" "-")
((triple2 ((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is not smart.
("Charlie" "is" "smart" "-")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple2 ((triple2 ((triple2) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is not smart.
("Charlie" "is" "smart" "-")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3