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