Charlie is red. Erin is white. Erin is young. Gary is quiet. Gary is white. Harry is nice. Harry is quiet. If Erin is red then Erin is white. If Erin is quiet then Erin is nice. Kind, young things are nice. If Harry is kind then Harry is white. If Charlie is nice and Charlie is blue then Charlie is young. If something is young and white then it is kind. Nice things are quiet. All blue, white things are nice.
Charlie is red.
("Charlie" "is" "red" "+")
Erin is white.
("Erin" "is" "white" "+")
Erin is young.
("Erin" "is" "young" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is white.
("Gary" "is" "white" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
If Erin is red then Erin is white.
((("Erin" "is" "red" "+")) -> ("Erin" "is" "white" "+"))
If Erin is quiet then Erin is nice.
((("Erin" "is" "quiet" "+")) -> ("Erin" "is" "nice" "+"))
Kind, young things are nice.
((("something" "is" "kind" "+") ("something" "is" "young" "+")) -> ("something" "is" "nice" "+"))
If Harry is kind then Harry is white.
((("Harry" "is" "kind" "+")) -> ("Harry" "is" "white" "+"))
If Charlie is nice and Charlie is blue then Charlie is young.
((("Charlie" "is" "nice" "+") ("Charlie" "is" "blue" "+")) -> ("Charlie" "is" "young" "+"))
If something is young and white then it is kind.
((("something" "is" "young" "+") ("something" "is" "white" "+")) -> ("something" "is" "kind" "+"))
Nice things are quiet.
((("something" "is" "nice" "+")) -> ("something" "is" "quiet" "+"))
All blue, white things are nice.
((("something" "is" "blue" "+") ("something" "is" "white" "+")) -> ("something" "is" "nice" "+"))
Harry is quiet.
True
1
proof
[(triple7 OR ((triple6) -> rule7))]
("Harry" "is" "quiet" "+")
triple7
((triple6) -> (rule7 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Erin is not white.
False
1
inv-proof
[(triple2)]
("Erin" "is" "white" "-")
triple2
Erin is kind.
True
3
proof
[(((triple3 triple2) -> rule6))]
("Erin" "is" "kind" "+")
((triple3 triple2) -> (rule6 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is not kind.
False
3
inv-proof
[(((triple3 triple2) -> rule6))]
("Erin" "is" "kind" "-")
((triple3 triple2) -> (rule6 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is nice.
True
5
proof
[(((((triple3 triple2) -> rule6) triple3) -> rule3))]
("Erin" "is" "nice" "+")
((((triple3 triple2) -> (rule6 % int2)) triple3) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is not nice.
False
5
inv-proof
[(((((triple3 triple2) -> rule6) triple3) -> rule3))]
("Erin" "is" "nice" "-")
((((triple3 triple2) -> (rule6 % int2)) triple3) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is quiet.
True
6
proof
[(((((((triple3 triple2) -> rule6) triple3) -> rule3)) -> rule7))]
("Erin" "is" "quiet" "+")
((((((triple3 triple2) -> (rule6 % int3)) triple3) -> (rule3 % int2))) -> (rule7 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is not quiet.
False
6
inv-proof
[(((((((triple3 triple2) -> rule6) triple3) -> rule3)) -> rule7))]
("Erin" "is" "quiet" "-")
((((((triple3 triple2) -> (rule6 % int3)) triple3) -> (rule3 % int2))) -> (rule7 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Charlie is not nice.
Unknown
inv-rconc
[@2: Charlie is nice.[CWA. Example of deepest failure = (rule3 <- rule6 <- FAIL)]]
("Charlie" "is" "nice" "-")
Charlie is kind.
Unknown
rconc
[@1: Charlie is kind.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "kind" "+")
Gary is not kind.
Unknown
inv-rconc
[@1: Gary is kind.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Gary" "is" "kind" "-")
Charlie is quiet.
Unknown
rconc
[@3: Charlie is quiet.[CWA. Example of deepest failure = (rule7 <- rule3 <- rule6 <- FAIL)]]
("Charlie" "is" "quiet" "+")
Erin is not blue.
Unknown
inv-random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "-")
Gary is blue.
Unknown
random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "+")
Erin is not red.
Unknown
inv-random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "-")
Harry is young.
Unknown
random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "+")
@0: Charlie is red.[(triple1)] Erin is white.[(triple2)] Erin is young.[(triple3)] Gary is quiet.[(triple4)] Gary is white.[(triple5)] Harry is nice.[(triple6)] Harry is quiet.[(triple7 OR ((triple6) -> rule7))] @1: Erin is kind.[(((triple3 triple2) -> rule6))] @2: Erin is nice.[(((((triple3 triple2) -> rule6) triple3) -> rule3))] @3: Erin is quiet.[(((((((triple3 triple2) -> rule6) triple3) -> rule3)) -> rule7))]
Charlie is red.
("Charlie" "is" "red" "+")
triple1
Erin is white.
("Erin" "is" "white" "+")
triple2
Erin is young.
("Erin" "is" "young" "+")
triple3
Gary is quiet.
("Gary" "is" "quiet" "+")
triple4
Gary is white.
("Gary" "is" "white" "+")
triple5
Harry is nice.
("Harry" "is" "nice" "+")
triple6
Harry is quiet.
("Harry" "is" "quiet" "+")
triple7
((triple6) -> (rule7 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
((triple3 triple2) -> (rule6 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
((((triple3 triple2) -> (rule6 % int2)) triple3) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
((((((triple3 triple2) -> (rule6 % int3)) triple3) -> (rule3 % int2))) -> (rule7 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3