Anne is round. Charlie is rough. Fiona is smart. Kind, smart things are round. If something is furry then it is smart. All rough things are white. All rough, furry things are kind. If Charlie is rough and Charlie is nice then Charlie is furry. If Anne is kind then Anne is not furry. If something is white then it is furry. If Anne is round then Anne is not nice.
Anne is round.
("Anne" "is" "round" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Kind, smart things are round.
((("something" "is" "kind" "+") ("something" "is" "smart" "+")) -> ("something" "is" "round" "+"))
If something is furry then it is smart.
((("something" "is" "furry" "+")) -> ("something" "is" "smart" "+"))
All rough things are white.
((("something" "is" "rough" "+")) -> ("something" "is" "white" "+"))
All rough, furry things are kind.
((("something" "is" "rough" "+") ("something" "is" "furry" "+")) -> ("something" "is" "kind" "+"))
If Charlie is rough and Charlie is nice then Charlie is furry.
((("Charlie" "is" "rough" "+") ("Charlie" "is" "nice" "+")) -> ("Charlie" "is" "furry" "+"))
If Anne is kind then Anne is not furry.
((("Anne" "is" "kind" "+")) -> ("Anne" "is" "furry" "-"))
If something is white then it is furry.
((("something" "is" "white" "+")) -> ("something" "is" "furry" "+"))
If Anne is round then Anne is not nice.
((("Anne" "is" "round" "+")) -> ("Anne" "is" "nice" "-"))
Charlie is rough.
True
1
proof
[(triple2)]
("Charlie" "is" "rough" "+")
triple2
Anne is not round.
False
1
inv-proof
[(triple1)]
("Anne" "is" "round" "-")
triple1
Anne is not nice.
True
2
proof
[(((triple1) -> rule8))]
("Anne" "is" "nice" "-")
((triple1) -> (rule8 % int1))
Anne is not nice.
("Anne" "is" "nice" "-")
int1
Charlie is not white.
False
2
inv-proof
[(((triple2) -> rule3))]
("Charlie" "is" "white" "-")
((triple2) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is furry.
True
3
proof
[(((((triple2) -> rule3)) -> rule7))]
("Charlie" "is" "furry" "+")
((((triple2) -> (rule3 % int2))) -> (rule7 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is not furry.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule7))]
("Charlie" "is" "furry" "-")
((((triple2) -> (rule3 % int2))) -> (rule7 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is smart.
True
4
proof
[(((((((triple2) -> rule3)) -> rule7)) -> rule2))]
("Charlie" "is" "smart" "+")
((((((triple2) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Charlie is not kind.
False
5
inv-proof
[(((triple2 ((((triple2) -> rule3)) -> rule7)) -> rule4))]
("Charlie" "is" "kind" "-")
((triple2 ((((triple2) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Anne is not white.
Unknown
inv-rconc
[@1: Anne is white.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "white" "-")
Fiona is white.
Unknown
rconc
[@1: Fiona is white.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "white" "+")
Fiona is not kind.
Unknown
inv-rconc
[@1: Fiona is kind.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Fiona" "is" "kind" "-")
Anne is furry.
Unknown
rconc
[@2: Anne is furry.[CWA. Example of deepest failure = (rule7 <- rule3 <- FAIL)]]
("Anne" "is" "furry" "+")
Charlie is not nice.
Unknown
inv-random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "-")
Anne is rough.
Unknown
random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "+")
Fiona is not rough.
Unknown
inv-random
[@0: Fiona is rough.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "rough" "-")
Fiona is nice.
Unknown
random
[@0: Fiona is nice.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "nice" "+")
@0: Anne is round.[(triple1)] Charlie is rough.[(triple2)] Fiona is smart.[(triple3)] @1: Anne is not nice.[(((triple1) -> rule8))] Charlie is white.[(((triple2) -> rule3))] @2: Charlie is furry.[(((((triple2) -> rule3)) -> rule7))] @3: Charlie is kind.[(((triple2 ((((triple2) -> rule3)) -> rule7)) -> rule4))] Charlie is smart.[(((((((triple2) -> rule3)) -> rule7)) -> rule2))] @4: Charlie is round.[(((((triple2 ((((triple2) -> rule3)) -> rule7)) -> rule4) ((((((triple2) -> rule3)) -> rule7)) -> rule2)) -> rule1))]
Anne is round.
("Anne" "is" "round" "+")
triple1
Charlie is rough.
("Charlie" "is" "rough" "+")
triple2
Fiona is smart.
("Fiona" "is" "smart" "+")
triple3
Anne is not nice.
("Anne" "is" "nice" "-")
((triple1) -> (rule8 % int1))
Anne is not nice.
("Anne" "is" "nice" "-")
int1
Charlie is white.
("Charlie" "is" "white" "+")
((triple2) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
((((triple2) -> (rule3 % int2))) -> (rule7 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple2 ((((triple2) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Charlie is smart.
("Charlie" "is" "smart" "+")
((((((triple2) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Charlie is round.
("Charlie" "is" "round" "+")
((((triple2 ((((triple2) -> (rule3 % int5))) -> (rule7 % int4))) -> (rule4 % int3)) ((((((triple2) -> (rule3 % int5))) -> (rule7 % int4))) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is furry.
("Charlie" "is" "furry" "+")
int4
Charlie is white.
("Charlie" "is" "white" "+")
int5