Anne is cold. Charlie is not furry. Fiona is furry. Gary is furry. If something is nice and not round then it is not quiet. All white things are not quiet. If Gary is furry then Gary is cold. Cold, furry things are white. If something is white and cold then it is furry. If something is white and not quiet then it is young.
Anne is cold.
("Anne" "is" "cold" "+")
Charlie is not furry.
("Charlie" "is" "furry" "-")
Fiona is furry.
("Fiona" "is" "furry" "+")
Gary is furry.
("Gary" "is" "furry" "+")
If something is nice and not round then it is not quiet.
((("something" "is" "nice" "+") ("something" "is" "round" "~")) -> ("something" "is" "quiet" "-"))
All white things are not quiet.
((("something" "is" "white" "+")) -> ("something" "is" "quiet" "-"))
If Gary is furry then Gary is cold.
((("Gary" "is" "furry" "+")) -> ("Gary" "is" "cold" "+"))
Cold, furry things are white.
((("something" "is" "cold" "+") ("something" "is" "furry" "+")) -> ("something" "is" "white" "+"))
If something is white and cold then it is furry.
((("something" "is" "white" "+") ("something" "is" "cold" "+")) -> ("something" "is" "furry" "+"))
If something is white and not quiet then it is young.
((("something" "is" "white" "+") ("something" "is" "quiet" "~")) -> ("something" "is" "young" "+"))
Charlie is not furry.
True
1
proof
[(triple2)]
("Charlie" "is" "furry" "-")
triple2
Fiona is not furry.
False
1
inv-proof
[(triple3)]
("Fiona" "is" "furry" "-")
triple3
Gary is cold.
True
2
proof
[(((triple4) -> rule3))]
("Gary" "is" "cold" "+")
((triple4) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is not cold.
False
2
inv-proof
[(((triple4) -> rule3))]
("Gary" "is" "cold" "-")
((triple4) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is white.
True
4
proof
[(((((triple4) -> rule3) triple4) -> rule4))]
("Gary" "is" "white" "+")
((((triple4) -> (rule3 % int2)) triple4) -> (rule4 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is not white.
False
4
inv-proof
[(((((triple4) -> rule3) triple4) -> rule4))]
("Gary" "is" "white" "-")
((((triple4) -> (rule3 % int2)) triple4) -> (rule4 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is not quiet.
True
5
proof
[(((((((triple4) -> rule3) triple4) -> rule4)) -> rule2))]
("Gary" "is" "quiet" "-")
((((((triple4) -> (rule3 % int3)) triple4) -> (rule4 % int2))) -> (rule2 % int1))
Gary is not quiet.
("Gary" "is" "quiet" "-")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is quiet.
False
5
inv-proof
[(((((((triple4) -> rule3) triple4) -> rule4)) -> rule2))]
("Gary" "is" "quiet" "+")
((((((triple4) -> (rule3 % int3)) triple4) -> (rule4 % int2))) -> (rule2 % int1))
Gary is not quiet.
("Gary" "is" "quiet" "-")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Anne is not furry.
Unknown
inv-rconc
[@2: Anne is furry.[CWA. Example of deepest failure = (rule5 <- rule4 <- FAIL)]]
("Anne" "is" "furry" "-")
Anne is white.
Unknown
rconc
[@2: Anne is white.[CWA. Example of deepest failure = (rule4 <- rule5 <- FAIL)]]
("Anne" "is" "white" "+")
Fiona is not young.
Unknown
inv-rconc
[@1: Fiona is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Fiona" "is" "young" "-")
Anne is young.
Unknown
rconc
[@1: Anne is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Anne" "is" "young" "+")
Fiona is not round.
Unknown
inv-random
[@0: Fiona is round.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "round" "-")
Fiona is quiet.
Unknown
random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "+")
Gary is not round.
Unknown
inv-random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "-")
Charlie is cold.
Unknown
random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "+")
@0: Anne is cold.[(triple1)] Charlie is not furry.[(triple2)] Fiona is furry.[(triple3)] Gary is furry.[(triple4)] @1: Gary is cold.[(((triple4) -> rule3))] @2: Gary is white.[(((((triple4) -> rule3) triple4) -> rule4))] @3: Gary is not quiet.[(((((((triple4) -> rule3) triple4) -> rule4)) -> rule2))] @4: Gary is young.[(((((((triple4) -> rule3) triple4) -> rule4) ((((((triple4) -> rule3) triple4) -> rule4)) -> rule2)) -> rule6))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Charlie is not furry.
("Charlie" "is" "furry" "-")
triple2
Fiona is furry.
("Fiona" "is" "furry" "+")
triple3
Gary is furry.
("Gary" "is" "furry" "+")
triple4
Gary is cold.
("Gary" "is" "cold" "+")
((triple4) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
((((triple4) -> (rule3 % int2)) triple4) -> (rule4 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is not quiet.
("Gary" "is" "quiet" "-")
((((((triple4) -> (rule3 % int3)) triple4) -> (rule4 % int2))) -> (rule2 % int1))
Gary is not quiet.
("Gary" "is" "quiet" "-")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is young.
("Gary" "is" "young" "+")
((((((triple4) -> (rule3 % int4)) triple4) -> (rule4 % int3)) ((((((triple4) -> (rule3 % int4)) triple4) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is not quiet.
("Gary" "is" "quiet" "-")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is cold.
("Gary" "is" "cold" "+")
int4