Erin is kind. Fiona is blue. Fiona is not quiet. Fiona is not white. Gary is quiet. Harry is blue. Harry is not kind. Harry is rough. Harry is round. Harry is white. If Gary is rough and Gary is not kind then Gary is not quiet. All round things are quiet. All quiet things are rough. All round things are rough. All red things are round. All quiet things are blue. Kind things are white. All kind, white things are red.
Erin is kind.
("Erin" "is" "kind" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is not quiet.
("Fiona" "is" "quiet" "-")
Fiona is not white.
("Fiona" "is" "white" "-")
Gary is quiet.
("Gary" "is" "quiet" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is not kind.
("Harry" "is" "kind" "-")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is white.
("Harry" "is" "white" "+")
If Gary is rough and Gary is not kind then Gary is not quiet.
((("Gary" "is" "rough" "+") ("Gary" "is" "kind" "~")) -> ("Gary" "is" "quiet" "-"))
All round things are quiet.
((("something" "is" "round" "+")) -> ("something" "is" "quiet" "+"))
All quiet things are rough.
((("something" "is" "quiet" "+")) -> ("something" "is" "rough" "+"))
All round things are rough.
((("something" "is" "round" "+")) -> ("something" "is" "rough" "+"))
All red things are round.
((("something" "is" "red" "+")) -> ("something" "is" "round" "+"))
All quiet things are blue.
((("something" "is" "quiet" "+")) -> ("something" "is" "blue" "+"))
Kind things are white.
((("something" "is" "kind" "+")) -> ("something" "is" "white" "+"))
All kind, white things are red.
((("something" "is" "kind" "+") ("something" "is" "white" "+")) -> ("something" "is" "red" "+"))
Harry is not kind.
True
1
proof
[(triple7)]
("Harry" "is" "kind" "-")
triple7
Harry is not blue.
False
1
inv-proof
[(triple6 OR ((((triple9) -> rule2)) -> rule6))]
("Harry" "is" "blue" "-")
triple6
((((triple9) -> (rule2 % int2))) -> (rule6 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Gary is rough.
True
2
proof
[(((triple5) -> rule3))]
("Gary" "is" "rough" "+")
((triple5) -> (rule3 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is not rough.
False
2
inv-proof
[(((triple5) -> rule3))]
("Gary" "is" "rough" "-")
((triple5) -> (rule3 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Erin is red.
True
4
proof
[(((triple1 ((triple1) -> rule7)) -> rule8))]
("Erin" "is" "red" "+")
((triple1 ((triple1) -> (rule7 % int2))) -> (rule8 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is not red.
False
4
inv-proof
[(((triple1 ((triple1) -> rule7)) -> rule8))]
("Erin" "is" "red" "-")
((triple1 ((triple1) -> (rule7 % int2))) -> (rule8 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is round.
True
5
proof
[(((((triple1 ((triple1) -> rule7)) -> rule8)) -> rule5))]
("Erin" "is" "round" "+")
((((triple1 ((triple1) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
Erin is not round.
False
5
inv-proof
[(((((triple1 ((triple1) -> rule7)) -> rule8)) -> rule5))]
("Erin" "is" "round" "-")
((((triple1 ((triple1) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
Erin is quiet.
True
6
proof
[(((((((triple1 ((triple1) -> rule7)) -> rule8)) -> rule5)) -> rule2))]
("Erin" "is" "quiet" "+")
((((((triple1 ((triple1) -> (rule7 % int4))) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
int4
Erin is not quiet.
False
6
inv-proof
[(((((((triple1 ((triple1) -> rule7)) -> rule8)) -> rule5)) -> rule2))]
("Erin" "is" "quiet" "-")
((((((triple1 ((triple1) -> (rule7 % int4))) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
int4
Erin is blue.
True
7
proof
[(((((((((triple1 ((triple1) -> rule7)) -> rule8)) -> rule5)) -> rule2)) -> rule6))]
("Erin" "is" "blue" "+")
((((((((triple1 ((triple1) -> (rule7 % int5))) -> (rule8 % int4))) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is red.
("Erin" "is" "red" "+")
int4
Erin is white.
("Erin" "is" "white" "+")
int5
Erin is not blue.
False
7
inv-proof
[(((((((((triple1 ((triple1) -> rule7)) -> rule8)) -> rule5)) -> rule2)) -> rule6))]
("Erin" "is" "blue" "-")
((((((((triple1 ((triple1) -> (rule7 % int5))) -> (rule8 % int4))) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is red.
("Erin" "is" "red" "+")
int4
Erin is white.
("Erin" "is" "white" "+")
int5
Gary is not round.
Unknown
inv-rconc
[@2: Gary is round.[CWA. Example of deepest failure = (rule5 <- rule8 <- FAIL)]]
("Gary" "is" "round" "-")
Fiona is red.
Unknown
rconc
[@1: Fiona is red.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Fiona" "is" "red" "+")
Gary is not red.
Unknown
inv-rconc
[@1: Gary is red.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Gary" "is" "red" "-")
Gary is white.
Unknown
rconc
[@1: Gary is white.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Gary" "is" "white" "+")
Fiona is not rough.
Unknown
inv-rconc
[@3: Fiona is rough.[CWA. Example of deepest failure = (rule4 <- rule5 <- rule8 <- FAIL)]]
("Fiona" "is" "rough" "-")
Harry is red.
Unknown
rconc
[@1: Harry is red.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Harry" "is" "red" "+")
Fiona is not kind.
Unknown
inv-random
[@0: Fiona is kind.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "kind" "-")
Gary is kind.
Unknown
random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "+")
@0: Erin is kind.[(triple1)] Fiona is blue.[(triple2)] Fiona is not quiet.[(triple3)] Fiona is not white.[(triple4)] Gary is quiet.[(triple5)] Harry is blue.[(triple6 OR ((((triple9) -> rule2)) -> rule6))] Harry is not kind.[(triple7)] Harry is rough.[(triple8 OR ((triple9) -> rule4) OR ((((triple9) -> rule2)) -> rule3))] Harry is round.[(triple9)] Harry is white.[(triple10)] @1: Erin is white.[(((triple1) -> rule7))] Gary is blue.[(((triple5) -> rule6))] Gary is rough.[(((triple5) -> rule3))] Harry is quiet.[(((triple9) -> rule2))] @2: Erin is red.[(((triple1 ((triple1) -> rule7)) -> rule8))] @3: Erin is round.[(((((triple1 ((triple1) -> rule7)) -> rule8)) -> rule5))] @4: Erin is quiet.[(((((((triple1 ((triple1) -> rule7)) -> rule8)) -> rule5)) -> rule2))] Erin is rough.[(((((((triple1 ((triple1) -> rule7)) -> rule8)) -> rule5)) -> rule4) OR ((((((((triple1 ((triple1) -> rule7)) -> rule8)) -> rule5)) -> rule2)) -> rule3))] @5: Erin is blue.[(((((((((triple1 ((triple1) -> rule7)) -> rule8)) -> rule5)) -> rule2)) -> rule6))]
Erin is kind.
("Erin" "is" "kind" "+")
triple1
Fiona is blue.
("Fiona" "is" "blue" "+")
triple2
Fiona is not quiet.
("Fiona" "is" "quiet" "-")
triple3
Fiona is not white.
("Fiona" "is" "white" "-")
triple4
Gary is quiet.
("Gary" "is" "quiet" "+")
triple5
Harry is blue.
("Harry" "is" "blue" "+")
triple6
((((triple9) -> (rule2 % int2))) -> (rule6 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is not kind.
("Harry" "is" "kind" "-")
triple7
Harry is rough.
("Harry" "is" "rough" "+")
triple8
((triple9) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((((triple9) -> (rule2 % int2))) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
triple9
Harry is white.
("Harry" "is" "white" "+")
triple10
Erin is white.
("Erin" "is" "white" "+")
((triple1) -> (rule7 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
((triple5) -> (rule6 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
((triple5) -> (rule3 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple9) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
((triple1 ((triple1) -> (rule7 % int2))) -> (rule8 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
((((triple1 ((triple1) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
Erin is quiet.
("Erin" "is" "quiet" "+")
((((((triple1 ((triple1) -> (rule7 % int4))) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
int4
Erin is rough.
("Erin" "is" "rough" "+")
((((((triple1 ((triple1) -> (rule7 % int4))) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
int4
((((((((triple1 ((triple1) -> (rule7 % int5))) -> (rule8 % int4))) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is red.
("Erin" "is" "red" "+")
int4
Erin is white.
("Erin" "is" "white" "+")
int5
Erin is blue.
("Erin" "is" "blue" "+")
((((((((triple1 ((triple1) -> (rule7 % int5))) -> (rule8 % int4))) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is red.
("Erin" "is" "red" "+")
int4
Erin is white.
("Erin" "is" "white" "+")
int5