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