Anne is white. Gary is kind. If something is kind then it is smart. If something is big and green then it is smart. If something is green and white then it is blue. If something is big and blue then it is kind. If Gary is smart then Gary is green. All cold, big things are green. All kind, smart things are white. If something is big and cold then it is kind.
Anne is white.
("Anne" "is" "white" "+")
Gary is kind.
("Gary" "is" "kind" "+")
If something is kind then it is smart.
((("something" "is" "kind" "+")) -> ("something" "is" "smart" "+"))
If something is big and green then it is smart.
((("something" "is" "big" "+") ("something" "is" "green" "+")) -> ("something" "is" "smart" "+"))
If something is green and white then it is blue.
((("something" "is" "green" "+") ("something" "is" "white" "+")) -> ("something" "is" "blue" "+"))
If something is big and blue then it is kind.
((("something" "is" "big" "+") ("something" "is" "blue" "+")) -> ("something" "is" "kind" "+"))
If Gary is smart then Gary is green.
((("Gary" "is" "smart" "+")) -> ("Gary" "is" "green" "+"))
All cold, big things are green.
((("something" "is" "cold" "+") ("something" "is" "big" "+")) -> ("something" "is" "green" "+"))
All kind, smart things are white.
((("something" "is" "kind" "+") ("something" "is" "smart" "+")) -> ("something" "is" "white" "+"))
If something is big and cold then it is kind.
((("something" "is" "big" "+") ("something" "is" "cold" "+")) -> ("something" "is" "kind" "+"))
Anne is white.
True
1
proof
[(triple1)]
("Anne" "is" "white" "+")
triple1
Gary is not kind.
False
1
inv-proof
[(triple2)]
("Gary" "is" "kind" "-")
triple2
Gary is smart.
True
2
proof
[(((triple2) -> rule1))]
("Gary" "is" "smart" "+")
((triple2) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is not smart.
False
2
inv-proof
[(((triple2) -> rule1))]
("Gary" "is" "smart" "-")
((triple2) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is white.
True
4
proof
[(((triple2 ((triple2) -> rule1)) -> rule7))]
("Gary" "is" "white" "+")
((triple2 ((triple2) -> (rule1 % int2))) -> (rule7 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is not green.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule5))]
("Gary" "is" "green" "-")
((((triple2) -> (rule1 % int2))) -> (rule5 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is blue.
True
8
proof
[(((((((triple2) -> rule1)) -> rule5) ((triple2 ((triple2) -> rule1)) -> rule7)) -> rule3))]
("Gary" "is" "blue" "+")
((((((triple2) -> (rule1 % int4))) -> (rule5 % int3)) ((triple2 ((triple2) -> (rule1 % int4))) -> (rule7 % int2))) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
int4
Gary is not blue.
False
8
inv-proof
[(((((((triple2) -> rule1)) -> rule5) ((triple2 ((triple2) -> rule1)) -> rule7)) -> rule3))]
("Gary" "is" "blue" "-")
((((((triple2) -> (rule1 % int4))) -> (rule5 % int3)) ((triple2 ((triple2) -> (rule1 % int4))) -> (rule7 % int2))) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
int4
Anne is not kind.
Unknown
inv-rconc
[@1: Anne is kind.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "kind" "-")
Anne is blue.
Unknown
rconc
[@2: Anne is blue.[CWA. Example of deepest failure = (rule3 <- rule6 <- FAIL)]]
("Anne" "is" "blue" "+")
Anne is not green.
Unknown
inv-rconc
[@1: Anne is green.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Anne" "is" "green" "-")
Anne is smart.
Unknown
rconc
[@2: Anne is smart.[CWA. Example of deepest failure = (rule1 <- rule4 <- FAIL)]]
("Anne" "is" "smart" "+")
Anne is not cold.
Unknown
inv-random
[@0: Anne is cold.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "cold" "-")
Gary is big.
Unknown
random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "+")
Gary is not cold.
Unknown
inv-random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "-")
Anne is big.
Unknown
random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "+")
@0: Anne is white.[(triple1)] Gary is kind.[(triple2)] @1: Gary is smart.[(((triple2) -> rule1))] @2: Gary is green.[(((((triple2) -> rule1)) -> rule5))] Gary is white.[(((triple2 ((triple2) -> rule1)) -> rule7))] @3: Gary is blue.[(((((((triple2) -> rule1)) -> rule5) ((triple2 ((triple2) -> rule1)) -> rule7)) -> rule3))]
Anne is white.
("Anne" "is" "white" "+")
triple1
Gary is kind.
("Gary" "is" "kind" "+")
triple2
Gary is smart.
("Gary" "is" "smart" "+")
((triple2) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
((((triple2) -> (rule1 % int2))) -> (rule5 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
((triple2 ((triple2) -> (rule1 % int2))) -> (rule7 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
((((((triple2) -> (rule1 % int4))) -> (rule5 % int3)) ((triple2 ((triple2) -> (rule1 % int4))) -> (rule7 % int2))) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
int4