Charlie is rough. Green, round people are cold. Smart people are round. If someone is rough then they are round. Round people are kind. Round, green people are kind. All round, kind people are smart.
Charlie is rough.
("Charlie" "is" "rough" "+")
Green, round people are cold.
((("someone" "is" "green" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "cold" "+"))
Smart people are round.
((("someone" "is" "smart" "+")) -> ("someone" "is" "round" "+"))
If someone is rough then they are round.
((("someone" "is" "rough" "+")) -> ("someone" "is" "round" "+"))
Round people are kind.
((("someone" "is" "round" "+")) -> ("someone" "is" "kind" "+"))
Round, green people are kind.
((("someone" "is" "round" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "kind" "+"))
All round, kind people are smart.
((("someone" "is" "round" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "smart" "+"))
Charlie is rough.
True
1
proof
[(triple1)]
("Charlie" "is" "rough" "+")
triple1
Charlie is not rough.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "rough" "-")
triple1
Charlie is round.
True
2
proof
[(((triple1) -> rule3))]
("Charlie" "is" "round" "+")
((triple1) -> (rule3 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is not round.
False
2
inv-proof
[(((triple1) -> rule3))]
("Charlie" "is" "round" "-")
((triple1) -> (rule3 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is kind.
True
3
proof
[(((((triple1) -> rule3)) -> rule4))]
("Charlie" "is" "kind" "+")
((((triple1) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is not kind.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule4))]
("Charlie" "is" "kind" "-")
((((triple1) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is smart.
True
6
proof
[(((((triple1) -> rule3) ((((triple1) -> rule3)) -> rule4)) -> rule6))]
("Charlie" "is" "smart" "+")
((((triple1) -> (rule3 % int3)) ((((triple1) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is not smart.
False
6
inv-proof
[(((((triple1) -> rule3) ((((triple1) -> rule3)) -> rule4)) -> rule6))]
("Charlie" "is" "smart" "-")
((((triple1) -> (rule3 % int3)) ((((triple1) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is not cold.
Unknown
inv-rconc
[@1: Charlie is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "cold" "-")
Charlie is white.
Unknown
random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "+")
@0: Charlie is rough.[(triple1)] @1: Charlie is round.[(((triple1) -> rule3))] @2: Charlie is kind.[(((((triple1) -> rule3)) -> rule4))] @3: Charlie is smart.[(((((triple1) -> rule3) ((((triple1) -> rule3)) -> rule4)) -> rule6))]
Charlie is rough.
("Charlie" "is" "rough" "+")
triple1
Charlie is round.
("Charlie" "is" "round" "+")
((triple1) -> (rule3 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
((((triple1) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
((((triple1) -> (rule3 % int3)) ((((triple1) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3