Charlie is white. All smart, cold people are blue. White people are blue. If someone is nice and not big then they are blue. If Charlie is blue and Charlie is white then Charlie is nice. If someone is cold then they are nice. All white, nice people are cold.
Charlie is white.
("Charlie" "is" "white" "+")
All smart, cold people are blue.
((("someone" "is" "smart" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "blue" "+"))
White people are blue.
((("someone" "is" "white" "+")) -> ("someone" "is" "blue" "+"))
If someone is nice and not big then they are blue.
((("someone" "is" "nice" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "blue" "+"))
If Charlie is blue and Charlie is white then Charlie is nice.
((("Charlie" "is" "blue" "+") ("Charlie" "is" "white" "+")) -> ("Charlie" "is" "nice" "+"))
If someone is cold then they are nice.
((("someone" "is" "cold" "+")) -> ("someone" "is" "nice" "+"))
All white, nice people are cold.
((("someone" "is" "white" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "cold" "+"))
Charlie is white.
True
1
proof
[(triple1)]
("Charlie" "is" "white" "+")
triple1
Charlie is not white.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "white" "-")
triple1
Charlie is blue.
True
2
proof
[(((triple1) -> rule2))]
("Charlie" "is" "blue" "+")
((triple1) -> (rule2 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is not blue.
False
2
inv-proof
[(((triple1) -> rule2))]
("Charlie" "is" "blue" "-")
((triple1) -> (rule2 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is nice.
True
4
proof
[(((((triple1) -> rule2) triple1) -> rule4))]
("Charlie" "is" "nice" "+")
((((triple1) -> (rule2 % int2)) triple1) -> (rule4 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is not nice.
False
4
inv-proof
[(((((triple1) -> rule2) triple1) -> rule4))]
("Charlie" "is" "nice" "-")
((((triple1) -> (rule2 % int2)) triple1) -> (rule4 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is cold.
True
6
proof
[(((triple1 ((((triple1) -> rule2) triple1) -> rule4)) -> rule6))]
("Charlie" "is" "cold" "+")
((triple1 ((((triple1) -> (rule2 % int3)) triple1) -> (rule4 % int2))) -> (rule6 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is not cold.
False
6
inv-proof
[(((triple1 ((((triple1) -> rule2) triple1) -> rule4)) -> rule6))]
("Charlie" "is" "cold" "-")
((triple1 ((((triple1) -> (rule2 % int3)) triple1) -> (rule4 % int2))) -> (rule6 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is not red.
Unknown
inv-random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "-")
Charlie is smart.
Unknown
random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "+")
@0: Charlie is white.[(triple1)] @1: Charlie is blue.[(((triple1) -> rule2))] @2: Charlie is nice.[(((((triple1) -> rule2) triple1) -> rule4))] @3: Charlie is cold.[(((triple1 ((((triple1) -> rule2) triple1) -> rule4)) -> rule6))]
Charlie is white.
("Charlie" "is" "white" "+")
triple1
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple1) -> (rule2 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
((((triple1) -> (rule2 % int2)) triple1) -> (rule4 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple1 ((((triple1) -> (rule2 % int3)) triple1) -> (rule4 % int2))) -> (rule6 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3