Anne is not blue. Anne is not cold. Anne is kind. Anne is red. Anne is round. Anne is not smart. Anne is not young. Dave is blue. Harry is round. Harry is young. If something is red and young then it is cold. If something is blue then it is not cold. Smart things are young. All young, kind things are round. Blue things are round. If something is smart and cold then it is kind. If Harry is smart then Harry is not round. Round, cold things are red.
Anne is not blue.
("Anne" "is" "blue" "-")
Anne is not cold.
("Anne" "is" "cold" "-")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is not smart.
("Anne" "is" "smart" "-")
Anne is not young.
("Anne" "is" "young" "-")
Dave is blue.
("Dave" "is" "blue" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is young.
("Harry" "is" "young" "+")
If something is red and young then it is cold.
((("something" "is" "red" "+") ("something" "is" "young" "+")) -> ("something" "is" "cold" "+"))
If something is blue then it is not cold.
((("something" "is" "blue" "+")) -> ("something" "is" "cold" "-"))
Smart things are young.
((("something" "is" "smart" "+")) -> ("something" "is" "young" "+"))
All young, kind things are round.
((("something" "is" "young" "+") ("something" "is" "kind" "+")) -> ("something" "is" "round" "+"))
Blue things are round.
((("something" "is" "blue" "+")) -> ("something" "is" "round" "+"))
If something is smart and cold then it is kind.
((("something" "is" "smart" "+") ("something" "is" "cold" "+")) -> ("something" "is" "kind" "+"))
If Harry is smart then Harry is not round.
((("Harry" "is" "smart" "+")) -> ("Harry" "is" "round" "-"))
Round, cold things are red.
((("something" "is" "round" "+") ("something" "is" "cold" "+")) -> ("something" "is" "red" "+"))
Anne is not smart.
True
1
proof
[(triple6)]
("Anne" "is" "smart" "-")
triple6
Anne is blue.
False
1
inv-proof
[(triple1)]
("Anne" "is" "blue" "+")
triple1
Dave is round.
True
2
proof
[(((triple8) -> rule5))]
("Dave" "is" "round" "+")
((triple8) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is not round.
False
2
inv-proof
[(((triple8) -> rule5))]
("Dave" "is" "round" "-")
((triple8) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Harry is not red.
Unknown
inv-rconc
[@2: Harry is red.[CWA. Example of deepest failure = (rule8 <- rule1 <- FAIL)]]
("Harry" "is" "red" "-")
Harry is kind.
Unknown
rconc
[@1: Harry is kind.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "kind" "+")
Harry is not blue.
Unknown
inv-random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "-")
Harry is smart.
Unknown
random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "+")
@0: Anne is kind.[(triple3)] Anne is not blue.[(triple1)] Anne is not cold.[(triple2)] Anne is not smart.[(triple6)] Anne is not young.[(triple7)] Anne is red.[(triple4)] Anne is round.[(triple5)] Dave is blue.[(triple8)] Harry is round.[(triple9)] Harry is young.[(triple10)] @1: Dave is not cold.[(((triple8) -> rule2))] Dave is round.[(((triple8) -> rule5))]
Anne is kind.
("Anne" "is" "kind" "+")
triple3
Anne is not blue.
("Anne" "is" "blue" "-")
triple1
Anne is not cold.
("Anne" "is" "cold" "-")
triple2
Anne is not smart.
("Anne" "is" "smart" "-")
triple6
Anne is not young.
("Anne" "is" "young" "-")
triple7
Anne is red.
("Anne" "is" "red" "+")
triple4
Anne is round.
("Anne" "is" "round" "+")
triple5
Dave is blue.
("Dave" "is" "blue" "+")
triple8
Harry is round.
("Harry" "is" "round" "+")
triple9
Harry is young.
("Harry" "is" "young" "+")
triple10
Dave is not cold.
("Dave" "is" "cold" "-")
((triple8) -> (rule2 % int1))
Dave is not cold.
("Dave" "is" "cold" "-")
int1
Dave is round.
("Dave" "is" "round" "+")
((triple8) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1