Anne is smart. Gary is big. If something is smart and not nice then it is rough. If something is young then it is rough. If Gary is nice and Gary is young then Gary is cold. Big things are young. All rough things are smart. Red things are not smart. If something is nice and young then it is not red. If Anne is rough and Anne is not nice then Anne is cold.
Anne is smart.
("Anne" "is" "smart" "+")
Gary is big.
("Gary" "is" "big" "+")
If something is smart and not nice then it is rough.
((("something" "is" "smart" "+") ("something" "is" "nice" "~")) -> ("something" "is" "rough" "+"))
If something is young then it is rough.
((("something" "is" "young" "+")) -> ("something" "is" "rough" "+"))
If Gary is nice and Gary is young then Gary is cold.
((("Gary" "is" "nice" "+") ("Gary" "is" "young" "+")) -> ("Gary" "is" "cold" "+"))
Big things are young.
((("something" "is" "big" "+")) -> ("something" "is" "young" "+"))
All rough things are smart.
((("something" "is" "rough" "+")) -> ("something" "is" "smart" "+"))
Red things are not smart.
((("something" "is" "red" "+")) -> ("something" "is" "smart" "-"))
If something is nice and young then it is not red.
((("something" "is" "nice" "+") ("something" "is" "young" "+")) -> ("something" "is" "red" "-"))
If Anne is rough and Anne is not nice then Anne is cold.
((("Anne" "is" "rough" "+") ("Anne" "is" "nice" "~")) -> ("Anne" "is" "cold" "+"))
Gary is big.
True
1
proof
[(triple2)]
("Gary" "is" "big" "+")
triple2
Gary is not big.
False
1
inv-proof
[(triple2)]
("Gary" "is" "big" "-")
triple2
Gary is young.
True
2
proof
[(((triple2) -> rule4))]
("Gary" "is" "young" "+")
((triple2) -> (rule4 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is not young.
False
2
inv-proof
[(((triple2) -> rule4))]
("Gary" "is" "young" "-")
((triple2) -> (rule4 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is rough.
True
3
proof
[(((((triple2) -> rule4)) -> rule2))]
("Gary" "is" "rough" "+")
((((triple2) -> (rule4 % int2))) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is not rough.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule2))]
("Gary" "is" "rough" "-")
((((triple2) -> (rule4 % int2))) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is smart.
True
4
proof
[(((((((triple2) -> rule4)) -> rule2)) -> rule5))]
("Gary" "is" "smart" "+")
((((((triple2) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Gary is not smart.
False
4
inv-proof
[(((((((triple2) -> rule4)) -> rule2)) -> rule5))]
("Gary" "is" "smart" "-")
((((((triple2) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Anne is not young.
Unknown
inv-rconc
[@1: Anne is young.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "young" "-")
Gary is cold.
Unknown
rconc
[@1: Gary is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "cold" "+")
Anne is not cold.
Unknown
inv-rconc
[@1: Anne is cold.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Anne" "is" "cold" "-")
Anne is rough.
Unknown
rconc
[@2: Anne is rough.[CWA. Example of deepest failure = (rule2 <- rule4 <- FAIL)]]
("Anne" "is" "rough" "+")
Gary is not red.
Unknown
inv-random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "-")
Anne is big.
Unknown
random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "+")
Gary is not nice.
Unknown
inv-random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "-")
Anne is red.
Unknown
random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "+")
@0: Anne is smart.[(triple1)] Gary is big.[(triple2)] @1: Gary is young.[(((triple2) -> rule4))] @2: Gary is rough.[(((((triple2) -> rule4)) -> rule2))] @3: Gary is smart.[(((((((triple2) -> rule4)) -> rule2)) -> rule5))]
Anne is smart.
("Anne" "is" "smart" "+")
triple1
Gary is big.
("Gary" "is" "big" "+")
triple2
Gary is young.
("Gary" "is" "young" "+")
((triple2) -> (rule4 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
((((triple2) -> (rule4 % int2))) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
((((((triple2) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3