Charlie is quiet. Erin is round. If something is quiet then it is green. If something is green and rough then it is quiet. Kind things are white. If Erin is quiet and Erin is green then Erin is not kind. If Erin is kind and Erin is smart then Erin is white. All green things are not smart. If something is green and not smart then it is round. All rough, smart things are round.
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Erin is round.
("Erin" "is" "round" "+")
If something is quiet then it is green.
((("something" "is" "quiet" "+")) -> ("something" "is" "green" "+"))
If something is green and rough then it is quiet.
((("something" "is" "green" "+") ("something" "is" "rough" "+")) -> ("something" "is" "quiet" "+"))
Kind things are white.
((("something" "is" "kind" "+")) -> ("something" "is" "white" "+"))
If Erin is quiet and Erin is green then Erin is not kind.
((("Erin" "is" "quiet" "+") ("Erin" "is" "green" "+")) -> ("Erin" "is" "kind" "-"))
If Erin is kind and Erin is smart then Erin is white.
((("Erin" "is" "kind" "+") ("Erin" "is" "smart" "+")) -> ("Erin" "is" "white" "+"))
All green things are not smart.
((("something" "is" "green" "+")) -> ("something" "is" "smart" "-"))
If something is green and not smart then it is round.
((("something" "is" "green" "+") ("something" "is" "smart" "~")) -> ("something" "is" "round" "+"))
All rough, smart things are round.
((("something" "is" "rough" "+") ("something" "is" "smart" "+")) -> ("something" "is" "round" "+"))
Charlie is quiet.
True
1
proof
[(triple1)]
("Charlie" "is" "quiet" "+")
triple1
Charlie is not quiet.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "quiet" "-")
triple1
Charlie is green.
True
2
proof
[(((triple1) -> rule1))]
("Charlie" "is" "green" "+")
((triple1) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is not green.
False
2
inv-proof
[(((triple1) -> rule1))]
("Charlie" "is" "green" "-")
((triple1) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is not smart.
True
3
proof
[(((((triple1) -> rule1)) -> rule6))]
("Charlie" "is" "smart" "-")
((((triple1) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is not smart.
("Charlie" "is" "smart" "-")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is smart.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule6))]
("Charlie" "is" "smart" "+")
((((triple1) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is not smart.
("Charlie" "is" "smart" "-")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is round.
True
6
proof
[(((((triple1) -> rule1) ((((triple1) -> rule1)) -> rule6)) -> rule7))]
("Charlie" "is" "round" "+")
((((triple1) -> (rule1 % int3)) ((((triple1) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is not smart.
("Charlie" "is" "smart" "-")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Charlie is not round.
False
6
inv-proof
[(((((triple1) -> rule1) ((((triple1) -> rule1)) -> rule6)) -> rule7))]
("Charlie" "is" "round" "-")
((((triple1) -> (rule1 % int3)) ((((triple1) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is not smart.
("Charlie" "is" "smart" "-")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Erin is not white.
Unknown
inv-rconc
[@1: Erin is white.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "white" "-")
Charlie is white.
Unknown
rconc
[@1: Charlie is white.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "white" "+")
Erin is not quiet.
Unknown
inv-rconc
[@1: Erin is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "quiet" "-")
Erin is green.
Unknown
rconc
[@2: Erin is green.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Erin" "is" "green" "+")
Erin is not rough.
Unknown
inv-random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "-")
Charlie is kind.
Unknown
random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "+")
Erin is not kind.
Unknown
inv-random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "-")
Charlie is rough.
Unknown
random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "+")
@0: Charlie is quiet.[(triple1)] Erin is round.[(triple2)] @1: Charlie is green.[(((triple1) -> rule1))] @2: Charlie is not smart.[(((((triple1) -> rule1)) -> rule6))] @3: Charlie is round.[(((((triple1) -> rule1) ((((triple1) -> rule1)) -> rule6)) -> rule7))]
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple1
Erin is round.
("Erin" "is" "round" "+")
triple2
Charlie is green.
("Charlie" "is" "green" "+")
((triple1) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is not smart.
("Charlie" "is" "smart" "-")
((((triple1) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is not smart.
("Charlie" "is" "smart" "-")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
((((triple1) -> (rule1 % int3)) ((((triple1) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is not smart.
("Charlie" "is" "smart" "-")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3