Charlie is green. Charlie is red. Charlie is not rough. Gary is cold. Gary is green. Gary is white. Gary is young. All rough people are green. All cold people are white. If someone is green then they are cold.
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is not rough.
("Charlie" "is" "rough" "-")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is white.
("Gary" "is" "white" "+")
Gary is young.
("Gary" "is" "young" "+")
All rough people are green.
((("someone" "is" "rough" "+")) -> ("someone" "is" "green" "+"))
All cold people are white.
((("someone" "is" "cold" "+")) -> ("someone" "is" "white" "+"))
If someone is green then they are cold.
((("someone" "is" "green" "+")) -> ("someone" "is" "cold" "+"))
Gary is young.
True
1
proof
[(triple7)]
("Gary" "is" "young" "+")
triple7
Gary is not white.
False
1
inv-proof
[(triple6 OR ((triple4) -> rule2) OR ((((triple5) -> rule3)) -> rule2))]
("Gary" "is" "white" "-")
triple6
((triple4) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
((((triple5) -> (rule3 % int2))) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Charlie is cold.
True
2
proof
[(((triple1) -> rule3))]
("Charlie" "is" "cold" "+")
((triple1) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is not cold.
False
2
inv-proof
[(((triple1) -> rule3))]
("Charlie" "is" "cold" "-")
((triple1) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is white.
True
3
proof
[(((((triple1) -> rule3)) -> rule2))]
("Charlie" "is" "white" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is not white.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule2))]
("Charlie" "is" "white" "-")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is not round.
Unknown
inv-random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "-")
Charlie is young.
Unknown
random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "+")
Gary is not red.
Unknown
inv-random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "-")
Gary is round.
Unknown
random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "+")
@0: Charlie is green.[(triple1)] Charlie is not rough.[(triple3)] Charlie is red.[(triple2)] Gary is cold.[(triple4 OR ((triple5) -> rule3))] Gary is green.[(triple5)] Gary is white.[(triple6 OR ((triple4) -> rule2) OR ((((triple5) -> rule3)) -> rule2))] Gary is young.[(triple7)] @1: Charlie is cold.[(((triple1) -> rule3))] @2: Charlie is white.[(((((triple1) -> rule3)) -> rule2))]
Charlie is green.
("Charlie" "is" "green" "+")
triple1
Charlie is not rough.
("Charlie" "is" "rough" "-")
triple3
Charlie is red.
("Charlie" "is" "red" "+")
triple2
Gary is cold.
("Gary" "is" "cold" "+")
triple4
((triple5) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
triple5
Gary is white.
("Gary" "is" "white" "+")
triple6
((triple4) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
((((triple5) -> (rule3 % int2))) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
triple7
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple1) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2