Anne is not cold. Anne is nice. Anne is rough. Bob is cold. Bob is quiet. Gary is furry. Gary is nice. Gary is quiet. Gary is rough. Gary is not smart. If something is nice and not green then it is quiet. Nice, green things are quiet. Quiet things are furry. All furry, quiet things are rough. Rough, green things are not nice. All smart things are cold. If Bob is cold and Bob is rough then Bob is nice. If Anne is smart then Anne is not cold.
Anne is not cold.
("Anne" "is" "cold" "-")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is not smart.
("Gary" "is" "smart" "-")
If something is nice and not green then it is quiet.
((("something" "is" "nice" "+") ("something" "is" "green" "~")) -> ("something" "is" "quiet" "+"))
Nice, green things are quiet.
((("something" "is" "nice" "+") ("something" "is" "green" "+")) -> ("something" "is" "quiet" "+"))
Quiet things are furry.
((("something" "is" "quiet" "+")) -> ("something" "is" "furry" "+"))
All furry, quiet things are rough.
((("something" "is" "furry" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "rough" "+"))
Rough, green things are not nice.
((("something" "is" "rough" "+") ("something" "is" "green" "+")) -> ("something" "is" "nice" "-"))
All smart things are cold.
((("something" "is" "smart" "+")) -> ("something" "is" "cold" "+"))
If Bob is cold and Bob is rough then Bob is nice.
((("Bob" "is" "cold" "+") ("Bob" "is" "rough" "+")) -> ("Bob" "is" "nice" "+"))
If Anne is smart then Anne is not cold.
((("Anne" "is" "smart" "+")) -> ("Anne" "is" "cold" "-"))
Gary is rough.
True
1
proof
[(triple9 OR ((triple6 triple8) -> rule4) OR ((((triple8) -> rule3) triple8) -> rule4))]
("Gary" "is" "rough" "+")
triple9
((triple6 triple8) -> (rule4 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
((((triple8) -> (rule3 % int2)) triple8) -> (rule4 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Anne is not rough.
False
1
inv-proof
[(triple3)]
("Anne" "is" "rough" "-")
triple3
Bob is furry.
True
2
proof
[(((triple5) -> rule3))]
("Bob" "is" "furry" "+")
((triple5) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is not furry.
False
2
inv-proof
[(((triple5) -> rule3))]
("Bob" "is" "furry" "-")
((triple5) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is rough.
True
4
proof
[(((((triple5) -> rule3) triple5) -> rule4))]
("Bob" "is" "rough" "+")
((((triple5) -> (rule3 % int2)) triple5) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is not rough.
False
4
inv-proof
[(((((triple5) -> rule3) triple5) -> rule4))]
("Bob" "is" "rough" "-")
((((triple5) -> (rule3 % int2)) triple5) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is nice.
True
6
proof
[(((triple4 ((((triple5) -> rule3) triple5) -> rule4)) -> rule7))]
("Bob" "is" "nice" "+")
((triple4 ((((triple5) -> (rule3 % int3)) triple5) -> (rule4 % int2))) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is not nice.
False
6
inv-proof
[(((triple4 ((((triple5) -> rule3) triple5) -> rule4)) -> rule7))]
("Bob" "is" "nice" "-")
((triple4 ((((triple5) -> (rule3 % int3)) triple5) -> (rule4 % int2))) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Anne is not quiet.
Unknown
inv-rconc
[@1: Anne is quiet.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "quiet" "-")
Anne is furry.
Unknown
rconc
[@2: Anne is furry.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Anne" "is" "furry" "+")
Gary is not cold.
Unknown
inv-rconc
[@1: Gary is cold.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Gary" "is" "cold" "-")
Bob is smart.
Unknown
random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "+")
Bob is not green.
Unknown
inv-random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "-")
Anne is green.
Unknown
random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "+")
Gary is not green.
Unknown
inv-random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "-")
Anne is smart.
Unknown
random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "+")
@0: Anne is nice.[(triple2)] Anne is not cold.[(triple1)] Anne is rough.[(triple3)] Bob is cold.[(triple4)] Bob is quiet.[(triple5)] Gary is furry.[(triple6 OR ((triple8) -> rule3))] Gary is nice.[(triple7)] Gary is not smart.[(triple10)] Gary is quiet.[(triple8)] Gary is rough.[(triple9 OR ((triple6 triple8) -> rule4) OR ((((triple8) -> rule3) triple8) -> rule4))] @1: Bob is furry.[(((triple5) -> rule3))] @2: Bob is rough.[(((((triple5) -> rule3) triple5) -> rule4))] @3: Bob is nice.[(((triple4 ((((triple5) -> rule3) triple5) -> rule4)) -> rule7))]
Anne is nice.
("Anne" "is" "nice" "+")
triple2
Anne is not cold.
("Anne" "is" "cold" "-")
triple1
Anne is rough.
("Anne" "is" "rough" "+")
triple3
Bob is cold.
("Bob" "is" "cold" "+")
triple4
Bob is quiet.
("Bob" "is" "quiet" "+")
triple5
Gary is furry.
("Gary" "is" "furry" "+")
triple6
((triple8) -> (rule3 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
triple7
Gary is not smart.
("Gary" "is" "smart" "-")
triple10
Gary is quiet.
("Gary" "is" "quiet" "+")
triple8
Gary is rough.
("Gary" "is" "rough" "+")
triple9
((triple6 triple8) -> (rule4 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
((((triple8) -> (rule3 % int2)) triple8) -> (rule4 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
((triple5) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
((((triple5) -> (rule3 % int2)) triple5) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
((triple4 ((((triple5) -> (rule3 % int3)) triple5) -> (rule4 % int2))) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3