Anne is big. Anne is nice. Bob is round. Charlie is nice. Charlie is not round. Charlie is young. Gary is not big. Gary is furry. Gary is not round. Gary is young. All cold people are kind. If someone is cold and not young then they are furry. All nice, kind people are furry. If someone is kind then they are big. If someone is kind and nice then they are big. Round people are cold.
Anne is big.
("Anne" "is" "big" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Bob is round.
("Bob" "is" "round" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is not round.
("Charlie" "is" "round" "-")
Charlie is young.
("Charlie" "is" "young" "+")
Gary is not big.
("Gary" "is" "big" "-")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is not round.
("Gary" "is" "round" "-")
Gary is young.
("Gary" "is" "young" "+")
All cold people are kind.
((("someone" "is" "cold" "+")) -> ("someone" "is" "kind" "+"))
If someone is cold and not young then they are furry.
((("someone" "is" "cold" "+") ("someone" "is" "young" "~")) -> ("someone" "is" "furry" "+"))
All nice, kind people are furry.
((("someone" "is" "nice" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "furry" "+"))
If someone is kind then they are big.
((("someone" "is" "kind" "+")) -> ("someone" "is" "big" "+"))
If someone is kind and nice then they are big.
((("someone" "is" "kind" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "big" "+"))
Round people are cold.
((("someone" "is" "round" "+")) -> ("someone" "is" "cold" "+"))
Charlie is young.
True
1
proof
[(triple6)]
("Charlie" "is" "young" "+")
triple6
Gary is round.
False
1
inv-proof
[(triple9)]
("Gary" "is" "round" "+")
triple9
Bob is cold.
True
2
proof
[(((triple3) -> rule6))]
("Bob" "is" "cold" "+")
((triple3) -> (rule6 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is not cold.
False
2
inv-proof
[(((triple3) -> rule6))]
("Bob" "is" "cold" "-")
((triple3) -> (rule6 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is kind.
True
3
proof
[(((((triple3) -> rule6)) -> rule1))]
("Bob" "is" "kind" "+")
((((triple3) -> (rule6 % int2))) -> (rule1 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is not kind.
False
3
inv-proof
[(((((triple3) -> rule6)) -> rule1))]
("Bob" "is" "kind" "-")
((((triple3) -> (rule6 % int2))) -> (rule1 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is big.
True
4
proof
[(((((((triple3) -> rule6)) -> rule1)) -> rule4))]
("Bob" "is" "big" "+")
((((((triple3) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Bob is not big.
False
4
inv-proof
[(((((((triple3) -> rule6)) -> rule1)) -> rule4))]
("Bob" "is" "big" "-")
((((((triple3) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Charlie is not big.
Unknown
inv-rconc
[@3: Charlie is big.[CWA. Example of deepest failure = (rule4 <- rule1 <- rule6 <- FAIL)]]
("Charlie" "is" "big" "-")
Charlie is cold.
Unknown
rconc
[@1: Charlie is cold.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "cold" "+")
Anne is not kind.
Unknown
inv-rconc
[@2: Anne is kind.[CWA. Example of deepest failure = (rule1 <- rule6 <- FAIL)]]
("Anne" "is" "kind" "-")
Charlie is kind.
Unknown
rconc
[@2: Charlie is kind.[CWA. Example of deepest failure = (rule1 <- rule6 <- FAIL)]]
("Charlie" "is" "kind" "+")
Gary is not nice.
Unknown
inv-random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "-")
Bob is young.
Unknown
random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "+")
Anne is not round.
Unknown
inv-random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "-")
Anne is young.
Unknown
random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "+")
@0: Anne is big.[(triple1)] Anne is nice.[(triple2)] Bob is round.[(triple3)] Charlie is nice.[(triple4)] Charlie is not round.[(triple5)] Charlie is young.[(triple6)] Gary is furry.[(triple8)] Gary is not big.[(triple7)] Gary is not round.[(triple9)] Gary is young.[(triple10)] @1: Bob is cold.[(((triple3) -> rule6))] @2: Bob is kind.[(((((triple3) -> rule6)) -> rule1))] @3: Bob is big.[(((((((triple3) -> rule6)) -> rule1)) -> rule4))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is nice.
("Anne" "is" "nice" "+")
triple2
Bob is round.
("Bob" "is" "round" "+")
triple3
Charlie is nice.
("Charlie" "is" "nice" "+")
triple4
Charlie is not round.
("Charlie" "is" "round" "-")
triple5
Charlie is young.
("Charlie" "is" "young" "+")
triple6
Gary is furry.
("Gary" "is" "furry" "+")
triple8
Gary is not big.
("Gary" "is" "big" "-")
triple7
Gary is not round.
("Gary" "is" "round" "-")
triple9
Gary is young.
("Gary" "is" "young" "+")
triple10
Bob is cold.
("Bob" "is" "cold" "+")
((triple3) -> (rule6 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
((((triple3) -> (rule6 % int2))) -> (rule1 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
((((((triple3) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3