Erin is blue. Erin is green. Erin is nice. Erin is quiet. Harry is green. Harry is red. Harry is smart. White, blue things are nice. If something is red and blue then it is white. All red, green things are blue.
Erin is blue.
("Erin" "is" "blue" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is smart.
("Harry" "is" "smart" "+")
White, blue things are nice.
((("something" "is" "white" "+") ("something" "is" "blue" "+")) -> ("something" "is" "nice" "+"))
If something is red and blue then it is white.
((("something" "is" "red" "+") ("something" "is" "blue" "+")) -> ("something" "is" "white" "+"))
All red, green things are blue.
((("something" "is" "red" "+") ("something" "is" "green" "+")) -> ("something" "is" "blue" "+"))
Erin is green.
True
1
proof
[(triple2)]
("Erin" "is" "green" "+")
triple2
Harry is not red.
False
1
inv-proof
[(triple6)]
("Harry" "is" "red" "-")
triple6
Harry is blue.
True
3
proof
[(((triple6 triple5) -> rule3))]
("Harry" "is" "blue" "+")
((triple6 triple5) -> (rule3 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is not blue.
False
3
inv-proof
[(((triple6 triple5) -> rule3))]
("Harry" "is" "blue" "-")
((triple6 triple5) -> (rule3 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is white.
True
5
proof
[(((triple6 ((triple6 triple5) -> rule3)) -> rule2))]
("Harry" "is" "white" "+")
((triple6 ((triple6 triple5) -> (rule3 % int2))) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is not white.
False
5
inv-proof
[(((triple6 ((triple6 triple5) -> rule3)) -> rule2))]
("Harry" "is" "white" "-")
((triple6 ((triple6 triple5) -> (rule3 % int2))) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is nice.
True
9
proof
[(((((triple6 ((triple6 triple5) -> rule3)) -> rule2) ((triple6 triple5) -> rule3)) -> rule1))]
("Harry" "is" "nice" "+")
((((triple6 ((triple6 triple5) -> (rule3 % int3))) -> (rule2 % int2)) ((triple6 triple5) -> (rule3 % int3))) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is not nice.
False
9
inv-proof
[(((((triple6 ((triple6 triple5) -> rule3)) -> rule2) ((triple6 triple5) -> rule3)) -> rule1))]
("Harry" "is" "nice" "-")
((((triple6 ((triple6 triple5) -> (rule3 % int3))) -> (rule2 % int2)) ((triple6 triple5) -> (rule3 % int3))) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Erin is not white.
Unknown
inv-rconc
[@1: Erin is white.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "white" "-")
Erin is red.
Unknown
random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "+")
Erin is not smart.
Unknown
inv-random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "-")
Harry is quiet.
Unknown
random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "+")
@0: Erin is blue.[(triple1)] Erin is green.[(triple2)] Erin is nice.[(triple3)] Erin is quiet.[(triple4)] Harry is green.[(triple5)] Harry is red.[(triple6)] Harry is smart.[(triple7)] @1: Harry is blue.[(((triple6 triple5) -> rule3))] @2: Harry is white.[(((triple6 ((triple6 triple5) -> rule3)) -> rule2))] @3: Harry is nice.[(((((triple6 ((triple6 triple5) -> rule3)) -> rule2) ((triple6 triple5) -> rule3)) -> rule1))]
Erin is blue.
("Erin" "is" "blue" "+")
triple1
Erin is green.
("Erin" "is" "green" "+")
triple2
Erin is nice.
("Erin" "is" "nice" "+")
triple3
Erin is quiet.
("Erin" "is" "quiet" "+")
triple4
Harry is green.
("Harry" "is" "green" "+")
triple5
Harry is red.
("Harry" "is" "red" "+")
triple6
Harry is smart.
("Harry" "is" "smart" "+")
triple7
Harry is blue.
("Harry" "is" "blue" "+")
((triple6 triple5) -> (rule3 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
((triple6 ((triple6 triple5) -> (rule3 % int2))) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
((((triple6 ((triple6 triple5) -> (rule3 % int3))) -> (rule2 % int2)) ((triple6 triple5) -> (rule3 % int3))) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3