Anne is blue. Fiona is red. Gary is red. Harry is rough. If something is cold and red then it is white. Blue things are white. If something is white and young then it is blue. Rough things are young. If something is red and kind then it is cold. Young, white things are kind. If something is young and rough then it is kind. All rough, blue things are white.
Anne is blue.
("Anne" "is" "blue" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Gary is red.
("Gary" "is" "red" "+")
Harry is rough.
("Harry" "is" "rough" "+")
If something is cold and red then it is white.
((("something" "is" "cold" "+") ("something" "is" "red" "+")) -> ("something" "is" "white" "+"))
Blue things are white.
((("something" "is" "blue" "+")) -> ("something" "is" "white" "+"))
If something is white and young then it is blue.
((("something" "is" "white" "+") ("something" "is" "young" "+")) -> ("something" "is" "blue" "+"))
Rough things are young.
((("something" "is" "rough" "+")) -> ("something" "is" "young" "+"))
If something is red and kind then it is cold.
((("something" "is" "red" "+") ("something" "is" "kind" "+")) -> ("something" "is" "cold" "+"))
Young, white things are kind.
((("something" "is" "young" "+") ("something" "is" "white" "+")) -> ("something" "is" "kind" "+"))
If something is young and rough then it is kind.
((("something" "is" "young" "+") ("something" "is" "rough" "+")) -> ("something" "is" "kind" "+"))
All rough, blue things are white.
((("something" "is" "rough" "+") ("something" "is" "blue" "+")) -> ("something" "is" "white" "+"))
Harry is rough.
True
1
proof
[(triple4)]
("Harry" "is" "rough" "+")
triple4
Anne is not blue.
False
1
inv-proof
[(triple1)]
("Anne" "is" "blue" "-")
triple1
Harry is young.
True
2
proof
[(((triple4) -> rule4))]
("Harry" "is" "young" "+")
((triple4) -> (rule4 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is not young.
False
2
inv-proof
[(((triple4) -> rule4))]
("Harry" "is" "young" "-")
((triple4) -> (rule4 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is kind.
True
4
proof
[(((((triple4) -> rule4) triple4) -> rule7))]
("Harry" "is" "kind" "+")
((((triple4) -> (rule4 % int2)) triple4) -> (rule7 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is not kind.
False
4
inv-proof
[(((((triple4) -> rule4) triple4) -> rule7))]
("Harry" "is" "kind" "-")
((((triple4) -> (rule4 % int2)) triple4) -> (rule7 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Fiona is not blue.
Unknown
inv-rconc
[@2: Fiona is blue.[CWA. Example of deepest failure = (rule3 <- rule4 <- FAIL)]]
("Fiona" "is" "blue" "-")
Fiona is kind.
Unknown
rconc
[@2: Fiona is kind.[CWA. Example of deepest failure = (rule6 <- rule4 <- FAIL)]]
("Fiona" "is" "kind" "+")
Harry is not blue.
Unknown
inv-rconc
[@2: Harry is blue.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Harry" "is" "blue" "-")
Fiona is rough.
Unknown
random
[@0: Fiona is rough.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "rough" "+")
Harry is not red.
Unknown
inv-random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "-")
Anne is red.
Unknown
random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "+")
@0: Anne is blue.[(triple1)] Fiona is red.[(triple2)] Gary is red.[(triple3)] Harry is rough.[(triple4)] @1: Anne is white.[(((triple1) -> rule2))] Harry is young.[(((triple4) -> rule4))] @2: Harry is kind.[(((((triple4) -> rule4) triple4) -> rule7))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Fiona is red.
("Fiona" "is" "red" "+")
triple2
Gary is red.
("Gary" "is" "red" "+")
triple3
Harry is rough.
("Harry" "is" "rough" "+")
triple4
Anne is white.
("Anne" "is" "white" "+")
((triple1) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
((triple4) -> (rule4 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
((((triple4) -> (rule4 % int2)) triple4) -> (rule7 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2