Anne is green. Gary is big. Harry is quiet. All green people are cold. If someone is green and cold then they are big. If Gary is cold then Gary is quiet. All nice people are green. Big, cold people are quiet. If Gary is red and Gary is green then Gary is big.
Anne is green.
("Anne" "is" "green" "+")
Gary is big.
("Gary" "is" "big" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
All green people are cold.
((("someone" "is" "green" "+")) -> ("someone" "is" "cold" "+"))
If someone is green and cold then they are big.
((("someone" "is" "green" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "big" "+"))
If Gary is cold then Gary is quiet.
((("Gary" "is" "cold" "+")) -> ("Gary" "is" "quiet" "+"))
All nice people are green.
((("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
Big, cold people are quiet.
((("someone" "is" "big" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "quiet" "+"))
If Gary is red and Gary is green then Gary is big.
((("Gary" "is" "red" "+") ("Gary" "is" "green" "+")) -> ("Gary" "is" "big" "+"))
Harry is quiet.
True
1
proof
[(triple3)]
("Harry" "is" "quiet" "+")
triple3
Gary is not big.
False
1
inv-proof
[(triple2)]
("Gary" "is" "big" "-")
triple2
Anne is cold.
True
2
proof
[(((triple1) -> rule1))]
("Anne" "is" "cold" "+")
((triple1) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is not cold.
False
2
inv-proof
[(((triple1) -> rule1))]
("Anne" "is" "cold" "-")
((triple1) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is big.
True
4
proof
[(((triple1 ((triple1) -> rule1)) -> rule2))]
("Anne" "is" "big" "+")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is not big.
False
4
inv-proof
[(((triple1 ((triple1) -> rule1)) -> rule2))]
("Anne" "is" "big" "-")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is quiet.
True
7
proof
[(((((triple1 ((triple1) -> rule1)) -> rule2) ((triple1) -> rule1)) -> rule5))]
("Anne" "is" "quiet" "+")
((((triple1 ((triple1) -> (rule1 % int3))) -> (rule2 % int2)) ((triple1) -> (rule1 % int3))) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is not quiet.
False
7
inv-proof
[(((((triple1 ((triple1) -> rule1)) -> rule2) ((triple1) -> rule1)) -> rule5))]
("Anne" "is" "quiet" "-")
((((triple1 ((triple1) -> (rule1 % int3))) -> (rule2 % int2)) ((triple1) -> (rule1 % int3))) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Gary is not quiet.
Unknown
inv-rconc
[@3: Gary is quiet.[CWA. Example of deepest failure = (rule3 <- rule1 <- rule4 <- FAIL)]]
("Gary" "is" "quiet" "-")
Gary is cold.
Unknown
rconc
[@2: Gary is cold.[CWA. Example of deepest failure = (rule1 <- rule4 <- FAIL)]]
("Gary" "is" "cold" "+")
Harry is not big.
Unknown
inv-rconc
[@2: Harry is big.[CWA. Example of deepest failure = (rule2 <- rule4 <- FAIL)]]
("Harry" "is" "big" "-")
Gary is green.
Unknown
rconc
[@1: Gary is green.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "green" "+")
Harry is not nice.
Unknown
inv-random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "-")
Anne is red.
Unknown
random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "+")
Anne is not furry.
Unknown
inv-random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "-")
Harry is red.
Unknown
random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "+")
@0: Anne is green.[(triple1)] Gary is big.[(triple2)] Harry is quiet.[(triple3)] @1: Anne is cold.[(((triple1) -> rule1))] @2: Anne is big.[(((triple1 ((triple1) -> rule1)) -> rule2))] @3: Anne is quiet.[(((((triple1 ((triple1) -> rule1)) -> rule2) ((triple1) -> rule1)) -> rule5))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Gary is big.
("Gary" "is" "big" "+")
triple2
Harry is quiet.
("Harry" "is" "quiet" "+")
triple3
Anne is cold.
("Anne" "is" "cold" "+")
((triple1) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
((((triple1 ((triple1) -> (rule1 % int3))) -> (rule2 % int2)) ((triple1) -> (rule1 % int3))) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3