Anne is cold. Anne is green. Anne is kind. Anne is white. Anne is young. Charlie is not green. Charlie is kind. Charlie is rough. Charlie is not young. Dave is kind. Dave is white. Harry is blue. Harry is green. Harry is white. Harry is not young. If something is white then it is cold. If Dave is not blue then Dave is young.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is white.
("Anne" "is" "white" "+")
Anne is young.
("Anne" "is" "young" "+")
Charlie is not green.
("Charlie" "is" "green" "-")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is not young.
("Charlie" "is" "young" "-")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is white.
("Dave" "is" "white" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is white.
("Harry" "is" "white" "+")
Harry is not young.
("Harry" "is" "young" "-")
If something is white then it is cold.
((("something" "is" "white" "+")) -> ("something" "is" "cold" "+"))
If Dave is not blue then Dave is young.
((("Dave" "is" "blue" "~")) -> ("Dave" "is" "young" "+"))
Harry is white.
True
1
proof
[(triple14)]
("Harry" "is" "white" "+")
triple14
Anne is not cold.
False
1
inv-proof
[(triple1 OR ((triple4) -> rule1))]
("Anne" "is" "cold" "-")
triple1
((triple4) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Harry is cold.
True
2
proof
[(((triple14) -> rule1))]
("Harry" "is" "cold" "+")
((triple14) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is not cold.
False
2
inv-proof
[(((triple14) -> rule1))]
("Harry" "is" "cold" "-")
((triple14) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Charlie is not cold.
Unknown
inv-rconc
[@1: Charlie is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "cold" "-")
Dave is young.
Unknown
rconc
[@1: Dave is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "young" "+")
Dave is not blue.
Unknown
inv-random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "-")
Anne is rough.
Unknown
random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "+")
@0: Anne is cold.[(triple1 OR ((triple4) -> rule1))] Anne is green.[(triple2)] Anne is kind.[(triple3)] Anne is white.[(triple4)] Anne is young.[(triple5)] Charlie is kind.[(triple7)] Charlie is not green.[(triple6)] Charlie is not young.[(triple9)] Charlie is rough.[(triple8)] Dave is kind.[(triple10)] Dave is white.[(triple11)] Harry is blue.[(triple12)] Harry is green.[(triple13)] Harry is not young.[(triple15)] Harry is white.[(triple14)] @1: Dave is cold.[(((triple11) -> rule1))] Harry is cold.[(((triple14) -> rule1))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
((triple4) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
triple2
Anne is kind.
("Anne" "is" "kind" "+")
triple3
Anne is white.
("Anne" "is" "white" "+")
triple4
Anne is young.
("Anne" "is" "young" "+")
triple5
Charlie is kind.
("Charlie" "is" "kind" "+")
triple7
Charlie is not green.
("Charlie" "is" "green" "-")
triple6
Charlie is not young.
("Charlie" "is" "young" "-")
triple9
Charlie is rough.
("Charlie" "is" "rough" "+")
triple8
Dave is kind.
("Dave" "is" "kind" "+")
triple10
Dave is white.
("Dave" "is" "white" "+")
triple11
Harry is blue.
("Harry" "is" "blue" "+")
triple12
Harry is green.
("Harry" "is" "green" "+")
triple13
Harry is not young.
("Harry" "is" "young" "-")
triple15
Harry is white.
("Harry" "is" "white" "+")
triple14
Dave is cold.
("Dave" "is" "cold" "+")
((triple11) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
((triple14) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1