Anne is round. Fiona is not quiet. Gary is not blue. Harry is round. If something is round and white then it is blue. If something is rough and not furry then it is not cold. If something is round then it is white.
Anne is round.
("Anne" "is" "round" "+")
Fiona is not quiet.
("Fiona" "is" "quiet" "-")
Gary is not blue.
("Gary" "is" "blue" "-")
Harry is round.
("Harry" "is" "round" "+")
If something is round and white then it is blue.
((("something" "is" "round" "+") ("something" "is" "white" "+")) -> ("something" "is" "blue" "+"))
If something is rough and not furry then it is not cold.
((("something" "is" "rough" "+") ("something" "is" "furry" "~")) -> ("something" "is" "cold" "-"))
If something is round then it is white.
((("something" "is" "round" "+")) -> ("something" "is" "white" "+"))
Gary is not blue.
True
1
proof
[(triple3)]
("Gary" "is" "blue" "-")
triple3
Anne is not round.
False
1
inv-proof
[(triple1)]
("Anne" "is" "round" "-")
triple1
Anne is white.
True
2
proof
[(((triple1) -> rule3))]
("Anne" "is" "white" "+")
((triple1) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is not white.
False
2
inv-proof
[(((triple1) -> rule3))]
("Anne" "is" "white" "-")
((triple1) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Harry is blue.
True
4
proof
[(((triple4 ((triple4) -> rule3)) -> rule1))]
("Harry" "is" "blue" "+")
((triple4 ((triple4) -> (rule3 % int2))) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is not blue.
False
4
inv-proof
[(((triple4 ((triple4) -> rule3)) -> rule1))]
("Harry" "is" "blue" "-")
((triple4 ((triple4) -> (rule3 % int2))) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Fiona is not blue.
Unknown
inv-rconc
[@1: Fiona is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "blue" "-")
Fiona is white.
Unknown
rconc
[@1: Fiona is white.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "white" "+")
Gary is not white.
Unknown
inv-rconc
[@1: Gary is white.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "white" "-")
Fiona is round.
Unknown
random
[@0: Fiona is round.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "round" "+")
Gary is not rough.
Unknown
inv-random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "-")
Harry is cold.
Unknown
random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "+")
@0: Anne is round.[(triple1)] Fiona is not quiet.[(triple2)] Gary is not blue.[(triple3)] Harry is round.[(triple4)] @1: Anne is white.[(((triple1) -> rule3))] Harry is white.[(((triple4) -> rule3))] @2: Anne is blue.[(((triple1 ((triple1) -> rule3)) -> rule1))] Harry is blue.[(((triple4 ((triple4) -> rule3)) -> rule1))]
Anne is round.
("Anne" "is" "round" "+")
triple1
Fiona is not quiet.
("Fiona" "is" "quiet" "-")
triple2
Gary is not blue.
("Gary" "is" "blue" "-")
triple3
Harry is round.
("Harry" "is" "round" "+")
triple4
Anne is white.
("Anne" "is" "white" "+")
((triple1) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
((triple4) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
((triple4 ((triple4) -> (rule3 % int2))) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2