Anne is big. Anne is red. Dave is cold. Dave is not furry. Dave is nice. Dave is rough. Dave is young. Gary is big. Gary is red. Gary is young. Nice, red people are big. If someone is rough and nice then they are cold. All rough people are nice. If someone is red then they are rough. If Gary is big then Gary is nice. If someone is furry and not red then they are young. If someone is young and not rough then they are furry. If Anne is nice and Anne is not furry then Anne is cold.
Anne is big.
("Anne" "is" "big" "+")
Anne is red.
("Anne" "is" "red" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is not furry.
("Dave" "is" "furry" "-")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is young.
("Dave" "is" "young" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is young.
("Gary" "is" "young" "+")
Nice, red people are big.
((("someone" "is" "nice" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "big" "+"))
If someone is rough and nice then they are cold.
((("someone" "is" "rough" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "cold" "+"))
All rough people are nice.
((("someone" "is" "rough" "+")) -> ("someone" "is" "nice" "+"))
If someone is red then they are rough.
((("someone" "is" "red" "+")) -> ("someone" "is" "rough" "+"))
If Gary is big then Gary is nice.
((("Gary" "is" "big" "+")) -> ("Gary" "is" "nice" "+"))
If someone is furry and not red then they are young.
((("someone" "is" "furry" "+") ("someone" "is" "red" "~")) -> ("someone" "is" "young" "+"))
If someone is young and not rough then they are furry.
((("someone" "is" "young" "+") ("someone" "is" "rough" "~")) -> ("someone" "is" "furry" "+"))
If Anne is nice and Anne is not furry then Anne is cold.
((("Anne" "is" "nice" "+") ("Anne" "is" "furry" "~")) -> ("Anne" "is" "cold" "+"))
Dave is not furry.
True
1
proof
[(triple4)]
("Dave" "is" "furry" "-")
triple4
Gary is not red.
False
1
inv-proof
[(triple9)]
("Gary" "is" "red" "-")
triple9
Gary is nice.
True
2
proof
[(((triple8) -> rule5) OR ((((triple9) -> rule4)) -> rule3))]
("Gary" "is" "nice" "+")
((triple8) -> (rule5 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
((((triple9) -> (rule4 % int2))) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Anne is not rough.
False
2
inv-proof
[(((triple2) -> rule4))]
("Anne" "is" "rough" "-")
((triple2) -> (rule4 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Gary is cold.
True
5
proof
[(((((triple9) -> rule4) ((triple8) -> rule5)) -> rule2) OR ((((triple9) -> rule4) ((((triple9) -> rule4)) -> rule3)) -> rule2))]
("Gary" "is" "cold" "+")
((((triple9) -> (rule4 % int3)) ((triple8) -> (rule5 % int2))) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
((((triple9) -> (rule4 % int3)) ((((triple9) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is not cold.
False
5
inv-proof
[(((((triple9) -> rule4) ((triple8) -> rule5)) -> rule2) OR ((((triple9) -> rule4) ((((triple9) -> rule4)) -> rule3)) -> rule2))]
("Gary" "is" "cold" "-")
((((triple9) -> (rule4 % int3)) ((triple8) -> (rule5 % int2))) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
((((triple9) -> (rule4 % int3)) ((((triple9) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Anne is cold.
True
6
proof
[(((((triple2) -> rule4) ((((triple2) -> rule4)) -> rule3)) -> rule2))]
("Anne" "is" "cold" "+")
((((triple2) -> (rule4 % int3)) ((((triple2) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Anne is not cold.
False
6
inv-proof
[(((((triple2) -> rule4) ((((triple2) -> rule4)) -> rule3)) -> rule2))]
("Anne" "is" "cold" "-")
((((triple2) -> (rule4 % int3)) ((((triple2) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Anne is not furry.
Unknown
inv-rconc
[@1: Anne is furry.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Anne" "is" "furry" "-")
Gary is furry.
Unknown
rconc
[@1: Gary is furry.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Gary" "is" "furry" "+")
Dave is not big.
Unknown
inv-rconc
[@1: Dave is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "big" "-")
Anne is young.
Unknown
rconc
[@1: Anne is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Anne" "is" "young" "+")
@0: Anne is big.[(triple1 OR ((((((triple2) -> rule4)) -> rule3) triple2) -> rule1))] Anne is red.[(triple2)] Dave is cold.[(triple3 OR ((triple6 triple5) -> rule2) OR ((triple6 ((triple6) -> rule3)) -> rule2))] Dave is nice.[(triple5 OR ((triple6) -> rule3))] Dave is not furry.[(triple4)] Dave is rough.[(triple6)] Dave is young.[(triple7)] Gary is big.[(triple8 OR ((((((triple9) -> rule4)) -> rule3) triple9) -> rule1))] Gary is red.[(triple9)] Gary is young.[(triple10)] @1: Anne is rough.[(((triple2) -> rule4))] Gary is nice.[(((triple8) -> rule5) OR ((((triple9) -> rule4)) -> rule3))] Gary is rough.[(((triple9) -> rule4))] @2: Anne is nice.[(((((triple2) -> rule4)) -> rule3))] Gary is cold.[(((((triple9) -> rule4) ((triple8) -> rule5)) -> rule2) OR ((((triple9) -> rule4) ((((triple9) -> rule4)) -> rule3)) -> rule2))] @3: Anne is cold.[(((((triple2) -> rule4) ((((triple2) -> rule4)) -> rule3)) -> rule2))]
Anne is big.
("Anne" "is" "big" "+")
triple1
((((((triple2) -> (rule4 % int3))) -> (rule3 % int2)) triple2) -> (rule1 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Anne is red.
("Anne" "is" "red" "+")
triple2
Dave is cold.
("Dave" "is" "cold" "+")
triple3
((triple6 triple5) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
((triple6 ((triple6) -> (rule3 % int2))) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
triple5
((triple6) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is not furry.
("Dave" "is" "furry" "-")
triple4
Dave is rough.
("Dave" "is" "rough" "+")
triple6
Dave is young.
("Dave" "is" "young" "+")
triple7
Gary is big.
("Gary" "is" "big" "+")
triple8
((((((triple9) -> (rule4 % int3))) -> (rule3 % int2)) triple9) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is red.
("Gary" "is" "red" "+")
triple9
Gary is young.
("Gary" "is" "young" "+")
triple10
Anne is rough.
("Anne" "is" "rough" "+")
((triple2) -> (rule4 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
((triple8) -> (rule5 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
((((triple9) -> (rule4 % int2))) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
((triple9) -> (rule4 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
((((triple2) -> (rule4 % int2))) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
((((triple9) -> (rule4 % int3)) ((triple8) -> (rule5 % int2))) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
((((triple9) -> (rule4 % int3)) ((((triple9) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Anne is cold.
("Anne" "is" "cold" "+")
((((triple2) -> (rule4 % int3)) ((((triple2) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3