Charlie is green. If Charlie is big then Charlie is smart. All kind, green people are young. If someone is kind then they are big. If someone is rough and green then they are kind. If Charlie is green then Charlie is kind. All young people are smart. If Charlie is kind and Charlie is big then Charlie is green. All quiet people are rough.
Charlie is green.
("Charlie" "is" "green" "+")
If Charlie is big then Charlie is smart.
((("Charlie" "is" "big" "+")) -> ("Charlie" "is" "smart" "+"))
All kind, green people are young.
((("someone" "is" "kind" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "young" "+"))
If someone is kind then they are big.
((("someone" "is" "kind" "+")) -> ("someone" "is" "big" "+"))
If someone is rough and green then they are kind.
((("someone" "is" "rough" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "kind" "+"))
If Charlie is green then Charlie is kind.
((("Charlie" "is" "green" "+")) -> ("Charlie" "is" "kind" "+"))
All young people are smart.
((("someone" "is" "young" "+")) -> ("someone" "is" "smart" "+"))
If Charlie is kind and Charlie is big then Charlie is green.
((("Charlie" "is" "kind" "+") ("Charlie" "is" "big" "+")) -> ("Charlie" "is" "green" "+"))
All quiet people are rough.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "rough" "+"))
Charlie is green.
True
1
proof
[(triple1)]
("Charlie" "is" "green" "+")
triple1
Charlie is not green.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "green" "-")
triple1
Charlie is kind.
True
2
proof
[(((triple1) -> rule5))]
("Charlie" "is" "kind" "+")
((triple1) -> (rule5 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is not kind.
False
2
inv-proof
[(((triple1) -> rule5))]
("Charlie" "is" "kind" "-")
((triple1) -> (rule5 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is big.
True
3
proof
[(((((triple1) -> rule5)) -> rule3))]
("Charlie" "is" "big" "+")
((((triple1) -> (rule5 % int2))) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is not young.
False
4
inv-proof
[(((((triple1) -> rule5) triple1) -> rule2))]
("Charlie" "is" "young" "-")
((((triple1) -> (rule5 % int2)) triple1) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is not rough.
Unknown
inv-rconc
[@1: Charlie is rough.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Charlie" "is" "rough" "-")
Charlie is quiet.
Unknown
random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "+")
@0: Charlie is green.[(triple1)] @1: Charlie is kind.[(((triple1) -> rule5))] @2: Charlie is big.[(((((triple1) -> rule5)) -> rule3))] Charlie is young.[(((((triple1) -> rule5) triple1) -> rule2))] @3: Charlie is smart.[(((((((triple1) -> rule5)) -> rule3)) -> rule1) OR ((((((triple1) -> rule5) triple1) -> rule2)) -> rule6))]
Charlie is green.
("Charlie" "is" "green" "+")
triple1
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple1) -> (rule5 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
((((triple1) -> (rule5 % int2))) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
((((triple1) -> (rule5 % int2)) triple1) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
((((((triple1) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
((((((triple1) -> (rule5 % int3)) triple1) -> (rule2 % int2))) -> (rule6 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3