Erin is kind. Erin is nice. Fiona is green. Fiona is kind. Gary is kind. Gary is not nice. Harry is kind. If Harry is nice then Harry is blue. If someone is kind and white then they are quiet. If someone is white then they are kind. If Gary is white then Gary is quiet. If Fiona is quiet and Fiona is white then Fiona is green. All nice people are white. All kind people are white. Quiet, blue people are red. If Harry is quiet then Harry is nice.
Erin is kind.
("Erin" "is" "kind" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is not nice.
("Gary" "is" "nice" "-")
Harry is kind.
("Harry" "is" "kind" "+")
If Harry is nice then Harry is blue.
((("Harry" "is" "nice" "+")) -> ("Harry" "is" "blue" "+"))
If someone is kind and white then they are quiet.
((("someone" "is" "kind" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "quiet" "+"))
If someone is white then they are kind.
((("someone" "is" "white" "+")) -> ("someone" "is" "kind" "+"))
If Gary is white then Gary is quiet.
((("Gary" "is" "white" "+")) -> ("Gary" "is" "quiet" "+"))
If Fiona is quiet and Fiona is white then Fiona is green.
((("Fiona" "is" "quiet" "+") ("Fiona" "is" "white" "+")) -> ("Fiona" "is" "green" "+"))
All nice people are white.
((("someone" "is" "nice" "+")) -> ("someone" "is" "white" "+"))
All kind people are white.
((("someone" "is" "kind" "+")) -> ("someone" "is" "white" "+"))
Quiet, blue people are red.
((("someone" "is" "quiet" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "red" "+"))
If Harry is quiet then Harry is nice.
((("Harry" "is" "quiet" "+")) -> ("Harry" "is" "nice" "+"))
Harry is kind.
True
1
proof
[(triple7)]
("Harry" "is" "kind" "+")
triple7
Fiona is not green.
False
1
inv-proof
[(triple3 OR ((((triple4 ((triple4) -> rule7)) -> rule2) ((triple4) -> rule7)) -> rule5))]
("Fiona" "is" "green" "-")
triple3
((((triple4 ((triple4) -> (rule7 % int3))) -> (rule2 % int2)) ((triple4) -> (rule7 % int3))) -> (rule5 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
int3
Erin is white.
True
2
proof
[(((triple1) -> rule7) OR ((triple2) -> rule6))]
("Erin" "is" "white" "+")
((triple1) -> (rule7 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((triple2) -> (rule6 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is not white.
False
2
inv-proof
[(((triple1) -> rule7) OR ((triple2) -> rule6))]
("Erin" "is" "white" "-")
((triple1) -> (rule7 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((triple2) -> (rule6 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Gary is quiet.
True
3
proof
[(((((triple5) -> rule7)) -> rule4) OR ((triple5 ((triple5) -> rule7)) -> rule2))]
("Gary" "is" "quiet" "+")
((((triple5) -> (rule7 % int2))) -> (rule4 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
((triple5 ((triple5) -> (rule7 % int2))) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is not quiet.
False
3
inv-proof
[(((((triple5) -> rule7)) -> rule4) OR ((triple5 ((triple5) -> rule7)) -> rule2))]
("Gary" "is" "quiet" "-")
((((triple5) -> (rule7 % int2))) -> (rule4 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
((triple5 ((triple5) -> (rule7 % int2))) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Harry is nice.
True
5
proof
[(((((triple7 ((triple7) -> rule7)) -> rule2)) -> rule9))]
("Harry" "is" "nice" "+")
((((triple7 ((triple7) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule9 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is not nice.
False
5
inv-proof
[(((((triple7 ((triple7) -> rule7)) -> rule2)) -> rule9))]
("Harry" "is" "nice" "-")
((((triple7 ((triple7) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule9 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is blue.
True
6
proof
[(((((((triple7 ((triple7) -> rule7)) -> rule2)) -> rule9)) -> rule1))]
("Harry" "is" "blue" "+")
((((((triple7 ((triple7) -> (rule7 % int4))) -> (rule2 % int3))) -> (rule9 % int2))) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is white.
("Harry" "is" "white" "+")
int4
Harry is not blue.
False
6
inv-proof
[(((((((triple7 ((triple7) -> rule7)) -> rule2)) -> rule9)) -> rule1))]
("Harry" "is" "blue" "-")
((((((triple7 ((triple7) -> (rule7 % int4))) -> (rule2 % int3))) -> (rule9 % int2))) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is white.
("Harry" "is" "white" "+")
int4
Harry is red.
True
11
proof
[(((((triple7 ((triple7) -> rule7)) -> rule2) ((((((triple7 ((triple7) -> rule7)) -> rule2)) -> rule9)) -> rule1)) -> rule8))]
("Harry" "is" "red" "+")
((((triple7 ((triple7) -> (rule7 % int5))) -> (rule2 % int4)) ((((((triple7 ((triple7) -> (rule7 % int5))) -> (rule2 % int4))) -> (rule9 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is quiet.
("Harry" "is" "quiet" "+")
int4
Harry is white.
("Harry" "is" "white" "+")
int5
Harry is not red.
False
11
inv-proof
[(((((triple7 ((triple7) -> rule7)) -> rule2) ((((((triple7 ((triple7) -> rule7)) -> rule2)) -> rule9)) -> rule1)) -> rule8))]
("Harry" "is" "red" "-")
((((triple7 ((triple7) -> (rule7 % int5))) -> (rule2 % int4)) ((((((triple7 ((triple7) -> (rule7 % int5))) -> (rule2 % int4))) -> (rule9 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is quiet.
("Harry" "is" "quiet" "+")
int4
Harry is white.
("Harry" "is" "white" "+")
int5
Gary is not red.
Unknown
inv-rconc
[@1: Gary is red.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Gary" "is" "red" "-")
Fiona is red.
Unknown
rconc
[@1: Fiona is red.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Fiona" "is" "red" "+")
Erin is not red.
Unknown
inv-rconc
[@1: Erin is red.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Erin" "is" "red" "-")
Gary is blue.
Unknown
random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "+")
Fiona is not blue.
Unknown
inv-random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "-")
Gary is green.
Unknown
random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "+")
Harry is not green.
Unknown
inv-random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "-")
Erin is blue.
Unknown
random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "+")
Erin is not green.
Unknown
inv-random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "-")
Fiona is nice.
Unknown
random
[@0: Fiona is nice.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "nice" "+")
@0: Erin is kind.[(triple1 OR ((((triple2) -> rule6)) -> rule3))] Erin is nice.[(triple2)] Fiona is green.[(triple3 OR ((((triple4 ((triple4) -> rule7)) -> rule2) ((triple4) -> rule7)) -> rule5))] Fiona is kind.[(triple4)] Gary is kind.[(triple5)] Gary is not nice.[(triple6)] Harry is kind.[(triple7)] @1: Erin is white.[(((triple1) -> rule7) OR ((triple2) -> rule6))] Fiona is white.[(((triple4) -> rule7))] Gary is white.[(((triple5) -> rule7))] Harry is white.[(((triple7) -> rule7))] @2: Erin is quiet.[(((triple1 ((triple1) -> rule7)) -> rule2) OR ((triple1 ((triple2) -> rule6)) -> rule2) OR ((((((triple2) -> rule6)) -> rule3) ((triple1) -> rule7)) -> rule2) OR ((((((triple2) -> rule6)) -> rule3) ((triple2) -> rule6)) -> rule2))] Fiona is quiet.[(((triple4 ((triple4) -> rule7)) -> rule2))] Gary is quiet.[(((((triple5) -> rule7)) -> rule4) OR ((triple5 ((triple5) -> rule7)) -> rule2))] Harry is quiet.[(((triple7 ((triple7) -> rule7)) -> rule2))] @3: Harry is nice.[(((((triple7 ((triple7) -> rule7)) -> rule2)) -> rule9))] @4: Harry is blue.[(((((((triple7 ((triple7) -> rule7)) -> rule2)) -> rule9)) -> rule1))] @5: Harry is red.[(((((triple7 ((triple7) -> rule7)) -> rule2) ((((((triple7 ((triple7) -> rule7)) -> rule2)) -> rule9)) -> rule1)) -> rule8))]
Erin is kind.
("Erin" "is" "kind" "+")
triple1
((((triple2) -> (rule6 % int2))) -> (rule3 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
triple2
Fiona is green.
("Fiona" "is" "green" "+")
triple3
((((triple4 ((triple4) -> (rule7 % int3))) -> (rule2 % int2)) ((triple4) -> (rule7 % int3))) -> (rule5 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
int3
Fiona is kind.
("Fiona" "is" "kind" "+")
triple4
Gary is kind.
("Gary" "is" "kind" "+")
triple5
Gary is not nice.
("Gary" "is" "nice" "-")
triple6
Harry is kind.
("Harry" "is" "kind" "+")
triple7
Erin is white.
("Erin" "is" "white" "+")
((triple1) -> (rule7 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((triple2) -> (rule6 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
((triple4) -> (rule7 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
((triple5) -> (rule7 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
((triple7) -> (rule7 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
((triple1 ((triple1) -> (rule7 % int2))) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
((triple1 ((triple2) -> (rule6 % int2))) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
((((((triple2) -> (rule6 % int3))) -> (rule3 % int2)) ((triple1) -> (rule7 % int3))) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
((((((triple2) -> (rule6 % int3))) -> (rule3 % int2)) ((triple2) -> (rule6 % int3))) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((triple4 ((triple4) -> (rule7 % int2))) -> (rule2 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
((((triple5) -> (rule7 % int2))) -> (rule4 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
((triple5 ((triple5) -> (rule7 % int2))) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple7 ((triple7) -> (rule7 % int2))) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
((((triple7 ((triple7) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule9 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is blue.
("Harry" "is" "blue" "+")
((((((triple7 ((triple7) -> (rule7 % int4))) -> (rule2 % int3))) -> (rule9 % int2))) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is white.
("Harry" "is" "white" "+")
int4
Harry is red.
("Harry" "is" "red" "+")
((((triple7 ((triple7) -> (rule7 % int5))) -> (rule2 % int4)) ((((((triple7 ((triple7) -> (rule7 % int5))) -> (rule2 % int4))) -> (rule9 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is quiet.
("Harry" "is" "quiet" "+")
int4
Harry is white.
("Harry" "is" "white" "+")
int5