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