Bob is not cold. Bob is kind. Bob is red. Charlie is cold. Charlie is kind. Dave is rough. Gary is kind. If someone is white then they are rough. Furry people are red. All rough people are white. If Gary is white then Gary is red. If Charlie is cold then Charlie is white. If Gary is kind then Gary is rough. If someone is rough and cold then they are furry. If someone is furry and not white then they are not nice.
Bob is not cold.
("Bob" "is" "cold" "-")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is red.
("Bob" "is" "red" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Gary is kind.
("Gary" "is" "kind" "+")
If someone is white then they are rough.
((("someone" "is" "white" "+")) -> ("someone" "is" "rough" "+"))
Furry people are red.
((("someone" "is" "furry" "+")) -> ("someone" "is" "red" "+"))
All rough people are white.
((("someone" "is" "rough" "+")) -> ("someone" "is" "white" "+"))
If Gary is white then Gary is red.
((("Gary" "is" "white" "+")) -> ("Gary" "is" "red" "+"))
If Charlie is cold then Charlie is white.
((("Charlie" "is" "cold" "+")) -> ("Charlie" "is" "white" "+"))
If Gary is kind then Gary is rough.
((("Gary" "is" "kind" "+")) -> ("Gary" "is" "rough" "+"))
If someone is rough and cold then they are furry.
((("someone" "is" "rough" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "furry" "+"))
If someone is furry and not white then they are not nice.
((("someone" "is" "furry" "+") ("someone" "is" "white" "~")) -> ("someone" "is" "nice" "-"))
Bob is kind.
True
1
proof
[(triple2)]
("Bob" "is" "kind" "+")
triple2
Charlie is not cold.
False
1
inv-proof
[(triple4)]
("Charlie" "is" "cold" "-")
triple4
Charlie is white.
True
2
proof
[(((triple4) -> rule5))]
("Charlie" "is" "white" "+")
((triple4) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Gary is not rough.
False
2
inv-proof
[(((triple7) -> rule6))]
("Gary" "is" "rough" "-")
((triple7) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Charlie is rough.
True
3
proof
[(((((triple4) -> rule5)) -> rule1))]
("Charlie" "is" "rough" "+")
((((triple4) -> (rule5 % int2))) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Gary is not white.
False
3
inv-proof
[(((((triple7) -> rule6)) -> rule3))]
("Gary" "is" "white" "-")
((((triple7) -> (rule6 % int2))) -> (rule3 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Charlie is furry.
True
5
proof
[(((((((triple4) -> rule5)) -> rule1) triple4) -> rule7))]
("Charlie" "is" "furry" "+")
((((((triple4) -> (rule5 % int3))) -> (rule1 % int2)) triple4) -> (rule7 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Charlie is not furry.
False
5
inv-proof
[(((((((triple4) -> rule5)) -> rule1) triple4) -> rule7))]
("Charlie" "is" "furry" "-")
((((((triple4) -> (rule5 % int3))) -> (rule1 % int2)) triple4) -> (rule7 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Bob is not rough.
Unknown
inv-rconc
[@2: Bob is rough.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Bob" "is" "rough" "-")
Gary is furry.
Unknown
rconc
[@1: Gary is furry.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Gary" "is" "furry" "+")
Bob is not furry.
Unknown
inv-rconc
[@1: Bob is furry.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Bob" "is" "furry" "-")
Dave is red.
Unknown
rconc
[@2: Dave is red.[CWA. Example of deepest failure = (rule2 <- rule7 <- FAIL)]]
("Dave" "is" "red" "+")
Charlie is not nice.
Unknown
inv-random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "-")
Bob is nice.
Unknown
random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "+")
Dave is not nice.
Unknown
inv-random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "-")
Dave is kind.
Unknown
random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "+")
@0: Bob is kind.[(triple2)] Bob is not cold.[(triple1)] Bob is red.[(triple3)] Charlie is cold.[(triple4)] Charlie is kind.[(triple5)] Dave is rough.[(triple6)] Gary is kind.[(triple7)] @1: Charlie is white.[(((triple4) -> rule5))] Dave is white.[(((triple6) -> rule3))] Gary is rough.[(((triple7) -> rule6))] @2: Charlie is rough.[(((((triple4) -> rule5)) -> rule1))] Gary is white.[(((((triple7) -> rule6)) -> rule3))] @3: Charlie is furry.[(((((((triple4) -> rule5)) -> rule1) triple4) -> rule7))] Gary is red.[(((((((triple7) -> rule6)) -> rule3)) -> rule4))] @4: Charlie is red.[(((((((((triple4) -> rule5)) -> rule1) triple4) -> rule7)) -> rule2))]
Bob is kind.
("Bob" "is" "kind" "+")
triple2
Bob is not cold.
("Bob" "is" "cold" "-")
triple1
Bob is red.
("Bob" "is" "red" "+")
triple3
Charlie is cold.
("Charlie" "is" "cold" "+")
triple4
Charlie is kind.
("Charlie" "is" "kind" "+")
triple5
Dave is rough.
("Dave" "is" "rough" "+")
triple6
Gary is kind.
("Gary" "is" "kind" "+")
triple7
Charlie is white.
("Charlie" "is" "white" "+")
((triple4) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
((triple6) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
((triple7) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
((((triple4) -> (rule5 % int2))) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
((((triple7) -> (rule6 % int2))) -> (rule3 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
((((((triple4) -> (rule5 % int3))) -> (rule1 % int2)) triple4) -> (rule7 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Gary is red.
("Gary" "is" "red" "+")
((((((triple7) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Charlie is red.
("Charlie" "is" "red" "+")
((((((((triple4) -> (rule5 % int4))) -> (rule1 % int3)) triple4) -> (rule7 % int2))) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
int4