Anne is blue. Charlie is green. Fiona is green. Harry is big. All quiet, green things are blue. All white things are blue. Big things are white.
Anne is blue.
("Anne" "is" "blue" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Harry is big.
("Harry" "is" "big" "+")
All quiet, green things are blue.
((("something" "is" "quiet" "+") ("something" "is" "green" "+")) -> ("something" "is" "blue" "+"))
All white things are blue.
((("something" "is" "white" "+")) -> ("something" "is" "blue" "+"))
Big things are white.
((("something" "is" "big" "+")) -> ("something" "is" "white" "+"))
Charlie is green.
True
1
proof
[(triple2)]
("Charlie" "is" "green" "+")
triple2
Harry is not big.
False
1
inv-proof
[(triple4)]
("Harry" "is" "big" "-")
triple4
Harry is white.
True
2
proof
[(((triple4) -> rule3))]
("Harry" "is" "white" "+")
((triple4) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is not white.
False
2
inv-proof
[(((triple4) -> rule3))]
("Harry" "is" "white" "-")
((triple4) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is blue.
True
3
proof
[(((((triple4) -> rule3)) -> rule2))]
("Harry" "is" "blue" "+")
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is not blue.
False
3
inv-proof
[(((((triple4) -> rule3)) -> rule2))]
("Harry" "is" "blue" "-")
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Fiona is not white.
Unknown
inv-rconc
[@1: Fiona is white.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "white" "-")
Charlie is blue.
Unknown
rconc
[@2: Charlie is blue.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Charlie" "is" "blue" "+")
Charlie is not white.
Unknown
inv-rconc
[@1: Charlie is white.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "white" "-")
Fiona is quiet.
Unknown
random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "+")
Charlie is not red.
Unknown
inv-random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "-")
Charlie is rough.
Unknown
random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "+")
@0: Anne is blue.[(triple1)] Charlie is green.[(triple2)] Fiona is green.[(triple3)] Harry is big.[(triple4)] @1: Harry is white.[(((triple4) -> rule3))] @2: Harry is blue.[(((((triple4) -> rule3)) -> rule2))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Charlie is green.
("Charlie" "is" "green" "+")
triple2
Fiona is green.
("Fiona" "is" "green" "+")
triple3
Harry is big.
("Harry" "is" "big" "+")
triple4
Harry is white.
("Harry" "is" "white" "+")
((triple4) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2