Anne is not cold. Anne is rough. Dave is furry. Dave is round. Gary is red. Gary is round. Harry is cold. Harry is not furry. Harry is kind. Harry is round. If Gary is big then Gary is cold. If Dave is not cold then Dave is furry. If Harry is big then Harry is kind. Rough people are big. If Anne is rough then Anne is round. If Gary is cold and Gary is big then Gary is rough. If Gary is cold then Gary is furry. If someone is red then they are rough. If someone is furry then they are not kind.
Anne is not cold.
("Anne" "is" "cold" "-")
Anne is rough.
("Anne" "is" "rough" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is round.
("Dave" "is" "round" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is round.
("Gary" "is" "round" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is not furry.
("Harry" "is" "furry" "-")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is round.
("Harry" "is" "round" "+")
If Gary is big then Gary is cold.
((("Gary" "is" "big" "+")) -> ("Gary" "is" "cold" "+"))
If Dave is not cold then Dave is furry.
((("Dave" "is" "cold" "~")) -> ("Dave" "is" "furry" "+"))
If Harry is big then Harry is kind.
((("Harry" "is" "big" "+")) -> ("Harry" "is" "kind" "+"))
Rough people are big.
((("someone" "is" "rough" "+")) -> ("someone" "is" "big" "+"))
If Anne is rough then Anne is round.
((("Anne" "is" "rough" "+")) -> ("Anne" "is" "round" "+"))
If Gary is cold and Gary is big then Gary is rough.
((("Gary" "is" "cold" "+") ("Gary" "is" "big" "+")) -> ("Gary" "is" "rough" "+"))
If Gary is cold then Gary is furry.
((("Gary" "is" "cold" "+")) -> ("Gary" "is" "furry" "+"))
If someone is red then they are rough.
((("someone" "is" "red" "+")) -> ("someone" "is" "rough" "+"))
If someone is furry then they are not kind.
((("someone" "is" "furry" "+")) -> ("someone" "is" "kind" "-"))
Harry is kind.
True
1
proof
[(triple9)]
("Harry" "is" "kind" "+")
triple9
Harry is not cold.
False
1
inv-proof
[(triple7)]
("Harry" "is" "cold" "-")
triple7
Anne is round.
True
2
proof
[(((triple2) -> rule5))]
("Anne" "is" "round" "+")
((triple2) -> (rule5 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Dave is kind.
False
2
inv-proof
[(((triple3) -> rule9))]
("Dave" "is" "kind" "+")
((triple3) -> (rule9 % int1))
Dave is not kind.
("Dave" "is" "kind" "-")
int1
Gary is big.
True
3
proof
[(((((triple5) -> rule8)) -> rule4))]
("Gary" "is" "big" "+")
((((triple5) -> (rule8 % int2))) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is not big.
False
3
inv-proof
[(((((triple5) -> rule8)) -> rule4))]
("Gary" "is" "big" "-")
((((triple5) -> (rule8 % int2))) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is cold.
True
4
proof
[(((((((triple5) -> rule8)) -> rule4)) -> rule1))]
("Gary" "is" "cold" "+")
((((((triple5) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is not cold.
False
4
inv-proof
[(((((((triple5) -> rule8)) -> rule4)) -> rule1))]
("Gary" "is" "cold" "-")
((((((triple5) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is furry.
True
5
proof
[(((((((((triple5) -> rule8)) -> rule4)) -> rule1)) -> rule7))]
("Gary" "is" "furry" "+")
((((((((triple5) -> (rule8 % int4))) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Gary is rough.
("Gary" "is" "rough" "+")
int4
Gary is not furry.
False
5
inv-proof
[(((((((((triple5) -> rule8)) -> rule4)) -> rule1)) -> rule7))]
("Gary" "is" "furry" "-")
((((((((triple5) -> (rule8 % int4))) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Gary is rough.
("Gary" "is" "rough" "+")
int4
Gary is not kind.
True
6
proof
[(((((((((((triple5) -> rule8)) -> rule4)) -> rule1)) -> rule7)) -> rule9))]
("Gary" "is" "kind" "-")
((((((((((triple5) -> (rule8 % int5))) -> (rule4 % int4))) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule9 % int1))
Gary is not kind.
("Gary" "is" "kind" "-")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
int4
Gary is rough.
("Gary" "is" "rough" "+")
int5
Gary is kind.
False
6
inv-proof
[(((((((((((triple5) -> rule8)) -> rule4)) -> rule1)) -> rule7)) -> rule9))]
("Gary" "is" "kind" "+")
((((((((((triple5) -> (rule8 % int5))) -> (rule4 % int4))) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule9 % int1))
Gary is not kind.
("Gary" "is" "kind" "-")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
int4
Gary is rough.
("Gary" "is" "rough" "+")
int5
Dave is not rough.
Unknown
inv-rconc
[@1: Dave is rough.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Dave" "is" "rough" "-")
Dave is big.
Unknown
rconc
[@2: Dave is big.[CWA. Example of deepest failure = (rule4 <- rule8 <- FAIL)]]
("Dave" "is" "big" "+")
Harry is not rough.
Unknown
inv-rconc
[@1: Harry is rough.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Harry" "is" "rough" "-")
Harry is big.
Unknown
rconc
[@2: Harry is big.[CWA. Example of deepest failure = (rule4 <- rule8 <- FAIL)]]
("Harry" "is" "big" "+")
Dave is not red.
Unknown
inv-random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "-")
Harry is red.
Unknown
random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "+")
Anne is not kind.
Unknown
inv-random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "-")
Anne is furry.
Unknown
random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "+")
Anne is not red.
Unknown
inv-random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "-")
Dave is cold.
Unknown
random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "+")
@0: Anne is not cold.[(triple1)] Anne is rough.[(triple2)] Dave is furry.[(triple3)] Dave is round.[(triple4)] Gary is red.[(triple5)] Gary is round.[(triple6)] Harry is cold.[(triple7)] Harry is kind.[(triple9)] Harry is not furry.[(triple8)] Harry is round.[(triple10)] @1: Anne is big.[(((triple2) -> rule4))] Anne is round.[(((triple2) -> rule5))] Dave is not kind.[(((triple3) -> rule9))] Gary is rough.[(((triple5) -> rule8))] @2: Gary is big.[(((((triple5) -> rule8)) -> rule4))] @3: Gary is cold.[(((((((triple5) -> rule8)) -> rule4)) -> rule1))] @4: Gary is furry.[(((((((((triple5) -> rule8)) -> rule4)) -> rule1)) -> rule7))] @5: Gary is not kind.[(((((((((((triple5) -> rule8)) -> rule4)) -> rule1)) -> rule7)) -> rule9))]
Anne is not cold.
("Anne" "is" "cold" "-")
triple1
Anne is rough.
("Anne" "is" "rough" "+")
triple2
Dave is furry.
("Dave" "is" "furry" "+")
triple3
Dave is round.
("Dave" "is" "round" "+")
triple4
Gary is red.
("Gary" "is" "red" "+")
triple5
Gary is round.
("Gary" "is" "round" "+")
triple6
Harry is cold.
("Harry" "is" "cold" "+")
triple7
Harry is kind.
("Harry" "is" "kind" "+")
triple9
Harry is not furry.
("Harry" "is" "furry" "-")
triple8
Harry is round.
("Harry" "is" "round" "+")
triple10
Anne is big.
("Anne" "is" "big" "+")
((triple2) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
((triple2) -> (rule5 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Dave is not kind.
("Dave" "is" "kind" "-")
((triple3) -> (rule9 % int1))
Dave is not kind.
("Dave" "is" "kind" "-")
int1
Gary is rough.
("Gary" "is" "rough" "+")
((triple5) -> (rule8 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
((((triple5) -> (rule8 % int2))) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
((((((triple5) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is furry.
("Gary" "is" "furry" "+")
((((((((triple5) -> (rule8 % int4))) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Gary is rough.
("Gary" "is" "rough" "+")
int4
Gary is not kind.
("Gary" "is" "kind" "-")
((((((((((triple5) -> (rule8 % int5))) -> (rule4 % int4))) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule9 % int1))
Gary is not kind.
("Gary" "is" "kind" "-")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
int4
Gary is rough.
("Gary" "is" "rough" "+")
int5