Anne is blue. Anne is kind. Anne is nice. Anne is rough. Erin is blue. Erin is not rough. Erin is not young. Fiona is kind. Fiona is nice. Gary is kind. Gary is nice. All round people are not young. If someone is kind and young then they are rough. All kind people are rough. If someone is blue and nice then they are smart. If someone is rough then they are smart. All young, round people are kind. If someone is young then they are not kind. If Gary is smart then Gary is blue. All blue, kind people are round.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is not rough.
("Erin" "is" "rough" "-")
Erin is not young.
("Erin" "is" "young" "-")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is nice.
("Gary" "is" "nice" "+")
All round people are not young.
((("someone" "is" "round" "+")) -> ("someone" "is" "young" "-"))
If someone is kind and young then they are rough.
((("someone" "is" "kind" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "rough" "+"))
All kind people are rough.
((("someone" "is" "kind" "+")) -> ("someone" "is" "rough" "+"))
If someone is blue and nice then they are smart.
((("someone" "is" "blue" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "smart" "+"))
If someone is rough then they are smart.
((("someone" "is" "rough" "+")) -> ("someone" "is" "smart" "+"))
All young, round people are kind.
((("someone" "is" "young" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "kind" "+"))
If someone is young then they are not kind.
((("someone" "is" "young" "+")) -> ("someone" "is" "kind" "-"))
If Gary is smart then Gary is blue.
((("Gary" "is" "smart" "+")) -> ("Gary" "is" "blue" "+"))
All blue, kind people are round.
((("someone" "is" "blue" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "round" "+"))
Anne is rough.
True
1
proof
[(triple4 OR ((triple2) -> rule3))]
("Anne" "is" "rough" "+")
triple4
((triple2) -> (rule3 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Erin is rough.
False
1
inv-proof
[(triple6)]
("Erin" "is" "rough" "+")
triple6
Anne is smart.
True
2
proof
[(((triple4) -> rule5) OR ((triple1 triple3) -> rule4) OR ((((triple2) -> rule3)) -> rule5))]
("Anne" "is" "smart" "+")
((triple4) -> (rule5 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
((triple1 triple3) -> (rule4 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
((((triple2) -> (rule3 % int2))) -> (rule5 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Fiona is not rough.
False
2
inv-proof
[(((triple8) -> rule3))]
("Fiona" "is" "rough" "-")
((triple8) -> (rule3 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is smart.
True
3
proof
[(((((triple8) -> rule3)) -> rule5))]
("Fiona" "is" "smart" "+")
((((triple8) -> (rule3 % int2))) -> (rule5 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Gary is not smart.
False
3
inv-proof
[(((((triple10) -> rule3)) -> rule5))]
("Gary" "is" "smart" "-")
((((triple10) -> (rule3 % int2))) -> (rule5 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is blue.
True
4
proof
[(((((((triple10) -> rule3)) -> rule5)) -> rule8))]
("Gary" "is" "blue" "+")
((((((triple10) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is not blue.
False
4
inv-proof
[(((((((triple10) -> rule3)) -> rule5)) -> rule8))]
("Gary" "is" "blue" "-")
((((((triple10) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is round.
True
6
proof
[(((((((((triple10) -> rule3)) -> rule5)) -> rule8) triple10) -> rule9))]
("Gary" "is" "round" "+")
((((((((triple10) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule8 % int2)) triple10) -> (rule9 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is rough.
("Gary" "is" "rough" "+")
int4
Gary is not round.
False
6
inv-proof
[(((((((((triple10) -> rule3)) -> rule5)) -> rule8) triple10) -> rule9))]
("Gary" "is" "round" "-")
((((((((triple10) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule8 % int2)) triple10) -> (rule9 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is rough.
("Gary" "is" "rough" "+")
int4
Gary is not young.
True
7
proof
[(((((((((((triple10) -> rule3)) -> rule5)) -> rule8) triple10) -> rule9)) -> rule1))]
("Gary" "is" "young" "-")
((((((((((triple10) -> (rule3 % int5))) -> (rule5 % int4))) -> (rule8 % int3)) triple10) -> (rule9 % int2))) -> (rule1 % int1))
Gary is not young.
("Gary" "is" "young" "-")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
int4
Gary is rough.
("Gary" "is" "rough" "+")
int5
Gary is young.
False
7
inv-proof
[(((((((((((triple10) -> rule3)) -> rule5)) -> rule8) triple10) -> rule9)) -> rule1))]
("Gary" "is" "young" "+")
((((((((((triple10) -> (rule3 % int5))) -> (rule5 % int4))) -> (rule8 % int3)) triple10) -> (rule9 % int2))) -> (rule1 % int1))
Gary is not young.
("Gary" "is" "young" "-")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
int4
Gary is rough.
("Gary" "is" "rough" "+")
int5
Erin is not round.
Unknown
inv-rconc
[@2: Erin is round.[CWA. Example of deepest failure = (rule9 <- rule6 <- FAIL)]]
("Erin" "is" "round" "-")
Erin is smart.
Unknown
rconc
[@1: Erin is smart.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Erin" "is" "smart" "+")
Fiona is not round.
Unknown
inv-rconc
[@1: Fiona is round.[CWA. Example of deepest failure = (rule9 <- FAIL)]]
("Fiona" "is" "round" "-")
Erin is kind.
Unknown
rconc
[@1: Erin is kind.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Erin" "is" "kind" "+")
Fiona is not young.
Unknown
inv-random
[@0: Fiona is young.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "young" "-")
Fiona is blue.
Unknown
random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "+")
@0: Anne is blue.[(triple1)] Anne is kind.[(triple2)] Anne is nice.[(triple3)] Anne is rough.[(triple4 OR ((triple2) -> rule3))] Erin is blue.[(triple5)] Erin is not rough.[(triple6)] Erin is not young.[(triple7)] Fiona is kind.[(triple8)] Fiona is nice.[(triple9)] Gary is kind.[(triple10)] Gary is nice.[(triple11)] @1: Anne is round.[(((triple1 triple2) -> rule9))] Anne is smart.[(((triple4) -> rule5) OR ((triple1 triple3) -> rule4) OR ((((triple2) -> rule3)) -> rule5))] Fiona is rough.[(((triple8) -> rule3))] Gary is rough.[(((triple10) -> rule3))] @2: Anne is not young.[(((((triple1 triple2) -> rule9)) -> rule1))] Fiona is smart.[(((((triple8) -> rule3)) -> rule5))] Gary is smart.[(((((triple10) -> rule3)) -> rule5))] @3: Gary is blue.[(((((((triple10) -> rule3)) -> rule5)) -> rule8))] @4: Gary is round.[(((((((((triple10) -> rule3)) -> rule5)) -> rule8) triple10) -> rule9))] @5: Gary is not young.[(((((((((((triple10) -> rule3)) -> rule5)) -> rule8) triple10) -> rule9)) -> rule1))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is kind.
("Anne" "is" "kind" "+")
triple2
Anne is nice.
("Anne" "is" "nice" "+")
triple3
Anne is rough.
("Anne" "is" "rough" "+")
triple4
((triple2) -> (rule3 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
triple5
Erin is not rough.
("Erin" "is" "rough" "-")
triple6
Erin is not young.
("Erin" "is" "young" "-")
triple7
Fiona is kind.
("Fiona" "is" "kind" "+")
triple8
Fiona is nice.
("Fiona" "is" "nice" "+")
triple9
Gary is kind.
("Gary" "is" "kind" "+")
triple10
Gary is nice.
("Gary" "is" "nice" "+")
triple11
Anne is round.
("Anne" "is" "round" "+")
((triple1 triple2) -> (rule9 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
((triple4) -> (rule5 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
((triple1 triple3) -> (rule4 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
((((triple2) -> (rule3 % int2))) -> (rule5 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
((triple8) -> (rule3 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
((triple10) -> (rule3 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Anne is not young.
("Anne" "is" "young" "-")
((((triple1 triple2) -> (rule9 % int2))) -> (rule1 % int1))
Anne is not young.
("Anne" "is" "young" "-")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
((((triple8) -> (rule3 % int2))) -> (rule5 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
((((triple10) -> (rule3 % int2))) -> (rule5 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
((((((triple10) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is round.
("Gary" "is" "round" "+")
((((((((triple10) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule8 % int2)) triple10) -> (rule9 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is rough.
("Gary" "is" "rough" "+")
int4
Gary is not young.
("Gary" "is" "young" "-")
((((((((((triple10) -> (rule3 % int5))) -> (rule5 % int4))) -> (rule8 % int3)) triple10) -> (rule9 % int2))) -> (rule1 % int1))
Gary is not young.
("Gary" "is" "young" "-")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
int4
Gary is rough.
("Gary" "is" "rough" "+")
int5