Charlie is blue. If Charlie is big then Charlie is nice. If Charlie is blue then Charlie is rough. If something is rough then it is big. Cold things are nice. If something is blue and not nice then it is not red. All red, rough things are not young.
Charlie is blue.
("Charlie" "is" "blue" "+")
If Charlie is big then Charlie is nice.
((("Charlie" "is" "big" "+")) -> ("Charlie" "is" "nice" "+"))
If Charlie is blue then Charlie is rough.
((("Charlie" "is" "blue" "+")) -> ("Charlie" "is" "rough" "+"))
If something is rough then it is big.
((("something" "is" "rough" "+")) -> ("something" "is" "big" "+"))
Cold things are nice.
((("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
If something is blue and not nice then it is not red.
((("something" "is" "blue" "+") ("something" "is" "nice" "~")) -> ("something" "is" "red" "-"))
All red, rough things are not young.
((("something" "is" "red" "+") ("something" "is" "rough" "+")) -> ("something" "is" "young" "-"))
Charlie is blue.
True
1
proof
[(triple1)]
("Charlie" "is" "blue" "+")
triple1
Charlie is not blue.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "blue" "-")
triple1
Charlie is rough.
True
2
proof
[(((triple1) -> rule2))]
("Charlie" "is" "rough" "+")
((triple1) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is not rough.
False
2
inv-proof
[(((triple1) -> rule2))]
("Charlie" "is" "rough" "-")
((triple1) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is big.
True
3
proof
[(((((triple1) -> rule2)) -> rule3))]
("Charlie" "is" "big" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is not big.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule3))]
("Charlie" "is" "big" "-")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is nice.
True
4
proof
[(((((((triple1) -> rule2)) -> rule3)) -> rule1))]
("Charlie" "is" "nice" "+")
((((((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is not nice.
False
4
inv-proof
[(((((((triple1) -> rule2)) -> rule3)) -> rule1))]
("Charlie" "is" "nice" "-")
((((((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is not young.
Unknown
inv-random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "-")
Charlie is red.
Unknown
random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "+")
@0: Charlie is blue.[(triple1)] @1: Charlie is rough.[(((triple1) -> rule2))] @2: Charlie is big.[(((((triple1) -> rule2)) -> rule3))] @3: Charlie is nice.[(((((((triple1) -> rule2)) -> rule3)) -> rule1))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple1) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
((((((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3