Bob is not furry. Charlie is quiet. Gary is cold. Gary is furry. Gary is not green. Gary is rough. Harry is cold. Quiet things are white. If something is green and white then it is furry. If something is white and furry then it is cold. All furry things are cold. If something is quiet then it is green. All white things are kind. If something is green and white then it is rough. If Bob is cold then Bob is white.
Bob is not furry.
("Bob" "is" "furry" "-")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is not green.
("Gary" "is" "green" "-")
Gary is rough.
("Gary" "is" "rough" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Quiet things are white.
((("something" "is" "quiet" "+")) -> ("something" "is" "white" "+"))
If something is green and white then it is furry.
((("something" "is" "green" "+") ("something" "is" "white" "+")) -> ("something" "is" "furry" "+"))
If something is white and furry then it is cold.
((("something" "is" "white" "+") ("something" "is" "furry" "+")) -> ("something" "is" "cold" "+"))
All furry things are cold.
((("something" "is" "furry" "+")) -> ("something" "is" "cold" "+"))
If something is quiet then it is green.
((("something" "is" "quiet" "+")) -> ("something" "is" "green" "+"))
All white things are kind.
((("something" "is" "white" "+")) -> ("something" "is" "kind" "+"))
If something is green and white then it is rough.
((("something" "is" "green" "+") ("something" "is" "white" "+")) -> ("something" "is" "rough" "+"))
If Bob is cold then Bob is white.
((("Bob" "is" "cold" "+")) -> ("Bob" "is" "white" "+"))
Gary is cold.
True
1
proof
[(triple3 OR ((triple4) -> rule4))]
("Gary" "is" "cold" "+")
triple3
((triple4) -> (rule4 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Charlie is not quiet.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "quiet" "-")
triple2
Charlie is white.
True
2
proof
[(((triple2) -> rule1))]
("Charlie" "is" "white" "+")
((triple2) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is not green.
False
2
inv-proof
[(((triple2) -> rule5))]
("Charlie" "is" "green" "-")
((triple2) -> (rule5 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is furry.
True
5
proof
[(((((triple2) -> rule5) ((triple2) -> rule1)) -> rule2))]
("Charlie" "is" "furry" "+")
((((triple2) -> (rule5 % int3)) ((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Charlie is not kind.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule6))]
("Charlie" "is" "kind" "-")
((((triple2) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is cold.
True
6
proof
[(((((((triple2) -> rule5) ((triple2) -> rule1)) -> rule2)) -> rule4) OR ((((triple2) -> rule1) ((((triple2) -> rule5) ((triple2) -> rule1)) -> rule2)) -> rule3))]
("Charlie" "is" "cold" "+")
((((((triple2) -> (rule5 % int4)) ((triple2) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Charlie is green.
("Charlie" "is" "green" "+")
int4
((((triple2) -> (rule1 % int4)) ((((triple2) -> (rule5 % int3)) ((triple2) -> (rule1 % int4))) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
int4
Charlie is not cold.
False
6
inv-proof
[(((((((triple2) -> rule5) ((triple2) -> rule1)) -> rule2)) -> rule4) OR ((((triple2) -> rule1) ((((triple2) -> rule5) ((triple2) -> rule1)) -> rule2)) -> rule3))]
("Charlie" "is" "cold" "-")
((((((triple2) -> (rule5 % int4)) ((triple2) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Charlie is green.
("Charlie" "is" "green" "+")
int4
((((triple2) -> (rule1 % int4)) ((((triple2) -> (rule5 % int3)) ((triple2) -> (rule1 % int4))) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
int4
Bob is not cold.
Unknown
inv-rconc
[@1: Bob is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "cold" "-")
Harry is kind.
Unknown
rconc
[@2: Harry is kind.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("Harry" "is" "kind" "+")
Gary is not kind.
Unknown
inv-rconc
[@2: Gary is kind.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("Gary" "is" "kind" "-")
Harry is green.
Unknown
rconc
[@1: Harry is green.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Harry" "is" "green" "+")
Gary is not quiet.
Unknown
inv-random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "-")
Bob is quiet.
Unknown
random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "+")
@0: Bob is not furry.[(triple1)] Charlie is quiet.[(triple2)] Gary is cold.[(triple3 OR ((triple4) -> rule4))] Gary is furry.[(triple4)] Gary is not green.[(triple5)] Gary is rough.[(triple6)] Harry is cold.[(triple7)] @1: Charlie is green.[(((triple2) -> rule5))] Charlie is white.[(((triple2) -> rule1))] @2: Charlie is furry.[(((((triple2) -> rule5) ((triple2) -> rule1)) -> rule2))] Charlie is kind.[(((((triple2) -> rule1)) -> rule6))] Charlie is rough.[(((((triple2) -> rule5) ((triple2) -> rule1)) -> rule7))] @3: Charlie is cold.[(((((((triple2) -> rule5) ((triple2) -> rule1)) -> rule2)) -> rule4) OR ((((triple2) -> rule1) ((((triple2) -> rule5) ((triple2) -> rule1)) -> rule2)) -> rule3))]
Bob is not furry.
("Bob" "is" "furry" "-")
triple1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple2
Gary is cold.
("Gary" "is" "cold" "+")
triple3
((triple4) -> (rule4 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
triple4
Gary is not green.
("Gary" "is" "green" "-")
triple5
Gary is rough.
("Gary" "is" "rough" "+")
triple6
Harry is cold.
("Harry" "is" "cold" "+")
triple7
Charlie is green.
("Charlie" "is" "green" "+")
((triple2) -> (rule5 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
((triple2) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
((((triple2) -> (rule5 % int3)) ((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
((((triple2) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
((((triple2) -> (rule5 % int3)) ((triple2) -> (rule1 % int2))) -> (rule7 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Charlie is cold.
("Charlie" "is" "cold" "+")
((((((triple2) -> (rule5 % int4)) ((triple2) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Charlie is green.
("Charlie" "is" "green" "+")
int4
((((triple2) -> (rule1 % int4)) ((((triple2) -> (rule5 % int3)) ((triple2) -> (rule1 % int4))) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
int4