Anne is blue. Anne is quiet. Anne is white. Charlie is blue. Charlie is cold. Charlie is white. Fiona is blue. Fiona is not cold. Fiona is furry. Fiona is green. Fiona is red. Fiona is white. Harry is blue. Harry is cold. Harry is red. Harry is not white. If something is green and cold then it is blue. Green, cold things are furry. If Fiona is cold then Fiona is red. If Harry is blue then Harry is green. If something is furry and not quiet then it is not green. If something is blue and not red then it is white.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is white.
("Anne" "is" "white" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is not cold.
("Fiona" "is" "cold" "-")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is not white.
("Harry" "is" "white" "-")
If something is green and cold then it is blue.
((("something" "is" "green" "+") ("something" "is" "cold" "+")) -> ("something" "is" "blue" "+"))
Green, cold things are furry.
((("something" "is" "green" "+") ("something" "is" "cold" "+")) -> ("something" "is" "furry" "+"))
If Fiona is cold then Fiona is red.
((("Fiona" "is" "cold" "+")) -> ("Fiona" "is" "red" "+"))
If Harry is blue then Harry is green.
((("Harry" "is" "blue" "+")) -> ("Harry" "is" "green" "+"))
If something is furry and not quiet then it is not green.
((("something" "is" "furry" "+") ("something" "is" "quiet" "~")) -> ("something" "is" "green" "-"))
If something is blue and not red then it is white.
((("something" "is" "blue" "+") ("something" "is" "red" "~")) -> ("something" "is" "white" "+"))
Anne is quiet.
True
1
proof
[(triple2)]
("Anne" "is" "quiet" "+")
triple2
Anne is not white.
False
1
inv-proof
[(triple3)]
("Anne" "is" "white" "-")
triple3
Harry is green.
True
2
proof
[(((triple13) -> rule4))]
("Harry" "is" "green" "+")
((triple13) -> (rule4 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is not green.
False
2
inv-proof
[(((triple13) -> rule4))]
("Harry" "is" "green" "-")
((triple13) -> (rule4 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is furry.
True
4
proof
[(((((triple13) -> rule4) triple14) -> rule2))]
("Harry" "is" "furry" "+")
((((triple13) -> (rule4 % int2)) triple14) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is not furry.
False
4
inv-proof
[(((((triple13) -> rule4) triple14) -> rule2))]
("Harry" "is" "furry" "-")
((((triple13) -> (rule4 % int2)) triple14) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Charlie is not furry.
Unknown
inv-rconc
[@1: Charlie is furry.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "furry" "-")
Anne is furry.
Unknown
rconc
[@1: Anne is furry.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "furry" "+")
Charlie is not green.
Unknown
inv-random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "-")
Fiona is quiet.
Unknown
random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "+")
Anne is not green.
Unknown
inv-random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "-")
Harry is quiet.
Unknown
random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "+")
@0: Anne is blue.[(triple1)] Anne is quiet.[(triple2)] Anne is white.[(triple3)] Charlie is blue.[(triple4)] Charlie is cold.[(triple5)] Charlie is white.[(triple6)] Fiona is blue.[(triple7)] Fiona is furry.[(triple9)] Fiona is green.[(triple10)] Fiona is not cold.[(triple8)] Fiona is red.[(triple11)] Fiona is white.[(triple12)] Harry is blue.[(triple13)] Harry is cold.[(triple14)] Harry is not white.[(triple16)] Harry is red.[(triple15)] @1: Harry is green.[(((triple13) -> rule4))] @2: Harry is furry.[(((((triple13) -> rule4) triple14) -> rule2))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
Anne is white.
("Anne" "is" "white" "+")
triple3
Charlie is blue.
("Charlie" "is" "blue" "+")
triple4
Charlie is cold.
("Charlie" "is" "cold" "+")
triple5
Charlie is white.
("Charlie" "is" "white" "+")
triple6
Fiona is blue.
("Fiona" "is" "blue" "+")
triple7
Fiona is furry.
("Fiona" "is" "furry" "+")
triple9
Fiona is green.
("Fiona" "is" "green" "+")
triple10
Fiona is not cold.
("Fiona" "is" "cold" "-")
triple8
Fiona is red.
("Fiona" "is" "red" "+")
triple11
Fiona is white.
("Fiona" "is" "white" "+")
triple12
Harry is blue.
("Harry" "is" "blue" "+")
triple13
Harry is cold.
("Harry" "is" "cold" "+")
triple14
Harry is not white.
("Harry" "is" "white" "-")
triple16
Harry is red.
("Harry" "is" "red" "+")
triple15
Harry is green.
("Harry" "is" "green" "+")
((triple13) -> (rule4 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
((((triple13) -> (rule4 % int2)) triple14) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2