Anne is rough. Erin is furry. Harry is not green. All rough things are cold. Furry things are cold. If something is big and blue then it is rough. If something is rough and cold then it is green. All green things are not big. If something is rough then it is blue. Rough things are blue. If something is cold and not green then it is kind.
Anne is rough.
("Anne" "is" "rough" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Harry is not green.
("Harry" "is" "green" "-")
All rough things are cold.
((("something" "is" "rough" "+")) -> ("something" "is" "cold" "+"))
Furry things are cold.
((("something" "is" "furry" "+")) -> ("something" "is" "cold" "+"))
If something is big and blue then it is rough.
((("something" "is" "big" "+") ("something" "is" "blue" "+")) -> ("something" "is" "rough" "+"))
If something is rough and cold then it is green.
((("something" "is" "rough" "+") ("something" "is" "cold" "+")) -> ("something" "is" "green" "+"))
All green things are not big.
((("something" "is" "green" "+")) -> ("something" "is" "big" "-"))
If something is rough then it is blue.
((("something" "is" "rough" "+")) -> ("something" "is" "blue" "+"))
Rough things are blue.
((("something" "is" "rough" "+")) -> ("something" "is" "blue" "+"))
If something is cold and not green then it is kind.
((("something" "is" "cold" "+") ("something" "is" "green" "~")) -> ("something" "is" "kind" "+"))
Anne is rough.
True
1
proof
[(triple1)]
("Anne" "is" "rough" "+")
triple1
Erin is not furry.
False
1
inv-proof
[(triple2)]
("Erin" "is" "furry" "-")
triple2
Erin is cold.
True
2
proof
[(((triple2) -> rule2))]
("Erin" "is" "cold" "+")
((triple2) -> (rule2 % int1))
Erin is cold.
("Erin" "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
Erin is not blue.
Unknown
inv-rconc
[@2: Erin is blue.[CWA. Example of deepest failure = (rule6 <- rule3 <- FAIL)]]
("Erin" "is" "blue" "-")
Harry is kind.
Unknown
rconc
[@1: Harry is kind.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Harry" "is" "kind" "+")
Harry is not furry.
Unknown
inv-random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "-")
Anne is furry.
Unknown
random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "+")
@0: Anne is rough.[(triple1)] Erin is furry.[(triple2)] Harry is not green.[(triple3)] @1: Anne is blue.[(((triple1) -> rule6) OR ((triple1) -> rule7))] Anne is cold.[(((triple1) -> rule1))] Erin is cold.[(((triple2) -> rule2))] @2: Anne is green.[(((triple1 ((triple1) -> rule1)) -> rule4))] @3: Anne is not big.[(((((triple1 ((triple1) -> rule1)) -> rule4)) -> rule5))]
Anne is rough.
("Anne" "is" "rough" "+")
triple1
Erin is furry.
("Erin" "is" "furry" "+")
triple2
Harry is not green.
("Harry" "is" "green" "-")
triple3
Anne is blue.
("Anne" "is" "blue" "+")
((triple1) -> (rule6 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
((triple1) -> (rule7 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
((triple1) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
((triple2) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is not big.
("Anne" "is" "big" "-")
((((triple1 ((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Anne is not big.
("Anne" "is" "big" "-")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3