Anne is nice. Charlie is white. Gary is not round. Harry is nice. If Harry is not green then Harry is white. If someone is nice and round then they are smart. White, kind people are not smart. Round people are smart. If someone is smart then they are not kind. All round people are not white. If someone is rough and green then they are white. All nice people are round.
Anne is nice.
("Anne" "is" "nice" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Gary is not round.
("Gary" "is" "round" "-")
Harry is nice.
("Harry" "is" "nice" "+")
If Harry is not green then Harry is white.
((("Harry" "is" "green" "~")) -> ("Harry" "is" "white" "+"))
If someone is nice and round then they are smart.
((("someone" "is" "nice" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "smart" "+"))
White, kind people are not smart.
((("someone" "is" "white" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "smart" "-"))
Round people are smart.
((("someone" "is" "round" "+")) -> ("someone" "is" "smart" "+"))
If someone is smart then they are not kind.
((("someone" "is" "smart" "+")) -> ("someone" "is" "kind" "-"))
All round people are not white.
((("someone" "is" "round" "+")) -> ("someone" "is" "white" "-"))
If someone is rough and green then they are white.
((("someone" "is" "rough" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "white" "+"))
All nice people are round.
((("someone" "is" "nice" "+")) -> ("someone" "is" "round" "+"))
Charlie is white.
True
1
proof
[(triple2)]
("Charlie" "is" "white" "+")
triple2
Gary is round.
False
1
inv-proof
[(triple3)]
("Gary" "is" "round" "+")
triple3
Harry is round.
True
2
proof
[(((triple4) -> rule8))]
("Harry" "is" "round" "+")
((triple4) -> (rule8 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Anne is not round.
False
2
inv-proof
[(((triple1) -> rule8))]
("Anne" "is" "round" "-")
((triple1) -> (rule8 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is smart.
True
3
proof
[(((((triple1) -> rule8)) -> rule4) OR ((triple1 ((triple1) -> rule8)) -> rule2))]
("Anne" "is" "smart" "+")
((((triple1) -> (rule8 % int2))) -> (rule4 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
((triple1 ((triple1) -> (rule8 % int2))) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is not smart.
False
3
inv-proof
[(((((triple1) -> rule8)) -> rule4) OR ((triple1 ((triple1) -> rule8)) -> rule2))]
("Anne" "is" "smart" "-")
((((triple1) -> (rule8 % int2))) -> (rule4 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
((triple1 ((triple1) -> (rule8 % int2))) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is not kind.
True
4
proof
[(((((((triple1) -> rule8)) -> rule4)) -> rule5) OR ((((triple1 ((triple1) -> rule8)) -> rule2)) -> rule5))]
("Anne" "is" "kind" "-")
((((((triple1) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Anne is not kind.
("Anne" "is" "kind" "-")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
((((triple1 ((triple1) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Anne is not kind.
("Anne" "is" "kind" "-")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Harry is kind.
False
4
inv-proof
[(((((((triple4) -> rule8)) -> rule4)) -> rule5) OR ((((triple4 ((triple4) -> rule8)) -> rule2)) -> rule5))]
("Harry" "is" "kind" "+")
((((((triple4) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Harry is not kind.
("Harry" "is" "kind" "-")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
((((triple4 ((triple4) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Harry is not kind.
("Harry" "is" "kind" "-")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Gary is not smart.
Unknown
inv-rconc
[@1: Gary is smart.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "smart" "-")
Charlie is smart.
Unknown
rconc
[@2: Charlie is smart.[CWA. Example of deepest failure = (rule4 <- rule8 <- FAIL)]]
("Charlie" "is" "smart" "+")
Charlie is not round.
Unknown
inv-rconc
[@1: Charlie is round.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Charlie" "is" "round" "-")
Gary is white.
Unknown
rconc
[@1: Gary is white.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Gary" "is" "white" "+")
Gary is not rough.
Unknown
inv-random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "-")
Harry is green.
Unknown
random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "+")
Gary is not kind.
Unknown
inv-random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "-")
Charlie is nice.
Unknown
random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "+")
@0: Anne is nice.[(triple1)] Charlie is white.[(triple2)] Gary is not round.[(triple3)] Harry is nice.[(triple4)] @1: Anne is round.[(((triple1) -> rule8))] Harry is round.[(((triple4) -> rule8))] @2: Anne is not white.[(((((triple1) -> rule8)) -> rule6))] Anne is smart.[(((((triple1) -> rule8)) -> rule4) OR ((triple1 ((triple1) -> rule8)) -> rule2))] Harry is not white.[(((((triple4) -> rule8)) -> rule6))] Harry is smart.[(((((triple4) -> rule8)) -> rule4) OR ((triple4 ((triple4) -> rule8)) -> rule2))] @3: Anne is not kind.[(((((((triple1) -> rule8)) -> rule4)) -> rule5) OR ((((triple1 ((triple1) -> rule8)) -> rule2)) -> rule5))] Harry is not kind.[(((((((triple4) -> rule8)) -> rule4)) -> rule5) OR ((((triple4 ((triple4) -> rule8)) -> rule2)) -> rule5))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Charlie is white.
("Charlie" "is" "white" "+")
triple2
Gary is not round.
("Gary" "is" "round" "-")
triple3
Harry is nice.
("Harry" "is" "nice" "+")
triple4
Anne is round.
("Anne" "is" "round" "+")
((triple1) -> (rule8 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
((triple4) -> (rule8 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Anne is not white.
("Anne" "is" "white" "-")
((((triple1) -> (rule8 % int2))) -> (rule6 % int1))
Anne is not white.
("Anne" "is" "white" "-")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
((((triple1) -> (rule8 % int2))) -> (rule4 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
((triple1 ((triple1) -> (rule8 % int2))) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Harry is not white.
("Harry" "is" "white" "-")
((((triple4) -> (rule8 % int2))) -> (rule6 % int1))
Harry is not white.
("Harry" "is" "white" "-")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
((((triple4) -> (rule8 % int2))) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
((triple4 ((triple4) -> (rule8 % int2))) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Anne is not kind.
("Anne" "is" "kind" "-")
((((((triple1) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Anne is not kind.
("Anne" "is" "kind" "-")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
((((triple1 ((triple1) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Anne is not kind.
("Anne" "is" "kind" "-")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Harry is not kind.
("Harry" "is" "kind" "-")
((((((triple4) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Harry is not kind.
("Harry" "is" "kind" "-")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
((((triple4 ((triple4) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Harry is not kind.
("Harry" "is" "kind" "-")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3