Anne is cold. Anne is red. Bob is big. Bob is kind. Erin is green. Erin is red. Harry is big. If Erin is kind then Erin is red. Red, furry things are rough. If something is green and rough then it is kind. If something is cold then it is furry. Green things are cold. All furry, big things are cold. All kind things are big. If Anne is furry then Anne is cold.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is red.
("Anne" "is" "red" "+")
Bob is big.
("Bob" "is" "big" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is red.
("Erin" "is" "red" "+")
Harry is big.
("Harry" "is" "big" "+")
If Erin is kind then Erin is red.
((("Erin" "is" "kind" "+")) -> ("Erin" "is" "red" "+"))
Red, furry things are rough.
((("something" "is" "red" "+") ("something" "is" "furry" "+")) -> ("something" "is" "rough" "+"))
If something is green and rough then it is kind.
((("something" "is" "green" "+") ("something" "is" "rough" "+")) -> ("something" "is" "kind" "+"))
If something is cold then it is furry.
((("something" "is" "cold" "+")) -> ("something" "is" "furry" "+"))
Green things are cold.
((("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
All furry, big things are cold.
((("something" "is" "furry" "+") ("something" "is" "big" "+")) -> ("something" "is" "cold" "+"))
All kind things are big.
((("something" "is" "kind" "+")) -> ("something" "is" "big" "+"))
If Anne is furry then Anne is cold.
((("Anne" "is" "furry" "+")) -> ("Anne" "is" "cold" "+"))
Erin is red.
True
1
proof
[(triple6)]
("Erin" "is" "red" "+")
triple6
Bob is not big.
False
1
inv-proof
[(triple3 OR ((triple4) -> rule7))]
("Bob" "is" "big" "-")
triple3
((triple4) -> (rule7 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Erin is cold.
True
2
proof
[(((triple5) -> rule5))]
("Erin" "is" "cold" "+")
((triple5) -> (rule5 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Anne is not furry.
False
2
inv-proof
[(((triple1) -> rule4))]
("Anne" "is" "furry" "-")
((triple1) -> (rule4 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Erin is furry.
True
3
proof
[(((((triple5) -> rule5)) -> rule4))]
("Erin" "is" "furry" "+")
((((triple5) -> (rule5 % int2))) -> (rule4 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is not furry.
False
3
inv-proof
[(((((triple5) -> rule5)) -> rule4))]
("Erin" "is" "furry" "-")
((((triple5) -> (rule5 % int2))) -> (rule4 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is rough.
True
5
proof
[(((triple6 ((((triple5) -> rule5)) -> rule4)) -> rule2))]
("Erin" "is" "rough" "+")
((triple6 ((((triple5) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is not rough.
False
5
inv-proof
[(((triple6 ((((triple5) -> rule5)) -> rule4)) -> rule2))]
("Erin" "is" "rough" "-")
((triple6 ((((triple5) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is kind.
True
7
proof
[(((triple5 ((triple6 ((((triple5) -> rule5)) -> rule4)) -> rule2)) -> rule3))]
("Erin" "is" "kind" "+")
((triple5 ((triple6 ((((triple5) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Erin is cold.
("Erin" "is" "cold" "+")
int4
Erin is not kind.
False
7
inv-proof
[(((triple5 ((triple6 ((((triple5) -> rule5)) -> rule4)) -> rule2)) -> rule3))]
("Erin" "is" "kind" "-")
((triple5 ((triple6 ((((triple5) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Erin is cold.
("Erin" "is" "cold" "+")
int4
Erin is big.
True
8
proof
[(((((triple5 ((triple6 ((((triple5) -> rule5)) -> rule4)) -> rule2)) -> rule3)) -> rule7))]
("Erin" "is" "big" "+")
((((triple5 ((triple6 ((((triple5) -> (rule5 % int5))) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is furry.
("Erin" "is" "furry" "+")
int4
Erin is cold.
("Erin" "is" "cold" "+")
int5
Erin is not big.
False
8
inv-proof
[(((((triple5 ((triple6 ((((triple5) -> rule5)) -> rule4)) -> rule2)) -> rule3)) -> rule7))]
("Erin" "is" "big" "-")
((((triple5 ((triple6 ((((triple5) -> (rule5 % int5))) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is furry.
("Erin" "is" "furry" "+")
int4
Erin is cold.
("Erin" "is" "cold" "+")
int5
Bob is not cold.
Unknown
inv-rconc
[@3: Bob is cold.[CWA. Example of deepest failure = (rule6 <- rule4 <- rule5 <- FAIL)]]
("Bob" "is" "cold" "-")
Bob is furry.
Unknown
rconc
[@2: Bob is furry.[CWA. Example of deepest failure = (rule4 <- rule5 <- FAIL)]]
("Bob" "is" "furry" "+")
Harry is not rough.
Unknown
inv-rconc
[@1: Harry is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "rough" "-")
Harry is cold.
Unknown
rconc
[@3: Harry is cold.[CWA. Example of deepest failure = (rule6 <- rule4 <- rule5 <- FAIL)]]
("Harry" "is" "cold" "+")
Bob is not rough.
Unknown
inv-rconc
[@1: Bob is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "rough" "-")
Anne is big.
Unknown
rconc
[@2: Anne is big.[CWA. Example of deepest failure = (rule7 <- rule3 <- FAIL)]]
("Anne" "is" "big" "+")
Bob is not red.
Unknown
inv-random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "-")
Anne is green.
Unknown
random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "+")
Harry is not green.
Unknown
inv-random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "-")
Harry is red.
Unknown
random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "+")
@0: Anne is cold.[(triple1)] Anne is red.[(triple2)] Bob is big.[(triple3 OR ((triple4) -> rule7))] Bob is kind.[(triple4)] Erin is green.[(triple5)] Erin is red.[(triple6)] Harry is big.[(triple7)] @1: Anne is furry.[(((triple1) -> rule4))] Erin is cold.[(((triple5) -> rule5))] @2: Anne is rough.[(((triple2 ((triple1) -> rule4)) -> rule2))] Erin is furry.[(((((triple5) -> rule5)) -> rule4))] @3: Erin is rough.[(((triple6 ((((triple5) -> rule5)) -> rule4)) -> rule2))] @4: Erin is kind.[(((triple5 ((triple6 ((((triple5) -> rule5)) -> rule4)) -> rule2)) -> rule3))] @5: Erin is big.[(((((triple5 ((triple6 ((((triple5) -> rule5)) -> rule4)) -> rule2)) -> rule3)) -> rule7))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is red.
("Anne" "is" "red" "+")
triple2
Bob is big.
("Bob" "is" "big" "+")
triple3
((triple4) -> (rule7 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
triple4
Erin is green.
("Erin" "is" "green" "+")
triple5
Erin is red.
("Erin" "is" "red" "+")
triple6
Harry is big.
("Harry" "is" "big" "+")
triple7
Anne is furry.
("Anne" "is" "furry" "+")
((triple1) -> (rule4 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
((triple5) -> (rule5 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
((triple2 ((triple1) -> (rule4 % int2))) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
((((triple5) -> (rule5 % int2))) -> (rule4 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
((triple6 ((((triple5) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is kind.
("Erin" "is" "kind" "+")
((triple5 ((triple6 ((((triple5) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Erin is cold.
("Erin" "is" "cold" "+")
int4
Erin is big.
("Erin" "is" "big" "+")
((((triple5 ((triple6 ((((triple5) -> (rule5 % int5))) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is furry.
("Erin" "is" "furry" "+")
int4
Erin is cold.
("Erin" "is" "cold" "+")
int5