Anne is cold. Harry is not quiet. If something is green and round then it is cold. Smart things are round. If something is cold then it is round. All quiet, round things are not blue. If something is smart then it is green. If Harry is not round and Harry is not green then Harry is white. All round things are white. If something is smart and not cold then it is white.
Anne is cold.
("Anne" "is" "cold" "+")
Harry is not quiet.
("Harry" "is" "quiet" "-")
If something is green and round then it is cold.
((("something" "is" "green" "+") ("something" "is" "round" "+")) -> ("something" "is" "cold" "+"))
Smart things are round.
((("something" "is" "smart" "+")) -> ("something" "is" "round" "+"))
If something is cold then it is round.
((("something" "is" "cold" "+")) -> ("something" "is" "round" "+"))
All quiet, round things are not blue.
((("something" "is" "quiet" "+") ("something" "is" "round" "+")) -> ("something" "is" "blue" "-"))
If something is smart then it is green.
((("something" "is" "smart" "+")) -> ("something" "is" "green" "+"))
If Harry is not round and Harry is not green then Harry is white.
((("Harry" "is" "round" "~") ("Harry" "is" "green" "~")) -> ("Harry" "is" "white" "+"))
All round things are white.
((("something" "is" "round" "+")) -> ("something" "is" "white" "+"))
If something is smart and not cold then it is white.
((("something" "is" "smart" "+") ("something" "is" "cold" "~")) -> ("something" "is" "white" "+"))
Harry is not quiet.
True
1
proof
[(triple2)]
("Harry" "is" "quiet" "-")
triple2
Anne is not cold.
False
1
inv-proof
[(triple1)]
("Anne" "is" "cold" "-")
triple1
Anne is round.
True
2
proof
[(((triple1) -> rule3))]
("Anne" "is" "round" "+")
((triple1) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is not round.
False
2
inv-proof
[(((triple1) -> rule3))]
("Anne" "is" "round" "-")
((triple1) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is white.
True
3
proof
[(((((triple1) -> rule3)) -> rule7))]
("Anne" "is" "white" "+")
((((triple1) -> (rule3 % int2))) -> (rule7 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is not white.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule7))]
("Anne" "is" "white" "-")
((((triple1) -> (rule3 % int2))) -> (rule7 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Harry is not cold.
Unknown
inv-rconc
[@2: Harry is cold.[CWA. Example of deepest failure = (rule1 <- rule5 <- FAIL)]]
("Harry" "is" "cold" "-")
Anne is green.
Unknown
rconc
[@1: Anne is green.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Anne" "is" "green" "+")
Harry is not green.
Unknown
inv-rconc
[@1: Harry is green.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Harry" "is" "green" "-")
Anne is quiet.
Unknown
random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "+")
Anne is not blue.
Unknown
inv-random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "-")
Harry is blue.
Unknown
random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "+")
@0: Anne is cold.[(triple1)] Harry is not quiet.[(triple2)] @1: Anne is round.[(((triple1) -> rule3))] @2: Anne is white.[(((((triple1) -> rule3)) -> rule7))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Harry is not quiet.
("Harry" "is" "quiet" "-")
triple2
Anne is round.
("Anne" "is" "round" "+")
((triple1) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
((((triple1) -> (rule3 % int2))) -> (rule7 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2