Charlie is blue. If Charlie is smart then Charlie is young. If something is big and not blue then it is quiet. Round things are quiet. If something is young and not blue then it is not nice. All quiet things are smart. Blue things are smart.
Charlie is blue.
("Charlie" "is" "blue" "+")
If Charlie is smart then Charlie is young.
((("Charlie" "is" "smart" "+")) -> ("Charlie" "is" "young" "+"))
If something is big and not blue then it is quiet.
((("something" "is" "big" "+") ("something" "is" "blue" "~")) -> ("something" "is" "quiet" "+"))
Round things are quiet.
((("something" "is" "round" "+")) -> ("something" "is" "quiet" "+"))
If something is young and not blue then it is not nice.
((("something" "is" "young" "+") ("something" "is" "blue" "~")) -> ("something" "is" "nice" "-"))
All quiet things are smart.
((("something" "is" "quiet" "+")) -> ("something" "is" "smart" "+"))
Blue things are smart.
((("something" "is" "blue" "+")) -> ("something" "is" "smart" "+"))
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 smart.
True
2
proof
[(((triple1) -> rule6))]
("Charlie" "is" "smart" "+")
((triple1) -> (rule6 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is not smart.
False
2
inv-proof
[(((triple1) -> rule6))]
("Charlie" "is" "smart" "-")
((triple1) -> (rule6 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is young.
True
3
proof
[(((((triple1) -> rule6)) -> rule1))]
("Charlie" "is" "young" "+")
((((triple1) -> (rule6 % int2))) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is not young.
False
3
inv-proof
[(((((triple1) -> rule6)) -> rule1))]
("Charlie" "is" "young" "-")
((((triple1) -> (rule6 % int2))) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is not quiet.
Unknown
inv-rconc
[@1: Charlie is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "quiet" "-")
Charlie is big.
Unknown
random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "+")
Charlie is not nice.
Unknown
inv-random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "-")
Charlie is round.
Unknown
random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "+")
@0: Charlie is blue.[(triple1)] @1: Charlie is smart.[(((triple1) -> rule6))] @2: Charlie is young.[(((((triple1) -> rule6)) -> rule1))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple1) -> (rule6 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
((((triple1) -> (rule6 % int2))) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2