Anne is furry. Charlie is round. Gary is round. Harry is not furry. Furry people are cold. Furry, quiet people are cold. All blue, round people are not cold. All round people are quiet. All cold people are not round. If someone is furry and not round then they are not white.
Anne is furry.
("Anne" "is" "furry" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Gary is round.
("Gary" "is" "round" "+")
Harry is not furry.
("Harry" "is" "furry" "-")
Furry people are cold.
((("someone" "is" "furry" "+")) -> ("someone" "is" "cold" "+"))
Furry, quiet people are cold.
((("someone" "is" "furry" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "cold" "+"))
All blue, round people are not cold.
((("someone" "is" "blue" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "cold" "-"))
All round people are quiet.
((("someone" "is" "round" "+")) -> ("someone" "is" "quiet" "+"))
All cold people are not round.
((("someone" "is" "cold" "+")) -> ("someone" "is" "round" "-"))
If someone is furry and not round then they are not white.
((("someone" "is" "furry" "+") ("someone" "is" "round" "~")) -> ("someone" "is" "white" "-"))
Harry is not furry.
True
1
proof
[(triple4)]
("Harry" "is" "furry" "-")
triple4
Harry is furry.
False
1
inv-proof
[(triple4)]
("Harry" "is" "furry" "+")
triple4
Anne is cold.
True
2
proof
[(((triple1) -> rule1))]
("Anne" "is" "cold" "+")
((triple1) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Gary is not quiet.
False
2
inv-proof
[(((triple3) -> rule4))]
("Gary" "is" "quiet" "-")
((triple3) -> (rule4 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Anne is not round.
True
3
proof
[(((((triple1) -> rule1)) -> rule5))]
("Anne" "is" "round" "-")
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Anne is not round.
("Anne" "is" "round" "-")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is round.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule5))]
("Anne" "is" "round" "+")
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Anne is not round.
("Anne" "is" "round" "-")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is not white.
True
5
proof
[(((triple1 ((((triple1) -> rule1)) -> rule5)) -> rule6))]
("Anne" "is" "white" "-")
((triple1 ((((triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Anne is not white.
("Anne" "is" "white" "-")
int1
Anne is not round.
("Anne" "is" "round" "-")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is white.
False
5
inv-proof
[(((triple1 ((((triple1) -> rule1)) -> rule5)) -> rule6))]
("Anne" "is" "white" "+")
((triple1 ((((triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Anne is not white.
("Anne" "is" "white" "-")
int1
Anne is not round.
("Anne" "is" "round" "-")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Charlie is not cold.
Unknown
inv-rconc
[@1: Charlie is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "cold" "-")
Gary is cold.
Unknown
rconc
[@1: Gary is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "cold" "+")
Harry is not quiet.
Unknown
inv-rconc
[@1: Harry is quiet.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Harry" "is" "quiet" "-")
Harry is cold.
Unknown
rconc
[@1: Harry is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "cold" "+")
Gary is not white.
Unknown
inv-random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "-")
Anne is blue.
Unknown
random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "+")
Gary is not blue.
Unknown
inv-random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "-")
Anne is smart.
Unknown
random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "+")
@0: Anne is furry.[(triple1)] Charlie is round.[(triple2)] Gary is round.[(triple3)] Harry is not furry.[(triple4)] @1: Anne is cold.[(((triple1) -> rule1))] Charlie is quiet.[(((triple2) -> rule4))] Gary is quiet.[(((triple3) -> rule4))] @2: Anne is not round.[(((((triple1) -> rule1)) -> rule5))] @3: Anne is not white.[(((triple1 ((((triple1) -> rule1)) -> rule5)) -> rule6))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Charlie is round.
("Charlie" "is" "round" "+")
triple2
Gary is round.
("Gary" "is" "round" "+")
triple3
Harry is not furry.
("Harry" "is" "furry" "-")
triple4
Anne is cold.
("Anne" "is" "cold" "+")
((triple1) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple2) -> (rule4 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple3) -> (rule4 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Anne is not round.
("Anne" "is" "round" "-")
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Anne is not round.
("Anne" "is" "round" "-")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is not white.
("Anne" "is" "white" "-")
((triple1 ((((triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Anne is not white.
("Anne" "is" "white" "-")
int1
Anne is not round.
("Anne" "is" "round" "-")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3