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