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