Anne is cold. Anne is rough. Charlie is kind. Erin is blue. Erin is cold. Erin is furry. Gary is cold. Furry people are green. All rough people are furry. Green people are furry. If someone is rough then they are young. If Erin is green and Erin is furry then Erin is young. If someone is young then they are kind. If someone is green and furry then they are rough. If Charlie is young then Charlie is rough.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Furry people are green.
((("someone" "is" "furry" "+")) -> ("someone" "is" "green" "+"))
All rough people are furry.
((("someone" "is" "rough" "+")) -> ("someone" "is" "furry" "+"))
Green people are furry.
((("someone" "is" "green" "+")) -> ("someone" "is" "furry" "+"))
If someone is rough then they are young.
((("someone" "is" "rough" "+")) -> ("someone" "is" "young" "+"))
If Erin is green and Erin is furry then Erin is young.
((("Erin" "is" "green" "+") ("Erin" "is" "furry" "+")) -> ("Erin" "is" "young" "+"))
If someone is young then they are kind.
((("someone" "is" "young" "+")) -> ("someone" "is" "kind" "+"))
If someone is green and furry then they are rough.
((("someone" "is" "green" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "rough" "+"))
If Charlie is young then Charlie is rough.
((("Charlie" "is" "young" "+")) -> ("Charlie" "is" "rough" "+"))
Erin is cold.
True
1
proof
[(triple5)]
("Erin" "is" "cold" "+")
triple5
Gary is not cold.
False
1
inv-proof
[(triple7)]
("Gary" "is" "cold" "-")
triple7
Erin is green.
True
2
proof
[(((triple6) -> rule1))]
("Erin" "is" "green" "+")
((triple6) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is not green.
False
2
inv-proof
[(((triple6) -> rule1))]
("Erin" "is" "green" "-")
((triple6) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is young.
True
4
proof
[(((((triple6) -> rule1) triple6) -> rule5) OR ((((((triple6) -> rule1) triple6) -> rule7)) -> rule4))]
("Erin" "is" "young" "+")
((((triple6) -> (rule1 % int2)) triple6) -> (rule5 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
((((((triple6) -> (rule1 % int3)) triple6) -> (rule7 % int2))) -> (rule4 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Anne is not green.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule1))]
("Anne" "is" "green" "-")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Erin is kind.
True
5
proof
[(((((((triple6) -> rule1) triple6) -> rule5)) -> rule6) OR ((((((((triple6) -> rule1) triple6) -> rule7)) -> rule4)) -> rule6))]
("Erin" "is" "kind" "+")
((((((triple6) -> (rule1 % int3)) triple6) -> (rule5 % int2))) -> (rule6 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
((((((((triple6) -> (rule1 % int4)) triple6) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
int4
Erin is not kind.
False
5
inv-proof
[(((((((triple6) -> rule1) triple6) -> rule5)) -> rule6) OR ((((((((triple6) -> rule1) triple6) -> rule7)) -> rule4)) -> rule6))]
("Erin" "is" "kind" "-")
((((((triple6) -> (rule1 % int3)) triple6) -> (rule5 % int2))) -> (rule6 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
((((((((triple6) -> (rule1 % int4)) triple6) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
int4
Gary is not young.
Unknown
inv-rconc
[@4: Gary is young.[CWA. Example of deepest failure = (rule4 <- rule7 <- rule1 <- rule2 <- FAIL)]]
("Gary" "is" "young" "-")
Gary is rough.
Unknown
rconc
[@3: Gary is rough.[CWA. Example of deepest failure = (rule7 <- rule1 <- rule2 <- FAIL)]]
("Gary" "is" "rough" "+")
Charlie is not young.
Unknown
inv-rconc
[@5: Charlie is young.[CWA. Example of deepest failure = (rule4 <- rule7 <- rule1 <- rule2 <- rule8 <- FAIL)]]
("Charlie" "is" "young" "-")
Charlie is rough.
Unknown
rconc
[@5: Charlie is rough.[CWA. Example of deepest failure = (rule7 <- rule1 <- rule2 <- rule8 <- rule4 <- FAIL)]]
("Charlie" "is" "rough" "+")
Gary is not blue.
Unknown
inv-random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "-")
Charlie is cold.
Unknown
random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "+")
Charlie is not blue.
Unknown
inv-random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "-")
Anne is blue.
Unknown
random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "+")
@0: Anne is cold.[(triple1)] Anne is rough.[(triple2)] Charlie is kind.[(triple3)] Erin is blue.[(triple4)] Erin is cold.[(triple5)] Erin is furry.[(triple6)] Gary is cold.[(triple7)] @1: Anne is furry.[(((triple2) -> rule2))] Anne is young.[(((triple2) -> rule4))] Erin is green.[(((triple6) -> rule1))] @2: Anne is green.[(((((triple2) -> rule2)) -> rule1))] Anne is kind.[(((((triple2) -> rule4)) -> rule6))] Erin is rough.[(((((triple6) -> rule1) triple6) -> rule7))] Erin is young.[(((((triple6) -> rule1) triple6) -> rule5) OR ((((((triple6) -> rule1) triple6) -> rule7)) -> rule4))] @3: Erin is kind.[(((((((triple6) -> rule1) triple6) -> rule5)) -> rule6) OR ((((((((triple6) -> rule1) triple6) -> rule7)) -> rule4)) -> rule6))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is rough.
("Anne" "is" "rough" "+")
triple2
Charlie is kind.
("Charlie" "is" "kind" "+")
triple3
Erin is blue.
("Erin" "is" "blue" "+")
triple4
Erin is cold.
("Erin" "is" "cold" "+")
triple5
Erin is furry.
("Erin" "is" "furry" "+")
triple6
Gary is cold.
("Gary" "is" "cold" "+")
triple7
Anne is furry.
("Anne" "is" "furry" "+")
((triple2) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
((triple2) -> (rule4 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
((triple6) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
((((triple2) -> (rule4 % int2))) -> (rule6 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
((((triple6) -> (rule1 % int2)) triple6) -> (rule7 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
((((triple6) -> (rule1 % int2)) triple6) -> (rule5 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
((((((triple6) -> (rule1 % int3)) triple6) -> (rule7 % int2))) -> (rule4 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is kind.
("Erin" "is" "kind" "+")
((((((triple6) -> (rule1 % int3)) triple6) -> (rule5 % int2))) -> (rule6 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
((((((((triple6) -> (rule1 % int4)) triple6) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
int4