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