Anne is quiet. Bob is white. Charlie is not nice. Harry is quiet. If Charlie is cold then Charlie is not furry. If someone is white and big then they are furry. If someone is big then they are furry. If someone is white and nice then they are big. If Anne is quiet then Anne is nice. Quiet people are white. If Bob is quiet and Bob is not furry then Bob is cold. If someone is quiet and not white then they are not rough.
Anne is quiet.
("Anne" "is" "quiet" "+")
Bob is white.
("Bob" "is" "white" "+")
Charlie is not nice.
("Charlie" "is" "nice" "-")
Harry is quiet.
("Harry" "is" "quiet" "+")
If Charlie is cold then Charlie is not furry.
((("Charlie" "is" "cold" "+")) -> ("Charlie" "is" "furry" "-"))
If someone is white and big then they are furry.
((("someone" "is" "white" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "furry" "+"))
If someone is big then they are furry.
((("someone" "is" "big" "+")) -> ("someone" "is" "furry" "+"))
If someone is white and nice then they are big.
((("someone" "is" "white" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "big" "+"))
If Anne is quiet then Anne is nice.
((("Anne" "is" "quiet" "+")) -> ("Anne" "is" "nice" "+"))
Quiet people are white.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "white" "+"))
If Bob is quiet and Bob is not furry then Bob is cold.
((("Bob" "is" "quiet" "+") ("Bob" "is" "furry" "~")) -> ("Bob" "is" "cold" "+"))
If someone is quiet and not white then they are not rough.
((("someone" "is" "quiet" "+") ("someone" "is" "white" "~")) -> ("someone" "is" "rough" "-"))
Bob is white.
True
1
proof
[(triple2)]
("Bob" "is" "white" "+")
triple2
Anne is not quiet.
False
1
inv-proof
[(triple1)]
("Anne" "is" "quiet" "-")
triple1
Anne is nice.
True
2
proof
[(((triple1) -> rule5))]
("Anne" "is" "nice" "+")
((triple1) -> (rule5 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is not nice.
False
2
inv-proof
[(((triple1) -> rule5))]
("Anne" "is" "nice" "-")
((triple1) -> (rule5 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is big.
True
5
proof
[(((((triple1) -> rule6) ((triple1) -> rule5)) -> rule4))]
("Anne" "is" "big" "+")
((((triple1) -> (rule6 % int3)) ((triple1) -> (rule5 % int2))) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Anne is not big.
False
5
inv-proof
[(((((triple1) -> rule6) ((triple1) -> rule5)) -> rule4))]
("Anne" "is" "big" "-")
((((triple1) -> (rule6 % int3)) ((triple1) -> (rule5 % int2))) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Anne is furry.
True
6
proof
[(((((((triple1) -> rule6) ((triple1) -> rule5)) -> rule4)) -> rule3) OR ((((triple1) -> rule6) ((((triple1) -> rule6) ((triple1) -> rule5)) -> rule4)) -> rule2))]
("Anne" "is" "furry" "+")
((((((triple1) -> (rule6 % int4)) ((triple1) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is white.
("Anne" "is" "white" "+")
int4
((((triple1) -> (rule6 % int4)) ((((triple1) -> (rule6 % int4)) ((triple1) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is white.
("Anne" "is" "white" "+")
int4
Anne is not furry.
False
6
inv-proof
[(((((((triple1) -> rule6) ((triple1) -> rule5)) -> rule4)) -> rule3) OR ((((triple1) -> rule6) ((((triple1) -> rule6) ((triple1) -> rule5)) -> rule4)) -> rule2))]
("Anne" "is" "furry" "-")
((((((triple1) -> (rule6 % int4)) ((triple1) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is white.
("Anne" "is" "white" "+")
int4
((((triple1) -> (rule6 % int4)) ((((triple1) -> (rule6 % int4)) ((triple1) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is white.
("Anne" "is" "white" "+")
int4
Bob is not cold.
Unknown
inv-rconc
[@1: Bob is cold.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Bob" "is" "cold" "-")
Charlie is white.
Unknown
rconc
[@1: Charlie is white.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "white" "+")
Bob is not furry.
Unknown
inv-rconc
[@2: Bob is furry.[CWA. Example of deepest failure = (rule2 <- rule4 <- FAIL)]]
("Bob" "is" "furry" "-")
Harry is big.
Unknown
rconc
[@1: Harry is big.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Harry" "is" "big" "+")
Charlie is not cold.
Unknown
inv-random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "-")
Harry is cold.
Unknown
random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "+")
Bob is not quiet.
Unknown
inv-random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "-")
Harry is rough.
Unknown
random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "+")
@0: Anne is quiet.[(triple1)] Bob is white.[(triple2)] Charlie is not nice.[(triple3)] Harry is quiet.[(triple4)] @1: Anne is nice.[(((triple1) -> rule5))] Anne is white.[(((triple1) -> rule6))] Harry is white.[(((triple4) -> rule6))] @2: Anne is big.[(((((triple1) -> rule6) ((triple1) -> rule5)) -> rule4))] @3: Anne is furry.[(((((((triple1) -> rule6) ((triple1) -> rule5)) -> rule4)) -> rule3) OR ((((triple1) -> rule6) ((((triple1) -> rule6) ((triple1) -> rule5)) -> rule4)) -> rule2))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Bob is white.
("Bob" "is" "white" "+")
triple2
Charlie is not nice.
("Charlie" "is" "nice" "-")
triple3
Harry is quiet.
("Harry" "is" "quiet" "+")
triple4
Anne is nice.
("Anne" "is" "nice" "+")
((triple1) -> (rule5 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
((triple1) -> (rule6 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
((triple4) -> (rule6 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
((((triple1) -> (rule6 % int3)) ((triple1) -> (rule5 % int2))) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
((((((triple1) -> (rule6 % int4)) ((triple1) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is white.
("Anne" "is" "white" "+")
int4
((((triple1) -> (rule6 % int4)) ((((triple1) -> (rule6 % int4)) ((triple1) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is white.
("Anne" "is" "white" "+")
int4