Anne is big. Anne is kind. Anne is nice. Anne is rough. Bob is green. Bob is kind. Bob is not nice. Charlie is cold. Charlie is furry. Charlie is kind. Charlie is nice. Gary is furry. Gary is kind. Gary is not nice. Gary is rough. If something is kind and not big then it is cold. If something is kind and big then it is cold. If Gary is rough and Gary is not kind then Gary is nice. If Bob is nice then Bob is furry. If Bob is nice and Bob is big then Bob is not rough. If Anne is big and Anne is rough then Anne is furry. All furry things are rough. If something is kind and green then it is furry.
Anne is big.
("Anne" "is" "big" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is not nice.
("Bob" "is" "nice" "-")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is not nice.
("Gary" "is" "nice" "-")
Gary is rough.
("Gary" "is" "rough" "+")
If something is kind and not big then it is cold.
((("something" "is" "kind" "+") ("something" "is" "big" "~")) -> ("something" "is" "cold" "+"))
If something is kind and big then it is cold.
((("something" "is" "kind" "+") ("something" "is" "big" "+")) -> ("something" "is" "cold" "+"))
If Gary is rough and Gary is not kind then Gary is nice.
((("Gary" "is" "rough" "+") ("Gary" "is" "kind" "~")) -> ("Gary" "is" "nice" "+"))
If Bob is nice then Bob is furry.
((("Bob" "is" "nice" "+")) -> ("Bob" "is" "furry" "+"))
If Bob is nice and Bob is big then Bob is not rough.
((("Bob" "is" "nice" "+") ("Bob" "is" "big" "+")) -> ("Bob" "is" "rough" "-"))
If Anne is big and Anne is rough then Anne is furry.
((("Anne" "is" "big" "+") ("Anne" "is" "rough" "+")) -> ("Anne" "is" "furry" "+"))
All furry things are rough.
((("something" "is" "furry" "+")) -> ("something" "is" "rough" "+"))
If something is kind and green then it is furry.
((("something" "is" "kind" "+") ("something" "is" "green" "+")) -> ("something" "is" "furry" "+"))
Gary is not nice.
True
1
proof
[(triple14)]
("Gary" "is" "nice" "-")
triple14
Anne is not nice.
False
1
inv-proof
[(triple3)]
("Anne" "is" "nice" "-")
triple3
Bob is furry.
True
3
proof
[(((triple6 triple5) -> rule8))]
("Bob" "is" "furry" "+")
((triple6 triple5) -> (rule8 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Anne is not cold.
False
3
inv-proof
[(((triple2 triple1) -> rule2))]
("Anne" "is" "cold" "-")
((triple2 triple1) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Bob is rough.
True
4
proof
[(((((triple6 triple5) -> rule8)) -> rule7))]
("Bob" "is" "rough" "+")
((((triple6 triple5) -> (rule8 % int2))) -> (rule7 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is not rough.
False
4
inv-proof
[(((((triple6 triple5) -> rule8)) -> rule7))]
("Bob" "is" "rough" "-")
((((triple6 triple5) -> (rule8 % int2))) -> (rule7 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is not cold.
Unknown
inv-rconc
[@1: Bob is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "cold" "-")
Gary is cold.
Unknown
rconc
[@1: Gary is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "cold" "+")
Gary is not green.
Unknown
inv-random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "-")
Gary is big.
Unknown
random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "+")
Bob is not big.
Unknown
inv-random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "-")
Charlie is green.
Unknown
random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "+")
@0: Anne is big.[(triple1)] Anne is kind.[(triple2)] Anne is nice.[(triple3)] Anne is rough.[(triple4)] Bob is green.[(triple5)] Bob is kind.[(triple6)] Bob is not nice.[(triple7)] Charlie is cold.[(triple8)] Charlie is furry.[(triple9)] Charlie is kind.[(triple10)] Charlie is nice.[(triple11)] Gary is furry.[(triple12)] Gary is kind.[(triple13)] Gary is not nice.[(triple14)] Gary is rough.[(triple15 OR ((triple12) -> rule7))] @1: Anne is cold.[(((triple2 triple1) -> rule2))] Anne is furry.[(((triple1 triple4) -> rule6))] Bob is furry.[(((triple6 triple5) -> rule8))] Charlie is rough.[(((triple9) -> rule7))] @2: Bob is rough.[(((((triple6 triple5) -> rule8)) -> rule7))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is kind.
("Anne" "is" "kind" "+")
triple2
Anne is nice.
("Anne" "is" "nice" "+")
triple3
Anne is rough.
("Anne" "is" "rough" "+")
triple4
Bob is green.
("Bob" "is" "green" "+")
triple5
Bob is kind.
("Bob" "is" "kind" "+")
triple6
Bob is not nice.
("Bob" "is" "nice" "-")
triple7
Charlie is cold.
("Charlie" "is" "cold" "+")
triple8
Charlie is furry.
("Charlie" "is" "furry" "+")
triple9
Charlie is kind.
("Charlie" "is" "kind" "+")
triple10
Charlie is nice.
("Charlie" "is" "nice" "+")
triple11
Gary is furry.
("Gary" "is" "furry" "+")
triple12
Gary is kind.
("Gary" "is" "kind" "+")
triple13
Gary is not nice.
("Gary" "is" "nice" "-")
triple14
Gary is rough.
("Gary" "is" "rough" "+")
triple15
((triple12) -> (rule7 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
((triple2 triple1) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
((triple1 triple4) -> (rule6 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
((triple6 triple5) -> (rule8 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple9) -> (rule7 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
((((triple6 triple5) -> (rule8 % int2))) -> (rule7 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2