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