Anne is kind. Bob is white. Gary is not kind. If Gary is round and Gary is young then Gary is white. Kind things are young. All cold things are not blue. Young things are blue. All round things are white. If Anne is kind and Anne is blue then Anne is round.
Anne is kind.
("Anne" "is" "kind" "+")
Bob is white.
("Bob" "is" "white" "+")
Gary is not kind.
("Gary" "is" "kind" "-")
If Gary is round and Gary is young then Gary is white.
((("Gary" "is" "round" "+") ("Gary" "is" "young" "+")) -> ("Gary" "is" "white" "+"))
Kind things are young.
((("something" "is" "kind" "+")) -> ("something" "is" "young" "+"))
All cold things are not blue.
((("something" "is" "cold" "+")) -> ("something" "is" "blue" "-"))
Young things are blue.
((("something" "is" "young" "+")) -> ("something" "is" "blue" "+"))
All round things are white.
((("something" "is" "round" "+")) -> ("something" "is" "white" "+"))
If Anne is kind and Anne is blue then Anne is round.
((("Anne" "is" "kind" "+") ("Anne" "is" "blue" "+")) -> ("Anne" "is" "round" "+"))
Anne is kind.
True
1
proof
[(triple1)]
("Anne" "is" "kind" "+")
triple1
Gary is kind.
False
1
inv-proof
[(triple3)]
("Gary" "is" "kind" "+")
triple3
Anne is young.
True
2
proof
[(((triple1) -> rule2))]
("Anne" "is" "young" "+")
((triple1) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is not young.
False
2
inv-proof
[(((triple1) -> rule2))]
("Anne" "is" "young" "-")
((triple1) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is blue.
True
3
proof
[(((((triple1) -> rule2)) -> rule4))]
("Anne" "is" "blue" "+")
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is not blue.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule4))]
("Anne" "is" "blue" "-")
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is round.
True
5
proof
[(((triple1 ((((triple1) -> rule2)) -> rule4)) -> rule6))]
("Anne" "is" "round" "+")
((triple1 ((((triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is not round.
False
5
inv-proof
[(((triple1 ((((triple1) -> rule2)) -> rule4)) -> rule6))]
("Anne" "is" "round" "-")
((triple1 ((((triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Gary is not blue.
Unknown
inv-rconc
[@2: Gary is blue.[CWA. Example of deepest failure = (rule4 <- rule2 <- FAIL)]]
("Gary" "is" "blue" "-")
Bob is blue.
Unknown
rconc
[@2: Bob is blue.[CWA. Example of deepest failure = (rule4 <- rule2 <- FAIL)]]
("Bob" "is" "blue" "+")
Gary is not young.
Unknown
inv-rconc
[@1: Gary is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "young" "-")
Gary is white.
Unknown
rconc
[@1: Gary is white.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "white" "+")
Anne is not cold.
Unknown
inv-random
[@0: Anne is cold.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "cold" "-")
Bob is kind.
Unknown
random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "+")
Bob is not rough.
Unknown
inv-random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "-")
Anne is rough.
Unknown
random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "+")
@0: Anne is kind.[(triple1)] Bob is white.[(triple2)] Gary is not kind.[(triple3)] @1: Anne is young.[(((triple1) -> rule2))] @2: Anne is blue.[(((((triple1) -> rule2)) -> rule4))] @3: Anne is round.[(((triple1 ((((triple1) -> rule2)) -> rule4)) -> rule6))] @4: Anne is white.[(((((triple1 ((((triple1) -> rule2)) -> rule4)) -> rule6)) -> rule5))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Bob is white.
("Bob" "is" "white" "+")
triple2
Gary is not kind.
("Gary" "is" "kind" "-")
triple3
Anne is young.
("Anne" "is" "young" "+")
((triple1) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
((triple1 ((((triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is white.
("Anne" "is" "white" "+")
((((triple1 ((((triple1) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
int4