Anne is big. Harry is blue. If Anne is young and Anne is rough then Anne is green. If something is big then it is cold. Cold things are big. Blue, green things are big. If something is blue then it is green. Rough things are cold. All young, blue things are rough. Blue, rough things are kind.
Anne is big.
("Anne" "is" "big" "+")
Harry is blue.
("Harry" "is" "blue" "+")
If Anne is young and Anne is rough then Anne is green.
((("Anne" "is" "young" "+") ("Anne" "is" "rough" "+")) -> ("Anne" "is" "green" "+"))
If something is big then it is cold.
((("something" "is" "big" "+")) -> ("something" "is" "cold" "+"))
Cold things are big.
((("something" "is" "cold" "+")) -> ("something" "is" "big" "+"))
Blue, green things are big.
((("something" "is" "blue" "+") ("something" "is" "green" "+")) -> ("something" "is" "big" "+"))
If something is blue then it is green.
((("something" "is" "blue" "+")) -> ("something" "is" "green" "+"))
Rough things are cold.
((("something" "is" "rough" "+")) -> ("something" "is" "cold" "+"))
All young, blue things are rough.
((("something" "is" "young" "+") ("something" "is" "blue" "+")) -> ("something" "is" "rough" "+"))
Blue, rough things are kind.
((("something" "is" "blue" "+") ("something" "is" "rough" "+")) -> ("something" "is" "kind" "+"))
Anne is big.
True
1
proof
[(triple1)]
("Anne" "is" "big" "+")
triple1
Harry is not blue.
False
1
inv-proof
[(triple2)]
("Harry" "is" "blue" "-")
triple2
Anne is cold.
True
2
proof
[(((triple1) -> rule2))]
("Anne" "is" "cold" "+")
((triple1) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Harry is not green.
False
2
inv-proof
[(((triple2) -> rule5))]
("Harry" "is" "green" "-")
((triple2) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is big.
True
4
proof
[(((triple2 ((triple2) -> rule5)) -> rule4))]
("Harry" "is" "big" "+")
((triple2 ((triple2) -> (rule5 % int2))) -> (rule4 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is not big.
False
4
inv-proof
[(((triple2 ((triple2) -> rule5)) -> rule4))]
("Harry" "is" "big" "-")
((triple2 ((triple2) -> (rule5 % int2))) -> (rule4 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is cold.
True
5
proof
[(((((triple2 ((triple2) -> rule5)) -> rule4)) -> rule2))]
("Harry" "is" "cold" "+")
((((triple2 ((triple2) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is not cold.
False
5
inv-proof
[(((((triple2 ((triple2) -> rule5)) -> rule4)) -> rule2))]
("Harry" "is" "cold" "-")
((((triple2 ((triple2) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Anne is not kind.
Unknown
inv-rconc
[@1: Anne is kind.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Anne" "is" "kind" "-")
Harry is rough.
Unknown
rconc
[@1: Harry is rough.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Harry" "is" "rough" "+")
Harry is not kind.
Unknown
inv-rconc
[@2: Harry is kind.[CWA. Example of deepest failure = (rule8 <- rule7 <- FAIL)]]
("Harry" "is" "kind" "-")
Anne is rough.
Unknown
rconc
[@1: Anne is rough.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Anne" "is" "rough" "+")
Anne is not young.
Unknown
inv-random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "-")
Harry is young.
Unknown
random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "+")
@0: Anne is big.[(triple1)] Harry is blue.[(triple2)] @1: Anne is cold.[(((triple1) -> rule2))] Harry is green.[(((triple2) -> rule5))] @2: Harry is big.[(((triple2 ((triple2) -> rule5)) -> rule4))] @3: Harry is cold.[(((((triple2 ((triple2) -> rule5)) -> rule4)) -> rule2))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Harry is blue.
("Harry" "is" "blue" "+")
triple2
Anne is cold.
("Anne" "is" "cold" "+")
((triple1) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
((triple2) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
((triple2 ((triple2) -> (rule5 % int2))) -> (rule4 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
((((triple2 ((triple2) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3