Anne is kind. Charlie is nice. Dave is big. Harry is big. All cold, big things are young. If something is blue then it is young. If something is kind and not red then it is cold. If something is young then it is not cold. If Charlie is nice then Charlie is blue. All red, nice things are blue. All young, big things are not nice. If Harry is blue and Harry is not kind then Harry is not big.
Anne is kind.
("Anne" "is" "kind" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Dave is big.
("Dave" "is" "big" "+")
Harry is big.
("Harry" "is" "big" "+")
All cold, big things are young.
((("something" "is" "cold" "+") ("something" "is" "big" "+")) -> ("something" "is" "young" "+"))
If something is blue then it is young.
((("something" "is" "blue" "+")) -> ("something" "is" "young" "+"))
If something is kind and not red then it is cold.
((("something" "is" "kind" "+") ("something" "is" "red" "~")) -> ("something" "is" "cold" "+"))
If something is young then it is not cold.
((("something" "is" "young" "+")) -> ("something" "is" "cold" "-"))
If Charlie is nice then Charlie is blue.
((("Charlie" "is" "nice" "+")) -> ("Charlie" "is" "blue" "+"))
All red, nice things are blue.
((("something" "is" "red" "+") ("something" "is" "nice" "+")) -> ("something" "is" "blue" "+"))
All young, big things are not nice.
((("something" "is" "young" "+") ("something" "is" "big" "+")) -> ("something" "is" "nice" "-"))
If Harry is blue and Harry is not kind then Harry is not big.
((("Harry" "is" "blue" "+") ("Harry" "is" "kind" "~")) -> ("Harry" "is" "big" "-"))
Anne is kind.
True
1
proof
[(triple1)]
("Anne" "is" "kind" "+")
triple1
Harry is not big.
False
1
inv-proof
[(triple4)]
("Harry" "is" "big" "-")
triple4
Charlie is blue.
True
2
proof
[(((triple2) -> rule5))]
("Charlie" "is" "blue" "+")
((triple2) -> (rule5 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is not blue.
False
2
inv-proof
[(((triple2) -> rule5))]
("Charlie" "is" "blue" "-")
((triple2) -> (rule5 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is young.
True
3
proof
[(((((triple2) -> rule5)) -> rule2))]
("Charlie" "is" "young" "+")
((((triple2) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is not young.
False
3
inv-proof
[(((((triple2) -> rule5)) -> rule2))]
("Charlie" "is" "young" "-")
((((triple2) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is not cold.
True
4
proof
[(((((((triple2) -> rule5)) -> rule2)) -> rule4))]
("Charlie" "is" "cold" "-")
((((((triple2) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is not cold.
("Charlie" "is" "cold" "-")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is cold.
False
4
inv-proof
[(((((((triple2) -> rule5)) -> rule2)) -> rule4))]
("Charlie" "is" "cold" "+")
((((((triple2) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is not cold.
("Charlie" "is" "cold" "-")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Anne is not young.
Unknown
inv-rconc
[@2: Anne is young.[CWA. Example of deepest failure = (rule2 <- rule6 <- FAIL)]]
("Anne" "is" "young" "-")
Anne is cold.
Unknown
rconc
[@1: Anne is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "cold" "+")
Dave is not young.
Unknown
inv-rconc
[@2: Dave is young.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Dave" "is" "young" "-")
Anne is blue.
Unknown
rconc
[@1: Anne is blue.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Anne" "is" "blue" "+")
Harry is not kind.
Unknown
inv-random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "-")
Charlie is big.
Unknown
random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "+")
Anne is not nice.
Unknown
inv-random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "-")
Anne is red.
Unknown
random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "+")
@0: Anne is kind.[(triple1)] Charlie is nice.[(triple2)] Dave is big.[(triple3)] Harry is big.[(triple4)] @1: Charlie is blue.[(((triple2) -> rule5))] @2: Charlie is young.[(((((triple2) -> rule5)) -> rule2))] @3: Charlie is not cold.[(((((((triple2) -> rule5)) -> rule2)) -> rule4))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple2
Dave is big.
("Dave" "is" "big" "+")
triple3
Harry is big.
("Harry" "is" "big" "+")
triple4
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple2) -> (rule5 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
((((triple2) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is not cold.
("Charlie" "is" "cold" "-")
((((((triple2) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is not cold.
("Charlie" "is" "cold" "-")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3