Anne is not cold. Bob is kind. Gary is kind. All kind things are blue. Quiet, kind things are young. All quiet, smart things are young. If Bob is blue then Bob is young. If something is blue and not kind then it is not rough. If something is young then it is rough. If something is kind then it is not quiet. If something is kind and not blue then it is cold.
Anne is not cold.
("Anne" "is" "cold" "-")
Bob is kind.
("Bob" "is" "kind" "+")
Gary is kind.
("Gary" "is" "kind" "+")
All kind things are blue.
((("something" "is" "kind" "+")) -> ("something" "is" "blue" "+"))
Quiet, kind things are young.
((("something" "is" "quiet" "+") ("something" "is" "kind" "+")) -> ("something" "is" "young" "+"))
All quiet, smart things are young.
((("something" "is" "quiet" "+") ("something" "is" "smart" "+")) -> ("something" "is" "young" "+"))
If Bob is blue then Bob is young.
((("Bob" "is" "blue" "+")) -> ("Bob" "is" "young" "+"))
If something is blue and not kind then it is not rough.
((("something" "is" "blue" "+") ("something" "is" "kind" "~")) -> ("something" "is" "rough" "-"))
If something is young then it is rough.
((("something" "is" "young" "+")) -> ("something" "is" "rough" "+"))
If something is kind then it is not quiet.
((("something" "is" "kind" "+")) -> ("something" "is" "quiet" "-"))
If something is kind and not blue then it is cold.
((("something" "is" "kind" "+") ("something" "is" "blue" "~")) -> ("something" "is" "cold" "+"))
Anne is not cold.
True
1
proof
[(triple1)]
("Anne" "is" "cold" "-")
triple1
Bob is not kind.
False
1
inv-proof
[(triple2)]
("Bob" "is" "kind" "-")
triple2
Bob is blue.
True
2
proof
[(((triple2) -> rule1))]
("Bob" "is" "blue" "+")
((triple2) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Gary is not blue.
False
2
inv-proof
[(((triple3) -> rule1))]
("Gary" "is" "blue" "-")
((triple3) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Bob is young.
True
3
proof
[(((((triple2) -> rule1)) -> rule4))]
("Bob" "is" "young" "+")
((((triple2) -> (rule1 % int2))) -> (rule4 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is not young.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule4))]
("Bob" "is" "young" "-")
((((triple2) -> (rule1 % int2))) -> (rule4 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Anne is not young.
Unknown
inv-rconc
[@1: Anne is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "young" "-")
Gary is rough.
Unknown
rconc
[@2: Gary is rough.[CWA. Example of deepest failure = (rule6 <- rule2 <- FAIL)]]
("Gary" "is" "rough" "+")
Anne is not blue.
Unknown
inv-rconc
[@1: Anne is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "blue" "-")
Anne is kind.
Unknown
random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "+")
Bob is not smart.
Unknown
inv-random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "-")
Anne is quiet.
Unknown
random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "+")
@0: Anne is not cold.[(triple1)] Bob is kind.[(triple2)] Gary is kind.[(triple3)] @1: Bob is blue.[(((triple2) -> rule1))] Bob is not quiet.[(((triple2) -> rule7))] Gary is blue.[(((triple3) -> rule1))] Gary is not quiet.[(((triple3) -> rule7))] @2: Bob is young.[(((((triple2) -> rule1)) -> rule4))] @3: Bob is rough.[(((((((triple2) -> rule1)) -> rule4)) -> rule6))]
Anne is not cold.
("Anne" "is" "cold" "-")
triple1
Bob is kind.
("Bob" "is" "kind" "+")
triple2
Gary is kind.
("Gary" "is" "kind" "+")
triple3
Bob is blue.
("Bob" "is" "blue" "+")
((triple2) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is not quiet.
("Bob" "is" "quiet" "-")
((triple2) -> (rule7 % int1))
Bob is not quiet.
("Bob" "is" "quiet" "-")
int1
Gary is blue.
("Gary" "is" "blue" "+")
((triple3) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is not quiet.
("Gary" "is" "quiet" "-")
((triple3) -> (rule7 % int1))
Gary is not quiet.
("Gary" "is" "quiet" "-")
int1
Bob is young.
("Bob" "is" "young" "+")
((((triple2) -> (rule1 % int2))) -> (rule4 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
((((((triple2) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3