Charlie is not kind. Dave is red. Erin is young. Harry is kind. If someone is quiet and not kind then they are nice. If someone is quiet then they are not nice. All kind people are red. Red people are smart. If someone is red then they are quiet. Cold, kind people are quiet.
Charlie is not kind.
("Charlie" "is" "kind" "-")
Dave is red.
("Dave" "is" "red" "+")
Erin is young.
("Erin" "is" "young" "+")
Harry is kind.
("Harry" "is" "kind" "+")
If someone is quiet and not kind then they are nice.
((("someone" "is" "quiet" "+") ("someone" "is" "kind" "~")) -> ("someone" "is" "nice" "+"))
If someone is quiet then they are not nice.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "nice" "-"))
All kind people are red.
((("someone" "is" "kind" "+")) -> ("someone" "is" "red" "+"))
Red people are smart.
((("someone" "is" "red" "+")) -> ("someone" "is" "smart" "+"))
If someone is red then they are quiet.
((("someone" "is" "red" "+")) -> ("someone" "is" "quiet" "+"))
Cold, kind people are quiet.
((("someone" "is" "cold" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "quiet" "+"))
Harry is kind.
True
1
proof
[(triple4)]
("Harry" "is" "kind" "+")
triple4
Dave is not red.
False
1
inv-proof
[(triple2)]
("Dave" "is" "red" "-")
triple2
Harry is red.
True
2
proof
[(((triple4) -> rule3))]
("Harry" "is" "red" "+")
((triple4) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Dave is not quiet.
False
2
inv-proof
[(((triple2) -> rule5))]
("Dave" "is" "quiet" "-")
((triple2) -> (rule5 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Harry is smart.
True
3
proof
[(((((triple4) -> rule3)) -> rule4))]
("Harry" "is" "smart" "+")
((((triple4) -> (rule3 % int2))) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Dave is nice.
False
3
inv-proof
[(((((triple2) -> rule5)) -> rule2))]
("Dave" "is" "nice" "+")
((((triple2) -> (rule5 % int2))) -> (rule2 % int1))
Dave is not nice.
("Dave" "is" "nice" "-")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Harry is not nice.
True
4
proof
[(((((((triple4) -> rule3)) -> rule5)) -> rule2))]
("Harry" "is" "nice" "-")
((((((triple4) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Harry is not nice.
("Harry" "is" "nice" "-")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Harry is nice.
False
4
inv-proof
[(((((((triple4) -> rule3)) -> rule5)) -> rule2))]
("Harry" "is" "nice" "+")
((((((triple4) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Harry is not nice.
("Harry" "is" "nice" "-")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Erin is not smart.
Unknown
inv-rconc
[@2: Erin is smart.[CWA. Example of deepest failure = (rule4 <- rule3 <- FAIL)]]
("Erin" "is" "smart" "-")
Charlie is nice.
Unknown
rconc
[@1: Charlie is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "nice" "+")
Erin is not nice.
Unknown
inv-rconc
[@1: Erin is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "nice" "-")
Erin is red.
Unknown
rconc
[@1: Erin is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "red" "+")
Harry is not cold.
Unknown
inv-random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "-")
Erin is kind.
Unknown
random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "+")
Dave is not cold.
Unknown
inv-random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "-")
Charlie is young.
Unknown
random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "+")
@0: Charlie is not kind.[(triple1)] Dave is red.[(triple2)] Erin is young.[(triple3)] Harry is kind.[(triple4)] @1: Dave is quiet.[(((triple2) -> rule5))] Dave is smart.[(((triple2) -> rule4))] Harry is red.[(((triple4) -> rule3))] @2: Dave is not nice.[(((((triple2) -> rule5)) -> rule2))] Harry is quiet.[(((((triple4) -> rule3)) -> rule5))] Harry is smart.[(((((triple4) -> rule3)) -> rule4))] @3: Harry is not nice.[(((((((triple4) -> rule3)) -> rule5)) -> rule2))]
Charlie is not kind.
("Charlie" "is" "kind" "-")
triple1
Dave is red.
("Dave" "is" "red" "+")
triple2
Erin is young.
("Erin" "is" "young" "+")
triple3
Harry is kind.
("Harry" "is" "kind" "+")
triple4
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple2) -> (rule5 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
((triple2) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
((triple4) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Dave is not nice.
("Dave" "is" "nice" "-")
((((triple2) -> (rule5 % int2))) -> (rule2 % int1))
Dave is not nice.
("Dave" "is" "nice" "-")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
((((triple4) -> (rule3 % int2))) -> (rule5 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
((((triple4) -> (rule3 % int2))) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is not nice.
("Harry" "is" "nice" "-")
((((((triple4) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Harry is not nice.
("Harry" "is" "nice" "-")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3